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
i : Fin (n + 1)
hi : i ≠ 0
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
⊢ 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)⟫

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]

Premises used: Ne.symm, inv_pow, inner_smul_right, neg_vsub_eq_vsub_rev, mul_neg, inner_neg_left, Affine.Simplex.inner_vsub_vsub_altitudeFoot_eq_height_sq
-- 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)
hi : i ≠ 0
⊢ 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:
simp [height]

Premises used: Affine.Simplex.height
-- 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 :
  (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
⊢ (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)⁻¹

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
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
⊢ (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:
simp_rw [neg_mul]

Premises used: neg_mul
-- 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 :
  (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
⊢ (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:
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]

Premises used: Finset.mem_univ, Finset.sum_erase_eq_sub, Finset.filter_ne', real_inner_self_eq_norm_mul_norm, dist_eq_norm_vsub, Finset.sum_neg_distrib, sub_neg_eq_add
-- 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)
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
⊢ (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:
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]

Premises used: Affine.Simplex.height, Affine.Simplex.ne_altitudeFoot, mul_eq_zero, ne_eq, add_sub_cancel, dist_eq_zero, or_self, not_false_eq_true, one_mul, div_self
-- 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.{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
-- 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.{u_1 + 1} (α := V) (∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i)) 0
⊢ (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

Premises used: Affine.Simplex.points, Affine.Simplex.height, Real, HMul.hMul, Inner.inner, VSub.vsub, Inv.inv, 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
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⟫
⊢ ∑ 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

Premises used: Finset.mul_sum, inner_sum
-- 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 :
  ∑ 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),
      (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

Premises used: Affine.Simplex.height, inner_zero_right, MulZeroClass.mul_zero, inner_smul_right
-- 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 (α := ℝ)
    (∑ 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),
      (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:
h
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
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
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⟫)
⊢ 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:
convert! h using 2 with j
-- 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 (α := ℝ)
    (∑ 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
j : Fin (n + 1)
h_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:
ring
-- 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 :
  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)⁻¹)
⊢ (s.height i)⁻¹ < ∑ j : Fin (n + 1) with j ≠ i, (s.height j)⁻¹

Tactic:
rw [inv_height_eq_sum_mul_inv_dist]

Premises used: Affine.Simplex.inv_height_eq_sum_mul_inv_dist
-- 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)
⊢ 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:
Finset.sum_lt_sum_of_nonempty ?_ ?_

Premises used: Finset.sum_lt_sum_of_nonempty
-- 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)
refine_1 : Finset.Nonempty (α := Fin (n + 1)) {k : Fin (n + 1) | k ≠ i}
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)⁻¹
⊢ 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:
refine Finset.sum_lt_sum_of_nonempty ?_ ?_

Premises used: Finset.sum_lt_sum_of_nonempty
-- 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)
refine_1 : #(Finset.erase Finset.univ i) ≠ 0
⊢ Finset.Nonempty (α := Fin (n + 1)) {k : Fin (n + 1) | k ≠ i}

Tactic:
rw [Finset.filter_ne', ← Finset.card_ne_zero]

Premises used: Finset.filter_ne', Finset.card_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
refine_1 : n ≠ 0
⊢ #(Finset.erase Finset.univ i) ≠ 0

Tactic:
simp only [Finset.mem_univ, Finset.card_erase_of_mem, Finset.card_univ, Fintype.card_fin,
      add_tsub_cancel_right]

Premises used: Finset.mem_univ, Finset.card_univ, Fintype.card_fin, Finset.card_erase_of_mem, add_tsub_cancel_right
-- 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)
⊢ n ≠ 0

Tactic:
NeZero.ne _

Premises used: NeZero.ne
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
⊢ n ≠ 0

Tactic:
exact NeZero.ne _

Premises used: NeZero.ne
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
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)⁻¹

Tactic:
mul_lt_of_lt_one_left ?_ ?_

Premises used: mul_lt_of_lt_one_left
-- 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)
hj : Membership.mem (γ := Finset (Fin (n + 1))) {k : Fin (n + 1) | k ≠ i} j
refine_2 : 0 < (s.height j)⁻¹
refine_2₁ : -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) < 1
⊢ -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) * (s.height j)⁻¹ <
    (s.height j)⁻¹

Tactic:
refine mul_lt_of_lt_one_left ?_ ?_

Premises used: mul_lt_of_lt_one_left
-- 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)
hj : Membership.mem (γ := Finset (Fin (n + 1))) {k : Fin (n + 1) | k ≠ i} j
⊢ 0 < (s.height j)⁻¹

Tactic:
simp [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
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 : -1 < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)
⊢ -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) < 1

Tactic:
rw [neg_lt]

Premises used: neg_lt
-- 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)
hj : Membership.mem (γ := Finset (Fin (n + 1))) {k : Fin (n + 1) | k ≠ i} j
⊢ -1 < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)

Tactic:
neg_one_lt_inner_vsub_altitudeFoot_div _ _ _

Premises used: Affine.Simplex.neg_one_lt_inner_vsub_altitudeFoot_div
-- 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)
hj : Membership.mem (γ := Finset (Fin (n + 1))) {k : Fin (n + 1) | k ≠ i} j
⊢ -1 < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)

Tactic:
exact neg_one_lt_inner_vsub_altitudeFoot_div _ _ _

Premises used: Affine.Simplex.neg_one_lt_inner_vsub_altitudeFoot_div
-- 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 : 0 < s.excenterWeightsUnnorm {i} i + ∑ i_1 ∈ {i}ᶜ, s.excenterWeightsUnnorm {i} i_1
⊢ LT.lt (α := ℝ) 0 (∑ j : Fin (n + 1), s.excenterWeightsUnnorm {i} j)

Tactic:
rw [← Finset.sum_add_sum_compl {i}, Finset.sum_singleton]

Premises used: Finset.sum_singleton, Singleton.singleton, Finset.sum_add_sum_compl
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
simp : (s.height i)⁻¹ < ∑ i_1 ∈ {i}ᶜ, s.excenterWeightsUnnorm {i} i_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

Tactic:
simp only [Finset.mem_singleton, ↓reduceIte, neg_mul, one_mul, lt_neg_add_iff_add_lt, add_zero]

Premises used: Finset.mem_singleton, lt_neg_add_iff_add_lt, reduceIte, neg_mul, add_zero, one_mul
-- 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)
⊢ (s.height i)⁻¹ < ∑ j : Fin (n + 1) with j ≠ i, (s.height j)⁻¹

Tactic:
s.inv_height_lt_sum_inv_height i

Premises used: Affine.Simplex.inv_height_lt_sum_inv_height
-- 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)
h : Eq (α := Finset (Fin (n + 1))) {i}ᶜ {k : Fin (n + 1) | k ≠ i}
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)⁻¹
⊢ (s.height i)⁻¹ < ∑ i_1 ∈ {i}ᶜ, s.excenterWeightsUnnorm {i} i_1

Tactic:
convert! s.inv_height_lt_sum_inv_height i using 2 with j h

Premises used: Affine.Simplex.inv_height_lt_sum_inv_height
-- 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)
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
⊢ Eq (α := Finset (Fin (n + 1))) {i}ᶜ {k : Fin (n + 1) | k ≠ i}

Tactic:
ext j
-- 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)
⊢ Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ j ↔
    Membership.mem (γ := Finset (Fin (n + 1))) {k : Fin (n + 1) | k ≠ i} j

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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) {k : Fin (n + 1) | k ≠ i} j
⊢ j ≠ i

Tactic:
rw [Finset.mem_filter_univ] at h

Premises used: Finset.mem_filter_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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
h : j ≠ i
⊢ s.excenterWeightsUnnorm {i} j = (s.height j)⁻¹

Tactic:
simp [excenterWeightsUnnorm, h]

Premises used: Affine.Simplex.excenterWeightsUnnorm
-- 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)
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
⊢ Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} i) : SignType) (-1 : SignType)

Tactic:
simp_rw [excenterWeights, Pi.smul_apply, smul_eq_mul, sign_mul]

Premises used: sign_mul, Affine.Simplex.excenterWeights, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
⊢ HMul.hMul (α := SignType) (β := SignType) (1 : SignType)
      ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} i) : SignType) =
    (SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} i)

Tactic:
one_mul _

Premises used: one_mul