awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Membership.mem (γ := Submodule R M) (span R {x, y}) z ↔ ∃ (a : R) (b : R), a • x + b • y = z
have 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
Tactic: simp_rw [mem_span_insert, mem_span_singleton, exists_exists_eq_and, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Membership.mem (γ := Submodule R M) (span R {x, y}) z ↔ ∃ (a : R) (b : R), a • x + b • y = z
have 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
Tactic: simp_rw [mem_span_insert, mem_span_singleton, exists_exists_eq_and, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Membership.mem (γ := Submodule R M) (span R {x, y}) z ↔ ∃ (a : R) (b : R), a • x + b • y = z
have simp_rw₂ : (∃ (a : R) (a_1 : R), z = a • x + a_1 • y) ↔ ∃ (a : R) (b : R), a • x + b • y = z
Tactic: simp_rw [mem_span_insert, mem_span_singleton, exists_exists_eq_and, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Membership.mem (γ := Submodule R M) (span R {x, y, z}) w ↔ ∃ (a : R) (b : R) (c : R), a • x + b • y + c • z = w
have 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
Tactic: rw [mem_span_insert]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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), 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
have 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
Tactic: simp_rw [mem_span_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
have 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
Tactic: refine exists_congr fun a ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ (∃ (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
have 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
Tactic: refine exists_congr fun a ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ a • x + b • y + c • z = a • x + (b • y + c • z)
have rw : a • x + (b • y + c • z) = a • x + (b • y + c • z)
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq.{u_4 + 1} (α := Submodule R M) (span R 0) ⊥
have rw : Eq (α := Submodule R M) (R ∙ 0) ⊥
Tactic: rw [← singleton_zero, span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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) ⊥
⊢ Eq.{u_4 + 1} (α := Submodule R M) (span R 0) ⊥
have rw₁ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [← singleton_zero, span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ R ∙ m ≤ p ↔ m ∈ p
have rw : {m} ⊆ (↑p : Set M) ↔ m ∈ p
Tactic: rw [span_le, singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ R ∙ m ≤ p ↔ m ∈ p
have rw₁ : m ∈ (↑p : Set M) ↔ m ∈ p
Tactic: rw [span_le, singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ R ∙ m ≤ p ↔ m ∈ p
have rw₂ : m ∈ p ↔ m ∈ p
Tactic: rw [span_le, singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : ι), p i) (span R (⋃ (i : ι), (↑(p i) : Set M)))
have simp_rw : Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : ι), p i) (⨆ (i : ι), span R (↑(p i) : Set M))
Tactic: simp_rw [← iSup_span, span_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : ι), ⨆ (_ : h i), p i) (span R (⋃ (i : ι), ⋃ (_ : h i), (↑(p i) : Set M)))
have simp_rw : Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : ι), ⨆ (_ : h i), p i) (⨆ (i : ι), ⨆ (_ : h i), span R (↑(p i) : Set M))
Tactic: simp_rw [← Submodule.iSup_span, Submodule.span_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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}
⊢ p = sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
have a : p ≤ sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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}
⊢ p = sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
have a₁ : sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m} ≤ p
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Membership.mem (γ := Submodule R M) (sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}) m
have pos : ∀ (h : m = 0), Membership.mem (γ := Submodule R M) (sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}) m
Tactic: by_cases h : m = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Membership.mem (γ := Submodule R M) (sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}) m
have neg : ∀ (h : ¬m = 0), Membership.mem (γ := Submodule R M) (sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}) m
Tactic: by_cases h : m = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
have pos : Membership.mem (γ := Submodule R M) (sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}) 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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}
⊢ sSup {T : Submodule R M | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m} ≤ p
have 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
Tactic: rw [sSup_le_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) m ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
have rw : (∀ (b : Submodule R M), (∀ (i : ι), p i ≤ b) → R ∙ m ≤ b) ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
Tactic: rw [← span_singleton_le_iff_mem, le_iSup_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ m ∈ sSup s ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N
have simp_rw : Membership.mem (γ := Submodule R M) (⨆ a ∈ s, a) m ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N
Tactic: simp_rw [sSup_eq_iSup, Submodule.mem_iSup, iSup_le_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ m ∈ sSup s ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N
have 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
Tactic: simp_rw [sSup_eq_iSup, Submodule.mem_iSup, iSup_le_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
have 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
Tactic: refine span_induction (fun x hx => ?_) ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x
have refine_2 : ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) 0
Tactic: refine span_induction (fun x hx => ?_) ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x
have 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)
Tactic: refine span_induction (fun x hx => ?_) ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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)
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x
have 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)
Tactic: refine span_induction (fun x hx => ?_) ?_ ?_ ?_ hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
have refine_1 : (↑{x} : Set M) ⊆ S
Tactic: refine ⟨{x}, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x
have refine_1₁ : Membership.mem (γ := Submodule R M) (span R (↑{x} : Set M)) x
Tactic: refine ⟨{x}, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ (↑{x} : Set M) ⊆ S
have refine_1 : {x} ⊆ S
Tactic: rwa [Finset.coe_singleton, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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) (span R (↑{x} : Set M)) x
have refine_1 : Membership.mem (γ := Submodule R M) (R ∙ x) x
Tactic: rw [Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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)) 0
have h : (↑∅ : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑∅ : Set M)) 0
Tactic: use ∅
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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)
have refine_3 : (↑(X ∪ Y) : Set M) ⊆ S
Tactic: refine ⟨X ∪ Y, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) (x + y)
have refine_3₁ : Membership.mem (γ := Submodule R M) (span R (↑(X ∪ Y) : Set M)) (x + y)
Tactic: refine ⟨X ∪ Y, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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 ∪ Y) : Set M) ⊆ S
have refine_3 : (↑X : Set M) ∪ (↑Y : Set M) ⊆ S
Tactic: rw [Finset.coe_union]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Membership.mem (γ := Submodule R M) (span R (↑(X ∪ Y) : Set M)) (x + y)
have 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
Tactic: rw [Finset.coe_union, span_union, mem_sup]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
have 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
Tactic: classical
  refine span_induction (fun x hx => ?_) ?_ ?_ ?_ hx
  · refine ⟨{x}, ?_, ?_⟩
    · rwa [Finset.coe_singleton, Set.singleton_subset_iff]
    · rw [Finset.coe_singleton]
      exact Submodule.mem_span_singleton_self x
  · use ∅
    simp
  · rintro x y - - ⟨X, hX, hxX⟩ ⟨Y, hY, hyY⟩
    refine ⟨X ∪ Y, ?_, ?_⟩
    · rw [Finset.coe_union]
      exact Set.union_subset hX hY
    rw [Finset.coe_union, span_union, mem_sup]
    exact ⟨x, hxX, y, hyY, rfl⟩
  · rintro a x - ⟨T, hT, h2⟩
    exact ⟨T, hT, smul_mem _ _ h2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x
have refine_2 : ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) 0
Tactic: classical
  refine span_induction (fun x hx => ?_) ?_ ?_ ?_ hx
  · refine ⟨{x}, ?_, ?_⟩
    · rwa [Finset.coe_singleton, Set.singleton_subset_iff]
    · rw [Finset.coe_singleton]
      exact Submodule.mem_span_singleton_self x
  · use ∅
    simp
  · rintro x y - - ⟨X, hX, hxX⟩ ⟨Y, hY, hyY⟩
    refine ⟨X ∪ Y, ?_, ?_⟩
    · rw [Finset.coe_union]
      exact Set.union_subset hX hY
    rw [Finset.coe_union, span_union, mem_sup]
    exact ⟨x, hxX, y, hyY, rfl⟩
  · rintro a x - ⟨T, hT, h2⟩
    exact ⟨T, hT, smul_mem _ _ h2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ S ∧ Membership.mem (γ := Submodule R M) (span R (↑T : Set M)) x
have 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)
Tactic: classical
  refine span_induction (fun x hx => ?_) ?_ ?_ ?_ hx
  · refine ⟨{x}, ?_, ?_⟩
    · rwa [Finset.coe_singleton, Set.singleton_subset_iff]
    · rw [Finset.coe_singleton]
      exact Submodule.mem_span_singleton_self x
  · use ∅
    simp
  · rintro x y - - ⟨X, hX, hxX⟩ ⟨Y, hY, hyY⟩
    refine ⟨X ∪ Y, ?_, ?_⟩
    · rw [Finset.coe_union]
      exact Set.union_subset hX hY
    rw [Finset.coe_union, span_union, mem_sup]
    exact ⟨x, hxX, y, hyY, rfl⟩
  · rintro a x - ⟨T, hT, h2⟩
    exact ⟨T, hT, smul_mem _ _ h2⟩