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
n : ℕ
s : Simplex ℝ P n
i j : Fin (n + 1)
h : i ≠ j
this : NeZero n
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range (s.faceOpposite i).points)))ᗮ
    (s.points i -ᵥ s.altitudeFoot i)

Tactic:
vsub_orthogonalProjection_mem_direction_orthogonal _ _

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, Set.Mem, setOf, 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 : ℕ
s : Simplex ℝ P n
i j : Fin (n + 1)
h : i ≠ j
this : NeZero n
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range (s.faceOpposite i).points)))ᗮ
    (s.points i -ᵥ s.altitudeFoot i)

Tactic:
exact vsub_orthogonalProjection_mem_direction_orthogonal _ _

Premises used: EuclideanGeometry.vsub_orthogonalProjection_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 : ℕ
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
rwa₁ : ⟪s.altitudeFoot i -ᵥ s.points j, s.points i -ᵥ s.altitudeFoot i⟫ = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ⟪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

Tactic:
rwa [height, inner_vsub_vsub_left_eq_dist_sq_right_iff, inner_vsub_left_eq_zero_symm]

Premises used: Affine.Simplex.height, inner_vsub_vsub_left_eq_dist_sq_right_iff, inner_vsub_left_eq_zero_symm
-- 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
inst_4 : NeZero n
i j : Fin (n + 1)
h : i ≠ j
suffices : ⟪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

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]
-- 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
inst_4 : NeZero n
i j : Fin (n + 1)
h : i ≠ j
⊢ ⟪s.points j -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ = 0

Tactic:
s.inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero h

Premises used: Affine.Simplex.inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero
-- 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
inst_4 : NeZero n
i j : Fin (n + 1)
h : i ≠ j
⊢ ⟪s.points j -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ = 0

Tactic:
exact s.inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero h

Premises used: Affine.Simplex.inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero
-- 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
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
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

Tactic:
apply lt_of_le_of_ne

Premises used: lt_of_le_of_ne
-- 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
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‖

Tactic:
abs_real_inner_le_norm _ _

Premises used: abs_real_inner_le_norm
-- 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
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
h : s.height i * s.height 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⟫| ≤ s.height i * s.height j

Tactic:
convert! abs_real_inner_le_norm _ _ using 1

Premises used: abs_real_inner_le_norm
-- 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
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‖

Tactic:
simp only [dist_eq_norm_vsub, height]

Premises used: Affine.Simplex.height, dist_eq_norm_vsub
-- 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
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.points i -ᵥ s.altitudeFoot i‖ * ‖s.points j -ᵥ s.altitudeFoot j‖
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| ≠ s.height i * s.height j

Tactic:
simp_rw [height, dist_eq_norm_vsub]

Premises used: Affine.Simplex.height, dist_eq_norm_vsub
-- 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
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ s.points i -ᵥ s.altitudeFoot i ≠ 0

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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ s.points j -ᵥ s.altitudeFoot j ≠ 0

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 : ℕ
s : Simplex ℝ P n
inst_4 : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
a : ¬∃ (r : ℝ), r ≠ 0 ∧ s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
⊢ |⟪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:
rw [← Real.norm_eq_abs, ne_eq, norm_inner_eq_norm_iff (by simp) (by simp)]

Premises used: norm_inner_eq_norm_iff, ne_eq, Real.norm_eq_abs
-- 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
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)
this : s.points j -ᵥ s.altitudeFoot j = 0
⊢ False

Tactic:
simp at this
-- 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
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 : s.points j -ᵥ s.altitudeFoot j = 0
⊢ False

Tactic:
suffices s.points j -ᵥ s.altitudeFoot j = 0 by
      simp at this
-- 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
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 (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points) ⊓ (vectorSpan ℝ (Set.range s.points))ᗮ)
    (s.points j -ᵥ s.altitudeFoot j)
⊢ s.points j -ᵥ s.altitudeFoot j = 0

Tactic:
rw [← Submodule.mem_bot ℝ,
      ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]

Premises used: Affine.Simplex.points, Real, vectorSpan, Submodule.mem_bot, Submodule.inf_orthogonal_eq_bot, Set.range
-- 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
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)

Tactic:
⟨vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
      (mem_affineSpan _ (Set.mem_range_self _)) ?_, ?_⟩

Premises used: Set.mem_range_self, Set.Mem, setOf, mem_affineSpan, Set.inter, And.intro, 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
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)
a₁ : s.points j -ᵥ s.altitudeFoot j ∈ (↑(vectorSpan ℝ (Set.range s.points))ᗮ : Set V)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points) ⊓ (vectorSpan ℝ (Set.range s.points))ᗮ)
    (s.points j -ᵥ s.altitudeFoot j)

Tactic:
refine ⟨vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
      (mem_affineSpan _ (Set.mem_range_self _)) ?_, ?_⟩
-- 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
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)

Tactic:
SetLike.le_def.1 (affineSpan_mono _ ?_) (Subtype.property _)

Premises used: SetLike.le_def, Iff.mp, affineSpan_mono, Subtype.property
-- 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
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 : Set.range (s.faceOpposite j).points ⊆ Set.range s.points
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.altitudeFoot j)

Tactic:
refine SetLike.le_def.1 (affineSpan_mono _ ?_) (Subtype.property _)

Premises used: SetLike.le_def, Iff.mp, affineSpan_mono, Subtype.property
-- 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
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)
⊢ Set.range (s.faceOpposite j).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 : ℕ
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)
linarith : n + 1 ≤ 2 → -1 + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 2) + (HAdd.hAdd (α := ℤ) 1 1 - (↑n : ℤ)) = 0
⊢ 2 < n + 1

Tactic:
linarith only [Nat.AtLeastTwo.one_lt (n := n)]

Premises used: Nat.AtLeastTwo.one_lt
-- 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
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)), 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)])
-- 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
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
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))
⊢ 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⟩
-- 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
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
rw : s.points k ∈ s.points '' {i}ᶜ
⊢ s.points k ∈ Set.range (s.faceOpposite i).points

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 : ℕ
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 ∈ s.points '' {i}ᶜ

Tactic:
Set.mem_image_of_mem _ hki

Premises used: Set.mem_image_of_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 : ℕ
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 ∈ s.points '' {i}ᶜ

Tactic:
exact Set.mem_image_of_mem _ hki

Premises used: Set.mem_image_of_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 : ℕ
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

Tactic:
have hki' : s.points k ∈ Set.range (s.faceOpposite i).points := by
          rw [range_faceOpposite_points]
          exact Set.mem_image_of_mem _ hki
-- 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
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
rw : s.points k ∈ s.points '' {j}ᶜ
⊢ s.points k ∈ Set.range (s.faceOpposite j).points

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 : ℕ
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 ∈ s.points '' {j}ᶜ

Tactic:
Set.mem_image_of_mem _ hkj

Premises used: Set.mem_image_of_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 : ℕ
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 ∈ s.points '' {j}ᶜ

Tactic:
exact Set.mem_image_of_mem _ hkj

Premises used: Set.mem_image_of_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 : ℕ
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

Tactic:
have hkj' : s.points k ∈ Set.range (s.faceOpposite j).points := by
          rw [range_faceOpposite_points]
          exact Set.mem_image_of_mem _ hkj
-- 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
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
simp : Set.range s.points = s.points '' ({i}ᶜ ∪ {j}ᶜ)
⊢ Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points

Tactic:
simp only [range_faceOpposite_points, ← Set.image_union]

Premises used: Affine.Simplex.range_faceOpposite_points, Set.image_union
-- 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
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
simp_rw : s.points '' Set.univ = s.points '' ({i} ∩ {j})ᶜ
⊢ Set.range s.points = s.points '' ({i}ᶜ ∪ {j}ᶜ)

Tactic:
simp_rw [← Set.image_univ, ← Set.compl_inter]

Premises used: Set.image_univ, Set.compl_inter
-- 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
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
rw : j ∉ {i}
⊢ s.points '' Set.univ = s.points '' ({i} ∩ {j})ᶜ

Tactic:
rw [Set.inter_singleton_eq_empty.mpr ?_, Set.compl_empty]

Premises used: Iff.mpr, Set.inter_singleton_eq_empty, Set.compl_empty
-- 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
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
⊢ j ∉ {i}

Tactic:
simpa using hij.symm

Premises used: Ne.symm
-- 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
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

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
-- 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
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
hs : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ Eq (α := Submodule ℝ V) (vectorSpan ℝ (Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points))
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points))

Tactic:
AffineSubspace.vectorSpan_union_of_mem_of_mem ℝ hki' hkj'

Premises used: Real, AffineSubspace.vectorSpan_union_of_mem_of_mem