awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
hp : Injective (α := N) (β := M →ₗ[R] R) (⇑p.flip : (a : N) → M →ₗ[R] R)
⊢ Eq (α := PointedCone R N) (dual p univ) 0
have refine : ∀ (y : N) (hy : Membership.mem (γ := Submodule.{u_1, u_3} { c : R // 0 ≤ c } N) (dual p univ) y),
  Eq (α := M →ₗ[R] R) ((p.flip : (a : N) → M →ₗ[R] R) y : M →ₗ[R] R) (0 : M →ₗ[R] R)
Tactic: refine le_antisymm (fun y hy ↦ (map_eq_zero_iff p.flip hp).1 ?_) (by simp)
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
hp : Injective (α := N) (β := M →ₗ[R] R) (⇑p.flip : (a : N) → M →ₗ[R] R)
y : N
hy : Membership.mem (γ := Submodule.{u_1, u_3} { c : R // 0 ≤ c } N) (dual p univ) y
⊢ Eq (α := M →ₗ[R] R) ((p.flip : (a : N) → M →ₗ[R] R) y : M →ₗ[R] R) (0 : M →ₗ[R] R)
have h : ∀ (x : M),
  Eq.{u_1 + 1} (α := R) ((((p.flip : (a : N) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) ((0 : (a : M) → R) x : R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Convex.Cone.Dual (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommGroup N
inst_6 : Module R N
p : M →ₗ[R] N →ₗ[R] R
s : Set M
⊢ Eq (α := PointedCone R N) (dual p (-s)) (-dual p s)
have h : ∀ (x : N), Membership.mem (γ := PointedCone R N) (dual p (-s)) x ↔ Membership.mem (γ := PointedCone R N) (-dual p s) x
Tactic: ext
-- 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 : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).altitude = s.altitude ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
have h : ∀ (i : Fin (m + 1)) (x : P),
  x ∈ (s.reindex e).altitude i ↔ x ∈ (s.altitude ∘ (⇑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 : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
i : Fin (m + 1)
x : P
⊢ x ∈ (s.reindex e).altitude i ↔ x ∈ (s.altitude ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
have h : Membership.mem (γ := AffineSubspace ℝ P)
    (mk' ((s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i)
        (direction
            (affineSpan ℝ
              (s.points '' (Set.image (α := Fin (m + 1)) (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)) {i})ᶜ)))ᗮ ⊓
      affineSpan ℝ (Set.range (s.reindex e).points))
    x ↔
  x ∈ (s.altitude ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
Tactic: simp_rw [altitude, reindex_points, Set.image_comp, Equiv.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 : Fin (n + 1)
⊢ (s.altitude i).direction = (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
have rw : Eq (α := Submodule ℝ V)
  (direction (mk' (s.points i) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ affineSpan ℝ (Set.range s.points)))
  ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
Tactic: rw [altitude_def,
    direction_inf_of_mem (self_mem_mk' (s.points i) _) (mem_affineSpan ℝ (Set.mem_range_self _)),
    direction_mk', 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 : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
rw :
  Eq (α := Submodule ℝ V)
    (direction (mk' (s.points i) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
⊢ (s.altitude i).direction = (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
have rw₁ : Eq (α := Submodule ℝ V)
  (direction (mk' (s.points i) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ) ⊓
    direction (affineSpan ℝ (Set.range s.points)))
  ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
Tactic: rw [altitude_def,
    direction_inf_of_mem (self_mem_mk' (s.points i) _) (mem_affineSpan ℝ (Set.mem_range_self _)),
    direction_mk', 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 : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
rw :
  Eq (α := Submodule ℝ V)
    (direction (mk' (s.points i) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₁ :
  Eq (α := Submodule ℝ V)
    (direction (mk' (s.points i) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ) ⊓
      direction (affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
⊢ (s.altitude i).direction = (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
have rw₂ : Eq (α := Submodule ℝ V) ((direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ direction (affineSpan ℝ (Set.range s.points)))
  ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
Tactic: rw [altitude_def,
    direction_inf_of_mem (self_mem_mk' (s.points i) _) (mem_affineSpan ℝ (Set.mem_range_self _)),
    direction_mk', 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 : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
rw :
  Eq (α := Submodule ℝ V)
    (direction (mk' (s.points i) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₁ :
  Eq (α := Submodule ℝ V)
    (direction (mk' (s.points i) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ) ⊓
      direction (affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₂ :
  Eq (α := Submodule ℝ V)
    ((direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ direction (affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
⊢ (s.altitude i).direction = (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
have rw₃ : Eq (α := Submodule ℝ V) ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ direction (affineSpan ℝ (Set.range s.points)))
  ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
Tactic: rw [altitude_def,
    direction_inf_of_mem (self_mem_mk' (s.points i) _) (mem_affineSpan ℝ (Set.mem_range_self _)),
    direction_mk', 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 : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
rw :
  Eq (α := Submodule ℝ V)
    (direction (mk' (s.points i) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₁ :
  Eq (α := Submodule ℝ V)
    (direction (mk' (s.points i) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ) ⊓
      direction (affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₂ :
  Eq (α := Submodule ℝ V)
    ((direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ direction (affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₃ :
  Eq (α := Submodule ℝ V) ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ direction (affineSpan ℝ (Set.range s.points)))
    ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
⊢ (s.altitude i).direction = (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
have rw₄ : Eq (α := Submodule ℝ V) ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
  ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
Tactic: rw [altitude_def,
    direction_inf_of_mem (self_mem_mk' (s.points i) _) (mem_affineSpan ℝ (Set.mem_range_self _)),
    direction_mk', 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 : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ vectorSpan ℝ (s.points '' {i}ᶜ) ⟂ (s.altitude i).direction
have rw : vectorSpan ℝ (s.points '' {i}ᶜ) ⟂ (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
Tactic: rw [direction_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
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 : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ (s.map f.toAffineMap ⋯).altitude i = AffineSubspace.map f.toAffineMap (s.altitude i)
have refine_1 : Membership.mem (α := P₂) ((s.map f.toAffineMap sorry).altitude i) ((f : (a : P) → P₂) (s.points i) : P₂)
Tactic: refine (eq_iff_direction_eq_of_mem (p := f (s.points i)) ?_ ?_).mpr ?_
-- 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
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 : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
refine_1 : Membership.mem (α := P₂) ((s.map f.toAffineMap ⋯).altitude i) ((f : (a : P) → P₂) (s.points i) : P₂)
⊢ (s.map f.toAffineMap ⋯).altitude i = AffineSubspace.map f.toAffineMap (s.altitude i)
have refine_2 : Membership.mem (α := P₂) (AffineSubspace.map f.toAffineMap (s.altitude i)) ((f : (a : P) → P₂) (s.points i) : P₂)
Tactic: refine (eq_iff_direction_eq_of_mem (p := f (s.points i)) ?_ ?_).mpr ?_
-- 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
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 : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
refine_1 : Membership.mem (α := P₂) ((s.map f.toAffineMap ⋯).altitude i) ((f : (a : P) → P₂) (s.points i) : P₂)
refine_2 :
  Membership.mem (α := P₂) (AffineSubspace.map f.toAffineMap (s.altitude i)) ((f : (a : P) → P₂) (s.points i) : P₂)
⊢ (s.map f.toAffineMap ⋯).altitude i = AffineSubspace.map f.toAffineMap (s.altitude i)
have refine_3 : ((s.map f.toAffineMap sorry).altitude i).direction = (AffineSubspace.map f.toAffineMap (s.altitude i)).direction
Tactic: refine (eq_iff_direction_eq_of_mem (p := f (s.points i)) ?_ ?_).mpr ?_
-- 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
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 : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ ((s.map f.toAffineMap ⋯).altitude i).direction = (AffineSubspace.map f.toAffineMap (s.altitude i)).direction
have hf : Function.Injective.{u_1 + 1, u_3 + 1} (α := V) (β := V₂) (⇑f.linear : (a : V) → V₂)
Tactic: have hf : Function.Injective f.linear := f.linearIsometry.injective
-- 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ AffineSubspace.map S.subtype (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i) = s.altitude i
have rw : s.altitude i = AffineSubspace.map S.subtype (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i)
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 : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ Eq.{u_2 + 1} (α := AffineSubspace ℝ ↥S) (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i : AffineSubspace ℝ ↥S)
    (comap S.subtype (s.altitude i) : AffineSubspace ℝ ↥S)
have this : Nonempty.{u_2 + 1} ↥S
Tactic: haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
this : Nonempty.{u_2 + 1} ↥S
⊢ Eq.{u_2 + 1} (α := AffineSubspace ℝ ↥S) (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i : AffineSubspace ℝ ↥S)
    (comap S.subtype (s.altitude i) : AffineSubspace ℝ ↥S)
have rw : Eq.{u_2 + 1} (α := AffineSubspace ℝ ↥S) (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i : AffineSubspace ℝ ↥S)
  (comap S.subtype (AffineSubspace.map S.subtype (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i)) :
    AffineSubspace ℝ ↥S)
Tactic: rw [← s.map_altitude_restrict S hS, comap_map_eq_of_injective S.subtype_injective]
-- 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
this : Nonempty.{u_2 + 1} ↥S
rw :
  Eq.{u_2 + 1} (α := AffineSubspace ℝ ↥S) (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i : AffineSubspace ℝ ↥S)
    (comap S.subtype (AffineSubspace.map S.subtype (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i)) :
      AffineSubspace ℝ ↥S)
⊢ Eq.{u_2 + 1} (α := AffineSubspace ℝ ↥S) (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i : AffineSubspace ℝ ↥S)
    (comap S.subtype (s.altitude i) : AffineSubspace ℝ ↥S)
have rw₁ : Eq.{u_2 + 1} (α := AffineSubspace ℝ ↥S) (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i : AffineSubspace ℝ ↥S)
  (altitude.{u_1, u_2} (P := ↥S) (s.restrict S hS) i : AffineSubspace ℝ ↥S)
Tactic: rw [← s.map_altitude_restrict S hS, comap_map_eq_of_injective S.subtype_injective]
-- 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
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 : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ FiniteDimensional.{0, u_1} ℝ ↥(s.altitude i).direction
have rw : FiniteDimensional.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
Tactic: rw [direction_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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ finrank.{0, u_1} ℝ ↥(s.altitude i).direction = 1
have rw : finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = 1
Tactic: rw [direction_altitude]
-- 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)
⊢ finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = 1
have 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))
Tactic: have h := Submodule.finrank_add_inf_finrank_orthogonal
    (vectorSpan_mono ℝ (Set.image_subset_range s.points {i}ᶜ))
-- 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))
⊢ n - 1 + 1 = n
have this : n ≠ 0
Tactic: have := NeZero.ne n
-- 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))
this : n ≠ 0
⊢ n - 1 + 1 = n
have zero : ∀ [NeZero (R := ℕ) 0] (s : Simplex ℝ P 0) (i : Fin (HAdd.hAdd (α := ℕ) 0 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)))
  (this : Ne (α := ℕ) 0 0), HSub.hSub (α := ℕ) 0 1 + 1 = 0
Tactic: cases n
Cleared hypotheses: n, inst_4, s, i, h, 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 : ℕ
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))
this : n ≠ 0
zero :
  ∀ [NeZero (R := ℕ) 0] (s : Simplex ℝ P 0) (i : Fin (HAdd.hAdd (α := ℕ) 0 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)))
    (this : Ne (α := ℕ) 0 0), HSub.hSub (α := ℕ) 0 1 + 1 = 0
⊢ n - 1 + 1 = n
have succ : ∀ (n : ℕ) [NeZero (n + 1)] (s : Simplex ℝ P (n + 1)) (i : Fin (n + 1 + 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)))
  (this : n + 1 ≠ 0), n + 1 - 1 + 1 = n + 1
Tactic: cases n
Cleared hypotheses: n, inst_4, s, i, h, this
-- 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))
⊢ finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = 1
have hn : n - 1 + 1 = n
Tactic: have hn : (n - 1) + 1 = n := by
    have := NeZero.ne n
    cases n <;> lia
-- 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
⊢ card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
have rw : Fintype.card (Fin (n + 1)) - card (α := Fin (n + 1)) {i} = n - 1 + 1
Tactic: 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
rw : Fintype.card (Fin (n + 1)) - card (α := Fin (n + 1)) {i} = n - 1 + 1
⊢ card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
have rw₁ : Fintype.card (Fin (n + 1)) - 1 = n - 1 + 1
Tactic: 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
rw : Fintype.card (Fin (n + 1)) - card (α := Fin (n + 1)) {i} = n - 1 + 1
rw₁ : Fintype.card (Fin (n + 1)) - 1 = n - 1 + 1
⊢ card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
have rw₂ : n + 1 - 1 = n - 1 + 1
Tactic: 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
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
⊢ card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
have rw₃ : n + 1 - 1 = n
Tactic: rw [card_compl, card_singleton, Fintype.card_fin, hn, add_tsub_cancel_right]