awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
rw : Fintype.card (Fin (n + 1)) - card (α := Fin (n + 1)) {i} = n - 1 + 1
rw₁ : Fintype.card (Fin (n + 1)) - 1 = n - 1 + 1
rw₂ : n + 1 - 1 = n - 1 + 1
rw₃ : n + 1 - 1 = n
⊢ card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
have rw₄ : n = n
Tactic: rw [card_compl, card_singleton, Fintype.card_fin, hn, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
⊢ finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = 1
have hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
Tactic: have hc : #({i}ᶜ) = (n - 1) + 1 := by
    rw [card_compl, card_singleton, Fintype.card_fin, hn, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
⊢ finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = 1
have refine : finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
Tactic: refine add_left_cancel (_root_.trans h ?_)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
have rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
Tactic: rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
have rw₁ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i} : Set (Fin (n + 1)))ᶜ)) + 1
Tactic: rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
rw₁ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i} : Set (Fin (n + 1)))ᶜ)) + 1
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
have rw₂ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i}ᶜ : Set (Fin (n + 1))))) + 1
Tactic: rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
rw₁ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i} : Set (Fin (n + 1)))ᶜ)) + 1
rw₂ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i}ᶜ : Set (Fin (n + 1))))) + 1
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
have rw₃ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (↑(image s.points {i}ᶜ) : Set P)) + 1
Tactic: rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
rw₁ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i} : Set (Fin (n + 1)))ᶜ)) + 1
rw₂ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i}ᶜ : Set (Fin (n + 1))))) + 1
rw₃ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (↑(image s.points {i}ᶜ) : Set P)) + 1
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
have rw₄ : n = n - 1 + 1
Tactic: rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
rw₁ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i} : Set (Fin (n + 1)))ᶜ)) + 1
rw₂ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i}ᶜ : Set (Fin (n + 1))))) + 1
rw₃ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (↑(image s.points {i}ᶜ) : Set P)) + 1
rw₄ : n = n - 1 + 1
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
have rw₅ : n = n
Tactic: rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
have rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
Tactic: classical
  rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
have rw₁ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i} : Set (Fin (n + 1)))ᶜ)) + 1
Tactic: classical
  rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
rw₁ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i} : Set (Fin (n + 1)))ᶜ)) + 1
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
have rw₂ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i}ᶜ : Set (Fin (n + 1))))) + 1
Tactic: classical
  rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
rw₁ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i} : Set (Fin (n + 1)))ᶜ)) + 1
rw₂ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i}ᶜ : Set (Fin (n + 1))))) + 1
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
have rw₃ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (↑(image s.points {i}ᶜ) : Set P)) + 1
Tactic: classical
  rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
rw₁ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i} : Set (Fin (n + 1)))ᶜ)) + 1
rw₂ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i}ᶜ : Set (Fin (n + 1))))) + 1
rw₃ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (↑(image s.points {i}ᶜ) : Set P)) + 1
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
have rw₄ : n = n - 1 + 1
Tactic: classical
  rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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 :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
rw₁ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i} : Set (Fin (n + 1)))ᶜ)) + 1
rw₂ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i}ᶜ : Set (Fin (n + 1))))) + 1
rw₃ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (↑(image s.points {i}ᶜ) : Set P)) + 1
rw₄ : n = n - 1 + 1
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
have rw₅ : n = n
Tactic: classical
  rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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)
p : P
⊢ affineSpan ℝ {p, s.points i} = s.altitude i ↔
    p ≠ s.points i ∧
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p ∧
        Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ (p -ᵥ s.points i)
have rw : vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction ↔
  p ≠ s.points i ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
      Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
Tactic: rw [eq_iff_direction_eq_of_mem (mem_affineSpan ℝ (Set.mem_insert_of_mem _ (Set.mem_singleton _)))
      (s.mem_altitude _),
    ← vsub_right_mem_direction_iff_mem (mem_affineSpan ℝ (Set.mem_range_self i)) p,
    direction_affineSpan, direction_affineSpan, direction_affineSpan]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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)
p : P
⊢ vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction ↔
    p ≠ s.points i ∧
      Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
        Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
have mp : vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction →
  p ≠ s.points i ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
      Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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)
p : P
mp :
  vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction →
    p ≠ s.points i ∧
      Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
        Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
⊢ vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction ↔
    p ≠ s.points i ∧
      Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
        Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
have mpr : p ≠ s.points i ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
      Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i) →
  vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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)
p : P
h : vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
⊢ p ≠ s.points i ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
      Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
have mp : p ≠ s.points i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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)
p : P
h : vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
mp : p ≠ s.points i
⊢ p ≠ s.points i ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
      Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
have mp₁ : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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)
p : P
h : vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
heq : p = s.points i
⊢ False
have h₁ : ⊥ = (s.altitude i).direction
Tactic: rw [heq, Set.pair_eq_singleton, vectorSpan_singleton] at h
Cleared hypotheses: h, heq
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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)
p : P
h : ⊥ = (s.altitude i).direction
heq : p = s.points i
⊢ finrank.{0, u_1} ℝ ↥(s.altitude i).direction = 0
have rw : finrank.{0, u_1} ℝ ↥⊥ = 0
Tactic: rw [← h, finrank_bot]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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)
p : P
h : ⊥ = (s.altitude i).direction
heq : p = s.points i
rw : finrank.{0, u_1} ℝ ↥⊥ = 0
⊢ finrank.{0, u_1} ℝ ↥(s.altitude i).direction = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [← h, finrank_bot]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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)
p : P
h : ⊥ = (s.altitude i).direction
heq : p = s.points i
⊢ False
have hd : finrank.{0, u_1} ℝ ↥(s.altitude i).direction = 0
Tactic: have hd : finrank ℝ (s.altitude i).direction = 0 := by rw [← h, finrank_bot]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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)
p : P
h : vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
have mp : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (P := P) {p, s.points i}) (p -ᵥ s.points i)
Tactic: rw [← Submodule.mem_inf, _root_.inf_comm, ← direction_altitude, ← h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Altitude (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)
p : P
hne : p ≠ s.points i
h :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
⊢ vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
have h₁ : p -ᵥ s.points i ∈ (s.altitude i).direction
Tactic: rw [← Submodule.mem_inf, _root_.inf_comm, ← direction_altitude] at h
Cleared hypotheses: h