mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : P ≃ᵃⁱ[ℝ] P
h : f s.center = s.center
⊢ map (↑f.toAffineEquiv) (s.orthRadius p) = s.orthRadius (f p)

Tactic:
rw [orthRadius, map_mk', orthRadius]
  convert! rfl using 2
  convert! (Submodule.map_orthogonal_equiv (ℝ ∙ (p -ᵥ s.center)) f.linearIsometryEquiv).symm
  simp [Submodule.map_span, Set.image_singleton, h]

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
p : P
h : s.IsTangent as
hpar : as ∥ s.orthRadius p
hp : p ∈ s
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center) p)

Tactic:
rcases h with ⟨q, hqs, hqas, hqo⟩

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 : 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
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center) p)
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case neg.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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₂ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖

Tactic:
Ne,

Goal state after:
case neg.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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
⊢ ¬⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ = ‖p₂ -ᵥ s.center‖ * ‖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
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius = 0
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center) p)

Tactic:
mem_sphere,

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 : dist p s.center = s.radius
q : P
hqs : dist q s.center = s.radius
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius = 0
⊢ as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center) p)
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
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₃
p : P
⊢ Function.Injective ![i₁, i₂, i₃]

Tactic:
intro i j hij

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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
i j : Fin (Nat.succ 0).succ.succ
hij : ![i₁, i₂, i₃] i = ![i₁, i₂, i₃] j
⊢ i = j
Module: Mathlib.Geometry.Euclidean.Circumcenter

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✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
⊢ ∃! cs₂, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius

Tactic:
let ycc₂ := (x * x + y * y - cr * cr) / (2 * y)

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 : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
⊢ ∃! cs₂, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case h.left.right
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✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
p₁ : P
hp₁ : p₁ ∈ insert p ps
⊢ p₁ ∈ { center := cc₂, radius := cr₂ }

Tactic:
mem_sphere,

Goal state after:
case h.left.right
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✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
p₁ : P
hp₁ : p₁ ∈ insert p ps
⊢ dist p₁ { center := cc₂, radius := cr₂ }.center = { center := cc₂, radius := cr₂ }.radius
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

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
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₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁)
h₁' : excenter t signs = excenter t {i₁}
h₂' : excenter t signs = incenter t
⊢ excenter t signs = incenter t

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
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₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁)
h₁' : excenter t signs = excenter t {i₁}
h₂' : excenter t signs = excenter t {i₂}
⊢ excenter t signs = incenter t

Tactic:
· exact h₂'

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
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₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁)
h₁' : excenter t signs = excenter t {i₁}
h₂' : excenter t signs = excenter t {i₂}
⊢ excenter t signs = incenter t
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
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
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₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁) + ↑π
h₁' : excenter t signs = incenter t
h₂' : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₁}

Tactic:
· exact h₂'

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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
⊢ ¬√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖ = 0

Tactic:
div_eq_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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
⊢ ¬√(s.radius ^ 2 - dist p s.center ^ 2) = 0 * ‖v‖

V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
⊢ ‖v‖ ≠ 0
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

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
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₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃) + ↑π
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁) + ↑π
h₁' : excenter t signs = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₃}

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
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₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃) + ↑π
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁) + ↑π
h₁' : excenter t signs = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₃}

Tactic:
· exact h₂'

Goal state after:
case inl.inr
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₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃) + ↑π
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁) + ↑π
h₁' : excenter t signs = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₃}
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

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₁ : P
hp₁ : p₁ ∈ s
hr : s.radius ≠ 0
hp₂ : p₁ ∈ s
⊢ ∠ p₁ s.center p₁ = 0

Tactic:
exact angle_self_of_ne fun h => hr (center_mem_iff.mp (h ▸ hp₁))

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

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ ∡ p₁ s.center p₃ = 2 • ∡ p₁ p₂ p₃

Tactic:
mem_sphere,

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center = s.radius
hp₃ : dist p₃ s.center = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ ∡ p₁ s.center p₃ = 2 • ∡ p₁ p₂ p₃
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₄ : p₄ ∈ s
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄

Tactic:
mem_sphere,

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ p₄ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center = s.radius
hp₃ : dist p₃ s.center = s.radius
hp₄ : dist p₄ s.center = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: case convert_3
V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ 2 • ∡ p₁ p₂ p₃ + 2 • ∡ p₃ p₁ s.center = ↑π

Tactic:
rw [add_comm,
    two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi hp₁ hp₂ hp₃ hp₁p₂.symm hp₂p₃ hp₁p₃]

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

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 : Simplex ℝ P 0
i : Fin 1
h : s.circumcenter ∈ affineSpan ℝ (Set.range s.points)
a : Fin 1
⊢ a = default

Tactic:
simp only [Fin.eq_zero]

Goal state after:
Module: Mathlib.Geometry.Euclidean.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
inst✝ : n.AtLeastTwo
⊢ Function.Injective fun i ↦ s.excenter {i}

Tactic:
intro i j hij

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 : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : (fun i ↦ s.excenter {i}) i = (fun i ↦ s.excenter {i}) j
⊢ i = j
Module: Mathlib.Geometry.Euclidean.Triangle

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
a b c : P
hbc : ¬b = c
m : P := midpoint ℝ b c
this : dist b c ≠ 0
hm :
  dist a b ^ 2 * (2⁻¹ * dist b c) + dist a c ^ 2 * (2⁻¹ * dist b c) =
    dist b c * (dist a (midpoint ℝ b c) ^ 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))
⊢ 2 / dist b c * (dist a b ^ 2 * (2⁻¹ * dist b c) + dist a c ^ 2 * (2⁻¹ * dist b c)) =
    2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)

Tactic:
rw [hm]
        field

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

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 : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
⊢ Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}

Tactic:
by
  by_cases hc : Collinear ℝ ({p₁, p₂, p₄} : Set P)
  · by_cases he : p₁ = p₄
    · rw [he, Set.insert_eq_self.2
        (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _)))]
      by_cases hl : Collinear ℝ ({p₂, p₃, p₄} : Set P); · exact Or.inr hl
      rw [or_iff_left hl]
      let t : Affine.Triangle ℝ P := ⟨![p₂, p₃, p₄], affineIndependent_iff_not_collinear_set.2 hl⟩
      rw [cospherical_iff_exists_sphere]
      refine ⟨t.circumsphere, ?_⟩
      simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff]
      exact ⟨t.mem_circumsphere 0, t.mem_circumsphere 1, t.mem_circumsphere 2⟩
    have hc' : Collinear ℝ ({p₁, p₃, p₄} : Set P) := by
      rwa [← collinear_iff_of_two_zsmul_oangle_eq h]
    refine Or.inr ?_
    rw [Set.insert_comm p₁ p₂] at hc
    rwa [Set.insert_comm p₁ p₂, hc'.collinear_insert_iff_of_ne (Set.mem_insert _ _)
      (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))) he]
  · exact Or.inl (cospherical_of_two_zsmul_oangle_eq_of_not_collinear h hc)

Goal state after:
Module: Mathlib.Geometry.Euclidean.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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
signs : Finset (Fin (n + 1))
⊢ s.ExcenterExists signs ∧ p = s.excenter signs →
    ∃ r, ∀ (i : Fin (n + 1)), (s.signedInfDist i) p = (if i ∈ signs then -1 else 1) * r

Tactic:
rintro ⟨h, rfl⟩

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
hp : s.excenter signs ∈ affineSpan ℝ (Set.range s.points)
⊢ ∃ r, ∀ (i : Fin (n + 1)), (s.signedInfDist i) (s.excenter signs) = (if i ∈ signs then -1 else 1) * r
Module: Mathlib.Geometry.Euclidean.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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
⊢ Function.Injective (s.touchpoint signs)

Tactic:
intro i j hij

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 : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
⊢ i = j
Module: Mathlib.Topology.MetricSpace.Congruence

Goal state before:
pp: case pos
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
h : Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
hi : i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

pp: case neg
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
h : Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
hi : ¬i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

Tactic:
· simp [hi]

Goal state after:
case neg
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
h : Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
hi : ¬i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Geometry.Euclidean.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
inst✝ : n.AtLeastTwo
i : Fin (n + 1)
⊢ s.touchpoint ∅ i ∈ (s.faceOpposite i).interior

Tactic:
rw [faceOpposite, ← affineCombination_touchpointWeights,
    s.affineCombination_mem_interior_face_iff_pos _ (s.sum_touchpointWeights _ _)]
  simp only [Finset.mem_compl, Finset.mem_singleton, Decidable.not_not, forall_eq,
    touchpointWeights_eq_zero, and_true]
  intro j hj
  exact s.touchpointWeights_empty_pos (Ne.symm hj)

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : z = 0
⊢ y ∈ Submodule.span ℝ≥0 {x, z}

Tactic:
subst z

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : ¬x = 0
h : angle x 0 = angle x y + angle y 0
hxz₁ : ¬angle x 0 = π
hxz₂ : ¬angle x 0 = 0
h_sin_xz : Real.sin (angle x 0) ≠ 0
⊢ y ∈ Submodule.span ℝ≥0 {x, 0}
Module: Mathlib.Geometry.Euclidean.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
inst✝ : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : ∑ i, s.excenterWeightsUnnorm signs i ≠ 0
i j : Fin (n + 1)
he : Pi.single j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : (if k ∈ signs then -1 else 1) * (s.height k)⁻¹ = 0
hk : k ∈ signs
⊢ False

Tactic:
simp [hk, (s.height_pos k).ne'] at he'

Goal state after: