awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
refine :
  ∀ (f : α →₀ M),
    Membership.mem (γ := Submodule R (α →₀ M)) ⊤ f →
      Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (a : α), LinearMap.range (lsingle a)) f
⊢ Eq (α := Submodule R (α →₀ M)) (⨆ (a : α), LinearMap.range (lsingle a)) ⊤

Tactic:
refine eq_top_iff.2 <| SetLike.le_def.2 fun f _ => ?_

Premises used: Iff.mpr, eq_top_iff, SetLike.le_def
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α →₀ M
h : Membership.mem (γ := Submodule R (α →₀ M)) ⊤ f
rw : Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (a : α), LinearMap.range (lsingle a)) (f.sum single)
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (a : α), LinearMap.range (lsingle a)) f

Tactic:
rw [← sum_single f]

Premises used: Finsupp.sum_single
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α →₀ M
h : Membership.mem (γ := Submodule R (α →₀ M)) ⊤ f
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (a : α), LinearMap.range (lsingle a)) (f.sum single)

Tactic:
sum_mem fun a _ => Submodule.mem_iSup_of_mem a ⟨_, rfl⟩

Premises used: Set.Mem, Finsupp.sum, Exists.intro, Submodule.mem_iSup_of_mem, DFunLike.coe, sum_mem, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : α →₀ M
h : Membership.mem (γ := Submodule R (α →₀ M)) ⊤ f
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (⨆ (a : α), LinearMap.range (lsingle a)) (f.sum single)

Tactic:
exact sum_mem fun a _ => Submodule.mem_iSup_of_mem a ⟨_, rfl⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
⊢ Disjoint (α := Submodule R (α →₀ M)) (⨆ a ∈ s, LinearMap.range (lsingle a)) (⨆ a ∈ t, LinearMap.range (lsingle a))

Tactic:
(Disjoint.mono
      (lsingle_range_le_ker_lapply s sᶜ disjoint_compl_right)
      (lsingle_range_le_ker_lapply t tᶜ disjoint_compl_right))
      ?_

Premises used: Compl.compl, disjoint_compl_right, Disjoint.mono, Finsupp.lsingle_range_le_ker_lapply
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
s₁ : Disjoint (α := Submodule R (α →₀ M)) (⨅ a ∈ sᶜ, ker (lapply a)) (⨅ a ∈ tᶜ, ker (lapply a))
⊢ Disjoint (α := Submodule R (α →₀ M)) (⨆ a ∈ s, LinearMap.range (lsingle a)) (⨆ a ∈ t, LinearMap.range (lsingle a))

Tactic:
refine
    (Disjoint.mono
      (lsingle_range_le_ker_lapply s sᶜ disjoint_compl_right)
      (lsingle_range_le_ker_lapply t tᶜ disjoint_compl_right))
      ?_

Premises used: Compl.compl, disjoint_compl_right, Disjoint.mono, Finsupp.lsingle_range_le_ker_lapply
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
rw : LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) ⊥
⊢ Disjoint (α := Submodule R (α →₀ M)) (⨅ a ∈ sᶜ, ker (lapply a)) (⨅ a ∈ tᶜ, ker (lapply a))

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) ⊥

Tactic:
le_trans (le_iInf fun i => ?_) iInf_ker_lapply_le_bot

Premises used: Finsupp.iInf_ker_lapply_le_bot, le_iInf, le_trans
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
refine :
  ∀ (i : α), LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) ⊥

Tactic:
refine le_trans (le_iInf fun i => ?_) iInf_ker_lapply_le_bot

Premises used: Finsupp.iInf_ker_lapply_le_bot, le_iInf, le_trans
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
pos :
  ∀ (his : i ∈ s),
    LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
neg :
  ∀ (his : i ∉ s),
    LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))

Tactic:
by_cases his : i ∈ s
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
pos :
  ∀ (hit : i ∈ t),
    LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
neg :
  ∀ (hit : i ∉ t),
    LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))

Tactic:
by_cases hit : i ∈ t
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : i ∈ t
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))

Tactic:
(hs.le_bot ⟨his, hit⟩).elim

Premises used: Disjoint.le_bot, False.elim, And.intro
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : i ∈ t
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))

Tactic:
exact (hs.le_bot ⟨his, hit⟩).elim

Premises used: Disjoint.le_bot, False.elim, And.intro
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : i ∉ t
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))

Tactic:
inf_le_of_right_le (iInf_le_of_le i <| iInf_le _ hit)

Premises used: inf_le_of_right_le, iInf_le_of_le, iInf_le
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∈ s
hit : i ∉ t
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))

Tactic:
exact inf_le_of_right_le (iInf_le_of_le i <| iInf_le _ hit)

Premises used: inf_le_of_right_le
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∉ s
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))

Tactic:
inf_le_of_left_le (iInf_le_of_le i <| iInf_le _ his)

Premises used: inf_le_of_left_le, iInf_le_of_le, iInf_le
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∉ s
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))

Tactic:
exact inf_le_of_left_le (iInf_le_of_le i <| iInf_le _ his)

Premises used: inf_le_of_left_le
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Set α
hs : Disjoint s t
i : α
pos :
  ∀ (his : i ∈ s),
    LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
neg neg₁ :
  ∀ (his : i ∉ s),
    LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))
⊢ LE.le (α := Submodule R (α →₀ M)) ((⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a)) (ker (lapply i))

Tactic:
classical
    by_cases his : i ∈ s
    · by_cases hit : i ∈ t
      · exact (hs.le_bot ⟨his, hit⟩).elim
      exact inf_le_of_right_le (iInf_le_of_le i <| iInf_le _ hit)
    exact inf_le_of_left_le (iInf_le_of_le i <| iInf_le _ his)
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
a : α
rw : Eq (α := Submodule R (α →₀ M)) (span R (single a '' s)) (span R ((⇑(lsingle a) : (a : M) → α →₀ M) '' s))
⊢ Eq (α := Submodule R (α →₀ M)) (span R (single a '' s)) (map (lsingle a) (span R s))

Tactic:
rw [← span_image]

Premises used: Submodule.span_image
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
a : α
⊢ Eq (α := Submodule R (α →₀ M)) (span R (single a '' s)) (span R ((⇑(lsingle a) : (a : M) → α →₀ M) '' s))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
⊢ Eq (α := Submodule R (β →₀ R)) (LinearMap.range (lmapDomain R R u)) (span R (Set.range fun (x : α) ↦ single (u x) 1))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
refine_1 :
  LE.le (α := Submodule R (β →₀ R)) (LinearMap.range (lmapDomain R R u))
    (span R (Set.range fun (x : α) ↦ single (u x) 1))
refine_2 :
  LE.le (α := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (LinearMap.range (lmapDomain R R u))
⊢ Eq (α := Submodule R (β →₀ R)) (LinearMap.range (lmapDomain R R u)) (span R (Set.range fun (x : α) ↦ single (u x) 1))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
i : α
s : R
refine_1 :
  Membership.mem (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (HSMul.hSMul (β := β →₀ R) s (single (u i) 1))
⊢ Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) (single i s) : β →₀ R)

Tactic:
rw [lmapDomain_apply, mapDomain_single, ← Finsupp.smul_single_one]

Premises used: Finsupp.mapDomain_single, Finsupp.smul_single_one, Finsupp.lmapDomain_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
i : α
s : R
⊢ Membership.mem (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (HSMul.hSMul (β := β →₀ R) s (single (u i) 1))

Tactic:
Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)

Premises used: Set.Mem, Exists.intro, Submodule.subset_span, rfl, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
i : α
s : R
⊢ Membership.mem (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (HSMul.hSMul (β := β →₀ R) s (single (u i) 1))

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
⊢ Membership.mem (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) 0)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
f g : α →₀ R
hf :
  Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) f : β →₀ R)
hg :
  Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) g : β →₀ R)
refine_1 :
  Membership.mem (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (HAdd.hAdd (α := β →₀ R) (β := β →₀ R) ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) f : β →₀ R)
      ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) g : β →₀ R))
⊢ Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) (f + g) : β →₀ R)

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
f g : α →₀ R
hf :
  Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) f : β →₀ R)
hg :
  Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) g : β →₀ R)
⊢ Membership.mem (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (HAdd.hAdd (α := β →₀ R) (β := β →₀ R) ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) f : β →₀ R)
      ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) g : β →₀ R))

Tactic:
Submodule.add_mem _ hf hg

Premises used: Set.Mem, Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
f g : α →₀ R
hf :
  Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) f : β →₀ R)
hg :
  Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) g : β →₀ R)
⊢ Membership.mem (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (HAdd.hAdd (α := β →₀ R) (β := β →₀ R) ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) f : β →₀ R)
      ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) g : β →₀ R))

Tactic:
exact Submodule.add_mem _ hf hg

Premises used: Submodule.add_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
x : α →₀ R
refine_1 :
  ∀ (i : α) (s : R),
    Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
      ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) (single i s) : β →₀ R)
refine_1₁ :
  Membership.mem (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) 0)
refine_1₂ :
  ∀ (f g : α →₀ R)
    (hf :
      Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
        ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) f : β →₀ R))
    (hg :
      Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
        ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) g : β →₀ R)),
    Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
      ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) (f + g) : β →₀ R)
⊢ Membership.mem (α := β →₀ R) (γ := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) x : β →₀ R)

Tactic:
induction x using induction_linear with
    | single i s =>
        rw [lmapDomain_apply, mapDomain_single, ← Finsupp.smul_single_one]
        exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)
    | zero => simp
    | add f g hf hg =>
        rw [map_add]
        exact Submodule.add_mem _ hf hg

Premises used: map_add, Finsupp.mapDomain_single, Submodule.zero, Submodule.add, Finsupp.smul_single_one, Finsupp.lmapDomain_apply, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
refine_2 : ∀ (y : α), single (u y) 1 ∈ (↑(LinearMap.range (lmapDomain R R u)) : Set (β →₀ R))
⊢ LE.le (α := Submodule R (β →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (LinearMap.range (lmapDomain R R u))

Tactic:
rw [Submodule.span_le, Set.range_subset_iff]

Premises used: Set.range_subset_iff, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
i : α
⊢ Eq (α := β →₀ R) ((lmapDomain R R u : (a : α →₀ R) → β →₀ R) (single i 1) : β →₀ R) (single (u i) 1 : β →₀ R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
β : Type u_7
u : α → β
i : α
⊢ single (u i) 1 ∈ (↑(LinearMap.range (lmapDomain R R u)) : Set (β →₀ R))

Tactic:
exact ⟨Finsupp.single i 1, by simp⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) ⊤

Tactic:
eq_top_iff'.mpr fun x ↦ ?_

Premises used: Iff.mpr, Submodule.eq_top_iff'
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
refine :
  ∀ (x : α →₀ M),
    Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) x
⊢ Eq (α := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) ⊤

Tactic:
refine eq_top_iff'.mpr fun x ↦ ?_

Premises used: Iff.mpr, Submodule.eq_top_iff'
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) 0

Tactic:
Submodule.zero_mem ..

Premises used: Set.Mem, Submodule.zero_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) 0

Tactic:
exact Submodule.zero_mem ..

Premises used: Submodule.zero_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : α →₀ M
f_in : Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) f
g_in : Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) g
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) (f + g)

Tactic:
add_mem f_in g_in

Premises used: AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : α →₀ M
f_in : Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) f
g_in : Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) g
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) (f + g)

Tactic:
exact add_mem f_in g_in

Premises used: AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : α
b : M
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) (single a b)

Tactic:
mem_span_of_mem ⟨a, b, rfl⟩

Premises used: Submodule.mem_span_of_mem, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : α
b : M
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), single i x_1 = x}) (single a b)

Tactic:
exact mem_span_of_mem ⟨a, b, rfl⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : α →₀ M
zero :
  Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), Finsupp.single i x_1 = x}) 0
add :
  ∀ (f g : α →₀ M)
    (f_in :
      Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), Finsupp.single i x_1 = x})
        f)
    (g_in :
      Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), Finsupp.single i x_1 = x})
        g),
    Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), Finsupp.single i x_1 = x})
      (f + g)
single :
  ∀ (a : α) (b : M),
    Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), Finsupp.single i x_1 = x})
      (Finsupp.single a b)
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (span R {x : α →₀ M | ∃ (i : α) (x_1 : M), Finsupp.single i x_1 = x}) x

Tactic:
induction x using Finsupp.induction_linear with
  | zero => exact Submodule.zero_mem ..
  | add f g f_in g_in => exact add_mem f_in g_in
  | single a b => exact mem_span_of_mem ⟨a, b, rfl⟩

Premises used: Submodule.zero_mem, Submodule.zero, Submodule.add, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) m
⊢ ∀ (h : LE.le (α := Submodule R M) (R ∙ m) (⨆ (i : ι), p i)),
    ∃ (s : Finset ι), LE.le (α := Submodule R M) (R ∙ m) (⨆ i ∈ s, p i)

Tactic:
have :=
    CompleteLattice.IsCompactElement.exists_finset_of_le_iSup (Submodule R M)
      (Submodule.singleton_span_isCompactElement m) p
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) m
this :
  ∀ (h : LE.le (α := Submodule R M) (R ∙ m) (⨆ (i : ι), p i)),
    ∃ (s : Finset ι), LE.le (α := Submodule R M) (R ∙ m) (⨆ i ∈ s, p i)
⊢ ∀ (h : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) m),
    ∃ (s : Finset ι), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) m

Tactic:
simp only [Submodule.span_singleton_le_iff_mem] at this

Premises used: Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) m
this :
  ∀ (h : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) m),
    ∃ (s : Finset ι), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) m
⊢ ∃ (s : Finset ι), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) m

Tactic:
this hm
-- Module: Mathlib.LinearAlgebra.Finsupp.Span
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
p : ι → Submodule R M
m : M
hm : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) m
this :
  ∀ (h : Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) m),
    ∃ (s : Finset ι), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) m
⊢ ∃ (s : Finset ι), Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) m

Tactic:
exact this hm