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
x : M
mp : (∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v) → ∀ (v : M), ∃ (r : R), r • x = v
mpr : (∀ (v : M), ∃ (r : R), r • x = v) → ∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v
mp₁ mp₂ mp₃ :
  (∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v) → ∀ (v : M), ∃ (r : R), r • x = v
mpr₁ mpr₂ mpr₃ :
  (∀ (v : M), ∃ (r : R), r • x = v) → ∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v
mp₄ mp₅ mp₆ :
  (∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v) → ∀ (v : M), ∃ (r : R), r • x = v
mpr₄ mpr₅ mpr₆ :
  (∀ (v : M), ∃ (r : R), r • x = v) → ∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v
mp₇ mp₈ mp₉ :
  (∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v) → ∀ (v : M), ∃ (r : R), r • x = v
mpr₇ mpr₈ mpr₉ :
  (∀ (v : M), ∃ (r : R), r • x = v) → ∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v
mp₁₀ mp₁₁ :
  (∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v) → ∀ (v : M), ∃ (r : R), r • x = v
mpr₁₀ mpr₁₁ :
  (∀ (v : M), ∃ (r : R), r • x = v) → ∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v
⊢ (∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v) ↔ ∀ (v : M), ∃ (r : R), r • x = v

Tactic:
tauto
-- 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
h : ∀ (x : M), Membership.mem (γ := Submodule R M) (R ∙ 0) x ↔ Membership.mem (γ := Submodule R M) ⊥ x
⊢ Eq (α := Submodule R M) (R ∙ 0) ⊥

Tactic:
ext
-- 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
x : M
⊢ Membership.mem (γ := Submodule R M) (R ∙ 0) x ↔ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
simp [mem_span_singleton, eq_comm]

Premises used: Submodule.mem_span_singleton, eq_comm
-- 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
y : M
⊢ (↑(R ∙ y) : Set M) = range fun (x : R) ↦ x • y

Tactic:
Set.ext fun _ => mem_span_singleton

Premises used: Set.ext, Submodule.mem_span_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 : Type u_9
inst_3 : SMul S R
inst_4 : SMul S M
inst_5 : IsScalarTower S R M
r : S
x : M
rw : Membership.mem (γ := Submodule R M) (R ∙ x) (r • x)
⊢ LE.le (α := Submodule R M) (R ∙ r • x) (R ∙ x)

Tactic:
rw [span_le, Set.singleton_subset_iff, SetLike.mem_coe]

Premises used: Set.singleton_subset_iff, SetLike.mem_coe, Submodule.span_le
-- 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 : Type u_9
inst_3 : SMul S R
inst_4 : SMul S M
inst_5 : IsScalarTower S R M
r : S
x : M
⊢ Membership.mem (γ := Submodule R M) (R ∙ x) (r • x)

Tactic:
smul_of_tower_mem _ _ (mem_span_singleton_self _)

Premises used: Submodule.mem_span_singleton_self, Submodule.smul_of_tower_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 : Type u_9
inst_3 : SMul S R
inst_4 : SMul S M
inst_5 : IsScalarTower S R M
r : S
x : M
⊢ Membership.mem (γ := Submodule R M) (R ∙ x) (r • x)

Tactic:
exact smul_of_tower_mem _ _ (mem_span_singleton_self _)

Premises used: Submodule.mem_span_singleton_self, Submodule.smul_of_tower_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
G : Type u_9
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
g : G
x : M
⊢ Eq (α := Submodule R M) (R ∙ g • x) (R ∙ x)

Tactic:
le_antisymm (span_singleton_smul_le R g x) ?_

Premises used: le_antisymm, Submodule.span_singleton_smul_le
-- 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
G : Type u_9
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
g : G
x : M
refine : LE.le (α := Submodule R M) (R ∙ x) (R ∙ g • x)
⊢ Eq (α := Submodule R M) (R ∙ g • x) (R ∙ x)

Tactic:
refine le_antisymm (span_singleton_smul_le R g x) ?_

Premises used: le_antisymm, Submodule.span_singleton_smul_le
-- 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
G : Type u_9
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
g : G
x : M
⊢ LE.le (α := Submodule R M) (R ∙ g⁻¹ • g • x) (R ∙ g • x)

Tactic:
span_singleton_smul_le R g⁻¹ (g • x)

Premises used: Inv.inv, HSMul.hSMul, Submodule.span_singleton_smul_le
-- 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
G : Type u_9
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
g : G
x : M
h : x = g⁻¹ • g • x
⊢ LE.le (α := Submodule R M) (R ∙ x) (R ∙ g • x)

Tactic:
convert! span_singleton_smul_le R g⁻¹ (g • x)

Premises used: Inv.inv, HSMul.hSMul, Submodule.span_singleton_smul_le
-- 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
G : Type u_9
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
g : G
x : M
⊢ x = g⁻¹ • g • x

Tactic:
(inv_smul_smul g x).symm

Premises used: inv_smul_smul, Eq.symm
-- 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
G : Type u_9
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
g : G
x : M
⊢ x = g⁻¹ • g • x

Tactic:
exact (inv_smul_smul g x).symm

Premises used: inv_smul_smul, Eq.symm
-- 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
r : R
hr : IsUnit r
x : M
⊢ IsUnit r

Tactic:
hr
-- 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
r : R
hr : IsUnit r
x : M
lift : ∀ (r : Rˣ), Eq (α := Submodule R M) (R ∙ (↑r : R) • x) (R ∙ x)
⊢ Eq (α := Submodule R M) (R ∙ r • x) (R ∙ x)

Tactic:
lift r to Rˣ using hr
-- 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
x : M
r : Rˣ
rw : Eq (α := Submodule R M) (R ∙ r • x) (R ∙ x)
⊢ Eq (α := Submodule R M) (R ∙ (↑r : R) • x) (R ∙ x)

Tactic:
rw [← Units.smul_def]

Premises used: Units.smul_def
-- 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
x : M
r : Rˣ
⊢ Eq (α := Submodule R M) (R ∙ r • x) (R ∙ x)

Tactic:
span_singleton_group_smul_eq R r x

Premises used: Submodule.span_singleton_group_smul_eq
-- 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
x : M
r : Rˣ
⊢ Eq (α := Submodule R M) (R ∙ r • x) (R ∙ x)

Tactic:
exact span_singleton_group_smul_eq R r x

Premises used: Submodule.span_singleton_group_smul_eq
-- 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
x y z : M
hxy : Membership.mem (γ := Submodule R M) (R ∙ y) x
hyz : Membership.mem (γ := Submodule R M) (R ∙ z) y
rw : ∀ (hxy : {x} ⊆ (↑(R ∙ y) : Set M)) (hyz : {y} ⊆ (↑(R ∙ z) : Set M)), {x} ⊆ (↑(R ∙ z) : Set M)
⊢ Membership.mem (γ := Submodule R M) (R ∙ z) x

Tactic:
rw [← SetLike.mem_coe, ← singleton_subset_iff] at *

Premises used: Set.singleton_subset_iff, SetLike.mem_coe
-- 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
x y z : M
hxy : {x} ⊆ (↑(R ∙ y) : Set M)
hyz : {y} ⊆ (↑(R ∙ z) : Set M)
⊢ {x} ⊆ (↑(R ∙ z) : Set M)

Tactic:
Submodule.subset_span_trans hxy hyz

Premises used: Submodule.subset_span_trans
-- 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
x y z : M
hxy : {x} ⊆ (↑(R ∙ y) : Set M)
hyz : {y} ⊆ (↑(R ∙ z) : Set M)
⊢ {x} ⊆ (↑(R ∙ z) : Set M)

Tactic:
exact Submodule.subset_span_trans hxy hyz

Premises used: Submodule.subset_span_trans
-- 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
x : M
s : Set M
rw : Eq (α := Submodule R M) (span R ({x} ∪ s)) (R ∙ x ⊔ span R s)
rw₁ rw₂ : Eq (α := Submodule R M) (R ∙ x ⊔ span R s) (R ∙ x ⊔ span R s)
⊢ Eq (α := Submodule R M) (span R (insert x s)) (R ∙ x ⊔ span R s)

Tactic:
rw [insert_eq, span_union]

Premises used: Set.insert_eq, Submodule.span_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
x : M
s : Set M
h : Membership.mem (γ := Submodule R M) (span R s) x
⊢ Eq (α := Submodule R M) (span R (insert x s)) (span R s)

Tactic:
span_eq_of_le _ (Set.insert_subset_iff.mpr ⟨h, subset_span⟩) (span_mono <| subset_insert _ _)

Premises used: Iff.mpr, Submodule.span_eq_of_le, Set.insert_subset_iff, And.intro, Submodule.span_mono, Submodule.subset_span, Set.subset_insert
-- 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
⊢ Eq (α := Submodule R M) (span R (↑(span R s) : Set M)) (span R s)

Tactic:
span_eq _

Premises used: Submodule.span_eq
-- 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
x : M
s : Set M
y : M
⊢ Membership.mem (γ := Submodule R M) (span R (insert y s)) x ↔
    ∃ (a : R) (z : M), Membership.mem (γ := Submodule R M) (span R s) z ∧ x = a • y + z

Tactic:
simp [span_insert, mem_sup, mem_span_singleton, eq_comm (a := x)]

Premises used: Submodule.mem_span_singleton, eq_comm, Submodule.mem_sup, Submodule.span_insert
-- 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
x y z : M
simp_rw :
  (∃ (a : R) (z_1 : M), Membership.mem (γ := Submodule R M) (R ∙ y) z_1 ∧ z = a • x + z_1) ↔
    ∃ (a : R) (b : R), a • x + b • y = z
simp_rw₁ : (∃ (a : R) (z_1 : M), (∃ (a : R), a • y = z_1) ∧ z = a • x + z_1) ↔ ∃ (a : R) (b : R), a • x + b • y = z
simp_rw₂ : (∃ (a : R) (a_1 : R), z = a • x + a_1 • y) ↔ ∃ (a : R) (b : R), a • x + b • y = z
⊢ Membership.mem (γ := Submodule R M) (span R {x, y}) z ↔ ∃ (a : R) (b : R), a • x + b • y = z

Tactic:
simp_rw [mem_span_insert, mem_span_singleton, exists_exists_eq_and, eq_comm]

Premises used: Submodule.mem_span_singleton, eq_comm, exists_exists_eq_and, Submodule.mem_span_insert
-- 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
w x y z : M
rw :
  (∃ (a : R) (z_1 : M), Membership.mem (γ := Submodule R M) (span R {y, z}) z_1 ∧ w = a • x + z_1) ↔
    ∃ (a : R) (b : R) (c : R), a • x + b • y + c • z = w
⊢ Membership.mem (γ := Submodule R M) (span R {x, y, z}) w ↔ ∃ (a : R) (b : R) (c : R), a • x + b • y + c • z = w

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 : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
w x y z : M
simp_rw :
  (∃ (a : R) (z_1 : M), (∃ (a : R) (b : R), a • y + b • z = z_1) ∧ w = a • x + z_1) ↔
    ∃ (a : R) (b : R) (c : R), a • x + b • y + c • z = w
⊢ (∃ (a : R) (z_1 : M), Membership.mem (γ := Submodule R M) (span R {y, z}) z_1 ∧ w = a • x + z_1) ↔
    ∃ (a : R) (b : R) (c : R), a • x + b • y + c • z = w

Tactic:
simp_rw [mem_span_pair]

Premises used: Submodule.mem_span_pair
-- 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
w x y z : M
⊢ (∃ (a : R) (z_1 : M), (∃ (a : R) (b : R), a • y + b • z = z_1) ∧ w = a • x + z_1) ↔
    ∃ (a : R) (b : R) (c : R), a • x + b • y + c • z = w

Tactic:
exists_congr fun a ↦ ⟨?_, ?_⟩

Premises used: exists_congr, Iff.intro
-- 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
w x y z : M
refine_1 :
  ∀ (a : R),
    (∃ (z_1 : M), (∃ (a : R) (b : R), a • y + b • z = z_1) ∧ w = a • x + z_1) →
      ∃ (b : R) (c : R), a • x + b • y + c • z = w
refine_2 :
  ∀ (a : R),
    (∃ (b : R) (c : R), a • x + b • y + c • z = w) →
      ∃ (z_1 : M), (∃ (a : R) (b : R), a • y + b • z = z_1) ∧ w = a • x + z_1
⊢ (∃ (a : R) (z_1 : M), (∃ (a : R) (b : R), a • y + b • z = z_1) ∧ w = a • x + z_1) ↔
    ∃ (a : R) (b : R) (c : R), a • x + b • y + c • z = w

Tactic:
refine exists_congr fun a ↦ ⟨?_, ?_⟩

Premises used: exists_congr, Iff.intro
-- 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
x y z : M
a b c : R
rw rw₁ : a • x + (b • y + c • z) = a • x + (b • y + c • z)
⊢ a • x + b • y + c • z = a • x + (b • y + c • z)

Tactic:
rw [add_assoc]

Premises used: add_assoc
-- 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
x y z : M
a b c : R
⊢ ∃ (b_1 : R) (c_1 : R), a • x + b_1 • y + c_1 • z = a • x + (b • y + c • z)

Tactic:
exact ⟨b, c, by rw [add_assoc]⟩
-- 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
x y z : M
a b c : R
⊢ ∃ (z_1 : M), (∃ (a : R) (b : R), a • y + b • z = z_1) ∧ a • x + b • y + c • z = a • x + z_1

Tactic:
exact ⟨b • y + c • z, ⟨b, c, rfl⟩, by rw [add_assoc]⟩
-- 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
⊢ Eq (α := Submodule R M) (span R s) ⊥ ↔ ∀ x ∈ s, x = 0

Tactic:
eq_bot_iff.trans
    ⟨fun H _ h => (mem_bot R).1 <| H <| subset_span h, fun H =>
      span_le.2 fun x h => (mem_bot R).2 <| H x h⟩

Premises used: Iff.mpr, Submodule.mem_bot, Iff.intro, Iff.mp, Iff.trans, Submodule.subset_span, eq_bot_iff, Submodule.span_le
-- 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
x : M
⊢ Eq (α := Submodule R M) (R ∙ x) ⊥ ↔ x = 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
rw : Eq (α := Submodule R M) (R ∙ 0) ⊥
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) 0 0
⊢ Eq.{u_4 + 1} (α := Submodule R M) (span R 0) ⊥

Tactic:
rw [← singleton_zero, span_singleton_eq_bot]

Premises used: Submodule.span_singleton_eq_bot, Set.singleton_zero
-- 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
m : M
p : Submodule R M
rw : {m} ⊆ (↑p : Set M) ↔ m ∈ p
rw₁ : m ∈ (↑p : Set M) ↔ m ∈ p
rw₂ rw₃ : m ∈ p ↔ m ∈ p
⊢ R ∙ m ≤ p ↔ m ∈ p

Tactic:
rw [span_le, singleton_subset_iff, SetLike.mem_coe]

Premises used: Set.singleton_subset_iff, SetLike.mem_coe, Submodule.span_le
-- 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
ι : Sort u_9
p : ι → Set M
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : ι), span R (p i)) (span R (⋃ (i : ι), p i))

Tactic:
le_antisymm (iSup_le fun i => span_mono <| subset_iUnion _ i) <|
    span_le.mpr <| iUnion_subset fun i _ hm => mem_iSup_of_mem i <| subset_span hm

Premises used: Iff.mpr, Set.iUnion_subset, Set.subset_iUnion, le_antisymm, Submodule.span_mono, Submodule.mem_iSup_of_mem, iSup_le, Submodule.subset_span, Submodule.span_le
-- 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
ι : Sort u_9
p : ι → Submodule R M
simp_rw : Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : ι), p i) (⨆ (i : ι), span R (↑(p i) : Set M))
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : ι), p i) (span R (⋃ (i : ι), (↑(p i) : Set M)))

Tactic:
simp_rw [← iSup_span, span_eq]

Premises used: Submodule.iSup_span, Submodule.span_eq
-- 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
ι : Sort u_9
p : ι → Submodule R M
h : ι → Prop
simp_rw :
  Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : ι), ⨆ (_ : h i), p i) (⨆ (i : ι), ⨆ (_ : h i), span R (↑(p i) : Set M))
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : ι), ⨆ (_ : h i), p i) (span R (⋃ (i : ι), ⋃ (_ : h i), (↑(p i) : Set M)))

Tactic:
simp_rw [← Submodule.iSup_span, Submodule.span_eq]

Premises used: Submodule.iSup_span, Submodule.span_eq
-- 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
p : Submodule R M
S : Set (Submodule R M) := {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
a : p ≤ sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
a₁ : sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m} ≤ p
⊢ p = sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
p : Submodule R M
S : Set (Submodule R M) := {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
hm : m ∈ p
pos : ∀ (h : m = 0), Membership.mem (γ := Submodule R M) (sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}) m
neg : ∀ (h : ¬m = 0), Membership.mem (γ := Submodule R M) (sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}) m
⊢ Membership.mem (γ := Submodule R M) (sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}) m

Tactic:
by_cases h : m = 0
-- 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
p : Submodule R M
S : Set (Submodule R M) := {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
hm : m ∈ p
h : m = 0
pos : Membership.mem (γ := Submodule R M) (sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}) 0
⊢ Membership.mem (γ := Submodule R M) (sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}) m

Tactic:
rw [h]
-- 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
p : Submodule R M
S : Set (Submodule R M) := {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
hm : m ∈ p
h : m = 0
⊢ Membership.mem (γ := Submodule R M) (sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ 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
p : Submodule R M
S : Set (Submodule R M) := {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
hm : m ∈ p
h : ¬m = 0
⊢ Membership.mem (γ := Submodule R M) (sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}) m

Tactic:
@le_sSup _ _ S _ ⟨m, ⟨hm, ⟨h, rfl⟩⟩⟩ m (mem_span_singleton_self m)

Premises used: Set.Mem, setOf, Submodule.mem_span_singleton_self, And.intro, Exists.intro, le_sSup, 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
p : Submodule R M
S : Set (Submodule R M) := {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
hm : m ∈ p
h : ¬m = 0
⊢ Membership.mem (γ := Submodule R M) (sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}) m

Tactic:
exact @le_sSup _ _ S _ ⟨m, ⟨hm, ⟨h, rfl⟩⟩⟩ m (mem_span_singleton_self m)

Premises used: Submodule.mem_span_singleton_self, And.intro, Exists.intro, le_sSup, 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
p : Submodule R M
S : Set (Submodule R M) := {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
a :
  ∀ (b : Submodule R M),
    Membership.mem (γ := Set (Submodule R M)) {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m} b → b ≤ p
⊢ sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m} ≤ p

Tactic:
rw [sSup_le_iff]

Premises used: sSup_le_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
p : Submodule R M
S : Set (Submodule R M) := {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
w : M
left : w ∈ p
left_1 : w ≠ 0
a a₁ a₂ a₃ : w ∈ p
⊢ R ∙ w ≤ p

Tactic:
rwa [span_singleton_le_iff_mem]

Premises used: Submodule.span_singleton_le_iff_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
I : Submodule R M
a : M
⊢ I < I ⊔ R ∙ a ↔ a ∉ I

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
ι : Sort u_9
p : ι → Submodule R M
m : M
rw : (∀ (b : Submodule R M), (∀ (i : ι), p i ≤ b) → R ∙ m ≤ b) ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
⊢ Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) m ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
rw [← span_singleton_le_iff_mem, le_iSup_iff]

Premises used: Submodule.span_singleton_le_iff_mem, le_iSup_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
ι : Sort u_9
p : ι → Submodule R M
m : M
⊢ (∀ (b : Submodule R M), (∀ (i : ι), p i ≤ b) → R ∙ m ≤ b) ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
simp only [span_singleton_le_iff_mem]

Premises used: Submodule.span_singleton_le_iff_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 (Submodule R M)
m : M
simp_rw : Membership.mem (γ := Submodule R M) (⨆ a ∈ s, a) m ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N
simp_rw₁ :
  (∀ (N : Submodule R M), (∀ (i : Submodule R M), ⨆ (_ : i ∈ s), i ≤ N) → m ∈ N) ↔
    ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N
⊢ m ∈ sSup s ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N

Tactic:
simp_rw [sSup_eq_iSup, Submodule.mem_iSup, iSup_le_iff]

Premises used: sSup_eq_iSup, iSup_le_iff, Submodule.mem_iSup
-- 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
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x

Tactic:
span_induction (fun x hx => ?_) ?_ ?_ ?_ hx

Premises used: Submodule.span_induction