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
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: 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
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), (↑T : Set M) ⊆ s ∧ (↑(insert a t) : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
have 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 a t) : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
Tactic: obtain ⟨T, hTs, htT⟩ := IH (by simp_all [Set.insert_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
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), (↑T : Set M) ⊆ s ∧ (↑(insert a t) : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
have 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 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 _ _))
-- 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
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 : Finset M), (↑T : Set M) ⊆ s ∧ (↑(insert a t) : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
have insert : (↑(insert a t) : Set M) ⊆ (↑(span R (↑(T ∪ T') : Set M)) : Set M)
Tactic: refine ⟨T ∪ T', by simp_all, ?_⟩
-- 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
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
⊢ (↑(insert a t) : Set M) ⊆ (↑(span R (↑(T ∪ T') : Set M)) : Set M)
have 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)
Tactic: simp only [Finset.coe_insert, Finset.coe_union, span_union, insert_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
s : Set M
t : Finset M
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)
have 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)
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 _))⟩
Cleared hypotheses: t, ht
-- 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
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)
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
have 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 a t) : Set M) ⊆ (↑(span R s) : Set M)),
  ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑(insert a 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 _))⟩
Cleared hypotheses: t, ht
-- 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
t : Finset M
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)
have 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)
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 _))⟩
Cleared hypotheses: t, ht
-- 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
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)
⊢ ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑t : Set M) ⊆ (↑(span R (↑T : Set M)) : Set M)
have 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 a t) : Set M) ⊆ (↑(span R s) : Set M)),
  ∃ (T : Finset M), (↑T : Set M) ⊆ s ∧ (↑(insert a 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 _))⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ (p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup
have h : ∀ (x : M), x ∈ (p ⊔ p').toAddSubgroup ↔ x ∈ p.toAddSubgroup ⊔ p'.toAddSubgroup
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ x ∈ (p ⊔ p').toAddSubgroup ↔ x ∈ p.toAddSubgroup ⊔ p'.toAddSubgroup
have h : (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubgroup, ∃ z ∈ p'.toAddSubgroup, y + z = x
Tactic: rw [mem_toAddSubgroup, mem_sup, AddSubgroup.mem_sup]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Membership.mem (γ := Submodule R M) (span R (insert y s)) x ↔
    ∃ (a : R), Membership.mem (γ := Submodule R M) (span R s) (x + a • y)
have 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)
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 : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
s : Set M
⊢ (∃ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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)
⊢ (∃ (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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (span R (range v))
have refine_1 : LE.le (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (span R (range v))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
refine_1 :
  LE.le (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (span R (range v))
⊢ Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (span R (range v))
have refine_2 : LE.le (α := Submodule R M) (span R (range v)) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i))))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ LE.le (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (span R (range v))
have refine_1 : ∀ (y : ι), Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) y)
Tactic: simp only [span_le, Set.range_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 : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ LE.le (α := Submodule R M) (span R (range v)) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i))))
have refine_2 : ∀ (y : ι),
  Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v y)
Tactic: simp only [span_le, Set.range_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 : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
⊢ Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) k)
have refine_1 : Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) j)
Tactic: obtain rfl | hjk := eq_or_ne j k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
refine_1 : Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) j)
⊢ Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) k)
have refine_1₁ : ∀ (hjk : j ≠ k),
  Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) k)
Tactic: obtain rfl | hjk := eq_or_ne j k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
⊢ Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v k)
have refine_2 : Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v j)
Tactic: obtain rfl | hjk := eq_or_ne j k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
k : ι
refine_2 :
  Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v j)
⊢ Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v k)
have refine_2₁ : ∀ (hjk : j ≠ k),
  Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v k)
Tactic: obtain rfl | hjk := eq_or_ne j k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ Membership.mem (γ := Submodule R M) (span R (range v)) (update (β := fun (a : ι) ↦ M) v j (v j + r • v i) j)
have refine_1 : Membership.mem (γ := Submodule R M) (span R (range v)) (v j + r • v i)
Tactic: rw [update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i)))) (v j)
have refine_2 : Membership.mem (γ := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + r • v i))))
  (v j + r • v i - r • v i)
Tactic: nth_rw 2 [← add_sub_cancel_right (v j) (r • v i)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j - r • v i)))) (span R (range v))
have rw : Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + -(r • v i))))) (span R (range v))
Tactic: rw [sub_eq_add_neg, ← neg_smul, span_range_update_add_smul hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
rw : Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + -(r • v i))))) (span R (range v))
⊢ Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j - r • v i)))) (span R (range v))
have rw₁ : Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + -r • v i)))) (span R (range v))
Tactic: rw [sub_eq_add_neg, ← neg_smul, span_range_update_add_smul hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_8
inst_3 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
rw : Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + -(r • v i))))) (span R (range v))
rw₁ : Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j + -r • v i)))) (span R (range v))
⊢ Eq (α := Submodule R M) (span R (range (update (β := fun (a : ι) ↦ M) v j (v j - r • v i)))) (span R (range v))
have rw₂ : Eq (α := Submodule R M) (span R (range v)) (span R (range v))
Tactic: rw [sub_eq_add_neg, ← neg_smul, span_range_update_add_smul hij]
-- 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
⊢ IsPrincipal.{u_1, u_4} R ↥p ↔ p.IsPrincipal
have simp_rw : (∃ (a : ↥p), Eq (α := Submodule R ↥p) ⊤ (R ∙ a)) ↔ ∃ (a : M), p = R ∙ a
Tactic: simp_rw [IsPrincipal, isPrincipal_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
p : Submodule R M
⊢ (∃ (a : ↥p), Eq (α := Submodule R ↥p) ⊤ (R ∙ a)) ↔ ∃ (a : M), p = R ∙ a
have mp : (∃ (a : ↥p), Eq (α := Submodule R ↥p) ⊤ (R ∙ a)) → ∃ (a : M), p = R ∙ a
Tactic: constructor
-- 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
mp : (∃ (a : ↥p), Eq (α := Submodule R ↥p) ⊤ (R ∙ a)) → ∃ (a : M), p = R ∙ a
⊢ (∃ (a : ↥p), Eq (α := Submodule R ↥p) ⊤ (R ∙ a)) ↔ ∃ (a : M), p = R ∙ a
have mpr : (∃ (a : M), p = R ∙ a) → ∃ (a : ↥p), Eq (α := Submodule R ↥p) ⊤ (R ∙ a)
Tactic: constructor
-- 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
a : ↥p
ha : Eq (α := Submodule R ↥p) ⊤ (R ∙ a)
⊢ ∃ (a : M), p = R ∙ a
have mp : ∀ (m : M) (hm : m ∈ p), Membership.mem (γ := Submodule R M) (R ∙ (↑a : M)) m
Tactic: refine ⟨a, le_antisymm (fun m hm ↦ ?_) <| (span_singleton_le_iff_mem ..).mpr a.2⟩
-- 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
a : ↥p
ha : Eq (α := Submodule R ↥p) ⊤ (R ∙ a)
m : M
hm : m ∈ p
⊢ Membership.mem (γ := Submodule R M) (R ∙ (↑a : M)) m
have mp : ∀ (r : R) (hr : r • a = Subtype.mk (p := fun (x : M) ↦ x ∈ p) m hm),
  Membership.mem (γ := Submodule R M) (R ∙ (↑a : M)) m
Tactic: have ⟨r, hr⟩ := mem_span_singleton.mp (ha ▸ (trivial : (⟨m, hm⟩ : p) ∈ ⊤))
-- 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
a : M
ha : p = R ∙ a
⊢ ∃ (a : ↥p), Eq (α := Submodule R ↥p) ⊤ (R ∙ a)
have mpr : ∀ (x : ↥p),
  Membership.mem (γ := Submodule R ↥p) ⊤ x →
    Membership.mem (γ := Submodule R ↥p) (R ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ p) a sorry) x
Tactic: refine ⟨⟨a, ha ▸ mem_span_singleton_self a⟩, .symm <| top_unique fun 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
p : Submodule R M
a : M
ha : p = R ∙ a
x : ↥p
h : Membership.mem (γ := Submodule R ↥p) ⊤ x
⊢ Membership.mem (γ := Submodule R ↥p) (R ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ p) a ⋯) x
have mpr : ∀ (r : R) (hr : r • a = (↑x : M)),
  Membership.mem (γ := Submodule R ↥p) (R ∙ Subtype.mk (p := fun (x : M) ↦ x ∈ p) a sorry) x
Tactic: have ⟨r, hr⟩ := mem_span_singleton.mp (ha.le x.2)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
inst_5 : IsPrincipal R M
⊢ ∃ (a : M₂), Eq (α := Submodule R M₂) ⊤ (R ∙ a)
have have : ∀ (m : M) (hm : Eq (α := Submodule R M) ⊤ (R ∙ m)), ∃ (a : M₂), Eq (α := Submodule R M₂) ⊤ (R ∙ a)
Tactic: have ⟨m, hm⟩ := IsPrincipal.principal (⊤ : Submodule R M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
inst_5 : IsPrincipal R M
m : M
hm : Eq (α := Submodule R M) ⊤ (R ∙ m)
⊢ ∃ (a : M₂), Eq (α := Submodule R M₂) ⊤ (R ∙ a)
have refine : ∀ (y : M₂),
  Membership.mem (γ := Submodule R M₂) ⊤ y →
    Membership.mem (γ := Submodule R M₂) (span R (singleton (α := M₂) ((f : (a : M) → M₂) m : M₂))) y
Tactic: refine ⟨f m, .symm <| top_unique fun y _ ↦ ?_⟩