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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
h :
  Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
    (1 : SignType)
h₁ :
  Eq (α := SignType) (-1 : SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} i) : SignType)
⊢ HMul.hMul (α := SignType) (β := SignType)
      ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
      ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} i) : SignType) =
    -1

Tactic:
convert! one_mul _

Premises used: one_mul
-- 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 : n.AtLeastTwo
i : Fin (n + 1)
h : LT.lt (α := ℝ) 0 (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
    (1 : SignType)

Tactic:
rw [sign_eq_one_iff, inv_pos]

Premises used: inv_pos, sign_eq_one_iff
-- 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 : n.AtLeastTwo
i : Fin (n + 1)
⊢ LT.lt (α := ℝ) 0 (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)

Tactic:
s.sum_excenterWeightsUnnorm_singleton_pos i

Premises used: Affine.Simplex.sum_excenterWeightsUnnorm_singleton_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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
⊢ LT.lt (α := ℝ) 0 (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)

Tactic:
exact s.sum_excenterWeightsUnnorm_singleton_pos i

Premises used: Affine.Simplex.sum_excenterWeightsUnnorm_singleton_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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
⊢ Eq (α := SignType) (-1 : SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} i) : SignType)

Tactic:
simp [excenterWeightsUnnorm]

Premises used: Affine.Simplex.excenterWeightsUnnorm
-- 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 : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
simp_rw :
  HMul.hMul (α := SignType) (β := SignType)
      ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
      ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} j) : SignType) =
    1
⊢ Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} j) : SignType) (1 : SignType)

Tactic:
simp_rw [excenterWeights, Pi.smul_apply, smul_eq_mul, sign_mul]

Premises used: sign_mul, Affine.Simplex.excenterWeights, smul_eq_mul, Pi.smul_apply
-- 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 : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
⊢ HMul.hMul (α := SignType) (β := SignType) (1 : SignType)
      ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} j) : SignType) =
    (SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} j)

Tactic:
one_mul _

Premises used: one_mul
-- 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 : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
h₁ :
  Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
    (1 : SignType)
h₂ : Eq (α := SignType) (1 : SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} j) : SignType)
⊢ HMul.hMul (α := SignType) (β := SignType)
      ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
      ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} j) : SignType) =
    1

Tactic:
convert! one_mul _

Premises used: one_mul
-- 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 : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
h₁ : LT.lt (α := ℝ) 0 (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
    (1 : SignType)

Tactic:
rw [sign_eq_one_iff, inv_pos]

Premises used: inv_pos, sign_eq_one_iff
-- 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 : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
⊢ LT.lt (α := ℝ) 0 (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)

Tactic:
s.sum_excenterWeightsUnnorm_singleton_pos i

Premises used: Affine.Simplex.sum_excenterWeightsUnnorm_singleton_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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
⊢ LT.lt (α := ℝ) 0 (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)

Tactic:
exact s.sum_excenterWeightsUnnorm_singleton_pos i

Premises used: Affine.Simplex.sum_excenterWeightsUnnorm_singleton_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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
h : i ≠ j
⊢ Eq (α := SignType) (1 : SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} j) : SignType)

Tactic:
simp [excenterWeightsUnnorm, h.symm]

Premises used: Ne.symm, Affine.Simplex.excenterWeightsUnnorm
-- 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 : n.AtLeastTwo
i : Fin (n + 1)
⊢ s.ExcenterExists {i}

Tactic:
(s.sum_excenterWeightsUnnorm_singleton_pos i).ne'

Premises used: Affine.Simplex.ExcenterExists, Affine.Simplex.sum_excenterWeightsUnnorm_singleton_pos, LT.lt.ne'
-- 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 : n.AtLeastTwo
i : Fin (n + 1)
⊢ (s.height i)⁻¹ < ∑ j : Fin (n + 1) with j ≠ i, (s.height j)⁻¹

Tactic:
have := s.inv_height_lt_sum_inv_height 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
this : (s.height i)⁻¹ < ∑ j : Fin (n + 1) with j ≠ i, (s.height j)⁻¹
rwa :
  ∀ (this : (s.height i)⁻¹ < ∑ j ∈ erase univ i, (s.height j)⁻¹),
    (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
rwa₁ :
  ∀ (this : (s.height i)⁻¹ < ∑ j ∈ {i}ᶜ, (s.height j)⁻¹),
    (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (this : (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹),
    (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
⊢ (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹

Tactic:
rwa [filter_ne', ← compl_singleton, ← add_lt_add_iff_left (s.height i)⁻¹] at this

Premises used: Affine.Simplex.height, Finset.compl_singleton, Inv.inv, Finset.filter_ne', add_lt_add_iff_left
-- 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 : n.AtLeastTwo
i : Fin (n + 1)
⊢ (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹

Tactic:
have h : (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹ := by
    have := s.inv_height_lt_sum_inv_height i
    rwa [filter_ne', ← compl_singleton, ← add_lt_add_iff_left (s.height i)⁻¹] at this
-- 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 : n.AtLeastTwo
i : Fin (n + 1)
h : (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
rwa : (s.height i)⁻¹ + (s.height i)⁻¹ < HAdd.hAdd (α := ℝ) (∑ j ∈ {i}, (s.height j)⁻¹) (∑ j ∈ {i}ᶜ, (s.height j)⁻¹)
rwa₁ rwa₂ rwa₃ rwa₄ : (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
⊢ 2 * (s.height i)⁻¹ < HAdd.hAdd (α := ℝ) (∑ j ∈ {i}, (s.height j)⁻¹) (∑ j ∈ {i}ᶜ, (s.height j)⁻¹)

Tactic:
rwa [two_mul, sum_singleton]

Premises used: two_mul, Finset.sum_singleton
-- 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 : n.AtLeastTwo
i : Fin (n + 1)
h : (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
⊢ 2 * (s.height i)⁻¹ < HAdd.hAdd (α := ℝ) (∑ j ∈ {i}, (s.height j)⁻¹) (∑ j ∈ {i}ᶜ, (s.height j)⁻¹)

Tactic:
replace h : 2 * (s.height i)⁻¹ < ∑ j ∈ {i}, (s.height j)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹ := by
    rwa [two_mul, sum_singleton]
-- 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 : n.AtLeastTwo
i : Fin (n + 1)
h : (s.height i)⁻¹ < HMul.hMul (α := ℝ) 2⁻¹ (∑ i : Fin (n + 1), (s.height i)⁻¹)
⊢ LT.lt (α := ℝ) 0 (∑ i : Fin (n + 1), (s.height i)⁻¹)

Tactic:
positivity
-- 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 : n.AtLeastTwo
i : Fin (n + 1)
h : 2 * (s.height i)⁻¹ < HAdd.hAdd (α := ℝ) (∑ j ∈ {i}, (s.height j)⁻¹) (∑ j ∈ {i}ᶜ, (s.height j)⁻¹)
rwa :
  ∀ (h : 2 * (s.height i)⁻¹ < ∑ i : Fin (n + 1), (s.height i)⁻¹),
    (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
rwa₁ :
  ∀ (h : (s.height i)⁻¹ < HMul.hMul (α := ℝ) 2⁻¹ (∑ i : Fin (n + 1), (s.height i)⁻¹)),
    (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (h : (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹),
    (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
⊢ (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹

Tactic:
rwa [sum_add_sum_compl, ← lt_inv_mul_iff₀ zero_lt_two, ← div_lt_iff₀ (by positivity)] at h

Premises used: div_lt_iff₀, lt_inv_mul_iff₀, Finset.sum_add_sum_compl
-- 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 : n.AtLeastTwo
i : Fin (n + 1)
h : 2 * (s.height i)⁻¹ < HAdd.hAdd (α := ℝ) (∑ j ∈ {i}, (s.height j)⁻¹) (∑ j ∈ {i}ᶜ, (s.height j)⁻¹)
⊢ (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹

Tactic:
replace h : (s.height i)⁻¹ / ∑ i, (s.height i)⁻¹ < 2⁻¹ := by
    rwa [sum_add_sum_compl, ← lt_inv_mul_iff₀ zero_lt_two, ← div_lt_iff₀ (by positivity)] at 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
h : (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
⊢ (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹

Tactic:
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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
h : (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
h₁ : s.excenterWeights ∅ i = (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹
⊢ s.excenterWeights ∅ i < 2⁻¹

Tactic:
convert! 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
h : (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
⊢ s.excenterWeights ∅ i = (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹

Tactic:
simp [excenterWeights, excenterWeightsUnnorm, div_eq_inv_mul]

Premises used: Affine.Simplex.excenterWeightsUnnorm, Affine.Simplex.excenterWeights, div_eq_inv_mul
-- 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
simp_rw :
  Eq.{u_2 + 1} (α := Sphere P)
    ({
        center :=
          (Finset.affineCombination ℝ (Finset.map e.symm.toEmbedding Finset.univ) s.points : (a : Fin (n + 1) → ℝ) → P)
            (s.excenterWeights (Finset.map e.symm.toEmbedding signs)),
        radius :=
          |((Finset.map e.symm.toEmbedding Finset.univ).sum
                (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)))⁻¹| } :
      Sphere P)
    ({
        center :=
          (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
            (s.excenterWeights (Finset.map e.symm.toEmbedding signs)),
        radius := |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i)⁻¹| } :
      Sphere P)
⊢ (s.reindex e).exsphere signs = s.exsphere (Finset.map e.symm.toEmbedding signs)

Tactic:
simp_rw [exsphere, excenterWeightsUnnorm_reindex, excenterWeights_reindex, Finset.sum_comp_equiv,
    reindex, ← Equiv.coe_toEmbedding, ← Finset.affineCombination_map]

Premises used: Equiv.coe_toEmbedding, Affine.Simplex.excenterWeightsUnnorm_reindex, Affine.Simplex.excenterWeights_reindex, Affine.Simplex.reindex, Finset.affineCombination_map, Affine.Simplex.exsphere, Finset.sum_comp_equiv
-- 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
⊢ Eq.{u_2 + 1} (α := Sphere P)
    ({
        center :=
          (Finset.affineCombination ℝ (Finset.map e.symm.toEmbedding Finset.univ) s.points : (a : Fin (n + 1) → ℝ) → P)
            (s.excenterWeights (Finset.map e.symm.toEmbedding signs)),
        radius :=
          |((Finset.map e.symm.toEmbedding Finset.univ).sum
                (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)))⁻¹| } :
      Sphere P)
    ({
        center :=
          (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
            (s.excenterWeights (Finset.map e.symm.toEmbedding signs)),
        radius := |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i)⁻¹| } :
      Sphere P)

Tactic:
simp
-- 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
simp_rw : s.exsphere (Finset.map e.symm.toEmbedding ∅) = s.exsphere ∅
⊢ (s.reindex e).insphere = s.insphere

Tactic:
simp_rw [insphere, exsphere_reindex]

Premises used: Affine.Simplex.exsphere_reindex, 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ s.exsphere (Finset.map e.symm.toEmbedding ∅) = s.exsphere ∅

Tactic:
simp
-- 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).excenter signs = (f : (a : P) → P₂) (s.excenter signs)

Tactic:
simp [excenter, exsphere, ← AffineIsometry.coe_toAffineMap, h.sum_excenterWeights_eq_one,
    Finset.map_affineCombination]

Premises used: Affine.Simplex.excenter, Finset.map_affineCombination, AffineIsometry.coe_toAffineMap, Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one, Affine.Simplex.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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) signs

Tactic:
rw [← s.excenterExists_restrict S hS] at h

Premises used: Affine.Simplex.excenterExists_restrict
-- 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))
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) signs
⊢ Nonempty.{u_2 + 1} ↥S

Tactic:
haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- 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))
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) signs
this : Nonempty.{u_2 + 1} ↥S
⊢ (↑((s.restrict S hS).excenter signs) : P) = s.excenter signs

Tactic:
(h.excenter_map S.subtypeₐᵢ).symm

Premises used: Affine.Simplex.ExcenterExists.excenter_map, Affine.Simplex.map, AffineSubspace.subtypeₐᵢ, 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))
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) signs
this : Nonempty.{u_2 + 1} ↥S
⊢ (↑((s.restrict S hS).excenter signs) : P) = s.excenter signs

Tactic:
exact (h.excenter_map S.subtypeₐᵢ).symm

Premises used: Affine.Simplex.ExcenterExists.excenter_map, AffineSubspace.subtypeₐᵢ, 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
simp_rw : (s.exsphere (Finset.map e.symm.toEmbedding ∅)).center = (s.exsphere ∅).center
⊢ (s.reindex e).incenter = s.incenter

Tactic:
simp_rw [incenter, exsphere_reindex]

Premises used: Affine.Simplex.incenter, Affine.Simplex.exsphere_reindex
-- 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.exsphere (Finset.map e.symm.toEmbedding ∅)).center = (s.exsphere ∅).center

Tactic:
simp
-- 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).incenter = (f : (a : P) → P₂) s.incenter

Tactic:
s.excenterExists_empty.excenter_map f

Premises used: Affine.Simplex.ExcenterExists.excenter_map, Affine.Simplex.incenter, 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ (↑((s.restrict S hS).incenter (n := n)) : P) = s.incenter

Tactic:
s.excenterExists_empty.excenter_restrict S hS

Premises used: Affine.Simplex.incenter, Affine.Simplex.ExcenterExists.excenter_restrict, 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
h : ∀ (x : Finset (Fin (n + 1))), (s.map f.toAffineMap ⋯).exradius x = s.exradius x
⊢ (s.map f.toAffineMap ⋯).exradius = s.exradius

Tactic:
ext
-- 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
x : Finset (Fin (n + 1))
⊢ (s.map f.toAffineMap ⋯).exradius x = s.exradius x

Tactic:
simp [exradius, exsphere]

Premises used: Affine.Simplex.exradius, Affine.Simplex.exsphere