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

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

Tactic:
rintro p hp

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

Goal state before:
pp: case neg.refine_3
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ s₂.radius - s₁.radius ≤ s₂.radius

pp: case neg.refine_3
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ 0 < s₂.radius - s₁.radius

Tactic:
· linarith

Goal state after:
case neg.refine_3
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ 0 < s₂.radius - s₁.radius
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case h.left.right.inl
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₁ = p
⊢ dist p₁ { center := cc₂, radius := cr₂ }.center * dist p₁ { center := cc₂, radius := cr₂ }.center =
    cr * cr + ycc₂ * ycc₂

Tactic:
rw [hp₁, hpo,
          dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd (orthogonalProjection_mem p) hcc _ _
            (vsub_orthogonalProjection_mem_direction_orthogonal s p),
          Real.norm_eq_abs, abs_mul_abs_self, ← dist_eq_norm_vsub V p, dist_comm _ cc]

Goal state after:
case h.left.right.inl
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₁ = p
⊢ dist cc ↑((orthogonalProjection s) p) * dist cc ↑((orthogonalProjection s) p) +
      (1 - ycc₂ / y) * (1 - ycc₂ / y) * (dist p ↑((orthogonalProjection s) p) * dist p ↑((orthogonalProjection s) p)) =
    cr * cr + ycc₂ * ycc₂
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) ∈
    ↑(Submodule.span ℝ (Set.range fun i ↦ s.points ↑i -ᵥ s.points 0))ᗮ

Tactic:
Submodule.span_range_eq_iSup,

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, (s.height i)⁻¹ ^ 2 • (s.points i -ᵥ s.altitudeFoot i) ∈ ↑(⨆ i, ℝ ∙ (s.points ↑i -ᵥ s.points 0))ᗮ
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₁ + (∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖

Tactic:
div_inv_eq_mul,

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₂
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * √(1 + (∡ p₂ p₁ s.center).tan ^ 2) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ + (∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this✝ : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
h✝ : r₁ + r₂ - 1 = 0
⊢ False

pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this✝ : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
h✝ : x + y = 0
⊢ False

Tactic:
· linarith

Goal state after:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this✝ : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
h✝ : x + y = 0
⊢ False
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)
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁ : t₁.points i₁ = t₂.points i₁
h₃ : t₁.points i₃ = t₂.points i₃
h₂ : 2 • ∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃) = 2 • ∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)
⊢ {
      center :=
        ((∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).tan⁻¹ / 2) •
            («o».rotation ↑(π / 2)) (t₁.points i₃ -ᵥ t₁.points i₁) +ᵥ
          midpoint ℝ (t₁.points i₁) (t₁.points i₃),
      radius := dist (t₁.points i₁) (t₁.points i₃) / |(∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).sin| / 2 } =
    {
      center :=
        ((∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).tan⁻¹ / 2) •
            («o».rotation ↑(π / 2)) (t₂.points i₃ -ᵥ t₂.points i₁) +ᵥ
          midpoint ℝ (t₂.points i₁) (t₂.points i₃),
      radius := dist (t₂.points i₁) (t₂.points i₃) / |(∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).sin| / 2 }

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁ : t₁.points i₁ = t₂.points i₁
h₃ : t₁.points i₃ = t₂.points i₃
h₂ : 2 • ∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃) = 2 • ∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)
⊢ {
      center :=
        ((∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).tan⁻¹ / 2) •
            («o».rotation ↑(π / 2)) (t₁.points i₃ -ᵥ t₂.points i₁) +ᵥ
          midpoint ℝ (t₂.points i₁) (t₁.points i₃),
      radius := dist (t₂.points i₁) (t₁.points i₃) / |(∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).sin| / 2 } =
    {
      center :=
        ((∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).tan⁻¹ / 2) •
            («o».rotation ↑(π / 2)) (t₂.points i₃ -ᵥ t₂.points i₁) +ᵥ
          midpoint ℝ (t₂.points i₁) (t₂.points i₃),
      radius := dist (t₂.points i₁) (t₂.points i₃) / |(∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).sin| / 2 }
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)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h : 2 • ∡ (t.points i₁) p (t.points i₃) = 2 • ∡ (t.points i₁) (t.points i₂) (t.points i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = t.points i₃
⊢ ¬Collinear ℝ {t'p i₁, t'p i₂, t'p i₃}

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h : 2 • ∡ (t.points i₁) p (t.points i₃) = 2 • ∡ (t.points i₁) (t.points i₂) (t.points i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = t.points i₃
⊢ ¬Collinear ℝ {t.points i₁, t'p i₂, t'p i₃}
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 : ℕ
r : ℝ
s : Simplex ℝ P n
p₁ : P
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h : s.points 0 ∈ affineSpan ℝ (Set.range s.points)
⊢ dist s.circumcenter p₁ * dist s.circumcenter p₁ =
    dist (s.points 0) p₁ * dist (s.points 0) p₁ - s.circumradius * s.circumradius

Tactic:
s.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₁ 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 : ℕ
r : ℝ
s : Simplex ℝ P n
p₁ : P
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h : s.points 0 ∈ affineSpan ℝ (Set.range s.points)
⊢ dist s.circumcenter p₁ * dist s.circumcenter p₁ =
    dist (s.points 0) ↑(s.orthogonalProjectionSpan p₁) * dist (s.points 0) ↑(s.orthogonalProjectionSpan p₁) +
        dist p₁ ↑(s.orthogonalProjectionSpan p₁) * dist p₁ ↑(s.orthogonalProjectionSpan p₁) -
      s.circumradius * s.circumradius
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)
hr : ∀ (i : Fin (n + 1)), dist (s₂.points i) s₁.circumcenter = s₁.circumradius
⊢ s₁.circumcenter = s₂.circumcenter

Tactic:
exact s₂.eq_circumcenter_of_dist_eq hs hr

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
hf : Fact (Module.finrank ℝ V = n)
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ n - 1 + 1 = Module.finrank ℝ V

Tactic:
hf.out

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
hf : Fact (Module.finrank ℝ V = n)
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ n - 1 + 1 = n
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case mp
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))
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
hw : ∑ j, w j = 1
⊢ (Finset.affineCombination ℝ Finset.univ s.points) w = s.touchpoint signs i → w = s.touchpointWeights signs i

Tactic:
← s.affineCombination_touchpointWeights

Goal state after:
case mp
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))
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
hw : ∑ j, w j = 1
⊢ (Finset.affineCombination ℝ Finset.univ s.points) w =
      (Finset.affineCombination ℝ Finset.univ s.points) (s.touchpointWeights signs i) →
    w = s.touchpointWeights signs i
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ Simplex.excenter t {i} = Simplex.incenter t ∨ ∃ i_1, Simplex.excenter t {i} = Simplex.excenter t {i_1}

pp: case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ Simplex.excenter t {i}ᶜ = Simplex.incenter t ∨ ∃ i_1, Simplex.excenter t {i}ᶜ = Simplex.excenter t {i_1}

Tactic:
· exact .inr ⟨i, rfl⟩

Goal state after:
case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ Simplex.excenter t {i}ᶜ = Simplex.incenter t ∨ ∃ i_1, Simplex.excenter t {i}ᶜ = Simplex.excenter t {i_1}
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ Simplex.excenter t {i}ᶜ = Simplex.incenter t ∨ ∃ i_1, Simplex.excenter t {i}ᶜ = Simplex.excenter t {i_1}

Tactic:
refine .inr ⟨i, ?_⟩

Goal state after:
case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i : Fin 3
⊢ Simplex.excenter t {i}ᶜ = Simplex.excenter t {i}
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
v₃ : ι → P₃
inst✝² : PseudoEMetricSpace P₁
inst✝¹ : PseudoEMetricSpace P₂
inst✝ : PseudoEMetricSpace P₃
r₁ : ℝ≥0
hr₁ : r₁ ≠ 0
h₁ : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r₁ * edist (v₂ i₁) (v₂ i₂)
r₂ : ℝ≥0
hr₂ : r₂ ≠ 0
h₂ : ∀ (i₁ i₂ : ι), edist (v₂ i₁) (v₂ i₂) = ↑r₂ * edist (v₃ i₁) (v₃ i₂)
x✝¹ x✝ : ι
⊢ edist (v₁ x✝¹) (v₁ x✝) = ↑r₁ * (↑r₂ * edist (v₃ x✝¹) (v₃ x✝))

Tactic:
h₁,

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
v₃ : ι → P₃
inst✝² : PseudoEMetricSpace P₁
inst✝¹ : PseudoEMetricSpace P₂
inst✝ : PseudoEMetricSpace P₃
r₁ : ℝ≥0
hr₁ : r₁ ≠ 0
h₁ : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r₁ * edist (v₂ i₁) (v₂ i₂)
r₂ : ℝ≥0
hr₂ : r₂ ≠ 0
h₂ : ∀ (i₁ i₂ : ι), edist (v₂ i₁) (v₂ i₂) = ↑r₂ * edist (v₃ i₁) (v₃ i₂)
x✝¹ x✝ : ι
⊢ ↑r₁ * edist (v₂ x✝¹) (v₂ x✝) = ↑r₁ * (↑r₂ * edist (v₃ x✝¹) (v₃ x✝))
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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
⊢ ⅟2 • (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      ⅟2 •
        ((↑n)⁻¹ • (s.points i -ᵥ s.circumcenter) -
          (((↑n)⁻¹ - 1) * (↑(n + 1) / ↑(n - 1))) • (s.centroid -ᵥ s.circumcenter)) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)

Tactic:
show ((n : ℝ)⁻¹ - 1) = -(n - 1) / n by field [hn.out],

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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
⊢ ⅟2 • (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      ⅟2 •
        ((↑n)⁻¹ • (s.points i -ᵥ s.circumcenter) -
          (-(↑n - 1) / ↑n * (↑(n + 1) / ↑(n - 1))) • (s.centroid -ᵥ s.circumcenter)) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ 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
⊢ angle z y = π / 2

Tactic:
← norm_add_eq_norm_sub_iff_angle_eq_pi_div_two,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
⊢ ‖z + y‖ = ‖z - y‖
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₃}
this : ∠ p₁ p₂ p₃ = ∠ p₁ p₄ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₄ p₃

Tactic:
grind [oangle_eq_of_angle_eq_of_sign_eq, Sbtw.oangle_sign_eq_of_sbtw]

Goal state after:
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₃}
⊢ {t₂.points j₁, t₂.points j₂, t₂.points j₃} ⊆ ↑(affineSpan ℝ (Set.range t₁.points))

Tactic:
h₁,

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₁.orthocenter, t₂.points j₂, t₂.points j₃} ⊆ ↑(affineSpan ℝ (Set.range t₁.points))
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case right
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₃
he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)
hu : {j₂}ᶜ = {j₁, j₃}
⊢ t₁.points i₁ -ᵥ t₁.points i₂ ∈ line[ℝ, t₂.points j₁, t₂.points j₃].directionᗮ

Tactic:
h₁,

Goal state after:
case right
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₃
he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)
hu : {j₂}ᶜ = {j₁, j₃}
⊢ t₁.points i₁ -ᵥ t₁.points i₂ ∈ line[ℝ, t₁.orthocenter, t₂.points j₃].directionᗮ
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case right.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ dist (p i₃) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t

Tactic:
rw [← h₃,
        dist_reflection_eq_of_mem _
          (mem_affineSpan ℝ
            (Set.mem_image_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))))]

Goal state after:
case right.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ dist (t.points j₃) (Simplex.circumcenter t) = Simplex.circumradius t
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
⊢ I.IsInteriorPoint x ↔ ¬I.IsBoundaryPoint x

Tactic:
refine ⟨?_,
    by simpa only [or_iff_not_imp_right] using isInteriorPoint_or_isBoundaryPoint x (I := I)⟩

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
⊢ I.IsInteriorPoint x → ¬I.IsBoundaryPoint x