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
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₁
h : p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₂.direction
⊢ (p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P))) +ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₂

Tactic:
refine vadd_mem_of_mem_direction ?_ hq2

Premises used: AffineSubspace.vadd_mem_of_mem_direction
-- 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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₁
h : p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₁.direction
⊢ p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₂.direction

Tactic:
rw [← hd]
-- 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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₁
⊢ p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₁.direction

Tactic:
vsub_mem_direction hp hq1

Premises used: AffineSubspace.vsub_mem_direction
-- 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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₁
⊢ p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₁.direction

Tactic:
exact vsub_mem_direction hp hq1

Premises used: AffineSubspace.vsub_mem_direction
-- 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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₂
h : (p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P))) +ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₁
⊢ p ∈ s₁

Tactic:
rw [← vsub_vadd p hn.some]

Premises used: vsub_vadd, Set.Nonempty.some
-- 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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₂
⊢ (p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P))) +ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₁

Tactic:
vadd_mem_of_mem_direction ?_ hq1

Premises used: AffineSubspace.vadd_mem_of_mem_direction
-- 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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₂
h : p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₁.direction
⊢ (p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P))) +ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₁

Tactic:
refine vadd_mem_of_mem_direction ?_ hq1

Premises used: AffineSubspace.vadd_mem_of_mem_direction
-- 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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₂
h : p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₂.direction
⊢ p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₁.direction

Tactic:
rw [hd]
-- 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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₂
⊢ p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₂.direction

Tactic:
vsub_mem_direction hp hq2

Premises used: AffineSubspace.vsub_mem_direction
-- 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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
p : P
hq1 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₁ : Set P)
hq2 : hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ (↑s₂ : Set P)
hp : p ∈ s₂
⊢ p -ᵥ hn.some (s := (↑s₁ : Set P) ∩ (↑s₂ : Set P)) ∈ s₂.direction

Tactic:
exact vsub_mem_direction hp hq2

Premises used: AffineSubspace.vsub_mem_direction
-- 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
direction : Submodule k V
c : k
p₁ p₂ p₃ : P
hp₁ : Membership.mem (γ := Set P) {q : P | q -ᵥ p ∈ direction} p₁
hp₂ : Membership.mem (γ := Set P) {q : P | q -ᵥ p ∈ direction} p₂
hp₃ : Membership.mem (γ := Set P) {q : P | q -ᵥ p ∈ direction} p₃
⊢ Membership.mem (γ := Set P) {q : P | q -ᵥ p ∈ direction} (c • (p₁ -ᵥ p₂) +ᵥ p₃)

Tactic:
simpa [vadd_vsub_assoc] using
      direction.add_mem (direction.smul_mem c (direction.sub_mem hp₁ hp₂)) hp₃

Premises used: vadd_vsub_assoc, Submodule.sub_mem, Submodule.smul_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
p q : P
direction : Submodule k V
⊢ Membership.mem (γ := AffineSubspace k P) (mk' p direction) q ↔ q -ᵥ p ∈ direction

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- 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
direction : Submodule k V
⊢ Membership.mem (γ := AffineSubspace k P) (mk' p direction) 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
v : V
p : P
direction : Submodule k V
hv : v ∈ direction
⊢ Membership.mem (γ := AffineSubspace k P) (mk' p direction) (v +ᵥ p)

Tactic:
simpa
-- 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
direction : Submodule k V
⊢ (↑(mk' p direction) : Set P).Nonempty

Tactic:
⟨p, self_mem_mk' p direction⟩

Premises used: AffineSubspace.self_mem_mk', Set.Nonempty, Exists.intro
-- 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
direction : Submodule k V
⊢ Nonempty.{u_3 + 1} ↥(mk' p direction)

Tactic:
⟨⟨p, self_mem_mk' p direction⟩⟩

Premises used: AffineSubspace.self_mem_mk', Nonempty.intro, Subtype.mk
-- 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
direction : Submodule k V
h : ∀ (v : V), v ∈ AffineSubspace.direction (mk' p direction) ↔ v ∈ direction
⊢ AffineSubspace.direction (mk' p direction) = direction

Tactic:
ext v
-- 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
direction : Submodule k V
v : V
h :
  (∃ (p₁ : P),
      Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₁ ∧
        ∃ (p₂ : P), Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₂ ∧ v = p₁ -ᵥ p₂) ↔
    v ∈ direction
⊢ v ∈ AffineSubspace.direction (mk' p direction) ↔ v ∈ direction

Tactic:
rw [mem_direction_iff_eq_vsub (mk'_nonempty _ _)]

Premises used: AffineSubspace.mem_direction_iff_eq_vsub, AffineSubspace.mk'_nonempty
-- 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
direction : Submodule k V
v : V
h :
  (∃ (p₁ : P),
      Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₁ ∧
        ∃ (p₂ : P), Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₂ ∧ v = p₁ -ᵥ p₂) →
    v ∈ direction
h₁ :
  v ∈ direction →
    ∃ (p₁ : P),
      Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₁ ∧
        ∃ (p₂ : P), Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₂ ∧ v = p₁ -ᵥ p₂
⊢ (∃ (p₁ : P),
      Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₁ ∧
        ∃ (p₂ : P), Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₂ ∧ v = p₁ -ᵥ p₂) ↔
    v ∈ direction

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
p : P
direction : Submodule k V
p₁ : P
hp₁ : Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₁
p₂ : P
hp₂ : Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₂
⊢ p₁ -ᵥ p₂ ∈ direction

Tactic:
simpa using direction.sub_mem hp₁ hp₂

Premises used: Submodule.sub_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
p : P
direction : Submodule k V
v : V
⊢ v ∈ direction →
    ∃ (p₁ : P),
      Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₁ ∧
        ∃ (p₂ : P), Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₂ ∧ v = p₁ -ᵥ p₂

Tactic:
fun hv => ⟨v +ᵥ p, vadd_mem_mk' _ hv, p, self_mem_mk' _ _, (vadd_vsub _ _).symm⟩

Premises used: AffineSubspace.self_mem_mk', AffineSubspace.vadd_mem_mk', HVAdd.hVAdd, And.intro, Exists.intro, vadd_vsub, Eq.symm
-- 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
direction : Submodule k V
v : V
⊢ v ∈ direction →
    ∃ (p₁ : P),
      Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₁ ∧
        ∃ (p₂ : P), Membership.mem (γ := AffineSubspace k P) (mk' p direction) p₂ ∧ v = p₁ -ᵥ p₂

Tactic:
exact fun hv => ⟨v +ᵥ p, vadd_mem_mk' _ hv, p, self_mem_mk' _ _, (vadd_vsub _ _).symm⟩
-- 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
⊢ mk' p s.direction = s

Tactic:
ext_of_direction_eq (direction_mk' p s.direction) ⟨p, Set.mem_inter (self_mem_mk' _ _) hp⟩

Premises used: AffineSubspace.self_mem_mk', Set.mem_inter, Exists.intro, AffineSubspace.ext_of_direction_eq, AffineSubspace.direction_mk', AffineSubspace.direction
-- 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₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
hp : p = v +ᵥ p₁
rw : v +ᵥ p₁ ∈ (↑s₁ : Set P)
⊢ p ∈ (↑s₁ : Set P)

Tactic:
rw [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 : Set P
s₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
hp : p = v +ᵥ p₁
⊢ p₁ ∈ (↑s₁ : Set P)

Tactic:
have hp₁s₁ : p₁ ∈ (s₁ : Set P) := Set.mem_of_mem_of_subset 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 : Set P
s₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ (↑s₁ : Set P)
⊢ v +ᵥ p₁ ∈ (↑s₁ : Set P)

Tactic:
vadd_mem_of_mem_direction ?_ hp₁s₁

Premises used: AffineSubspace.vadd_mem_of_mem_direction
-- 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₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ (↑s₁ : Set P)
refine : v ∈ s₁.direction
⊢ v +ᵥ p₁ ∈ (↑s₁ : Set P)

Tactic:
refine vadd_mem_of_mem_direction ?_ hp₁s₁

Premises used: AffineSubspace.vadd_mem_of_mem_direction
-- 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₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ (↑s₁ : Set P)
⊢ vectorSpan k s ≤ s₁.direction

Tactic:
have hs : vectorSpan k s ≤ s₁.direction := vectorSpan_mono k 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 : Set P
s₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ (↑s₁ : Set P)
hs : vectorSpan k s ≤ s₁.direction
⊢ ∀ ⦃x : V⦄, Membership.mem (γ := Submodule k V) (vectorSpan k s) x → x ∈ s₁.direction

Tactic:
rw [SetLike.le_def] at hs

Premises used: SetLike.le_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₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ (↑s₁ : Set P)
hs : ∀ ⦃x : V⦄, Membership.mem (γ := Submodule k V) (vectorSpan k s) x → x ∈ s₁.direction
⊢ v ∈ (↑s₁.direction : Set V)

Tactic:
Set.mem_of_mem_of_subset hv hs

Premises used: Set.mem_of_mem_of_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
s₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ (↑s₁ : Set P)
hs : ∀ ⦃x : V⦄, Membership.mem (γ := Submodule k V) (vectorSpan k s) x → x ∈ s₁.direction
⊢ v ∈ (↑s₁.direction : Set V)

Tactic:
exact Set.mem_of_mem_of_subset hv hs

Premises used: Set.mem_of_mem_of_subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
p : Submodule k V
x : V
⊢ x ∈ p.toAffineSubspace ↔ x ∈ p

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Submodule k V
h : ∀ (x : V), x ∈ s.toAffineSubspace.direction ↔ x ∈ s
⊢ s.toAffineSubspace.direction = s

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Submodule k V
x : V
⊢ x ∈ s.toAffineSubspace.direction ↔ x ∈ s

Tactic:
simp [← s.toAffineSubspace.vadd_mem_iff_mem_direction _ s.zero_mem]

Premises used: Submodule.zero_mem, AffineSubspace.vadd_mem_iff_mem_direction
-- 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
⊢ (↑(affineSpan k s) : Set P) = spanPoints k s

Tactic:
rfl

Premises used: setOf, spanPoints, 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
p : P
s : Set P
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p ↔
    ∃ p₁ ∈ s, ∃ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v ∧ p = v +ᵥ p₁

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, 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 ⊆ (↑(affineSpan k s) : Set P)

Tactic:
subset_spanPoints k s

Premises used: setOf, spanPoints, 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
a : LE.le (α := Submodule k V) (AffineSubspace.direction (affineSpan k s)) (vectorSpan k s)
a₁ : LE.le (α := Submodule k V) (vectorSpan k s) (AffineSubspace.direction (affineSpan k s))
⊢ Eq (α := Submodule k V) (AffineSubspace.direction (affineSpan k s)) (vectorSpan k s)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
⊢ LE.le (α := Submodule k V) (AffineSubspace.direction (affineSpan k s)) (vectorSpan k s)

Tactic:
Submodule.span_le.2 ?_

Premises used: Iff.mpr, Set.Mem, Submodule.span_le
-- 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
a : (↑(affineSpan k s) : Set P) -ᵥ (↑(affineSpan k s) : Set P) ⊆ (↑(vectorSpan k s) : Set V)
⊢ LE.le (α := Submodule k V) (AffineSubspace.direction (affineSpan k s)) (vectorSpan k s)

Tactic:
refine Submodule.span_le.2 ?_

Premises used: Iff.mpr, Submodule.span_le
-- 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
v₁ : V
hv₁ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₁
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₂
hp₃ : p₃ = v₂ +ᵥ p₄
a : Membership.mem (γ := Submodule k V) (vectorSpan k s) (v₁ + (p₂ -ᵥ p₄) - v₂)
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁ -ᵥ p₃)

Tactic:
rw [hp₁, hp₃, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc]

Premises used: vadd_vsub_assoc, vsub_vadd_eq_vsub_sub
-- 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
v₁ : V
hv₁ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₁
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₂
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (v₁ + (p₂ -ᵥ p₄) - v₂)

Tactic:
(vectorSpan k s).sub_mem ((vectorSpan k s).add_mem hv₁ (vsub_mem_vectorSpan k hp₂ hp₄)) hv₂

Premises used: vsub_mem_vectorSpan, vectorSpan, Submodule.sub_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
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₁
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : Membership.mem (γ := Submodule k V) (vectorSpan k s) v₂
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (v₁ + (p₂ -ᵥ p₄) - v₂)

Tactic:
exact
      (vectorSpan k s).sub_mem ((vectorSpan k s).add_mem hv₁ (vsub_mem_vectorSpan k hp₂ hp₄)) hv₂

Premises used: vsub_mem_vectorSpan, vectorSpan, Submodule.sub_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
⊢ LE.le (α := Submodule k V) (vectorSpan k s) (AffineSubspace.direction (affineSpan k s))

Tactic:
vectorSpan_mono k (subset_spanPoints k s)

Premises used: Set.Mem, vectorSpan_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
⊢ LE.le (α := Submodule k V) (vectorSpan k s) (AffineSubspace.direction (affineSpan k s))

Tactic:
exact vectorSpan_mono k (subset_spanPoints k s)

Premises used: vectorSpan_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
p : P
s : Set P
hp : p ∈ s
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p

Tactic:
mem_spanPoints k p s hp

Premises used: Set.Mem, mem_spanPoints, setOf, spanPoints
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Set V
h : ∀ (x : V), x ∈ (↑(vectorSpan k s) : Set V) + s ↔ x ∈ (↑(affineSpan k s) : Set V)
⊢ (↑(vectorSpan k s) : Set V) + s = (↑(affineSpan k s) : Set V)

Tactic:
ext