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

Goal state before:
pp: case pos
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

pp: case neg
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : ¬p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Tactic:
·

Goal state after:
case pos
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
hrad : s.radius ≠ 0
hr : q -ᵥ s.center = 0 • (p -ᵥ s.center)
⊢ ℝ ∙ (p -ᵥ s.center) = ℝ ∙ (q -ᵥ s.center)

pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hr0 : r ≠ 0
⊢ ℝ ∙ (p -ᵥ s.center) = ℝ ∙ (q -ᵥ s.center)

Tactic:
·

Goal state after:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
hrad : s.radius ≠ 0
hr : q -ᵥ s.center = 0 • (p -ᵥ s.center)
⊢ ℝ ∙ (p -ᵥ s.center) = ℝ ∙ (q -ᵥ s.center)
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case h₁
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₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ p₁‖

pp: case h₂
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₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ ‖p₂ -ᵥ s.center + (s.center -ᵥ p₁)‖ = ‖p₂ -ᵥ s.center‖ + ‖s.center -ᵥ p₁‖

Tactic:
·

Goal state after:
case h₁
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₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ p₁‖
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hr0 : r ≠ 0
⊢ ℝ ∙ (p -ᵥ s.center) = ℝ ∙ (q -ᵥ s.center)

Tactic:
·

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hr0 : r ≠ 0
⊢ ℝ ∙ (p -ᵥ s.center) = ℝ ∙ (q -ᵥ s.center)
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case h₂
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₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ ‖p₂ -ᵥ s.center + (s.center -ᵥ p₁)‖ = ‖p₂ -ᵥ s.center‖ + ‖s.center -ᵥ p₁‖

Tactic:
·

Goal state after:
case h₂
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₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ ‖p₂ -ᵥ s.center + (s.center -ᵥ p₁)‖ = ‖p₂ -ᵥ s.center‖ + ‖s.center -ᵥ p₁‖
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case inr.inl
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
hp : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr : q -ᵥ s.center = 0 • (p -ᵥ s.center)
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)

pp: case inr.inr
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
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr0 : r ≠ 0
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)

Tactic:
·

Goal state after:
case inr.inl
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
hp : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr : q -ᵥ s.center = 0 • (p -ᵥ s.center)
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case inr.inr
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
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr0 : r ≠ 0
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)

Tactic:
·

Goal state after:
case inr.inr
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
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr0 : r ≠ 0
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case inl
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
hp₁ hp₂ : p₁ ∈ s
⊢ s.center ∈ line[ℝ, p₁, p₁] ↔ s.IsDiameter p₁ p₁

pp: case inr
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ s.center ∈ line[ℝ, p₁, p₂] ↔ s.IsDiameter p₁ p₂

Tactic:
·

Goal state after:
case inl
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
hp₁ hp₂ : p₁ ∈ s
⊢ s.center ∈ line[ℝ, p₁, p₁] ↔ s.IsDiameter p₁ p₁
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case inr
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ s.center ∈ line[ℝ, p₁, p₂] ↔ s.IsDiameter p₁ p₂

Tactic:
·

Goal state after:
case inr
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ s.center ∈ line[ℝ, p₁, p₂] ↔ s.IsDiameter p₁ p₂
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case mpr
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 q : P
⊢ q = p ∧ dist p s.center = s.radius → Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q}

Tactic:
·

Goal state after:
case mpr
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 q : P
⊢ q = p ∧ dist p s.center = s.radius → Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q}
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case inr.inr.inl
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
hp : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr : q -ᵥ s.center = 1 • (p -ᵥ s.center)
hr0 : 1 ≠ 0
hr' : |1| = 1
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)

pp: case inr.inr.inr
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
hp : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr : q -ᵥ s.center = -1 • (p -ᵥ s.center)
hr0 : -1 ≠ 0
hr' : |(-1)| = 1
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)

Tactic:
·

Goal state after:
case inr.inr.inl
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
hp : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr : q -ᵥ s.center = 1 • (p -ᵥ s.center)
hr0 : 1 ≠ 0
hr' : |1| = 1
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case inr.refine_1
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
h : s.center ∈ line[ℝ, p₁, p₂]
⊢ Collinear ℝ {p₁, s.center, p₂}

pp: case inr.refine_2
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
h : s.center ∈ line[ℝ, p₁, p₂]
⊢ dist s.center s.center ≤ s.radius

Tactic:
·

Goal state after:
case inr.refine_1
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
h : s.center ∈ line[ℝ, p₁, p₂]
⊢ Collinear ℝ {p₁, s.center, p₂}
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case inr.inr.inr
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
hp : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr : q -ᵥ s.center = -1 • (p -ᵥ s.center)
hr0 : -1 ≠ 0
hr' : |(-1)| = 1
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)

Tactic:
·

Goal state after:
case inr.inr.inr
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
hp : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr : q -ᵥ s.center = -1 • (p -ᵥ s.center)
hr0 : -1 ≠ 0
hr' : |(-1)| = 1
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case inr.refine_2
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
h : s.center ∈ line[ℝ, p₁, p₂]
⊢ dist s.center s.center ≤ s.radius

Tactic:
·

Goal state after:
case inr.refine_2
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₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
h : s.center ∈ line[ℝ, p₁, p₂]
⊢ dist s.center s.center ≤ s.radius
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

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 : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points),
        p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) ∧
          ∠ p p' ↑((s.faceOpposite i₁).orthogonalProjectionSpan p) =
            ∠ p p' ↑((s.faceOpposite i₂).orthogonalProjectionSpan p)
i : Fin (n + 1)
⊢ dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p) = dist p ↑((s.faceOpposite i₁).orthogonalProjectionSpan p)

Tactic:
by_cases hi : i = i₁

Goal state after:
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points),
        p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) ∧
          ∠ p p' ↑((s.faceOpposite i₁).orthogonalProjectionSpan p) =
            ∠ p p' ↑((s.faceOpposite i₂).orthogonalProjectionSpan p)
i : Fin (n + 1)
hi : i = i₁
⊢ dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p) = dist p ↑((s.faceOpposite i₁).orthogonalProjectionSpan p)

case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points),
        p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) ∧
          ∠ p p' ↑((s.faceOpposite i₁).orthogonalProjectionSpan p) =
            ∠ p p' ↑((s.faceOpposite i₂).orthogonalProjectionSpan p)
i : Fin (n + 1)
hi : ¬i = i₁
⊢ dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p) = dist p ↑((s.faceOpposite i₁).orthogonalProjectionSpan p)
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points),
        p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) ∧
          ∠ p p' ↑((s.faceOpposite i₁).orthogonalProjectionSpan p) =
            ∠ p p' ↑((s.faceOpposite i₂).orthogonalProjectionSpan p)
i : Fin (n + 1)
hi : i = i₁
⊢ dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p) = dist p ↑((s.faceOpposite i₁).orthogonalProjectionSpan p)

pp: case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points),
        p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) ∧
          ∠ p p' ↑((s.faceOpposite i₁).orthogonalProjectionSpan p) =
            ∠ p p' ↑((s.faceOpposite i₂).orthogonalProjectionSpan p)
i : Fin (n + 1)
hi : ¬i = i₁
⊢ dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p) = dist p ↑((s.faceOpposite i₁).orthogonalProjectionSpan p)

Tactic:
·

Goal state after:
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points),
        p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) ∧
          ∠ p p' ↑((s.faceOpposite i₁).orthogonalProjectionSpan p) =
            ∠ p p' ↑((s.faceOpposite i₂).orthogonalProjectionSpan p)
i : Fin (n + 1)
hi : i = i₁
⊢ dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p) = dist p ↑((s.faceOpposite i₁).orthogonalProjectionSpan p)
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h : ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center

pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h : ∀ p ∈ as, ¬Wbtw ℝ s₁.center p s₂.center
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center

Tactic:
·

Goal state after:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h : ∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case inl
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
h : dist p s.center < s.radius
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔
    s.radius < dist p s.center ∨
      Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0

pp: case inr.inl
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
h : dist p s.center = s.radius
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔
    s.radius < dist p s.center ∨
      Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0

pp: case inr.inr
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
h : s.radius < dist p s.center
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔
    s.radius < dist p s.center ∨
      Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0

Tactic:
·

Goal state after:
case inl
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
h : dist p s.center < s.radius
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔
    s.radius < dist p s.center ∨
      Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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
s₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h : ∀ p ∈ as, ¬Wbtw ℝ s₁.center p s₂.center
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center

Tactic:
·

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
s₁ s₂ : Sphere P
as : AffineSubspace ℝ P
h : ∀ p ∈ as, ¬Wbtw ℝ s₁.center p s₂.center
⊢ (∃ p ∈ as, Wbtw ℝ s₁.center p s₂.center) ∨ ∀ p ∈ as, ¬Sbtw ℝ s₁.center p s₂.center
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case inl.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
h : dist s.center s.center < s.radius
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius s.center) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬s.center = s.center ∨ Subsingleton V

pp: case inl.inr
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
h : dist p s.center < s.radius
hp : p ≠ s.center
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔ Module.finrank ℝ V = 1 ∧ ¬p = s.center ∨ Subsingleton V

Tactic:
·

Goal state after:
case inl.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
h : dist s.center s.center < s.radius
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius s.center) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬s.center = s.center ∨ Subsingleton V
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
⊢ s₁.IsExtTangentAt s₂ s₁.center → s₁.radius = 0 ∧ s₁.center ∈ s₂

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
s₁ s₂ : Sphere P
⊢ s₁.radius = 0 ∧ s₁.center ∈ s₂ → s₁.IsExtTangentAt s₂ s₁.center

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
⊢ s₁.IsExtTangentAt s₂ s₁.center → s₁.radius = 0 ∧ s₁.center ∈ s₂