awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
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
⊢ False
have h₁ : 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
Cleared hypotheses: h, hj
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
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
⊢ False
have revert : ∀ (h : s.excenterWeights ∅ j + s.excenterWeights ∅ i + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i = 1), False
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
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), False
have h : 1 < s.excenterWeights ∅ j + s.excenterWeights ∅ i + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i
Tactic: apply ne_of_gt
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
hj : j ≠ i
⊢ 1 < s.excenterWeights ∅ j + s.excenterWeights ∅ i + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i
have h : 1 < s.excenterWeights ∅ i + s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i
Tactic: nth_rw 2 [add_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
hj : j ≠ i
⊢ 1 < s.excenterWeights ∅ i + s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i
have h : s.excenterWeights ∅ i < s.excenterWeights ∅ i + s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i
Tactic: grw [hp]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
hj : j ≠ i
⊢ s.excenterWeights ∅ i < s.excenterWeights ∅ i + s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i
have h : 0 < s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i
Tactic: rw [add_assoc, lt_add_iff_pos_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ (s.signedInfDist i : (a : P) → ℝ) (s.excenter signs) =
    HMul.hMul (α := ℝ) (if i ∈ signs then -1 else 1) (∑ j : Fin (n + 1), s.excenterWeightsUnnorm signs j)⁻¹
have 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)⁻¹)⁻¹
Tactic: simp_rw [excenter_eq_affineCombination,
    signedInfDist_affineCombination _ _ h.sum_excenterWeights_eq_one, excenterWeights,
    Pi.smul_apply, ← dist_eq_norm_vsub, excenterWeightsUnnorm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ 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)⁻¹)⁻¹
have 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)⁻¹)⁻¹
Tactic: rw [← altitudeFoot, ← height]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist i : (a : P) → ℝ) (s.excenter signs) : ℝ) : SignType)
    ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights signs i) : SignType)
have 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)
Tactic: rw [excenter_eq_affineCombination,
    signedInfDist_affineCombination _ _ h.sum_excenterWeights_eq_one, sign_mul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ HMul.hMul (α := 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)
have 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)
Tactic: convert! mul_one _
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ 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)
have h₁ : 0 <
  dist (s.points i)
    (↑(((s.faceOpposite i).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.points i)) :
      P)
Tactic: rw [sign_eq_one_iff, ← dist_eq_norm_vsub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist i : (a : P) → ℝ) s.incenter : ℝ) : SignType) (1 : SignType)
have h : Eq (α := SignType) (1 : SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights ∅ i) : SignType)
Tactic: convert! s.excenterExists_empty.sign_signedInfDist_excenter i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), w j) 1
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.excenter signs ↔
    w = s.excenterWeights signs
have mp : (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.excenter signs →
  w = s.excenterWeights signs
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
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
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.excenter signs ↔
    w = s.excenterWeights signs
have mpr : w = s.excenterWeights signs →
  (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.excenter signs
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), w j) 1
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.excenter signs →
    w = s.excenterWeights signs
have 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
Tactic: simp_rw [excenter, exsphere]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), s.excenterWeights signs j) 1
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs) =
    s.excenter signs
have mpr : (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs) =
  (s.exsphere signs).center
Tactic: rw [excenter, exsphere]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
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
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.excenterWeights signs) =
    s.excenter signs
have 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)
Tactic: rw [excenter, exsphere]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
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)
⊢ False
have hm₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' (↑fs : Set (Fin (n + 1))))) (s.excenter signs)
Tactic: rw [range_face_points] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
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
have this : m + 1 ≤ #fs
Tactic: have : m + 1 ≤ #fs := hfs.ge
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
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
⊢ #fs < Finset.card (α := Fin (n + 1)) Finset.univ
have this₁ : m + 1 ≤ Finset.card (α := Fin (n + 1)) Finset.univ
Tactic: grw [fs.subset_univ] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
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
⊢ #fs < Finset.card (α := Fin (n + 1)) Finset.univ
have simp : ∀ (this : m + 1 ≤ n + 1), #fs < n + 1
Tactic: simp only [Finset.card_univ, Fintype.card_fin] at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
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)), i ∉ fs
have hc : #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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
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)), i ∉ fs
have obtain : ∀ (i : Fin (n + 1)) (hi : i ∉ fs), ∃ (i : Fin (n + 1)), i ∉ fs
Tactic: obtain ⟨i, -, hi⟩ := Finset.exists_mem_notMem_of_card_lt_card hc
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
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)
⊢ False
have obtain : ∀ (i : Fin (n + 1)) (hi : i ∉ (↑fs : Set (Fin (n + 1)))), 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⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
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)))
⊢ False
have 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
Tactic: rw [excenter_eq_affineCombination] at hm
Cleared hypotheses: hm, i, hi
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ n - 1 ≠ n
have this : n ≠ 0
Tactic: have := NeZero.ne n
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ s.excenter signs ≠ s.points i
have hf : s.excenter signs ∉ affineSpan ℝ (Set.range (ι := Fin (HAdd.hAdd (α := ℕ) 0 1)) (points (s.face sorry)))
Tactic: have hf := h.excenter_notMem_affineSpan_face (fs := {i}) (m := 0) (by simp) (NeZero.ne' _)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
⊢ s.excenter signs ∉ affineSpan ℝ {s.points i, s.points j}
have pos : ∀ (hij : i = j), s.excenter signs ∉ affineSpan ℝ {s.points i, s.points j}
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
pos : ∀ (hij : i = j), s.excenter signs ∉ affineSpan ℝ {s.points i, s.points j}
⊢ s.excenter signs ∉ affineSpan ℝ {s.points i, s.points j}
have neg : ∀ (hij : ¬i = j), s.excenter signs ∉ affineSpan ℝ {s.points i, s.points j}
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : i = j
⊢ s.excenter signs ∉ affineSpan ℝ {s.points i, s.points j}
have pos : ¬s.excenter signs = s.points j
Tactic: simp only [hij, Set.mem_singleton_iff, Set.insert_eq_of_mem,
      AffineSubspace.mem_affineSpan_singleton]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : ¬i = j
⊢ s.excenter signs ∉ affineSpan ℝ {s.points i, s.points j}
have h₁ : {s.points i, s.points j} = Set.range (s.face (fs := {i, j}) sorry).points
Tactic: convert!
    h.excenter_notMem_affineSpan_face (fs := { i, j }) (m := 1) (by simp_all)
      Nat.AtLeastTwo.ne_one.symm
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
⊢ s.excenterWeights signs₁ = s.excenterWeights signs₂ ↔ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
have refine_1 : ∀ (h : s.excenterWeights signs₁ = s.excenterWeights signs₂), signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
refine_1 : ∀ (h : s.excenterWeights signs₁ = s.excenterWeights signs₂), signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
⊢ s.excenterWeights signs₁ = s.excenterWeights signs₂ ↔ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
have refine_2 : ∀ (h : signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ), s.excenterWeights signs₁ = s.excenterWeights signs₂
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩