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 : Set P
p : (x : P) → Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) u) (v : P)
    (hv : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) v) (w : P)
    (hw : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) w),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x
⊢ ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x), p x hx

Tactic:
affineSpan_induction h ?mem ?smul_vsub_vadd

Premises used: affineSpan_induction
-- 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 : (x : P) → Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) u) (v : P)
    (hv : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) v) (w : P)
    (hw : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) w),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x
mem₁ : ∀ x ∈ s, ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x), p x hx
smul_vsub_vadd₁ :
  ∀ (c : k) (u v w : P),
    (∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) u), p u hx) →
      (∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) v), p v hx) →
        (∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) w), p w hx) →
          ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) (c • (u -ᵥ v) +ᵥ w)),
            p (c • (u -ᵥ v) +ᵥ w) hx
⊢ ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x), p x hx

Tactic:
refine affineSpan_induction h ?mem ?smul_vsub_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 : (x : P) → Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) u) (v : P)
    (hv : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) v) (w : P)
    (hw : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) w),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x
⊢ ∀ x ∈ s, ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x), p x hx

Tactic:
fun y hy ↦ ⟨subset_affineSpan _ _ hy, mem y hy⟩

Premises used: subset_affineSpan, 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
s : Set P
p : (x : P) → Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) u) (v : P)
    (hv : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) v) (w : P)
    (hw : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) w),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x
⊢ ∀ x ∈ s, ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x), p x hx

Tactic:
exact fun y hy ↦ ⟨subset_affineSpan _ _ hy, mem y hy⟩
-- 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 : (x : P) → Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) u) (v : P)
    (hv : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) v) (w : P)
    (hw : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) w),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x
⊢ ∀ (c : k) (u v w : P),
    (∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) u), p u hx) →
      (∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) v), p v hx) →
        (∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) w), p w hx) →
          ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) (c • (u -ᵥ v) +ᵥ w)),
            p (c • (u -ᵥ v) +ᵥ w) hx

Tactic:
fun c u v w hu hv hw ↦
      hu.elim fun hu' hu ↦ hv.elim fun hv' hv ↦ hw.elim fun hw' hw ↦
        ⟨AffineSubspace.smul_vsub_vadd_mem _ _ hu' hv' hw',
              smul_vsub_vadd _ _ _ _ _ _ _ hu hv hw⟩

Premises used: AffineSubspace.smul_vsub_vadd_mem, affineSpan, Exists.intro, Exists.elim
-- 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 : (x : P) → Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) u) (v : P)
    (hv : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) v) (w : P)
    (hw : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) w),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x
⊢ ∀ (c : k) (u v w : P),
    (∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) u), p u hx) →
      (∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) v), p v hx) →
        (∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) w), p w hx) →
          ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) (c • (u -ᵥ v) +ᵥ w)),
            p (c • (u -ᵥ v) +ᵥ w) hx

Tactic:
exact fun c u v w hu hv hw ↦
      hu.elim fun hu' hu ↦ hv.elim fun hv' hv ↦ hw.elim fun hw' hw ↦
        ⟨AffineSubspace.smul_vsub_vadd_mem _ _ hu' hv' hw',
              smul_vsub_vadd _ _ _ _ _ _ _ hu hv hw⟩
-- 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₂ : P
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) (p₁ -ᵥ p₂)

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

Premises used: Set.mem_singleton, vsub_mem_vectorSpan, Set.mem_insert_of_mem, Set.mem_insert
-- 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₂ : P
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) (p₂ -ᵥ p₁)

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

Premises used: Set.mem_singleton, vsub_mem_vectorSpan, Set.mem_insert_of_mem, Set.mem_insert
-- 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
r : k
p₁ p₂ : P
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) (r • (p₁ -ᵥ p₂))

Tactic:
Submodule.smul_mem _ _ (vsub_mem_vectorSpan_pair k p₁ p₂)

Premises used: vsub_mem_vectorSpan_pair, Set.Mem, Submodule.smul_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
r : k
p₁ p₂ : P
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) (r • (p₂ -ᵥ p₁))

Tactic:
Submodule.smul_mem _ _ (vsub_rev_mem_vectorSpan_pair k p₁ p₂)

Premises used: Set.Mem, vsub_rev_mem_vectorSpan_pair, Submodule.smul_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₂ : P
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₁

Tactic:
mem_affineSpan _ (Set.mem_insert _ _)

Premises used: mem_affineSpan, Set.mem_insert
-- 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₂ : P
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₂

Tactic:
mem_affineSpan _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))

Premises used: Set.mem_singleton, Set.mem_insert_of_mem, mem_affineSpan
-- 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₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
rw : p₁ ∈ (↑s : Set P) ∧ p₂ ∈ (↑s : Set P)
⊢ affineSpan k {p₁, p₂} ≤ s

Tactic:
rw [affineSpan_le, Set.insert_subset_iff, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, affineSpan_le, Set.insert_subset_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
p₁ p₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ p₁ ∈ (↑s : Set P) ∧ p₂ ∈ (↑s : Set P)

Tactic:
⟨hp₁, hp₂⟩

Premises used: And.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₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ p₁ ∈ (↑s : Set P) ∧ p₂ ∈ (↑s : Set P)

Tactic:
exact ⟨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
p₁ p₂ p₃ : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p₃}) p₁
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₁, p₃}) (affineSpan k {p₂, p₃})

Tactic:
affineSpan_pair_le_of_mem_of_mem h (right_mem_affineSpan_pair _ _ _)

Premises used: affineSpan_pair_le_of_mem_of_mem, right_mem_affineSpan_pair
-- 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₂ p₃ : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p₃}) p₁
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₂, p₁}) (affineSpan k {p₂, p₃})

Tactic:
affineSpan_pair_le_of_mem_of_mem (left_mem_affineSpan_pair _ _ _) h

Premises used: affineSpan_pair_le_of_mem_of_mem, left_mem_affineSpan_pair
-- 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₂ : Set P
h : s₁ ⊆ s₂
⊢ LE.le (α := AffineSubspace k P) (affineSpan k s₁) (affineSpan k s₂)

Tactic:
affineSpan_le_of_subset_coe (Set.Subset.trans h (subset_affineSpan k _))

Premises used: Set.Subset.trans, subset_affineSpan, affineSpan_le_of_subset_coe
-- 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
ps : Set P
rw : Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (↑(affineSpan k ps) : Set P))) (affineSpan k (insert p ps))
rw₁ : Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (↑(affineSpan k ps) : Set P))) (affineSpan k ({p} ∪ ps))
rw₂ :
  Eq (α := AffineSubspace k P) (affineSpan k {p} ⊔ affineSpan k (↑(affineSpan k ps) : Set P)) (affineSpan k ({p} ∪ ps))
rw₃ :
  Eq (α := AffineSubspace k P) (affineSpan k {p} ⊔ affineSpan k (↑(affineSpan k ps) : Set P))
    (affineSpan k {p} ⊔ affineSpan k ps)
rw₄ rw₅ : Eq (α := AffineSubspace k P) (affineSpan k {p} ⊔ affineSpan k ps) (affineSpan k {p} ⊔ affineSpan k ps)
⊢ Eq (α := AffineSubspace k P) (affineSpan k (insert p (↑(affineSpan k ps) : Set P))) (affineSpan k (insert p ps))

Tactic:
rw [Set.insert_eq, Set.insert_eq, span_union, span_union, affineSpan_coe]

Premises used: Set.insert_eq, AffineSubspace.span_union, AffineSubspace.affineSpan_coe
-- 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
ps : Set P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k ps) p
⊢ p ∈ (↑(affineSpan k ps) : Set P)

Tactic:
rw [← mem_coe] at h

Premises used: AffineSubspace.mem_coe
-- 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
ps : Set P
h : p ∈ (↑(affineSpan k ps) : Set P)
rw : Eq (α := AffineSubspace k P) (affineSpan k (insert p (↑(affineSpan k ps) : Set P))) (affineSpan k ps)
rw₁ : Eq (α := AffineSubspace k P) (affineSpan k (↑(affineSpan k ps) : Set P)) (affineSpan k ps)
rw₂ rw₃ : Eq (α := AffineSubspace k P) (affineSpan k ps) (affineSpan k ps)
⊢ Eq (α := AffineSubspace k P) (affineSpan k (insert p ps)) (affineSpan k ps)

Tactic:
rw [← affineSpan_insert_affineSpan, Set.insert_eq_of_mem h, affineSpan_coe]

Premises used: Set.insert_eq_of_mem, affineSpan_insert_affineSpan, AffineSubspace.affineSpan_coe
-- 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
ps : Set P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k ps) p
simp_rw : Eq (α := Submodule k V) (direction (affineSpan k (insert p ps))) (direction (affineSpan k ps))
⊢ Eq (α := Submodule k V) (vectorSpan k (insert p ps)) (vectorSpan k ps)

Tactic:
simp_rw [← direction_affineSpan, affineSpan_insert_eq_affineSpan _ h]

Premises used: direction_affineSpan, affineSpan_insert_eq_affineSpan
-- 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
x_1 x : V
hx : x ∈ s
⊢ Membership.mem (γ := Submodule k V) (Submodule.span k s) x

Tactic:
Submodule.subset_span hx

Premises used: Submodule.subset_span
-- 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
x_1 x : V
hx : x ∈ s
⊢ Membership.mem (γ := Submodule k V) (Submodule.span k s) x

Tactic:
exact Submodule.subset_span hx

Premises used: Submodule.subset_span
-- 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
x : V
c : k
u : V
hu_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) u
v : V
hv_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) v
w : V
hw_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) w
hu : Membership.mem (γ := Submodule k V) (Submodule.span k s) u
hv : Membership.mem (γ := Submodule k V) (Submodule.span k s) v
hw : Membership.mem (γ := Submodule k V) (Submodule.span k s) w
smul_vsub_vadd : Membership.mem (γ := Submodule k V) (Submodule.span k s) (c • (u - v) + w)
⊢ Membership.mem (γ := Submodule k V) (Submodule.span k s) (c • (u -ᵥ v) +ᵥ w)

Tactic:
simp only [vsub_eq_sub, vadd_eq_add]

Premises used: vadd_eq_add, vsub_eq_sub
-- 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
x : V
c : k
u : V
hu_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) u
v : V
hv_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) v
w : V
hw_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) w
hu : Membership.mem (γ := Submodule k V) (Submodule.span k s) u
hv : Membership.mem (γ := Submodule k V) (Submodule.span k s) v
hw : Membership.mem (γ := Submodule k V) (Submodule.span k s) w
apply : Membership.mem (γ := Submodule k V) (Submodule.span k s) (c • (u - v))
⊢ Membership.mem (γ := Submodule k V) (Submodule.span k s) (c • (u - v) + w)

Tactic:
apply Submodule.add_mem _ _ hw

Premises used: Submodule.add_mem
-- 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
x : V
c : k
u : V
hu_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) u
v : V
hv_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) v
w : V
hw_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) w
hu : Membership.mem (γ := Submodule k V) (Submodule.span k s) u
hv : Membership.mem (γ := Submodule k V) (Submodule.span k s) v
hw : Membership.mem (γ := Submodule k V) (Submodule.span k s) w
⊢ Membership.mem (γ := Submodule k V) (Submodule.span k s) (c • (u - v))

Tactic:
Submodule.smul_mem _ _ (Submodule.sub_mem _ hu hv)

Premises used: Set.Mem, Submodule.sub_mem, Submodule.smul_mem
-- 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
x : V
c : k
u : V
hu_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) u
v : V
hv_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) v
w : V
hw_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) w
hu : Membership.mem (γ := Submodule k V) (Submodule.span k s) u
hv : Membership.mem (γ := Submodule k V) (Submodule.span k s) v
hw : Membership.mem (γ := Submodule k V) (Submodule.span k s) w
⊢ Membership.mem (γ := Submodule k V) (Submodule.span k s) (c • (u - v))

Tactic:
exact Submodule.smul_mem _ _ (Submodule.sub_mem _ hu hv)

Premises used: Submodule.sub_mem, Submodule.smul_mem
-- 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
x : V
hx : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) x
mem : ∀ (x : V) (hx : x ∈ s), Membership.mem (γ := Submodule k V) (Submodule.span k s) x
smul_vsub_vadd :
  ∀ (c : k) (u : V),
    Membership.mem (γ := AffineSubspace k V) (affineSpan k s) u →
      ∀ (v : V),
        Membership.mem (γ := AffineSubspace k V) (affineSpan k s) v →
          ∀ (w : V),
            Membership.mem (γ := AffineSubspace k V) (affineSpan k s) w →
              ∀ (hu : Membership.mem (γ := Submodule k V) (Submodule.span k s) u)
                (hv : Membership.mem (γ := Submodule k V) (Submodule.span k s) v)
                (hw : Membership.mem (γ := Submodule k V) (Submodule.span k s) w),
                Membership.mem (γ := Submodule k V) (Submodule.span k s) (c • (u -ᵥ v) +ᵥ w)
⊢ Membership.mem (γ := Submodule k V) (Submodule.span k s) x

Tactic:
induction hx using affineSpan_induction' with
  | mem x hx => exact Submodule.subset_span hx
  | smul_vsub_vadd c u _ v _ w _ hu hv hw =>
    simp only [vsub_eq_sub, vadd_eq_add]
    apply Submodule.add_mem _ _ hw
    exact Submodule.smul_mem _ _ (Submodule.sub_mem _ hu hv)

Premises used: vadd_eq_add, Submodule.subset_span, vsub_eq_sub
-- 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
⊢ (↑(affineSpan k s) : Set V) ⊆ (↑(Submodule.span k s) : Set V)

Tactic:
affineSpan_le_toAffineSubspace_span

Premises used: affineSpan_le_toAffineSubspace_span, iInf, Set.Mem, Set.iInter, setOf, Set.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
s : Set V
rw : (↑(affineSpan k (insert 0 s)) : Set V) = (↑(Submodule.span k (insert 0 s)) : Set V)
⊢ (↑(affineSpan k (insert 0 s)) : Set V) = (↑(Submodule.span k s) : Set V)

Tactic:
rw [← Submodule.span_insert_zero]

Premises used: Submodule.span_insert_zero
-- 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
⊢ (↑(affineSpan k (insert 0 s)) : Set V) = (↑(Submodule.span k (insert 0 s)) : Set V)

Tactic:
affineSpan_subset_span.antisymm ?_

Premises used: Set.Mem, setOf, affineSpan_subset_span, HasSubset.Subset.antisymm
-- 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
refine : (↑(Submodule.span k (insert 0 s)) : Set V) ⊆ (↑(affineSpan k (insert 0 s)) : Set V)
⊢ (↑(affineSpan k (insert 0 s)) : Set V) = (↑(Submodule.span k (insert 0 s)) : Set V)

Tactic:
refine affineSpan_subset_span.antisymm ?_

Premises used: affineSpan_subset_span, HasSubset.Subset.antisymm
-- 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
rw : (↑(Submodule.span k (insert 0 s)) : Set V) ⊆ (↑(Submodule.span k (insert 0 s -ᵥ insert 0 s)) : Set V) + insert 0 s
⊢ (↑(Submodule.span k (insert 0 s)) : Set V) ⊆ (↑(affineSpan k (insert 0 s)) : Set V)

Tactic:
rw [← vectorSpan_add_self, vectorSpan_def]

Premises used: vectorSpan_def, vectorSpan_add_self
-- 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
⊢ (↑(Submodule.span k (insert 0 s)) : Set V) ⊆ (↑(Submodule.span k (insert 0 s -ᵥ insert 0 s)) : Set V) + insert 0 s

Tactic:
Subset.trans ?_ <| subset_add_left _ <| mem_insert ..

Premises used: Set.Subset.trans, Set.subset_add_left, Set.mem_insert
-- 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
refine : (↑(Submodule.span k (insert 0 s)) : Set V) ⊆ (↑(Submodule.span k (insert 0 s -ᵥ insert 0 s)) : Set V)
⊢ (↑(Submodule.span k (insert 0 s)) : Set V) ⊆ (↑(Submodule.span k (insert 0 s -ᵥ insert 0 s)) : Set V) + insert 0 s

Tactic:
refine Subset.trans ?_ <| subset_add_left _ <| mem_insert ..

Premises used: Set.Subset.trans, Set.subset_add_left, Set.mem_insert
-- 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
_a : insert 0 s ⊆ insert 0 s -ᵥ insert 0 s
⊢ (↑(Submodule.span k (insert 0 s)) : Set V) ⊆ (↑(Submodule.span k (insert 0 s -ᵥ insert 0 s)) : Set V)

Tactic:
gcongr
-- 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
⊢ insert 0 s ⊆ insert 0 s -ᵥ insert 0 s

Tactic:
subset_sub_left <| mem_insert ..

Premises used: Set.subset_sub_left, Set.mem_insert
-- 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
⊢ insert 0 s ⊆ insert 0 s -ᵥ insert 0 s

Tactic:
exact subset_sub_left <| mem_insert ..

Premises used: Set.subset_sub_left, Set.mem_insert