awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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 ∅) ⊥
rw₂ rw₃ : Eq.{u_2 + 1} (α := Submodule k V) ⊥ ⊥
⊢ Eq (α := Submodule k V) (vectorSpan.{u_1, u_2, u_3} k (P := P) ∅) ⊥

Tactic:
rw [vectorSpan_def, vsub_empty, Submodule.span_empty]

Premises used: Set.vsub_empty, vectorSpan_def, Submodule.span_empty
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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 : P
⊢ Eq (α := Submodule k V) (vectorSpan k (P := P) {p}) ⊥

Tactic:
simp [vectorSpan_def]

Premises used: vectorSpan_def
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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 -ᵥ s ⊆ (↑(vectorSpan k s) : Set V)

Tactic:
Submodule.subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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₁ ∈ s
hp₂ : p₂ ∈ s
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁ -ᵥ p₂)

Tactic:
vsub_set_subset_vectorSpan k s (vsub_mem_vsub hp₁ hp₂)

Premises used: Set.vsub_mem_vsub, vsub_set_subset_vectorSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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) ∅) ⊥
inr : ∀ (p : P) (h : Set.Subsingleton (α := P) {p}), Eq (α := Submodule k V) (vectorSpan k (P := P) {p}) ⊥
⊢ Eq (α := Submodule k V) (vectorSpan k s) ⊥

Tactic:
rcases h.eq_empty_or_singleton with rfl | ⟨p, rfl⟩

Premises used: Set.Subsingleton.eq_empty_or_singleton, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
h : Set.Subsingleton.{u_3} (α := P) ∅
⊢ Eq (α := Submodule k V) (vectorSpan.{u_1, u_2, u_3} k (P := P) ∅) ⊥

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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 : P
h : Set.Subsingleton (α := P) {p}
⊢ Eq (α := Submodule k V) (vectorSpan k (P := P) {p}) ⊥

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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

Tactic:
⟨fun h ↦ ?_, vectorSpan_of_subsingleton _⟩

Premises used: Iff.intro, vectorSpan_of_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
refine : ∀ (h : Eq (α := Submodule k V) (vectorSpan k s) ⊥), s.Subsingleton
⊢ Eq (α := Submodule k V) (vectorSpan k s) ⊥ ↔ s.Subsingleton

Tactic:
refine ⟨fun h ↦ ?_, vectorSpan_of_subsingleton _⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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) ⊥
by_contra : ∀ (hns : ¬s.Subsingleton), False
⊢ s.Subsingleton

Tactic:
by_contra hns
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
⊢ s.Nontrivial

Tactic:
rw [Set.not_subsingleton_iff] at hns

Premises used: Set.not_subsingleton_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
obtain : ∀ (p : P) (hp : p ∈ s) (q : P) (hq : q ∈ s) (hpq : p ≠ q), False
⊢ False

Tactic:
obtain ⟨p, hp, q, hq, hpq⟩ := hns
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p -ᵥ q)

Tactic:
have hpq' := vsub_mem_vectorSpan k hp hq
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
hpq' : Membership.mem (γ := Submodule k V) (vectorSpan k s) (p -ᵥ q)
⊢ False

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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 ⊆ spanPoints k s

Tactic:
fun p => mem_spanPoints k p s

Premises used: mem_spanPoints, Set.Subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
mpr : s.Nonempty → (spanPoints k s).Nonempty
⊢ (spanPoints k s).Nonempty ↔ s.Nonempty

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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 : ¬s.Nonempty → ¬(spanPoints k s).Nonempty
⊢ (spanPoints k s).Nonempty → s.Nonempty

Tactic:
contrapose
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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 : s = ∅ → spanPoints k s = ∅
⊢ ¬s.Nonempty → ¬(spanPoints k s).Nonempty

Tactic:
rw [Set.not_nonempty_iff_eq_empty, Set.not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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 = ∅
⊢ spanPoints k s = ∅

Tactic:
simp [h, spanPoints]

Premises used: spanPoints
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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

Tactic:
fun h => h.mono (subset_spanPoints _ _)

Premises used: Set.Nonempty.mono, subset_spanPoints
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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

Tactic:
exact fun h => h.mono (subset_spanPoints _ _)
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
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
⊢ v +ᵥ p ∈ spanPoints k s

Tactic:
rcases hp with ⟨p₂, ⟨hp₂, ⟨v₂, ⟨hv₂, hv₂p⟩⟩⟩⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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₂
rw : (v + v₂) +ᵥ p₂ ∈ spanPoints k s
⊢ v +ᵥ p ∈ spanPoints k s

Tactic:
rw [hv₂p, vadd_vadd]

Premises used: vadd_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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 + v₂) +ᵥ p₂ ∈ spanPoints k s

Tactic:
⟨p₂, hp₂, v + v₂, (vectorSpan k s).add_mem hv hv₂, rfl⟩

Premises used: vectorSpan, Set.Mem, setOf, spanPoints, HAdd.hAdd, And.intro, Exists.intro, rfl, Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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 + v₂) +ᵥ p₂ ∈ spanPoints k s

Tactic:
exact ⟨p₂, hp₂, v + v₂, (vectorSpan k s).add_mem hv hv₂, rfl⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
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₂)
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁ -ᵥ p₂)

Tactic:
rcases hp₁ with ⟨p₁a, ⟨hp₁a, ⟨v₁, ⟨hv₁, hv₁p⟩⟩⟩⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
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₂)
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁ -ᵥ p₂)

Tactic:
rcases hp₂ with ⟨p₂a, ⟨hp₂a, ⟨v₂, ⟨hv₂, hv₂p⟩⟩⟩⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
rw : Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁a -ᵥ p₂a + (v₁ - v₂))
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁ -ᵥ p₂)

Tactic:
rw [hv₁p, hv₂p, vsub_vadd_eq_vsub_sub (v₁ +ᵥ p₁a), vadd_vsub_assoc, add_comm, add_sub_assoc]

Premises used: add_sub_assoc, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, add_comm, HVAdd.hVAdd
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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) (v₁ - v₂)

Tactic:
have hv₁v₂ : v₁ - v₂ ∈ vectorSpan k s := (vectorSpan k s).sub_mem hv₁ hv₂
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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₂))

Tactic:
(vectorSpan k s).add_mem ?_ hv₁v₂

Premises used: vectorSpan, Set.Mem, Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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₂)
refine : Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁a -ᵥ p₂a)
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁a -ᵥ p₂a + (v₁ - v₂))

Tactic:
refine (vectorSpan k s).add_mem ?_ hv₁v₂

Premises used: vectorSpan, Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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)

Tactic:
vsub_mem_vectorSpan k hp₁a hp₂a

Premises used: vsub_mem_vectorSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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)

Tactic:
exact vsub_mem_vectorSpan k hp₁a hp₂a

Premises used: vsub_mem_vectorSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
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
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
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 }
⊢ { carrier := carrier, smul_vsub_vadd_mem := smul_vsub_vadd_mem : AffineSubspace k P } = q

Tactic:
cases q
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
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_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
h :
  { 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:
congr
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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 : P
s : AffineSubspace k P
⊢ p ∈ (↑s : Set P) ↔ p ∈ s

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
⊢ s.direction = vectorSpan k (↑s : Set P)

Tactic:
rfl

Premises used: AffineSubspace.direction, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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)
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)
⊢ 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)

Tactic:
rw [← vadd_vsub_assoc]

Premises used: vadd_vsub_assoc
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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)

Tactic:
vsub_mem_vsub ?_ hp₄

Premises used: Set.vsub_mem_vsub
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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)
refine : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂) 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)

Tactic:
refine vsub_mem_vsub ?_ hp₄

Premises used: Set.vsub_mem_vsub
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s.carrier

Tactic:
s.smul_vsub_vadd_mem 1 hp₁ hp₂ hp₃

Premises used: AffineSubspace.smul_vsub_vadd_mem, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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)
h₁ : (fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂ = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p₁ -ᵥ p₂)
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) ((fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂) p₃ ∈ (↑s : Set P)

Tactic:
convert! s.smul_vsub_vadd_mem 1 hp₁ hp₂ hp₃

Premises used: AffineSubspace.smul_vsub_vadd_mem, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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)
h₁ h₂ : (fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂ = p₁ -ᵥ p₂
⊢ (fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂ = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (p₁ -ᵥ p₂)

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
obtain : ∀ (p : P) (hp : p ∈ (↑s : Set P)), 0 ∈ (↑s : Set P) -ᵥ (↑s : Set P)
⊢ 0 ∈ (↑s : Set P) -ᵥ (↑s : Set P)

Tactic:
obtain ⟨p, hp⟩ := h
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
p : P
hp : p ∈ (↑s : Set P)
⊢ 0 ∈ (↑s : Set P) -ᵥ (↑s : Set P)

Tactic:
vsub_self p ▸ vsub_mem_vsub hp hp

Premises used: Set.Mem, Eq.rec, Set.vsub_mem_vsub, vsub_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
p : P
hp : p ∈ (↑s : Set P)
⊢ 0 ∈ (↑s : Set P) -ᵥ (↑s : Set P)

Tactic:
exact vsub_self p ▸ vsub_mem_vsub hp hp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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)
rw : (c • (p₁ -ᵥ p₂) +ᵥ p₂) -ᵥ p₂ ∈ (↑s : Set P) -ᵥ (↑s : Set P)
⊢ HSMul.hSMul (β := V) c ((fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂) ∈ (↑s : Set P) -ᵥ (↑s : Set P)

Tactic:
rw [← vadd_vsub (c • (p₁ -ᵥ p₂)) p₂]

Premises used: VSub.vsub, vadd_vsub, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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)

Tactic:
vsub_mem_vsub ?_ hp₂

Premises used: Set.vsub_mem_vsub