awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
⊢ 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:
orthogonalProjectionSpan_congr (s.range_faceOpposite_reindex e i) rfl

Premises used: Affine.Simplex.orthogonalProjectionSpan_congr, Affine.Simplex.range_faceOpposite_reindex, rfl
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
⊢ 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:
exact orthogonalProjectionSpan_congr (s.range_faceOpposite_reindex e i) rfl

Premises used: Affine.Simplex.orthogonalProjectionSpan_congr, Affine.Simplex.range_faceOpposite_reindex, rfl
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ (s.map f.toAffineMap ⋯).altitudeFoot i = (f : (a : P) → P₂) (s.altitudeFoot i)

Tactic:
simp [altitudeFoot, ← orthogonalProjectionSpan_map]

Premises used: Affine.Simplex.orthogonalProjectionSpan_map, Affine.Simplex.altitudeFoot
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
rw : s.altitudeFoot i = (↑((s.restrict S hS).altitudeFoot i) : P)
⊢ (↑((s.restrict S hS).altitudeFoot i) : P) = s.altitudeFoot i

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Geometry.Euclidean.Altitude
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).map (AffineIsometry.toAffineMap (subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S)) ⋯).altitudeFoot i =
    ((subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S : ↥S →ᵃⁱ[ℝ] P) : (a : ↥S) → P) ((s.restrict S hS).altitudeFoot i)

Tactic:
(s.restrict S hS).altitudeFoot_map S.subtypeₐᵢ i

Premises used: Affine.Simplex.altitudeFoot_map, AffineSubspace.subtypeₐᵢ
-- Module: Mathlib.Geometry.Euclidean.Altitude
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.altitudeFoot i = (↑((s.restrict S hS).altitudeFoot i) : P)

Tactic:
convert! (s.restrict S hS).altitudeFoot_map S.subtypeₐᵢ i
-- Module: Mathlib.Geometry.Euclidean.Altitude
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
⊢ 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

Premises used: Affine.Simplex.orthogonalProjectionSpan, eq_comm, Affine.Simplex.altitudeFoot, EuclideanGeometry.orthogonalProjection_eq_self_iff
-- Module: Mathlib.Geometry.Euclidean.Altitude
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 : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i)
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
rw : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.altitudeFoot i)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' {i}ᶜ)) (s.altitudeFoot i)

Tactic:
rw [← range_faceOpposite_points]

Premises used: Affine.Simplex.range_faceOpposite_points
-- Module: Mathlib.Geometry.Euclidean.Altitude
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.faceOpposite i).points)) (s.altitudeFoot i)

Tactic:
orthogonalProjection_mem _

Premises used: Set.Mem, EuclideanGeometry.orthogonalProjection_mem, Affine.Simplex.altitudeFoot
-- Module: Mathlib.Geometry.Euclidean.Altitude
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.faceOpposite i).points)) (s.altitudeFoot i)

Tactic:
exact orthogonalProjection_mem _

Premises used: EuclideanGeometry.orthogonalProjection_mem
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)

Tactic:
SetLike.le_def.1 (affineSpan_mono _ ?_) (s.altitudeFoot_mem_affineSpan_faceOpposite _)

Premises used: SetLike.le_def, Iff.mp, affineSpan_mono, Affine.Simplex.altitudeFoot_mem_affineSpan_faceOpposite
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
refine : Set.range (s.faceOpposite i).points ⊆ Set.range s.points
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.altitudeFoot i)

Tactic:
refine SetLike.le_def.1 (affineSpan_mono _ ?_) (s.altitudeFoot_mem_affineSpan_faceOpposite _)

Premises used: SetLike.le_def, Iff.mp, affineSpan_mono, Affine.Simplex.altitudeFoot_mem_affineSpan_faceOpposite
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
⊢ Set.range (s.faceOpposite i).points ⊆ Set.range s.points

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
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)
⊢ affineSpan ℝ {s.altitudeFoot i, s.points i} = s.altitude i

Tactic:
rw [affineSpan_pair_eq_altitude_iff]

Premises used: Affine.Simplex.affineSpan_pair_eq_altitude_iff
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)

Tactic:
⟨(s.ne_altitudeFoot i).symm, s.altitudeFoot_mem_affineSpan _, ?_⟩

Premises used: Affine.Simplex.ne_altitudeFoot, Affine.Simplex.altitudeFoot_mem_affineSpan, Ne.symm, And.intro
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
refine :
  Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ (s.altitudeFoot i -ᵥ s.points i)
⊢ 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:
refine ⟨(s.ne_altitudeFoot i).symm, s.altitudeFoot_mem_affineSpan _, ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
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)
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ (s.altitudeFoot i -ᵥ s.points i)

Tactic:
rw [altitudeFoot, orthogonalProjectionSpan]

Premises used: Affine.Simplex.orthogonalProjectionSpan, Affine.Simplex.altitudeFoot
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
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)
⊢ 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:
simp_rw [range_faceOpposite_points]

Premises used: Affine.Simplex.range_faceOpposite_points
-- Module: Mathlib.Geometry.Euclidean.Altitude
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 ℝ (s.points '' {i}ᶜ)) : (a : P) → ↥(affineSpan ℝ (s.points '' {i}ᶜ)))
            (s.points i)) :
        P) -ᵥ
      s.points i)

Tactic:
orthogonalProjection_vsub_mem_direction_orthogonal _ _

Premises used: Set.Mem, setOf, EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal
-- Module: Mathlib.Geometry.Euclidean.Altitude
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 ℝ (s.points '' {i}ᶜ)) : (a : P) → ↥(affineSpan ℝ (s.points '' {i}ᶜ)))
            (s.points i)) :
        P) -ᵥ
      s.points i)

Tactic:
exact orthogonalProjection_vsub_mem_direction_orthogonal _ _

Premises used: EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
rw : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {s.altitudeFoot i, s.points i}) (s.altitudeFoot i)
⊢ s.altitudeFoot i ∈ s.altitude i

Tactic:
rw [← affineSpan_pair_altitudeFoot_eq_altitude]

Premises used: Affine.Simplex.affineSpan_pair_altitudeFoot_eq_altitude
-- Module: Mathlib.Geometry.Euclidean.Altitude
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.altitudeFoot i, s.points i}) (s.altitudeFoot i)

Tactic:
left_mem_affineSpan_pair _ _ _

Premises used: left_mem_affineSpan_pair
-- Module: Mathlib.Geometry.Euclidean.Altitude
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.altitudeFoot i, s.points i}) (s.altitudeFoot i)

Tactic:
exact left_mem_affineSpan_pair _ _ _

Premises used: left_mem_affineSpan_pair
-- Module: Mathlib.Geometry.Euclidean.Altitude
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.altitudeFoot i = s.points i.rev

Tactic:
simp [altitudeFoot, faceOpposite_point_eq_point_rev]

Premises used: Affine.Simplex.faceOpposite_point_eq_point_rev, Affine.Simplex.altitudeFoot
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
h : ∀ (i : Fin (m + 1)), (s.reindex e).height i = (s.height ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
⊢ (s.reindex e).height = s.height ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))

Tactic:
ext i
-- Module: Mathlib.Geometry.Euclidean.Altitude
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).height i = (s.height ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i

Tactic:
simp [height]

Premises used: Affine.Simplex.height
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ (s.map f.toAffineMap ⋯).height i = s.height i

Tactic:
simp [height]

Premises used: Affine.Simplex.height
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
rw : s.height i = height.{u_1, u_2} (P := ↥S) (s.restrict S hS) i
⊢ height.{u_1, u_2} (P := ↥S) (s.restrict S hS) i = s.height i

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Geometry.Euclidean.Altitude
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).map (AffineIsometry.toAffineMap (subtypeₐᵢ.{0, u_1, u_2} (𝕜 := ℝ) (P := P) S)) ⋯).height i =
    height.{u_1, u_2} (P := ↥S) (s.restrict S hS) i

Tactic:
(s.restrict S hS).height_map S.subtypeₐᵢ i

Premises used: Affine.Simplex.height_map, AffineSubspace.subtypeₐᵢ
-- Module: Mathlib.Geometry.Euclidean.Altitude
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.height i = height.{u_1, u_2} (P := ↥S) (s.restrict S hS) i

Tactic:
convert! (s.restrict S hS).height_map S.subtypeₐᵢ i
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
⊢ 0 < s.height i

Tactic:
simp [height]

Premises used: Affine.Simplex.height
-- Module: Mathlib.Geometry.Euclidean.Altitude
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ 0 < s.height i

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Altitude
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)
1 : s.height ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = dist (s.points 0) (s.points 1)
⊢ s.height i = dist (s.points 0) (s.points 1)

Tactic:
fin_cases i
-- Module: Mathlib.Geometry.Euclidean.Altitude
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) (⟨0, ⋯⟩ : Fin 2)) = dist (s.points 0) (s.points 1)

Tactic:
simp [height]

Premises used: Affine.Simplex.height
-- Module: Mathlib.Geometry.Euclidean.Altitude
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
1 : s.height ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = dist (s.points 1) (s.points 0)
⊢ s.height ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = dist (s.points 0) (s.points 1)

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Altitude
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 1) (s.points 0)

Tactic:
simp [height]

Premises used: Affine.Simplex.height
-- Module: Mathlib.Geometry.Euclidean.Altitude
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 j : Fin (n + 1)
h : i ≠ j
⊢ NeZero n

Tactic:
grind [neZero_iff]

Premises used: neZero_iff
-- Module: Mathlib.Geometry.Euclidean.Altitude
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
⊢ NeZero n

Tactic:
grind [neZero_iff]

Premises used: neZero_iff
-- Module: Mathlib.Geometry.Euclidean.Altitude
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
⊢ NeZero n

Tactic:
haveI : NeZero n := by grind [neZero_iff]
-- Module: Mathlib.Geometry.Euclidean.Altitude
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

Tactic:
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 _ _))
    ?_

Premises used: Iff.mpr, Affine.Simplex.altitudeFoot_mem_affineSpan_image_compl, Ne.symm, Affine.Simplex.mem_affineSpan_image_iff, Submodule.inner_right_of_mem_orthogonal, vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
-- Module: Mathlib.Geometry.Euclidean.Altitude
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
refine : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (s.points i -ᵥ s.altitudeFoot i)
⊢ have this := ⋯;
  ⟪s.points j -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ = 0

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 _ _))
    ?_

Premises used: Iff.mpr, Affine.Simplex.altitudeFoot_mem_affineSpan_image_compl, Ne.symm, Affine.Simplex.mem_affineSpan_image_iff, Submodule.inner_right_of_mem_orthogonal, vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
-- Module: Mathlib.Geometry.Euclidean.Altitude
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
rw :
  Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range (s.faceOpposite i).points)))ᗮ
    (s.points i -ᵥ s.altitudeFoot i)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (s.points i -ᵥ s.altitudeFoot i)

Tactic:
rw [← direction_affineSpan, ← Affine.Simplex.range_faceOpposite_points]

Premises used: direction_affineSpan, Affine.Simplex.range_faceOpposite_points