From 95ab363e7d25d8b94093d4aac1711f94d98cca9c Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 24 Jan 2024 00:02:11 +0000 Subject: [PATCH] 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 --- Mathlib/Algebra/DirectLimit.lean | 2 +- Mathlib/Analysis/Analytic/Composition.lean | 2 +- Mathlib/GroupTheory/Perm/Cycle/Basic.lean | 4 ++-- Mathlib/Tactic/Rewrites.lean | 6 +++--- Mathlib/Topology/Homotopy/HomotopyGroup.lean | 22 +++++++++----------- lake-manifest.json | 2 +- lean-toolchain | 2 +- 7 files changed, 19 insertions(+), 21 deletions(-) diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean index 0785270864d78..5602d72fc5ffc 100644 --- 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 index 5bb25572b6e41..5ab5f2fb218ec 100644 --- 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 index 55466d735ae66..e25e4a5d2154e 100644 --- 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 index 6efc50765a575..9f3730cacc194 100644 --- 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 index aa0973165c5fc..3bf9198692c36 100644 --- 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 index 21197dc6ef9f9..8a83c2b2f9846 100644 --- 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 index 47fd8fbd2c40b..271fe10f7dbb4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-01-19 +leanprover/lean4:nightly-2024-01-22