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
mem :
  ∀ (x : M) (hx : x ∈ s),
    Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x
zero : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) 0
add :
  ∀ (x y : M),
    Membership.mem (γ := Submodule R M) (span R s) x →
      Membership.mem (γ := Submodule R M) (span R s) y →
        ∀ (h₁ : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x)
          (h₂ : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) y),
          Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (x + y)
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x
have smul : ∀ (r₁ : R) (y : M) (_h : Membership.mem (γ := Submodule R M) (span R s) y)
  (hy : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) y),
  Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • y)
Tactic: induction hx using span_induction with
    | mem x hx => exact subset_closure ⟨1, trivial, x, hx, one_smul R x⟩
    | zero => exact zero_mem _
    | add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
    | smul r₁ y _h hy =>
      clear _h
      induction hy using closure_induction with
      | mem _ h =>
        obtain ⟨r₂, -, x, hx, rfl⟩ := h
        exact subset_closure ⟨r₁ * r₂, trivial, x, hx, mul_smul ..⟩
      | zero => simp only [smul_zero, zero_mem]
      | add _ _ _ _ h₁ h₂ => simpa only [smul_add] using add_mem h₁ h₂
Cleared hypotheses: 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 (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x
⊢ Membership.mem (γ := AddSubmonoid M) (toAddSubmonoid (span R s)) x
have refine : HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s ⊆ (↑(toAddSubmonoid (span R s)) : Set M)
Tactic: refine closure_le.2 ?_ 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 (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x
⊢ Membership.mem (γ := AddSubmonoid M) (toAddSubmonoid (span R s)) x
have case : HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s ⊆ (↑(toAddSubmonoid (span R s)) : Set M)
Tactic: case of_mem_closure =>
    refine closure_le.2 ?_ hx
    rintro - ⟨r, -, x, hx, rfl⟩
    exact smul_mem _ _ (subset_span 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 (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x
case : HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s ⊆ (↑(toAddSubmonoid (span R s)) : Set M)
⊢ Membership.mem (γ := AddSubmonoid M) (toAddSubmonoid (span R s)) x
have case₁ : ∀ (r : R) (x : M) (hx : x ∈ s), (fun (x1 : R) (x2 : M) ↦ x1 • x2) r x ∈ (↑(toAddSubmonoid (span R s)) : Set M)
Tactic: case of_mem_closure =>
    refine closure_le.2 ?_ hx
    rintro - ⟨r, -, x, hx, rfl⟩
    exact smul_mem _ _ (subset_span 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
p : (x : M) → Membership.mem (γ := Submodule R M) (span R s) x → Prop
zero : p 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (span R s) x
⊢ p x hx
have have : ∀
  (key :
    ∀ {v : M},
      Membership.mem (γ := Submodule R M) (span R s) v ↔
        Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) v),
  p x hx
Tactic: have key {v} : v ∈ span R s ↔ v ∈ closure (@univ R • s) := by simp [← span_eq_closure]
-- 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
p : (x : M) → Membership.mem (γ := Submodule R M) (span R s) x → Prop
zero : p 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (span R s) x
key :
  ∀ {v : M},
    Membership.mem (γ := Submodule R M) (span R s) v ↔
      Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) v
⊢ p x hx
have refine : ∀ (x : M) (h : x ∈ HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s),
  (fun (x : M)
        (hx : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x) ↦
      p x sorry)
    x sorry
Tactic: refine AddSubmonoid.closure_induction (motive := fun x hx ↦ p x (key.mpr hx))
    ?_ zero (by simpa only [key] using add) (key.mp hx)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
s : Set M
⊢ Eq (α := AddSubmonoid M) (toAddSubmonoid (span ℕ s)) (AddSubmonoid.closure s)
have refine : LE.le (α := AddSubmonoid M) (toAddSubmonoid (span ℕ s)) (AddSubmonoid.closure s)
Tactic: refine Eq.symm (AddSubmonoid.closure_eq_of_le subset_span ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
s : Set M
⊢ LE.le (α := Submodule ℕ M) (span ℕ s)
    ((OrderIso.symm (OrderIso.symm AddSubmonoid.toNatSubmodule) : (a : AddSubmonoid M) → Submodule ℕ M)
      (AddSubmonoid.closure s))
have rw : s ⊆
  (↑((OrderIso.symm (OrderIso.symm AddSubmonoid.toNatSubmodule) : (a : AddSubmonoid M) → Submodule ℕ M)
          (AddSubmonoid.closure s) :
        Submodule ℕ M) :
    Set M)
Tactic: rw [span_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
s : AddSubmonoid M
⊢ toAddSubmonoid (span ℕ (↑s : Set M)) = s
have rw : AddSubmonoid.closure (↑s : Set M) = s
Tactic: rw [span_nat_eq_addSubmonoidClosure, s.closure_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
s : AddSubmonoid M
rw : AddSubmonoid.closure (↑s : Set M) = s
⊢ toAddSubmonoid (span ℕ (↑s : Set M)) = s
have rw₁ : s = s
Tactic: rw [span_nat_eq_addSubmonoidClosure, s.closure_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
M : Type u_9
inst : AddCommGroup M
s : AddSubgroup M
⊢ toAddSubgroup (module_M := AddCommGroup.toIntModule M) (span ℤ (↑s : Set M)) = s
have rw : AddSubgroup.closure (↑s : Set M) = s
Tactic: rw [span_int_eq_addSubgroupClosure, s.closure_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
M : Type u_9
inst : AddCommGroup M
s : AddSubgroup M
rw : AddSubgroup.closure (↑s : Set M) = s
⊢ toAddSubgroup (module_M := AddCommGroup.toIntModule M) (span ℤ (↑s : Set M)) = s
have rw₁ : s = s
Tactic: rw [span_int_eq_addSubgroupClosure, s.closure_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
s t : Set M
hst : Disjoint (α := Submodule R M) (span R s) (span R t)
⊢ Disjoint (s \ {0}) t
have rw : ∀ ⦃a : M⦄, a ∈ s \ {0} → ∀ ⦃b : M⦄, b ∈ t → a ≠ b
Tactic: rw [disjoint_iff_forall_ne]
-- 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 t : Set M
hst : Disjoint (α := Submodule R M) (span R s) (span R t)
h0s : 0 ∉ s
⊢ Disjoint s t
have rw : Disjoint (s \ {0}) t
Tactic: rw [← diff_singleton_eq_self h0s]
-- 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)
⊢ span R (⋂ S ∈ s, (↑S : Set M)) = sInf s
have rw : span R (↑(sInf s) : Set M) = sInf s
Tactic: rw [← Submodule.coe_sInf, 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
s : Set (Submodule R M)
rw : span R (↑(sInf s) : Set M) = sInf s
⊢ span R (⋂ S ∈ s, (↑S : Set M)) = sInf s
have rw₁ : sInf s = sInf s
Tactic: rw [← Submodule.coe_sInf, 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
s : Set (Set M)
⊢ Eq (α := Submodule R M) (span R (⋃₀ s)) (sSup (span R '' s))
have refine : LE.le (α := Submodule R M) (span R (⋃₀ s)) (sSup (span R '' s))
Tactic: refine le_antisymm ?_ (sSup_le fun P ⟨t, ht, h⟩ ↦ h ▸ span_mono (subset_sUnion_of_mem 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 (Set M)
⊢ LE.le (α := Submodule R M) (span R (⋃₀ s)) (sSup (span R '' s))
have rw : ⋃₀ s ⊆ (↑(sSup (span R '' s)) : Set M)
Tactic: rw [span_le]
-- 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 M
⊢ p ⊔ span R s = span R ((↑p : Set M) ∪ s)
have rw : p ⊔ span R s = span R (↑p : Set M) ⊔ span R s
Tactic: rw [Submodule.span_union, p.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 M
rw : p ⊔ span R s = span R (↑p : Set M) ⊔ span R s
⊢ p ⊔ span R s = span R ((↑p : Set M) ∪ s)
have rw₁ : p ⊔ span R s = p ⊔ span R s
Tactic: rw [Submodule.span_union, p.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 M
⊢ span R s ⊔ p = span R (s ∪ (↑p : Set M))
have rw : span R s ⊔ p = span R s ⊔ span R (↑p : Set M)
Tactic: rw [Submodule.span_union, p.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 M
rw : span R s ⊔ p = span R s ⊔ span R (↑p : Set M)
⊢ span R s ⊔ p = span R (s ∪ (↑p : Set M))
have rw₁ : span R s ⊔ p = span R s ⊔ p
Tactic: rw [Submodule.span_union, p.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
v : ι → M
⊢ Eq (α := Submodule R M) (span R (range v)) (⨆ (i : ι), R ∙ v i)
have rw : Eq.{u_4 + 1} (α := Submodule R M) (⨆ x ∈ range v, R ∙ x) (⨆ (i : ι), R ∙ v i)
Tactic: rw [span_eq_iSup_of_singleton_spans, iSup_range]
-- 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
v : ι → M
rw : Eq.{u_4 + 1} (α := Submodule R M) (⨆ x ∈ range v, R ∙ x) (⨆ (i : ι), R ∙ v i)
⊢ Eq (α := Submodule R M) (span R (range v)) (⨆ (i : ι), R ∙ v i)
have rw₁ : Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : ι), R ∙ v i) (⨆ (i : ι), R ∙ v i)
Tactic: rw [span_eq_iSup_of_singleton_spans, iSup_range]
-- 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
r : R
⊢ LE.le (α := Submodule R M) (span R (r • s)) (span R s)
have rw : r • s ⊆ (↑(span R s) : Set M)
Tactic: rw [span_le]
-- 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
inst_3 : Nonempty ι
S : ι → Submodule R M
H : Directed (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) S
x : M
⊢ x ∈ iSup S ↔ ∃ (i : ι), x ∈ S i
have rw : (∃ (i : ι), x ∈ (↑(S i) : Set M)) ↔ ∃ (i : ι), x ∈ S i
Tactic: rw [← SetLike.mem_coe, coe_iSup_of_directed S H, mem_iUnion]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (hypothesis)
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)
z : M
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) s
⊢ z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y
have this : Nonempty.{u_4 + 1} (↑s : Type u_4)
Tactic: have : Nonempty s := hs.to_subtype
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (hypothesis)
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'
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x
have h₁ : 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
Cleared hypotheses: 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
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
have refine_1 : ∀ (x : M) (h : x ∈ (↑p : Set M) ∪ (↑p' : Set M)), ∃ y ∈ p, ∃ z ∈ p', y + z = x
Tactic: refine span_induction ?_ ?_ ?_ ?_ 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
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
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x
have refine_2 : ∃ y ∈ p, ∃ z ∈ p', y + z = 0
Tactic: refine span_induction ?_ ?_ ?_ ?_ 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
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
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x
have 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
Tactic: refine span_induction ?_ ?_ ?_ ?_ 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
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
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x
have 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
Tactic: refine span_induction ?_ ?_ ?_ ?_ 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
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₁ + y₂ + (z₁ + z₂) = y₁ + z₁ + (y₂ + z₂)
have rw : y₁ + (y₂ + (z₁ + z₂)) = y₁ + z₁ + (y₂ + z₂)
Tactic: rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm 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
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₂)
⊢ y₁ + y₂ + (z₁ + z₂) = y₁ + z₁ + (y₂ + z₂)
have rw₁ : y₁ + (y₂ + (z₁ + z₂)) = y₁ + (z₁ + (y₂ + z₂))
Tactic: rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm 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
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₂))
⊢ y₁ + y₂ + (z₁ + z₂) = y₁ + z₁ + (y₂ + z₂)
have rw₂ : y₁ + (y₂ + z₁ + z₂) = y₁ + (z₁ + (y₂ + z₂))
Tactic: rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm 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
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₂))
⊢ y₁ + y₂ + (z₁ + z₂) = y₁ + z₁ + (y₂ + z₂)
have rw₃ : y₁ + (y₂ + z₁ + z₂) = y₁ + (z₁ + y₂ + z₂)
Tactic: rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm 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
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₂)
⊢ y₁ + y₂ + (z₁ + z₂) = y₁ + z₁ + (y₂ + z₂)
have rw₄ : y₁ + (z₁ + y₂ + z₂) = y₁ + (z₁ + y₂ + z₂)
Tactic: rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm 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
p p' : Submodule R M
⊢ Codisjoint p p' ↔ ∀ (z : M), ∃ (x : M) (y : M), x ∈ p ∧ y ∈ p' ∧ x + y = z
have rw : (∀ (x : M), x ∈ p ⊔ p') ↔ ∀ (z : M), ∃ (x : M) (y : M), x ∈ p ∧ y ∈ p' ∧ x + y = z
Tactic: rw [codisjoint_iff, eq_top_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 p' : Submodule R M
⊢ (↑(p ⊔ p') : Set M) = (↑p : Set M) + (↑p' : Set M)
have h : ∀ (x : M), x ∈ (↑(p ⊔ p') : Set M) ↔ x ∈ (↑p : Set M) + (↑p' : Set M)
Tactic: ext
-- 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 p' : Submodule R M
x : M
⊢ x ∈ (↑(p ⊔ p') : Set M) ↔ x ∈ (↑p : Set M) + (↑p' : Set M)
have h : (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ x_1 ∈ (↑p : Set M), ∃ y ∈ (↑p' : Set M), x_1 + y = x
Tactic: rw [SetLike.mem_coe, mem_sup, Set.mem_add]
-- 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 p' : Submodule R M
⊢ (p ⊔ p').toAddSubmonoid = p.toAddSubmonoid ⊔ p'.toAddSubmonoid
have h : ∀ (x : M), x ∈ (p ⊔ p').toAddSubmonoid ↔ x ∈ p.toAddSubmonoid ⊔ p'.toAddSubmonoid
Tactic: ext 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 p' : Submodule R M
x : M
⊢ x ∈ (p ⊔ p').toAddSubmonoid ↔ x ∈ p.toAddSubmonoid ⊔ p'.toAddSubmonoid
have h : (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubmonoid, ∃ z ∈ p'.toAddSubmonoid, y + z = x
Tactic: rw [mem_toAddSubmonoid, mem_sup, AddSubmonoid.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
p p' : Submodule R M
⊢ p ⊔ p' = ⊤ ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v
have rw : (∀ (x : M), x ∈ p ⊔ p') ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v
Tactic: rw [eq_top_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 p' : Submodule R M
⊢ (∀ (x : M), x ∈ p ⊔ p') ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v
have refine : ∀ (m : M), m ∈ p ⊔ p' ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
Tactic: refine forall_congr' fun m ↦ ?_
-- 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 p' : Submodule R M
m : M
⊢ m ∈ p ⊔ p' ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
have rw : (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
Tactic: rw [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
p p' : Submodule R M
m : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
have mp : (∃ y ∈ p, ∃ z ∈ p', y + z = m) → ∃ u ∈ p, ∃ v ∈ p', m = u + v
Tactic: tauto
-- 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 p' : Submodule R M
m : M
mp : (∃ y ∈ p, ∃ z ∈ p', y + z = m) → ∃ u ∈ p, ∃ v ∈ p', m = u + v
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
have mpr : (∃ u ∈ p, ∃ v ∈ p', m = u + v) → ∃ y ∈ p, ∃ z ∈ p', y + z = m
Tactic: tauto
-- 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 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
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
have mp₁ : ∀ w ∈ p, ∀ w_1 ∈ p', w + w_1 = m → ∃ u ∈ p, ∃ v ∈ p', m = u + v
Tactic: tauto
-- 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 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
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
have mpr₁ : ∀ w ∈ p, ∀ w_1 ∈ p', m = w + w_1 → ∃ y ∈ p, ∃ z ∈ p', y + z = m
Tactic: tauto