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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
h :
  Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
    (1 : SignType)
⊢ 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) (-1 : SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} i) : SignType)
Tactic: convert! one_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)
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
    (1 : SignType)
have h : LT.lt (α := ℝ) 0 (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)
Tactic: rw [sign_eq_one_iff, inv_pos]
-- 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)
h : i ≠ j
⊢ Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} j) : 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} j) : 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 j : Fin (n + 1)
h : i ≠ j
⊢ 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} j) : 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 _
-- 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)
h : i ≠ j
h₁ :
  Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
    (1 : SignType)
⊢ 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} j) : SignType) =
    1
have h₂ : Eq (α := SignType) (1 : SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeightsUnnorm {i} j) : SignType)
Tactic: convert! one_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 j : Fin (n + 1)
h : i ≠ j
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)⁻¹ : SignType)
    (1 : SignType)
have h₁ : LT.lt (α := ℝ) 0 (∑ i_1 : Fin (n + 1), s.excenterWeightsUnnorm {i} i_1)
Tactic: rw [sign_eq_one_iff, inv_pos]
-- 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 : Fin (n + 1)
⊢ (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
have this : (s.height i)⁻¹ < ∑ j : Fin (n + 1) with j ≠ i, (s.height j)⁻¹
Tactic: have := s.inv_height_lt_sum_inv_height 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
this : (s.height i)⁻¹ < ∑ j : Fin (n + 1) with j ≠ i, (s.height j)⁻¹
⊢ (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
have rwa : ∀ (this : (s.height i)⁻¹ < ∑ j ∈ erase univ i, (s.height j)⁻¹),
  (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
Tactic: rwa [filter_ne', ← compl_singleton, ← add_lt_add_iff_left (s.height i)⁻¹] 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
this : (s.height i)⁻¹ < ∑ j : Fin (n + 1) with j ≠ i, (s.height j)⁻¹
rwa :
  ∀ (this : (s.height i)⁻¹ < ∑ j ∈ erase univ i, (s.height j)⁻¹),
    (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
⊢ (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
have rwa₁ : ∀ (this : (s.height i)⁻¹ < ∑ j ∈ {i}ᶜ, (s.height j)⁻¹),
  (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
Tactic: rwa [filter_ne', ← compl_singleton, ← add_lt_add_iff_left (s.height i)⁻¹] 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
this : (s.height i)⁻¹ < ∑ j : Fin (n + 1) with j ≠ i, (s.height j)⁻¹
rwa :
  ∀ (this : (s.height i)⁻¹ < ∑ j ∈ erase univ i, (s.height j)⁻¹),
    (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
rwa₁ :
  ∀ (this : (s.height i)⁻¹ < ∑ j ∈ {i}ᶜ, (s.height j)⁻¹),
    (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
⊢ (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
have rwa₂ : ∀ (this : (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹),
  (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
Tactic: rwa [filter_ne', ← compl_singleton, ← add_lt_add_iff_left (s.height i)⁻¹] at this
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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
⊢ s.excenterWeights ∅ i < 2⁻¹
have h : (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
Tactic: have h : (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹ := by
    have := s.inv_height_lt_sum_inv_height i
    rwa [filter_ne', ← compl_singleton, ← add_lt_add_iff_left (s.height i)⁻¹] at 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
h : (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
⊢ 2 * (s.height i)⁻¹ < HAdd.hAdd (α := ℝ) (∑ j ∈ {i}, (s.height j)⁻¹) (∑ j ∈ {i}ᶜ, (s.height j)⁻¹)
have rwa : (s.height i)⁻¹ + (s.height i)⁻¹ < HAdd.hAdd (α := ℝ) (∑ j ∈ {i}, (s.height j)⁻¹) (∑ j ∈ {i}ᶜ, (s.height j)⁻¹)
Tactic: rwa [two_mul, sum_singleton]
-- 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 : Fin (n + 1)
h : (s.height i)⁻¹ + (s.height i)⁻¹ < (s.height i)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
⊢ s.excenterWeights ∅ i < 2⁻¹
have h₁ : 2 * (s.height i)⁻¹ < HAdd.hAdd (α := ℝ) (∑ j ∈ {i}, (s.height j)⁻¹) (∑ j ∈ {i}ᶜ, (s.height j)⁻¹)
Tactic: replace h : 2 * (s.height i)⁻¹ < ∑ j ∈ {i}, (s.height j)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹ := by
    rwa [two_mul, sum_singleton]
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)
h : 2 * (s.height i)⁻¹ < HAdd.hAdd (α := ℝ) (∑ j ∈ {i}, (s.height j)⁻¹) (∑ j ∈ {i}ᶜ, (s.height j)⁻¹)
⊢ (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
have rwa : ∀ (h : 2 * (s.height i)⁻¹ < ∑ i : Fin (n + 1), (s.height i)⁻¹), (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
Tactic: rwa [sum_add_sum_compl, ← lt_inv_mul_iff₀ zero_lt_two, ← div_lt_iff₀ (by positivity)] 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)
h : 2 * (s.height i)⁻¹ < HAdd.hAdd (α := ℝ) (∑ j ∈ {i}, (s.height j)⁻¹) (∑ j ∈ {i}ᶜ, (s.height j)⁻¹)
rwa :
  ∀ (h : 2 * (s.height i)⁻¹ < ∑ i : Fin (n + 1), (s.height i)⁻¹),
    (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
⊢ (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
have rwa₁ : ∀ (h : (s.height i)⁻¹ < HMul.hMul (α := ℝ) 2⁻¹ (∑ i : Fin (n + 1), (s.height i)⁻¹)),
  (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
Tactic: rwa [sum_add_sum_compl, ← lt_inv_mul_iff₀ zero_lt_two, ← div_lt_iff₀ (by positivity)] 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)
h : 2 * (s.height i)⁻¹ < HAdd.hAdd (α := ℝ) (∑ j ∈ {i}, (s.height j)⁻¹) (∑ j ∈ {i}ᶜ, (s.height j)⁻¹)
rwa :
  ∀ (h : 2 * (s.height i)⁻¹ < ∑ i : Fin (n + 1), (s.height i)⁻¹),
    (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
rwa₁ :
  ∀ (h : (s.height i)⁻¹ < HMul.hMul (α := ℝ) 2⁻¹ (∑ i : Fin (n + 1), (s.height i)⁻¹)),
    (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
⊢ (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
have rwa₂ : ∀ (h : (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹),
  (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
Tactic: rwa [sum_add_sum_compl, ← lt_inv_mul_iff₀ zero_lt_two, ← div_lt_iff₀ (by positivity)] 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
h : 2 * (s.height i)⁻¹ < HAdd.hAdd (α := ℝ) (∑ j ∈ {i}, (s.height j)⁻¹) (∑ j ∈ {i}ᶜ, (s.height j)⁻¹)
⊢ s.excenterWeights ∅ i < 2⁻¹
have h₁ : (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
Tactic: replace h : (s.height i)⁻¹ / ∑ i, (s.height i)⁻¹ < 2⁻¹ := by
    rwa [sum_add_sum_compl, ← lt_inv_mul_iff₀ zero_lt_two, ← div_lt_iff₀ (by positivity)] 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)
h : (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹ < 2⁻¹
⊢ s.excenterWeights ∅ i < 2⁻¹
have h₁ : s.excenterWeights ∅ i = (s.height i)⁻¹ / ∑ i : Fin (n + 1), (s.height i)⁻¹
Tactic: convert! 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
⊢ (s.reindex e).exsphere signs = s.exsphere (Finset.map e.symm.toEmbedding signs)
have simp_rw : Eq.{u_2 + 1} (α := Sphere P)
  ({
      center :=
        (Finset.affineCombination ℝ (Finset.map e.symm.toEmbedding Finset.univ) s.points : (a : Fin (n + 1) → ℝ) → P)
          (s.excenterWeights (Finset.map e.symm.toEmbedding signs)),
      radius :=
        |((Finset.map e.symm.toEmbedding Finset.univ).sum
              (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)))⁻¹| } :
    Sphere P)
  ({
      center :=
        (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
          (s.excenterWeights (Finset.map e.symm.toEmbedding signs)),
      radius := |(∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i)⁻¹| } :
    Sphere P)
Tactic: simp_rw [exsphere, excenterWeightsUnnorm_reindex, excenterWeights_reindex, Finset.sum_comp_equiv,
    reindex, ← Equiv.coe_toEmbedding, ← Finset.affineCombination_map]
-- 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).insphere = s.insphere
have simp_rw : s.exsphere (Finset.map e.symm.toEmbedding ∅) = s.exsphere ∅
Tactic: simp_rw [insphere, exsphere_reindex]
-- 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ (↑((s.restrict S hS).excenter signs) : P) = s.excenter signs
have h₁ : ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) signs
Tactic: rw [← s.excenterExists_restrict S hS] 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
signs : Finset (Fin (n + 1))
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) signs
⊢ (↑((s.restrict S hS).excenter signs) : P) = s.excenter signs
have this : Nonempty.{u_2 + 1} ↥S
Tactic: haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).incenter = s.incenter
have simp_rw : (s.exsphere (Finset.map e.symm.toEmbedding ∅)).center = (s.exsphere ∅).center
Tactic: simp_rw [incenter, exsphere_reindex]
-- 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).exradius = s.exradius
have h : ∀ (x : Finset (Fin (n + 1))), (s.map f.toAffineMap sorry).exradius x = s.exradius x
Tactic: ext
-- 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ exradius.{u_1, u_2} (P := ↥S) (s.restrict S hS) = s.exradius
have h : ∀ (x : Finset (Fin (n + 1))), exradius.{u_1, u_2} (P := ↥S) (s.restrict S hS) x = s.exradius x
Tactic: ext
-- 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).inradius = s.inradius
have simp_rw : (s.exsphere (Finset.map e.symm.toEmbedding ∅)).radius = (s.exsphere ∅).radius
Tactic: simp_rw [inradius, exsphere_reindex]
-- 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
⊢ s.exsphere Finset.univ = s.insphere
have rw : s.exsphere ∅ᶜ = s.insphere
Tactic: rw [← Finset.compl_empty, exsphere_compl, insphere]
-- 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
rw : s.exsphere ∅ᶜ = s.insphere
⊢ s.exsphere Finset.univ = s.insphere
have rw₁ : s.exsphere ∅ = s.insphere
Tactic: rw [← Finset.compl_empty, exsphere_compl, insphere]
-- 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
rw : s.exsphere ∅ᶜ = s.insphere
rw₁ : s.exsphere ∅ = s.insphere
⊢ s.exsphere Finset.univ = s.insphere
have rw₂ : s.exsphere ∅ = s.exsphere ∅
Tactic: rw [← Finset.compl_empty, exsphere_compl, insphere]
-- 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
⊢ s.excenter Finset.univ = s.incenter
have rw : (s.exsphere Finset.univ).center = s.incenter
Tactic: rw [excenter, exsphere_univ, insphere_center]
-- 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
rw : (s.exsphere Finset.univ).center = s.incenter
⊢ s.excenter Finset.univ = s.incenter
have rw₁ : s.insphere.center = s.incenter
Tactic: rw [excenter, exsphere_univ, insphere_center]
-- 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
rw : (s.exsphere Finset.univ).center = s.incenter
rw₁ : s.insphere.center = s.incenter
⊢ s.excenter Finset.univ = s.incenter
have rw₂ : s.incenter = s.incenter
Tactic: rw [excenter, exsphere_univ, insphere_center]
-- 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
⊢ s.exradius Finset.univ = s.inradius
have rw : (s.exsphere Finset.univ).radius = s.inradius
Tactic: rw [exradius, exsphere_univ, insphere_radius]
-- 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
rw : (s.exsphere Finset.univ).radius = s.inradius
⊢ s.exradius Finset.univ = s.inradius
have rw₁ : s.insphere.radius = s.inradius
Tactic: rw [exradius, exsphere_univ, insphere_radius]
-- 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
rw : (s.exsphere Finset.univ).radius = s.inradius
rw₁ : s.insphere.radius = s.inradius
⊢ s.exradius Finset.univ = s.inradius
have rw₂ : s.inradius = s.inradius
Tactic: rw [exradius, exsphere_univ, insphere_radius]
-- 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
⊢ s.incenter ∈ s.interior
have h : Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights ∅ i) 1
Tactic: have h := s.excenterExists_empty.sum_excenterWeights_eq_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
h : Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights ∅ i) 1
⊢ s.incenter ∈ s.interior
have rw : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (s.excenterWeights ∅ i)
Tactic: rw [incenter_eq_affineCombination, s.affineCombination_mem_interior_iff 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
h : Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights ∅ i) 1
i : Fin (n + 1)
⊢ Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (s.excenterWeights ∅ i)
have refine : s.excenterWeights ∅ i < 1
Tactic: refine ⟨s.excenterWeights_empty_pos 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
h : Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights ∅ i) 1
i : Fin (n + 1)
⊢ s.excenterWeights ∅ i < 1
have by_contra! : ∀ (hp : 1 ≤ s.excenterWeights ∅ i), False
Tactic: by_contra! 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
h : Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights ∅ i) 1
i : Fin (n + 1)
hp : 1 ≤ s.excenterWeights ∅ i
⊢ False
have obtain : ∀ (j : Fin (n + 1)) (hj : j ≠ i), False
Tactic: obtain ⟨j, hj⟩ := exists_ne i