chore: changes up to nightly-2024-01-22 (#9930)

This is a PR to `bump/v4.6.0`, incorporating the changes on `nightly-testing` up to `nightly-2024-01-22`. Note that for now this moves `aesop` to the `nightly-testing` branch. Once leanprover-community/aesop#97 lands we can move this back to `bump/v4.6.0`. This PR doesn't need to wait on that, however. Co-authored-by: Scott Morrison <[email protected]>
leanprover-community · Jan 24, 2024 · 95ab363 · 95ab363
1 parent 92344f4
commit 95ab363
Show file tree

Hide file tree

Showing 7 changed files with 19 additions and 21 deletions.
diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean
@@ -719,7 +719,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
         have := DirectedSystem.map_map (fun i j h => f' i j h) hij (le_refl j : j ≤ j)
         rw [this]
         exact sub_self _
-        exacts [Or.inr rfl, Or.inl rfl]
+        exacts [Or.inl rfl, Or.inr rfl]
     · refine' ⟨i, {⟨i, 1⟩}, _, isSupported_sub (isSupported_of.2 rfl) isSupported_one, _⟩
       · rintro k (rfl | h)
         rfl

diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean
@@ -1165,9 +1165,9 @@ def sigmaEquivSigmaPi (n : ℕ) :
       rw [get_of_eq (splitWrtComposition_join _ _ _)]
       · simp only [get_ofFn]
         rfl
-      · congr
       · simp only [map_ofFn]
         rfl
+      · congr
 #align composition.sigma_equiv_sigma_pi Composition.sigmaEquivSigmaPi
 
 end Composition

diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
@@ -1793,9 +1793,9 @@ theorem Disjoint.isConj_mul {α : Type*} [Finite α] {σ τ π ρ : Perm α} (hc
           · rw [mul_apply, mul_apply] at h
             rw [h, inv_apply_self, (hd1 x).resolve_left hxσ]
           · rwa [mul_apply, mul_apply, inv_apply_self, apply_eq_iff_eq]
+        · rwa [Subtype.coe_mk, mem_coe, mem_support]
         · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
             apply_mem_support, mem_support]
-        · rwa [Subtype.coe_mk, mem_coe, mem_support]
       · rw [mem_coe, ← apply_mem_support, mem_support] at hxτ
         rw [Set.union_apply_right hd1''.le_bot _, Set.union_apply_right hd1''.le_bot _]
         simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inr, comp_apply,
@@ -1804,9 +1804,9 @@ theorem Disjoint.isConj_mul {α : Type*} [Finite α] {σ τ π ρ : Perm α} (hc
           · rw [mul_apply, mul_apply] at h
             rw [inv_apply_self, h, (hd1 (τ x)).resolve_right hxτ]
           · rwa [mul_apply, mul_apply, inv_apply_self, apply_eq_iff_eq]
+        · rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]
         · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ,
             mem_coe, mem_support]
-        · rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]
 #align equiv.perm.disjoint.is_conj_mul Equiv.Perm.Disjoint.isConj_mul
 
 section FixedPoints

diff --git a/Mathlib/Tactic/Rewrites.lean b/Mathlib/Tactic/Rewrites.lean
@@ -32,10 +32,10 @@ namespace Lean.Meta
 
 /-- Extract the lemma, with arguments, that was used to produce a `RewriteResult`. -/
 -- This assumes that `r.eqProof` was constructed as:
--- `mkAppN (mkConst ``Eq.ndrec [u1, u2]) #[α, a, motive, h₁, b, h₂]`
--- and we want `h₂`.
+-- `mkApp6 (.const ``congrArg _) α eType lhs rhs motive heq`
+-- in `Lean.Meta.Tactic.Rewrite` and we want `heq`.
 def RewriteResult.by? (r : RewriteResult) : Option Expr :=
-  if r.eqProof.isAppOfArity ``Eq.ndrec 6 then
+  if r.eqProof.isAppOfArity ``congrArg 6 then
     r.eqProof.getArg! 5
   else
     none

diff --git a/Mathlib/Topology/Homotopy/HomotopyGroup.lean b/Mathlib/Topology/Homotopy/HomotopyGroup.lean
@@ -332,18 +332,16 @@ theorem homotopicFrom (i : N) {p q : Ω^ N X x} :
     obtain rfl | h := eq_or_ne j i
     · rw [H.eq_fst]; exacts [congr_arg p ((Cube.splitAt j).left_inv _), jH]
     · rw [p.2 _ ⟨j, jH⟩]; apply boundary; exact ⟨⟨j, h⟩, jH⟩
-    /- porting note: the following is indented two spaces more than it should be due to
-      strange behavior of `erw` -/
-    all_goals
-      intro
-      apply (homotopyFrom_apply _ _ _).trans
-      first
-      | rw [H.apply_zero]
-      | rw [H.apply_one]
-      first
-      | apply congr_arg p
-      | apply congr_arg q
-      apply (Cube.splitAt i).left_inv
+  all_goals
+    intro
+    apply (homotopyFrom_apply _ _ _).trans
+    first
+    | rw [H.apply_zero]
+    | rw [H.apply_one]
+    first
+    | apply congr_arg p
+    | apply congr_arg q
+    apply (Cube.splitAt i).left_inv
 #align gen_loop.homotopic_from GenLoop.homotopicFrom
 
 /-- Concatenation of two `GenLoop`s along the `i`th coordinate. -/

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "77d0b4a2399ef5716e98a936ce994708aae33ff2",
+   "rev": "7a0082b8286da58fb63d0abfe2a78b3c164bd62a",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "bump/v4.6.0",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-19
+leanprover/lean4:nightly-2024-01-22
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:nightly-2024-01-19
		leanprover/lean4:nightly-2024-01-22