awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  HMul.hMul (α := SignType) (β := SignType)
      ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights signs i) : SignType)
      ((SignType.sign : (a : ℝ) → SignType)
          ‖s.points i -ᵥ
              (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                      (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                    (s.points i)) :
                P)‖ :
        SignType) =
    (SignType.sign : (a : ℝ) → SignType) (s.excenterWeights signs i)
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist i : (a : P) → ℝ) (s.excenter signs) : ℝ) : SignType)
    ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights signs i) : SignType)

Tactic:
rw [excenter_eq_affineCombination,
    signedInfDist_affineCombination _ _ h.sum_excenterWeights_eq_one, sign_mul]

Premises used: Affine.Simplex.excenter_eq_affineCombination, sign_mul, Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one, Affine.Simplex.signedInfDist_affineCombination
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ HMul.hMul (α := SignType) (β := SignType)
      ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights signs i) : SignType) (1 : SignType) =
    (SignType.sign : (a : ℝ) → SignType) (s.excenterWeights signs i)

Tactic:
mul_one _

Premises used: mul_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)
h₁ :
  Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType)
        ‖s.points i -ᵥ
            (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                    (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                  (s.points i)) :
              P)‖ :
      SignType)
    (1 : SignType)
⊢ HMul.hMul (α := SignType) (β := SignType)
      ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights signs i) : SignType)
      ((SignType.sign : (a : ℝ) → SignType)
          ‖s.points i -ᵥ
              (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                      (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                    (s.points i)) :
                P)‖ :
        SignType) =
    (SignType.sign : (a : ℝ) → SignType) (s.excenterWeights signs i)

Tactic:
convert! mul_one _

Premises used: mul_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)
h₁ :
  0 <
    dist (s.points i)
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.points i)) :
        P)
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType)
        ‖s.points i -ᵥ
            (↑(((s.faceOpposite i).orthogonalProjectionSpan :
                    (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
                  (s.points i)) :
              P)‖ :
      SignType)
    (1 : SignType)

Tactic:
rw [sign_eq_one_iff, ← dist_eq_norm_vsub]

Premises used: dist_eq_norm_vsub, 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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ 0 <
    dist (s.points i)
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.points i)) :
        P)

Tactic:
s.height_pos _

Premises used: Affine.Simplex.height, Affine.Simplex.height_pos, 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)
⊢ 0 <
    dist (s.points i)
      (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.points i)) :
        P)

Tactic:
exact s.height_pos _

Premises used: Affine.Simplex.height_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
i : Fin (n + 1)
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist i : (a : P) → ℝ) (s.excenter ∅) : ℝ) : SignType)
    ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights ∅ i) : SignType)

Tactic:
s.excenterExists_empty.sign_signedInfDist_excenter i

Premises used: Affine.Simplex.ExcenterExists.sign_signedInfDist_excenter, Affine.Simplex.excenterExists_empty
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
h : Eq (α := SignType) (1 : SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights ∅ i) : SignType)
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist i : (a : P) → ℝ) s.incenter : ℝ) : SignType) (1 : SignType)

Tactic:
convert! s.excenterExists_empty.sign_signedInfDist_excenter i

Premises used: Affine.Simplex.ExcenterExists.sign_signedInfDist_excenter, Affine.Simplex.excenterExists_empty
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ Eq (α := SignType) (1 : SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights ∅ i) : SignType)

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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), w j) 1
mp :
  (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.excenter signs →
    w = s.excenterWeights signs
mpr :
  w = s.excenterWeights signs →
    (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.excenter signs
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.excenter signs ↔
    w = s.excenterWeights signs

Tactic:
constructor
-- 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
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), w j) 1
mp :
  Eq.{u_2 + 1} (α := P) ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs) : P) →
    w = s.excenterWeights signs
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.excenter signs →
    w = s.excenterWeights signs

Tactic:
simp_rw [excenter, exsphere]

Premises used: Affine.Simplex.excenter, 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
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), w j) 1
⊢ Eq.{u_2 + 1} (α := P) ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs) : P) →
    w = s.excenterWeights signs

Tactic:
fun he ↦ (affineIndependent_iff_eq_of_fintype_affineCombination_eq ℝ s.points).1
      s.independent _ _ hw h.sum_excenterWeights_eq_one he

Premises used: Affine.Simplex.points, Real, affineIndependent_iff_eq_of_fintype_affineCombination_eq, Affine.Simplex.excenterWeights, Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one, Iff.mp, Affine.Simplex.independent
-- 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
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), w j) 1
⊢ Eq.{u_2 + 1} (α := P) ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs) : P) →
    w = s.excenterWeights signs

Tactic:
exact fun he ↦ (affineIndependent_iff_eq_of_fintype_affineCombination_eq ℝ s.points).1
      s.independent _ _ hw h.sum_excenterWeights_eq_one he

Premises used: Affine.Simplex.points, Real, affineIndependent_iff_eq_of_fintype_affineCombination_eq, Affine.Simplex.excenterWeights, Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one, Iff.mp, Affine.Simplex.independent
-- 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
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), s.excenterWeights signs j) 1
mpr :
  (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs) =
    (s.exsphere signs).center
mpr₁ mpr₂ :
  Eq.{u_2 + 1} (α := P)
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs) : P)
    (Sphere.center
        {
          center :=
            (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs),
          radius := |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹| } :
      P)
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs) =
    s.excenter signs

Tactic:
rw [excenter, exsphere]

Premises used: Affine.Simplex.excenter, 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
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.face hfs).points)) (s.excenter signs)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1))))) (s.excenter signs)

Tactic:
rw [range_face_points] at hm

Premises used: Affine.Simplex.range_face_points
-- 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
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1))))) (s.excenter signs)
⊢ m + 1 ≤ #fs

Tactic:
have : m + 1 ≤ #fs := hfs.ge
-- 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
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1))))) (s.excenter signs)
this : m + 1 ≤ #fs
⊢ m + 1 ≤ Finset.card (α := Fin (n + 1)) Finset.univ

Tactic:
grw [fs.subset_univ] at this

Premises used: Finset.subset_univ
-- 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
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1))))) (s.excenter signs)
this : m + 1 ≤ Finset.card (α := Fin (n + 1)) Finset.univ
simp : ∀ (this : m + 1 ≤ n + 1), #fs < n + 1
⊢ #fs < Finset.card (α := Fin (n + 1)) Finset.univ

Tactic:
simp only [Finset.card_univ, Fintype.card_fin] at *

Premises used: Finset.card_univ, Fintype.card_fin
-- 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
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1))))) (s.excenter signs)
this : m + 1 ≤ n + 1
⊢ #fs < n + 1

Tactic:
lia
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1))))) (s.excenter signs)
⊢ #fs < Finset.card (α := Fin (n + 1)) Finset.univ

Tactic:
have hc : #fs < #(Finset.univ : Finset (Fin (n + 1))) := by
      have : m + 1 ≤ #fs := hfs.ge
      grw [fs.subset_univ] at this
      simp only [Finset.card_univ, Fintype.card_fin] at *
      lia
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1))))) (s.excenter signs)
hc : #fs < Finset.card (α := Fin (n + 1)) Finset.univ
obtain : ∀ (i : Fin (n + 1)) (hi : i ∉ fs), ∃ (i : Fin (n + 1)), i ∉ fs
⊢ ∃ (i : Fin (n + 1)), i ∉ fs

Tactic:
obtain ⟨i, -, hi⟩ := Finset.exists_mem_notMem_of_card_lt_card hc

Premises used: Finset.exists_mem_notMem_of_card_lt_card
-- 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
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1))))) (s.excenter signs)
hc : #fs < Finset.card (α := Fin (n + 1)) Finset.univ
i : Fin (n + 1)
hi : i ∉ fs
⊢ ∃ (i : Fin (n + 1)), i ∉ fs

Tactic:
⟨i, hi⟩

Premises used: Exists.intro
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1))))) (s.excenter signs)
hc : #fs < Finset.card (α := Fin (n + 1)) Finset.univ
i : Fin (n + 1)
hi : i ∉ fs
⊢ ∃ (i : Fin (n + 1)), i ∉ fs

Tactic:
exact ⟨i, hi⟩
-- 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
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1))))) (s.excenter signs)
obtain : ∀ (i : Fin (n + 1)) (hi : i ∉ (↑fs : Set (Fin (n + 1)))), False
⊢ False

Tactic:
obtain ⟨i, hi⟩ : ∃ i, i ∉ (fs : Set (Fin (n + 1))) := by
    simp only [SetLike.mem_coe]
    have hc : #fs < #(Finset.univ : Finset (Fin (n + 1))) := by
      have : m + 1 ≤ #fs := hfs.ge
      grw [fs.subset_univ] at this
      simp only [Finset.card_univ, Fintype.card_fin] at *
      lia
    obtain ⟨i, -, hi⟩ := Finset.exists_mem_notMem_of_card_lt_card hc
    exact ⟨i, hi⟩

Premises used: SetLike.coe
-- 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
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1))))) (s.excenter signs)
i : Fin (n + 1)
hi : i ∉ (↑fs : Set (Fin (n + 1)))
rw :
  ∀
    (hm :
      Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1)))))
        ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs) : P))
    (i : Fin (n + 1)) (hi : i ∉ (↑fs : Set (Fin (n + 1)))), False
⊢ False

Tactic:
rw [excenter_eq_affineCombination] at hm

Premises used: Affine.Simplex.excenter_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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1)))))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs) : P)
i : Fin (n + 1)
hi : i ∉ (↑fs : Set (Fin (n + 1)))
⊢ False

Tactic:
h.excenterWeights_ne_zero i (s.independent.eq_zero_of_affineCombination_mem_affineSpan
    h.sum_excenterWeights_eq_one hm (Finset.mem_univ i) hi)

Premises used: Finset.mem_univ, Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one, Affine.Simplex.independent, Affine.Simplex.ExcenterExists.excenterWeights_ne_zero, AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan
-- 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
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1)))))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs) : P)
i : Fin (n + 1)
hi : i ∉ (↑fs : Set (Fin (n + 1)))
⊢ False

Tactic:
exact h.excenterWeights_ne_zero i (s.independent.eq_zero_of_affineCombination_mem_affineSpan
    h.sum_excenterWeights_eq_one hm (Finset.mem_univ i) hi)

Premises used: Finset.mem_univ, Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one, Affine.Simplex.independent, Affine.Simplex.ExcenterExists.excenterWeights_ne_zero, AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan
-- 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
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
⊢ s.incenter ∉ affineSpan ℝ (Set.range (s.face hfs).points)

Tactic:
s.excenterExists_empty.excenter_notMem_affineSpan_face hfs hne

Premises used: Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_face, Set.Mem, 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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ n ≠ 0

Tactic:
have := NeZero.ne n
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
this : n ≠ 0
⊢ n - 1 ≠ n

Tactic:
lia
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ s.incenter ∉ affineSpan ℝ (Set.range (s.faceOpposite i).points)

Tactic:
s.excenterExists_empty.excenter_notMem_affineSpan_faceOpposite i

Premises used: Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_faceOpposite, Set.Mem, 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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ Finset.card (α := Fin (n + 1)) {i} = HAdd.hAdd (α := ℕ) 0 1

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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ s.excenter signs ∉ affineSpan ℝ (Set.range (ι := Fin (HAdd.hAdd (α := ℕ) 0 1)) (points (s.face ⋯)))

Tactic:
have hf := h.excenter_notMem_affineSpan_face (fs := {i}) (m := 0) (by simp) (NeZero.ne' _)