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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ ↑π + ↑(π / 2) + ↑(π / 2) = 0

pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ (o.rotation ↑(π / 2)) x ≠ 0

Tactic:
← Real.Angle.coe_add,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ ↑(π + π / 2) + ↑(π / 2) = 0

V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ (o.rotation ↑(π / 2)) x ≠ 0
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ ↑(π + π / 2) + ↑(π / 2) = 0

pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ (o.rotation ↑(π / 2)) x ≠ 0

Tactic:
← Real.Angle.coe_add,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ ↑(π + π / 2 + π / 2) = 0

V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ (o.rotation ↑(π / 2)) x ≠ 0
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Projection

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
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ ↑((orthogonalProjection s) p)
⊢ 2 • ∡ p (↑((orthogonalProjection s) p)) p' = ↑π

Tactic:
by
  rw [Real.Angle.two_zsmul_eq_pi_iff]
  exact oangle_self_orthogonalProjection p hp h hp'

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

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
⊢ (o.oangle (r • y - x) y).sign = -(o.oangle x y).sign

Tactic:
rw [← oangle_sign_neg_left, sub_eq_neg_add, oangle_sign_add_smul_left]

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

Goal state before:
pp: case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : r₁ = 0
⊢ (o.oangle (r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (0 - r₂ * r₃) * (o.oangle x y).sign

Tactic:
zero_sub,

Goal state after:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : r₁ = 0
⊢ (o.oangle (r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (-(r₂ * r₃)) * (o.oangle x y).sign
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x ↦ (↑x.1, p₅, x.2 +ᵥ ↑x.1)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ line[ℝ, p₁, p₂]
⊢ 0 - r • (p₂ -ᵥ p₁) ≠ 0

Tactic:
zero_sub,

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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x ↦ (↑x.1, p₅, x.2 +ᵥ ↑x.1)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ line[ℝ, p₁, p₂]
⊢ -(r • (p₂ -ᵥ p₁)) ≠ 0
Module: Mathlib.Geometry.Euclidean.PerpBisector

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 p : P
hab : a ≠ b
hp : p ∈ perpBisector a b
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b) s)
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b) s -ᵥ midpoint ℝ a b⟫ = 0

Tactic:
← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p : P
hab : a ≠ b
hp : p ∈ perpBisector a b
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b) s)
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
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
p q : P
⊢ ((signedDist (p -ᵥ q)) p) q = -dist p q

Tactic:
rw [← neg_eq_iff_eq_neg, ← signedDist_neg, neg_vsub_eq_vsub_rev]
  apply signedDist_vsub_self

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
r : ℝ
v : V
p₁ p₂ : P
⊢ r * ⟪v, r • v⟫ + 2 * (r * ⟪v, p₁ -ᵥ p₂⟫) + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ =
    ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫

Tactic:
real_inner_smul_right

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
r : ℝ
v : V
p₁ p₂ : P
⊢ r * (r * ⟪v, v⟫) + 2 * (r * ⟪v, p₁ -ᵥ p₂⟫) + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ =
    ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ 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
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ AffineIndependent ℝ ![p₁, p₂, p₃]

Tactic:
by
  refine hs.affineIndependent ?_ ?_
  · simp [h₁, h₂, h₃, Set.insert_subset_iff]
  · simp only [Matrix.vecCons, Fin.cons_injective_iff]
    simp [h₁₂, h₁₃, h₂₃, Function.Injective, eq_iff_true_of_subsingleton]

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✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp : Sbtw ℝ p₁ p p₂
⊢ dist s.center p < s.radius

Tactic:
set o := s.center

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp : Sbtw ℝ p₁ p p₂
o : P := s.center
⊢ dist o p < s.radius
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

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

Tactic:
real_inner_self_eq_norm_mul_norm,

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 : Sphere P
p₁ p₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖ - ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫
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 : V
hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ), ∃ c, c • ⟨v, hv⟩ = w
hvc : ∀ w ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ, ∃ c, c • v = w
hvp : 0 ≤ s.radius ^ 2 - dist p s.center ^ 2
p' : P
h : p' ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)
⊢ p' ∈ s.orthRadius p

Tactic:
exact h.2

Goal state after:
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₃
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₁)
⊢ excenter t signs = incenter t

Tactic:
have h₁' := t.eq_incenter_or_eq_excenter_singleton_of_oangle_eq h₁₂ 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
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 ∨ excenter t signs = excenter t {i₁}
⊢ excenter t signs = incenter t
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₃
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₁) + ↑π
⊢ excenter t signs = excenter t {i₁}

Tactic:
have h₁' := t.eq_incenter_or_eq_excenter_singleton_of_oangle_eq h₁₂ 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
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 ∨ excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₁}
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
h₁ : ∡ (t.points i₂) (t.points i₁) p = ∡ p (t.points i₁) (t.points i₃)
h₂ : ∡ (t.points i₃) (t.points i₂) p = ∡ p (t.points i₂) (t.points i₁) + ↑π
⊢ p = excenter t {i₁}

Tactic:
obtain ⟨signs, rfl⟩ := t.eq_excenter_of_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃ (by rw [h₁])
    (by rw [h₂]; simp)
  have h₁' := t.eq_incenter_or_eq_excenter_singleton_of_oangle_eq h₁₂ h₁₃ h₂₃ h₁
  have h₂' := t.eq_excenter_singleton_of_oangle_eq_add_pi h₂₃ h₁₂.symm h₁₃.symm h₂
  rcases h₁' with h₁' | h₁'
  · rcases h₂' with h₂' | h₂'
    · rw [h₁'] at h₂'
      exfalso
      exact (t.excenter_singleton_ne_incenter _).symm h₂'
    · exact h₂'
  · exact h₁'

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
this :
  ∀ (i : Fin (n + 1)),
    i ≠ 0 → ∑ j, ⟪s.points i -ᵥ s.points 0, (s.height j)⁻¹ ^ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫ = 0
⊢ ∑ i, (s.height i)⁻¹ ^ 2 • (s.points i -ᵥ s.altitudeFoot i) ∈ ↑(vectorSpan ℝ (Set.range s.points))ᗮ

Tactic:
rw [vectorSpan_range_eq_span_range_vsub_right_ne _ _ 0, Submodule.span_range_eq_iSup,
      ← Submodule.iInf_orthogonal, Submodule.coe_iInf, Set.mem_iInter]

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
this :
  ∀ (i : Fin (n + 1)),
    i ≠ 0 → ∑ j, ⟪s.points i -ᵥ s.points 0, (s.height j)⁻¹ ^ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫ = 0
⊢ ∀ (i : { x // x ≠ 0 }),
    ∑ i, (s.height i)⁻¹ ^ 2 • (s.points i -ᵥ s.altitudeFoot i) ∈ ↑(ℝ ∙ (s.points ↑i -ᵥ s.points 0))ᗮ
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case e'_2.a
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)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ (Finset.univ.erase 0).erase i
⊢ ⟪s.points i -ᵥ s.points 0, (s.height j)⁻¹ ^ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫ = 0

Tactic:
real_inner_smul_right

Goal state after:
case e'_2.a
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)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ (Finset.univ.erase 0).erase i
⊢ (s.height j)⁻¹ ^ 2 * ⟪s.points i -ᵥ s.points 0, s.points j -ᵥ s.altitudeFoot j⟫ = 0
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
i : Fin (n + 1)
⊢ (s.height i)⁻¹ +
      (∑ x,
          ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) *
            (s.height x)⁻¹ -
        ⟪s.points i -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ / (s.height i * s.height i) * (s.height i)⁻¹) =
    0

Tactic:
real_inner_self_eq_norm_mul_norm,

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
i : Fin (n + 1)
⊢ (s.height i)⁻¹ +
      (∑ x,
          ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) *
            (s.height x)⁻¹ -
        ‖s.points i -ᵥ s.altitudeFoot i‖ * ‖s.points i -ᵥ s.altitudeFoot i‖ / (s.height i * s.height i) *
          (s.height i)⁻¹) =
    0
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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).insphere = s.insphere

Tactic:
by
  simp_rw [insphere, exsphere_reindex]
  simp

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
⊢ (⟪x, x⟫ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (⟪y, y⟫ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)

Tactic:
real_inner_self_eq_norm_mul_norm,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
⊢ (‖x‖ * ‖x‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (⟪y, y⟫ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
⊢ (‖x‖ * ‖x‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (⟪y, y⟫ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)

Tactic:
real_inner_self_eq_norm_mul_norm,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
⊢ (‖x‖ * ‖x‖ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (‖y‖ * ‖y‖ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
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
V₂ : Type u_3
P₂ : Type u_4
inst✝⁴ : NormedAddCommGroup V₂
inst✝³ : InnerProductSpace ℝ V₂
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₂ P₂
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
x✝ : Finset (Fin (n + 1))
⊢ (s.map f.toAffineMap ⋯).exradius x✝ = s.exradius x✝

Tactic:
simp [exradius, exsphere]

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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
x✝ : Finset (Fin (n + 1))
⊢ (s.restrict S hS).exradius x✝ = s.exradius x✝

Tactic:
simp [exradius, exsphere]

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

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖x - y‖)
hxy : ¬x = y
⊢ ‖x‖ = ‖y‖

Tactic:
mul_comm,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : ⟪x, x - y⟫ / (‖x - y‖ * ‖x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖x - y‖)
hxy : ¬x = y
⊢ ‖x‖ = ‖y‖
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : (⟪x, x⟫ - ⟪x, y⟫) * ‖x‖⁻¹ = (⟪y, y⟫ - ⟪x, y⟫) * ‖y‖⁻¹
⊢ ‖x‖ = ‖y‖

Tactic:
real_inner_self_eq_norm_mul_norm,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : (‖x‖ * ‖x‖ - ⟪x, y⟫) * ‖x‖⁻¹ = (⟪y, y⟫ - ⟪x, y⟫) * ‖y‖⁻¹
⊢ ‖x‖ = ‖y‖
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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ dist p₁ p₂ * 2⁻¹ / (∡ p₂ p₁ s.center).cos = s.radius

Tactic:
mul_comm,

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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ 2⁻¹ * dist p₁ p₂ / (∡ p₂ p₁ s.center).cos = s.radius
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : (‖x‖ * ‖x‖ - ⟪x, y⟫) * ‖x‖⁻¹ = (⟪y, y⟫ - ⟪x, y⟫) * ‖y‖⁻¹
⊢ ‖x‖ = ‖y‖

Tactic:
real_inner_self_eq_norm_mul_norm,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : (‖x‖ * ‖x‖ - ⟪x, y⟫) * ‖x‖⁻¹ = (‖y‖ * ‖y‖ - ⟪x, y⟫) * ‖y‖⁻¹
⊢ ‖x‖ = ‖y‖
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : 0 - ‖y‖ = 0
hx0 : x = 0
⊢ ‖x‖ = ‖y‖

Tactic:
zero_sub,

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : -‖y‖ = 0
hx0 : x = 0
⊢ ‖x‖ = ‖y‖
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : -(‖y‖ - ‖x‖) = ⟪x, y⟫ * (‖y‖ - ‖x‖) / (‖x‖ * ‖y‖)
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖x‖ = ‖y‖

Tactic:
mul_comm,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : -(‖y‖ - ‖x‖) = (‖y‖ - ‖x‖) * ⟪x, y⟫ / (‖x‖ * ‖y‖)
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖x‖ = ‖y‖
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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * √(1 + (∡ p₂ p₁ s.center).tan ^ 2) * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ *
      √(1 + (∡ p₂ p₁ s.center).tan ^ 2) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
      ‖(∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖ *
        ‖(∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖

Tactic:
mul_comm,

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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ √(1 + (∡ p₂ p₁ s.center).tan ^ 2) *
      (‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * √(1 + (∡ p₂ p₁ s.center).tan ^ 2) * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
      ‖(∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖ *
        ‖(∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖
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
n : ℕ
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
h : p = s.circumsphere.center ∧ r = s.circumsphere.radius
⊢ r = s.circumradius

Tactic:
exact h.2

Goal state after:
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
p₁ p₂ p₃ : P
h : ¬Collinear ℝ {p₁, p₂, p₃}
sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃)
⊢ dist p₁ p₂ * Real.sin (∠ p₁ p₂ p₃) = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁)

Tactic:
mul_comm,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ¬Collinear ℝ {p₁, p₂, p₃}
sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃)
⊢ Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂ = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁)