merge nightly-testing

Aesop/RuleSet.lean

@@ -372,7 +372,7 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) :
   if let some decl := f.matchesSimpTheorem? then
     for h : i in [:rs.simpTheoremsArray.size] do
       have i_valid : i < simpTheoremsArray'.fst.size := by
-        simp_all [Membership.mem, simpTheoremsArray'.snd]
+        simp_all +zetaDelta [Membership.mem, simpTheoremsArray'.snd]
       let (name, simpTheorems) := simpTheoremsArray'.fst[i]
       if SimpTheorems.containsDecl simpTheorems decl then
         let origin := .decl decl (inv := false)
@@ -383,7 +383,7 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) :
         anyErased := true
   let simpTheoremsArray := simpTheoremsArray'.fst
   let simpTheoremsArrayNonempty : 0 < simpTheoremsArray.size := by
-    simp [simpTheoremsArray'.snd, rs.simpTheoremsArrayNonempty]
+    simp [simpTheoremsArray, simpTheoremsArray'.snd, rs.simpTheoremsArrayNonempty]
   let rs := { rs with
     localNormSimpRules, simpTheoremsArray, simpTheoremsArrayNonempty
   }

Aesop/Util/Basic.lean

@@ -79,7 +79,9 @@ open DiscrTree
 
 -- For `type = ∀ (x₁, ..., xₙ), T`, returns keys that match `T * ... *` (with
 -- `n` stars).
-def getConclusionDiscrTreeKeys (type : Expr) : MetaM (Array Key) :=
+
+def getConclusionDiscrTreeKeys (type : Expr) :
+    MetaM (Array Key) :=
   withoutModifyingState do
     let (_, _, conclusion) ← forallMetaTelescope type
     mkDiscrTreePath conclusion

AesopTest/List.lean

@@ -892,7 +892,7 @@ theorem last_append (l₁ l₂ : List α) (h : l₂ ≠ []) :
   last (l₁ ++ l₂) (append_ne_nil_of_right_ne_nil l₁ h) = last l₂ h := by
   induction l₁ <;> aesop
 
-theorem last_concat {a : α} (l : List α) : last (concat l a) (concat_ne_nil a l) = a := by
+theorem last_concat {a : α} (l : List α) : last (concat l a) (by exact X.concat_ne_nil a l) = a := by
   aesop
 
 @[simp] theorem last_singleton (a : α) : last [a] (cons_ne_nil a []) = a := rfl

AesopTest/RulePattern.lean

@@ -23,8 +23,8 @@ example (m n : Nat) : (↑m : Int) < 0 ∧ (↑n : Int) > 0 := by
   set_option aesop.check.script false in
   aesop!
   all_goals
-    guard_hyp fwd_1 : 0 ≤ (m : Int)
     guard_hyp fwd_2 : 0 ≤ (n : Int)
+    guard_hyp fwd_1 : 0 ≤ (m : Int)
     falso
 
 @[aesop safe forward (pattern := min x y)]

AesopTest/SaturatePerformance.lean

@@ -41,11 +41,11 @@ import Aesop
 error: unsolved goals
 α : Type u_1
 l0 l1 l2 : List α
-fwd : (l0 ++ l1).length ≥ 0
-fwd_1 : (l0 ++ l1 ++ l2).length ≥ 0
-fwd_2 : l2.length ≥ 0
-fwd_3 : l0.length ≥ 0
-fwd_4 : l1.length ≥ 0
+fwd : l1.length ≥ 0
+fwd_1 : (l0 ++ l1).length ≥ 0
+fwd_2 : (l0 ++ l1 ++ l2).length ≥ 0
+fwd_3 : l2.length ≥ 0
+fwd_4 : l0.length ≥ 0
 ⊢ (l0 ++ l1 ++ l2).length = l0.length + l1.length + l2.length
 -/
 #guard_msgs in