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)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
have mpr : ℝ ∙ (p -ᵥ s.points i) = (s.altitude i).direction
Tactic: rw [vectorSpan_eq_span_vsub_set_left_ne ℝ (Set.mem_insert _ _),
      Set.insert_diff_of_mem _ (Set.mem_singleton _),
      Set.diff_singleton_eq_self fun h => hne (Set.mem_singleton_iff.1 h), Set.image_singleton]
-- 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
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ ℝ ∙ (p -ᵥ s.points i) = (s.altitude i).direction
have mpr : ℝ ∙ (p -ᵥ s.points i) ≤ (s.altitude i).direction
Tactic: refine Submodule.eq_of_le_of_finrank_eq ?_ ?_
-- 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
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
mpr : ℝ ∙ (p -ᵥ s.points i) ≤ (s.altitude i).direction
⊢ ℝ ∙ (p -ᵥ s.points i) = (s.altitude i).direction
have mpr₁ : finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.points i)) = finrank.{0, u_1} ℝ ↥(s.altitude i).direction
Tactic: refine Submodule.eq_of_le_of_finrank_eq ?_ ?_
-- 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
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ ℝ ∙ (p -ᵥ s.points i) ≤ (s.altitude i).direction
have mpr : {p -ᵥ s.points i} ⊆ (↑(s.altitude i).direction : Set V)
Tactic: rw [Submodule.span_le]
-- 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
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.points i)) = finrank.{0, u_1} ℝ ↥(s.altitude i).direction
have mpr : card (α := V) (Set.toFinset {p -ᵥ s.points i}) = 1
Tactic: rw [finrank_direction_altitude, finrank_span_set_eq_card]
-- 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
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
mpr : card (α := V) (Set.toFinset {p -ᵥ s.points i}) = 1
⊢ finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.points i)) = finrank.{0, u_1} ℝ ↥(s.altitude i).direction
have mpr₁ : LinearIndepOn (ι := V) ℝ id {p -ᵥ s.points i}
Tactic: rw [finrank_direction_altitude, finrank_span_set_eq_card]
-- 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).altitudeFoot = s.altitudeFoot ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
have h : ∀ (i : Fin (m + 1)), (s.reindex e).altitudeFoot i = (s.altitudeFoot ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
Tactic: ext i
-- 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
i : Fin (m + 1)
⊢ (s.reindex e).altitudeFoot i = (s.altitudeFoot ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
have h : Eq.{u_2 + 1} (α := P)
  (↑((((s.reindex e).faceOpposite i).orthogonalProjectionSpan :
          (a : P) → ↥(affineSpan ℝ (Set.range ((s.reindex e).faceOpposite i).points)))
        (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i))) :
    P)
  (↑(((s.faceOpposite ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)).orthogonalProjectionSpan :
          (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)).points)))
        (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i))) :
    P)
Tactic: simp only [altitudeFoot, reindex_points, Function.comp_apply]
-- 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ (↑((s.restrict S hS).altitudeFoot i) : P) = s.altitudeFoot i
have rw : s.altitudeFoot i = (↑((s.restrict S hS).altitudeFoot i) : P)
Tactic: rw [eq_comm]
-- 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 : s.points i = s.altitudeFoot i
⊢ False
have h₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i)
Tactic: rw [eq_comm, altitudeFoot, orthogonalProjectionSpan, orthogonalProjection_eq_self_iff] at h
Cleared hypotheses: 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)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' {i}ᶜ)) (s.altitudeFoot i)
have rw : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.altitudeFoot i)
Tactic: rw [← range_faceOpposite_points]
-- 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)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.altitudeFoot i)
have refine : Set.range (s.faceOpposite i).points ⊆ Set.range s.points
Tactic: refine SetLike.le_def.1 (affineSpan_mono _ ?_) (s.altitudeFoot_mem_affineSpan_faceOpposite _)
-- 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)
⊢ affineSpan ℝ {s.altitudeFoot i, s.points i} = s.altitude i
have rw : s.altitudeFoot i ≠ s.points i ∧
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.altitudeFoot i) ∧
    Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ (s.altitudeFoot i -ᵥ s.points i)
Tactic: rw [affineSpan_pair_eq_altitude_iff]
-- 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)
⊢ s.altitudeFoot i ≠ s.points i ∧
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.altitudeFoot i) ∧
      Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ
        (s.altitudeFoot i -ᵥ s.points i)
have refine : Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ (s.altitudeFoot i -ᵥ s.points i)
Tactic: refine ⟨(s.ne_altitudeFoot i).symm, s.altitudeFoot_mem_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)
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ (s.altitudeFoot i -ᵥ s.points i)
have rw : Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ
  ((↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
            (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
          (s.points i)) :
      P) -ᵥ
    s.points i)
Tactic: rw [altitudeFoot, orthogonalProjectionSpan]
-- 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)
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ
    ((↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) :
              (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite i).points)))
            (s.points i)) :
        P) -ᵥ
      s.points i)
have simp_rw : Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ
  ((↑((orthogonalProjection (affineSpan ℝ (s.points '' {i}ᶜ)) : (a : P) → ↥(affineSpan ℝ (s.points '' {i}ᶜ)))
          (s.points i)) :
      P) -ᵥ
    s.points i)
Tactic: simp_rw [range_faceOpposite_points]
-- 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)
⊢ s.altitudeFoot i ∈ s.altitude i
have rw : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {s.altitudeFoot i, s.points i}) (s.altitudeFoot i)
Tactic: rw [← affineSpan_pair_altitudeFoot_eq_altitude]
-- 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).height = s.height ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
have h : ∀ (i : Fin (m + 1)), (s.reindex e).height i = (s.height ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
Tactic: ext i
-- 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ height.{u_1, u_2} (P := ↥S) (s.restrict S hS) i = s.height i
have rw : s.height i = height.{u_1, u_2} (P := ↥S) (s.restrict S hS) i
Tactic: rw [eq_comm]
-- 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
s : Simplex ℝ P 1
i : Fin 2
⊢ s.height i = dist (s.points 0) (s.points 1)
have 0 : s.height ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) = dist (s.points 0) (s.points 1)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
s : Simplex ℝ P 1
i : Fin 2
0 : s.height ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = dist (s.points 0) (s.points 1)
⊢ s.height i = dist (s.points 0) (s.points 1)
have 1 : s.height ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) = dist (s.points 0) (s.points 1)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
s : Simplex ℝ P 1
⊢ s.height ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = dist (s.points 0) (s.points 1)
have 1 : s.height ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) = dist (s.points 1) (s.points 0)
Tactic: rw [dist_comm]
-- 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 : ℕ
s : Simplex ℝ P n
i j : Fin (n + 1)
h : i ≠ j
⊢ have this := ⋯;
  ⟪s.points j -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ = 0
have this : NeZero n
Tactic: haveI : NeZero n := by grind [neZero_iff]
-- 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 : ℕ
s : Simplex ℝ P n
i j : Fin (n + 1)
h : i ≠ j
this : NeZero n
⊢ have this := ⋯;
  ⟪s.points j -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ = 0
have refine : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (s.points i -ᵥ s.altitudeFoot i)
Tactic: refine Submodule.inner_right_of_mem_orthogonal
    (K := vectorSpan ℝ (s.points '' {i}ᶜ))
    (vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
      (s.mem_affineSpan_image_iff.2 h.symm)
      (Affine.Simplex.altitudeFoot_mem_affineSpan_image_compl _ _))
    ?_
-- 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 : ℕ
s : Simplex ℝ P n
i j : Fin (n + 1)
h : i ≠ j
this : NeZero n
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (s.points i -ᵥ s.altitudeFoot i)
have rw : Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range (s.faceOpposite i).points)))ᗮ
  (s.points i -ᵥ s.altitudeFoot i)
Tactic: rw [← direction_affineSpan, ← Affine.Simplex.range_faceOpposite_points]
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : NeZero n
i j : Fin (n + 1)
h : i ≠ j
this : ⟪s.points j -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ = 0
⊢ ⟪s.points i -ᵥ s.points j, s.points i -ᵥ s.altitudeFoot i⟫ = HPow.hPow (β := ℕ) (s.height i) 2
have rwa : ⟪s.points i -ᵥ s.points j, s.points i -ᵥ s.altitudeFoot i⟫ = HPow.hPow (β := ℕ) (dist (s.points i) (s.altitudeFoot i)) 2
Tactic: rwa [height, inner_vsub_vsub_left_eq_dist_sq_right_iff, inner_vsub_left_eq_zero_symm]
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : NeZero n
i j : Fin (n + 1)
h : i ≠ j
this : ⟪s.points j -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ = 0
rwa :
  ⟪s.points i -ᵥ s.points j, s.points i -ᵥ s.altitudeFoot i⟫ =
    HPow.hPow (β := ℕ) (dist (s.points i) (s.altitudeFoot i)) 2
⊢ ⟪s.points i -ᵥ s.points j, s.points i -ᵥ s.altitudeFoot i⟫ = HPow.hPow (β := ℕ) (s.height i) 2
have rwa₁ : ⟪s.altitudeFoot i -ᵥ s.points j, s.points i -ᵥ s.altitudeFoot i⟫ = 0
Tactic: rwa [height, inner_vsub_vsub_left_eq_dist_sq_right_iff, inner_vsub_left_eq_zero_symm]
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : NeZero n
i j : Fin (n + 1)
h : i ≠ j
⊢ ⟪s.points i -ᵥ s.points j, s.points i -ᵥ s.altitudeFoot i⟫ = HPow.hPow (β := ℕ) (s.height i) 2
have suffices : ⟪s.points j -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ = 0
Tactic: suffices ⟪s.points j -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ = 0 by
    rwa [height, inner_vsub_vsub_left_eq_dist_sq_right_iff, inner_vsub_left_eq_zero_symm]
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < s.height i * s.height j
have a : |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| ≤ s.height i * s.height j
Tactic: apply lt_of_le_of_ne
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
a : |⟪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
have a₁ : |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| ≠ s.height i * s.height j
Tactic: apply lt_of_le_of_ne
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| ≤ s.height i * s.height j
have h : s.height i * s.height j = ‖s.points i -ᵥ s.altitudeFoot i‖ * ‖s.points j -ᵥ s.altitudeFoot j‖
Tactic: convert! abs_real_inner_le_norm _ _ using 1
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| ≠ s.height i * s.height j
have a : |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| ≠
  ‖s.points i -ᵥ s.altitudeFoot i‖ * ‖s.points j -ᵥ s.altitudeFoot j‖
Tactic: simp_rw [height, dist_eq_norm_vsub]
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| ≠
    ‖s.points i -ᵥ s.altitudeFoot i‖ * ‖s.points j -ᵥ s.altitudeFoot j‖
have a : ¬∃ (r : ℝ), r ≠ 0 ∧ s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
Tactic: rw [← Real.norm_eq_abs, ne_eq, norm_inner_eq_norm_iff (by simp) (by simp)]
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
⊢ False
have a : s.points j -ᵥ s.altitudeFoot j = 0
Tactic: suffices s.points j -ᵥ s.altitudeFoot j = 0 by
      simp at this
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
⊢ s.points j -ᵥ s.altitudeFoot j = 0
have a : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points) ⊓ (vectorSpan ℝ (Set.range s.points))ᗮ)
  (s.points j -ᵥ s.altitudeFoot j)
Tactic: rw [← Submodule.mem_bot ℝ,
      ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points) ⊓ (vectorSpan ℝ (Set.range s.points))ᗮ)
    (s.points j -ᵥ s.altitudeFoot j)
have a : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.altitudeFoot j)
Tactic: refine ⟨vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
      (mem_affineSpan _ (Set.mem_range_self _)) ?_, ?_⟩
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
a : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.altitudeFoot j)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points) ⊓ (vectorSpan ℝ (Set.range s.points))ᗮ)
    (s.points j -ᵥ s.altitudeFoot j)
have a₁ : s.points j -ᵥ s.altitudeFoot j ∈ (↑(vectorSpan ℝ (Set.range s.points))ᗮ : Set V)
Tactic: refine ⟨vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
      (mem_affineSpan _ (Set.mem_range_self _)) ?_, ?_⟩
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.altitudeFoot j)
have a : Set.range (s.faceOpposite j).points ⊆ Set.range s.points
Tactic: refine SetLike.le_def.1 (affineSpan_mono _ ?_) (Subtype.property _)
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
⊢ 2 < n + 1
have linarith : n + 1 ≤ 2 → -1 + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 2) + (HAdd.hAdd (α := ℤ) 1 1 - (↑n : ℤ)) = 0
Tactic: linarith only [Nat.AtLeastTwo.one_lt (n := n)]
-- 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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (s.points j -ᵥ s.altitudeFoot j)
have hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
Tactic: have hk : ∃ k, k ≠ i ∧ k ≠ j := Fin.exists_ne_and_ne_of_two_lt i j
        (by linarith only [Nat.AtLeastTwo.one_lt (n := n)])