Squashed lean-pr-testing-3121

commit 05ed454 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Mon Jan 15 21:11:11 2024 +0000 Trigger CI for leanprover/lean4#3121 commit f984c96 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Mon Jan 15 19:02:16 2024 +0000 Trigger CI for leanprover/lean4#3121 commit 0dcffb9 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Mon Jan 15 17:27:43 2024 +0000 Trigger CI for leanprover/lean4#3121 commit 60c2d87 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Mon Jan 15 16:41:44 2024 +0000 Trigger CI for leanprover/lean4#3121 commit 5b3c8cb Author: leanprover-community-mathlib4-bot <[email protected]> Date: Mon Jan 15 14:54:42 2024 +0000 Trigger CI for leanprover/lean4#3121 commit 9cdd75f Author: Joachim Breitner <[email protected]> Date: Mon Jan 15 15:48:45 2024 +0100 Reduce diff to nightly-testing commit d85e0f1 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Mon Jan 15 14:35:23 2024 +0000 Trigger CI for leanprover/lean4#3121 commit 4239974 Merge: fee326a 2a84dcf Author: leanprover-community-mathlib4-bot <[email protected]> Date: Mon Jan 15 14:17:15 2024 +0000 Trigger CI for leanprover/lean4#3121 commit fee326a Author: leanprover-community-mathlib4-bot <[email protected]> Date: Mon Jan 8 13:40:55 2024 +0000 Trigger CI for leanprover/lean4#3121 commit 84a9d48 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Mon Jan 8 13:16:22 2024 +0000 Trigger CI for leanprover/lean4#3121 commit 27867dd Author: Joachim Breitner <[email protected]> Date: Mon Jan 8 12:42:07 2024 +0100 Try to fix rw? commit 5189cc8 Author: Joachim Breitner <[email protected]> Date: Mon Jan 8 12:39:41 2024 +0100 Trigger CI commit 9dd93f9 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Sat Dec 30 11:09:38 2023 +0000 Trigger CI for leanprover/lean4#3121 commit 0494ec5 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Thu Dec 28 18:22:37 2023 +0000 Trigger CI for leanprover/lean4#3121 commit aa43b20 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Thu Dec 28 15:48:58 2023 +0000 Trigger CI for leanprover/lean4#3121 commit af6cccb Author: Joachim Breitner <[email protected]> Date: Thu Dec 28 15:56:05 2023 +0100 Fix some fallout (reorder goals) commit cb55f12 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Thu Dec 28 12:32:36 2023 +0000 Trigger CI for leanprover/lean4#3121 commit 780f9f2 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Thu Dec 28 11:36:42 2023 +0000 Update lean-toolchain for testing leanprover/lean4#3121 commit 8e0fec8 Merge: a21ddd8 e352bb7 Author: leanprover-community-mathlib4-bot <[email protected]> Date: Thu Dec 21 09:30:49 2023 +0000 Merge master into nightly-testing commit a21ddd8 Author: Scott Morrison <[email protected]> Date: Thu Dec 21 19:37:19 2023 +1100 merge lean-pr-testing-2964
leanprover-community · Jan 20, 2024 · 5f2c304 · 5f2c304
1 parent c147d05
commit 5f2c304
Show file tree

Hide file tree

Showing 5 changed files with 17 additions and 19 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
@@ -31,10 +31,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. -/