mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
⊢ (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓
        affineSpan ℝ (Set.range s.points)).direction =
    (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
direction_inf_of_mem_inf s.mongePoint_mem_mongePlane,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
⊢ (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ).direction ⊓
      (affineSpan ℝ (Set.range s.points)).direction =
    (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
r : ℝ
hr : r ≠ 0
⊢ s.secondInter p (r • v) = s.secondInter p v

Tactic:
by
  simp_rw [Sphere.secondInter, real_inner_smul_left, inner_smul_right, smul_smul,
    div_mul_eq_div_div]
  rw [mul_comm, ← mul_div_assoc, ← mul_div_assoc, mul_div_cancel_left₀ _ hr, mul_comm, mul_assoc,
    mul_div_cancel_left₀ _ hr, mul_comm]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist t.orthocenter ((reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) (circumcenter t)) = circumradius t

Tactic:
exact dist_orthocenter_reflection_circumcenter _ h

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist t.orthocenter ((reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) (circumcenter t)) = circumradius t

Tactic:
dist_orthocenter_reflection_circumcenter t h

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ circumradius t = circumradius t
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
x : G
hx : x ∈ ↑X
⊢ x⁻¹ ∈ ↑X

Tactic:
norm_cast at *
      have : x • X ⊆ X := by
        simpa [← hXn, add_assoc, ← sq] using! smul_finset_subset_mul (t := X) hx
      have : x • X = X := eq_of_subset_of_card_le this (card_smul_finset ..).ge
      rw [← eq_inv_smul_iff] at this
      rw [this]
      simpa [mem_inv_smul_finset_iff]

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
n : ℕ∞ω
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
c₁ c₂ : C^n⟮I, N; 𝓘(𝕜, 𝕜), 𝕜⟯
f : C^n⟮I, N; 𝓘(𝕜, V), V⟯
⊢ (c₁ * c₂) • f = c₁ • c₂ • f

Tactic:
ext x; exact mul_smul (c₁ x) (c₂ x) (f x)

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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
x : M
⊢ I.IsInteriorPoint x ∨ I.IsBoundaryPoint x

Tactic:
IsInteriorPoint,

Goal state after:
𝕜 : 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
x : M
⊢ ↑(extChartAt I x) x ∈ interior (range ↑I) ∨ I.IsBoundaryPoint x
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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
inst✝ : I.Boundaryless
x : M
r : interior (extChartAt I x).target = (extChartAt I x).target
this : extChartAt I x = (chartAt H x).extend I
⊢ ↑(extChartAt I x) x ∈ interior (extChartAt I x).target

Tactic:
r

Goal state after:
𝕜 : 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
inst✝ : I.Boundaryless
x : M
r : interior (extChartAt I x).target = (extChartAt I x).target
this : extChartAt I x = (chartAt H x).extend I
⊢ ↑(extChartAt I x) x ∈ (extChartAt I x).target
Module: Mathlib.Geometry.Manifold.LocalDiffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : ModelWithCorners 𝕜 F' H₃
M : Type u_8
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H₁ M
N : Type u_9
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H₂ N
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.25
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ Function.LeftInverse ⇑(mfderiv% ↑hf.localInverse.toPartialEquiv (f x)) ⇑(mfderiv% f x)

Tactic:
apply ContinuousLinearMap.leftInverse_of_comp
    rw [← mfderiv_id, ← hf.localInverse_eventuallyEq_left.mfderiv_eq]
    exact (mfderiv_comp _ (hf.localInverse_mdifferentiableAt hn) (hf.mdifferentiableAt hn)).symm

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

Goal state before:
pp: case e'_3
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
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
hd : ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑e.symm) y
x✝ : E
⊢ f c = (f ∘ ↑e.symm) (↑e c)

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
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
hd : ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑e.symm) y
⊢ IsLocalMax (norm ∘ f ∘ ↑e.symm) (↑e c)

Tactic:
· exact congr_arg f (extChartAt_to_inv _).symm

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
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
hd : ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑e.symm) y
⊢ IsLocalMax (norm ∘ f ∘ ↑e.symm) (↑e c)
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
U : Set M
a b : M
hpc : IsPreconnected U
hc✝ : IsCompact U
ho : IsOpen[inst✝²] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
c : M
hcU : c ∈ U
hc : IsMaxOn (fun x ↦ ‖f x‖) U c
this : ∀ x ∈ U, ‖f x‖ = ‖f c‖
⊢ ‖0‖ = 0

Tactic:
norm_zero

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
U : Set M
a b : M
hpc : IsPreconnected U
hc✝ : IsCompact U
ho : IsOpen[inst✝²] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
c : M
hcU : c ∈ U
hc : IsMaxOn (fun x ↦ ‖f x‖) U c
this : ∀ x ∈ U, ‖f x‖ = ‖f c‖
⊢ 0 = 0
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: case mp
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))
hp : (I.prod J).IsInteriorPoint p
⊢ p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N

Tactic:
IsInteriorPoint,

Goal state after:
case mp
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))
hp : ↑(extChartAt (I.prod J) p) p ∈ interior (range ↑(I.prod J))
⊢ p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N
Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent

Goal state before:
pp: case e_f.e_f.hc
𝕜 : 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
inst✝⁶ : IsManifold I 1 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'
inst✝ : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)
x₀ x : N
hx : f x ∈ (chartAt H (f x₀)).source
hy : g x ∈ (chartAt H' (g x₀)).source
⊢ MDiffAt[range ↑I] ↑(extChartAt I (f x₀)).symm (↑(extChartAt I (f x₀)) (f x))

Tactic:
· apply mdifferentiableWithinAt_extChartAt_symm
      apply (extChartAt I (f x₀)).map_source
      simpa using hx

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: case mpr
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))
hp : p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N
⊢ (I.prod J).IsInteriorPoint p

Tactic:
IsInteriorPoint,

Goal state after:
case mpr
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))
hp : p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N
⊢ ↑(extChartAt (I.prod J) p) p ∈ interior (range ↑(I.prod J))
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 : LeftInvariantDerivation I G
⊢ ⁅X, X⁆ = 0

Tactic:
ext1; simp only [commutator_apply, sub_self]; rfl

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

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
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'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
n : ℕ∞ω
t : Set M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
hV : MDiffAt[t] (T% V) (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : 2 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x ↦ (mfderiv[s] f x).inverse
hv : (MDiffAt[s ∩ f ⁻¹' t] fun x ↦ ⟨f x, v x⟩) x₀
this : (MDiffAt[s] fun x ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderiv[s] f x)) x₀
⊢ (↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (f x₀)) (f x₀) ⋯) ∘SL
      mfderiv[s] f x₀ ∘SL
        ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x₀
              ⋯).symm).IsInvertible

Tactic:
exact isInvertible_equiv.comp (hf'.comp isInvertible_equiv)

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

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
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'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x ↦ (mfderiv[s] f x).inverse
hv : ContMDiffWithinAt I I'.tangent m (fun x ↦ ⟨f x, v x⟩) (s ∩ f ⁻¹' t) x₀
this :
  ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m
    (fun x ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderiv[s] f x)) s x₀
⊢ (↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (f x₀)) (f x₀) ⋯) ∘SL
      mfderiv[s] f x₀ ∘SL
        ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x₀
              ⋯).symm).IsInvertible

Tactic:
exact isInvertible_equiv.comp (hf'.comp isInvertible_equiv)

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 : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
s : Set M
hs : IsOpen[inst✝¹] s
x✝ : ImmersionAtProp F I J M N f φ ψ
equiv : (E × F) ≃L[𝕜] E''
hf : EqOn (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (⇑equiv ∘ fun x ↦ (x, 0)) (φ.extend I).target
⊢ ((φ.restr s).extend I).target ⊆ (φ.extend I).target

Tactic:
simp; grind

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

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
h'z : ⟨z, hz⟩ ∈ {z | ↑z < y}
⊢ ⟨min ((↑⟨toLp 2 fun x_1 ↦ ↑⟨z, hz⟩ - x, ⋯⟩).ofLp 0 + x) y, ⋯⟩ = ⟨z, hz⟩

Tactic:
simp only [mem_ofPred_eq, mem_Icc] at hz h'z

Goal state after:
x y : ℝ
h : Fact (x < y)
z : ℝ
hz✝ : z ∈ Icc x y
h'z : z < y
hz : x ≤ z ∧ z ≤ y
⊢ ⟨min ((↑⟨toLp 2 fun x_1 ↦ ↑⟨z, hz✝⟩ - x, ⋯⟩).ofLp 0 + x) y, ⋯⟩ = ⟨z, hz✝⟩
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
h'z : ⟨z, hz⟩ ∈ {z | x < ↑z}
⊢ ⟨max (y - (↑⟨toLp 2 fun x_1 ↦ y - ↑⟨z, hz⟩, ⋯⟩).ofLp 0) x, ⋯⟩ = ⟨z, hz⟩

Tactic:
simp only [mem_ofPred_eq, mem_Icc] at hz h'z

Goal state after:
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : ℝ
hz✝ : z ∈ Icc x y
h'z : x < z
hz : x ≤ z ∧ z ≤ y
⊢ ⟨max (y - (↑⟨toLp 2 fun x_1 ↦ y - ↑⟨z, hz✝⟩, ⋯⟩).ofLp 0) x, ⋯⟩ = ⟨z, hz✝⟩
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
z : ↑(Icc x y)
h : y ≤ ↑z
⊢ chartAt (EuclideanHalfSpace 1) z = IccRightChart x y

Tactic:
simp [Icc_chartedSpaceChartAt, reduceIte, not_lt.mpr h]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
⊢ ⟪↑(stereoInvFun hv w), v⟫_ℝ < 1

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
⊢ ‖↑(stereoInvFun hv w)‖ = 1

Tactic:
· have hw : ⟪v, w⟫_ℝ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2
    have hw' : (‖(w : E)‖ ^ 2 + 4)⁻¹ * (‖(w : E)‖ ^ 2 - 4) < 1 := by
      rw [inv_mul_lt_iff₀']
      · linarith
      positivity
    simpa [real_inner_comm, inner_add_right, inner_smul_right, real_inner_self_eq_norm_mul_norm, hw,
      hv] using hw'

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
⊢ ‖↑(stereoInvFun hv w)‖ = 1
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

Goal state before:
pp: case e'_11
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}
⊢ v = a⁻¹ • a • v

Tactic:
simp only [smul_smul, inv_mul_eq_div, div_self ha, one_smul]

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

Goal state before:
pp: case e'_11
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
t₀ a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurveAt (γ ∘ fun x ↦ x * a) (a • v) (t₀ / a)
⊢ v = a⁻¹ • a • v

Tactic:
simp only [smul_smul, inv_mul_eq_div, div_self ha, one_smul]

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

Goal state before:
pp: case e'_11
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
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurve (γ ∘ fun x ↦ x * a) (a • v)
⊢ v = a⁻¹ • a • v

Tactic:
simp only [smul_smul, inv_mul_eq_div, div_self ha, one_smul]

Goal state after: