mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Group.Growth.QuotientInter

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x ↦ x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' ↑A ^ m)
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' ↑A ^ m → φ a ∈ A ^ m
hπφ : ∀ {a : G ⧸ H}, a ∈ ⇑π '' ↑A ^ m → π (φ a) = a
a₁ b₁ : G
hb₁ : b₁ ∈ ↑A ^ m
ha₁ : a₁ ∈ H
a₂ b₂ : G
hb₂ : b₂ ∈ ↑A ^ m
ha₂ : a₂ ∈ H
hab : φ (π b₁) * a₁ = φ (π b₂) * a₂
hπa₁ : π a₁ = 1
⊢ φ (π b₁) = φ (π b₂) ∧ a₁ = a₂

Tactic:
have hπa₂ : π a₂ = 1 := (QuotientGroup.eq_one_iff _).2 ha₂

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x ↦ x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' ↑A ^ m)
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' ↑A ^ m → φ a ∈ A ^ m
hπφ : ∀ {a : G ⧸ H}, a ∈ ⇑π '' ↑A ^ m → π (φ a) = a
a₁ b₁ : G
hb₁ : b₁ ∈ ↑A ^ m
ha₁ : a₁ ∈ H
a₂ b₂ : G
hb₂ : b₂ ∈ ↑A ^ m
ha₂ : a₂ ∈ H
hab : φ (π b₁) * a₁ = φ (π b₂) * a₂
hπa₁ : π a₁ = 1
hπa₂ : π a₂ = 1
⊢ φ (π b₁) = φ (π b₂) ∧ a₁ = a₂
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
hX₁ : 1 ∈ {1}
hXclosure : (↑(closure ↑{1})).Infinite
⊢ StrictMono fun n ↦ {1} ^ n

Tactic:
simp [closure_singleton_one] at hXclosure

Goal state after:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ t₁.points i₁ ∈ altitude t₂ j₃

Tactic:
· rw [altitude_replace_orthocenter_eq_affineSpan hi₁₃ hi₁₂ hi₂₃.symm hj₁₃ hj₁₂ hj₂₃.symm h₁ h₃ h₂]
    exact mem_affineSpan ℝ (Set.mem_insert _ _)

Goal state after:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
⊢ Fintype.card ↑(Set.range t.points) ≤ Fintype.card ↑(Set.range p)

Tactic:
Set.card_range_of_injective hpi,

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
⊢ Fintype.card ↑(Set.range t.points) ≤ Fintype.card (Fin 3)
Module: Mathlib.Geometry.Manifold.Complex

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c
this : e.target ∈ 𝓝 (↑e c)
y : E
hyt : y ∈ e.target
hy₂ :
  ContinuousAt f (↑e.symm y) ∧
    DifferentiableWithinAt ℂ (↑(extChartAt 𝓘(ℂ, F) 0) ∘ f ∘ ↑(extChartAt I c).symm) univ (↑(extChartAt I c) (↑e.symm y))
hys : ↑e.symm y ∈ (chartAt H c).source
hfy : f (↑e.symm y) ∈ (chartAt F 0).source
⊢ DifferentiableAt ℂ (f ∘ ↑e.symm) y

Tactic:
differentiableWithinAt_univ,

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c
this : e.target ∈ 𝓝 (↑e c)
y : E
hyt : y ∈ e.target
hy₂ :
  ContinuousAt f (↑e.symm y) ∧
    DifferentiableAt ℂ (↑(extChartAt 𝓘(ℂ, F) 0) ∘ f ∘ ↑(extChartAt I c).symm) (↑(extChartAt I c) (↑e.symm y))
hys : ↑e.symm y ∈ (chartAt H c).source
hfy : f (↑e.symm y) ∈ (chartAt F 0).source
⊢ DifferentiableAt ℂ (f ∘ ↑e.symm) y
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

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
s : Set M
x : M
F : Type u_18
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : M → F
hf : MDiffAt[s] f x
⊢ DifferentiableWithinAt 𝕜 (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
by
  simpa [extChartAt_self_eq] using (mdifferentiableWithinAt_iff.1 hf).2

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
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
fg : G → TangentBundle I G := fun g ↦ ⟨g, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
⊢ ContMDiff I I.tangent (minSmoothness 𝕜 2) fun g ↦ ⟨g, mulInvariantVectorField v g⟩

Tactic:
let fv : G → TangentBundle I G := fun _ ↦ TotalSpace.mk' E 1 v

Goal state after:
𝕜 : 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
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
fg : G → TangentBundle I G := fun g ↦ ⟨g, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun x ↦ ⟨1, v⟩
⊢ ContMDiff I I.tangent (minSmoothness 𝕜 2) fun g ↦ ⟨g, mulInvariantVectorField v g⟩
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun x ↦ ⟨x, W x⟩) x
hs : UniqueMDiffAt[s] x
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := ⋯
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x := ⋯
f' : E → 𝕜 := ⋯
s' : Set E := ⋯
A : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := ⋯
B : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := ⋯
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (lieBracketWithin 𝕜 V' (f' • W') s') x =
    mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (fun y ↦ A y + B y) x

Tactic:
simp only [mpullback_apply]
    congr
    exact lieBracketWithin_smul_right (V := V') hf.differentiableWithinAt_comp_extChartAt_symm
      hW.differentiableWithinAt_mpullbackWithin_vectorField hs

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

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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W V₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDiffAt (T% V) x
hV₁ : MDiffAt (T% V₁) x
⊢ mlieBracketWithin I (V + V₁) W univ x = mlieBracketWithin I V W univ x + mlieBracketWithin I V₁ W univ x

Tactic:
exact mlieBracketWithin_add_left hV hV₁ (uniqueMDiffWithinAt_univ _)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
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
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f : M → N
φ : N → N'
h : IsImmersionAtOfComplement F J J' n φ (f x)
h' : ContMDiffAt I J' n (φ ∘ f) x
t : Set M
ht : t ⊆ f ⁻¹' h.domChart.source
hxt : x ∈ t
f' : E → E'' := ↑(h.domChart.extend J) ∘ f ∘ ↑(extChartAt I x).symm
⊢ ContDiffWithinAt 𝕜 n f' (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
set φ' := (h.codChart.extend J') ∘ φ ∘ (h.domChart.extend J).symm

Goal state after:
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
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
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f : M → N
φ : N → N'
h : IsImmersionAtOfComplement F J J' n φ (f x)
h' : ContMDiffAt I J' n (φ ∘ f) x
t : Set M
ht : t ⊆ f ⁻¹' h.domChart.source
hxt : x ∈ t
f' : E → E'' := ↑(h.domChart.extend J) ∘ f ∘ ↑(extChartAt I x).symm
φ' : E'' → E''' := ↑(h.codChart.extend J') ∘ φ ∘ ↑(h.domChart.extend J).symm
⊢ ContDiffWithinAt 𝕜 n f' (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I x) x)
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

Tactic:
by
  have h₀ : HasFDerivAt (fun w : E => ‖w‖ ^ 2) (0 : StrongDual ℝ E) 0 := by
    convert! (hasStrictFDerivAt_norm_sq (0 : E)).hasFDerivAt
    simp only [map_zero, smul_zero]
  have h₁ : HasFDerivAt (fun w : E => (‖w‖ ^ 2 + 4)⁻¹) (0 : StrongDual ℝ E) 0 := by
    convert! (hasFDerivAt_inv _).comp _ (h₀.add (hasFDerivAt_const 4 0)) <;> simp
  have h₂ : HasFDerivAt (fun w => (4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v)
      ((4 : ℝ) • ContinuousLinearMap.id ℝ E) 0 := by
    convert!
      ((hasFDerivAt_const (4 : ℝ) 0).smul (hasFDerivAt_id 0)).add
        ((h₀.sub (hasFDerivAt_const (4 : ℝ) 0)).smul (hasFDerivAt_const v 0)) using 1
    ext w
    simp
  convert! h₁.smul h₂ using 1
  ext w
  simp

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)
⊢ ∀ (x : { x // x ∈ sphere 0 1 }) (y : E),
    ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) x).symm)
      ((extChartAt (𝓡 n) x).target ∩ ↑(extChartAt (𝓡 n) x).symm ⁻¹' Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y).source)

Tactic:
intro v

Goal state after:
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),
    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)
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I m M
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), f x ∈ sphere 0 1
⊢ ∀ (y : ↑(sphere 0 1)),
    ContMDiffOn I (𝓡 n) m (↑(extChartAt (𝓡 n) y) ∘ Set.codRestrict f (sphere 0 1) hf')
      (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt (𝓡 n) y).source)

Tactic:
intro v

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I m M
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), f x ∈ sphere 0 1
v : ↑(sphere 0 1)
⊢ ContMDiffOn I (𝓡 n) m (↑(extChartAt (𝓡 n) v) ∘ Set.codRestrict f (sphere 0 1) hf')
    (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt (𝓡 n) v).source)
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : M
f : M → M'
hf : ContMDiffWithinAt I I' n f s x₀
hmn : m + 1 ≤ n
hx : x₀ ∈ s
hs : UniqueMDiff[s]
⊢ ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' id f (mfderiv[s] f) x₀) s x₀

Tactic:
by
  have : CMDiffAt[s ×ˢ s] n (fun x : M × M ↦ f x.2) (x₀, x₀) :=
    hf.comp (x₀, x₀) contMDiffWithinAt_snd mapsTo_snd_prod
  exact this.mfderivWithin contMDiffWithinAt_id hx (mapsTo_id _) hmn hs

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.UnitInterval

Goal state before:
pp: x y : ↑I
⊢ volume (Ico x y) = ENNReal.ofReal (↑y - ↑x)

Tactic:
by
  simp only [volume_apply, image_subtype_val_Ico, Real.volume_Ico]

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

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✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x : M
⊢ riemannianEDist I x x = 0

Tactic:
by
  apply le_antisymm _ bot_le
  exact (riemannianEDist_le_pathELength (γ := fun (t : ℝ) ↦ x) (a := 0) (b := 0)
    contMDiffOn_const rfl rfl le_rfl).trans_eq (by simp)

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

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✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ < ↑C
C_pos : 0 < C
⊢ ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C

Tactic:
filter_upwards [hC] with y hy

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✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ < ↑C
C_pos : 0 < C
y : M
hy : ‖mfderiv% ↑(extChartAt I x) y‖ < ↑C
⊢ ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

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✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ < ↑C
C_pos : 0 < C
⊢ ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C

Tactic:
filter_upwards [hC] with y hy

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✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ < ↑C
C_pos : 0 < C
y : E
hy : ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ < ↑C
⊢ ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
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
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
⊢ ∃ δ, 0 < δ ∧ (r' ^ 2)⁻¹ < 1 - δ * C

Tactic:
by
    have A : ∀ᶠ δ in 𝓝[>] (0 : ℝ), 0 < δ := self_mem_nhdsWithin
    have B : Tendsto (fun δ ↦ 1 - δ * C) (𝓝[>] 0) (𝓝 (1 - 0 * C)) := by
      apply tendsto_inf_left
      exact tendsto_const_nhds.sub (tendsto_id.mul tendsto_const_nhds)
    have B' : ∀ᶠ δ in 𝓝[>] 0, (r' ^ 2)⁻¹ < 1 - δ * C := by
      apply (tendsto_order.1 B).1
      simpa using inv_lt_one_of_one_lt₀ (by nlinarith)
    exact (A.and B').exists

Goal state after:
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:
intro U hxU

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
⊢ (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)
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
n : ℕ∞ω
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
inst✝² : VectorBundle 𝕜 F V
inst✝¹ : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
b : Basis ι 𝕜 F
⊢ ∀ {x : M}, x ∈ e.baseSet → ⊤ ≤ Submodule.span 𝕜 (Set.range fun x_1 ↦ e.localFrame b x_1 x)

Tactic:
by
    intro x hx
    convert! (e.basisAt b hx).span_eq.ge
    simp [hx, basisAt]

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
inst✝⁴ : VectorBundle 𝕜 F V
inst✝³ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝² : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
x : M
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) x
i : ι
aux : M → 𝕜 := fun x ↦ (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i
this : MDiffAt aux x
⊢ MDiffAt ((LinearMap.piApply (Trivialization.localFrameCoeff I e b i)) s) x

Tactic:
by
    apply this.congr_of_eventuallyEq
    apply eventuallyEq_of_mem (s := e.baseSet) (by simp [e.open_baseSet.mem_nhds hxe])
    intro y hy
    simp [aux, e.localFrameCoeff_eq_coeff hy]

Goal state after: