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 j : Fin (n + 1)
hij : Eq (α := Finset (Fin (n + 1))) {i} {j}ᶜ
this : 2 ≤ n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
inr :
  ∀
    (hij :
      ∀ (a : Fin (n + 1)),
        Membership.mem (γ := Finset (Fin (n + 1))) {i} a ↔ Membership.mem (γ := Finset (Fin (n + 1))) {j}ᶜ a)
    (this : 2 ≤ n) (k : Fin (n + 1)) (hki : k ≠ i) (hkj : k ≠ j), i = j
⊢ i = j

Tactic:
rw [Finset.ext_iff] at hij

Premises used: Finset.ext_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)
hij :
  ∀ (a : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) {i} a ↔ Membership.mem (γ := Finset (Fin (n + 1))) {j}ᶜ a
this : 2 ≤ n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
⊢ Membership.mem (γ := Finset (Fin (n + 1))) {i} k ↔ Membership.mem (γ := Finset (Fin (n + 1))) {j}ᶜ k

Tactic:
replace hij := hij k
-- 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)
this : 2 ≤ n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hij : Membership.mem (γ := Finset (Fin (n + 1))) {i} k ↔ Membership.mem (γ := Finset (Fin (n + 1))) {j}ᶜ k
⊢ i = j

Tactic:
simp_all
-- 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 :
  AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points))
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs))
      (s.points i) ↔
    0 < s.excenterWeights signs i
rw₁ rw₂ : 0 < s.excenterWeights signs i ↔ 0 < s.excenterWeights signs i
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.excenter signs) (s.points i) ↔
    0 < s.excenterWeights signs i

Tactic:
rw [excenter_eq_affineCombination,
    s.sSameSide_affineSpan_faceOpposite_point_right_iff h.sum_excenterWeights_eq_one]

Premises used: Affine.Simplex.excenter_eq_affineCombination, Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one, Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_right_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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i)
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs)) ↔
    0 < s.excenterWeights signs i
rw₁ rw₂ : 0 < s.excenterWeights signs i ↔ 0 < s.excenterWeights signs i
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) (s.excenter signs) ↔
    0 < s.excenterWeights signs i

Tactic:
rw [excenter_eq_affineCombination,
    s.sSameSide_affineSpan_faceOpposite_point_left_iff h.sum_excenterWeights_eq_one]

Premises used: Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_left_iff, Affine.Simplex.excenter_eq_affineCombination, 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
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
rw₁ rw₂ : s.excenterWeights signs i < 0 ↔ 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

Tactic:
rw [excenter_eq_affineCombination,
    s.sOppSide_affineSpan_faceOpposite_point_right_iff h.sum_excenterWeights_eq_one]

Premises used: Affine.Simplex.excenter_eq_affineCombination, Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one, Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_right_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
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
rw₁ rw₂ : s.excenterWeights signs i < 0 ↔ 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

Tactic:
rw [excenter_eq_affineCombination,
    s.sOppSide_affineSpan_faceOpposite_point_left_iff h.sum_excenterWeights_eq_one]

Premises used: Affine.Simplex.excenter_eq_affineCombination, Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one, Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_left_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
i : Fin (n + 1)
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) s.incenter (s.points i)

Tactic:
s.excenterExists_empty.sSameSide_excenter_point_iff.2 (s.excenterWeights_empty_pos i)

Premises used: Iff.mpr, Affine.Simplex.incenter, Affine.Simplex.excenterWeights_empty_pos, Affine.Simplex.excenterExists_empty, Affine.Simplex.ExcenterExists.sSameSide_excenter_point_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
i : Fin (n + 1)
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) s.incenter

Tactic:
s.excenterExists_empty.sSameSide_point_excenter_iff.2 (s.excenterWeights_empty_pos i)

Premises used: Iff.mpr, Affine.Simplex.incenter, Affine.Simplex.excenterWeights_empty_pos, Affine.Simplex.excenterExists_empty, Affine.Simplex.ExcenterExists.sSameSide_point_excenter_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)
rw : s.excenterWeights {i} i < 0
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} i) : SignType) (-1 : SignType)
rw₂ rw₃ : Eq (α := SignType) (-1) (-1)
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.excenter {i}) (s.points i)

Tactic:
rw [(s.excenterExists_singleton i).sOppSide_excenter_point_iff, ← sign_eq_neg_one_iff,
    s.sign_excenterWeights_singleton_neg i]

Premises used: Affine.Simplex.ExcenterExists.sOppSide_excenter_point_iff, Affine.Simplex.sign_excenterWeights_singleton_neg, Affine.Simplex.excenterExists_singleton, sign_eq_neg_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)
rw : s.excenterWeights {i} i < 0
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} i) : SignType) (-1 : SignType)
rw₂ rw₃ : Eq (α := SignType) (-1) (-1)
⊢ AffineSubspace.SOppSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) (s.excenter {i})

Tactic:
rw [(s.excenterExists_singleton i).sOppSide_point_excenter_iff, ← sign_eq_neg_one_iff,
    s.sign_excenterWeights_singleton_neg i]

Premises used: Affine.Simplex.sign_excenterWeights_singleton_neg, Affine.Simplex.ExcenterExists.sOppSide_point_excenter_iff, Affine.Simplex.excenterExists_singleton, sign_eq_neg_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
rw : 0 < s.excenterWeights {j} i
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {j} i) : SignType) (1 : SignType)
rw₂ rw₃ : Eq (α := SignType) 1 1
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.excenter {j}) (s.points i)

Tactic:
rw [(s.excenterExists_singleton j).sSameSide_excenter_point_iff, ← sign_eq_one_iff,
    s.sign_excenterWeights_singleton_pos h.symm]

Premises used: Affine.Simplex.sign_excenterWeights_singleton_pos, Ne.symm, Affine.Simplex.excenterExists_singleton, sign_eq_one_iff, Affine.Simplex.ExcenterExists.sSameSide_excenter_point_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
rw : 0 < s.excenterWeights {j} i
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {j} i) : SignType) (1 : SignType)
rw₂ rw₃ : Eq (α := SignType) 1 1
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) (s.excenter {j})

Tactic:
rw [(s.excenterExists_singleton j).sSameSide_point_excenter_iff, ← sign_eq_one_iff,
    s.sign_excenterWeights_singleton_pos h.symm]

Premises used: Affine.Simplex.sign_excenterWeights_singleton_pos, Ne.symm, Affine.Simplex.excenterExists_singleton, sign_eq_one_iff, Affine.Simplex.ExcenterExists.sSameSide_point_excenter_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
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))
i : Fin (m + 1)
⊢ (s.reindex e).touchpoint signs i =
    s.touchpoint (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)

Tactic:
orthogonalProjectionSpan_congr (s.range_faceOpposite_reindex _ _) (s.excenter_reindex _ _)

Premises used: Affine.Simplex.orthogonalProjectionSpan_congr, Affine.Simplex.range_faceOpposite_reindex, Affine.Simplex.touchpoint, Affine.Simplex.excenter_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
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₂
i : Fin (n + 1)
⊢ (s.map f.toAffineMap ⋯).touchpoint signs i = (f : (a : P) → P₂) (s.touchpoint signs i)

Tactic:
simp [touchpoint, h.excenter_map, ← orthogonalProjectionSpan_map]

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

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
i : Fin (n + 1)
⊢ 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
i : Fin (n + 1)
this : Nonempty.{u_2 + 1} ↥S
⊢ (↑((s.restrict S hS).touchpoint signs i) : P) = s.touchpoint signs i

Tactic:
(h.touchpoint_map S.subtypeₐᵢ i).symm

Premises used: Affine.Simplex.ExcenterExists.touchpoint_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
i : Fin (n + 1)
this : Nonempty.{u_2 + 1} ↥S
⊢ (↑((s.restrict S hS).touchpoint signs i) : P) = s.touchpoint signs i

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

Premises used: Affine.Simplex.ExcenterExists.touchpoint_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))
i : Fin (n + 1)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.touchpoint signs i)

Tactic:
orthogonalProjection_mem _

Premises used: Set.Mem, EuclideanGeometry.orthogonalProjection_mem, Affine.Simplex.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))
i : Fin (n + 1)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.touchpoint signs i)

Tactic:
SetLike.le_def.1 (affineSpan_mono _ ?_) (s.touchpoint_mem_affineSpan signs i)

Premises used: SetLike.le_def, Affine.Simplex.touchpoint_mem_affineSpan, Iff.mp, affineSpan_mono
-- 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)
refine : Set.range (s.faceOpposite i).points ⊆ Set.range s.points
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.touchpoint signs i)

Tactic:
refine SetLike.le_def.1 (affineSpan_mono _ ?_) (s.touchpoint_mem_affineSpan signs i)

Premises used: SetLike.le_def, Affine.Simplex.touchpoint_mem_affineSpan, Iff.mp, affineSpan_mono
-- 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)
⊢ Set.range (s.faceOpposite i).points ⊆ Set.range s.points

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
s : Simplex ℝ P 1
signs : Finset (Fin 2)
i : Fin 2
⊢ s.touchpoint signs i = s.points i.rev

Tactic:
s.orthogonalProjectionSpan_faceOpposite_eq_point_rev _ _

Premises used: Set.Mem, Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev, Affine.Simplex.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)
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)⁻¹|
⊢ (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

Tactic:
rw [h.signedInfDist_excenter_eq_mul_sum_inv, mul_assoc, exradius_eq_abs_inv_sum]

Premises used: mul_assoc, Affine.Simplex.exradius_eq_abs_inv_sum, Affine.Simplex.ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv
-- 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)
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)⁻¹|
⊢ 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:
congr
-- 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)
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
e_a₅ 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)⁻¹|

Tactic:
rw [← mul_eq_one_iff_inv_eq₀ h, ← mul_assoc, self_mul_sign, ← abs_mul, mul_inv_cancel₀ h, abs_one]

Premises used: mul_inv_cancel₀, mul_eq_one_iff_inv_eq₀, mul_assoc, abs_mul, self_mul_sign, abs_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
i : Fin (n + 1)
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
⊢ (s.signedInfDist i : (a : P) → ℝ) s.incenter = s.inradius

Tactic:
rw [incenter, exsphere_center, s.excenterExists_empty.signedInfDist_excenter]

Premises used: Affine.Simplex.incenter, Affine.Simplex.ExcenterExists.signedInfDist_excenter, Affine.Simplex.exsphere_center, 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
i : Fin (n + 1)
⊢ 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:
simp (discharger := 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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  HMul.hMul (α := ℝ) |if i ∈ signs then -1 else 1|
        |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
      s.exradius signs =
    s.exradius signs
⊢ dist (s.excenter signs) (s.touchpoint signs i) = s.exradius signs

Tactic:
rw [touchpoint,
    ← abs_signedInfDist_eq_dist_of_mem_affineSpan_range i h.excenter_mem_affineSpan_range,
    h.signedInfDist_excenter, abs_mul, abs_mul, abs_of_nonneg (s.exradius_nonneg signs)]

Premises used: abs_mul, Affine.Simplex.exradius_nonneg, Affine.Simplex.ExcenterExists.excenter_mem_affineSpan_range, Affine.Simplex.touchpoint, abs_of_nonneg, Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range, Affine.Simplex.ExcenterExists.signedInfDist_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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
simp :
  |(↑((SignType.sign : (a : ℝ) → SignType) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)) : ℝ)| *
      s.exradius signs =
    s.exradius 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 =
    s.exradius signs

Tactic:
simp only [abs_ite, abs_neg, abs_one, ite_self, one_mul]

Premises used: abs_neg, abs_ite, ite_self, abs_one, one_mul