awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬(↑r₁ : k) = r₂
⊢ False
have h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
Tactic: have h₁₂ : (r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃} := by
      rw [hr₁, hr₂, add_comm, vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, neg_mem_iff, ← hr₃]
      exact smul_vsub_mem_vectorSpan_pair _ _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬(↑r₁ : k) = r₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))
have rw : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₃ -ᵥ p₁))
Tactic: rw [add_comm, ← smul_add, vsub_add_vsub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬(↑r₁ : k) = r₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
⊢ False
have h₁₁ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))
Tactic: have h₁₁ : (r₁ : k) • (p₂ -ᵥ p₁) + (r₁ : k) • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃} := by
      rw [add_comm, ← smul_add, vsub_add_vsub_cancel]
      exact smul_vsub_rev_mem_vectorSpan_pair _ _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬(↑r₁ : k) = r₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
h₁₁ :
  Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))
⊢ False
have h₂₁ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((r₂ - (↑r₁ : k)) • (p₃ -ᵥ p₂))
Tactic: have h₂₁ : (r₂ - r₁) • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃} := by
      simpa [sub_smul] using sub_mem h₁₂ h₁₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬(↑r₁ : k) = r₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
h₁₁ :
  Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))
h₂₁ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((r₂ - (↑r₁ : k)) • (p₃ -ᵥ p₂))
⊢ r₂ - (↑r₁ : k) ≠ 0
have rwa : r₂ ≠ (↑r₁ : k)
Tactic: rwa [sub_ne_zero, ne_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬(↑r₁ : k) = r₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
h₁₁ :
  Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))
h₂₁ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((r₂ - (↑r₁ : k)) • (p₃ -ᵥ p₂))
rwa : r₂ ≠ (↑r₁ : k)
⊢ r₂ - (↑r₁ : k) ≠ 0
have rwa₁ : (↑r₁ : k) ≠ r₂
Tactic: rwa [sub_ne_zero, ne_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ affineSpan k {p₁, p₃}
r₁ : kˣ
hr₁ : (↑r₁ : k) • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬(↑r₁ : k) = r₂
h₁₂ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂))
h₁₁ :
  Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((↑r₁ : k) • (p₂ -ᵥ p₁) + (↑r₁ : k) • (p₃ -ᵥ p₂))
h₂₁ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₃}) ((r₂ - (↑r₁ : k)) • (p₃ -ᵥ p₂))
⊢ False
have h₂₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₃}) p₂
Tactic: rw [Submodule.smul_mem_iff _ (by rwa [sub_ne_zero, ne_comm]), ← direction_affineSpan,
      vsub_left_mem_direction_iff_mem (right_mem_affineSpan_pair _ _ _)] at h₂₁
Cleared hypotheses: h₂₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
⊢ Eq (α := Submodule k V) (vectorSpan.{u_1, u_2, u_3} k (P := P) ∅) ⊥
have rw : Eq (α := Submodule k V) (Submodule.span k (VSub.vsub.{u_2, u_3} (P := Set P) ∅ ∅)) ⊥
Tactic: rw [vectorSpan_def, vsub_empty, Submodule.span_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
rw : Eq (α := Submodule k V) (Submodule.span k (VSub.vsub.{u_2, u_3} (P := Set P) ∅ ∅)) ⊥
⊢ Eq (α := Submodule k V) (vectorSpan.{u_1, u_2, u_3} k (P := P) ∅) ⊥
have rw₁ : Eq.{u_2 + 1} (α := Submodule k V) (Submodule.span k ∅) ⊥
Tactic: rw [vectorSpan_def, vsub_empty, Submodule.span_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
rw : Eq (α := Submodule k V) (Submodule.span k (VSub.vsub.{u_2, u_3} (P := Set P) ∅ ∅)) ⊥
rw₁ : Eq.{u_2 + 1} (α := Submodule k V) (Submodule.span k ∅) ⊥
⊢ Eq (α := Submodule k V) (vectorSpan.{u_1, u_2, u_3} k (P := P) ∅) ⊥
have rw₂ : Eq.{u_2 + 1} (α := Submodule k V) ⊥ ⊥
Tactic: rw [vectorSpan_def, vsub_empty, Submodule.span_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : s.Subsingleton
⊢ Eq (α := Submodule k V) (vectorSpan k s) ⊥
have inl : ∀ (h : Set.Subsingleton.{u_3} (α := P) ∅), Eq (α := Submodule k V) (vectorSpan.{u_1, u_2, u_3} k (P := P) ∅) ⊥
Tactic: rcases h.eq_empty_or_singleton with rfl | ⟨p, rfl⟩
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : s.Subsingleton
inl : ∀ (h : Set.Subsingleton.{u_3} (α := P) ∅), Eq (α := Submodule k V) (vectorSpan.{u_1, u_2, u_3} k (P := P) ∅) ⊥
⊢ Eq (α := Submodule k V) (vectorSpan k s) ⊥
have inr : ∀ (p : P) (h : Set.Subsingleton (α := P) {p}), Eq (α := Submodule k V) (vectorSpan k (P := P) {p}) ⊥
Tactic: rcases h.eq_empty_or_singleton with rfl | ⟨p, rfl⟩
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
⊢ Eq (α := Submodule k V) (vectorSpan k s) ⊥ ↔ s.Subsingleton
have refine : ∀ (h : Eq (α := Submodule k V) (vectorSpan k s) ⊥), s.Subsingleton
Tactic: refine ⟨fun h ↦ ?_, vectorSpan_of_subsingleton _⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Eq (α := Submodule k V) (vectorSpan k s) ⊥
⊢ s.Subsingleton
have by_contra : ∀ (hns : ¬s.Subsingleton), False
Tactic: by_contra hns
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Eq (α := Submodule k V) (vectorSpan k s) ⊥
hns : ¬s.Subsingleton
⊢ False
have hns₁ : s.Nontrivial
Tactic: rw [Set.not_subsingleton_iff] at hns
Cleared hypotheses: hns
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Eq (α := Submodule k V) (vectorSpan k s) ⊥
hns : s.Nontrivial
⊢ False
have obtain : ∀ (p : P) (hp : p ∈ s) (q : P) (hq : q ∈ s) (hpq : p ≠ q), False
Tactic: obtain ⟨p, hp, q, hq, hpq⟩ := hns
Cleared hypotheses: hns
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Eq (α := Submodule k V) (vectorSpan k s) ⊥
p : P
hp : p ∈ s
q : P
hq : q ∈ s
hpq : p ≠ q
⊢ False
have hpq' : Membership.mem (γ := Submodule k V) (vectorSpan k s) (p -ᵥ q)
Tactic: have hpq' := vsub_mem_vectorSpan k hp hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
⊢ (spanPoints k s).Nonempty ↔ s.Nonempty
have mp : (spanPoints k s).Nonempty → s.Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
mp : (spanPoints k s).Nonempty → s.Nonempty
⊢ (spanPoints k s).Nonempty ↔ s.Nonempty
have mpr : s.Nonempty → (spanPoints k s).Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
⊢ (spanPoints k s).Nonempty → s.Nonempty
have mp : ¬s.Nonempty → ¬(spanPoints k s).Nonempty
Tactic: contrapose
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
⊢ ¬s.Nonempty → ¬(spanPoints k s).Nonempty
have mp : s = ∅ → spanPoints k s = ∅
Tactic: rw [Set.not_nonempty_iff_eq_empty, Set.not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
v : V
hp : p ∈ spanPoints k s
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
⊢ v +ᵥ p ∈ spanPoints k s
have rcases : ∀ (p₂ : P) (hp₂ : p₂ ∈ s) (v₂ : V) (hv₂ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₂)
  (hv₂p : p = v₂ +ᵥ p₂), v +ᵥ p ∈ spanPoints k s
Tactic: rcases hp with ⟨p₂, ⟨hp₂, ⟨v₂, ⟨hv₂, hv₂p⟩⟩⟩⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
p₂ : P
hp₂ : p₂ ∈ s
v₂ : V
hv₂ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₂
hv₂p : p = v₂ +ᵥ p₂
⊢ v +ᵥ p ∈ spanPoints k s
have rw : (v + v₂) +ᵥ p₂ ∈ spanPoints k s
Tactic: rw [hv₂p, vadd_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₁ p₂ : P
hp₁ : p₁ ∈ spanPoints k s
hp₂ : p₂ ∈ spanPoints k s
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁ -ᵥ p₂)
have rcases : ∀ (p₁a : P) (hp₁a : p₁a ∈ s) (v₁ : V) (hv₁ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₁)
  (hv₁p : p₁ = v₁ +ᵥ p₁a), Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁ -ᵥ p₂)
Tactic: rcases hp₁ with ⟨p₁a, ⟨hp₁a, ⟨v₁, ⟨hv₁, hv₁p⟩⟩⟩⟩
Cleared hypotheses: hp₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₁ p₂ : P
hp₂ : p₂ ∈ spanPoints k s
p₁a : P
hp₁a : p₁a ∈ s
v₁ : V
hv₁ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₁
hv₁p : p₁ = v₁ +ᵥ p₁a
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁ -ᵥ p₂)
have rcases : ∀ (p₂a : P) (hp₂a : p₂a ∈ s) (v₂ : V) (hv₂ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₂)
  (hv₂p : p₂ = v₂ +ᵥ p₂a), Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁ -ᵥ p₂)
Tactic: rcases hp₂ with ⟨p₂a, ⟨hp₂a, ⟨v₂, ⟨hv₂, hv₂p⟩⟩⟩⟩
Cleared hypotheses: hp₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₁ p₂ p₁a : P
hp₁a : p₁a ∈ s
v₁ : V
hv₁ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₁
hv₁p : p₁ = v₁ +ᵥ p₁a
p₂a : P
hp₂a : p₂a ∈ s
v₂ : V
hv₂ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₂
hv₂p : p₂ = v₂ +ᵥ p₂a
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁ -ᵥ p₂)
have rw : Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁a -ᵥ p₂a + (v₁ - v₂))
Tactic: rw [hv₁p, hv₂p, vsub_vadd_eq_vsub_sub (v₁ +ᵥ p₁a), vadd_vsub_assoc, add_comm, add_sub_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₁ p₂ p₁a : P
hp₁a : p₁a ∈ s
v₁ : V
hv₁ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₁
hv₁p : p₁ = v₁ +ᵥ p₁a
p₂a : P
hp₂a : p₂a ∈ s
v₂ : V
hv₂ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₂
hv₂p : p₂ = v₂ +ᵥ p₂a
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁a -ᵥ p₂a + (v₁ - v₂))
have hv₁v₂ : Membership.mem (γ := Submodule k V) (vectorSpan k s) (v₁ - v₂)
Tactic: have hv₁v₂ : v₁ - v₂ ∈ vectorSpan k s := (vectorSpan k s).sub_mem hv₁ hv₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p₁ p₂ p₁a : P
hp₁a : p₁a ∈ s
v₁ : V
hv₁ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₁
hv₁p : p₁ = v₁ +ᵥ p₁a
p₂a : P
hp₂a : p₂a ∈ s
v₂ : V
hv₂ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₂
hv₂p : p₂ = v₂ +ᵥ p₂a
hv₁v₂ : Membership.mem (γ := Submodule k V) (vectorSpan k s) (v₁ - v₂)
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁a -ᵥ p₂a + (v₁ - v₂))
have refine : Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁a -ᵥ p₂a)
Tactic: refine (vectorSpan k s).add_mem ?_ hv₁v₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p q : AffineSubspace k P
h : p.carrier = q.carrier
⊢ p = q
have mk : ∀ (carrier : Set P)
  (smul_vsub_vadd_mem :
    ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier → p₂ ∈ carrier → p₃ ∈ carrier → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier),
  { carrier := carrier, smul_vsub_vadd_mem := smul_vsub_vadd_mem : AffineSubspace k P }.carrier = q.carrier →
    { carrier := carrier, smul_vsub_vadd_mem := smul_vsub_vadd_mem : AffineSubspace k P } = q
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
q : AffineSubspace k P
carrier : Set P
smul_vsub_vadd_mem :
  ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier → p₂ ∈ carrier → p₃ ∈ carrier → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier
h : { carrier := carrier, smul_vsub_vadd_mem := smul_vsub_vadd_mem : AffineSubspace k P }.carrier = q.carrier
⊢ { carrier := carrier, smul_vsub_vadd_mem := smul_vsub_vadd_mem : AffineSubspace k P } = q
have mk : ∀ (carrier_1 : Set P)
  (smul_vsub_vadd_mem_1 :
    ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier_1 → p₂ ∈ carrier_1 → p₃ ∈ carrier_1 → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier_1),
  { carrier := carrier, smul_vsub_vadd_mem := smul_vsub_vadd_mem : AffineSubspace k P }.carrier =
      { carrier := carrier_1, smul_vsub_vadd_mem := smul_vsub_vadd_mem_1 : AffineSubspace k P }.carrier →
    { carrier := carrier, smul_vsub_vadd_mem := smul_vsub_vadd_mem : AffineSubspace k P } =
      { carrier := carrier_1, smul_vsub_vadd_mem := smul_vsub_vadd_mem_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s : Set P)
p₃ : P
hp₃ : p₃ ∈ (↑s : Set P)
p₄ : P
hp₄ : p₄ ∈ (↑s : Set P)
⊢ HAdd.hAdd (α := V) ((fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂) ((fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₃ p₄) ∈
    (↑s : Set P) -ᵥ (↑s : Set P)
have rw : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂) p₃ -ᵥ p₄ ∈ (↑s : Set P) -ᵥ (↑s : Set P)
Tactic: rw [← vadd_vsub_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s : Set P)
p₃ : P
hp₃ : p₃ ∈ (↑s : Set P)
p₄ : P
hp₄ : p₄ ∈ (↑s : Set P)
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂) p₃ -ᵥ p₄ ∈ (↑s : Set P) -ᵥ (↑s : Set P)
have refine : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂) p₃ ∈ (↑s : Set P)
Tactic: refine vsub_mem_vsub ?_ hp₄
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s : Set P)
p₃ : P
hp₃ : p₃ ∈ (↑s : Set P)
p₄ : P
hp₄ : p₄ ∈ (↑s : Set P)
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂) p₃ ∈ (↑s : Set P)
have h₁ : (fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂ = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p₁ -ᵥ p₂)
Tactic: convert! s.smul_vsub_vadd_mem 1 hp₁ hp₂ hp₃
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s : Set P)
p₃ : P
hp₃ : p₃ ∈ (↑s : Set P)
p₄ : P
hp₄ : p₄ ∈ (↑s : Set P)
⊢ (fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂ = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p₁ -ᵥ p₂)
have h₁ : (fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂ = p₁ -ᵥ p₂
Tactic: rw [one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
⊢ 0 ∈ (↑s : Set P) -ᵥ (↑s : Set P)
have obtain : ∀ (p : P) (hp : p ∈ (↑s : Set P)), 0 ∈ (↑s : Set P) -ᵥ (↑s : Set P)
Tactic: obtain ⟨p, hp⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
c : k
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s : Set P)
⊢ HSMul.hSMul (β := V) c ((fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂) ∈ (↑s : Set P) -ᵥ (↑s : Set P)
have rw : (c • (p₁ -ᵥ p₂) +ᵥ p₂) -ᵥ p₂ ∈ (↑s : Set P) -ᵥ (↑s : Set P)
Tactic: rw [← vadd_vsub (c • (p₁ -ᵥ p₂)) p₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
c : k
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s : Set P)
⊢ (c • (p₁ -ᵥ p₂) +ᵥ p₂) -ᵥ p₂ ∈ (↑s : Set P) -ᵥ (↑s : Set P)
have refine : c • (p₁ -ᵥ p₂) +ᵥ p₂ ∈ (↑s : Set P)
Tactic: refine vsub_mem_vsub ?_ hp₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
⊢ directionOfNonempty h = s.direction
have refine : directionOfNonempty h ≤ s.direction
Tactic: refine le_antisymm ?_ (Submodule.span_le.2 Set.Subset.rfl)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
v : V
⊢ v ∈ s.direction ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂
have rw : (∃ x ∈ (↑s : Set P), ∃ y ∈ (↑s : Set P), x -ᵥ y = v) ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂
Tactic: rw [← SetLike.mem_coe, coe_direction_eq_vsub_set h, Set.mem_vsub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ s.direction
p : P
hp : p ∈ s
⊢ v +ᵥ p ∈ s
have rw : ∀ (hv : ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂) {p : P} (hp : p ∈ s), v +ᵥ p ∈ s
Tactic: rw [mem_direction_iff_eq_vsub ⟨p, hp⟩] at hv
Cleared hypotheses: hv, p, hp