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 : ℕ
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)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
⊢ Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
have rcases : ∀ (k : Fin (n + 1)) (hki : k ≠ i) (hkj : k ≠ j),
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
Tactic: rcases hk with ⟨k, hki, hkj⟩
Cleared hypotheses: hk
-- 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)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
⊢ s.points k ∈ Set.range (s.faceOpposite i).points
have rw : s.points k ∈ s.points '' {i}ᶜ
Tactic: rw [range_faceOpposite_points]
-- 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)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
⊢ Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
have hki' : s.points k ∈ Set.range (s.faceOpposite i).points
Tactic: have hki' : s.points k ∈ Set.range (s.faceOpposite i).points := by
          rw [range_faceOpposite_points]
          exact Set.mem_image_of_mem _ hki
-- 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)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hki' : s.points k ∈ Set.range (s.faceOpposite i).points
⊢ s.points k ∈ Set.range (s.faceOpposite j).points
have rw : s.points k ∈ s.points '' {j}ᶜ
Tactic: rw [range_faceOpposite_points]
-- 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)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hki' : s.points k ∈ Set.range (s.faceOpposite i).points
⊢ Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
have hkj' : s.points k ∈ Set.range (s.faceOpposite j).points
Tactic: have hkj' : s.points k ∈ Set.range (s.faceOpposite j).points := by
          rw [range_faceOpposite_points]
          exact Set.mem_image_of_mem _ hkj
-- 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)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hki' : s.points k ∈ Set.range (s.faceOpposite i).points
hkj' : s.points k ∈ Set.range (s.faceOpposite j).points
⊢ Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
have simp : Set.range s.points = s.points '' ({i}ᶜ ∪ {j}ᶜ)
Tactic: simp only [range_faceOpposite_points, ← Set.image_union]
-- 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)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hki' : s.points k ∈ Set.range (s.faceOpposite i).points
hkj' : s.points k ∈ Set.range (s.faceOpposite j).points
⊢ Set.range s.points = s.points '' ({i}ᶜ ∪ {j}ᶜ)
have simp_rw : s.points '' Set.univ = s.points '' ({i} ∩ {j})ᶜ
Tactic: simp_rw [← Set.image_univ, ← Set.compl_inter]
-- 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)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hki' : s.points k ∈ Set.range (s.faceOpposite i).points
hkj' : s.points k ∈ Set.range (s.faceOpposite j).points
⊢ s.points '' Set.univ = s.points '' ({i} ∩ {j})ᶜ
have rw : j ∉ {i}
Tactic: rw [Set.inter_singleton_eq_empty.mpr ?_, Set.compl_empty]
-- 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)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hki' : s.points k ∈ Set.range (s.faceOpposite i).points
hkj' : s.points k ∈ Set.range (s.faceOpposite j).points
⊢ Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
have hs : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
Tactic: have hs :
            Set.range s.points =
              Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points := by
          simp only [range_faceOpposite_points, ← Set.image_union]
          simp_rw [← Set.image_univ, ← Set.compl_inter]
          rw [Set.inter_singleton_eq_empty.mpr ?_, Set.compl_empty]
          simpa using hij.symm
-- 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)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (s.points j -ᵥ s.altitudeFoot j)
have hs : Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
  (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
Tactic: have hs : vectorSpan ℝ (Set.range s.points) =
          vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔
            vectorSpan ℝ (Set.range (s.faceOpposite j).points) := by
        rcases hk with ⟨k, hki, hkj⟩
        have hki' : s.points k ∈ Set.range (s.faceOpposite i).points := by
          rw [range_faceOpposite_points]
          exact Set.mem_image_of_mem _ hki
        have hkj' : s.points k ∈ Set.range (s.faceOpposite j).points := by
          rw [range_faceOpposite_points]
          exact Set.mem_image_of_mem _ hkj
        have hs :
            Set.range s.points =
              Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points := by
          simp only [range_faceOpposite_points, ← Set.image_union]
          simp_rw [← Set.image_univ, ← Set.compl_inter]
          rw [Set.inter_singleton_eq_empty.mpr ?_, Set.compl_empty]
          simpa using hij.symm
        convert! AffineSubspace.vectorSpan_union_of_mem_of_mem ℝ hki' hkj'
-- 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)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (s.points j -ᵥ s.altitudeFoot j)
have a : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ
    (s.points j -ᵥ s.altitudeFoot j) ∧
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ
    (s.points j -ᵥ s.altitudeFoot j)
Tactic: rw [hs, ← Submodule.inf_orthogonal, Submodule.mem_inf]
-- 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)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ
      (s.points j -ᵥ s.altitudeFoot j) ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ
      (s.points j -ᵥ s.altitudeFoot j)
have a : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ
  (s.points j -ᵥ s.altitudeFoot j)
Tactic: refine ⟨?_, ?_⟩
-- 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)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
a :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ
    (s.points j -ᵥ s.altitudeFoot j)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ
      (s.points j -ᵥ s.altitudeFoot j) ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ
      (s.points j -ᵥ s.altitudeFoot j)
have a₁ : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ
  (s.points j -ᵥ s.altitudeFoot j)
Tactic: refine ⟨?_, ?_⟩
-- 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)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite i).points))ᗮ
    (s.points j -ᵥ s.altitudeFoot j)
have a : Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range (s.faceOpposite i).points)))ᗮ
  (r • (s.points i -ᵥ s.altitudeFoot i))
Tactic: rw [h, ← 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 : ℕ
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)
hk : ∃ (k : Fin (n + 1)), k ≠ i ∧ k ≠ j
hs :
  Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ
    (s.points j -ᵥ s.altitudeFoot j)
have a : Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range (s.faceOpposite j).points)))ᗮ
  (s.points j -ᵥ s.altitudeFoot j)
Tactic: rw [← 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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
⊢ -(s.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫
have inl : -(s.height i * s.height i) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j
-- 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)
inl : -(s.height i * s.height i) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫
⊢ -(s.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫
have inr : ∀ (hij : i ≠ j), -(s.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫
Tactic: obtain rfl | hij := eq_or_ne i j
-- 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 : Fin (n + 1)
⊢ -(s.height i * s.height i) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫
have inl : -(s.height i * s.height i) < HPow.hPow (β := ℕ) ‖s.points i -ᵥ s.altitudeFoot i‖ 2
Tactic: rw [real_inner_self_eq_norm_sq]
-- 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 : Fin (n + 1)
⊢ -(s.height i * s.height i) < HPow.hPow (β := ℕ) ‖s.points i -ᵥ s.altitudeFoot i‖ 2
have inl : -(s.height i * s.height i) < 0
Tactic: refine lt_of_lt_of_le (b := 0) ?_ ?_
-- 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 : Fin (n + 1)
inl : -(s.height i * s.height i) < 0
⊢ -(s.height i * s.height i) < HPow.hPow (β := ℕ) ‖s.points i -ᵥ s.altitudeFoot i‖ 2
have inl₁ : 0 ≤ HPow.hPow (β := ℕ) ‖s.points i -ᵥ s.altitudeFoot i‖ 2
Tactic: refine lt_of_lt_of_le (b := 0) ?_ ?_
-- 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 : Fin (n + 1)
⊢ -(s.height i * s.height i) < 0
have inl : 0 < s.height i * s.height i
Tactic: rw [neg_lt_zero]
-- 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.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫
have inr : -⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ < s.height i * s.height j
Tactic: rw [neg_lt]
-- 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 inr : |(-⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫)| < s.height i * s.height j
Tactic: refine lt_of_abs_lt ?_
-- 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 inr : |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < s.height i * s.height j
Tactic: rw [abs_neg]
-- 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)| < 1
have rw : |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < |s.height i * s.height j|
Tactic: rw [abs_div, div_lt_one (by simp [height])]
-- 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 nth_rw : |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < s.height i * s.height j
Tactic: nth_rw 2 [abs_eq_self.2]
-- 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
nth_rw : |⟪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 nth_rw₁ : 0 ≤ s.height i * s.height j
Tactic: nth_rw 2 [abs_eq_self.2]
-- 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
⊢ 0 ≤ s.height i * s.height j
have simp : 0 ≤ dist (s.points i) (s.altitudeFoot i) * dist (s.points j) (s.altitudeFoot j)
Tactic: simp only [height]
-- 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 : n.AtLeastTwo
s : Simplex ℝ P n
i j : Fin (n + 1)
⊢ -1 < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)
have rw : -(s.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫
Tactic: rw [neg_lt, neg_div', div_lt_one (by simp [height]), neg_lt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_5
inst_5 : TopologicalSpace H
G : Type u_7
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_11
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
α : Sort u_13
h : M ≃ₘ^n⟮I, J⟯ N
f : α → M
⊢ Eq.{u_11 + 1} (α := Set N) (range ((⇑h : (a : M) → N) ∘ f)) ((⇑h.symm : (a : N) → M) ⁻¹' range f)
have rw : Eq.{u_11 + 1} (α := Set N) ((⇑h : (a : M) → N) '' range f) ((⇑h.symm : (a : N) → M) ⁻¹' range f)
Tactic: rw [range_comp, image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
H : Type u_5
inst_5 : TopologicalSpace H
G : Type u_7
inst_6 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
N : Type u_11
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
α : Sort u_13
h : M ≃ₘ^n⟮I, J⟯ N
f : α → M
rw : Eq.{u_11 + 1} (α := Set N) ((⇑h : (a : M) → N) '' range f) ((⇑h.symm : (a : N) → M) ⁻¹' range f)
⊢ Eq.{u_11 + 1} (α := Set N) (range ((⇑h : (a : M) → N) ∘ f)) ((⇑h.symm : (a : N) → M) ⁻¹' range f)
have rw₁ : Eq.{u_11 + 1} (α := Set N) ((⇑h.symm : (a : N) → M) ⁻¹' range f) ((⇑h.symm : (a : N) → M) ⁻¹' range f)
Tactic: rw [range_comp, image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Diffeomorph (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst_10 : TopologicalSpace M
inst_11 : ChartedSpace H M
M' : Type u_10
inst_12 : TopologicalSpace M'
inst_13 : ChartedSpace H' M'
N : Type u_11
inst_14 : TopologicalSpace N
inst_15 : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
⊢ ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s x ↔
    ContMDiffWithinAt J I' m f ((⇑h.symm : (a : N) → M) ⁻¹' s) ((h : (a : M) → N) x)
have mp : ContMDiffWithinAt I I' m (f ∘ (⇑h : (a : M) → N)) s x →
  ContMDiffWithinAt J I' m f ((⇑h.symm : (a : N) → M) ⁻¹' s) ((h : (a : M) → N) x)
Tactic: constructor