awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
inl :
  ∀ (h' : LT.lt (α := ℝ) 0 (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)),
    |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
        s.exradius signs =
      s.exradius signs
inr :
  ∀ (h' : Eq (α := ℝ) 0 (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)),
    |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
        s.exradius signs =
      s.exradius signs
inr₁ :
  ∀ (h' : LT.lt (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0),
    |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
        s.exradius signs =
      s.exradius signs
⊢ |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
      s.exradius signs =
    s.exradius signs

Tactic:
rcases lt_trichotomy 0 (∑ i, s.excenterWeightsUnnorm signs i) with h' | h' | h'

Premises used: Finset.univ, Affine.Simplex.excenterWeightsUnnorm, OfNat.ofNat, Finset.sum, lt_trichotomy
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
h' : LT.lt (α := ℝ) 0 (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)
⊢ |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
      s.exradius signs =
    s.exradius signs

Tactic:
simp [h']
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
h' : Eq (α := ℝ) 0 (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)
⊢ |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
      s.exradius signs =
    s.exradius signs

Tactic:
simp [h h'.symm]

Premises used: Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
h' : LT.lt (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0
⊢ |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
      s.exradius signs =
    s.exradius signs

Tactic:
simp [h']
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ dist s.incenter (s.touchpoint ∅ i) = s.inradius

Tactic:
s.excenterExists_empty.dist_excenter _

Premises used: Affine.Simplex.ExcenterExists.dist_excenter, Affine.Simplex.incenter, Affine.Simplex.inradius, Affine.Simplex.excenterExists_empty
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i₁ i₂ : Fin (n + 1)
⊢ dist (s.excenter signs) (s.touchpoint signs i₁) = dist (s.excenter signs) (s.touchpoint signs i₂)

Tactic:
simp_rw [h.dist_excenter]

Premises used: Affine.Simplex.ExcenterExists.dist_excenter
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
⊢ dist s.incenter (s.touchpoint ∅ i₁) = dist s.incenter (s.touchpoint ∅ i₂)

Tactic:
s.excenterExists_empty.dist_excenter_eq_dist_excenter _ _

Premises used: Affine.Simplex.incenter, Affine.Simplex.ExcenterExists.dist_excenter_eq_dist_excenter, Affine.Simplex.excenterExists_empty
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ s.touchpoint signs i ∈ s.exsphere signs

Tactic:
mem_sphere'.2 (h.dist_excenter i)

Premises used: Iff.mpr, Affine.Simplex.ExcenterExists.dist_excenter, EuclideanGeometry.mem_sphere'
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ s.touchpoint ∅ i ∈ s.insphere

Tactic:
s.excenterExists_empty.touchpoint_mem_exsphere _

Premises used: Set.Mem, Affine.Simplex.ExcenterExists.touchpoint_mem_exsphere, Affine.Simplex.excenterExists_empty
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  (s.exsphere signs).IsTangentAt
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₁ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₂ :
  (s.exsphere signs).IsTangentAt
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
    (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw₃ :
  dist (s.exsphere signs).center
      (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.exsphere signs).center) :
        P) =
    (s.exsphere signs).radius
rw₄ :
  dist (s.exsphere signs).center
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.exsphere signs).center) :
        P) =
    (s.exsphere signs).radius
rw₅ :
  dist (s.excenter signs)
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.excenter signs)) :
        P) =
    (s.exsphere signs).radius
rw₆ :
  dist (s.excenter signs)
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.excenter signs)) :
        P) =
    s.exradius signs
rw₇ : dist (s.excenter signs) (s.touchpoint signs i) = s.exradius signs
rw₈ rw₉ : s.exradius signs = s.exradius signs
⊢ (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))

Tactic:
rw [touchpoint, orthogonalProjectionSpan, excenter,
    ← EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt,
    ← orthogonalProjectionSpan, ← excenter, ← exradius, ← touchpoint, h.dist_excenter]

Premises used: Affine.Simplex.excenter, Affine.Simplex.orthogonalProjectionSpan, Affine.Simplex.ExcenterExists.dist_excenter, Affine.Simplex.touchpoint, Affine.Simplex.exradius, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ s.insphere.IsTangentAt (s.touchpoint ∅ i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))

Tactic:
s.excenterExists_empty.isTangentAt_touchpoint i

Premises used: Affine.Simplex.ExcenterExists.isTangentAt_touchpoint, Affine.Simplex.excenterExists_empty, Affine.Simplex.insphere
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
p : P
ht : (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points))
rw :
  (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P) =
    s.touchpoint signs i
rw₁ :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
rw₂ :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.excenter signs)) :
      P)
rw₃ rw₄ :
  Eq.{u_2 + 1} (α := P)
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
    (↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.exsphere signs).center) :
      P)
⊢ p = s.touchpoint signs i

Tactic:
rw [ht.eq_orthogonalProjection, touchpoint, orthogonalProjectionSpan, excenter]

Premises used: Affine.Simplex.excenter, Affine.Simplex.orthogonalProjectionSpan, Affine.Simplex.touchpoint, EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
p : P
⊢ (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points)) ↔ p = s.touchpoint signs i

Tactic:
⟨eq_touchpoint_of_isTangentAt_exsphere, ?_⟩

Premises used: Iff.intro, Affine.Simplex.eq_touchpoint_of_isTangentAt_exsphere
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
p : P
refine :
  p = s.touchpoint signs i → (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points))
⊢ (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points)) ↔ p = s.touchpoint signs i

Tactic:
refine ⟨eq_touchpoint_of_isTangentAt_exsphere, ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))

Tactic:
h.isTangentAt_touchpoint i

Premises used: Affine.Simplex.ExcenterExists.isTangentAt_touchpoint
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))

Tactic:
exact h.isTangentAt_touchpoint i

Premises used: Affine.Simplex.ExcenterExists.isTangentAt_touchpoint
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
⊢ s.insphere.IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points)) ↔ p = s.touchpoint ∅ i

Tactic:
s.excenterExists_empty.isTangentAt_exsphere_iff_eq_touchpoint

Premises used: Affine.Simplex.ExcenterExists.isTangentAt_exsphere_iff_eq_touchpoint, Affine.Simplex.excenterExists_empty, Affine.Simplex.insphere
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : 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)
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
    ((s.exsphere signs).orthRadius (s.touchpoint signs i))

Tactic:
(h.isTangentAt_touchpoint i).eq_orthRadius_of_finrank_add_one_eq (h.exradius_pos.ne') ?_

Premises used: EuclideanGeometry.Sphere.IsTangentAt.eq_orthRadius_of_finrank_add_one_eq, Affine.Simplex.ExcenterExists.isTangentAt_touchpoint, LT.lt.ne', Affine.Simplex.ExcenterExists.exradius_pos
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : 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)
refine :
  Module.finrank.{0, u_1} ℝ ↥(AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite i).points))) + 1 =
    Module.finrank ℝ V
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
    ((s.exsphere signs).orthRadius (s.touchpoint signs i))

Tactic:
refine (h.isTangentAt_touchpoint i).eq_orthRadius_of_finrank_add_one_eq (h.exradius_pos.ne') ?_

Premises used: EuclideanGeometry.Sphere.IsTangentAt.eq_orthRadius_of_finrank_add_one_eq, Affine.Simplex.ExcenterExists.isTangentAt_touchpoint, LT.lt.ne', Affine.Simplex.ExcenterExists.exradius_pos
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : 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)
rw : n - 1 + 1 = n
⊢ Module.finrank.{0, u_1} ℝ ↥(AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite i).points))) + 1 =
    Module.finrank ℝ V

Tactic:
rw [direction_affineSpan, (s.faceOpposite i).independent.finrank_vectorSpan_add_one,
    Fintype.card_fin, hf.out]

Premises used: direction_affineSpan, Fintype.card_fin, AffineIndependent.finrank_vectorSpan_add_one, Affine.Simplex.independent, Affine.Simplex.faceOpposite, Fact.out
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : 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 ≠ 0

Tactic:
have := NeZero.ne n
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : 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)
this : n ≠ 0
⊢ n - 1 + 1 = n

Tactic:
lia
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : Fact (Module.finrank ℝ V = n)
i : Fin (n + 1)
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
    (s.insphere.orthRadius (s.touchpoint ∅ i))

Tactic:
s.excenterExists_empty.affineSpan_faceOpposite_eq_orthRadius i

Premises used: Affine.Simplex.ExcenterExists.affineSpan_faceOpposite_eq_orthRadius, Affine.Simplex.excenterExists_empty, Affine.Simplex.insphere
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
signs : Finset (Fin (n + 1))
⊢ (∃ (r : ℝ), ∀ (i : Fin (n + 1)), (s.signedInfDist i : (a : P) → ℝ) p = (if i ∈ signs then -1 else 1) * r) ↔
    s.ExcenterExists signs ∧ p = s.excenter signs

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
signs : Finset (Fin (n + 1))
refine_1 :
  (∃ (r : ℝ), ∀ (i : Fin (n + 1)), (s.signedInfDist i : (a : P) → ℝ) p = (if i ∈ signs then -1 else 1) * r) →
    s.ExcenterExists signs ∧ p = s.excenter signs
refine_2 :
  s.ExcenterExists signs ∧ p = s.excenter signs →
    ∃ (r : ℝ), ∀ (i : Fin (n + 1)), (s.signedInfDist i : (a : P) → ℝ) p = (if i ∈ signs then -1 else 1) * r
⊢ (∃ (r : ℝ), ∀ (i : Fin (n + 1)), (s.signedInfDist i : (a : P) → ℝ) p = (if i ∈ signs then -1 else 1) * r) ↔
    s.ExcenterExists signs ∧ p = s.excenter signs

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
signs : Finset (Fin (n + 1))
r : ℝ
h : ∀ (i : Fin (n + 1)), (s.signedInfDist i : (a : P) → ℝ) p = (if i ∈ signs then -1 else 1) * r
refine_1 :
  ∀ (w : Fin (n + 1) → ℝ) (h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1)
    (hp :
      Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P))
    (h :
      ∀ (i : Fin (n + 1)),
        (s.signedInfDist i : (a : P) → ℝ)
            ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
          (if i ∈ signs then -1 else 1) * r),
    s.ExcenterExists signs ∧
      (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.excenter signs
⊢ s.ExcenterExists signs ∧ p = s.excenter signs

Tactic:
obtain ⟨w, h1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp

Premises used: eq_affineCombination_of_mem_affineSpan_of_fintype, rfl
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
rw :
  (s.signedInfDist i : (a : P) → ℝ)
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
    (if i ∈ signs then -1 else 1) * r
⊢ w i * ‖s.points i -ᵥ s.altitudeFoot i‖ = (if i ∈ signs then -1 else 1) * r

Tactic:
rw [altitudeFoot, ← s.signedInfDist_affineCombination i h1]

Premises used: Affine.Simplex.altitudeFoot, Affine.Simplex.signedInfDist_affineCombination
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
⊢ (s.signedInfDist i : (a : P) → ℝ)
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
    (if i ∈ signs then -1 else 1) * r

Tactic:
h i
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i : (a : P) → ℝ)
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
      (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
⊢ (s.signedInfDist i : (a : P) → ℝ)
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P) =
    (if i ∈ signs then -1 else 1) * r

Tactic:
exact h i