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 : ℕ
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
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
⊢ n - 1 + 1 = n

Tactic:
cases 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
inst_4 : 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:
lia
-- 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 + 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:
lia
-- 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 :
  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

Tactic:
have hn : (n - 1) + 1 = n := by
    have := NeZero.ne n
    cases n <;> lia
-- 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 :
  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
rw₃ : n + 1 - 1 = n
rw₄ rw₅ : n = n
⊢ card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1

Tactic:
rw [card_compl, card_singleton, Fintype.card_fin, hn, add_tsub_cancel_right]

Premises used: Fintype.card_fin, Finset.card_compl, add_tsub_cancel_right, Finset.card_singleton
-- 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 :
  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

Tactic:
have hc : #({i}ᶜ) = (n - 1) + 1 := by
    rw [card_compl, card_singleton, Fintype.card_fin, hn, add_tsub_cancel_right]
-- 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 :
  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
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
⊢ finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = 1

Tactic:
add_left_cancel (_root_.trans h ?_)

Premises used: trans, add_left_cancel
-- 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 :
  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
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
refine :
  finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
⊢ finrank.{0, u_1} ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = 1

Tactic:
refine add_left_cancel (_root_.trans h ?_)

Premises used: trans, add_left_cancel
-- 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 :
  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
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
rw₁ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i} : Set (Fin (n + 1)))ᶜ)) + 1
rw₂ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i}ᶜ : Set (Fin (n + 1))))) + 1
rw₃ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (↑(image s.points {i}ᶜ) : Set P)) + 1
rw₄ : n = n - 1 + 1
rw₅ rw₆ : n = n
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1

Tactic:
rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]

Premises used: Fintype.card_fin, Finset.coe_singleton, Finset.coe_image, AffineIndependent.finrank_vectorSpan_image_finset, Finset.coe_compl, AffineIndependent.finrank_vectorSpan, Affine.Simplex.independent
-- 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 :
  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
hc : card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1
rw : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
rw₁ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i} : Set (Fin (n + 1)))ᶜ)) + 1
rw₂ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' (↑{i}ᶜ : Set (Fin (n + 1))))) + 1
rw₃ : n = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (↑(image s.points {i}ᶜ) : Set P)) + 1
rw₄ : n = n - 1 + 1
rw₅ rw₆ : n = n
⊢ finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank.{0, u_1} ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1

Tactic:
classical
  rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton,
    ← Finset.coe_compl, ← Finset.coe_image,
    s.independent.finrank_vectorSpan_image_finset hc, hn]

Premises used: Fintype.card_fin, Finset.coe_singleton, Finset.coe_image, Finset.coe_compl, AffineIndependent.finrank_vectorSpan, Affine.Simplex.independent
-- 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)
p : P
rw :
  vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction ↔
    p ≠ s.points i ∧
      Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
        Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
⊢ affineSpan ℝ {p, s.points i} = s.altitude i ↔
    p ≠ s.points i ∧
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p ∧
        Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (s.points '' {i}ᶜ)))ᗮ (p -ᵥ s.points i)

Tactic:
rw [eq_iff_direction_eq_of_mem (mem_affineSpan ℝ (Set.mem_insert_of_mem _ (Set.mem_singleton _)))
      (s.mem_altitude _),
    ← vsub_right_mem_direction_iff_mem (mem_affineSpan ℝ (Set.mem_range_self i)) p,
    direction_affineSpan, direction_affineSpan, direction_affineSpan]

Premises used: Set.mem_range_self, Set.mem_singleton, direction_affineSpan, Real, Set.mem_insert_of_mem, mem_affineSpan, AffineSubspace.eq_iff_direction_eq_of_mem, Affine.Simplex.mem_altitude, AffineSubspace.vsub_right_mem_direction_iff_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)
p : P
mp :
  vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction →
    p ≠ s.points i ∧
      Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
        Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
mpr :
  p ≠ s.points i ∧
      Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
        Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i) →
    vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
⊢ vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction ↔
    p ≠ s.points i ∧
      Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
        Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)

Tactic:
constructor
-- 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)
p : P
h : vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
mp : p ≠ s.points i
mp₁ :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
⊢ p ≠ s.points i ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
      Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)

Tactic:
constructor
-- 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)
p : P
h : vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
heq : p = s.points i
⊢ ⊥ = (s.altitude i).direction

Tactic:
rw [heq, Set.pair_eq_singleton, vectorSpan_singleton] at h

Premises used: vectorSpan_singleton, Set.pair_eq_singleton
-- 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)
p : P
h : vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
heq : p = s.points i
h₁ : ⊥ = (s.altitude i).direction
⊢ p = s.points i

Tactic:
rw [heq, Set.pair_eq_singleton, vectorSpan_singleton] at h

Premises used: vectorSpan_singleton, Set.pair_eq_singleton
-- 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)
p : P
h : ⊥ = (s.altitude i).direction
heq : p = s.points i
rw : finrank.{0, u_1} ℝ ↥⊥ = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ finrank.{0, u_1} ℝ ↥(s.altitude i).direction = 0

Tactic:
rw [← h, finrank_bot]

Premises used: finrank_bot
-- 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)
p : P
h : ⊥ = (s.altitude i).direction
heq : p = s.points i
⊢ finrank.{0, u_1} ℝ ↥(s.altitude i).direction = 0

Tactic:
have hd : finrank ℝ (s.altitude i).direction = 0 := by rw [← h, finrank_bot]
-- 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)
p : P
h : ⊥ = (s.altitude i).direction
heq : p = s.points i
hd : finrank.{0, u_1} ℝ ↥(s.altitude i).direction = 0
⊢ False

Tactic:
simp at hd
-- 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)
p : P
h : vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
mp : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (P := P) {p, s.points i}) (p -ᵥ s.points i)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)

Tactic:
rw [← Submodule.mem_inf, _root_.inf_comm, ← direction_altitude, ← h]

Premises used: Submodule.mem_inf, inf_comm, Affine.Simplex.direction_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)
p : P
h : vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (P := P) {p, s.points i}) (p -ᵥ s.points i)

Tactic:
vsub_mem_vectorSpan ℝ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_singleton _))

Premises used: Set.mem_singleton, vsub_mem_vectorSpan, Real, Set.mem_insert_of_mem, Set.mem_insert
-- 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)
p : P
h : vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (P := P) {p, s.points i}) (p -ᵥ s.points i)

Tactic:
exact
        vsub_mem_vectorSpan ℝ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_singleton _))

Premises used: Set.mem_singleton, vsub_mem_vectorSpan, Real, Set.mem_insert_of_mem, Set.mem_insert
-- 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)
p : P
hne : p ≠ s.points i
h :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.points i) ∧
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ (p -ᵥ s.points i)
⊢ p -ᵥ s.points i ∈ (s.altitude i).direction

Tactic:
rw [← Submodule.mem_inf, _root_.inf_comm, ← direction_altitude] at h

Premises used: Submodule.mem_inf, inf_comm, Affine.Simplex.direction_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)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
mpr : ℝ ∙ (p -ᵥ s.points i) = (s.altitude i).direction
⊢ vectorSpan ℝ (P := P) {p, s.points i} = (s.altitude i).direction

Tactic:
rw [vectorSpan_eq_span_vsub_set_left_ne ℝ (Set.mem_insert _ _),
      Set.insert_diff_of_mem _ (Set.mem_singleton _),
      Set.diff_singleton_eq_self fun h => hne (Set.mem_singleton_iff.1 h), Set.image_singleton]

Premises used: Set.mem_singleton, Real, Set.image_singleton, Set.diff_singleton_eq_self, vectorSpan_eq_span_vsub_set_left_ne, Set.insert_diff_of_mem, Set.mem_singleton_iff, Iff.mp, Set.mem_insert
-- 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)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ ℝ ∙ (p -ᵥ s.points i) = (s.altitude i).direction

Tactic:
Submodule.eq_of_le_of_finrank_eq ?_ ?_

Premises used: Submodule.eq_of_le_of_finrank_eq
-- 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)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
mpr : ℝ ∙ (p -ᵥ s.points i) ≤ (s.altitude i).direction
mpr₁ : finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.points i)) = finrank.{0, u_1} ℝ ↥(s.altitude i).direction
⊢ ℝ ∙ (p -ᵥ s.points i) = (s.altitude i).direction

Tactic:
refine Submodule.eq_of_le_of_finrank_eq ?_ ?_

Premises used: Submodule.eq_of_le_of_finrank_eq
-- 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)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
mpr : {p -ᵥ s.points i} ⊆ (↑(s.altitude i).direction : Set V)
⊢ ℝ ∙ (p -ᵥ s.points i) ≤ (s.altitude i).direction

Tactic:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- 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)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ {p -ᵥ s.points i} ⊆ (↑(s.altitude i).direction : Set V)

Tactic:
simpa using 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)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
mpr : card (α := V) (Set.toFinset {p -ᵥ s.points i}) = 1
mpr₁ : LinearIndepOn (ι := V) ℝ id {p -ᵥ s.points i}
⊢ finrank.{0, u_1} ℝ ↥(ℝ ∙ (p -ᵥ s.points i)) = finrank.{0, u_1} ℝ ↥(s.altitude i).direction

Tactic:
rw [finrank_direction_altitude, finrank_span_set_eq_card]

Premises used: finrank_span_set_eq_card, Affine.Simplex.finrank_direction_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)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ card (α := V) (Set.toFinset {p -ᵥ s.points i}) = 1

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)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ id (p -ᵥ s.points i) ≠ 0

Tactic:
simpa using hne
-- 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)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ LinearIndepOn (ι := V) ℝ id {p -ᵥ s.points i}

Tactic:
exact .singleton <| by simpa using hne
-- 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).altitudeFoot i = (s.altitudeFoot ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
⊢ (s.reindex e).altitudeFoot = s.altitudeFoot ∘ (⇑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)
h :
  Eq.{u_2 + 1} (α := P)
    (↑((((s.reindex e).faceOpposite i).orthogonalProjectionSpan :
            (a : P) → ↥(affineSpan ℝ (Set.range ((s.reindex e).faceOpposite i).points)))
          (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i))) :
      P)
    (↑(((s.faceOpposite ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)).orthogonalProjectionSpan :
            (a : P) →
              ↥(affineSpan ℝ (Set.range (s.faceOpposite ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)).points)))
          (s.points ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i))) :
      P)
⊢ (s.reindex e).altitudeFoot i = (s.altitudeFoot ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i

Tactic:
simp only [altitudeFoot, reindex_points, Function.comp_apply]

Premises used: Affine.Simplex.altitudeFoot, Affine.Simplex.reindex_points, Function.comp_apply