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

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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
h₁ : ↑((orthogonalProjection s₁) p) ∈ line[ℝ, p', ↑((orthogonalProjection s₂) p)]
h₁' : ↑((orthogonalProjection s₁) p) ∈ s₁ ⊓ s₂
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection (s₁ ⊓ s₂)) p)

Tactic:
rw [← orthogonalProjection_orthogonalProjection_of_le inf_le_left, eq_comm,
        orthogonalProjection_eq_self_iff]

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
h₁ : ↑((orthogonalProjection s₁) p) ∈ line[ℝ, p', ↑((orthogonalProjection s₂) p)]
h₁' : ↑((orthogonalProjection s₁) p) ∈ s₁ ⊓ s₂
⊢ ↑((orthogonalProjection s₁) p) ∈ s₁ ⊓ s₂
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p ↦ (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) sp
p : P × P × P
hp : ∃ x, s.SSameSide p₃ x ∧ (p₁, x, p₂) = p
⊢ ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ ↑π

Tactic:
obtain ⟨p', hp', rfl⟩ := hp

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p ↦ (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) sp
p' : P
hp' : s.SSameSide p₃ p'
⊢ ∡ (p₁, p', p₂).1 (p₁, p', p₂).2.1 (p₁, p', p₂).2.2 ≠ 0 ∧ ∡ (p₁, p', p₂).1 (p₁, p', p₂).2.1 (p₁, p', p₂).2.2 ≠ ↑π
Module: Mathlib.Geometry.Euclidean.SignedDist

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 : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ (s.signedInfDist p) p = ‖p -ᵥ ↑((orthogonalProjection s) p)‖

Tactic:
by
  rw [signedInfDist_eq_signedDist_orthogonalProjection, signedDist_vsub_self, dist_eq_norm_vsub']

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

Goal state before:
pp: case hc
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : ⟪v, v⟫ ≠ 0
hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫)
⊢ 2 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
r : ℝ
hr : 0 < r
he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂
⊢ Wbtw ℝ p₂ ((p₁ -ᵥ p₂) +ᵥ p₂) p₄ ∨ Wbtw ℝ p₂ p₄ ((p₁ -ᵥ p₂) +ᵥ p₂)

Tactic:
← vsub_vadd p₄ p₂,

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
r : ℝ
hr : 0 < r
he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂
⊢ Wbtw ℝ p₂ ((p₁ -ᵥ p₂) +ᵥ p₂) ((p₄ -ᵥ p₂) +ᵥ p₂) ∨ Wbtw ℝ p₂ ((p₄ -ᵥ p₂) +ᵥ p₂) ((p₁ -ᵥ p₂) +ᵥ p₂)
Module: Mathlib.Geometry.Euclidean.SignedDist

Goal state before:
pp: case hp₁
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
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
h : ∑ i, w i = 1
⊢ ∀ (i_1 : Fin (n + 1)), ¬i_1 = i → ↑(s.signedInfDist i) (s.points i_1) = 0

Tactic:
intro j

Goal state after:
case hp₁
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
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
h : ∑ i, w i = 1
j : Fin (n + 1)
⊢ ¬j = i → ↑(s.signedInfDist i) (s.points j) = 0
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
this : (∡ p₁ p₂ p₃).toReal = (∡ p₁ p₂ p₄).toReal / 2
⊢ |(∡ p₁ p₂ p₄).toReal| / |2| = |(∡ p₁ p₂ p₄).toReal| / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case h
P : Type u_2
inst✝ : MetricSpace P
p : P
⊢ ∃ radius, ∀ p_1 ∈ {p}, dist p_1 p = radius

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₁ p₂ = 2 * (‖2‖⁻¹ * dist p₁ p₂)

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ 2 * s.radius = 0 ↔ s.radius = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ p₁ ∈ Sphere.ofDiameter p₁ p₂

Tactic:
simp [Sphere.ofDiameter, mem_sphere, inv_mul_eq_div]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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
⊢ -⟪p -ᵥ s.center, p -ᵥ s.center⟫ = 0 ↔ p = s.center

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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
⊢ p ∈ mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ -(s.center -ᵥ p) ∈ (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ).directionᗮ

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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
⊢ ↑((orthogonalProjection (s.orthRadius p)) s.center) = p

Tactic:
by
  simp_rw [orthRadius, coe_orthogonalProjection_eq_iff_mem]
  rw [← Submodule.neg_mem_iff]
  simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : 2 • ∡ p₂ p₁ p = 2 • ∡ p p₁ p₃
h' : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = p₁
⊢ dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, 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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : 2 • ∡ p₂ p₁ p = 2 • ∡ p p₁ p₃
h' : ↑((orthogonalProjection line[ℝ, p₁, p₃]) p) = p₁
⊢ dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)

Tactic:
· exact dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₁ h₂ h h'

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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : 2 • ∡ p₂ p₁ p = 2 • ∡ p p₁ p₃
h' : ↑((orthogonalProjection line[ℝ, p₁, p₃]) p) = p₁
⊢ dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : Fin 3 → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
hfn0 : ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0
i : Fin 3
hi : i ≠ 0
⊢ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫

Tactic:
have hsdi := hsd i

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : Fin 3 → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
hfn0 : ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0
i : Fin 3
hi : i ≠ 0
hsdi : f i = 0 ∨ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
⊢ f i = -2 * ⟪v, p 0 -ᵥ c⟫ / ⟪v, v⟫
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case e'_3
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h : dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
ho : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
hs : ↑((orthogonalProjection (line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃])) p) = ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
⊢ {p₁} = ![p₁, p₂, p₃] '' {0}

Tactic:
simp

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

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 : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
⊢ p = p₁ ∨ p = p₂

Tactic:
have ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0 :=
    inner_vsub_vsub_of_dist_eq_of_dist_eq (hp₁c₁.trans hp₂c₁.symm) (hp₁c₂.trans hp₂c₂.symm)
  have hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0 :=
    inner_vsub_vsub_of_dist_eq_of_dist_eq (hp₁c₁.trans hpc₁.symm) (hp₁c₂.trans hpc₂.symm)
  let b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
  have hb : LinearIndependent ℝ b := by
    refine linearIndependent_of_ne_zero_of_inner_eq_zero ?_ ?_
    · intro i
      fin_cases i <;> simp [b, hc.symm, hp.symm]
    · intro i j hij
      fin_cases i <;> fin_cases j <;> try exact False.elim (hij rfl)
      · exact ho
      · rw [real_inner_comm]
        exact ho
  have hbs : Submodule.span ℝ (Set.range b) = s.direction := by
    refine Submodule.eq_of_le_of_finrank_eq ?_ ?_
    · rw [Submodule.span_le, Set.range_subset_iff]
      intro i
      fin_cases i
      · exact vsub_mem_direction hc₂s hc₁s
      · exact vsub_mem_direction hp₂s hp₁s
    · rw [finrank_span_eq_card hb, Fintype.card_fin, hd]
  have hv : ∀ v ∈ s.direction, ∃ t₁ t₂ : ℝ, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁) := by
    intro v hv
    have hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁} := by
      have hu : (Finset.univ : Finset (Fin 2)) = {0, 1} := by decide
      classical
      rw [← Fintype.coe_image_univ, hu]
      simp [b]
    rw [← hbs, hr, Submodule.mem_span_insert] at hv
    rcases hv with ⟨t₁, v', hv', hv⟩
    rw [Submodule.mem_span_singleton] at hv'
    rcases hv' with ⟨t₂, rfl⟩
    exact ⟨t₁, t₂, hv⟩
  rcases hv (p -ᵥ p₁) (vsub_mem_direction hps hp₁s) with ⟨t₁, t₂, hpt⟩
  simp only [hpt, inner_add_right, inner_smul_right, ho, mul_zero, add_zero,
    mul_eq_zero, inner_self_eq_zero, vsub_eq_zero_iff_eq, hc.symm, or_false] at hop
  rw [hop, zero_smul, zero_add, ← eq_vadd_iff_vsub_eq] at hpt
  subst hpt
  have hp' : (p₂ -ᵥ p₁ : V) ≠ 0 := by simp [hp.symm]
  have hp₂ : dist ((1 : ℝ) • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁ := by simp [hp₂c₁]
  rw [← hp₁c₁, dist_smul_vadd_eq_dist _ _ hp'] at hpc₁ hp₂
  simp only [one_ne_zero, false_or] at hp₂
  rw [hp₂.symm] at hpc₁
  rcases hpc₁ with hpc₁ | hpc₁ <;> simp [hpc₁]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case refine_2.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
⊢ s.orthRadius p ≤ s.orthRadius p

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case refine_2.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
⊢ s.orthRadius p ≤ s.orthRadius s.center

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case e'_8
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h : dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
ho : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
hs : ↑((orthogonalProjection (line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃])) p) = ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
hinf : line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] = affineSpan ℝ {p₁}
⊢ {p₁, p₂} ∪ {p₁, p₃} = Set.range ![p₁, p₂, p₃]

Tactic:
simp

Goal state after:
case e'_8
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h : dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
ho : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
hs : ↑((orthogonalProjection (line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃])) p) = ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
hinf : line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] = affineSpan ℝ {p₁}
⊢ {p₃, p₁, p₂} = {p₃, p₂, p₁}
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case refine_2.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
as : AffineSubspace ℝ P
hr : s.radius = 0
hm : s.center ∈ as
⊢ as ≤ s.orthRadius s.center

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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
as : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥as
inst✝ : as.direction.HasOrthogonalProjection
⊢ Metric.infDist s.center ↑as = s.radius ↔ s.IsTangent as

Tactic:
rw [← dist_orthogonalProjection_eq_infDist, dist_orthogonalProjection_eq_radius_iff_isTangent]

Goal state after:
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
hp₁ : p₁ ∈ s
hp₂ : dist p₁ s.center ≤ s.radius
⊢ 0 ≤ ⟪p₁ -ᵥ p₁, p₁ -ᵥ s.center⟫

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case refine_2.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
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
⊢ Wbtw ℝ s₁.center s₁.center s₂.center

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case refine_2.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
hr : s₁.radius = 0
hc : s₁.center ∈ s₂
⊢ Wbtw ℝ s₂.center s₁.center s₁.center

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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
h : p ∈ s
⊢ Wbtw ℝ s.center s.center p

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t ∅)) =
    dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t ∅))
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₃).points

Tactic:
simp

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t ∅)) =
    dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t ∅))
⊢ ∃ x, ¬x = i₃ ∧ t.points x = t.points i₁
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t ∅)) =
    dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t ∅))
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₂).points

Tactic:
simp

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t ∅)) =
    dist (incenter t) ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t ∅))
⊢ ∃ x, ¬x = i₂ ∧ t.points x = t.points i₁
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t {i₁}))
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₃).points

Tactic:
simp

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t {i₁}))
⊢ ∃ x, ¬x = i₃ ∧ t.points x = t.points i₁
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t {i₁}))
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₂).points

Tactic:
simp

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t {i₁}))
⊢ ∃ x, ¬x = i₂ ∧ t.points x = t.points i₁