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

Goal state before:
pp: case inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
h : dist p s.center = s.radius
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔
    s.radius < dist p s.center ∨
      Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0

pp: case inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
h : s.radius < dist p s.center
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔
    s.radius < dist p s.center ∨
      Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0

Tactic:
·

Goal state after:
case inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
h : dist p s.center = s.radius
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔
    s.radius < dist p s.center ∨
      Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
h : s.radius < dist p s.center
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔
    s.radius < dist p s.center ∨
      Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0

Tactic:
·

Goal state after:
case inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
h : s.radius < dist p s.center
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔
    s.radius < dist p s.center ∨
      Module.finrank ℝ V = 1 ∧ dist p s.center < s.radius ∧ p ≠ s.center ∨ Subsingleton V ∧ s.radius ≠ 0
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t {i₁}))
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₃).points

pp: case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
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₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t {i₁}))
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₂).points

Tactic:
·

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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t {i₁}))
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₃).points
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
h : s₁.IsIntTangent s₂
⊢ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius

pp: case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
⊢ dist s₁.center s₂.center = s₂.radius - s₁.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius → s₁.IsIntTangent s₂

Tactic:
·

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
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
h : s₁.IsIntTangent s₂
⊢ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
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₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t {i₁}))
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₂).points

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
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₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₂).points))) (excenter t {i₁}))
⊢ t.points i₁ ∈ Set.range (faceOpposite t i₂).points
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
⊢ dist s₁.center s₂.center = s₂.radius - s₁.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius → s₁.IsIntTangent s₂

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
⊢ dist s₁.center s₂.center = s₂.radius - s₁.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius → s₁.IsIntTangent s₂
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
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
⊢ s₁.IsIntTangent s₂

pp: case neg
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
⊢ s₁.IsIntTangent s₂

Tactic:
·

Goal state after:
case pos
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
⊢ s₁.IsIntTangent s₂
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
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
⊢ s₁.IsIntTangent s₂

Tactic:
·

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
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
⊢ s₁.IsIntTangent s₂
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points))) (excenter t {i₁}))
⊢ t.points i₂ ∈ Set.range (faceOpposite t i₃).points

pp: case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
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₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points))) (excenter t {i₁}))
⊢ t.points i₂ ∈ Set.range (faceOpposite t i₁).points

Tactic:
·

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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points))) (excenter t {i₁}))
⊢ t.points i₂ ∈ Set.range (faceOpposite t i₃).points
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
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₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points))) (excenter t {i₁}))
⊢ t.points i₂ ∈ Set.range (faceOpposite t i₁).points

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
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₃
hd :
  dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₃).points))) (excenter t {i₁})) =
    dist (excenter t {i₁})
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (faceOpposite t i₁).points))) (excenter t {i₁}))
⊢ t.points i₂ ∈ Set.range (faceOpposite t i₁).points
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case neg.refine_1
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
⊢ (AffineMap.lineMap s₂.center s₁.center) (s₂.radius / (s₂.radius - s₁.radius)) ∈ s₁

pp: case neg.refine_2
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
⊢ (AffineMap.lineMap s₂.center s₁.center) (s₂.radius / (s₂.radius - s₁.radius)) ∈ s₂

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
⊢ Wbtw ℝ s₂.center s₁.center ((AffineMap.lineMap s₂.center s₁.center) (s₂.radius / (s₂.radius - s₁.radius)))

Tactic:
·

Goal state after:
case neg.refine_1
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
⊢ (AffineMap.lineMap s₂.center s₁.center) (s₂.radius / (s₂.radius - s₁.radius)) ∈ s₁
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case neg.refine_2
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
⊢ (AffineMap.lineMap s₂.center s₁.center) (s₂.radius / (s₂.radius - s₁.radius)) ∈ s₂

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
⊢ Wbtw ℝ s₂.center s₁.center ((AffineMap.lineMap s₂.center s₁.center) (s₂.radius / (s₂.radius - s₁.radius)))

Tactic:
·

Goal state after:
case neg.refine_2
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
⊢ (AffineMap.lineMap s₂.center s₁.center) (s₂.radius / (s₂.radius - s₁.radius)) ∈ s₂
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
⊢ Wbtw ℝ s₂.center s₁.center ((AffineMap.lineMap s₂.center s₁.center) (s₂.radius / (s₂.radius - s₁.radius)))

Tactic:
·

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
⊢ Wbtw ℝ s₂.center s₁.center ((AffineMap.lineMap s₂.center s₁.center) (s₂.radius / (s₂.radius - s₁.radius)))
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:
·

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
⊢ s₂.radius - s₁.radius ≤ s₂.radius
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
⊢ 0 < s₂.radius - s₁.radius

Tactic:
·

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.Sphere.OrthRadius

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
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.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p, -(√(s.radius ^ 2 - dist p s.center ^ 2) • v) +ᵥ p}

pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
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' ∈ {√(s.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p, -(√(s.radius ^ 2 - dist p s.center ^ 2) • v) +ᵥ p}
⊢ p' ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)

Tactic:
·

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
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.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p, -(√(s.radius ^ 2 - dist p s.center ^ 2) • v) +ᵥ p}
Module: Mathlib.Geometry.Euclidean.Angle.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
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₃)
hs : excenter t signs = incenter t
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}

pp: case inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
hs : excenter t signs = excenter t {i₁}
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}

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 signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
hs : excenter t signs = excenter t {i₂}
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}

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
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₃)
hs : excenter t signs = excenter t {i₃}
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}

Tactic:
·

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
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₃)
hs : excenter t signs = incenter t
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}