mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g✝ h : G
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^∞⟮I, G; 𝕜⟯⟨g⟩
hX : ((𝒅ₕ ⋯) ((Derivation.evalAt 1) ↑X)) (Y f) = ((Derivation.evalAt g) ↑X) (Y f)
⊢ ((𝒅ₕ ⋯) ((Derivation.evalAt 1) ⁅↑X, ↑Y⁆)) f = ((Derivation.evalAt g) ⁅↑X, ↑Y⁆) f

Tactic:
have hY := Derivation.congr_fun (left_invariant' g Y) (X f)

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g✝ h : G
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^∞⟮I, G; 𝕜⟯⟨g⟩
hX : ((𝒅ₕ ⋯) ((Derivation.evalAt 1) ↑X)) (Y f) = ((Derivation.evalAt g) ↑X) (Y f)
hY : ((𝒅ₕ ⋯) ((Derivation.evalAt 1) ↑Y)) (X f) = ((Derivation.evalAt g) ↑Y) (X f)
⊢ ((𝒅ₕ ⋯) ((Derivation.evalAt 1) ⁅↑X, ↑Y⁆)) f = ((Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_1
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst✝⁷ : NormedAddCommGroup EM
inst✝⁶ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace HM M
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 : (fun x ↦ (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀
x : M
hx : x ∈ (fun x ↦ (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet
⊢ (fun x ↦ ↑(extChartAt IB (f x₀).proj) (f x).proj) x =
    (Prod.fst ∘ fun x ↦
        (↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).1,
          (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).2))
      x

Tactic:
simp_rw [Function.comp, OpenPartialHomeomorph.coe_toPartialEquiv, Trivialization.coe_coe]
    rw [Trivialization.coe_fst']
    exact hx

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_1.h
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s t : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization F TotalSpace.proj := ⋯
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
ht : (MDiffAt[u] fun b ↦ (↑e ⟨b, t b⟩).2) x₀
⊢ ∀ x ∈ e.baseSet, (fun b ↦ (↑e ⟨b, (s + t) b⟩).2) x = ((fun b ↦ (↑e ⟨b, s b⟩).2) + fun b ↦ (↑e ⟨b, t b⟩).2) x

Tactic:
exact fun x hx ↦ (e.linear 𝕜 hx).1 ..

Goal state after:
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ mlieBracket I (mulInvariantVectorField u) (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)) 1 =
    mlieBracket I (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField v)) (mulInvariantVectorField w)
        1 +
      mlieBracket I (mulInvariantVectorField v) (mlieBracket I (mulInvariantVectorField u) (mulInvariantVectorField w))
        1

Tactic:
apply leibniz_identity_mlieBracket_apply

Goal state after:
case hU
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, mulInvariantVectorField u x⟩) 1

case hV
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, mulInvariantVectorField v x⟩) 1

case hW
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, mulInvariantVectorField w x⟩) 1
Module: Mathlib.Topology.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
e✝ : α ≃ β
inst✝³ : TopologicalSpace β
inst✝² : AddCommMonoid β
inst✝¹ : Semiring R
inst✝ : Module R β
e : α ≃ β
this✝¹ : TopologicalSpace α := e.topologicalSpace
this✝ : AddCommMonoid α := e.addCommMonoid
this : Module R α := Equiv.module R e
⊢ Continuous (linearEquiv R e).invFun

Tactic:
exact continuous_coinduced_rng

Goal state after:
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
H : Type u_7
inst✝³ : TopologicalSpace H
G : Type u_9
inst✝² : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝¹ : TopologicalSpace M
N : Type u_13
inst✝ : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
⊢ ImmersionAtProp F I J M N f φ ψ → ImmersionAtProp F I J M N g φ ψ

Tactic:
by
    intro ⟨equiv, hf⟩
    refine ⟨equiv, EqOn.trans (fun x hx ↦ ?_) (hf.mono (by simp))⟩
    have : ((φ.extend I).symm) x ∈ φ.source := by simp_all
    grind

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) :=
  ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := φ₀.trans (PiLp.equivOfUnique 2 ℝ fun x ↦ ℝ)
hz : ↑z < y
⊢ ↑z ∈ (Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.source

Tactic:
by simp [Homeomorph.addLeft]

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ↑(projIcc x y ⋯ z) < y
this✝ :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x_1 ↦ w - x;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
this : max x (min y w) - x = w - x
⊢ (((Subtype.val ∘ ↑(IccLeftChart x y)) ∘ projIcc x y ⋯ ∘ ↑(chartAt ℝ z).symm) w).ofLp i =
    (have this := toLp 2 fun x_1 ↦ w - x;
        this).ofLp
      i

Tactic:
by
      simpa [modelWithCornersEuclideanHalfSpace, IccLeftChart]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case hxs
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
E' : Type u_6
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
inst✝³ : IsManifold I 2 M
inst✝² : IsManifold I' 2 M'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
A' : x₀ = ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)
h'f : MDiffAt[s] f x₀
this✝ : (mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse = mfderiv% ↑(extChartAt I x₀) x₀
V' : (x : E') → TangentSpace 𝓘(𝕜, E') x := mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) V (range ↑I')
hV' : V' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) V (range ↑I')
W' : (x : E') → TangentSpace 𝓘(𝕜, E') x := mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) W (range ↑I')
hW' : W' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) W (range ↑I')
F : E → E' := (↑(extChartAt I' (f x₀)) ∘ f) ∘ ↑(extChartAt I x₀).symm
hF : F = (↑(extChartAt I' (f x₀)) ∘ f) ∘ ↑(extChartAt I x₀).symm
hFx₀ : ↑(extChartAt I' (f x₀)) (f x₀) = F (↑(extChartAt I x₀) x₀)
Y : (x : M') → TangentSpace I' x
this : (extChartAt I x₀).target ∈ 𝓝[↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x₀) x₀
y : E
hy : y ∈ ↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I
h'''y : y ∈ (extChartAt I x₀).target
h'y : f (↑(extChartAt I x₀).symm y) ∈ (extChartAt I' (f x₀)).source
h''y : f (↑(extChartAt I x₀).symm y) ∈ (chartAt H' (f x₀)).source
huy : UniqueMDiffAt[↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I] y
⊢ UniqueMDiffAt[s] (↑(extChartAt I x₀).symm y)

Tactic:
exact hu _ hy.1

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : { x // x ∈ sphere 0 1 }
y✝ : E
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
⊢ ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y✝) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) v).symm)
    ((extChartAt (𝓡 n) v).target ∩ ↑(extChartAt (𝓡 n) v).symm ⁻¹' Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y✝).source)

Tactic:
exact
      ((contDiff_stereoInvFunAux.comp (ℝ ∙ (-v : E))ᗮ.subtypeL.contDiff).comp
          U.symm.contDiff).contDiffOn

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

Goal state before:
pp: case e'_12
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v) {t | t * a ∈ s}
⊢ s = {t | t * a⁻¹ ∈ {t | t * a ∈ s}}

Tactic:
· simp only [mem_ofPred_eq, mul_assoc, inv_mul_eq_div, div_self ha, mul_one, ofPred_mem_eq]

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun x ↦
    (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x))
      (v (↑(extChartAt I (γ t₀)).symm x))
hv' :
  v' = fun x ↦
    (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x))
      (v (↑(extChartAt I (γ t₀)).symm x))
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨γ t₀, v (γ t₀)⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I (γ t₀)).symm)
    (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 (↑(extChartAt I (γ t₀)) (γ t₀))
hlip : LipschitzOnWith K v' s
⊢ γ =ᶠ[𝓝 t₀] γ'

Tactic:
have hlip (t : ℝ) : LipschitzOnWith K ((fun _ ↦ v') t) ((fun _ ↦ s) t) := hlip

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun x ↦
    (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x))
      (v (↑(extChartAt I (γ t₀)).symm x))
hv' :
  v' = fun x ↦
    (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x))
      (v (↑(extChartAt I (γ t₀)).symm x))
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨γ t₀, v (γ t₀)⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I (γ t₀)).symm)
    (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 (↑(extChartAt I (γ t₀)) (γ t₀))
hlip✝ : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith K ((fun x ↦ v') t) ((fun x ↦ s) t)
⊢ γ =ᶠ[𝓝 t₀] γ'
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t | γ t = γ' t} ∩ Ioo a b
hs : s = {t | γ t = γ' t} ∩ Ioo a b
⊢ EqOn γ γ' (Ioo a b)

Tactic:
suffices hsub : Ioo a b ⊆ s from fun t ht ↦ mem_ofPred.mp ((subset_def ▸ hsub) t ht).1

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t | γ t = γ' t} ∩ Ioo a b
hs : s = {t | γ t = γ' t} ∩ Ioo a b
⊢ Ioo a b ⊆ s
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
⊢ ∀ᶠ (y : B) in 𝓝 x,
    ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
      r

Tactic:
let G := (trivializationAt F E x).continuousLinearEquivAt ℝ x h'x

Goal state after:
B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
⊢ ∀ᶠ (y : B) in 𝓝 x,
    ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
      r
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: case e'_2.e'_6
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
V : Opens M
hUV : V ≤ U
hV₀f : ∀ y ∈ Set.range (Set.inclusion hUV), f y ≠ 0
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion hUV))
hxV₀ : ⟨x, hxU⟩ ∈ Set.range (Set.inclusion hUV)
hxV : x ∈ ↑V
hVf : ∀ (y : ↥V), f (Set.inclusion hUV y) ≠ 0
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ := ⟨(⇑f ∘ Set.inclusion hUV)⁻¹, ?mpr.refine_1⟩
y : ↥(Opposite.unop (Opposite.op V))
⊢ ↑(g * (ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV) f) y = ↑1 y

Tactic:
apply inv_mul_cancel₀

Goal state after:
case e'_2.e'_6
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := ⋯
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
V : Opens M
hUV : V ≤ U
hV₀f : ∀ y ∈ Set.range (Set.inclusion hUV), f y ≠ 0
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion hUV))
hxV₀ : ⟨x, hxU⟩ ∈ Set.range (Set.inclusion hUV)
hxV : x ∈ ↑V
hVf : ∀ (y : ↥V), f (Set.inclusion hUV y) ≠ 0
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ := ⋯
y : ↥(Opposite.unop (Opposite.op V))
⊢ (⇑f ∘ Set.inclusion hUV) y ≠ 0
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
⊢ nonunits ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) = ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))

Tactic:
ext1 f

Goal state after:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
⊢ f ∈ nonunits ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) ↔ f ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁹ : NormedAddCommGroup EM
inst✝⁸ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝⁷ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace HM M
EN : Type u_3
inst✝⁴ : NormedAddCommGroup EN
inst✝³ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝² : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace HN N
f : M → N
hf : ContMDiff IM IN ∞ f
x : M
U : Opens ↑↑(locallyRingedSpace IN N).toPresheafedSpace
hxU : (ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base) x ∈ U
⊢ (locallyRingedSpace IN N).presheaf.germ U ((ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base) x) hxU ≫
      PresheafedSpace.Hom.stalkMap (locallyRingedSpaceMapAux f hf) x ≫ smoothSheafCommRing.evalHom IM 𝓘(𝕜, 𝕜) M 𝕜 x =
    (locallyRingedSpace IN N).presheaf.germ U ((ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base) x) hxU ≫
      smoothSheafCommRing.evalHom IN 𝓘(𝕜, 𝕜) N 𝕜 (f x)

Tactic:
rw [PresheafedSpace.stalkMap_germ_assoc]

Goal state after:
𝕜 : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁹ : NormedAddCommGroup EM
inst✝⁸ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝⁷ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace HM M
EN : Type u_3
inst✝⁴ : NormedAddCommGroup EN
inst✝³ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝² : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace HN N
f : M → N
hf : ContMDiff IM IN ∞ f
x : M
U : Opens ↑↑(locallyRingedSpace IN N).toPresheafedSpace
hxU : (ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base) x ∈ U
⊢ (locallyRingedSpaceMapAux f hf).c.app (Opposite.op U) ≫
      (locallyRingedSpace IM M).presheaf.germ ((Opens.map (locallyRingedSpaceMapAux f hf).base).obj U) x hxU ≫
        smoothSheafCommRing.evalHom IM 𝓘(𝕜, 𝕜) M 𝕜 x =
    (locallyRingedSpace IN N).presheaf.germ U ((ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base) x) hxU ≫
      smoothSheafCommRing.evalHom IN 𝓘(𝕜, 𝕜) N 𝕜 (f x)
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
⊢ SubmersionAtProp F I J M N f φ ψ → SubmersionAtProp F I J M N g φ ψ

Tactic:
by
    intro ⟨equiv, hf⟩
    refine ⟨equiv, EqOn.trans (fun x hx ↦ ?_) (hf.mono (by simp))⟩
    have : ((φ.extend I).symm) x ∈ φ.source := by simp_all
    grind

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
F : Type u_5
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : (x : M) → TopologicalSpace (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F n s u
hs' : ∀ (i : ι), ∀ x ∈ u, s i x = s' i x
i : ι
⊢ ∀ y ∈ u, ⟨y, s' i y⟩ = ⟨y, s i y⟩

Tactic:
simp +contextual [hs']

Goal state after: