awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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)
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.excenter signs) (s.points i) ↔
    s.excenterWeights signs i < 0
have rw : AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs))
    (s.points i) ↔
  s.excenterWeights signs i < 0
Tactic: rw [excenter_eq_affineCombination,
    s.sOppSide_affineSpan_faceOpposite_point_right_iff h.sum_excenterWeights_eq_one]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 :
  AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points))
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs))
      (s.points i) ↔
    s.excenterWeights signs i < 0
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.excenter signs) (s.points i) ↔
    s.excenterWeights signs i < 0
have rw₁ : s.excenterWeights signs i < 0 ↔ s.excenterWeights signs i < 0
Tactic: rw [excenter_eq_affineCombination,
    s.sOppSide_affineSpan_faceOpposite_point_right_iff h.sum_excenterWeights_eq_one]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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)
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) (s.excenter signs) ↔
    s.excenterWeights signs i < 0
have rw : AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i)
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs)) ↔
  s.excenterWeights signs i < 0
Tactic: rw [excenter_eq_affineCombination,
    s.sOppSide_affineSpan_faceOpposite_point_left_iff h.sum_excenterWeights_eq_one]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 :
  AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i)
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs)) ↔
    s.excenterWeights signs i < 0
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) (s.excenter signs) ↔
    s.excenterWeights signs i < 0
have rw₁ : s.excenterWeights signs i < 0 ↔ s.excenterWeights signs i < 0
Tactic: rw [excenter_eq_affineCombination,
    s.sOppSide_affineSpan_faceOpposite_point_left_iff h.sum_excenterWeights_eq_one]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 : n.AtLeastTwo
i : Fin (n + 1)
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.excenter {i}) (s.points i)
have rw : s.excenterWeights {i} i < 0
Tactic: rw [(s.excenterExists_singleton i).sOppSide_excenter_point_iff, ← sign_eq_neg_one_iff,
    s.sign_excenterWeights_singleton_neg i]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 : n.AtLeastTwo
i : Fin (n + 1)
rw : s.excenterWeights {i} i < 0
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.excenter {i}) (s.points i)
have rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} i) : SignType) (-1 : SignType)
Tactic: rw [(s.excenterExists_singleton i).sOppSide_excenter_point_iff, ← sign_eq_neg_one_iff,
    s.sign_excenterWeights_singleton_neg i]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 : n.AtLeastTwo
i : Fin (n + 1)
rw : s.excenterWeights {i} i < 0
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} i) : SignType) (-1 : SignType)
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.excenter {i}) (s.points i)
have rw₂ : Eq (α := SignType) (-1) (-1)
Tactic: rw [(s.excenterExists_singleton i).sOppSide_excenter_point_iff, ← sign_eq_neg_one_iff,
    s.sign_excenterWeights_singleton_neg i]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 : n.AtLeastTwo
i : Fin (n + 1)
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) (s.excenter {i})
have rw : s.excenterWeights {i} i < 0
Tactic: rw [(s.excenterExists_singleton i).sOppSide_point_excenter_iff, ← sign_eq_neg_one_iff,
    s.sign_excenterWeights_singleton_neg i]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 : n.AtLeastTwo
i : Fin (n + 1)
rw : s.excenterWeights {i} i < 0
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) (s.excenter {i})
have rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} i) : SignType) (-1 : SignType)
Tactic: rw [(s.excenterExists_singleton i).sOppSide_point_excenter_iff, ← sign_eq_neg_one_iff,
    s.sign_excenterWeights_singleton_neg i]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 : n.AtLeastTwo
i : Fin (n + 1)
rw : s.excenterWeights {i} i < 0
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} i) : SignType) (-1 : SignType)
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) (s.excenter {i})
have rw₂ : Eq (α := SignType) (-1) (-1)
Tactic: rw [(s.excenterExists_singleton i).sOppSide_point_excenter_iff, ← sign_eq_neg_one_iff,
    s.sign_excenterWeights_singleton_neg i]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.excenter {j}) (s.points i)
have rw : 0 < s.excenterWeights {j} i
Tactic: rw [(s.excenterExists_singleton j).sSameSide_excenter_point_iff, ← sign_eq_one_iff,
    s.sign_excenterWeights_singleton_pos h.symm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
rw : 0 < s.excenterWeights {j} i
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.excenter {j}) (s.points i)
have rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {j} i) : SignType) (1 : SignType)
Tactic: rw [(s.excenterExists_singleton j).sSameSide_excenter_point_iff, ← sign_eq_one_iff,
    s.sign_excenterWeights_singleton_pos h.symm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
rw : 0 < s.excenterWeights {j} i
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {j} i) : SignType) (1 : SignType)
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.excenter {j}) (s.points i)
have rw₂ : Eq (α := SignType) 1 1
Tactic: rw [(s.excenterExists_singleton j).sSameSide_excenter_point_iff, ← sign_eq_one_iff,
    s.sign_excenterWeights_singleton_pos h.symm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) (s.excenter {j})
have rw : 0 < s.excenterWeights {j} i
Tactic: rw [(s.excenterExists_singleton j).sSameSide_point_excenter_iff, ← sign_eq_one_iff,
    s.sign_excenterWeights_singleton_pos h.symm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
rw : 0 < s.excenterWeights {j} i
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) (s.excenter {j})
have rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {j} i) : SignType) (1 : SignType)
Tactic: rw [(s.excenterExists_singleton j).sSameSide_point_excenter_iff, ← sign_eq_one_iff,
    s.sign_excenterWeights_singleton_pos h.symm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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 : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
rw : 0 < s.excenterWeights {j} i
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {j} i) : SignType) (1 : SignType)
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) (s.excenter {j})
have rw₂ : Eq (α := SignType) 1 1
Tactic: rw [(s.excenterExists_singleton j).sSameSide_point_excenter_iff, ← sign_eq_one_iff,
    s.sign_excenterWeights_singleton_pos h.symm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ (↑((s.restrict S hS).touchpoint signs i) : P) = s.touchpoint signs i
have rw : ∀ (h : ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) signs) (i : Fin (n + 1)),
  (↑((s.restrict S hS).touchpoint signs i) : P) = s.touchpoint signs i
Tactic: rw [← s.excenterExists_restrict S hS] at h
Cleared hypotheses: h, i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
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))
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) signs
i : Fin (n + 1)
⊢ (↑((s.restrict S hS).touchpoint signs i) : P) = s.touchpoint signs i
have this : Nonempty.{u_2 + 1} ↥S
Tactic: haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.touchpoint signs i)
have refine : Set.range (s.faceOpposite i).points ⊆ Set.range s.points
Tactic: refine SetLike.le_def.1 (affineSpan_mono _ ?_) (s.touchpoint_mem_affineSpan signs i)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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.signedInfDist i : (a : P) → ℝ) (s.excenter signs) =
    HMul.hMul (α := ℝ) (if i ∈ signs then -1 else 1)
        (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ) *
      s.exradius signs
have rw : HMul.hMul (α := ℝ) (if i ∈ signs then -1 else 1) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)⁻¹ =
  (if i ∈ signs then -1 else 1) *
    HMul.hMul (α := ℝ)
      (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹|
Tactic: rw [h.signedInfDist_excenter_eq_mul_sum_inv, mul_assoc, exradius_eq_abs_inv_sum]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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)
⊢ HMul.hMul (α := ℝ) (if i ∈ signs then -1 else 1) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)⁻¹ =
    (if i ∈ signs then -1 else 1) *
      HMul.hMul (α := ℝ)
        (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
        |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹|
have e_a : (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)⁻¹ =
  HMul.hMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
    |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹|
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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)
⊢ (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)⁻¹ =
    HMul.hMul (α := ℝ)
      (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹|
have e_a : (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) *
    HMul.hMul (α := ℝ)
      (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
  1
Tactic: rw [← mul_eq_one_iff_inv_eq₀ h, ← mul_assoc, self_mul_sign, ← abs_mul, mul_inv_cancel₀ h, abs_one]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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)
e_a :
  (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) *
      HMul.hMul (α := ℝ)
        (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
        |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
⊢ (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)⁻¹ =
    HMul.hMul (α := ℝ)
      (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹|
have e_a₁ : HMul.hMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)
      (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ) *
    |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
  1
Tactic: rw [← mul_eq_one_iff_inv_eq₀ h, ← mul_assoc, self_mul_sign, ← abs_mul, mul_inv_cancel₀ h, abs_one]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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)
e_a :
  (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) *
      HMul.hMul (α := ℝ)
        (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
        |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
e_a₁ :
  HMul.hMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)
        (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ) *
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
⊢ (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)⁻¹ =
    HMul.hMul (α := ℝ)
      (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹|
have e_a₂ : HMul.hMul (α := ℝ) |∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i|
    |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
  1
Tactic: rw [← mul_eq_one_iff_inv_eq₀ h, ← mul_assoc, self_mul_sign, ← abs_mul, mul_inv_cancel₀ h, abs_one]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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)
e_a :
  (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) *
      HMul.hMul (α := ℝ)
        (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
        |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
e_a₁ :
  HMul.hMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)
        (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ) *
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
e_a₂ :
  HMul.hMul (α := ℝ) |∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i|
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
⊢ (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)⁻¹ =
    HMul.hMul (α := ℝ)
      (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹|
have e_a₃ : |HMul.hMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)
      (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
  1
Tactic: rw [← mul_eq_one_iff_inv_eq₀ h, ← mul_assoc, self_mul_sign, ← abs_mul, mul_inv_cancel₀ h, abs_one]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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)
e_a :
  (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) *
      HMul.hMul (α := ℝ)
        (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
        |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
e_a₁ :
  HMul.hMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)
        (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ) *
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
e_a₂ :
  HMul.hMul (α := ℝ) |∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i|
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
e_a₃ :
  |HMul.hMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)
        (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
⊢ (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)⁻¹ =
    HMul.hMul (α := ℝ)
      (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹|
have e_a₄ : Eq (α := ℝ) |1| 1
Tactic: rw [← mul_eq_one_iff_inv_eq₀ h, ← mul_assoc, self_mul_sign, ← abs_mul, mul_inv_cancel₀ h, abs_one]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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)
e_a :
  (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) *
      HMul.hMul (α := ℝ)
        (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
        |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
e_a₁ :
  HMul.hMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)
        (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ) *
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
e_a₂ :
  HMul.hMul (α := ℝ) |∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i|
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
e_a₃ :
  |HMul.hMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)
        (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| =
    1
e_a₄ : Eq (α := ℝ) |1| 1
⊢ (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)⁻¹ =
    HMul.hMul (α := ℝ)
      (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)
      |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹|
have e_a₅ : Eq (α := ℝ) 1 1
Tactic: rw [← mul_eq_one_iff_inv_eq₀ h, ← mul_assoc, self_mul_sign, ← abs_mul, mul_inv_cancel₀ h, abs_one]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
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.signedInfDist i : (a : P) → ℝ) s.incenter = s.inradius
have rw : HMul.hMul (α := ℝ) (if Membership.mem (γ := Finset (Fin (n + 1))) ∅ i then -1 else 1)
      (↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm ∅ j)) : ℝ) *
    s.exradius ∅ =
  s.inradius
Tactic: rw [incenter, exsphere_center, s.excenterExists_empty.signedInfDist_excenter]