From d6727073b9c6e3c96d3e0427403f7d90699ebd87 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 2 Mar 2026 13:29:25 +0000 Subject: [PATCH 1/3] chore: more simp lemmas --- .../Topology/FiberBundle/Trivialization.lean | 21 +++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/Mathlib/Topology/FiberBundle/Trivialization.lean b/Mathlib/Topology/FiberBundle/Trivialization.lean index 82202cef4c4db4..5356fa7e13ce6f 100644 --- a/Mathlib/Topology/FiberBundle/Trivialization.lean +++ b/Mathlib/Topology/FiberBundle/Trivialization.lean @@ -122,9 +122,11 @@ theorem coe_fst' (ex : proj x ∈ e.baseSet) : (e x).1 = proj x := protected theorem eqOn : EqOn (Prod.fst ∘ e) proj e.source := fun _ hx => e.coe_fst hx +@[simp] theorem mk_proj_snd (ex : x ∈ e.source) : (proj x, (e x).2) = e x := Prod.ext (e.coe_fst ex).symm rfl +@[simp] theorem mk_proj_snd' (ex : proj x ∈ e.baseSet) : (proj x, (e x).2) = e x := Prod.ext (e.coe_fst' ex).symm rfl @@ -148,17 +150,19 @@ theorem proj_surjOn_baseSet [Nonempty F] : Set.SurjOn proj e.source e.baseSet := ⟨e.toPartialEquiv.symm (b, y), e.toPartialEquiv.map_target <| e.mem_target.2 hb, e.proj_symm_apply' hb⟩ +@[simp, mfld_simps] theorem apply_symm_apply {x : B × F} (hx : x ∈ e.target) : e (e.toPartialEquiv.symm x) = x := e.toPartialEquiv.right_inv hx +@[simp, mfld_simps] theorem apply_symm_apply' {b : B} {x : F} (hx : b ∈ e.baseSet) : e (e.toPartialEquiv.symm (b, x)) = (b, x) := e.apply_symm_apply (e.mem_target.2 hx) +@[simp, mfld_simps] theorem symm_apply_apply {x : Z} (hx : x ∈ e.source) : e.toPartialEquiv.symm (e x) = x := e.toPartialEquiv.left_inv hx -@[simp, mfld_simps] theorem symm_apply_mk_proj {x : Z} (ex : x ∈ e.source) : e.toPartialEquiv.symm (proj x, (e x).2) = x := by rw [← e.coe_fst ex, ← e.coe_coe, e.left_inv ex] @@ -214,6 +218,7 @@ theorem coe_coe_fst (hb : b ∈ e'.baseSet) : (e' y).1 = b := by theorem mk_mem_target {x : B} {y : F} : (x, y) ∈ e'.target ↔ x ∈ e'.baseSet := e'.mem_target +@[simp, mfld_simps] theorem symm_coe_proj {x : B} {y : F} (e' : Pretrivialization F (π F E)) (h : x ∈ e'.baseSet) : (e'.toPartialEquiv.symm (x, y)).1 = x := e'.proj_symm_apply' h @@ -246,15 +251,17 @@ theorem mk_symm (e : Pretrivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet TotalSpace.mk b (e.symm b y) = e.toPartialEquiv.symm (b, y) := by simp only [e.symm_apply hb, TotalSpace.mk_cast (e.proj_symm_apply' hb), TotalSpace.eta] +@[simp, mfld_simps] theorem symm_proj_apply (e : Pretrivialization F (π F E)) (z : TotalSpace F E) (hz : z.proj ∈ e.baseSet) : e.symm z.proj (e z).2 = z.2 := by rw [e.symm_apply hz, cast_eq_iff_heq, e.mk_proj_snd' hz, e.symm_apply_apply (e.mem_source.mpr hz)] +@[simp, mfld_simps] theorem symm_apply_apply_mk (e : Pretrivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : E b) : e.symm b (e ⟨b, y⟩).2 = y := e.symm_proj_apply ⟨b, y⟩ hb -@[simp] +@[simp, mfld_simps] theorem apply_mk_symm (e : Pretrivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : F) : e ⟨b, e.symm b y⟩ = (b, y) := by rw [e.mk_symm hb, e.apply_symm_apply (e.mk_mem_target.mpr hb)] @@ -420,6 +427,7 @@ protected theorem eqOn : EqOn (Prod.fst ∘ e) proj e.source := fun _x hx => e.c theorem mem_source : x ∈ e.source ↔ proj x ∈ e.baseSet := by rw [e.source_eq, mem_preimage] +@[simp, mfld_simps] theorem coe_fst' (ex : proj x ∈ e.baseSet) : (e x).1 = proj x := e.coe_fst (e.mem_source.2 ex) @@ -455,10 +463,12 @@ theorem proj_symm_apply' {b : B} {x : F} (hx : b ∈ e.baseSet) : theorem proj_surjOn_baseSet [Nonempty F] : Set.SurjOn proj e.source e.baseSet := e.toPretrivialization.proj_surjOn_baseSet +@[simp, mfld_simps] theorem apply_symm_apply {x : B × F} (hx : x ∈ e.target) : e (e.toOpenPartialHomeomorph.symm x) = x := e.toOpenPartialHomeomorph.right_inv hx +@[simp, mfld_simps] theorem apply_symm_apply' {b : B} {x : F} (hx : b ∈ e.baseSet) : e (e.toOpenPartialHomeomorph.symm (b, x)) = (b, x) := e.toPretrivialization.apply_symm_apply' hx @@ -633,13 +643,13 @@ protected theorem continuousOn : ContinuousOn e' e'.source := theorem coe_mem_source : ↑y ∈ e'.source ↔ b ∈ e'.baseSet := e'.mem_source -@[simp, mfld_simps] theorem coe_coe_fst (hb : b ∈ e'.baseSet) : (e' y).1 = b := e'.coe_fst (e'.mem_source.2 hb) theorem mk_mem_target {y : F} : (b, y) ∈ e'.target ↔ b ∈ e'.baseSet := e'.toPretrivialization.mem_target +@[simp, mfld_simps] theorem symm_apply_apply {x : TotalSpace F E} (hx : x ∈ e'.source) : e'.toOpenPartialHomeomorph.symm (e' x) = x := e'.toPartialEquiv.left_inv hx @@ -671,10 +681,12 @@ theorem mk_symm (e : Trivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) ( TotalSpace.mk b (e.symm b y) = e.toOpenPartialHomeomorph.symm (b, y) := e.toPretrivialization.mk_symm hb y +@[simp, mfld_simps] theorem symm_proj_apply (e : Trivialization F (π F E)) (z : TotalSpace F E) (hz : z.proj ∈ e.baseSet) : e.symm z.proj (e z).2 = z.2 := e.toPretrivialization.symm_proj_apply z hz +@[simp, mfld_simps] theorem symm_apply_apply_mk (e : Trivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : E b) : e.symm b (e ⟨b, y⟩).2 = y := e.symm_proj_apply ⟨b, y⟩ hb @@ -731,6 +743,7 @@ theorem coordChange_apply_snd (e₁ e₂ : Trivialization F proj) {p : Z} (h : p e₁.coordChange e₂ (proj p) (e₁ p).snd = (e₂ p).snd := by rw [coordChange, e₁.symm_apply_mk_proj (e₁.mem_source.2 h)] +@[simp, mfld_simps] theorem coordChange_same_apply (e : Trivialization F proj) {b : B} (h : b ∈ e.baseSet) (x : F) : e.coordChange e b x = x := by rw [coordChange, e.apply_symm_apply' h] @@ -888,7 +901,7 @@ noncomputable def piecewiseLe [LinearOrder B] [OrderTopology B] (e e' : Triviali e.piecewiseLeOfEq (e'.transFiberHomeomorph (e'.coordChangeHomeomorph e He' He)) a He He' <| by rintro p rfl ext1 - · simp [e.coe_fst', e'.coe_fst', *] + · simp [*] · simp [coordChange_apply_snd, *] open Classical in From 4e92f4e458a15e47e4f8cad595bf25678b3ca53b Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 2 Mar 2026 15:50:16 +0000 Subject: [PATCH 2/3] chore: rephrase a TODO --- the current phrasing took me a moment to parse --- Mathlib/Topology/FiberBundle/Trivialization.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/FiberBundle/Trivialization.lean b/Mathlib/Topology/FiberBundle/Trivialization.lean index 5356fa7e13ce6f..d87dcd82cb22aa 100644 --- a/Mathlib/Topology/FiberBundle/Trivialization.lean +++ b/Mathlib/Topology/FiberBundle/Trivialization.lean @@ -91,7 +91,7 @@ lemma ext' (e e' : Pretrivialization F proj) (h₁ : e.toPartialEquiv = e'.toPar (h₂ : e.baseSet = e'.baseSet) : e = e' := by cases e; cases e'; congr --- TODO: move `ext` here? +-- TODO: tag this lemma with the `ext` attribute instead? lemma ext {e e' : Pretrivialization F proj} (h₁ : ∀ x, e x = e' x) (h₂ : ∀ x, e.toPartialEquiv.symm x = e'.toPartialEquiv.symm x) (h₃ : e.baseSet = e'.baseSet) : e = e' := by From a2d3ce47156b31187b4741c7de5ae8f4747d91ec Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 2 Mar 2026 21:45:01 +0000 Subject: [PATCH 3/3] chore: general golfs using these lemmas --- Mathlib/Geometry/Manifold/VectorBundle/Hom.lean | 5 +---- Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean | 5 +---- Mathlib/Topology/FiberBundle/Constructions.lean | 4 ++-- Mathlib/Topology/VectorBundle/Hom.lean | 4 +--- 4 files changed, 5 insertions(+), 13 deletions(-) diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Hom.lean b/Mathlib/Geometry/Manifold/VectorBundle/Hom.lean index dea744880414bd..090fe8851e7ff6 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/Hom.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/Hom.lean @@ -197,10 +197,7 @@ lemma ContMDiffWithinAt.clm_apply_of_inCoordinates exact FiberBundle.mem_baseSet_trivializationAt' (b₂ m₀) filter_upwards [A, A'] with m hm h'm rw [inCoordinates_eq hm h'm] - simp only [coe_comp', ContinuousLinearEquiv.coe_coe, Trivialization.continuousLinearEquivAt_apply, - Trivialization.continuousLinearEquivAt_symm_apply, Function.comp_apply] - congr - rw [Trivialization.symm_apply_apply_mk (trivializationAt F₁ E₁ (b₁ m₀)) hm (v m)] + simp [*] /-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a base map `b₁ : M → B₁`, and another base map `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending smoothly diff --git a/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean b/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean index d280f01cc94216..1ceadc7c458466 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean @@ -696,10 +696,7 @@ lemma MDifferentiableWithinAt.clm_apply_of_inCoordinates exact FiberBundle.mem_baseSet_trivializationAt' (b₂ m₀) filter_upwards [A, A'] with m hm h'm rw [inCoordinates_eq hm h'm] - simp only [coe_comp', ContinuousLinearEquiv.coe_coe, Trivialization.continuousLinearEquivAt_apply, - Trivialization.continuousLinearEquivAt_symm_apply, Function.comp_apply] - congr - rw [Trivialization.symm_apply_apply_mk (trivializationAt F₁ E₁ (b₁ m₀)) hm (v m)] + simp [hm] /-- Consider a differentiable map `v : M → E₁` to a vector bundle, over a basemap `b₁ : M → B₁`, and another basemap `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending diff --git a/Mathlib/Topology/FiberBundle/Constructions.lean b/Mathlib/Topology/FiberBundle/Constructions.lean index 6945408397a7b8..ea3ff754950fb6 100644 --- a/Mathlib/Topology/FiberBundle/Constructions.lean +++ b/Mathlib/Topology/FiberBundle/Constructions.lean @@ -169,14 +169,14 @@ theorem Prod.left_inv {x : TotalSpace (F₁ × F₂) (E₁ ×ᵇ E₂)} Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x := by obtain ⟨x, v₁, v₂⟩ := x obtain ⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩ := h - simp only [Prod.toFun', Prod.invFun', symm_apply_apply_mk, h₁, h₂] + simp [Prod.toFun', Prod.invFun', h₁, h₂] theorem Prod.right_inv {x : B × F₁ × F₂} (h : x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ (univ : Set (F₁ × F₂))) : Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x := by obtain ⟨x, w₁, w₂⟩ := x obtain ⟨⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩, -⟩ := h - simp only [Prod.toFun', Prod.invFun', apply_mk_symm, h₁, h₂] + simp [Prod.toFun', Prod.invFun', h₁, h₂] theorem Prod.continuous_inv_fun : ContinuousOn (Prod.invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ) := by diff --git a/Mathlib/Topology/VectorBundle/Hom.lean b/Mathlib/Topology/VectorBundle/Hom.lean index f5c2ec5cce88b1..42dec06ced46db 100644 --- a/Mathlib/Topology/VectorBundle/Hom.lean +++ b/Mathlib/Topology/VectorBundle/Hom.lean @@ -357,9 +357,7 @@ lemma ContinuousWithinAt.clm_apply_of_inCoordinates apply hb₂ apply (trivializationAt F₂ E₂ (b₂ m₀)).open_baseSet.mem_nhds exact FiberBundle.mem_baseSet_trivializationAt' (b₂ m₀) - filter_upwards [A, A'] with m hm h'm - simp [inCoordinates_eq hm h'm, - Trivialization.symm_apply_apply_mk (trivializationAt F₁ E₁ (b₁ m₀)) hm (v m)] + filter_upwards [A, A'] with m hm h'm using by simp [inCoordinates_eq hm h'm, hm] /-- Consider a continuous map `v : M → E₁` to a vector bundle, over a base map `b₁ : M → B₁`, and