awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
refine_1 :
  ∀ (x : M) (hx : x ∈ S),
    ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x
refine_2 : ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) 0
refine_3 :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x)
    (hy : Membership.mem (γ := Submodule R M) (span R S) y),
    (∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x) →
      (∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) y) →
        ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) (x + y)
refine_4 :
  ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x),
    (∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x) →
      ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) (a • x)
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x

Tactic:
refine span_induction (fun x hx => ?_) ?_ ?_ ?_ hx
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R S) x_1
x : M
hx : x ∈ S
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x

Tactic:
⟨{x}, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Singleton.singleton
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R S) x_1
x : M
hx : x ∈ S
refine_1 : (↑{x} : Set M) ⊆ S
refine_1₁ : Membership.mem (γ := Submodule R M) (span R (↑{x} : Set M)) x
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x

Tactic:
refine ⟨{x}, ?_, ?_⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R S) x_1
x : M
hx : x ∈ S
refine_1 : {x} ⊆ S
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : x ∈ S
⊢ (↑{x} : Set M) ⊆ S

Tactic:
rwa [Finset.coe_singleton, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Finset.coe_singleton
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R S) x_1
x : M
hx : x ∈ S
refine_1 : Membership.mem (γ := Submodule R M) (R ∙ x) x
⊢ Membership.mem (γ := Submodule R M) (span R (↑{x} : Set M)) x

Tactic:
rw [Finset.coe_singleton]

Premises used: Finset.coe_singleton
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R S) x_1
x : M
hx : x ∈ S
⊢ Membership.mem (γ := Submodule R M) (R ∙ x) x

Tactic:
Submodule.mem_span_singleton_self x

Premises used: Submodule.mem_span_singleton_self
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R S) x_1
x : M
hx : x ∈ S
⊢ Membership.mem (γ := Submodule R M) (R ∙ x) x

Tactic:
exact Submodule.mem_span_singleton_self x

Premises used: Submodule.mem_span_singleton_self
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
h : (↑∅ : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑∅ : Set M)) 0
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) 0

Tactic:
use ∅
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
⊢ (↑∅ : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑∅ : Set M)) 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx : Membership.mem (γ := Submodule R M) (span R S) x_1
x y : M
X : Finset M
hX : (↑X : Set M) ⊆ S
hxX : Membership.mem (γ := Submodule R M) (span R (↑X : Set M)) x
Y : Finset M
hY : (↑Y : Set M) ⊆ S
hyY : Membership.mem (γ := Submodule R M) (span R (↑Y : Set M)) y
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) (x + y)

Tactic:
⟨X ∪ Y, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Union.union
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx : Membership.mem (γ := Submodule R M) (span R S) x_1
x y : M
X : Finset M
hX : (↑X : Set M) ⊆ S
hxX : Membership.mem (γ := Submodule R M) (span R (↑X : Set M)) x
Y : Finset M
hY : (↑Y : Set M) ⊆ S
hyY : Membership.mem (γ := Submodule R M) (span R (↑Y : Set M)) y
refine_3 : (↑(X ∪ Y) : Set M) ⊆ S
refine_3₁ : Membership.mem (γ := Submodule R M) (span R (↑(X ∪ Y) : Set M)) (x + y)
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) (x + y)

Tactic:
refine ⟨X ∪ Y, ?_, ?_⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx : Membership.mem (γ := Submodule R M) (span R S) x_1
x y : M
X : Finset M
hX : (↑X : Set M) ⊆ S
hxX : Membership.mem (γ := Submodule R M) (span R (↑X : Set M)) x
Y : Finset M
hY : (↑Y : Set M) ⊆ S
hyY : Membership.mem (γ := Submodule R M) (span R (↑Y : Set M)) y
refine_3 : (↑X : Set M) ∪ (↑Y : Set M) ⊆ S
⊢ (↑(X ∪ Y) : Set M) ⊆ S

Tactic:
rw [Finset.coe_union]

Premises used: Finset.coe_union
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx : Membership.mem (γ := Submodule R M) (span R S) x_1
x y : M
X : Finset M
hX : (↑X : Set M) ⊆ S
hxX : Membership.mem (γ := Submodule R M) (span R (↑X : Set M)) x
Y : Finset M
hY : (↑Y : Set M) ⊆ S
hyY : Membership.mem (γ := Submodule R M) (span R (↑Y : Set M)) y
⊢ (↑X : Set M) ∪ (↑Y : Set M) ⊆ S

Tactic:
Set.union_subset hX hY

Premises used: Set.union_subset
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx : Membership.mem (γ := Submodule R M) (span R S) x_1
x y : M
X : Finset M
hX : (↑X : Set M) ⊆ S
hxX : Membership.mem (γ := Submodule R M) (span R (↑X : Set M)) x
Y : Finset M
hY : (↑Y : Set M) ⊆ S
hyY : Membership.mem (γ := Submodule R M) (span R (↑Y : Set M)) y
⊢ (↑X : Set M) ∪ (↑Y : Set M) ⊆ S

Tactic:
exact Set.union_subset hX hY

Premises used: Set.union_subset
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx : Membership.mem (γ := Submodule R M) (span R S) x_1
x y : M
X : Finset M
hX : (↑X : Set M) ⊆ S
hxX : Membership.mem (γ := Submodule R M) (span R (↑X : Set M)) x
Y : Finset M
hY : (↑Y : Set M) ⊆ S
hyY : Membership.mem (γ := Submodule R M) (span R (↑Y : Set M)) y
refine_3 :
  ∃ (y_1 : M),
    Membership.mem (γ := Submodule R M) (span R (↑X : Set M)) y_1 ∧
      ∃ (z : M), Membership.mem (γ := Submodule R M) (span R (↑Y : Set M)) z ∧ y_1 + z = x + y
⊢ Membership.mem (γ := Submodule R M) (span R (↑(X ∪ Y) : Set M)) (x + y)

Tactic:
rw [Finset.coe_union, span_union, mem_sup]

Premises used: Submodule.span_union, Submodule.mem_sup, Finset.coe_union
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx : Membership.mem (γ := Submodule R M) (span R S) x_1
x y : M
X : Finset M
hX : (↑X : Set M) ⊆ S
hxX : Membership.mem (γ := Submodule R M) (span R (↑X : Set M)) x
Y : Finset M
hY : (↑Y : Set M) ⊆ S
hyY : Membership.mem (γ := Submodule R M) (span R (↑Y : Set M)) y
⊢ ∃ (y_1 : M),
    Membership.mem (γ := Submodule R M) (span R (↑X : Set M)) y_1 ∧
      ∃ (z : M), Membership.mem (γ := Submodule R M) (span R (↑Y : Set M)) z ∧ y_1 + z = x + y

Tactic:
⟨x, hxX, y, hyY, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx : Membership.mem (γ := Submodule R M) (span R S) x_1
x y : M
X : Finset M
hX : (↑X : Set M) ⊆ S
hxX : Membership.mem (γ := Submodule R M) (span R (↑X : Set M)) x
Y : Finset M
hY : (↑Y : Set M) ⊆ S
hyY : Membership.mem (γ := Submodule R M) (span R (↑Y : Set M)) y
⊢ ∃ (y_1 : M),
    Membership.mem (γ := Submodule R M) (span R (↑X : Set M)) y_1 ∧
      ∃ (z : M), Membership.mem (γ := Submodule R M) (span R (↑Y : Set M)) z ∧ y_1 + z = x + y

Tactic:
exact ⟨x, hxX, y, hyY, rfl⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx : Membership.mem (γ := Submodule R M) (span R S) x_1
a : R
x : M
T : Finset M
hT : (↑T : Set M) ⊆ S
h2 : Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) (a • x)

Tactic:
⟨T, hT, smul_mem _ _ h2⟩

Premises used: And.intro, Exists.intro, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set M
x_1 : M
hx : Membership.mem (γ := Submodule R M) (span R S) x_1
a : R
x : M
T : Finset M
hT : (↑T : Set M) ⊆ S
h2 : Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) (a • x)

Tactic:
exact ⟨T, hT, smul_mem _ _ h2⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
ht : (↑∅ : Set M) ⊆ (↑(span R s) : Set M)
⊢ (↑∅ : Set M) ⊆ s ∧ (↑∅ : Set M) ⊆ (↑(span R (↑∅ : Set M)) : Set M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
ht : (↑∅ : Set M) ⊆ (↑(span R s) : Set M)
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑∅ : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)

Tactic:
exact ⟨∅, by simp⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
a : M
t : Finset M
hat : a ∉ t
IH :
  ∀ (ht : (↑t : Set M) ⊆ (↑(span R s) : Set M)),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
ht : (↑(insert a t) : Set M) ⊆ (↑(span R s) : Set M)
⊢ (↑t : Set M) ⊆ (↑(span R s) : Set M)

Tactic:
simp_all [Set.insert_subset_iff]

Premises used: Set.insert_subset_iff
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
a : M
t : Finset M
hat : a ∉ t
IH :
  ∀ (ht : (↑t : Set M) ⊆ (↑(span R s) : Set M)),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
ht : (↑(Insert.insert a t) : Set M) ⊆ (↑(span R s) : Set M)
insert :
  ∀ (T : Finset M) (hTs : (↑T : Set M) ⊆ s) (htT : (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑(Insert.insert a t) : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑(Insert.insert a t) : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)

Tactic:
obtain ⟨T, hTs, htT⟩ := IH (by simp_all [Set.insert_subset_iff])
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
a : M
t : Finset M
hat : a ∉ t
IH :
  ∀ (ht : (↑t : Set M) ⊆ (↑(span R s) : Set M)),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
ht : (↑(Insert.insert a t) : Set M) ⊆ (↑(span R s) : Set M)
T : Finset M
hTs : (↑T : Set M) ⊆ s
htT : (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
insert :
  ∀ (T' : Finset M) (hT's : (↑T' : Set M) ⊆ s) (haT' : Membership.mem (γ := Submodule R M) (span R (↑T' : Set M)) a),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑(Insert.insert a t) : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑(Insert.insert a t) : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)

Tactic:
obtain ⟨T', hT's, haT'⟩ := mem_span_finite_of_mem_span (ht (Finset.mem_insert_self _ _))

Premises used: Finset.mem_insert_self, Submodule.mem_span_finite_of_mem_span
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
a : M
t : Finset M
hat : a ∉ t
IH :
  ∀ (ht : (↑t : Set M) ⊆ (↑(span R s) : Set M)),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
ht : (↑(insert a t) : Set M) ⊆ (↑(span R s) : Set M)
T : Finset M
hTs : (↑T : Set M) ⊆ s
htT : (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
T' : Finset M
hT's : (↑T' : Set M) ⊆ s
haT' : Membership.mem (γ := Submodule R M) (span R (↑T' : Set M)) a
⊢ (↑(T ∪ T') : Set M) ⊆ s

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
a : M
t : Finset M
hat : a ∉ t
IH :
  ∀ (ht : (↑t : Set M) ⊆ (↑(span R s) : Set M)),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
ht : (↑(Insert.insert a t) : Set M) ⊆ (↑(span R s) : Set M)
T : Finset M
hTs : (↑T : Set M) ⊆ s
htT : (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
T' : Finset M
hT's : (↑T' : Set M) ⊆ s
haT' : Membership.mem (γ := Submodule R M) (span R (↑T' : Set M)) a
insert : (↑(Insert.insert a t) : Set M) ⊆ (↑(span R (↑(T ∪ T') : Set M)) : Set M)
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑(Insert.insert a t) : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)

Tactic:
refine ⟨T ∪ T', by simp_all, ?_⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
a : M
t : Finset M
hat : a ∉ t
IH :
  ∀ (ht : (↑t : Set M) ⊆ (↑(span R s) : Set M)),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
ht : (↑(Insert.insert a t) : Set M) ⊆ (↑(span R s) : Set M)
T : Finset M
hTs : (↑T : Set M) ⊆ s
htT : (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
T' : Finset M
hT's : (↑T' : Set M) ⊆ s
haT' : Membership.mem (γ := Submodule R M) (span R (↑T' : Set M)) a
insert :
  Membership.mem (γ := Submodule R M) (span R (↑T : Set M) ⊔ span R (↑T' : Set M)) a ∧
    (↑t : Set M) ⊆ (↑(span R (↑T : Set M) ⊔ span R (↑T' : Set M)) : Set M)
⊢ (↑(Insert.insert a t) : Set M) ⊆ (↑(span R (↑(T ∪ T') : Set M)) : Set M)

Tactic:
simp only [Finset.coe_insert, Finset.coe_union, span_union, insert_subset_iff, SetLike.mem_coe]

Premises used: Set.insert_subset_iff, Submodule.span_union, SetLike.mem_coe, Finset.coe_insert, Finset.coe_union
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
a : M
t : Finset M
hat : a ∉ t
IH :
  ∀ (ht : (↑t : Set M) ⊆ (↑(span R s) : Set M)),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
ht : (↑(insert a t) : Set M) ⊆ (↑(span R s) : Set M)
T : Finset M
hTs : (↑T : Set M) ⊆ s
htT : (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
T' : Finset M
hT's : (↑T' : Set M) ⊆ s
haT' : Membership.mem (γ := Submodule R M) (span R (↑T' : Set M)) a
⊢ Membership.mem (γ := Submodule R M) (span R (↑T : Set M) ⊔ span R (↑T' : Set M)) a ∧
    (↑t : Set M) ⊆ (↑(span R (↑T : Set M) ⊔ span R (↑T' : Set M)) : Set M)

Tactic:
⟨mem_sup_right haT', htT.trans (le_sup_left (a := span R _))⟩

Premises used: le_sup_left, HasSubset.Subset.trans, And.intro, Submodule.mem_sup_right
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
a : M
t : Finset M
hat : a ∉ t
IH :
  ∀ (ht : (↑t : Set M) ⊆ (↑(span R s) : Set M)),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
ht : (↑(insert a t) : Set M) ⊆ (↑(span R s) : Set M)
T : Finset M
hTs : (↑T : Set M) ⊆ s
htT : (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
T' : Finset M
hT's : (↑T' : Set M) ⊆ s
haT' : Membership.mem (γ := Submodule R M) (span R (↑T' : Set M)) a
⊢ Membership.mem (γ := Submodule R M) (span R (↑T : Set M) ⊔ span R (↑T' : Set M)) a ∧
    (↑t : Set M) ⊆ (↑(span R (↑T : Set M) ⊔ span R (↑T' : Set M)) : Set M)

Tactic:
exact ⟨mem_sup_right haT', htT.trans (le_sup_left (a := span R _))⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
t : Finset M
ht : (↑t : Set M) ⊆ (↑(span R s) : Set M)
empty :
  ∀ (ht : (↑∅ : Set M) ⊆ (↑(span R s) : Set M)),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑∅ : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
insert :
  ∀ (a : M) (t : Finset M) (hat : a ∉ t)
    (IH :
      ∀ (ht : (↑t : Set M) ⊆ (↑(span R s) : Set M)),
        ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M))
    (ht : (↑(Insert.insert a t) : Set M) ⊆ (↑(span R s) : Set M)),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑(Insert.insert a t) : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)

Tactic:
induction t using Finset.induction_on with
  | empty => exact ⟨∅, by simp⟩
  | insert a t hat IH =>
    obtain ⟨T, hTs, htT⟩ := IH (by simp_all [Set.insert_subset_iff])
    obtain ⟨T', hT's, haT'⟩ := mem_span_finite_of_mem_span (ht (Finset.mem_insert_self _ _))
    refine ⟨T ∪ T', by simp_all, ?_⟩
    simp only [Finset.coe_insert, Finset.coe_union, span_union, insert_subset_iff, SetLike.mem_coe]
    exact ⟨mem_sup_right haT', htT.trans (le_sup_left (a := span R _))⟩

Premises used: Insert.insert, Submodule.mem_span_finite_of_mem_span, Set.insert_subset_iff, Submodule.span_union, SetLike.mem_coe, Finset.coe_insert, Finset.coe_union
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
t : Finset M
ht : (↑t : Set M) ⊆ (↑(span R s) : Set M)
empty :
  ∀ (ht : (↑∅ : Set M) ⊆ (↑(span R s) : Set M)),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑∅ : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
insert :
  ∀ (a : M) (t : Finset M) (hat : a ∉ t)
    (IH :
      ∀ (ht : (↑t : Set M) ⊆ (↑(span R s) : Set M)),
        ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M))
    (ht : (↑(Insert.insert a t) : Set M) ⊆ (↑(span R s) : Set M)),
    ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑(Insert.insert a t) : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)

Tactic:
classical
  induction t using Finset.induction_on with
  | empty => exact ⟨∅, by simp⟩
  | insert a t hat IH =>
    obtain ⟨T, hTs, htT⟩ := IH (by simp_all [Set.insert_subset_iff])
    obtain ⟨T', hT's, haT'⟩ := mem_span_finite_of_mem_span (ht (Finset.mem_insert_self _ _))
    refine ⟨T ∪ T', by simp_all, ?_⟩
    simp only [Finset.coe_insert, Finset.coe_union, span_union, insert_subset_iff, SetLike.mem_coe]
    exact ⟨mem_sup_right haT', htT.trans (le_sup_left (a := span R _))⟩

Premises used: Insert.insert, Submodule.mem_span_finite_of_mem_span, Set.insert_subset_iff, Submodule.span_union, SetLike.mem_coe, Finset.coe_insert, Finset.coe_union
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
h : ∀ (x : M), x ∈ (p ⊔ p').toAddSubgroup ↔ x ∈ p.toAddSubgroup ⊔ p'.toAddSubgroup
⊢ (p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
x : M
h : (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubgroup, ∃ z ∈ p'.toAddSubgroup, y + z = x
⊢ x ∈ (p ⊔ p').toAddSubgroup ↔ x ∈ p.toAddSubgroup ⊔ p'.toAddSubgroup

Tactic:
rw [mem_toAddSubgroup, mem_sup, AddSubgroup.mem_sup]

Premises used: Submodule.mem_toAddSubgroup, AddSubgroup.mem_sup, Submodule.mem_sup
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
x : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubgroup, ∃ z ∈ p'.toAddSubgroup, y + z = x

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
s : Set M
rw :
  (∃ (a : R) (z : M), Membership.mem (γ := Submodule R M) (span R s) z ∧ x = a • y + z) ↔
    ∃ (a : R), Membership.mem (γ := Submodule R M) (span R s) (x + a • y)
⊢ Membership.mem (γ := Submodule R M) (span R (insert y s)) x ↔
    ∃ (a : R), Membership.mem (γ := Submodule R M) (span R s) (x + a • y)

Tactic:
rw [mem_span_insert]

Premises used: Submodule.mem_span_insert
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
s : Set M
mp :
  (∃ (a : R) (z : M), Membership.mem (γ := Submodule R M) (span R s) z ∧ x = a • y + z) →
    ∃ (a : R), Membership.mem (γ := Submodule R M) (span R s) (x + a • y)
mpr :
  (∃ (a : R), Membership.mem (γ := Submodule R M) (span R s) (x + a • y)) →
    ∃ (a : R) (z : M), Membership.mem (γ := Submodule R M) (span R s) z ∧ x = a • y + z
⊢ (∃ (a : R) (z : M), Membership.mem (γ := Submodule R M) (span R s) z ∧ x = a • y + z) ↔
    ∃ (a : R), Membership.mem (γ := Submodule R M) (span R s) (x + a • y)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
y : M
s : Set M
a : R
z : M
hz : Membership.mem (γ := Submodule R M) (span R s) z
⊢ Membership.mem (γ := Submodule R M) (span R s) (a • y + z + -a • y)

Tactic:
simp [hz, add_assoc]

Premises used: add_assoc
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
y : M
s : Set M
a : R
z : M
hz : Membership.mem (γ := Submodule R M) (span R s) z
⊢ ∃ (a_1 : R), Membership.mem (γ := Submodule R M) (span R s) (a • y + z + a_1 • y)

Tactic:
exact ⟨-a, by simp [hz, add_assoc]⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
s : Set M
a : R
h : Membership.mem (γ := Submodule R M) (span R s) (x + a • y)
⊢ x = -a • y + (x + a • y)

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
s : Set M
a : R
h : Membership.mem (γ := Submodule R M) (span R s) (x + a • y)
⊢ ∃ (a : R) (z : M), Membership.mem (γ := Submodule R M) (span R s) z ∧ x = a • y + z

Tactic:
exact ⟨-a, _, h, by simp [add_comm]⟩