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

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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p) ↔
    Real.arcsin (dist p ↑((orthogonalProjection s₁) p) / dist p p') =
      Real.arcsin (dist p ↑((orthogonalProjection s₂) p) / dist p p')

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
    · rw [h]
    · have hp : p ≠ p' := by
        rintro rfl
        exact h'.1 hp'₁
      have hpd : 0 < dist p p' := dist_pos.2 hp
      rw [Real.arcsin_inj (le_trans (by norm_num : (-1 : ℝ) ≤ 0) (by positivity))
        ((div_le_one hpd).2 ?_)
        (le_trans (by norm_num : (-1 : ℝ) ≤ 0) (by positivity)) ((div_le_one hpd).2 ?_)] at h
      · rwa [div_left_inj' hpd.ne'] at h
      · rw [dist_orthogonalProjection_eq_infDist]
        exact Metric.infDist_le_dist_of_mem (SetLike.mem_coe.1 hp'₁)
      · rw [dist_orthogonalProjection_eq_infDist]
        exact Metric.infDist_le_dist_of_mem (SetLike.mem_coe.1 hp'₂)

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

Goal state before:
pp: case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p q : P
h✝ : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
⊢ 0 ≤ ‖v‖⁻¹ * ‖q -ᵥ p‖ ∧ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p

Tactic:
constructor

Goal state after:
case h.left
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p q : P
h✝ : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
⊢ 0 ≤ ‖v‖⁻¹ * ‖q -ᵥ p‖

case h.right
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p q : P
h✝ : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
⊢ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p
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
v : V
p q : P
c : ℝ
⊢ ((signedDist v) ((AffineMap.lineMap p q) c)) q = (1 - c) * ((signedDist v) p) q

Tactic:
simpa using signedDist_lineMap_lineMap v p q c 1

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

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

Goal state before:
pp: P : Type u_2
inst✝ : MetricSpace P
s : Sphere P
⊢ { center := s.center, radius := s.radius } = s

Tactic:
ext

Goal state after:
case center
P : Type u_2
inst✝ : MetricSpace P
s : Sphere P
⊢ { center := s.center, radius := s.radius }.center = s.center

case radius
P : Type u_2
inst✝ : MetricSpace P
s : Sphere P
⊢ { center := s.center, radius := s.radius }.radius = s.radius
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : Nontrivial V
s : Sphere P
⊢ (Metric.sphere s.center s.radius).Nonempty ↔ 0 ≤ s.radius

Tactic:
by
  refine ⟨fun ⟨p, hp⟩ ↦ radius_nonneg_of_mem hp, fun h ↦ ?_⟩
  obtain ⟨v, hv⟩ := (NormedSpace.sphere_nonempty (x := (0 : V)) (r := s.radius)).2 h
  refine ⟨v +ᵥ s.center, ?_⟩
  simpa [mem_sphere] using hv

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

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

Tactic:
ext

Goal state after:
case center
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ (Sphere.ofDiameter p₁ p₂).center = s.center

case radius
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ (Sphere.ofDiameter p₁ p₂).radius = s.radius
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + ↑π
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₄)

Tactic:
oangle_pointReflection_right 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)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + ↑π
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + ↑π
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + ↑π
hs : line[ℝ, p₁, p₂].SOppSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₄)

Tactic:
oangle_pointReflection_right 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)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + ↑π
hs : line[ℝ, p₁, p₂].SOppSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + ↑π
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

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

Tactic:
· suffices {p₁} = ![p₁, p₂, p₃] '' {0} by grind
        simp

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hp : dist p s.center = s.radius
p' : P
⊢ p' ∈ s ∧ p' ∈ s.orthRadius p ↔ p' = p

Tactic:
constructor

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
s : Sphere P
p : P
hp : dist p s.center = s.radius
p' : P
⊢ p' ∈ s ∧ p' ∈ s.orthRadius p → p' = p

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 : dist p s.center = s.radius
p' : P
⊢ p' = p → p' ∈ s ∧ p' ∈ s.orthRadius p
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 q : P
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q} ↔ q = p ∧ dist p s.center = s.radius

Tactic:
constructor

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
s : Sphere P
p q : P
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q} → q = p ∧ dist p s.center = s.radius

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 q : P
⊢ q = p ∧ dist p s.center = s.radius → Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q}
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case inr.refine_1
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₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
h : s.center ∈ line[ℝ, p₁, p₂]
⊢ Collinear ℝ {s.center, p₁, p₂}

Tactic:
exact collinear_insert_of_mem_affineSpan_pair h

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points),
        p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) ∧
          ∠ p p' ↑((s.faceOpposite i₁).orthogonalProjectionSpan p) =
            ∠ p p' ↑((s.faceOpposite i₂).orthogonalProjectionSpan p)
⊢ ∃ r, ∀ (i : Fin (n + 1)), dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p) = r

Tactic:
refine ⟨dist p ((s.faceOpposite i₁).orthogonalProjectionSpan 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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points),
        p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) ∧
          ∠ p p' ↑((s.faceOpposite i₁).orthogonalProjectionSpan p) =
            ∠ p p' ↑((s.faceOpposite i₂).orthogonalProjectionSpan p)
⊢ ∀ (i : Fin (n + 1)),
    dist p ↑((s.faceOpposite i).orthogonalProjectionSpan p) = dist p ↑((s.faceOpposite i₁).orthogonalProjectionSpan p)
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
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
h : s₁.radius = s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
⊢ s₁ = s₂

Tactic:
ext

Goal state after:
case center
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 : s₁.radius = s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
⊢ s₁.center = s₂.center

case radius
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 : s₁.radius = s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
⊢ s₁.radius = s₂.radius
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case h
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)
⊢ ({ center := cc₂, radius := cr₂ }.center ∈ affineSpan ℝ (insert p ↑s) ∧
      insert p ps ⊆ Metric.sphere { center := cc₂, radius := cr₂ }.center { center := cc₂, radius := cr₂ }.radius) ∧
    ∀ (y : Sphere P),
      y.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere y.center y.radius →
        y = { center := cc₂, radius := cr₂ }

Tactic:
constructor

Goal state after:
case h.left
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 : ℝ := ⋯
y : ℝ := ⋯
hy0 : y ≠ 0
ycc₂ : ℝ := ⋯
cc₂ : P := ⋯
cr₂ : ℝ := ⋯
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
⊢ { center := cc₂, radius := cr₂ }.center ∈ affineSpan ℝ (insert p ↑s) ∧
    insert p ps ⊆ Metric.sphere { center := cc₂, radius := cr₂ }.center { center := cc₂, radius := cr₂ }.radius

case h.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 : ℝ := ⋯
y : ℝ := ⋯
hy0 : y ≠ 0
ycc₂ : ℝ := ⋯
cc₂ : P := ⋯
cr₂ : ℝ := ⋯
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
⊢ ∀ (y : Sphere P),
    y.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere y.center y.radius →
      y = { center := cc₂, radius := cr₂ }
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case h.left
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 : ℝ := ⋯
y : ℝ := ⋯
hy0 : y ≠ 0
ycc₂ : ℝ := ⋯
cc₂ : P := ⋯
cr₂ : ℝ := ⋯
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
⊢ { center := cc₂, radius := cr₂ }.center ∈ affineSpan ℝ (insert p ↑s) ∧
    insert p ps ⊆ Metric.sphere { center := cc₂, radius := cr₂ }.center { center := cc₂, radius := cr₂ }.radius

Tactic:
constructor

Goal state after:
case h.left.left
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 : ℝ := ⋯
y : ℝ := ⋯
hy0 : y ≠ 0
ycc₂ : ℝ := ⋯
cc₂ : P := ⋯
cr₂ : ℝ := ⋯
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
⊢ { center := cc₂, radius := cr₂ }.center ∈ affineSpan ℝ (insert p ↑s)

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 : ℝ := ⋯
y : ℝ := ⋯
hy0 : y ≠ 0
ycc₂ : ℝ := ⋯
cc₂ : P := ⋯
cr₂ : ℝ := ⋯
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
⊢ insert p ps ⊆ Metric.sphere { center := cc₂, radius := cr₂ }.center { center := cc₂, radius := cr₂ }.radius
Module: Mathlib.Geometry.Euclidean.Angle.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
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 {i₂}) = ∡ (excenter t {i₂}) (t.points i₁) (t.points i₃)
hs : excenter t signs = excenter t {i₂}
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}

Tactic:
t.oangle_excenter_singleton_eq_add_pi h₁₂.symm h₂₃ h₁₃

Goal state after:
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
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 : ∡ (excenter t {i₂}) (t.points i₁) (t.points i₃) + ↑π = ∡ (excenter t {i₂}) (t.points i₁) (t.points i₃)
hs : excenter t signs = excenter t {i₂}
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {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
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₂
⊢ (s.map f.toAffineMap ⋯).excenterWeightsUnnorm = s.excenterWeightsUnnorm

Tactic:
ext

Goal state after:
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))
x✝ : Fin (n + 1)
⊢ (s.map f.toAffineMap ⋯).excenterWeightsUnnorm x✝¹ x✝ = s.excenterWeightsUnnorm x✝¹ 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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ (s.restrict S hS).excenterWeightsUnnorm = s.excenterWeightsUnnorm

Tactic:
ext

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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
x✝¹ : Finset (Fin (n + 1))
x✝ : Fin (n + 1)
⊢ (s.restrict S hS).excenterWeightsUnnorm x✝¹ x✝ = s.excenterWeightsUnnorm x✝¹ 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₂
⊢ (s.map f.toAffineMap ⋯).ExcenterExists = s.ExcenterExists

Tactic:
ext

Goal state after:
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 ⋯).ExcenterExists x✝ ↔ s.ExcenterExists 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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ (s.restrict S hS).ExcenterExists = s.ExcenterExists

Tactic:
ext

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