awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ Finset.erase (Finset.erase Finset.univ 0) i
⊢ ⟪s.points i -ᵥ s.points 0, s.points j -ᵥ s.altitudeFoot j⟫ = 0
have h : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i -ᵥ s.points 0))ᗮ (s.points j -ᵥ s.altitudeFoot j)
Tactic: rw [← Submodule.mem_orthogonal_singleton_iff_inner_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
i : Fin (n + 1)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ Finset.erase (Finset.erase Finset.univ 0) i
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i -ᵥ s.points 0))ᗮ (s.points j -ᵥ s.altitudeFoot j)
have h : LE.le (α := Submodule ℝ V) (ℝ ∙ (s.points i -ᵥ s.points 0))
  (AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite j).points)))
Tactic: refine SetLike.le_def.1 (Submodule.orthogonal_le ?_)
      (vsub_orthogonalProjection_mem_direction_orthogonal _ _)
-- 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)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ Finset.erase (Finset.erase Finset.univ 0) i
⊢ LE.le (α := Submodule ℝ V) (ℝ ∙ (s.points i -ᵥ s.points 0))
    (AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite j).points)))
have h : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points)) (s.points i -ᵥ s.points 0)
Tactic: rw [Submodule.span_singleton_le_iff_mem, direction_affineSpan]
-- 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
i : Fin (n + 1)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ Finset.erase (Finset.erase Finset.univ 0) i
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points)) (s.points i -ᵥ s.points 0)
have hj₁ : j ≠ i ∧ j ≠ 0
Tactic: simp only [Finset.mem_erase, Finset.mem_univ, and_true] at hj
Cleared hypotheses: 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)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points)) (s.points i -ᵥ s.points 0)
have h : s.points i ∈ Set.range (s.faceOpposite j).points
Tactic: refine vsub_mem_vectorSpan _ ?_ ?_
-- 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)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
h : s.points i ∈ Set.range (s.faceOpposite j).points
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points)) (s.points i -ᵥ s.points 0)
have h₁ : s.points 0 ∈ Set.range (s.faceOpposite j).points
Tactic: refine vsub_mem_vectorSpan _ ?_ ?_
-- 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)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
⊢ s.points i ∈ Set.range (s.faceOpposite j).points
have h : ∃ (x : Fin (n + 1)), Membership.mem (γ := Set (Fin (n + 1))) {j}ᶜ x ∧ s.points x = s.points i
Tactic: simp only [range_faceOpposite_points, Set.mem_image]
-- 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)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
⊢ s.points 0 ∈ Set.range (s.faceOpposite j).points
have h : ∃ (x : Fin (n + 1)), Membership.mem (γ := Set (Fin (n + 1))) {j}ᶜ x ∧ s.points x = s.points 0
Tactic: simp only [range_faceOpposite_points, Set.mem_image]
-- 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)
hi : i ≠ 0
⊢ 0 =
    ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height 0)⁻¹ 2 • (s.points 0 -ᵥ s.altitudeFoot 0)⟫ +
      ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i)⟫
have h : 0 =
  -((HPow.hPow (β := ℕ) (s.height 0) 2)⁻¹ * HPow.hPow (β := ℕ) (s.height 0) 2) +
    HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 * HPow.hPow (β := ℕ) (s.height i) 2
Tactic: rw [inner_smul_right, inner_smul_right, inner_vsub_vsub_altitudeFoot_eq_height_sq _ hi,
      ← neg_vsub_eq_vsub_rev, inner_neg_left, inner_vsub_vsub_altitudeFoot_eq_height_sq _ hi.symm,
      mul_neg, inv_pow]
-- 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)
⊢ (s.height i)⁻¹ =
    ∑ j : Fin (n + 1) with j ≠ i,
      -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) * (s.height j)⁻¹
have rw : (s.height i)⁻¹ -
    ∑ j : Fin (n + 1) with j ≠ i,
      -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) * (s.height j)⁻¹ =
  0
Tactic: rw [← sub_eq_zero]
-- 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)
⊢ (s.height i)⁻¹ -
      ∑ j : Fin (n + 1) with j ≠ i,
        -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) *
          (s.height j)⁻¹ =
    0
have simp_rw : (s.height i)⁻¹ -
    ∑ x : Fin (n + 1) with x ≠ i,
      -(⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) * (s.height x)⁻¹) =
  0
Tactic: simp_rw [neg_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
i : Fin (n + 1)
⊢ (s.height i)⁻¹ -
      ∑ x : Fin (n + 1) with x ≠ i,
        -(⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) *
            (s.height x)⁻¹) =
    0
have rw : (s.height i)⁻¹ +
    (∑ x : Fin (n + 1),
        ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) * (s.height x)⁻¹ -
      dist (s.points i) (s.altitudeFoot i) * dist (s.points i) (s.altitudeFoot i) / (s.height i * s.height i) *
        (s.height i)⁻¹) =
  0
Tactic: rw [Finset.sum_neg_distrib, sub_neg_eq_add, Finset.filter_ne',
    Finset.sum_erase_eq_sub (Finset.mem_univ _), real_inner_self_eq_norm_mul_norm,
    ← 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)
⊢ (s.height i)⁻¹ +
      (∑ x : Fin (n + 1),
          ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) *
            (s.height x)⁻¹ -
        dist (s.points i) (s.altitudeFoot i) * dist (s.points i) (s.altitudeFoot i) / (s.height i * s.height i) *
          (s.height i)⁻¹) =
    0
have simp : Eq (α := ℝ)
  (∑ x : Fin (n + 1),
    ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ /
        (dist (s.points i) (s.altitudeFoot i) * dist (s.points x) (s.altitudeFoot x)) *
      (dist (s.points x) (s.altitudeFoot x))⁻¹)
  0
Tactic: simp only [height, ne_eq, mul_eq_zero, dist_eq_zero, ne_altitudeFoot, or_self,
    not_false_eq_true, div_self, one_mul, add_sub_cancel]
-- 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
i : Fin (n + 1)
⊢ Eq (α := ℝ)
    (∑ x : Fin (n + 1),
      ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ /
          (dist (s.points i) (s.altitudeFoot i) * dist (s.points x) (s.altitudeFoot x)) *
        (dist (s.points x) (s.altitudeFoot x))⁻¹)
    0
have h : Eq.{u_1 + 1} (α := V) (∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i)) 0
Tactic: have h := s.sum_inv_height_sq_smul_vsub_eq_zero
-- 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
i : Fin (n + 1)
h : Eq.{u_1 + 1} (α := V) (∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i)) 0
⊢ Eq (α := ℝ)
    (∑ x : Fin (n + 1),
      ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ /
          (dist (s.points i) (s.altitudeFoot i) * dist (s.points x) (s.altitudeFoot x)) *
        (dist (s.points x) (s.altitudeFoot x))⁻¹)
    0
have h₁ : (s.height i)⁻¹ *
    ⟪s.points i -ᵥ s.altitudeFoot i,
      ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i)⟫ =
  (s.height i)⁻¹ * ⟪s.points i -ᵥ s.altitudeFoot i, 0⟫
Tactic: apply_fun fun v ↦ (s.height i)⁻¹ * ⟪s.points i -ᵥ s.altitudeFoot i, v⟫ at h
Cleared hypotheses: h
-- 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
i : Fin (n + 1)
h :
  (s.height i)⁻¹ *
      ⟪s.points i -ᵥ s.altitudeFoot i,
        ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i)⟫ =
    (s.height i)⁻¹ * ⟪s.points i -ᵥ s.altitudeFoot i, 0⟫
⊢ Eq (α := ℝ)
    (∑ x : Fin (n + 1),
      ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ /
          (dist (s.points i) (s.altitudeFoot i) * dist (s.points x) (s.altitudeFoot x)) *
        (dist (s.points x) (s.altitudeFoot x))⁻¹)
    0
have h₁ : ∑ i_1 : Fin (n + 1),
    (s.height i)⁻¹ *
      ⟪s.points i -ᵥ s.altitudeFoot i, HPow.hPow (β := ℕ) (s.height i_1)⁻¹ 2 • (s.points i_1 -ᵥ s.altitudeFoot i_1)⟫ =
  (s.height i)⁻¹ * ⟪s.points i -ᵥ s.altitudeFoot i, 0⟫
Tactic: rw [inner_sum, Finset.mul_sum] at h
Cleared hypotheses: h
-- 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
i : Fin (n + 1)
h :
  ∑ i_1 : Fin (n + 1),
      (s.height i)⁻¹ *
        ⟪s.points i -ᵥ s.altitudeFoot i, HPow.hPow (β := ℕ) (s.height i_1)⁻¹ 2 • (s.points i_1 -ᵥ s.altitudeFoot i_1)⟫ =
    (s.height i)⁻¹ * ⟪s.points i -ᵥ s.altitudeFoot i, 0⟫
⊢ Eq (α := ℝ)
    (∑ x : Fin (n + 1),
      ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ /
          (dist (s.points i) (s.altitudeFoot i) * dist (s.points x) (s.altitudeFoot x)) *
        (dist (s.points x) (s.altitudeFoot x))⁻¹)
    0
have h₁ : Eq (α := ℝ)
  (∑ x : Fin (n + 1),
    (dist (s.points i) (s.altitudeFoot i))⁻¹ *
      (HPow.hPow (β := ℕ) (dist (s.points x) (s.altitudeFoot x))⁻¹ 2 *
        ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫))
  0
Tactic: simp only [inner_zero_right, mul_zero, inner_smul_right, height] at 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)
h :
  Eq (α := ℝ)
    (∑ x : Fin (n + 1),
      (dist (s.points i) (s.altitudeFoot i))⁻¹ *
        (HPow.hPow (β := ℕ) (dist (s.points x) (s.altitudeFoot x))⁻¹ 2 *
          ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫))
    0
⊢ Eq (α := ℝ)
    (∑ x : Fin (n + 1),
      ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ /
          (dist (s.points i) (s.altitudeFoot i) * dist (s.points x) (s.altitudeFoot x)) *
        (dist (s.points x) (s.altitudeFoot x))⁻¹)
    0
have h₁ : ∀ (j : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ j →
    ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ /
          (dist (s.points i) (s.altitudeFoot i) * dist (s.points j) (s.altitudeFoot j)) *
        (dist (s.points j) (s.altitudeFoot j))⁻¹ =
      (dist (s.points i) (s.altitudeFoot i))⁻¹ *
        (HPow.hPow (β := ℕ) (dist (s.points j) (s.altitudeFoot j))⁻¹ 2 *
          ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫)
Tactic: convert! h using 2 with 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
i : Fin (n + 1)
⊢ (s.height i)⁻¹ < ∑ j : Fin (n + 1) with j ≠ i, (s.height j)⁻¹
have rw : LT.lt (α := ℝ)
  (∑ j : Fin (n + 1) with j ≠ i,
    -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) * (s.height j)⁻¹)
  (∑ j : Fin (n + 1) with j ≠ i, (s.height j)⁻¹)
Tactic: rw [inv_height_eq_sum_mul_inv_dist]
-- 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
i : Fin (n + 1)
⊢ LT.lt (α := ℝ)
    (∑ j : Fin (n + 1) with j ≠ i,
      -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) * (s.height j)⁻¹)
    (∑ j : Fin (n + 1) with j ≠ i, (s.height j)⁻¹)
have refine_1 : Finset.Nonempty (α := Fin (n + 1)) {k : Fin (n + 1) | k ≠ i}
Tactic: refine Finset.sum_lt_sum_of_nonempty ?_ ?_
-- 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
i : Fin (n + 1)
refine_1 : Finset.Nonempty (α := Fin (n + 1)) {k : Fin (n + 1) | k ≠ i}
⊢ LT.lt (α := ℝ)
    (∑ j : Fin (n + 1) with j ≠ i,
      -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) * (s.height j)⁻¹)
    (∑ j : Fin (n + 1) with j ≠ i, (s.height j)⁻¹)
have refine_2 : ∀ (i_1 : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) {k : Fin (n + 1) | k ≠ i} i_1 →
    -(⟪s.points i -ᵥ s.altitudeFoot i, s.points i_1 -ᵥ s.altitudeFoot i_1⟫ / (s.height i * s.height i_1)) *
        (s.height i_1)⁻¹ <
      (s.height i_1)⁻¹
Tactic: refine Finset.sum_lt_sum_of_nonempty ?_ ?_
-- 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
i : Fin (n + 1)
⊢ Finset.Nonempty (α := Fin (n + 1)) {k : Fin (n + 1) | k ≠ i}
have refine_1 : #(Finset.erase Finset.univ i) ≠ 0
Tactic: rw [Finset.filter_ne', ← Finset.card_ne_zero]
-- 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
i : Fin (n + 1)
⊢ #(Finset.erase Finset.univ i) ≠ 0
have refine_1 : n ≠ 0
Tactic: simp only [Finset.mem_univ, Finset.card_erase_of_mem, Finset.card_univ, Fintype.card_fin,
      add_tsub_cancel_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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
hj : Membership.mem (γ := Finset (Fin (n + 1))) {k : Fin (n + 1) | k ≠ i} j
⊢ -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) * (s.height j)⁻¹ <
    (s.height j)⁻¹
have refine_2 : 0 < (s.height j)⁻¹
Tactic: refine mul_lt_of_lt_one_left ?_ ?_
-- 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
i j : Fin (n + 1)
hj : Membership.mem (γ := Finset (Fin (n + 1))) {k : Fin (n + 1) | k ≠ i} j
refine_2 : 0 < (s.height j)⁻¹
⊢ -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) * (s.height j)⁻¹ <
    (s.height j)⁻¹
have refine_2₁ : -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) < 1
Tactic: refine mul_lt_of_lt_one_left ?_ ?_
-- 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
i j : Fin (n + 1)
hj : Membership.mem (γ := Finset (Fin (n + 1))) {k : Fin (n + 1) | k ≠ i} j
⊢ -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) < 1
have refine_2 : -1 < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)
Tactic: rw [neg_lt]
-- 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
i : Fin (n + 1)
⊢ LT.lt (α := ℝ) 0 (∑ j : Fin (n + 1), s.excenterWeightsUnnorm {i} j)
have rw : 0 < s.excenterWeightsUnnorm {i} i + ∑ i_1 ∈ {i}ᶜ, s.excenterWeightsUnnorm {i} i_1
Tactic: rw [← Finset.sum_add_sum_compl {i}, Finset.sum_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
i : Fin (n + 1)
⊢ 0 <
    (if Membership.mem (γ := Finset (Fin (n + 1))) {i} i then -1 else 1) * (s.height i)⁻¹ +
      ∑ i_1 ∈ {i}ᶜ, s.excenterWeightsUnnorm {i} i_1
have simp : (s.height i)⁻¹ < ∑ i_1 ∈ {i}ᶜ, s.excenterWeightsUnnorm {i} i_1
Tactic: simp only [Finset.mem_singleton, ↓reduceIte, neg_mul, one_mul, lt_neg_add_iff_add_lt, add_zero]
-- 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
i : Fin (n + 1)
⊢ (s.height i)⁻¹ < ∑ i_1 ∈ {i}ᶜ, s.excenterWeightsUnnorm {i} i_1
have h : Eq (α := Finset (Fin (n + 1))) {i}ᶜ {k : Fin (n + 1) | k ≠ i}
Tactic: convert! s.inv_height_lt_sum_inv_height i using 2 with j 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
h : Eq (α := Finset (Fin (n + 1))) {i}ᶜ {k : Fin (n + 1) | k ≠ i}
⊢ (s.height i)⁻¹ < ∑ i_1 ∈ {i}ᶜ, s.excenterWeightsUnnorm {i} i_1
have h₁ : ∀ (j : Fin (n + 1)) (h : Membership.mem (γ := Finset (Fin (n + 1))) {k : Fin (n + 1) | k ≠ i} j),
  s.excenterWeightsUnnorm {i} j = (s.height j)⁻¹
Tactic: convert! s.inv_height_lt_sum_inv_height i using 2 with j 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
⊢ Eq (α := Finset (Fin (n + 1))) {i}ᶜ {k : Fin (n + 1) | k ≠ i}
have h : ∀ (j : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ j ↔
    Membership.mem (γ := Finset (Fin (n + 1))) {k : Fin (n + 1) | k ≠ i} j
Tactic: ext j
-- 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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) {k : Fin (n + 1) | k ≠ i} j
⊢ s.excenterWeightsUnnorm {i} j = (s.height j)⁻¹
have h₁ : j ≠ i
Tactic: rw [Finset.mem_filter_univ] at 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
⊢ Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} i) : SignType) (-1 : SignType)
have simp_rw : HMul.hMul (α := SignType) (β := SignType)
    ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
    ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} i) : SignType) =
  -1
Tactic: simp_rw [excenterWeights, Pi.smul_apply, smul_eq_mul, 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
⊢ HMul.hMul (α := SignType) (β := SignType)
      ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
      ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} i) : SignType) =
    -1
have h : Eq (α := SignType)
  ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
  (1 : SignType)
Tactic: convert! one_mul _