awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
s : Set α
p q : α →₀ M
hp : Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} p
hq : Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} q
rw rw₁ : (↑p.support : Set α) ∪ (↑q.support : Set α) ⊆ (↑p.support : Set α) ∪ (↑q.support : Set α)
⊢ (↑(p.support ∪ q.support) : Set α) ⊆ (↑p.support : Set α) ∪ (↑q.support : Set α)

Tactic:
rw [Finset.coe_union]

Premises used: Finset.coe_union
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
s : Set α
p q : α →₀ M
hp : Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} p
hq : Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} q
refine : (↑(p.support ∪ q.support) : Set α) ⊆ (↑p.support : Set α) ∪ (↑q.support : Set α)
⊢ Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} (p + q)

Tactic:
classical
    refine Subset.trans (Subset.trans (Finset.coe_subset.2 support_add) ?_) (union_subset hp hq)
    rw [Finset.coe_union]

Premises used: Iff.mpr, Set.Subset.trans, Set.union_subset, Finsupp.support_add, Finset.coe_union, Finset.coe_subset
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
s : Set α
simp : ∀ (x : α), Ne.{u_2 + 1} (α := M) 0 0 → x ∈ s
⊢ Membership.mem (γ := Set (α →₀ M)) {p : α →₀ M | (↑p.support : Set α) ⊆ s} 0

Tactic:
simp only [subset_def, Finset.mem_coe, Set.mem_setOf_eq, mem_support_iff, zero_apply]

Premises used: Finsupp.mem_support_iff, Set.subset_def, Set.mem_setOf_eq, Finsupp.zero_apply, Finset.mem_coe
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
s : Set α
h : α
ha : Ne.{u_2 + 1} (α := M) 0 0
⊢ h ∈ s

Tactic:
(ha rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : AddCommMonoid P
inst_7 : Module R P
s : Set α
h : α
ha : Ne.{u_2 + 1} (α := M) 0 0
⊢ h ∈ s

Tactic:
exact (ha rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
p : α →₀ M
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (supported M R s) p ↔ (↑p.support : Set α) ⊆ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
p : α →₀ M
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (supported M R s) p ↔
    ∀ x ∉ s, Eq.{u_2 + 1} (α := M) ((p : (a : α) → M) x : M) (0 : M)

Tactic:
simp [mem_supported, Set.subset_def, not_imp_comm]

Premises used: Finsupp.mem_supported, Set.subset_def, not_imp_comm
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : α →₀ M
rw rw₁ : (↑p.support : Set α) ⊆ (↑p.support : Set α)
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (supported M R (↑p.support : Set α)) p

Tactic:
rw [Finsupp.mem_supported]

Premises used: Finsupp.mem_supported
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
a : α
b : M
h : a ∈ s
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (supported M R s) (single a b)

Tactic:
Set.Subset.trans support_single_subset (Finset.singleton_subset_set_iff.2 h)

Premises used: Iff.mpr, Set.Mem, Set.Subset.trans, Finset.singleton_subset_set_iff, setOf, Set.Subset, Finsupp.support_single_subset
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
⊢ Eq (α := Submodule R (α →₀ R)) (supported R R s) (span R ((fun (i : α) ↦ single i 1) '' s))

Tactic:
(span_eq_of_le _ ?_ (SetLike.le_def.2 fun l hl => ?_)).symm

Premises used: Iff.mpr, Submodule.span_eq_of_le, SetLike.le_def, Eq.symm
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
refine_1 : (fun (i : α) ↦ single i 1) '' s ⊆ (↑(supported R R s) : Set (α →₀ R))
refine_2 :
  ∀ (l : α →₀ R) (hl : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l),
    Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s)) l
⊢ Eq (α := Submodule R (α →₀ R)) (supported R R s) (span R ((fun (i : α) ↦ single i 1) '' s))

Tactic:
refine (span_eq_of_le _ ?_ (SetLike.le_def.2 fun l hl => ?_)).symm

Premises used: Iff.mpr, Submodule.span_eq_of_le, SetLike.le_def, Eq.symm
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
w : α
hp : w ∈ s
⊢ (fun (i : α) ↦ (single i 1 : α →₀ R)) w ∈ (↑(supported R R s) : Set (α →₀ R))

Tactic:
single_mem_supported R 1 hp

Premises used: Set.Mem, setOf, OfNat.ofNat, Finsupp.single_mem_supported
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
w : α
hp : w ∈ s
⊢ (fun (i : α) ↦ (single i 1 : α →₀ R)) w ∈ (↑(supported R R s) : Set (α →₀ R))

Tactic:
exact single_mem_supported R 1 hp

Premises used: OfNat.ofNat, Finsupp.single_mem_supported
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l
refine_2 : Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s)) (l.sum single)
⊢ Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s)) l

Tactic:
rw [← l.sum_single]

Premises used: Finsupp.sum_single
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l
⊢ Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s)) (l.sum single)

Tactic:
sum_mem fun i il => ?_

Premises used: Set.Mem, Finsupp.sum, sum_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l
refine_2 :
  ∀ (i : α) (il : i ∈ l.support),
    Membership.mem (α := α →₀ R) (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s))
      (single i ((l : (a : α) → R) i) : α →₀ R)
⊢ Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s)) (l.sum single)

Tactic:
refine sum_mem fun i il => ?_

Premises used: sum_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l
i : α
il : i ∈ l.support
⊢ single i ((l : (a : α) → R) i) = HSMul.hSMul (α := R) (β := α →₀ R) ((l : (a : α) → R) i : R) (single i 1)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l
i : α
il : i ∈ l.support
refine_2 :
  Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s))
    (HSMul.hSMul (α := R) (β := α →₀ R) ((l : (a : α) → R) i : R) (single i 1))
⊢ Membership.mem (α := α →₀ R) (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s))
    (single i ((l : (a : α) → R) i) : α →₀ R)

Tactic:
rw [show single i (l i) = l i • single i 1 by simp]
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l
i : α
il : i ∈ l.support
⊢ Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s))
    (HSMul.hSMul (α := R) (β := α →₀ R) ((l : (a : α) → R) i : R) (single i 1))

Tactic:
smul_mem _ (l i) (subset_span (mem_image_of_mem _ (hl il)))

Premises used: Set.Mem, Set.mem_image_of_mem, Submodule.subset_span, DFunLike.coe, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
s : Set α
l : α →₀ R
hl : Membership.mem (γ := Submodule R (α →₀ R)) (supported R R s) l
i : α
il : i ∈ l.support
⊢ Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (i : α) ↦ single i 1) '' s))
    (HSMul.hSMul (α := R) (β := α →₀ R) ((l : (a : α) → R) i : R) (single i 1))

Tactic:
exact smul_mem _ (l i) (subset_span (mem_image_of_mem _ (hl il)))

Premises used: Set.mem_image_of_mem, Submodule.subset_span, DFunLike.coe, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
inst_1 : Nontrivial R
a : α
s : Set α
⊢ Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (x : α) ↦ single x 1) '' s)) (single a 1) ↔ a ∈ s

Tactic:
⟨fun h => ?_, fun h => Submodule.subset_span <| Set.mem_image_of_mem _ h⟩

Premises used: Set.mem_image_of_mem, Iff.intro, Submodule.subset_span, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
inst_1 : Nontrivial R
a : α
s : Set α
refine :
  ∀ (h : Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (x : α) ↦ single x 1) '' s)) (single a 1)), a ∈ s
⊢ Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (x : α) ↦ single x 1) '' s)) (single a 1) ↔ a ∈ s

Tactic:
refine ⟨fun h => ?_, fun h => Submodule.subset_span <| Set.mem_image_of_mem _ h⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
inst_1 : Nontrivial R
a : α
s : Set α
h : Membership.mem (γ := Submodule R (α →₀ R)) (span R ((fun (x : α) ↦ single x 1) '' s)) (single a 1)
⊢ (↑{a} : Set α) ⊆ s

Tactic:
rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported,
    Finsupp.support_single _ (one_ne_zero' R)] at h

Premises used: Finsupp.support_single, Finsupp.mem_supported, one_ne_zero', Finsupp.supported_eq_span_single
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
R : Type u_5
inst : Semiring R
inst_1 : Nontrivial R
a : α
s : Set α
h : (↑{a} : Set α) ⊆ s
⊢ a ∈ s

Tactic:
simpa using h
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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)
⊢ LE.le (α := Submodule R (α →₀ M)) (span R s) (supported M R (⋃ x ∈ s, (↑x.support : Set α)))

Tactic:
span_le.mpr fun _ h ↦ subset_biUnion_of_mem h (u := (SetLike.coe ·.support))

Premises used: Iff.mpr, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
l : α →₀ M
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
⊢ (↑((restrictDom M R s : (a : α →₀ M) → ↥(supported M R s)) l) : α →₀ M) = filter (fun (x : α) ↦ x ∈ s) l

Tactic:
rfl

Premises used: Finsupp.filter, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
h :
  ∀ (l : ↥(supported M R s)) (a : α),
    Eq.{u_2 + 1} (α := M)
      (((↑((restrictDom M R s ∘ₗ Submodule.subtype (supported M R s) : (a : ↥(supported M R s)) → ↥(supported M R s))
                  l) :
              α →₀ M) :
            (a : α) → M)
          a :
        M)
      (((↑((LinearMap.id : (a : ↥(supported M R s)) → ↥(supported M R s)) l) : α →₀ M) : (a : α) → M) a : M)
⊢ Eq (α := ↥(supported M R s) →ₗ[R] ↥(supported M R s)) (restrictDom M R s ∘ₗ Submodule.subtype (supported M R s))
    LinearMap.id

Tactic:
ext l a
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
l : ↥(supported M R s)
a : α
pos :
  ∀ (h : a ∈ s),
    Eq.{u_2 + 1} (α := M)
      (((↑((restrictDom M R s ∘ₗ Submodule.subtype (supported M R s) : (a : ↥(supported M R s)) → ↥(supported M R s))
                  l) :
              α →₀ M) :
            (a : α) → M)
          a :
        M)
      (((↑((LinearMap.id : (a : ↥(supported M R s)) → ↥(supported M R s)) l) : α →₀ M) : (a : α) → M) a : M)
neg :
  ∀ (h : a ∉ s),
    Eq.{u_2 + 1} (α := M)
      (((↑((restrictDom M R s ∘ₗ Submodule.subtype (supported M R s) : (a : ↥(supported M R s)) → ↥(supported M R s))
                  l) :
              α →₀ M) :
            (a : α) → M)
          a :
        M)
      (((↑((LinearMap.id : (a : ↥(supported M R s)) → ↥(supported M R s)) l) : α →₀ M) : (a : α) → M) a : M)
⊢ Eq.{u_2 + 1} (α := M)
    (((↑((restrictDom M R s ∘ₗ Submodule.subtype (supported M R s) : (a : ↥(supported M R s)) → ↥(supported M R s)) l) :
            α →₀ M) :
          (a : α) → M)
        a :
      M)
    (((↑((LinearMap.id : (a : ↥(supported M R s)) → ↥(supported M R s)) l) : α →₀ M) : (a : α) → M) a : M)

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
l : ↥(supported M R s)
a : α
h : a ∈ s
⊢ Eq.{u_2 + 1} (α := M)
    (((↑((restrictDom M R s ∘ₗ Submodule.subtype (supported M R s) : (a : ↥(supported M R s)) → ↥(supported M R s)) l) :
            α →₀ M) :
          (a : α) → M)
        a :
      M)
    (((↑((LinearMap.id : (a : ↥(supported M R s)) → ↥(supported M R s)) l) : α →₀ M) : (a : α) → M) a : M)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
l : ↥(supported M R s)
a : α
h : a ∉ s
⊢ Eq.{u_2 + 1} (α := M)
    (((↑((restrictDom M R s ∘ₗ Submodule.subtype (supported M R s) : (a : ↥(supported M R s)) → ↥(supported M R s)) l) :
            α →₀ M) :
          (a : α) → M)
        a :
      M)
    (((↑((LinearMap.id : (a : ↥(supported M R s)) → ↥(supported M R s)) l) : α →₀ M) : (a : α) → M) a : M)

Tactic:
simpa [h] using ((mem_supported' R l.1).1 l.2 a h).symm

Premises used: Iff.mp, Eq.symm, Subtype.val, Subtype.property, Finsupp.mem_supported'
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
inst_3 : DecidablePred fun (x : α) ↦ x ∈ s
⊢ Eq (α := Submodule R ↥(supported M R s)) (LinearMap.range (restrictDom M R s)) ⊤

Tactic:
range_eq_top.2 <|
    Function.RightInverse.surjective <| LinearMap.congr_fun (restrictDom_comp_subtype s)

Premises used: Iff.mpr, LinearMap.range_eq_top, Finsupp.restrictDom_comp_subtype, LinearMap.congr_fun, Function.RightInverse.surjective
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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 α
st : s ⊆ t
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R s) (supported M R t)

Tactic:
fun _ h =>
  Set.Subset.trans h st

Premises used: Set.Mem, Set.Subset.trans, setOf, Set.Subset
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
l : α →₀ M
h : Membership.mem (γ := Submodule R (α →₀ M)) (supported M R ∅) l
h₁ : ∀ (a : α), Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
⊢ l = 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
l : α →₀ M
h : Membership.mem (γ := Submodule R (α →₀ M)) (supported M R ∅) l
a : α
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)

Tactic:
simp_all [mem_supported']

Premises used: Finsupp.mem_supported'
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
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)) (supported M R univ) ⊤

Tactic:
eq_top_iff.2 fun _ _ => Set.subset_univ _

Premises used: Iff.mpr, eq_top_iff, Set.subset_univ, Finsupp.support, SetLike.coe
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
δ : Type u_7
s : δ → Set α
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))

Tactic:
le_antisymm ?_ (iSup_le fun i => supported_mono <| Set.subset_iUnion _ _)

Premises used: Set.subset_iUnion, le_antisymm, Finsupp.supported_mono, iSup_le
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
δ : Type u_7
s : δ → Set α
refine : LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
⊢ Eq (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))

Tactic:
refine le_antisymm ?_ (iSup_le fun i => supported_mono <| Set.subset_iUnion _ _)

Premises used: Set.subset_iUnion, le_antisymm, Finsupp.supported_mono, iSup_le
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
δ : Type u_7
s : δ → Set α
haveI :
  ∀ (this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x),
    LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))

Tactic:
haveI := Classical.decPred fun x => x ∈ ⋃ i, s i
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
δ : Type u_7
s : δ → Set α
this_1 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
this :
  LE.le (α := Submodule R (α →₀ M))
    (LinearMap.range (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i)))
    (⨆ (i : δ), supported M R (s i))
rwa :
  ∀
    (this :
      LE.le (α := Submodule R (α →₀ M))
        (map (M := ↥(supported M R (⋃ (i : δ), s i))) (Submodule.subtype (supported M R (⋃ (i : δ), s i)))
          (LinearMap.range (restrictDom M R (⋃ (i : δ), s i))))
        (⨆ (i : δ), supported M R (s i))),
    LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
rwa₁ :
  ∀
    (this :
      LE.le (α := Submodule R (α →₀ M))
        (map (M := ↥(supported M R (⋃ (i : δ), s i))) (Submodule.subtype (supported M R (⋃ (i : δ), s i))) ⊤)
        (⨆ (i : δ), supported M R (s i))),
    LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
rwa₂ :
  ∀
    (this :
      LE.le (α := Submodule R (α →₀ M))
        (LinearMap.range (M := ↥(supported M R (⋃ (i : δ), s i))) (Submodule.subtype (supported M R (⋃ (i : δ), s i))))
        (⨆ (i : δ), supported M R (s i))),
    LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (this : LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))),
    LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))

Tactic:
rwa [LinearMap.range_comp, range_restrictDom, Submodule.map_top, range_subtype] at this

Premises used: Submodule.map_top, LinearMap.range_comp, Submodule.range_subtype, Finsupp.range_restrictDom
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
M₁ :
  LE.le (α := Submodule R (α →₀ M))
    (LinearMap.range (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i)))
    (⨆ (i : δ), supported M R (s i))
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (⋃ (i : δ), s i)) (⨆ (i : δ), supported M R (s i))

Tactic:
suffices
    LinearMap.range ((Submodule.subtype _).comp (restrictDom M R (⋃ i, s i))) ≤
      ⨆ i, supported M R (s i) by
    rwa [LinearMap.range_comp, range_restrictDom, Submodule.map_top, range_subtype] at this
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
rw :
  LE.le (α := Submodule R (α →₀ M)) ⊤
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
⊢ LE.le (α := Submodule R (α →₀ M))
    (LinearMap.range (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i)))
    (⨆ (i : δ), supported M R (s i))

Tactic:
rw [range_le_iff_comap, eq_top_iff]

Premises used: eq_top_iff, LinearMap.range_le_iff_comap
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
⊢ Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.LinearAlgebra.Finsupp.Supported
Goal:
α : Type u_1
M : Type u_2
R : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
δ : Type u_7
s : δ → Set α
this : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : δ), s i) x
⊢ Membership.mem (γ := Submodule R (α →₀ M))
    (comap (Submodule.subtype (supported M R (⋃ (i : δ), s i)) ∘ₗ restrictDom M R (⋃ (i : δ), s i))
      (⨆ (i : δ), supported M R (s i)))
    0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem