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
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
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
⊢ p x hx

Tactic:
have key {v} : v ∈ span R s ↔ v ∈ closure (@univ R • s) := by simp [← span_eq_closure]
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
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
⊢ ∀ (x y : M) (hx : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x)
    (hy : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) y),
    (fun (x : M)
            (hx : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x) ↦
          p x ⋯)
        x hx →
      (fun (x : M)
              (hx :
                Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x) ↦
            p x ⋯)
          y hy →
        (fun (x : M)
              (hx :
                Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x) ↦
            p x ⋯)
          (x + y) ⋯

Tactic:
simpa only [key] using 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
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
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 ⋯)
      x ⋯
⊢ p x hx

Tactic:
refine AddSubmonoid.closure_induction (motive := fun x hx ↦ p x (key.mpr hx))
    ?_ zero (by simpa only [key] using add) (key.mp hx)

Premises used: AddSubmonoid.closure_induction, Iff.mp
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
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_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R s) x_1
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
r : R
left : Membership.mem (γ := Set R) univ r
x : M
hx : x ∈ s
⊢ p ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r x) ⋯

Tactic:
smul_mem r 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 : 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_1 : M
hx_1 : Membership.mem (γ := Submodule R M) (span R s) x_1
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
r : R
left : Membership.mem (γ := Set R) univ r
x : M
hx : x ∈ s
⊢ p ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r x) ⋯

Tactic:
exact smul_mem r 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 : Set M
⊢ Eq (α := Submodule R ↥(span R s))
    (span R (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R s) x) ⁻¹' s)) ⊤

Tactic:
eq_top_iff.2 fun x _ ↦ Subtype.recOn x fun _ hx' ↦
    span_induction (fun _ h ↦ subset_span h) (zero_mem _) (fun _ _ _ _ ↦ add_mem)
      (fun _ _ _ ↦ smul_mem _ _) hx'

Premises used: Iff.mpr, eq_top_iff, Subtype.recOn
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
⊢ Eq.{u_4 + 1} (α := Submodule R ↥(span R s)) (span R {x : ↥(span R s) | (↑x : M) ∈ s}) ⊤

Tactic:
span_span_coe_preimage

Premises used: Set.preimage, Submodule.span_span_coe_preimage
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
M : Type u_4
inst : AddCommMonoid M
s : Set M
⊢ Eq (α := AddSubmonoid M) (toAddSubmonoid (span ℕ s)) (AddSubmonoid.closure s)

Tactic:
Eq.symm (AddSubmonoid.closure_eq_of_le subset_span ?_)

Premises used: AddSubmonoid.closure_eq_of_le, Submodule.subset_span, Eq.symm
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
M : Type u_4
inst : AddCommMonoid M
s : Set M
refine : LE.le (α := AddSubmonoid M) (toAddSubmonoid (span ℕ s)) (AddSubmonoid.closure s)
⊢ Eq (α := AddSubmonoid M) (toAddSubmonoid (span ℕ s)) (AddSubmonoid.closure s)

Tactic:
refine Eq.symm (AddSubmonoid.closure_eq_of_le subset_span ?_)

Premises used: AddSubmonoid.closure_eq_of_le, Submodule.subset_span, Eq.symm
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
M : Type u_4
inst : AddCommMonoid M
s : Set M
rw :
  s ⊆
    (↑((OrderIso.symm (OrderIso.symm AddSubmonoid.toNatSubmodule) : (a : AddSubmonoid M) → Submodule ℕ M)
            (AddSubmonoid.closure s) :
          Submodule ℕ M) :
      Set M)
⊢ LE.le (α := Submodule ℕ M) (span ℕ s)
    ((OrderIso.symm (OrderIso.symm AddSubmonoid.toNatSubmodule) : (a : AddSubmonoid M) → Submodule ℕ M)
      (AddSubmonoid.closure s))

Tactic:
rw [span_le]

Premises used: Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
M : Type u_4
inst : AddCommMonoid M
s : Set M
⊢ s ⊆
    (↑((OrderIso.symm (OrderIso.symm AddSubmonoid.toNatSubmodule) : (a : AddSubmonoid M) → Submodule ℕ M)
            (AddSubmonoid.closure s) :
          Submodule ℕ M) :
      Set M)

Tactic:
AddSubmonoid.subset_closure

Premises used: AddSubmonoid.subset_closure
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
M : Type u_4
inst : AddCommMonoid M
s : Set M
⊢ s ⊆
    (↑((OrderIso.symm (OrderIso.symm AddSubmonoid.toNatSubmodule) : (a : AddSubmonoid M) → Submodule ℕ M)
            (AddSubmonoid.closure s) :
          Submodule ℕ M) :
      Set M)

Tactic:
exact AddSubmonoid.subset_closure

Premises used: AddSubmonoid.subset_closure
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
M : Type u_4
inst : AddCommMonoid M
s : AddSubmonoid M
rw : AddSubmonoid.closure (↑s : Set M) = s
rw₁ rw₂ : s = s
⊢ toAddSubmonoid (span ℕ (↑s : Set M)) = s

Tactic:
rw [span_nat_eq_addSubmonoidClosure, s.closure_eq]

Premises used: AddSubmonoid.closure_eq, Submodule.span_nat_eq_addSubmonoidClosure
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
M : Type u_9
inst : AddCommGroup M
s : Set M
⊢ Eq (α := AddSubgroup M) (toAddSubgroup (module_M := AddCommGroup.toIntModule M) (span ℤ s)) (AddSubgroup.closure s)

Tactic:
Eq.symm <|
    AddSubgroup.closure_eq_of_le _ subset_span fun _ hx =>
      span_induction (fun _ hx => AddSubgroup.subset_closure hx) (AddSubgroup.zero_mem _)
        (fun _ _ _ _ => AddSubgroup.add_mem _) (fun _ _ _ _ => AddSubgroup.zsmul_mem _ ‹_› _) hx

Premises used: Submodule.span_induction, AddSubgroup.closure_eq_of_le, Submodule.subset_span, Eq.symm
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
M : Type u_9
inst : AddCommGroup M
s : AddSubgroup M
rw : AddSubgroup.closure (↑s : Set M) = s
rw₁ rw₂ : s = s
⊢ toAddSubgroup (module_M := AddCommGroup.toIntModule M) (span ℤ (↑s : Set M)) = s

Tactic:
rw [span_int_eq_addSubgroupClosure, s.closure_eq]

Premises used: Submodule.span_int_eq_addSubgroupClosure, AddSubgroup.closure_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
s t : Set M
hst : Disjoint (α := Submodule R M) (span R s) (span R t)
rw : ∀ ⦃a : M⦄, a ∈ s \ {0} → ∀ ⦃b : M⦄, b ∈ t → a ≠ b
⊢ Disjoint (s \ {0}) t

Tactic:
rw [disjoint_iff_forall_ne]

Premises used: Set.disjoint_iff_forall_ne
-- 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 t : Set M
hst : Disjoint (α := Submodule R M) (span R s) (span R t)
v : M
hvs : v ∈ s
hv0 : v ≠ 0
hvt : v ∈ t
⊢ False

Tactic:
hv0 <| (disjoint_def.1 hst) v (subset_span hvs) (subset_span hvt)

Premises used: Iff.mp, Submodule.subset_span, Submodule.disjoint_def
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set M
hst : Disjoint (α := Submodule R M) (span R s) (span R t)
v : M
hvs : v ∈ s
hv0 : v ≠ 0
hvt : v ∈ t
⊢ False

Tactic:
exact hv0 <| (disjoint_def.1 hst) v (subset_span hvs) (subset_span hvt)

Premises used: Iff.mp, Submodule.subset_span, Submodule.disjoint_def
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set M
hst : Disjoint (α := Submodule R M) (span R s) (span R t)
h0s : 0 ∉ s
rw : Disjoint (s \ {0}) t
⊢ Disjoint s t

Tactic:
rw [← diff_singleton_eq_self h0s]

Premises used: Set.diff_singleton_eq_self
-- 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 t : Set M
hst : Disjoint (α := Submodule R M) (span R s) (span R t)
h0s : 0 ∉ s
⊢ Disjoint (s \ {0}) t

Tactic:
hst.of_span

Premises used: Disjoint.of_span
-- 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 t : Set M
hst : Disjoint (α := Submodule R M) (span R s) (span R t)
h0s : 0 ∉ s
⊢ Disjoint (s \ {0}) t

Tactic:
exact hst.of_span

Premises used: Disjoint.of_span
-- 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
⊢ Eq.{u_4 + 1} (α := Submodule R M) (span R ∅) ⊥

Tactic:
(Submodule.gi R M).gc.l_bot

Premises used: Submodule.gi, GaloisConnection.l_bot, GaloisInsertion.gc
-- 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
⊢ Eq.{u_4 + 1} (α := Submodule R M) (span R univ) ⊤

Tactic:
eq_top_iff.2 <| SetLike.le_def.2 <| subset_span

Premises used: Iff.mpr, eq_top_iff, SetLike.le_def, Submodule.subset_span
-- 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 S' : Submodule R M
⊢ span R ((↑S : Set M) ∩ (↑S' : Set M)) = S ⊓ S'

Tactic:
(Submodule.gi R M).l_inf_u S S'

Premises used: Submodule.gi, GaloisInsertion.l_inf_u
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Set M)
⊢ LE.le (α := Submodule R M) (span R (⋂₀ s)) (sInf (span R '' s))

Tactic:
le_sInf fun _ ⟨_, hTs, h⟩ ↦ h ▸ span_mono (sInter_subset_of_mem hTs)

Premises used: Set.Mem, Eq.rec, LE.le, Set.sInter_subset_of_mem, _private.0.Submodule.span_sInf_le.match_1, Submodule.span_mono, Submodule.span, le_sInf, Set.sInter
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
⊢ span R (↑(sInf s) : Set M) = sInf s

Tactic:
span_eq (sInf s)

Premises used: Submodule.span_eq, InfSet.sInf
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
rw : span R (↑(sInf s) : Set M) = sInf s
rw₁ rw₂ : sInf s = sInf s
⊢ span R (⋂ S ∈ s, (↑S : Set M)) = sInf s

Tactic:
rw [← Submodule.coe_sInf, span_eq]

Premises used: Submodule.span_eq, Submodule.coe_sInf
-- 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 t : Set M
⊢ Eq (α := Submodule R M) (span R (s ∪ t)) (span R s ⊔ span R t)

Tactic:
(Submodule.gi R M).gc.l_sup

Premises used: Submodule.gi, GaloisConnection.l_sup, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Set M)
⊢ Eq (α := Submodule R M) (span R (⋃₀ s)) (sSup (span R '' s))

Tactic:
le_antisymm ?_ (sSup_le fun P ⟨t, ht, h⟩ ↦ h ▸ span_mono (subset_sUnion_of_mem ht))

Premises used: Set.sUnion, Eq.rec, LE.le, _private.0.Submodule.span_sSup.match_1, le_antisymm, Submodule.span_mono, Submodule.span, Set.subset_sUnion_of_mem, sSup_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 : Set (Set M)
refine : LE.le (α := Submodule R M) (span R (⋃₀ s)) (sSup (span R '' s))
⊢ Eq (α := 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))
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Set M)
rw : ⋃₀ s ⊆ (↑(sSup (span R '' s)) : Set M)
⊢ LE.le (α := Submodule R M) (span R (⋃₀ s)) (sSup (span R '' s))

Tactic:
rw [span_le]

Premises used: 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 : Set (Set M)
⊢ ⋃₀ s ⊆ (↑(sSup (span R '' s)) : Set M)

Tactic:
fun x ⟨t, hts, hxt⟩ ↦ le_sSup (mem_image_of_mem (span R) hts) (subset_span hxt)

Premises used: Membership.mem, Set.Subset, _private.0.Submodule.span_sSup.match_2, SetLike.coe, Set.mem_image_of_mem, Submodule.span, Set.image, le_sSup, Submodule.subset_span, SupSet.sSup
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Set M)
⊢ ⋃₀ s ⊆ (↑(sSup (span R '' s)) : Set M)

Tactic:
exact fun x ⟨t, hts, hxt⟩ ↦ le_sSup (mem_image_of_mem (span R) hts) (subset_span hxt)
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
⊢ span R (↑(sSup s) : Set M) = sSup s

Tactic:
Submodule.span_eq (sSup s)

Premises used: Submodule.span_eq, SupSet.sSup
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_9
s : ι → Set M
⊢ Eq.{u_4 + 1} (α := Submodule R M) (span R (⋃ (i : ι), s i)) (⨆ (i : ι), span R (s i))

Tactic:
(Submodule.gi R M).gc.l_iSup

Premises used: Submodule.gi, GaloisConnection.l_iSup, Set.iUnion, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_10
κ : ι → Sort u_9
s : (i : ι) → κ i → Set M
⊢ Eq.{u_4 + 1} (α := Submodule R M) (span R (⋃ (i : ι), ⋃ (j : κ i), s i j)) (⨆ (i : ι), ⨆ (j : κ i), span R (s i j))

Tactic:
(Submodule.gi R M).gc.l_iSup₂

Premises used: Submodule.gi, GaloisConnection.l_iSup₂, Set.iUnion, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
⊢ span R (⋃ S ∈ s, (↑S : Set M)) = sSup s

Tactic:
simpa using (Submodule.gi R M).l_sSup_u_image s

Premises used: Submodule.gi, GaloisInsertion.l_sSup_u_image
-- 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
inst_3 : DecidableEq M
α : Type u_9
s : Finset α
f : ↥s → Finset M
⊢ Eq (α := Submodule R M) (span R (↑(s.attach.biUnion f) : Set M)) (⨆ (x : ↥s), span R (↑(f x) : Set M))

Tactic:
simp [span_iUnion]

Premises used: Submodule.span_iUnion
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
s : Set M
rw : p ⊔ span R s = span R (↑p : Set M) ⊔ span R s
rw₁ rw₂ : p ⊔ span R s = p ⊔ span R s
⊢ p ⊔ span R s = span R ((↑p : Set M) ∪ s)

Tactic:
rw [Submodule.span_union, p.span_eq]

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
p : Submodule R M
s : Set M
rw : span R s ⊔ p = span R s ⊔ span R (↑p : Set M)
rw₁ rw₂ : span R s ⊔ p = span R s ⊔ p
⊢ span R s ⊔ p = span R (s ∪ (↑p : Set M))

Tactic:
rw [Submodule.span_union, p.span_eq]

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
s : Set M
⊢ Eq (α := Submodule R M) (span R s) (⨆ x ∈ s, R ∙ x)

Tactic:
simp only [← span_iUnion, Set.biUnion_of_singleton s]

Premises used: Set.biUnion_of_singleton, Submodule.span_iUnion
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_9
v : ι → M
rw : Eq.{u_4 + 1} (α := Submodule R M) (⨆ x ∈ range v, R ∙ x) (⨆ (i : ι), R ∙ v i)
rw₁ rw₂ : Eq.{u_4 + 1} (α := Submodule R M) (⨆ (i : ι), R ∙ v i) (⨆ (i : ι), R ∙ v i)
⊢ Eq (α := Submodule R M) (span R (range v)) (⨆ (i : ι), R ∙ v i)

Tactic:
rw [span_eq_iSup_of_singleton_spans, iSup_range]

Premises used: iSup_range, Submodule.span_eq_iSup_of_singleton_spans
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
rw : r • s ⊆ (↑(span R s) : Set M)
⊢ LE.le (α := Submodule R M) (span R (r • s)) (span R s)

Tactic:
rw [span_le]

Premises used: 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 : Set M
r : R
x : M
hx : x ∈ s
⊢ (fun (x : M) ↦ r • x) x ∈ (↑(span R s) : Set M)

Tactic:
smul_mem (span R s) r (subset_span hx)

Premises used: Set.Mem, Submodule.span, 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 : Set M
r : R
x : M
hx : x ∈ s
⊢ (fun (x : M) ↦ r • x) x ∈ (↑(span R s) : Set M)

Tactic:
exact smul_mem (span R s) r (subset_span hx)

Premises used: Submodule.span, 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
U V W : Set M
hUV : U ⊆ (↑(span R V) : Set M)
hVW : V ⊆ (↑(span R W) : Set M)
⊢ U ⊆ (↑(span R W) : Set M)

Tactic:
(Submodule.gi R M).gc.le_u_l_trans hUV hVW

Premises used: Submodule.gi, GaloisConnection.le_u_l_trans, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_9
inst_3 : Nonempty ι
S : ι → Submodule R M
H : Directed (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) S
⊢ (↑(iSup S) : Set M) = ⋃ (i : ι), (↑(S i) : Set M)

Tactic:
let s : Submodule R M :=
    { __ := AddSubmonoid.copy _ _ (AddSubmonoid.coe_iSup_of_directed H).symm
      smul_mem' := fun r _ hx ↦ have ⟨i, hi⟩ := Set.mem_iUnion.mp hx
        Set.mem_iUnion.mpr ⟨i, (S i).smul_mem' r hi⟩ }
  have : iSup S = s := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set M)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)
  this.symm ▸ rfl

Premises used: Iff.mpr, _private.0.Submodule.coe_iSup_of_directed.match_1, AddSubmonoid.copy, Set.iUnion_subset, Submodule.smul_mem', Submodule.toAddSubmonoid, iSup, Set.mem_iUnion, AddSubsemigroup.carrier, Membership.mem, Eq.rec, le_iSup, AddSubmonoid.toAddSubsemigroup, AddSubmonoid.coe_iSup_of_directed, le_antisymm, SetLike.coe, Exists.intro, Iff.mp, iSup_le, HSMul.hSMul, Submodule.mk, Eq.symm, Set.iUnion, 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
ι : Sort u_9
inst_3 : Nonempty ι
S : ι → Submodule R M
H : Directed (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) S
x : M
rw : (∃ (i : ι), x ∈ (↑(S i) : Set M)) ↔ ∃ (i : ι), x ∈ S i
⊢ x ∈ iSup S ↔ ∃ (i : ι), x ∈ S i

Tactic:
rw [← SetLike.mem_coe, coe_iSup_of_directed S H, mem_iUnion]

Premises used: Set.mem_iUnion, SetLike.mem_coe, Submodule.coe_iSup_of_directed
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_9
inst_3 : Nonempty ι
S : ι → Submodule R M
H : Directed (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) S
x : M
⊢ (∃ (i : ι), x ∈ (↑(S i) : Set M)) ↔ ∃ (i : ι), x ∈ S i

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
s : Set (Submodule R M)
z : M
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) s
⊢ Nonempty.{u_4 + 1} (↑s : Type u_4)

Tactic:
have : Nonempty s := hs.to_subtype
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
z : M
hs : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) s
this : Nonempty.{u_4 + 1} (↑s : Type u_4)
⊢ z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed _ hdir.directed_val, SetCoe.exists,
    exists_prop]

Premises used: SetCoe.exists, exists_prop, DirectedOn.directed_val, Submodule.mem_iSup_of_directed, sSup_eq_iSup'
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : ℕ →o Submodule R M
⊢ (↑(⨆ (k : ℕ), (a : (a : ℕ) → Submodule R M) k) : Set M) =
    ⋃ (k : ℕ), (↑((a : (a : ℕ) → Submodule R M) k : Submodule R M) : Set M)

Tactic:
coe_iSup_of_directed a a.monotone.directed_le

Premises used: OrderHom.monotone, Set.Mem, setOf, Submodule.coe_iSup_of_directed, Monotone.directed_le, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : ℕ →o Submodule R M
m : M
⊢ Membership.mem (γ := Submodule R M) (⨆ (k : ℕ), (a : (a : ℕ) → Submodule R M) k) m ↔
    ∃ (k : ℕ), Membership.mem (γ := Submodule R M) ((a : (a : ℕ) → Submodule R M) k : Submodule R M) m

Tactic:
mem_iSup_of_directed a a.monotone.directed_le

Premises used: OrderHom.monotone, Set.Mem, setOf, Monotone.directed_le, DFunLike.coe, Submodule.mem_iSup_of_directed