mathlib-initiative/mathlib-tactics huggingface dataset:
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
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
h : 0 = t
⊢ (AffineMap.lineMap p₁ p₂) t = p₁

Tactic:
← 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
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
h : 0 = t
⊢ (AffineMap.lineMap p₁ p₂) 0 = 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
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
⊢ dist o p < s.radius

Tactic:
set v := p₂ -ᵥ o

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
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
⊢ dist o p < s.radius
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₂ 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₁}
⊢ Fintype.card (Fin (Nat.succ 0).succ.succ) = finrank ℝ V + 1

Tactic:
simpa using Fact.out

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₁ s₂ : Sphere P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
h : dist s₁.center p + dist p s₂.center = dist s₁.center s₂.center
⊢ dist s₁.center s₂.center = s₁.radius + s₂.radius

Tactic:
← 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
s₁ s₂ : Sphere P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
h : dist s₁.center p + dist p s₂.center = dist s₁.center s₂.center
⊢ dist s₁.center p + dist p s₂.center = s₁.radius + s₂.radius
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' -ᵥ p ∈ (s.orthRadius p).direction

Tactic:
vsub_right_mem_direction_iff_mem (s.self_mem_orthRadius p)

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 : 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
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)⁻¹ =
    ∑ j with j ≠ i,
      -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) * (s.height j)⁻¹

Tactic:
by
  rw [← sub_eq_zero]
  simp_rw [neg_mul]
  rw [Finset.sum_neg_distrib, sub_neg_eq_add, Finset.filter_ne',
    Finset.sum_erase_eq_sub (Finset.mem_univ _), real_inner_self_eq_norm_mul_norm,
    ← dist_eq_norm_vsub]
  simp only [height, ne_eq, mul_eq_zero, dist_eq_zero, ne_altitudeFoot, or_self,
    not_false_eq_true, div_self, one_mul, add_sub_cancel]
  have h := s.sum_inv_height_sq_smul_vsub_eq_zero
  apply_fun fun v ↦ (s.height i)⁻¹ * ⟪s.points i -ᵥ s.altitudeFoot i, v⟫ at h
  rw [inner_sum, Finset.mul_sum] at h
  simp only [inner_zero_right, mul_zero, inner_smul_right, height] at h
  convert! h using 2 with j
  ring

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 : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
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)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
p0 : P
hp0 : p0 ∈ ps
h' : ↑⟨cc, hcc₃'⟩ = cc
⊢ dist p0 (t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc) *
      dist p0 (t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc) =
    √(cr * cr + t₃ * y * (t₃ * y)) * √(cr * cr + t₃ * y * (t₃ * y))

Tactic:
Real.mul_self_sqrt (add_nonneg (mul_self_nonneg _) (mul_self_nonneg _)),

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
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)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
p0 : P
hp0 : p0 ∈ ps
h' : ↑⟨cc, hcc₃'⟩ = cc
⊢ dist p0 (t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc) *
      dist p0 (t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc) =
    cr * cr + t₃ * y * (t₃ * y)
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inr.inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
hxy : x ≠ y
h_sin : ∀ (x y : V), x ≠ 0 → y ≠ 0 → Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) * ‖x‖ =
    √(⟪y, y⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) - (⟪x, y⟫ - ⟪y, y⟫) * (⟪x, y⟫ - ⟪y, y⟫)) / (‖y‖ * ‖x - y‖) *
      ‖x - y‖

Tactic:
have hsub : x - y ≠ 0 := sub_ne_zero_of_ne hxy

Goal state after:
case inr.inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
hxy : x ≠ y
h_sin : ∀ (x y : V), x ≠ 0 → y ≠ 0 → Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
hsub : x - y ≠ 0
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) * ‖x‖ =
    √(⟪y, y⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) - (⟪x, y⟫ - ⟪y, y⟫) * (⟪x, y⟫ - ⟪y, y⟫)) / (‖y‖ * ‖x - y‖) *
      ‖x - y‖
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)
signs : Finset (Fin (m + 1))
⊢ (s.reindex e).exsphere signs = s.exsphere (Finset.map e.symm.toEmbedding signs)

Tactic:
simp_rw [exsphere, excenterWeightsUnnorm_reindex, excenterWeights_reindex, Finset.sum_comp_equiv,
    reindex, ← Equiv.coe_toEmbedding, ← Finset.affineCombination_map]
  simp

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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
r : ℝ
hr : r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
⊢ ((«o».oangle (midpoint ℝ p₁ p₂ -ᵥ p₁) ((r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂) -ᵥ p₁)).tan / 2) •
        («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ
      midpoint ℝ p₁ p₂ =
    r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂

Tactic:
vadd_vsub_assoc

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₂
r : ℝ
hr : r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
⊢ ((«o».oangle (midpoint ℝ p₁ p₂ -ᵥ p₁) (r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) + (midpoint ℝ p₁ p₂ -ᵥ p₁))).tan / 2) •
        («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ
      midpoint ℝ p₁ p₂ =
    r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case h.right.refl
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)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
hcr₃val : cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
hcr₃ :
  dist cc ↑((orthogonalProjection s) p) * dist cc ↑((orthogonalProjection s) p) +
      (1 - t₃) * (1 - t₃) * (dist p ↑((orthogonalProjection s) p) * dist p ↑((orthogonalProjection s) p)) =
    cr * cr + t₃ * y * (t₃ * y)
⊢ { center := cc₃, radius := cr₃ } = { center := cc₂, radius := cr₂ }

Tactic:
have : t₃ * y = ycc₂ := by grind

Goal state after:
case h.right.refl
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)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
hcr₃val : cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
hcr₃ :
  dist cc ↑((orthogonalProjection s) p) * dist cc ↑((orthogonalProjection s) p) +
      (1 - t₃) * (1 - t₃) * (dist p ↑((orthogonalProjection s) p) * dist p ↑((orthogonalProjection s) p)) =
    cr * cr + t₃ * y * (t₃ * y)
this : t₃ * y = ycc₂
⊢ { center := cc₃, radius := cr₃ } = { center := cc₂, radius := cr₂ }
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 + 1)
h : 0 = s.circumradius
hr : ∀ (i : Fin (n + 1 + 1)), dist (s.points i) s.circumcenter = s.circumradius
⊢ False

Tactic:
← h,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 1)
h : 0 = s.circumradius
hr : ∀ (i : Fin (n + 1 + 1)), dist (s.points i) s.circumcenter = 0
⊢ False
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₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
hs : s₁.circumcenter ∈ affineSpan ℝ (Set.range s₂.points)
i : Fin (n + 1)
hi : s₂.points i ∈ Set.range s₂.points
⊢ dist (s₂.points i) s₁.circumcenter = s₁.circumradius

Tactic:
← h,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
hs : s₁.circumcenter ∈ affineSpan ℝ (Set.range s₂.points)
i : Fin (n + 1)
hi : s₂.points i ∈ Set.range s₁.points
⊢ dist (s₂.points i) s₁.circumcenter = s₁.circumradius
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]

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 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 b c * (dist a (midpoint ℝ b c) ^ 2 + 2⁻¹ * dist b c * (2⁻¹ * dist b c))) =
    2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2)
Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane

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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R '' ↑(perpBisector c y) = sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}

Tactic:
by
  rw [image_eq_preimage_of_inverse (inversion_involutive _ hR) (inversion_involutive _ hR),
    preimage_inversion_perpBisector hR hy]

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

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
t : Triangle ℝ P
i₂ i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
i : Fin (2 + 1)
h₁₂ : i ≠ i₂
h₁₃ : i ≠ i₃
hw : Simplex.touchpointWeights t {i} i₂ i + Simplex.touchpointWeights t {i} i₂ i₃ = 1
⊢ Simplex.touchpointWeights t {i} i₂ i =
    Finset.affineCombinationLineMapWeights i i₃ (Simplex.touchpointWeights t {i} i₂ i₃) i

Tactic:
Finset.affineCombinationLineMapWeights_apply_left h₁₃

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
t : Triangle ℝ P
i₂ i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
i : Fin (2 + 1)
h₁₂ : i ≠ i₂
h₁₃ : i ≠ i₃
hw : Simplex.touchpointWeights t {i} i₂ i + Simplex.touchpointWeights t {i} i₂ i₃ = 1
⊢ Simplex.touchpointWeights t {i} i₂ i = 1 - Simplex.touchpointWeights t {i} i₂ i₃
Module: Mathlib.Geometry.Euclidean.NinePointCircle

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
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
hn : ¬n = 0
⊢ s.points i -ᵥ s.mongePoint - (↑n)⁻¹ • (s.points i -ᵥ s.mongePoint) = (↑n / ↑n - 1 / ↑n) • (s.points i -ᵥ s.mongePoint)

Tactic:
div_self (by simpa using hn),

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
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
hn : ¬n = 0
⊢ s.points i -ᵥ s.mongePoint - (↑n)⁻¹ • (s.points i -ᵥ s.mongePoint) = (1 - 1 / ↑n) • (s.points i -ᵥ s.mongePoint)
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
h : Invertible (↑n + 2 + 1)
⊢ (↑n + 2 + 1) • (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) = ∑ i, (s.points i -ᵥ s.circumcenter)

Tactic:
rw [smul_eq_iff_eq_invOf_smul, smul_sum]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
h : Invertible (↑n + 2 + 1)
⊢ Finset.centroid ℝ univ s.points -ᵥ s.circumcenter = ∑ x, ⅟(↑n + 2 + 1) • (s.points x -ᵥ s.circumcenter)
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
h : Invertible (↑n + 2 + 1)
⊢ (affineCombination ℝ univ s.points) (centroidWeights ℝ univ) -ᵥ s.circumcenter =
    ∑ x, ⅟(↑n + 2 + 1) • (s.points x -ᵥ s.circumcenter)

Tactic:
← Finset.sum_smul_vsub_const_eq_affineCombination_vsub _ _ _ _ (by simp)

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
h : Invertible (↑n + 2 + 1)
⊢ ∑ i, centroidWeights ℝ univ i • (s.points i -ᵥ s.circumcenter) = ∑ x, ⅟(↑n + 2 + 1) • (s.points x -ᵥ s.circumcenter)
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
hzx : ⟪z, x⟫ = 0
⊢ |r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2| = |‖x‖ ^ 2 - ‖y‖ ^ 2|

Tactic:
by simp [hr, norm_smul, mul_pow, sq_abs]

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

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

Tactic:
suffices h_sim : Similar ![p₁, p, p₄] ![p₃, p, p₂] by
    grind [angle_comm, h_sim.angle_eq_all.right.left]

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

Goal state before:
pp: V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : dist p t ^ 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
x : P
hx : x ∈ line[ℝ, p, t]
r : ℝ
hr : r • (p -ᵥ t) = x -ᵥ t
⊢ (starRingEnd ℝ) r * ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0

Tactic:
h_orth,

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

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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
hu : Set.univ = {j₁, j₂, j₃}
⊢ insert (t₂.points j₁) (insert (t₂.points j₂) (t₂.points '' {j₃})) ⊆ ↑(affineSpan ℝ (Set.range t₁.points))

Tactic:
Set.image_singleton,

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
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
hu : Set.univ = {j₁, j₂, j₃}
⊢ {t₂.points j₁, t₂.points j₂, t₂.points j₃} ⊆ ↑(affineSpan ℝ (Set.range t₁.points))