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))
⊢ Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights signs i) 1 ↔ s.ExcenterExists signs

Tactic:
classical
  simp [sum_excenterWeights]

Premises used: Affine.Simplex.sum_excenterWeights
-- 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
simp_rw : LT.lt (α := ℝ) 0 (∑ x : Fin (n + 1), (s.height x)⁻¹)
⊢ LT.lt (α := ℝ) 0 (∑ i : Fin (n + 1), s.excenterWeightsUnnorm ∅ i)

Tactic:
simp_rw [excenterWeightsUnnorm_empty_apply]

Premises used: Affine.Simplex.excenterWeightsUnnorm_empty_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
⊢ LT.lt (α := ℝ) 0 (∑ x : Fin (n + 1), (s.height x)⁻¹)

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
simp : 0 < (∑ x : Fin (n + 1), (s.height x)⁻¹)⁻¹ * (s.height i)⁻¹
⊢ 0 < s.excenterWeights ∅ i

Tactic:
simp only [excenterWeights, excenterWeightsUnnorm_empty_apply, Pi.smul_apply, smul_eq_mul]

Premises used: Affine.Simplex.excenterWeightsUnnorm_empty_apply, 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
i : Fin (n + 1)
⊢ 0 < (∑ x : Fin (n + 1), (s.height x)⁻¹)⁻¹ * (s.height i)⁻¹

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Incenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
rw : 0 < s.excenterWeights ∅ i
⊢ Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights ∅ i) : SignType) (1 : SignType)

Tactic:
rw [sign_eq_one_iff]

Premises used: 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
i : Fin (n + 1)
⊢ 0 < s.excenterWeights ∅ i

Tactic:
s.excenterWeights_empty_pos i

Premises used: Affine.Simplex.excenterWeights_empty_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)
⊢ 0 < s.excenterWeights ∅ i

Tactic:
exact s.excenterWeights_empty_pos i

Premises used: Affine.Simplex.excenterWeights_empty_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
⊢ s.ExcenterExists ∅

Tactic:
s.sum_excenterWeightsUnnorm_empty_pos.ne'

Premises used: Affine.Simplex.ExcenterExists, LT.lt.ne', Affine.Simplex.sum_excenterWeightsUnnorm_empty_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
this :
  ∀ (i : Fin (n + 1)),
    i ≠ 0 →
      Eq (α := ℝ)
        (∑ j : Fin (n + 1),
          ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height j)⁻¹ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫)
        0
rw :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points) ⊓ (vectorSpan ℝ (Set.range s.points))ᗮ)
    (∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i))
⊢ Eq.{u_1 + 1} (α := V) (∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i)) 0

Tactic:
rw [← Submodule.mem_bot ℝ,
      ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]

Premises used: Affine.Simplex.points, Real, vectorSpan, Submodule.mem_bot, Submodule.inf_orthogonal_eq_bot, Set.range
-- 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
this :
  ∀ (i : Fin (n + 1)),
    i ≠ 0 →
      Eq (α := ℝ)
        (∑ j : Fin (n + 1),
          ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height j)⁻¹ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫)
        0
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points) ⊓ (vectorSpan ℝ (Set.range s.points))ᗮ)
    (∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i))

Tactic:
⟨Submodule.sum_smul_mem _ _ fun i hi ↦
              vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
                (mem_affineSpan _ (Set.mem_range_self _))
                (altitudeFoot_mem_affineSpan  _ _),
            ?_⟩

Premises used: Set.mem_range_self, Real, Submodule.sum_smul_mem, Set.Mem, setOf, Affine.Simplex.altitudeFoot_mem_affineSpan, mem_affineSpan, Set.inter, And.intro, vsub_mem_vectorSpan_of_mem_affineSpan_of_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
this :
  ∀ (i : Fin (n + 1)),
    i ≠ 0 →
      Eq (α := ℝ)
        (∑ j : Fin (n + 1),
          ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height j)⁻¹ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫)
        0
refine :
  ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i) ∈
    (↑(vectorSpan ℝ (Set.range s.points))ᗮ : Set V)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points) ⊓ (vectorSpan ℝ (Set.range s.points))ᗮ)
    (∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i))

Tactic:
refine ⟨Submodule.sum_smul_mem _ _ fun i hi ↦
              vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
                (mem_affineSpan _ (Set.mem_range_self _))
                (altitudeFoot_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
this :
  ∀ (i : Fin (n + 1)),
    i ≠ 0 →
      Eq (α := ℝ)
        (∑ j : Fin (n + 1),
          ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height j)⁻¹ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫)
        0
rw :
  ∀ (i : { x : Fin (n + 1) // x ≠ 0 }),
    ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i) ∈
      (↑(ℝ ∙ (s.points (↑i : Fin (n + 1)) -ᵥ s.points 0))ᗮ : Set V)
⊢ ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i) ∈
    (↑(vectorSpan ℝ (Set.range s.points))ᗮ : Set V)

Tactic:
rw [vectorSpan_range_eq_span_range_vsub_right_ne _ _ 0, Submodule.span_range_eq_iSup,
      ← Submodule.iInf_orthogonal, Submodule.coe_iInf, Set.mem_iInter]

Premises used: Submodule.span_range_eq_iSup, Set.mem_iInter, Submodule.coe_iInf, vectorSpan_range_eq_span_range_vsub_right_ne, Submodule.iInf_orthogonal, OfNat.ofNat
-- 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
this :
  ∀ (i : Fin (n + 1)),
    i ≠ 0 →
      Eq (α := ℝ)
        (∑ j : Fin (n + 1),
          ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height j)⁻¹ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫)
        0
i : { x : Fin (n + 1) // x ≠ 0 }
rcases :
  ∀ (i : Fin (n + 1)) (hi : i ≠ 0),
    ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i) ∈
      (↑(ℝ ∙ (s.points (↑(Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ≠ 0) i hi) : Fin (n + 1)) -ᵥ s.points 0))ᗮ : Set V)
⊢ ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i) ∈
    (↑(ℝ ∙ (s.points (↑i : Fin (n + 1)) -ᵥ s.points 0))ᗮ : Set V)

Tactic:
rcases i with ⟨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
this :
  ∀ (i : Fin (n + 1)),
    i ≠ 0 →
      Eq (α := ℝ)
        (∑ j : Fin (n + 1),
          ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height j)⁻¹ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫)
        0
i : Fin (n + 1)
hi : i ≠ 0
⊢ ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i) ∈
    (↑(ℝ ∙ (s.points (↑(Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ≠ 0) i hi) : Fin (n + 1)) -ᵥ s.points 0))ᗮ : Set V)

Tactic:
simpa only [SetLike.mem_coe, Submodule.mem_orthogonal_singleton_iff_inner_right, inner_sum]
      using this i hi

Premises used: inner_sum, Submodule.mem_orthogonal_singleton_iff_inner_right, SetLike.mem_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
suffices :
  ∀ (i : Fin (n + 1)),
    i ≠ 0 →
      Eq (α := ℝ)
        (∑ j : Fin (n + 1),
          ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height j)⁻¹ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫)
        0
⊢ Eq.{u_1 + 1} (α := V) (∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (s.height i)⁻¹ 2 • (s.points i -ᵥ s.altitudeFoot i)) 0

Tactic:
suffices ∀ i, i ≠ 0 →
      ∑ j, ⟪s.points i -ᵥ s.points 0, (s.height j)⁻¹ ^ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫ = 0 by
    rw [← Submodule.mem_bot ℝ,
      ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]
    refine ⟨Submodule.sum_smul_mem _ _ fun i hi ↦
              vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
                (mem_affineSpan _ (Set.mem_range_self _))
                (altitudeFoot_mem_affineSpan  _ _),
            ?_⟩
    rw [vectorSpan_range_eq_span_range_vsub_right_ne _ _ 0, Submodule.span_range_eq_iSup,
      ← Submodule.iInf_orthogonal, Submodule.coe_iInf, Set.mem_iInter]
    intro i
    rcases i with ⟨i, hi⟩
    simpa only [SetLike.mem_coe, Submodule.mem_orthogonal_singleton_iff_inner_right, inner_sum]
      using this 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
i : Fin (n + 1)
hi : i ≠ 0
rw :
  ⟪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)⟫ +
      ∑ x ∈ Finset.erase (Finset.erase Finset.univ 0) i,
        ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height x)⁻¹ 2 • (s.points x -ᵥ s.altitudeFoot x)⟫ =
    0
⊢ Eq (α := ℝ)
    (∑ j : Fin (n + 1),
      ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height j)⁻¹ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫)
    0

Tactic:
rw [← Finset.add_sum_erase _ _ (Finset.mem_univ 0),
    ← Finset.add_sum_erase _ _ (Finset.mem_erase.2 ⟨hi, Finset.mem_univ _⟩), ← add_assoc]

Premises used: Iff.mpr, Finset.mem_univ, add_assoc, Finset.add_sum_erase, Finset.mem_erase, And.intro, OfNat.ofNat
-- 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
⊢ ⟪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)⟫ +
      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:
add_zero _

Premises used: add_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)
hi : i ≠ 0
h :
  Eq (α := ℝ)
    (∑ x ∈ Finset.erase (Finset.erase Finset.univ 0) i,
      ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height x)⁻¹ 2 • (s.points x -ᵥ s.altitudeFoot x)⟫)
    0
h₁ :
  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)⟫
⊢ ⟪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)⟫ +
      ∑ x ∈ Finset.erase (Finset.erase Finset.univ 0) i,
        ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height x)⁻¹ 2 • (s.points x -ᵥ s.altitudeFoot x)⟫ =
    0

Tactic:
convert! add_zero _

Premises used: add_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)
hi : i ≠ 0
⊢ Eq (α := ℝ) (∑ _x ∈ Finset.erase (Finset.erase Finset.univ 0) i, 0) 0

Tactic:
Finset.sum_const_zero

Premises used: Finset.sum_const_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)
hi : i ≠ 0
h :
  ∀ (j : Fin (n + 1)) (hj : j ∈ Finset.erase (Finset.erase Finset.univ 0) i),
    ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height j)⁻¹ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫ = 0
⊢ Eq (α := ℝ)
    (∑ x ∈ Finset.erase (Finset.erase Finset.univ 0) i,
      ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height x)⁻¹ 2 • (s.points x -ᵥ s.altitudeFoot x)⟫)
    0

Tactic:
convert! Finset.sum_const_zero with j hj

Premises used: Finset.sum_const_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)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ Finset.erase (Finset.erase Finset.univ 0) i
h : HPow.hPow (β := ℕ) (s.height j)⁻¹ 2 * ⟪s.points i -ᵥ s.points 0, s.points j -ᵥ s.altitudeFoot j⟫ = 0
⊢ ⟪s.points i -ᵥ s.points 0, HPow.hPow (β := ℕ) (s.height j)⁻¹ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫ = 0

Tactic:
rw [real_inner_smul_right]

Premises used: real_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)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ Finset.erase (Finset.erase Finset.univ 0) i
⊢ HPow.hPow (β := ℕ) (s.height j)⁻¹ 2 * 0 = 0

Tactic:
mul_zero _

Premises used: MulZeroClass.mul_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)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ Finset.erase (Finset.erase Finset.univ 0) i
h : ⟪s.points i -ᵥ s.points 0, s.points j -ᵥ s.altitudeFoot j⟫ = 0
⊢ HPow.hPow (β := ℕ) (s.height j)⁻¹ 2 * ⟪s.points i -ᵥ s.points 0, s.points j -ᵥ s.altitudeFoot j⟫ = 0

Tactic:
convert! mul_zero _

Premises used: MulZeroClass.mul_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)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ Finset.erase (Finset.erase Finset.univ 0) i
h : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i -ᵥ s.points 0))ᗮ (s.points j -ᵥ s.altitudeFoot j)
⊢ ⟪s.points i -ᵥ s.points 0, s.points j -ᵥ s.altitudeFoot j⟫ = 0

Tactic:
rw [← Submodule.mem_orthogonal_singleton_iff_inner_right]

Premises used: Submodule.mem_orthogonal_singleton_iff_inner_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)
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)

Tactic:
SetLike.le_def.1 (Submodule.orthogonal_le ?_)
      (vsub_orthogonalProjection_mem_direction_orthogonal _ _)

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, SetLike.le_def, Iff.mp, Submodule.orthogonal_le
-- 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
j : Fin (n + 1)
hj : j ∈ Finset.erase (Finset.erase Finset.univ 0) i
h :
  LE.le (α := Submodule ℝ V) (ℝ ∙ (s.points i -ᵥ s.points 0))
    (AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite j).points)))
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i -ᵥ s.points 0))ᗮ (s.points j -ᵥ s.altitudeFoot j)

Tactic:
refine SetLike.le_def.1 (Submodule.orthogonal_le ?_)
      (vsub_orthogonalProjection_mem_direction_orthogonal _ _)

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, SetLike.le_def, Iff.mp, Submodule.orthogonal_le
-- 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
j : Fin (n + 1)
hj : j ∈ Finset.erase (Finset.erase Finset.univ 0) i
h : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points)) (s.points i -ᵥ s.points 0)
⊢ LE.le (α := Submodule ℝ V) (ℝ ∙ (s.points i -ᵥ s.points 0))
    (AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite j).points)))

Tactic:
rw [Submodule.span_singleton_le_iff_mem, direction_affineSpan]

Premises used: direction_affineSpan, Submodule.span_singleton_le_iff_mem
-- 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
j : Fin (n + 1)
hj : j ∈ Finset.erase (Finset.erase Finset.univ 0) i
⊢ j ≠ i ∧ j ≠ 0

Tactic:
simp only [Finset.mem_erase, Finset.mem_univ, and_true] at hj

Premises used: Finset.mem_univ, and_true, Finset.mem_erase
-- 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
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)

Tactic:
vsub_mem_vectorSpan _ ?_ ?_

Premises used: vsub_mem_vectorSpan, Set.Mem
-- 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
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
h : s.points i ∈ Set.range (s.faceOpposite j).points
h₁ : s.points 0 ∈ Set.range (s.faceOpposite j).points
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points)) (s.points i -ᵥ s.points 0)

Tactic:
refine vsub_mem_vectorSpan _ ?_ ?_

Premises used: vsub_mem_vectorSpan
-- 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
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
h : ∃ (x : Fin (n + 1)), Membership.mem (γ := Set (Fin (n + 1))) {j}ᶜ x ∧ s.points x = s.points i
⊢ s.points i ∈ Set.range (s.faceOpposite j).points

Tactic:
simp only [range_faceOpposite_points, Set.mem_image]

Premises used: Set.mem_image, Affine.Simplex.range_faceOpposite_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
i : Fin (n + 1)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
h : ∃ (x : Fin (n + 1)), Membership.mem (γ := Set (Fin (n + 1))) {j}ᶜ x ∧ s.points x = s.points 0
⊢ s.points 0 ∈ Set.range (s.faceOpposite j).points

Tactic:
simp only [range_faceOpposite_points, Set.mem_image]

Premises used: Set.mem_image, Affine.Simplex.range_faceOpposite_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
i : Fin (n + 1)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
⊢ ∃ (x : Fin (n + 1)), Membership.mem (γ := Set (Fin (n + 1))) {j}ᶜ x ∧ s.points x = s.points i

Tactic:
⟨i, hj.1.symm, rfl⟩

Premises used: Ne.symm, And.left, And.intro, Exists.intro, rfl
-- 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
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
⊢ ∃ (x : Fin (n + 1)), Membership.mem (γ := Set (Fin (n + 1))) {j}ᶜ x ∧ s.points x = s.points i

Tactic:
exact ⟨i, hj.1.symm, rfl⟩
-- 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
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
⊢ ∃ (x : Fin (n + 1)), Membership.mem (γ := Set (Fin (n + 1))) {j}ᶜ x ∧ s.points x = s.points 0

Tactic:
⟨0, hj.2.symm, rfl⟩

Premises used: Ne.symm, And.right, And.intro, Exists.intro, OfNat.ofNat, rfl
-- 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
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
⊢ ∃ (x : Fin (n + 1)), Membership.mem (γ := Set (Fin (n + 1))) {j}ᶜ x ∧ s.points x = s.points 0

Tactic:
exact ⟨0, hj.2.symm, rfl⟩