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

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
he : s.Equilateral
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) < π / 2

Tactic:
rw [he.angle_eq_pi_div_three h₁₂ h₁₃ 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
n : ℕ
s : Simplex ℝ P n
he : s.Equilateral
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ π / 3 < π / 2
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
P : Type u_2
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ {p₁, p₂, p₃}
⊢ ¬Collinear ℝ {p₁, p, p₄}

Tactic:
intro hcol

Goal state after:
V : Type u_1
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
P : Type u_2
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ {p₁, p₂, p₃}
hcol : Collinear ℝ {p₁, p, p₄}
⊢ False
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
P : Type u_2
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ {p₁, p₂, p₃}
h_notcol_p₁pp₄ : ¬Collinear ℝ {p₁, p, p₄}
⊢ ¬Collinear ℝ {p₃, p, p₂}

Tactic:
intro hcol

Goal state after:
V : Type u_1
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
P : Type u_2
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ {p₃, p, p₄}
h_notcol_p₁p₂p₃ : ¬Collinear ℝ {p₁, p₂, p₃}
h_notcol_p₁pp₄ : ¬Collinear ℝ {p₁, p, p₄}
hcol : Collinear ℝ {p₃, p, p₂}
⊢ False
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₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (Submodule.span ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ
x : V
⊢ (∃ i, x = s.points i₁ -ᵥ s.points ↑i) ↔ ∃ x_1 ∈ Set.univ \ {i₁}, s.points i₁ -ᵥ s.points x_1 = x

Tactic:
Set.mem_sdiff_singleton

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₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (Submodule.span ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ
x : V
⊢ (∃ i, x = s.points i₁ -ᵥ s.points ↑i) ↔ ∃ x_1, (x_1 ∈ Set.univ ∧ x_1 ≠ i₁) ∧ s.points i₁ -ᵥ s.points x_1 = x
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : dist p t ^ 2 = s.power p
⊢ s.IsTangentAt t line[ℝ, p, t]

Tactic:
have h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0 := by
      simp only [Sphere.power, ← mem_sphere.mp ht, dist_eq_norm_vsub V, sq,
                 ← vsub_add_vsub_cancel p t s.center] at h_dist_eq
      exact (norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero _ _).mp (by linarith)

Goal state after:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : dist p t ^ 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
⊢ s.IsTangentAt t line[ℝ, p, t]
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

Goal state before:
pp: case hw
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : Sphere P
n : ℕ
inst✝ : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P := (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points) w)) r
hp' : p' -ᵥ sx.points i = r • ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i)
⊢ ∑ i_1, (r • (w - Pi.single i 1) + Pi.single i 1) i_1 = 1

Tactic:
· simp [Finset.sum_add_distrib, ← Finset.mul_sum, hw]

Goal state after:
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
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : 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
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
y : N
hy : y ∈ hf.localInverse.source
this : ↑hf.localInverse.toPartialEquiv y ∈ (Exists.choose hf).source
⊢ ↑(Exists.choose hf).toPartialEquiv (↑hf.localInverse.toPartialEquiv y) = y

Tactic:
exact hf.choose.right_inv hy

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
⊢ (ModelWithCorners.boundary M)ᶜ = ModelWithCorners.interior M

Tactic:
← compl_interior,

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
⊢ (ModelWithCorners.interior M)ᶜᶜ = ModelWithCorners.interior M
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
h : ModelWithCorners.boundary M = ∅
x : M
⊢ x ∈ ModelWithCorners.interior M

Tactic:
← compl_interior,

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
h : (ModelWithCorners.interior M)ᶜ = ∅
x : M
⊢ x ∈ ModelWithCorners.interior M
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : 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
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle 1 F E IB
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
f : M → TotalSpace F E
s : Set M
x₀ : M
he : f x₀ ∈ e.source
⊢ MDiffAt[s] f x₀ ↔ (MDiffAt[s] fun x ↦ (f x).proj) x₀ ∧ (MDiffAt[s] fun x ↦ (↑e (f x)).2) x₀

Tactic:
rw [mdifferentiableWithinAt_totalSpace]
  apply and_congr_right
  intro hf
  rw [Trivialization.mdifferentiableWithinAt_snd_comp_iff₂ IB
    (FiberBundle.mem_trivializationAt_proj_source) he hf]

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

Goal state before:
pp: case hg
𝕜 : 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₀
⊢ MDiffAt[s] (↑(extChartAt I' (f x₀)) ∘ f) x₀

Tactic:
apply MDifferentiableAt.comp_mdifferentiableWithinAt (I' := I') _ _ h'f

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
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₀
⊢ MDiffAt ↑(extChartAt I' (f x₀)) (f x₀)
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
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ ContMDiffOn I J n f h.domChart.source

Tactic:
rw [← h.domChart.contMDiffOn_writtenInExtend_iff h.domChart_mem_maximalAtlas
    h.codChart_mem_maximalAtlas le_rfl h.mapsto_domChart_source_codChart_source,
    ← h.domChart.extend_target_eq_image_source]
  have : CMDiff n (h.equiv ∘ fun x ↦ (x, 0)) := by
    rw [contMDiff_iff_contDiff]; fun_prop
  exact this.contMDiffOn.congr h.writtenInCharts

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

Goal state before:
pp: case inr.inr
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p ∈ Ioo x y
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

Tactic:
· apply iff_of_false
    · simpa [← mem_compl_iff, ModelWithCorners.compl_boundary] using!
        Icc_isInteriorPoint_interior hp
    · rintro (rfl | rfl) <;> simp at hp

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

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:
Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

Goal state before:
pp: R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
this : (val ∘ fun x ↦ x⁻¹) = Ring.inverse ∘ val
x : Rˣ
⊢ ContMDiffAt 𝓘(𝕜, R) 𝓘(𝕜, R) n Ring.inverse ↑x

Tactic:
contMDiffAt_iff_contDiffAt

Goal state after:
R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
this : (val ∘ fun x ↦ x⁻¹) = Ring.inverse ∘ val
x : Rˣ
⊢ ContDiffAt 𝕜 n Ring.inverse ↑x
Module: Mathlib.Geometry.Manifold.IntegralCurve.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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
hsrc : γ t ∈ (chartAt H (γ t₀)).source
⊢ HasMFDerivAt% (↑(extChartAt I (γ t₀)) ∘ γ) t
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))))

Tactic:
apply (HasMFDerivAt.comp t (hasMFDerivAt_extChartAt (I := I) hsrc) ht2).congr_mfderiv

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
hsrc : γ t ∈ (chartAt H (γ t₀)).source
⊢ mfderiv% ↑(chartAt H (γ t₀)) (γ t) ∘SL ContinuousLinearMap.smulRight 1 (v (γ t)) =
    ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))
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
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
h : ContDiffOn ℝ ω (⇑U) Set.univ
H₁ :
  ContMDiffOn 𝓘(ℝ, E) (𝓡 n) ω (⇑U ∘ stereoToFun ↑(-v))
    ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)
H₂ : ContMDiffOn I 𝓘(ℝ, E) m f Set.univ
x : M
hfx : ‖f x‖ = 1
⊢ f x = -↑v ↔ ⟪f x, -↑v⟫_ℝ = 1

Tactic:
inner_eq_one_iff_of_norm_eq_one hfx

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)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
h : ContDiffOn ℝ ω (⇑U) Set.univ
H₁ :
  ContMDiffOn 𝓘(ℝ, E) (𝓡 n) ω (⇑U ∘ stereoToFun ↑(-v))
    ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)
H₂ : ContMDiffOn I 𝓘(ℝ, E) m f Set.univ
x : M
hfx : ‖f x‖ = 1
⊢ f x = -↑v ↔ f x = -↑v

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)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
h : ContDiffOn ℝ ω (⇑U) Set.univ
H₁ :
  ContMDiffOn 𝓘(ℝ, E) (𝓡 n) ω (⇑U ∘ stereoToFun ↑(-v))
    ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)
H₂ : ContMDiffOn I 𝓘(ℝ, E) m f Set.univ
x : M
hfx : ‖f x‖ = 1
⊢ ‖-↑v‖ = 1
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)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
this✝ : mfderiv[Icc a b] (γ ∘ f) t = mfderiv[Icc (f a) (f b)] γ (f t) ∘SL mfderiv[Icc a b] f t
this : (mfderiv[Icc a b] f t) 1 = derivWithin f (Icc a b) t • 1
⊢ ‖(mfderiv[Icc (f a) (f b)] γ (f t)) (derivWithin f (Icc a b) t • 1)‖ₑ =
    ENNReal.ofReal (derivWithin f (Icc a b) t) * ‖(mfderiv[f '' Icc a b] γ (f t)) 1‖ₑ

Tactic:
have : 0 ≤ derivWithin f (Icc a b) t := hf.derivWithin_nonneg

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✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
this✝¹ : mfderiv[Icc a b] (γ ∘ f) t = mfderiv[Icc (f a) (f b)] γ (f t) ∘SL mfderiv[Icc a b] f t
this✝ : (mfderiv[Icc a b] f t) 1 = derivWithin f (Icc a b) t • 1
this : 0 ≤ derivWithin f (Icc a b) t
⊢ ‖(mfderiv[Icc (f a) (f b)] γ (f t)) (derivWithin f (Icc a b) t • 1)‖ₑ =
    ENNReal.ofReal (derivWithin f (Icc a b) t) * ‖(mfderiv[f '' Icc a b] γ (f t)) 1‖ₑ
Module: Mathlib.Geometry.Manifold.Sheaf.Basic

Goal state before:
pp: H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens ↑(TopCat.of M)
f : ↥V → M'
h : ∀ (x : ↥V), ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i, ChartedSpace.LiftProp P fun x ↦ f (i x)
x : ↥V
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ ⇑i)
x' : ↥U := ⟨↑x, hxU⟩
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P (f ∘ inclusion hUV) x'

Tactic:
exact hU x'

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 : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
inst✝ : Finite ι
hs : IsLocalFrameOn I F n s u
hx : x ∈ u
t t' : (x : M) → V x
h : ∀ (i : ι), (hs.coeff i x) (t x) = (hs.coeff i x) (t' x)
⊢ t x = t' x

Tactic:
let : Fintype ι := Fintype.ofFinite ι

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
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 : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
inst✝ : Finite ι
hs : IsLocalFrameOn I F n s u
hx : x ∈ u
t t' : (x : M) → V x
h : ∀ (i : ι), (hs.coeff i x) (t x) = (hs.coeff i x) (t' x)
this : Fintype ι := Fintype.ofFinite ι
⊢ t x = t' x