diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean index 67910282..30811a11 100644 --- a/SphereEversion/Global/Gromov.lean +++ b/SphereEversion/Global/Gromov.lean @@ -29,12 +29,13 @@ variable {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] [FiniteDimens @[inherit_doc] local notation "J¹" => OneJetBundle IM M IX X +set_option backward.isDefEq.respectTransparency.types false in theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R) (hA : IsClosed A) (hδ_pos : ∀ x, 0 < δ x) (hδ_cont : Continuous δ) : R.SatisfiesHPrinciple A δ := by borelize EX - letI := manifoldMetric IM M - haveI := Manifold.locallyCompact_of_finiteDimensional (M := M) (I := IM) - haveI := Manifold.locallyCompact_of_finiteDimensional (M := X) (I := IX) + let := manifoldMetric IM M + have := Manifold.locallyCompact_of_finiteDimensional (M := M) (I := IM) + have := Manifold.locallyCompact_of_finiteDimensional (M := X) (I := IX) refine RelMfld.satisfiesHPrinciple_of_weak hA fun A hA 𝓕₀ h𝓕₀ ↦ ?_ obtain (hM | hM) := isEmpty_or_nonempty M · refine ⟨emptyHtpyFormalSol R, ?_, ?_, ?_, ?_⟩ <;> intro @@ -201,13 +202,11 @@ variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimens {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M'] [SigmaCompactSpace M'] [T2Space M'] -/- -Since every (σ-compact) manifold is metrizable, the metric space assumption can be removed. --/ +/- Since every (σ-compact) manifold is metrizable, the metric space assumption can be removed. -/ /-- Gromov's Theorem without metric space assumption -/ theorem RelMfld.Ample.satisfiesHPrincipleWith' {R : RelMfld IM M I' M'} (hRample : R.Ample) (hRopen : IsOpen R) (hC : IsClosed C) (hδ_pos : ∀ x, 0 < δ x) (hδ_cont : Continuous δ) : letI := manifoldMetric I' M' R.SatisfiesHPrincipleWith IP C δ := by - letI := manifoldMetric I' M' + let := manifoldMetric I' M' apply RelMfld.Ample.satisfiesHPrincipleWith <;> assumption diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index 29dbb9be..bec87cc3 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -85,7 +85,7 @@ theorem immersionRel_ample (h : finrank ℝ E < finrank ℝ E') : (immersionRel rw [RelMfld.ample_iff] rintro ⟨⟨m, m'⟩, φ : TangentSpace% m →L[ℝ] TangentSpace% m'⟩ (p : DualPair (TangentSpace% m)) (hφ : Injective φ) - haveI : FiniteDimensional ℝ (TangentSpace% m) := (by infer_instance : FiniteDimensional ℝ E) + have : FiniteDimensional ℝ (TangentSpace% m) := inferInstanceAs <| FiniteDimensional ℝ E have hcodim := one_lt_rank_of_rank_lt_rank p.ker_pi_ne_top h φ.toLinearMap rw [immersionRel_slice_eq I I' hφ] exact AmpleSet.of_one_lt_codim hcodim @@ -132,7 +132,7 @@ variable {n : ℕ} (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] theorem immersion_inclusion_sphere : Immersion (𝓡 n) 𝓘(ℝ, E) (fun x : sphere (0 : E) 1 ↦ (x : E)) ∞ where contMDiff := contMDiff_coe_sphere.of_le le_top - diff_injective := mfderiv_coe_sphere_injective + diff_injective := injective_mvfderiv_subtypeVal_sphere /-- The antipodal map on `𝕊^n ⊆ ℝ^{n+1}` is an immersion. -/ theorem immersion_antipodal_sphere : Immersion (𝓡 n) 𝓘(ℝ, E) @@ -144,7 +144,7 @@ theorem immersion_antipodal_sphere : Immersion (𝓡 n) 𝓘(ℝ, E) diff_injective x := by change Injective (mfderiv% (-fun x : sphere (0 : E) 1 ↦ (x : E)) x) rw [mfderiv_neg] - exact neg_injective.comp (mfderiv_coe_sphere_injective x) + exact neg_injective.comp (injective_mvfderiv_subtypeVal_sphere x) end sanitycheck @@ -191,7 +191,7 @@ def formalEversionAux : FamilyOneJetSec (𝓡 2) 𝕊² 𝓘(ℝ, E) E 𝓘(ℝ, /-- A formal eversion of a two-sphere into its ambient Euclidean space. -/ def formalEversionAux2 : HtpyFormalSol 𝓡_imm := { formalEversionAux E ω with - is_sol' := fun t x ↦ (ω.isometry_rot t x).injective.comp (mfderiv_coe_sphere_injective x) } + is_sol' t x := (ω.isometry_rot t x).injective.comp (injective_mvfderiv_subtypeVal_sphere x) } def formalEversion : HtpyFormalSol 𝓡_imm := (formalEversionAux2 E ω).reindex ⟨smoothStep, contMDiff_iff_contDiff.mpr smoothStep.smooth⟩ @@ -206,6 +206,7 @@ theorem formalEversion_zero (x : 𝕊²) : (formalEversion E ω 0).bs x = x := b theorem formalEversion_one (x : 𝕊²) : (formalEversion E ω 1).bs x = -x := by simp +set_option backward.isDefEq.respectTransparency.types false in theorem formalEversionHolAtZero {t : ℝ} (ht : t < 1 / 4) : (formalEversion E ω t).toOneJetSec.IsHolonomic := by intro x @@ -232,7 +233,7 @@ theorem formalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) : erw [mfderiv_neg, ContinuousLinearMap.coe_comp, Function.comp_apply, _root_.neg_apply, smoothStep.of_gt ht] rw [ω.rot_one]; · rfl - rw [← range_mfderiv_coe_sphere (n := 2) x] + rw [← range_mvfderiv_subtypeVal (n := 2) x] exact LinearMap.mem_range_self .. theorem formalEversion_hol_near_zero_one : @@ -308,13 +309,13 @@ theorem sphere_eversion : ((stdOrthonormalBasis _ _).reindex <| finCongr (Fact.out : finrank ℝ E = 3)).toBasis.orientation have rankE : finrank ℝ E = 3 := Fact.out - haveI : FiniteDimensional ℝ E := FiniteDimensional.of_finrank_eq_succ rankE + have : FiniteDimensional ℝ E := FiniteDimensional.of_finrank_eq_succ rankE have ineq_rank : finrank ℝ (EuclideanSpace ℝ (Fin 2)) < finrank ℝ E := by simp [rankE] let ε : 𝕊² → ℝ := fun _ ↦ 1 have hε_pos : ∀ x, 0 < ε x := fun _ ↦ zero_lt_one have hε_cont : Continuous ε := continuous_const - haveI : Nontrivial E := nontrivial_of_finrank_eq_succ (Fact.out : finrank ℝ E = 3) - haveI : Nonempty (sphere 0 1 : Set E) := + have : Nontrivial E := nontrivial_of_finrank_eq_succ (Fact.out : finrank ℝ E = 3) + have : Nonempty (sphere 0 1 : Set E) := (NormedSpace.sphere_nonempty.mpr zero_le_one).to_subtype rcases(immersionRel_satisfiesHPrincipleWith (𝓡 2) 𝕊² 𝓘(ℝ, E) E 𝓘(ℝ, ℝ) ℝ ineq_rank ((Finite.isClosed (by simp : ({0, 1} : Set ℝ).Finite)).prod isClosed_univ) hε_pos diff --git a/SphereEversion/Global/Localisation.lean b/SphereEversion/Global/Localisation.lean index d1f7f928..687887f8 100644 --- a/SphereEversion/Global/Localisation.lean +++ b/SphereEversion/Global/Localisation.lean @@ -24,6 +24,7 @@ Now we really bridge the gap all the way to vector spaces. variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] +set_option backward.isDefEq.respectTransparency.types false in /-- Convert a 1-jet section between vector spaces seen as manifold to a 1-jet section between those vector spaces. -/ def OneJetSec.loc (F : OneJetSec 𝓘(ℝ, E) E 𝓘(ℝ, E') E') : JetSec E E' where @@ -68,6 +69,7 @@ section Unloc variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] +set_option backward.isDefEq.respectTransparency.types false in /-- Convert a 1-jet section between vector spaces to a 1-jet section between those vector spaces seen as manifolds. -/ def JetSec.unloc (𝓕 : JetSec E E') : OneJetSec 𝓘(ℝ, E) E 𝓘(ℝ, E') E' where diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index 651331d0..ec4bb754 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -402,6 +402,7 @@ theorem ContMDiff.oneJetExt {f : M → M'} (hf : CMDiff ∞ f) : ContMDiff I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ (oneJetExt I I' f) := fun x ↦ ((hf x).contMDiffAt univ_mem).oneJetExt +set_option backward.isDefEq.respectTransparency.types false in theorem ContinuousAt.inTangentCoordinates_comp {f : N → M} {g : N → M'} {h : N → N'} {ϕ' : N → E' →L[𝕜] F'} {ϕ : N → E →L[𝕜] E'} {x₀ : N} (hg : ContinuousAt g x₀) : inTangentCoordinates I J' f h (fun x ↦ ϕ' x ∘L ϕ x) x₀ =ᶠ[𝓝 x₀] fun x ↦ @@ -428,6 +429,7 @@ variable (I') variable [IsManifold J ∞ N] +set_option backward.isDefEq.respectTransparency.types false in omit [IsManifold J' ∞ N'] in theorem ContMDiffAt.oneJet_comp {f1 : N' → M} (f2 : N' → M') {f3 : N' → N} {x₀ : N'} {h : ∀ x : N', OneJetSpace I' J (f2 x, f3 x)} {g : ∀ x : N', OneJetSpace I I' (f1 x, f2 x)} @@ -602,6 +604,7 @@ theorem partialEquiv_eq_equiv {α β} {f : PartialEquiv α β} {e : α ≃ β} ( @[inherit_doc] local notation "𝓜" => ModelProd (ModelProd H H') (E →L[𝕜] E') +set_option backward.isDefEq.respectTransparency.types false in /-- In the `OneJetBundle` to the model space, the charts are just the canonical identification between a product type and a bundle total space type, a.k.a. `Bundle.TotalSpace.toProd`. -/ @[simp, mfld_simps] @@ -620,6 +623,7 @@ theorem oneJetBundle_model_space_chartAt (p : OneJetBundle I H I' H') : OpenPartialHomeomorph.refl_prod_refl] rfl +set_option backward.isDefEq.respectTransparency.types false in @[simp, mfld_simps] theorem oneJetBundle_model_space_coe_chartAt (p : OneJetBundle I H I' H') : ⇑(chartAt 𝓜 p) = Bundle.TotalSpace.toProd (H × H') (E →L[𝕜] E') := by diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index 892d0fae..8a948d01 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -110,6 +110,7 @@ theorem isHolonomicAt_iff {F : OneJetSec I M I' M'} {x : M} : simp_rw [IsHolonomicAt, oneJetExt, Bundle.TotalSpace.ext_iff, heq_iff_eq, F.fst_eq, oneJetBundle_mk_fst, true_and, oneJetBundle_mk_snd] +set_option backward.isDefEq.respectTransparency.types false in theorem isHolonomicAt_congr {F F' : OneJetSec I M I' M'} {x : M} (h : F =ᶠ[𝓝 x] F') : F.IsHolonomicAt x ↔ F'.IsHolonomicAt x := by simp_rw [IsHolonomicAt] @@ -133,7 +134,7 @@ end OneJetSec def IsHolonomicGerm {x : M} (φ : Germ (𝓝 x) (OneJetBundle I M I' M')) : Prop := Quotient.liftOn' φ (fun F ↦ mfderiv% (fun x' ↦ (F x').1.2) x = (F x).2) (by - letI : Setoid (M → OneJetBundle I M I' M') := (𝓝 x).germSetoid (OneJetBundle I M I' M') + let : Setoid (M → OneJetBundle I M I' M') := (𝓝 x).germSetoid (OneJetBundle I M I' M') have key : ∀ f g, f ≈ g → diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean index 1b68ffe7..eff4d325 100644 --- a/SphereEversion/Global/Relation.lean +++ b/SphereEversion/Global/Relation.lean @@ -177,7 +177,7 @@ def RelMfld.slice (R : RelMfld I M I' M') (σ : OneJetBundle I M I' M') (p : Dua {w : TM' σ.1.2 | OneJetBundle.mk σ.1.1 σ.1.2 (p.update σ.2 w) ∈ R} omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in -/-- For some reason `rw [mem_setOf_eq]` fails after unfolding `slice`, +/-- For some reason `rw [mem_ofPred_eq]` fails after unfolding `slice`, but rewriting with this lemma works. -/ theorem mem_slice {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'} {p : DualPair <| TM σ.1.1} {w : TM' σ.1.2} : w ∈ R.slice σ p ↔ OneJetBundle.mk σ.1.1 σ.1.2 (p.update σ.2 w) ∈ R := @@ -198,6 +198,7 @@ theorem slice_mk_update {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'} def RelMfld.Ample (R : RelMfld I M I' M') : Prop := ∀ ⦃σ : OneJetBundle I M I' M'⦄ (p : DualPair <| TM σ.1.1), AmpleSet (R.slice σ p) +set_option backward.isDefEq.respectTransparency.types false in omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in theorem RelMfld.ample_iff (R : RelMfld I M I' M') : R.Ample ↔ @@ -349,8 +350,7 @@ def RelMfld.SatisfiesHPrinciple (R : RelMfld I M IX X) (C : Set M) (ε : M → theorem RelMfld.satisfiesHPrinciple_of_weak [FiniteDimensional ℝ E] [T2Space M] [SigmaCompactSpace M] {R : RelMfld I M IX X} {ε : M → ℝ} {C : Set M} (hC : IsClosed C) (h : ∀ A : Set M, IsClosed A → R.SatisfiesHPrincipleWeak A ε) : R.SatisfiesHPrinciple C ε := by - haveI := Manifold.metrizableSpace I M - letI : MetricSpace M := TopologicalSpace.metrizableSpaceMetric M + have := Manifold.metrizableSpace I M intro 𝓕₀ h𝓕₀ obtain ⟨C', hCC', hC', h𝓕₀C'⟩ := h𝓕₀.closed_neighborhood hC obtain ⟨𝓕, h1, h2, h3, h4⟩ := h C' hC' 𝓕₀ h𝓕₀C' @@ -480,6 +480,7 @@ theorem OpenSmoothEmbedding.smooth_transfer : theorem OneJetBundle.continuous_transfer : Continuous (φ.transfer ψ) := (OpenSmoothEmbedding.smooth_transfer _ _).continuous +set_option backward.isDefEq.respectTransparency.types false in omit [IsManifold IX ∞ X] [IsManifold IM ∞ M] [IsManifold IY ∞ Y] [IsManifold IN ∞ N] in theorem OpenSmoothEmbedding.range_transfer : @@ -706,6 +707,7 @@ theorem Jupdate_bs (F : OneJetSec IM M IN N) (G : HtpyOneJetSec IX X IY Y) (t : if x ∈ range φ then _ else _ split_ifs <;> rfl +set_option backward.isDefEq.respectTransparency.types false in theorem Jupdate_localize {F : OneJetSec IM M IN N} {G : HtpyOneJetSec IX X IY Y} (hK : IsCompact K) (hFG : ∀ t, ∀ x ∉ K, F (φ x) = (OneJetBundle.embedding φ ψ) (G t x)) (t : ℝ) (rg : range ((φ.Jupdate ψ F G hK hFG t).bs ∘ φ) ⊆ range ψ) (x : X) : diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean index 542e9ea7..8ad573eb 100644 --- a/SphereEversion/Global/TwistOneJetSec.lean +++ b/SphereEversion/Global/TwistOneJetSec.lean @@ -208,6 +208,7 @@ theorem FamilyOneJetEuclSec.contMDiff (s : FamilyOneJetEuclSec I M V J N) : variable {V'} +set_option backward.isDefEq.respectTransparency.types false in def familyJoin {f : N × M → V} (hf : CMDiff ∞ f) (s : FamilyOneJetEuclSec I M V J N) : FamilyOneJetSec I M 𝓘(ℝ, V) V J N where diff --git a/SphereEversion/Indexing.lean b/SphereEversion/Indexing.lean index 08aba2c4..158dda6e 100644 --- a/SphereEversion/Indexing.lean +++ b/SphereEversion/Indexing.lean @@ -64,7 +64,6 @@ theorem Set.countable_iff_exists_nonempty_indexType_equiv {α : Type*} {s : Set · refine ⟨fun hh ↦ ⟨0, ?_⟩, ?_⟩ · simp only [indexType_zero] obtain ⟨_i⟩ := Set.countable_infinite_iff_nonempty_denumerable.mp ⟨hh, h⟩ - haveI := _i exact ⟨(Denumerable.eqv s).symm⟩ · rintro ⟨n, ⟨fn⟩⟩ have hn : n = 0 := by diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index 9e40a70b..1df3a5e0 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -93,6 +93,7 @@ theorem inductive_construction {X Y : Type*} [TopologicalSpace X] {N : ℕ} {U : convert (h₁f _ _ hn₀' x) using 1 exact Germ.coe_eq.mpr hn₀.symm +set_option backward.isDefEq.respectTransparency.types false in theorem inductive_construction_of_loc' {X Y : Type*} [EMetricSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] (P₀ P₀' P₁ : ∀ x : X, Germ (𝓝 x) Y → Prop) {f₀ : X → Y} (hP₀f₀ : ∀ x, P₀ x f₀ ∧ P₀' x f₀) diff --git a/SphereEversion/Local/AmpleRelation.lean b/SphereEversion/Local/AmpleRelation.lean index 914d62f1..b25dbc82 100644 --- a/SphereEversion/Local/AmpleRelation.lean +++ b/SphereEversion/Local/AmpleRelation.lean @@ -86,7 +86,7 @@ theorem slice_of_ker_eq_ker {θ : OneJet E F} {p p' : DualPair E} (hpp' : p.π = congr 2 abel ext w - simp only [slice, mem_setOf_eq, map_sub, vadd_eq_add, mem_vadd_set_iff_neg_vadd_mem, key] + simp only [slice, mem_ofPred_eq, map_sub, vadd_eq_add, mem_vadd_set_iff_neg_vadd_mem, key] have : -(φ p.v - φ p'.v) + w + (φ p.v - φ p'.v) = w := by abel rw [this] diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean index 247dcd86..7e351398 100644 --- a/SphereEversion/Local/SphereEversion.lean +++ b/SphereEversion/Local/SphereEversion.lean @@ -228,7 +228,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank rw [injOn_iff_injective] let j := (ℝ ∙ x)ᗮ.subtypeL let p'' : DualPair (ℝ ∙ x)ᗮ := ⟨p.π.comp j, ⟨v', v'_in⟩, hπv'⟩ - have eq : ((ℝ ∙ x)ᗮ : Set E).restrict (p'.update φ w) = p''.update (φ.comp j) w := by + have eq : ((ℝ ∙ x)ᗮ : Set E).domRestrict (p'.update φ w) = p''.update (φ.comp j) w := by ext z simp [p', j, DualPair.update, p''] have eq' : (p''.π.ker).map (φ.comp j : _ →ₛₗ[.id ℝ] F) = @@ -244,7 +244,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank erw [← this, map_comp] rw [eq, p''.injective_update_iff, mem_compl_iff, eq'] · exact Iff.rfl - rw [← show ((ℝ ∙ x)ᗮ : Set E).restrict φ = φ.comp j by ext; rfl] + rw [← show ((ℝ ∙ x)ᗮ : Set E).domRestrict φ = φ.comp j by ext; rfl] exact hφ.injective end AssumeFiniteDimensional @@ -415,7 +415,7 @@ theorem sphere_eversion_of_loc [Fact (dim E = 3)] : classical borelize E have rankE : (dim E = 3) := Fact.out - haveI : FiniteDimensional ℝ E := FiniteDimensional.of_finrank_eq_succ rankE + have : FiniteDimensional ℝ E := FiniteDimensional.of_finrank_eq_succ rankE let ω : Orientation ℝ E (Fin 3) := ((stdOrthonormalBasis _ _).reindex <| finCongr rankE).toBasis.orientation have is_closed_pair : IsClosed ({0, 1} : Set ℝ) := (by simp : ({0, 1} : Set ℝ).Finite).isClosed diff --git a/SphereEversion/Loops/Basic.lean b/SphereEversion/Loops/Basic.lean index 79f4fea7..5a7092b7 100644 --- a/SphereEversion/Loops/Basic.lean +++ b/SphereEversion/Loops/Basic.lean @@ -378,6 +378,7 @@ theorem ContDiff.partial_loop {γ : E → Loop F} {n : ℕ∞} (hγ_diff : 𝒞 variable [FiniteDimensional ℝ F] +set_option backward.isDefEq.respectTransparency.types false in theorem Loop.support_diff {γ : E → Loop F} : Loop.support (Loop.diff γ) ⊆ Loop.support γ := by unfold Loop.support erw [closure_compl, closure_compl] diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean index 876f19c2..3f79eb2a 100644 --- a/SphereEversion/Loops/DeltaMollifier.lean +++ b/SphereEversion/Loops/DeltaMollifier.lean @@ -125,7 +125,7 @@ theorem ContDiff.periodize {f : ℝ → E} {n : ℕ∞} (h : ContDiff ℝ n f) ( refine (ProperlyDiscontinuousVAdd.finite_disjoint_inter_image (isCompact_Icc : IsCompact <| Icc (y - 1) (y + 1)) h').subset ?_ intro i hi - rw [mem_setOf_eq] + rw [mem_ofPred_eq] apply Nonempty.mono _ hi gcongr · rw [show (e i : ℝ → ℝ) = VAdd.vadd i by ext x; exact add_comm x i] diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean index f767284f..06199ee6 100644 --- a/SphereEversion/Loops/Exists.lean +++ b/SphereEversion/Loops/Exists.lean @@ -155,7 +155,7 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : let U₁ : Set ℝ := Iio (4⁻¹ : ℝ) ∪ Ioi (3 / 4) let U : Set (E × ℝ × ℝ) := (fun x ↦ x.2.1) ⁻¹' Iio (4⁻¹ : ℝ) ∪ (fun x ↦ fract x.2.2) ⁻¹' U₁ have hUC : U ∈ 𝓝ˢ C := by - haveI hU : IsOpen U := by + have hU : IsOpen U := by refine (isOpen_Iio.preimage continuous_snd.fst).union ?_ refine ((isOpen_Iio.union isOpen_Ioi).preimage_fract ?_).preimage continuous_snd.snd exact fun _ ↦ Or.inr (show (3 / 4 : ℝ) < 1 by norm_num) diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean index 7dd0d5a1..44fc05a0 100644 --- a/SphereEversion/Loops/Surrounding.lean +++ b/SphereEversion/Loops/Surrounding.lean @@ -153,10 +153,10 @@ theorem surrounded_iff_mem_interior_convexHull_aff_basis [FiniteDimensional ℝ basis.coord_apply_combination_of_mem (Finset.mem_univ i) w_sum] exact w_pos i · rintro ⟨b, h₀, h₁, h₂, h₃⟩ - haveI : Fintype b := (finite_set_of_fin_dim_affineIndependent ℝ h₁).fintype + have : Fintype b := (finite_set_of_fin_dim_affineIndependent ℝ h₁).fintype have hb : Fintype.card b = d + 1 := by rw [← h₁.affineSpan_eq_top_iff_card_eq_finrank_add_one, Subtype.range_coe_subtype, - setOf_mem_eq, h₂] + ofPred_mem_eq, h₂] let p := ((↑) : _ → F) ∘ (Fintype.equivFinOfCardEq hb).symm have hp : b = range p := by ext x @@ -166,7 +166,7 @@ theorem surrounded_iff_mem_interior_convexHull_aff_basis [FiniteDimensional ℝ replace h₁ : AffineIndependent ℝ p := h₁.comp_embedding (Fintype.equivFinOfCardEq hb).symm.toEmbedding let basis : AffineBasis ι ℝ F := ⟨_, h₁, h₂⟩ - erw [basis.interior_convexHull, mem_setOf_eq] at h₃ + erw [basis.interior_convexHull, mem_ofPred_eq] at h₃ refine ⟨p, fun i ↦ basis.coord i f, ⟨h₁, h₃, ?_, ?_⟩, fun i ↦ h₀ (mem_range_self i)⟩ · exact basis.sum_coord_apply_eq_one f · erw [← Finset.univ.affineCombination_eq_linear_combination p _ @@ -216,7 +216,7 @@ theorem smooth_surrounding [FiniteDimensional ℝ F] {x : F} {p : ι → F} {w : have hxp : W' (x, p) ∈ V := by simp [W', V, hp, h.coord_eq_w, h.w_pos] have hA : IsOpen A := by simp only [A, affineBases_findim ι ℝ F hι] - exact isOpen_univ.prod isOpen_setOf_affineIndependent + exact isOpen_univ.prod isOpen_setOfPred_affineIndependent have hU₂ : IsOpen U := hW'.isOpen_inter_preimage hA hV have hU₃ : U ∈ 𝓝 (x, p) := mem_nhds_iff.mpr ⟨U, le_refl U, hU₂, Set.mem_inter (by simp [hp, A]) (mem_preimage.mpr hxp)⟩ @@ -238,7 +238,7 @@ theorem smooth_surroundingPts [FiniteDimensional ℝ F] {x : F} {p : ι → F} { SmoothAt' (uncurry W) yq ∧ SurroundingPts yq.1 yq.2 (W yq.1 yq.2) := by refine Exists.imp (fun W hW ↦ ?_) (smooth_surrounding h) rw [nhds_prod_eq] at hW ⊢ - have := (IsOpen.eventually_mem isOpen_setOf_affineIndependent h.indep).prod_inr (𝓝 x) + have := (IsOpen.eventually_mem isOpen_setOfPred_affineIndependent h.indep).prod_inr (𝓝 x) filter_upwards [hW, this]; rintro ⟨y, q⟩ ⟨hW, h2W, h3W, hq⟩ h2q exact ⟨hW, h2q, h2W, h3W, hq⟩ @@ -283,7 +283,7 @@ theorem eventually_surroundingPts_of_tendsto_of_tendsto {l : Filter X} {m : Filt have hV' : V ∈ 𝓝 (W' (q, v)) := (isOpen_set_pi finite_univ fun _ _ ↦ isOpen_Ioi).mem_nhds hxp have hA : IsOpen A := by simp only [A, affineBases_findim ι ℝ F hι] - exact isOpen_univ.prod isOpen_setOf_affineIndependent + exact isOpen_univ.prod isOpen_setOfPred_affineIndependent have hW' : ContinuousAt W' (q, v) := (smooth_barycentric ι ℝ F hι (n := 0)).continuousOn.continuousAt (mem_nhds_iff.mpr ⟨A, Subset.rfl, hA, hqv⟩) @@ -937,7 +937,7 @@ def ContinuousGerm {x : E} (φ : Germ (𝓝 x) (ℝ → Loop F)) : Prop := rw [nhds_prod_eq] apply mem_of_superset (Filter.prod_mem_prod h univ_mem) rintro ⟨x', p⟩ ⟨hx' : γ x' = γ' x', -⟩ - simp only [mem_setOf_eq, hx']) + simp only [mem_ofPred_eq, hx']) variable (g b Ω) omit [NormedSpace ℝ E] diff --git a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean index 1e19c0b7..96f375c4 100644 --- a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean +++ b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean @@ -90,7 +90,7 @@ theorem Subsingleton.reallyConvex [Subsingleton 𝕜] : ReallyConvex 𝕜 s := b · exact reallyConvex_empty · refine Or.inr fun w _ _ _ ↦ ?_ convert hz - haveI := Module.subsingleton 𝕜 E + have := Module.subsingleton 𝕜 E exact Subsingleton.elim .. theorem reallyConvex_iff_hull [Nontrivial 𝕜] : ReallyConvex 𝕜 s ↔ reallyConvexHull 𝕜 s ⊆ s := by @@ -108,6 +108,7 @@ theorem ReallyConvex.sum_mem [Nontrivial 𝕜] [IsOrderedRing 𝕜] ∑ i ∈ t, w i • z i ∈ s := reallyConvex_iff_hull.mp hs (sum_mem_reallyConvexHull h₀ h₁ hz) +set_option backward.isDefEq.respectTransparency.types false in theorem ReallyConvex.finsum_mem [Nontrivial 𝕜] [IsOrderedRing 𝕜] (hs : ReallyConvex 𝕜 s) {ι : Type*} {w : ι → 𝕜} {z : ι → E} (h₀ : ∀ i, 0 ≤ w i) (h₁ : ∑ᶠ i, w i = 1) (hz : ∀ i ∈ support w, z i ∈ s) : @@ -141,7 +142,7 @@ theorem ReallyConvex.preimageₛₗ (f : E →ₛₗ[σ.toRingHom] E') {s : Set ReallyConvex 𝕜 (f ⁻¹' s) := by -- this proof would be easier by casing on `s = ∅`, and cases subsingleton_or_nontrivial 𝕜' - · haveI : Subsingleton E' := Module.subsingleton 𝕜' E' + · have : Subsingleton E' := Module.subsingleton 𝕜' E' refine Subsingleton.set_cases ?_ ?_ s · simp_rw [preimage_empty, reallyConvex_empty] · simp_rw [preimage_univ, reallyConvex_univ] diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean index 9113be1b..d6e0f696 100644 --- a/SphereEversion/ToMathlib/ExistsOfConvex.lean +++ b/SphereEversion/ToMathlib/ExistsOfConvex.lean @@ -112,6 +112,7 @@ variable {H₁ M₁ H₂ M₂ : Type*} omit [FiniteDimensional ℝ E₁] [FiniteDimensional ℝ E₂] [IsManifold I₁ ∞ M₁] [IsManifold I₂ ∞ M₂] in +set_option backward.isDefEq.respectTransparency.types false in theorem reallyConvex_contMDiffAtProd {x : M₁} (n : ℕ∞) : ReallyConvex (smoothGerm I₁ x) {φ : Germ (𝓝 x) (M₂ → F) | φ.ContMDiffAtProd I₁ I₂ n} := by classical diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean index 83799bce..36e175a0 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean @@ -255,7 +255,7 @@ def ContMDiffAtProd {x : M₁} (φ : Germ (𝓝 x) (M₂ → F)) (n : ℕ∞) : rw [← nhds_prod_eq] at h apply mem_of_superset h rintro ⟨x', y'⟩ ⟨hx' : f x' = g x', -⟩ - simp only [mem_setOf_eq, uncurry_apply_pair] + simp only [mem_ofPred_eq, uncurry_apply_pair] apply congr_fun exacts [hx'.symm, hx'] @@ -273,7 +273,7 @@ quotient.lift_on' φ (λ f, ∀ y ∈ h⁻¹' {x}, ContMDiffAt I₄ I₃ n (g rw ← nhds_prod_eq at h, apply mem_of_superset h, rintros ⟨x', y'⟩ ⟨(hx' : f x' = g x'), -⟩, - simp only [mem_setOf_eq, uncurry_apply_pair], + simp only [mem_ofPred_eq, uncurry_apply_pair], apply congr_fun, }, exacts [hx'.symm, hx'] end) diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean index 5fc945ae..a719d8af 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean @@ -131,6 +131,7 @@ variable {B F B' K : Type*} {E : B → Type*} {f : K} [TopologicalSpace B'] namespace Trivialization -- attribute [simps base_set] trivialization.pullback +set_option backward.isDefEq.respectTransparency.types false in theorem pullback_symm (e : Trivialization F (π F E)) (x : B') : (e.pullback f).symm x = e.symm (f x) := by ext y diff --git a/SphereEversion/ToMathlib/SmoothBarycentric.lean b/SphereEversion/ToMathlib/SmoothBarycentric.lean index 0b07797f..e753822f 100644 --- a/SphereEversion/ToMathlib/SmoothBarycentric.lean +++ b/SphereEversion/ToMathlib/SmoothBarycentric.lean @@ -21,7 +21,7 @@ theorem affineBases_findim [Fintype ι] [Field k] [Module k M] [FiniteDimensiona (h : Fintype.card ι = Module.finrank k M + 1) : affineBases ι k P = {v | AffineIndependent k v} := by ext v - simp only [affineBases, mem_setOf_eq, and_iff_left_iff_imp] + simp only [affineBases, mem_ofPred_eq, and_iff_left_iff_imp] exact fun h_ind ↦ h_ind.affineSpan_eq_top_iff_card_eq_finrank_add_one.mpr h theorem mem_affineBases_iff [Fintype ι] [DecidableEq ι] [Nontrivial R] (b : AffineBasis ι R P) diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean index 8a55a784..004223f2 100644 --- a/SphereEversion/ToMathlib/Topology/Misc.lean +++ b/SphereEversion/ToMathlib/Topology/Misc.lean @@ -65,7 +65,7 @@ instance : ProperlyDiscontinuousVAdd ℤ ℝ := ⟨fun {K L} hK hL ↦ by rcases eq_empty_or_nonempty K with (rfl | hK') <;> rcases eq_empty_or_nonempty L with (rfl | hL') <;> - try simp only [image_empty, inter_self, setOf_false, finite_empty, empty_inter, inter_empty, + try simp only [image_empty, inter_self, ofPred_false, finite_empty, empty_inter, inter_empty, Set.not_nonempty_empty, image_inter_nonempty_iff] have hSK := (hK.isLUB_sSup hK').1 have hIK := (hK.isGLB_sInf hK').1 @@ -145,7 +145,7 @@ theorem IsOpen.preimage_fract' {s : Set ℝ} (hs : IsOpen s) (h2s : 0 ∈ s → rintro x ⟨hx, hx'⟩ obtain (hx'' | hx'') := le_or_gt (n : ℝ) x · apply hδ - rw [mem_setOf_eq, abs_eq_self.mpr (fract_nonneg x)] + rw [mem_ofPred_eq, abs_eq_self.mpr (fract_nonneg x)] exact fract_lt hx'' hx' · apply hε' exact ⟨one_sub_lt_fract (by linarith [min_le_right ε (1 / 2)]) (by linarith) hx'', @@ -301,13 +301,13 @@ theorem decode₂_locallyFinite {ι} [Encodable ι] {s : ι → Set α} (hs : Lo have : encode ⁻¹' {i : ℕ | ((s <$> decode₂ ι i).getD ∅ ∩ U).Nonempty} = {i : ι | (s i ∩ U).Nonempty} := by - simp_rw [preimage_setOf_eq, decode₂_encode, map_eq_map, map_some, getD_some] + simp_rw [preimage_ofPred_eq, decode₂_encode, map_eq_map, map_some, getD_some] rw [← this] at hU refine finite_of_finite_preimage hU ?_ intro n hn rw [← decode₂_ne_none_iff] intro h - simp_rw [mem_setOf_eq, h, map_eq_map, map_none, getD_none, empty_inter] at hn + simp_rw [mem_ofPred_eq, h, map_eq_map, map_none, getD_none, empty_inter] at hn exact (not_nonempty_empty hn).elim variable {X : Type*} [EMetricSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] @@ -327,7 +327,7 @@ theorem exists_locallyFinite_subcover_of_locally {C : Set X} (hC : IsClosed C) { precise_refinement_set hC (fun x : s ↦ interior (V x)) (fun x ↦ isOpen_interior) this obtain ⟨K, hCK, hK, hKW⟩ := exists_subset_iUnion_closed_subset hC (fun x : s ↦ hW x) (fun x _ ↦ hlW.point_finite x) hUW - haveI : Encodable s := hs.toEncodable + have : Encodable s := hs.toEncodable let K' : ℕ → Set X := fun n ↦ (K <$> decode₂ s n).getD ∅ let W' : ℕ → Set X := fun n ↦ (W <$> decode₂ s n).getD ∅ refine ⟨K', W', ?_, ?_, ?_, ?_, ?_, ?_⟩ @@ -430,7 +430,7 @@ theorem image_coe_eq_iff_eq_univ {s : Set α} {t : Set s} : ((↑) : s → α) ' convert coe_injective.image_injective.eq_iff; rw [coe_image_univ] theorem preimage_coe_eq_univ {s t : Set α} : ((↑) : s → α) ⁻¹' t = univ ↔ s ⊆ t := by - simp only [preimage_eq_univ_iff, range_coe_subtype, setOf_mem_eq] + simp end Subtype @@ -462,7 +462,7 @@ theorem point_finite_of_locallyFinite_coe_preimage {ι X : Type*} [TopologicalSp by_cases hx : x ∈ s · exact hf.point_finite ⟨x, hx⟩ · have : ∀ i, x ∉ f i := fun i hxf ↦ hx (hfs i hxf) - simp only [this, setOf_false, finite_empty] + simp [this] end ParacompactSpace diff --git a/SphereEversion/ToMathlib/Topology/Paracompact.lean b/SphereEversion/ToMathlib/Topology/Paracompact.lean index 4af67c28..f9d5f945 100644 --- a/SphereEversion/ToMathlib/Topology/Paracompact.lean +++ b/SphereEversion/ToMathlib/Topology/Paracompact.lean @@ -68,12 +68,12 @@ theorem exists_countable_locallyFinite_cover {ι X : Type*} [TopologicalSpace X] refine ⟨U n, hU'' n x hn, ?_⟩ let P : ι × ℝ → Prop := fun z ↦ ((↿B) (z : ι × ℝ) ∩ U n).Nonempty erw [(Equiv.Set.sep s P).symm.set_finite_iff] - simp only [Set.iUnion_inter, ← inter_setOf_eq_sep, s] + simp only [Set.iUnion_inter, ← inter_ofPred_eq_sep, s] refine (hU' n).iUnion (fun m _ ↦ Set.toFinite _) fun m hm ↦ ?_ rw [Set.eq_empty_iff_forall_notMem] intro z simp only [Finset.coe_image, mem_inter_iff, mem_image, Finset.mem_coe, SetCoe.exists, - mem_setOf_eq, not_and, exists₂_imp, and_imp] + mem_ofPred_eq, not_and, exists₂_imp, and_imp] rintro x hx₁ - rfl rw [Set.not_nonempty_iff_eq_empty] have := Set.inter_subset_inter_left (U n) (h₂ m ⟨x, hx₁⟩) diff --git a/lake-manifest.json b/lake-manifest.json index d55f6004..cf559274 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,17 +15,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f98b1aa39a570b402eef93d709b461924e2d6da1", + "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.33.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12", + "rev": "16f02aa7642864af59f1ff0e384a015994db9118", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d662197a9ca6f411c5738c45ec0192c786462f5d", + "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc", + "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "88679d088c9720c27ebdf2ba4dafe17341747f94", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.32.0", + "inputRev": "v4.33.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "SphereEversion", diff --git a/lakefile.toml b/lakefile.toml index f2a95077..5aafe34f 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -11,6 +11,7 @@ weak.linter.style.header = false [[require]] name = "mathlib" scope = "leanprover-community" +rev = "v4.33.0" [[require]] name = "checkdecls" diff --git a/lean-toolchain b/lean-toolchain index 2544c30c..6a884ba1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.32.0 \ No newline at end of file +leanprover/lean4:v4.33.0 \ No newline at end of file