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
p p' : Submodule R M
h : x ∈ p ⊔ p'
⊢ Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x

Tactic:
rw [← span_eq p, ← span_eq p', ← span_union] at h

Premises used: Submodule.span_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
p p' : Submodule R M
h : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x

Tactic:
span_induction ?_ ?_ ?_ ?_ h

Premises used: Submodule.span_induction
-- 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
p p' : Submodule R M
h : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
refine_1 : ∀ (x : M) (h : x ∈ (↑p : Set M) ∪ (↑p' : Set M)), ∃ y ∈ p, ∃ z ∈ p', y + z = x
refine_2 : ∃ y ∈ p, ∃ z ∈ p', y + z = 0
refine_3 :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x)
    (hy : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) y),
    (∃ y ∈ p, ∃ z ∈ p', y + z = x) → (∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = y) → ∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = x + y
refine_4 :
  ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x),
    (∃ y ∈ p, ∃ z ∈ p', y + z = x) → ∃ y ∈ p, ∃ z ∈ p', y + z = a • x
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x

Tactic:
refine span_induction ?_ ?_ ?_ ?_ 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
x : M
p p' : Submodule R M
h_1 : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
y : M
h : y ∈ (↑p : Set M)
⊢ 0 ∈ p'

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
x : M
p p' : Submodule R M
h_1 : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
y : M
h : y ∈ (↑p : Set M)
⊢ y + 0 = y

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
x : M
p p' : Submodule R M
h_1 : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
y : M
h : y ∈ (↑p : Set M)
⊢ ∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = y

Tactic:
exact ⟨y, h, 0, by simp, 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
x : M
p p' : Submodule R M
h_1 : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
y : M
h : y ∈ (↑p' : Set M)
⊢ 0 ∈ p

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
x : M
p p' : Submodule R M
h_1 : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
y : M
h : y ∈ (↑p' : Set M)
⊢ 0 + y = y

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
x : M
p p' : Submodule R M
h_1 : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
y : M
h : y ∈ (↑p' : Set M)
⊢ ∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = y

Tactic:
exact ⟨0, by simp, y, h, 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
x : M
p p' : Submodule R M
h : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
⊢ 0 ∈ p

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
x : M
p p' : Submodule R M
h : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
⊢ 0 ∈ p' ∧ HAdd.hAdd (α := M) 0 0 = 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
x : M
p p' : Submodule R M
h : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = 0

Tactic:
exact ⟨0, by simp, 0, 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
x : M
p p' : Submodule R M
h : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
y₁ : M
hy₁ : y₁ ∈ p
z₁ : M
hz₁ : z₁ ∈ p'
y₂ : M
hy₂ : y₂ ∈ p
z₂ : M
hz₂ : z₂ ∈ p'
rw : y₁ + (y₂ + (z₁ + z₂)) = y₁ + z₁ + (y₂ + z₂)
rw₁ : y₁ + (y₂ + (z₁ + z₂)) = y₁ + (z₁ + (y₂ + z₂))
rw₂ : y₁ + (y₂ + z₁ + z₂) = y₁ + (z₁ + (y₂ + z₂))
rw₃ : y₁ + (y₂ + z₁ + z₂) = y₁ + (z₁ + y₂ + z₂)
rw₄ rw₅ : y₁ + (z₁ + y₂ + z₂) = y₁ + (z₁ + y₂ + z₂)
⊢ y₁ + y₂ + (z₁ + z₂) = y₁ + z₁ + (y₂ + z₂)

Tactic:
rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm y₂]

Premises used: add_assoc, add_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
x : M
p p' : Submodule R M
h : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
y₁ : M
hy₁ : y₁ ∈ p
z₁ : M
hz₁ : z₁ ∈ p'
y₂ : M
hy₂ : y₂ ∈ p
z₂ : M
hz₂ : z₂ ∈ p'
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = y₁ + z₁ + (y₂ + z₂)

Tactic:
exact ⟨_, add_mem hy₁ hy₂, _, add_mem hz₁ hz₂, by
        rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm 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
x : M
p p' : Submodule R M
h : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
a : R
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) (y + z)
⊢ a • y + a • z = a • (y + z)

Tactic:
simp [smul_add]

Premises used: smul_add
-- 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
p p' : Submodule R M
h : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) x
a : R
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : Membership.mem (γ := Submodule R M) (span R ((↑p : Set M) ∪ (↑p' : Set M))) (y + z)
⊢ ∃ y_1 ∈ p, ∃ z_1 ∈ p', y_1 + z_1 = a • (y + z)

Tactic:
exact ⟨_, smul_mem _ a hy, _, smul_mem _ a hz, by simp [smul_add]⟩
-- 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 p' : Submodule R M
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
⊢ y + z ∈ p ⊔ p'

Tactic:
add_mem ((le_sup_left : p ≤ p ⊔ p') hy) ((le_sup_right : p' ≤ p ⊔ p') hz)

Premises used: le_sup_left, le_sup_right, AddMemClass.add_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
p p' : Submodule R M
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
⊢ y + z ∈ p ⊔ p'

Tactic:
exact add_mem ((le_sup_left : p ≤ p ⊔ p') hy) ((le_sup_right : p' ≤ p ⊔ p') hz)

Premises used: le_sup_left, le_sup_right, AddMemClass.add_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
x : M
p p' : Submodule R M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ (y : ↥p) (z : ↥p'), (↑y : M) + (↑z : M) = x

Tactic:
simp only [Subtype.exists, exists_prop]

Premises used: Subtype.exists, exists_prop
-- 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 p' : Submodule R M
rw : (∀ (x : M), x ∈ p ⊔ p') ↔ ∀ (z : M), ∃ (x : M) (y : M), x ∈ p ∧ y ∈ p' ∧ x + y = z
⊢ Codisjoint p p' ↔ ∀ (z : M), ∃ (x : M) (y : M), x ∈ p ∧ y ∈ p' ∧ x + y = z

Tactic:
rw [codisjoint_iff, eq_top_iff']

Premises used: Submodule.eq_top_iff', codisjoint_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 p' : Submodule R M
z : M
⊢ (∃ y ∈ p, ∃ z_1 ∈ p', y + z_1 = z) ↔ ∃ (x : M) (y : M), x ∈ p ∧ y ∈ p' ∧ x + y = z

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 p' : Submodule R M
⊢ (∀ (x : M), x ∈ p ⊔ p') ↔ ∀ (z : M), ∃ (x : M) (y : M), x ∈ p ∧ y ∈ p' ∧ x + y = z

Tactic:
exact forall_congr' (fun z => mem_sup.trans <| by simp)

Premises used: forall_congr', Iff.trans, Submodule.mem_sup
-- 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 p' : Submodule R M
h : ∀ (x : M), x ∈ (↑(p ⊔ p') : Set M) ↔ x ∈ (↑p : Set M) + (↑p' : Set M)
⊢ (↑(p ⊔ p') : Set M) = (↑p : Set M) + (↑p' : Set M)

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
p p' : Submodule R M
x : M
h : (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ x_1 ∈ (↑p : Set M), ∃ y ∈ (↑p' : Set M), x_1 + y = x
⊢ x ∈ (↑(p ⊔ p') : Set M) ↔ x ∈ (↑p : Set M) + (↑p' : Set M)

Tactic:
rw [SetLike.mem_coe, mem_sup, Set.mem_add]

Premises used: SetLike.mem_coe, Submodule.mem_sup, Set.mem_add
-- 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 p' : Submodule R M
x : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ x_1 ∈ (↑p : Set M), ∃ y ∈ (↑p' : Set M), x_1 + y = x

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 p' : Submodule R M
h : ∀ (x : M), x ∈ (p ⊔ p').toAddSubmonoid ↔ x ∈ p.toAddSubmonoid ⊔ p'.toAddSubmonoid
⊢ (p ⊔ p').toAddSubmonoid = p.toAddSubmonoid ⊔ p'.toAddSubmonoid

Tactic:
ext 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
p p' : Submodule R M
x : M
h : (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubmonoid, ∃ z ∈ p'.toAddSubmonoid, y + z = x
⊢ x ∈ (p ⊔ p').toAddSubmonoid ↔ x ∈ p.toAddSubmonoid ⊔ p'.toAddSubmonoid

Tactic:
rw [mem_toAddSubmonoid, mem_sup, AddSubmonoid.mem_sup]

Premises used: Submodule.mem_toAddSubmonoid, AddSubmonoid.mem_sup, Submodule.mem_sup
-- 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 p' : Submodule R M
x : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubmonoid, ∃ z ∈ p'.toAddSubmonoid, y + z = x

Tactic:
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 p' : Submodule R M
rw : (∀ (x : M), x ∈ p ⊔ p') ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v
⊢ p ⊔ p' = ⊤ ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v

Tactic:
rw [eq_top_iff']

Premises used: Submodule.eq_top_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 p' : Submodule R M
⊢ (∀ (x : M), x ∈ p ⊔ p') ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v

Tactic:
forall_congr' fun m ↦ ?_

Premises used: forall_congr'
-- 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 p' : Submodule R M
refine : ∀ (m : M), m ∈ p ⊔ p' ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
⊢ (∀ (x : M), x ∈ p ⊔ p') ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v

Tactic:
refine forall_congr' fun m ↦ ?_

Premises used: forall_congr'
-- 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 p' : Submodule R M
m : M
rw : (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
⊢ m ∈ p ⊔ p' ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v

Tactic:
rw [mem_sup]

Premises used: Submodule.mem_sup
-- 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 p' : Submodule R M
m : M
mp : (∃ y ∈ p, ∃ z ∈ p', y + z = m) → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr : (∃ u ∈ p, ∃ v ∈ p', m = u + v) → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₁ mp₂ mp₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₁ mpr₂ mpr₃ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₄ mp₅ mp₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mpr₄ mpr₅ mpr₆ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mp₇ mp₈ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
mp₉ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₀ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₁ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p ∧ ∃ v ∈ p', m = w + v
mp₁₂ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₃ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p
mp₁₄ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mp₁₅ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₆ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → w ∈ p
mp₁₇ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mp₁₈ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → w + w_1 = m → M
mp₁₉ mp₂₀ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ v ∈ p', m = w + v
mpr₇ mpr₈ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
mpr₉ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → w ∈ p ∧ ∃ z ∈ p', w + z = m
mpr₁₀ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → m = w + w_1 → M
mpr₁₁ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → w ∈ p ∧ ∃ z ∈ p', w + z = m
mpr₁₂ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → m = w + w_1 → M
mpr₁₃ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → w ∈ p
mpr₁₄ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ z ∈ p', w + z = m
mpr₁₅ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → m = w + w_1 → M
mpr₁₆ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → w ∈ p
mpr₁₇ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ z ∈ p', w + z = m
mpr₁₈ : (w : M) → w ∈ p → (w_1 : M) → w_1 ∈ p' → m = w + w_1 → M
mpr₁₉ mpr₂₀ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ z ∈ p', w + z = m
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + 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
p p' : Submodule R M
P : M → Prop
simp : (∀ (x x_1 : M), x_1 ∈ p → ∀ x_2 ∈ p', x_1 + x_2 = x → P x) ↔ ∀ x₁ ∈ p, ∀ x₂ ∈ p', P (x₁ + x₂)
⊢ (∀ x ∈ p ⊔ p', P x) ↔ ∀ x₁ ∈ p, ∀ x₂ ∈ p', P (x₁ + x₂)

Tactic:
simp [mem_sup]

Premises used: Submodule.mem_sup
-- 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 p' : Submodule R M
P : M → Prop
⊢ (∀ (x x_1 : M), x_1 ∈ p → ∀ x_2 ∈ p', x_1 + x_2 = x → P x) ↔ ∀ x₁ ∈ p, ∀ x₂ ∈ p', P (x₁ + x₂)

Tactic:
aesop
-- 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 p' : Submodule R M
P : M → Prop
⊢ (∃ x ∈ p ⊔ p', P x) ↔ ∃ x₁ ∈ p, ∃ x₂ ∈ p', P (x₁ + x₂)

Tactic:
simp [mem_sup]

Premises used: Submodule.mem_sup
-- 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 ∙ x) x

Tactic:
subset_span rfl

Premises used: Submodule.subset_span, 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
x : M
h : x ≠ 0
h₁ : Ne (α := ↥(R ∙ x)) 0 (Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ x) x_1) x ⋯)
⊢ ∃ (x_1 : ↥(R ∙ x)) (y : ↥(R ∙ x)), x_1 ≠ y

Tactic:
use 0, ⟨x, Submodule.mem_span_singleton_self 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
x : M
h : x ≠ 0
H : Eq (α := ↥(R ∙ x)) 0 (Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submodule R M) (R ∙ x) x_1) x ⋯)
⊢ x = 0

Tactic:
rw [eq_comm, Submodule.mk_eq_zero] at H

Premises used: eq_comm, Submodule.mk_eq_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
x : M
h : x ≠ 0
H : x = 0
⊢ False

Tactic:
h 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
x : M
h : x ≠ 0
H : x = 0
⊢ False

Tactic:
exact h 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
x y : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
⊢ ∃ (a : R), a • y = x

Tactic:
span_induction ?_ ?_ ?_ ?_ h

Premises used: Submodule.span_induction
-- 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 : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
refine_1 : ∀ (x : M) (h : Membership.mem (γ := Set M) {y} x), ∃ (a : R), a • y = x
refine_2 : ∃ (a : R), a • y = 0
refine_3 :
  ∀ (x y_1 : M) (hx : Membership.mem (γ := Submodule R M) (R ∙ y) x)
    (hy : Membership.mem (γ := Submodule R M) (R ∙ y) y_1),
    (∃ (a : R), a • y = x) → (∃ (a : R), a • y = y_1) → ∃ (a : R), a • y = x + y_1
refine_4 :
  ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (R ∙ y) x),
    (∃ (a : R), a • y = x) → ∃ (a_2 : R), a_2 • y = a • x
⊢ ∃ (a : R), a • y = x

Tactic:
refine span_induction ?_ ?_ ?_ ?_ 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
x y : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) 1 y = y

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
x y : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
⊢ ∃ (a : R), a • y = y

Tactic:
exact ⟨1, 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
x y : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) 0 y = 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
x y : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
⊢ ∃ (a : R), a • y = 0

Tactic:
exact ⟨0, 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
x y : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
a b : R
⊢ (a + b) • y = a • y + b • y

Tactic:
simp [add_smul]

Premises used: add_smul
-- 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 : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
a b : R
⊢ ∃ (a_1 : R), a_1 • y = a • y + b • y

Tactic:
exact ⟨a + b, by simp [add_smul]⟩
-- 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 : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
a b : R
⊢ (a * b) • y = a • b • y

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- 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 : M
h : Membership.mem (γ := Submodule R M) (R ∙ y) x
a b : R
⊢ ∃ (a_1 : R), a_1 • y = a • b • y

Tactic:
exact ⟨a * b, by simp [smul_smul]⟩
-- 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
a : R
⊢ Membership.mem (γ := Set M) {y} y

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
y : M
a : R
⊢ Membership.mem (γ := Submodule R M) (R ∙ y) (a • y)

Tactic:
exact smul_mem _ _ (subset_span <| by simp)

Premises used: Submodule.subset_span, 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 : Submodule R M
f : LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥s
hf : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := ↥s) (⇑f : (a : R) → ↥s)
⊢ (↑((f : (a : R) → ↥s) 1) : M) ∈ (↑s : Set M)

Tactic:
(f 1).2

Premises used: OfNat.ofNat, DFunLike.coe, Subtype.property
-- 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 : Submodule R M
f : LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥s
hf : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := ↥s) (⇑f : (a : R) → ↥s)
⊢ (↑((f : (a : R) → ↥s) 1) : M) ∈ (↑s : Set M)

Tactic:
exact (f 1).2

Premises used: OfNat.ofNat, DFunLike.coe, Subtype.property
-- 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 : Submodule R M
f : LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥s
hf : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := ↥s) (⇑f : (a : R) → ↥s)
refine : ∀ (x : M) (hx : x ∈ s), ∃ (a : R), HSMul.hSMul (β := M) a (↑((f : (a : R) → ↥s) 1) : M) = x
⊢ s = R ∙ (↑((f : (a : R) → ↥s) 1) : M)

Tactic:
refine le_antisymm (fun x hx ↦ mem_span_singleton.mpr ?_)
    (span_le.mpr <| by rintro _ rfl; exact (f 1).2)

Premises used: Iff.mpr, le_antisymm, 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 : Submodule R M
f : LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥s
hf : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := ↥s) (⇑f : (a : R) → ↥s)
x : M
hx : x ∈ s
have :
  ∀ (r : R) (eq : (f : (a : R) → ↥s) r = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx),
    ∃ (a : R), HSMul.hSMul (β := M) a (↑((f : (a : R) → ↥s) 1) : M) = x
⊢ ∃ (a : R), HSMul.hSMul (β := M) a (↑((f : (a : R) → ↥s) 1) : M) = x

Tactic:
have ⟨r, eq⟩ := hf ⟨x, 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 : Submodule R M
f : LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥s
hf : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := ↥s) (⇑f : (a : R) → ↥s)
x : M
hx : x ∈ s
r : R
eq : (f : (a : R) → ↥s) r = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx
rw : (↑(HSMul.hSMul (β := ↥s) r ((f : (a : R) → ↥s) 1)) : M) = x
rw₁ : (↑((f : (a : R) → ↥s) (HSMul.hSMul (β := R) r 1)) : M) = x
rw₂ : (↑((f : (a : R) → ↥s) (r * 1)) : M) = x
rw₃ : (↑((f : (a : R) → ↥s) r) : M) = x
rw₄ rw₅ : (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx) : M) = x
⊢ HSMul.hSMul (β := M) r (↑((f : (a : R) → ↥s) 1) : M) = x

Tactic:
rw [← coe_smul, ← map_smul, smul_eq_mul, mul_one, eq]

Premises used: Submodule.coe_smul, smul_eq_mul, mul_one, map_smul
-- 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 : Submodule R M
f : LinearMap.{u_1, u_1, u_1, u_4} (RingHom.id R) R ↥s
hf : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := ↥s) (⇑f : (a : R) → ↥s)
x : M
hx : x ∈ s
r : R
eq : (f : (a : R) → ↥s) r = Subtype.mk (p := fun (x : M) ↦ x ∈ s) x hx
⊢ ∃ (a : R), HSMul.hSMul (β := M) a (↑((f : (a : R) → ↥s) 1) : M) = x

Tactic:
exact ⟨r, by rw [← coe_smul, ← map_smul, smul_eq_mul, mul_one, 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
rw : (∀ (v : M), Membership.mem (γ := Submodule R M) ⊤ v → ∃ (r : R), r • x = v) ↔ ∀ (v : M), ∃ (r : R), r • x = v
⊢ Eq (α := Submodule R M) (R ∙ x) ⊤ ↔ ∀ (v : M), ∃ (r : R), r • x = v

Tactic:
rw [eq_top_iff, le_span_singleton_iff]

Premises used: eq_top_iff, Submodule.le_span_singleton_iff