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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : ∀ (x : Finset (Fin (n + 1))), exradius.{u_1, u_2} (P := ↥S) (s.restrict S hS) x = s.exradius x
⊢ exradius.{u_1, u_2} (P := ↥S) (s.restrict S hS) = 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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
x : Finset (Fin (n + 1))
⊢ exradius.{u_1, u_2} (P := ↥S) (s.restrict S hS) x = s.exradius x

Tactic:
simp [exradius, exsphere]

Premises used: Affine.Simplex.exradius, 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
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 ∅)).radius = (s.exsphere ∅).radius
⊢ (s.reindex e).inradius = s.inradius

Tactic:
simp_rw [inradius, exsphere_reindex]

Premises used: Affine.Simplex.inradius, 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 ∅)).radius = (s.exsphere ∅).radius

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 ⋯).inradius = s.inradius

Tactic:
congr_fun (s.exradius_map f) _

Premises used: Affine.Simplex.exradius_map, Affine.Simplex.inradius, congr_fun
-- 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
⊢ inradius.{u_1, u_2} (P := ↥S) (n := n) (s.restrict S hS) = s.inradius

Tactic:
congr_fun (s.exradius_restrict S hS) _

Premises used: Affine.Simplex.inradius, Affine.Simplex.exradius_restrict, congr_fun
-- 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.exsphere signs).center = s.excenter signs

Tactic:
rfl

Premises used: Affine.Simplex.excenter, 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))
⊢ (s.exsphere signs).radius = s.exradius signs

Tactic:
rfl

Premises used: Affine.Simplex.exradius, 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
⊢ s.insphere.center = s.incenter

Tactic:
rfl

Premises used: Affine.Simplex.incenter, 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
⊢ s.insphere.radius = s.inradius

Tactic:
rfl

Premises used: Affine.Simplex.inradius, 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
⊢ s.exsphere ∅ = s.insphere

Tactic:
rfl

Premises used: Affine.Simplex.insphere, 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
⊢ s.excenter ∅ = s.incenter

Tactic:
rfl

Premises used: Affine.Simplex.incenter, 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
⊢ s.exradius ∅ = s.inradius

Tactic:
rfl

Premises used: Affine.Simplex.inradius, 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))
⊢ s.exsphere signsᶜ = s.exsphere signs

Tactic:
simp [exsphere, excenterWeights_compl, excenterWeightsUnnorm_compl, Pi.neg_apply]

Premises used: Affine.Simplex.exsphere, Pi.neg_apply, Affine.Simplex.excenterWeightsUnnorm_compl, Affine.Simplex.excenterWeights_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
rw : s.exsphere ∅ᶜ = s.insphere
rw₁ : s.exsphere ∅ = s.insphere
rw₂ rw₃ : s.exsphere ∅ = s.exsphere ∅
⊢ s.exsphere Finset.univ = s.insphere

Tactic:
rw [← Finset.compl_empty, exsphere_compl, insphere]

Premises used: Affine.Simplex.exsphere_compl, Finset.compl_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
rw : (s.exsphere Finset.univ).center = s.incenter
rw₁ : s.insphere.center = s.incenter
rw₂ rw₃ : s.incenter = s.incenter
⊢ s.excenter Finset.univ = s.incenter

Tactic:
rw [excenter, exsphere_univ, insphere_center]

Premises used: Affine.Simplex.excenter, Affine.Simplex.exsphere_univ, Affine.Simplex.insphere_center
-- 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
rw : (s.exsphere Finset.univ).radius = s.inradius
rw₁ : s.insphere.radius = s.inradius
rw₂ rw₃ : s.inradius = s.inradius
⊢ s.exradius Finset.univ = s.inradius

Tactic:
rw [exradius, exsphere_univ, insphere_radius]

Premises used: Affine.Simplex.insphere_radius, Affine.Simplex.exsphere_univ, Affine.Simplex.exradius
-- 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.excenter signs =
    (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs)

Tactic:
rfl

Premises used: Affine.Simplex.excenter, 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))
⊢ s.exradius signs = |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹|

Tactic:
rfl

Premises used: abs, Affine.Simplex.exradius, 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
⊢ s.incenter = (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights ∅)

Tactic:
rfl

Premises used: Affine.Simplex.incenter, 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
⊢ s.inradius = |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm ∅ i)⁻¹|

Tactic:
rfl

Premises used: abs, Affine.Simplex.inradius, 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))
⊢ 0 ≤ s.exradius signs

Tactic:
abs_nonneg _

Premises used: abs, Affine.Simplex.exradius, abs_nonneg
-- 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
⊢ 0 < s.exradius signs

Tactic:
abs_pos.2 (inv_ne_zero h)

Premises used: Iff.mpr, abs, abs_pos, Affine.Simplex.exradius, inv_ne_zero
-- 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
⊢ 0 < s.inradius

Tactic:
s.excenterExists_empty.exradius_pos

Premises used: Affine.Simplex.inradius, Affine.Simplex.excenterExists_empty, 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
⊢ 0 < s.exradius {i}

Tactic:
(s.excenterExists_singleton i).exradius_pos

Premises used: Affine.Simplex.excenterExists_singleton, 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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.excenter signs)

Tactic:
affineCombination_mem_affineSpan h.sum_excenterWeights_eq_one _

Premises used: Affine.Simplex.excenter, Set.Mem, affineCombination_mem_affineSpan, Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one
-- 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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.incenter

Tactic:
s.excenterExists_empty.excenter_mem_affineSpan_range

Premises used: Set.Mem, Affine.Simplex.incenter, Affine.Simplex.ExcenterExists.excenter_mem_affineSpan_range, 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
⊢ Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights ∅ i) 1

Tactic:
have h := s.excenterExists_empty.sum_excenterWeights_eq_one
-- 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
h : Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights ∅ i) 1
rw : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (s.excenterWeights ∅ i)
⊢ s.incenter ∈ s.interior

Tactic:
rw [incenter_eq_affineCombination, s.affineCombination_mem_interior_iff h]

Premises used: Affine.Simplex.affineCombination_mem_interior_iff, Affine.Simplex.incenter_eq_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
h : Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights ∅ i) 1
i : Fin (n + 1)
⊢ Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (s.excenterWeights ∅ i)

Tactic:
⟨s.excenterWeights_empty_pos i, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Affine.Simplex.excenterWeights_empty_pos, Set.Ioo
-- 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
h : Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights ∅ i) 1
i : Fin (n + 1)
refine : s.excenterWeights ∅ i < 1
⊢ Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (s.excenterWeights ∅ i)

Tactic:
refine ⟨s.excenterWeights_empty_pos 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
h : Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights ∅ i) 1
i : Fin (n + 1)
by_contra! : ∀ (hp : 1 ≤ s.excenterWeights ∅ i), False
⊢ s.excenterWeights ∅ i < 1

Tactic:
by_contra! hp
-- 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
h : Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights ∅ i) 1
i : Fin (n + 1)
hp : 1 ≤ s.excenterWeights ∅ i
obtain : ∀ (j : Fin (n + 1)) (hj : j ≠ i), False
⊢ False

Tactic:
obtain ⟨j, hj⟩ := exists_ne i

Premises used: exists_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
h : Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights ∅ i) 1
i : Fin (n + 1)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
hj : j ≠ i
⊢ s.excenterWeights ∅ j + s.excenterWeights ∅ i + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i = 1

Tactic:
rw [← Finset.sum_add_sum_compl {j, i}, Finset.sum_pair hj] at h

Premises used: Finset.sum_pair, Insert.insert, Singleton.singleton, 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
h : Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights ∅ i) 1
i : Fin (n + 1)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
hj : j ≠ i
h₁ : s.excenterWeights ∅ j + s.excenterWeights ∅ i + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i = 1
⊢ j ≠ i

Tactic:
rw [← Finset.sum_add_sum_compl {j, i}, Finset.sum_pair hj] at h

Premises used: Finset.sum_pair, Insert.insert, Singleton.singleton, 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
i : Fin (n + 1)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
h : s.excenterWeights ∅ j + s.excenterWeights ∅ i + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i = 1
hj : j ≠ i
revert : ∀ (h : s.excenterWeights ∅ j + s.excenterWeights ∅ i + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i = 1), False
⊢ False

Tactic:
revert 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)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
hj : j ≠ i
h : 1 < s.excenterWeights ∅ j + s.excenterWeights ∅ i + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i
⊢ ∀ (h : s.excenterWeights ∅ j + s.excenterWeights ∅ i + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i = 1), False

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- 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)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
hj : j ≠ i
h : 1 < s.excenterWeights ∅ i + s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i
⊢ 1 < s.excenterWeights ∅ j + s.excenterWeights ∅ i + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i

Tactic:
nth_rw 2 [add_comm]

Premises used: add_comm
-- 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)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
hj : j ≠ i
h : s.excenterWeights ∅ i < s.excenterWeights ∅ i + s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i
⊢ 1 < s.excenterWeights ∅ i + s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i

Tactic:
grw [hp]
-- 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)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
hj : j ≠ i
h : 0 < s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i
⊢ s.excenterWeights ∅ i < s.excenterWeights ∅ i + s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i

Tactic:
rw [add_assoc, lt_add_iff_pos_right]

Premises used: lt_add_iff_pos_right, add_assoc
-- 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)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
hj : j ≠ i
⊢ 0 < s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i

Tactic:
add_pos_of_pos_of_nonneg (s.excenterWeights_empty_pos j)
    (Finset.sum_nonneg fun k _ ↦ (s.excenterWeights_empty_pos k).le)

Premises used: LT.lt.le, Finset.sum_nonneg, Affine.Simplex.excenterWeights_empty_pos, add_pos_of_pos_of_nonneg
-- 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)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
hj : j ≠ i
⊢ 0 < s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i

Tactic:
exact add_pos_of_pos_of_nonneg (s.excenterWeights_empty_pos j)
    (Finset.sum_nonneg fun k _ ↦ (s.excenterWeights_empty_pos k).le)

Premises used: LT.lt.le, Finset.sum_nonneg, Affine.Simplex.excenterWeights_empty_pos, add_pos_of_pos_of_nonneg
-- 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)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.excenter {i})

Tactic:
(s.excenterExists_singleton i).excenter_mem_affineSpan_range

Premises used: Affine.Simplex.ExcenterExists.excenter_mem_affineSpan_range, Affine.Simplex.excenterExists_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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
simp_rw :
  HSMul.hSMul (α := ℝ) (∑ x : Fin (n + 1), (if x ∈ signs then -1 else 1) * (s.height x)⁻¹)⁻¹
        ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹) *
      dist (s.points i)
        (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
              (s.points i)) :
          P) =
    HMul.hMul (α := ℝ) (if i ∈ signs then -1 else 1)
      (∑ x : Fin (n + 1), (if x ∈ signs then -1 else 1) * (s.height x)⁻¹)⁻¹
⊢ (s.signedInfDist i : (a : P) → ℝ) (s.excenter signs) =
    HMul.hMul (α := ℝ) (if i ∈ signs then -1 else 1) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)⁻¹

Tactic:
simp_rw [excenter_eq_affineCombination,
    signedInfDist_affineCombination _ _ h.sum_excenterWeights_eq_one, excenterWeights,
    Pi.smul_apply, ← dist_eq_norm_vsub, excenterWeightsUnnorm]

Premises used: Affine.Simplex.excenter_eq_affineCombination, Affine.Simplex.excenterWeightsUnnorm, Affine.Simplex.excenterWeights, Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one, dist_eq_norm_vsub, Affine.Simplex.signedInfDist_affineCombination, 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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  HSMul.hSMul (α := ℝ) (∑ x : Fin (n + 1), (if x ∈ signs then -1 else 1) * (s.height x)⁻¹)⁻¹
        ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹) *
      s.height i =
    HMul.hMul (α := ℝ) (if i ∈ signs then -1 else 1)
      (∑ x : Fin (n + 1), (if x ∈ signs then -1 else 1) * (s.height x)⁻¹)⁻¹
⊢ HSMul.hSMul (α := ℝ) (∑ x : Fin (n + 1), (if x ∈ signs then -1 else 1) * (s.height x)⁻¹)⁻¹
        ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹) *
      dist (s.points i)
        (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
              (s.points i)) :
          P) =
    HMul.hMul (α := ℝ) (if i ∈ signs then -1 else 1)
      (∑ x : Fin (n + 1), (if x ∈ signs then -1 else 1) * (s.height x)⁻¹)⁻¹

Tactic:
rw [← altitudeFoot, ← height]

Premises used: Affine.Simplex.height, Affine.Simplex.altitudeFoot
-- 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)
⊢ HSMul.hSMul (α := ℝ) (∑ x : Fin (n + 1), (if x ∈ signs then -1 else 1) * (s.height x)⁻¹)⁻¹
        ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹) *
      s.height i =
    HMul.hMul (α := ℝ) (if i ∈ signs then -1 else 1)
      (∑ x : Fin (n + 1), (if x ∈ signs then -1 else 1) * (s.height x)⁻¹)⁻¹

Tactic:
simp [(s.height_pos i).ne']

Premises used: Affine.Simplex.height_pos, LT.lt.ne'