awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
i : (↑s : Type u_1)
a : M
⊢ Eq (α := α →₀ M)
    (↑((LinearEquiv.symm (supportedEquivFinsupp s) : (a : (↑s : Type u_1) →₀ M) → ↥(supported M R s)) (single i a)) :
      α →₀ M)
    (single (↑i : α) a)

Tactic:
simp
-- 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 α
i : (↑s : Type u_1)
a : M
⊢ Eq (α := α →₀ M)
    (↑((LinearEquiv.symm (supportedEquivFinsupp s) : (a : (↑s : Type u_1) →₀ M) → ↥(supported M R s)) (single i a)) :
      α →₀ M)
    (single (↑i : α) a)

Tactic:
classical simp
-- 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
f : α → α'
s : _root_.Set α'
l : α →₀ M
Set :
  ∀ (hl : (↑l.support : _root_.Set α) ⊆ f ⁻¹' s),
    Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (supported M R (f ⁻¹' s)) l →
    Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l

Tactic:
(hl : (l.support : Set α) ⊆ f ⁻¹' 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
α' : Type u_7
f : α → α'
s : Set α'
l : α →₀ M
hl : (↑l.support : Set α) ⊆ f ⁻¹' s
change : (↑(mapDomain f l).support : Set α') ⊆ s
⊢ Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l

Tactic:
change ↑(mapDomain f l).support ⊆ s

Premises used: Finsupp.mapDomain, Finsupp.support
-- 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
f : α → α'
s : Set α'
l : α →₀ M
hl : (↑l.support : Set α) ⊆ f ⁻¹' s
⊢ (↑(Finset.image f l.support) : Set α') ⊆ s

Tactic:
rw [← Set.image_subset_iff, ← Finset.coe_image] at hl

Premises used: Finset.coe_image, Set.image_subset_iff
-- 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
f : α → α'
s : Set α'
l : α →₀ M
hl : (↑(Finset.image f l.support) : Set α') ⊆ s
⊢ (↑(mapDomain f l).support : Set α') ⊆ s

Tactic:
Set.Subset.trans mapDomain_support hl

Premises used: Finsupp.mapDomain_support, Set.Subset.trans
-- 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
f : α → α'
s : Set α'
l : α →₀ M
hl : (↑(Finset.image f l.support) : Set α') ⊆ s
⊢ (↑(mapDomain f l).support : Set α') ⊆ s

Tactic:
exact Set.Subset.trans mapDomain_support hl

Premises used: Finsupp.mapDomain_support, Set.Subset.trans
-- 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
f : α → α'
s : Set α'
intro :
  ∀ ⦃l : α →₀ M⦄,
    Membership.mem (γ := Submodule R (α →₀ M)) (supported M R (f ⁻¹' s)) l →
      Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l
intro₁ :
  ∀ ⦃l : α →₀ M⦄ (hl : (↑l.support : Set α) ⊆ f ⁻¹' s),
    Membership.mem (γ := Submodule R (α →₀ M)) (comap (lmapDomain M R f) (supported M R s)) l
intro₂ : ∀ ⦃l : α →₀ M⦄ (hl : (↑l.support : Set α) ⊆ f ⁻¹' s), (↑(mapDomain f l).support : Set α') ⊆ s
intro₃ : ∀ ⦃l : α →₀ M⦄ (hl : (↑(Finset.image f l.support) : Set α') ⊆ s), (↑(mapDomain f l).support : Set α') ⊆ s
⊢ LE.le (α := Submodule R (α →₀ M)) (supported M R (f ⁻¹' s)) (comap (lmapDomain M R f) (supported M R s))

Tactic:
classical
  intro l (hl : (l.support : Set α) ⊆ f ⁻¹' s)
  change ↑(mapDomain f l).support ⊆ s
  rw [← Set.image_subset_iff, ← Finset.coe_image] at hl
  exact Set.Subset.trans mapDomain_support hl

Premises used: Finset.coe_image, Set.image_subset_iff
-- 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
f : α → α'
s : Set α
inl : IsEmpty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
inr : Nonempty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
⊢ Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- 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
f : α → α'
s : Set α
h : IsEmpty α
⊢ Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))

Tactic:
simp [s.eq_empty_of_isEmpty]

Premises used: Set.eq_empty_of_isEmpty
-- 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
f : α → α'
s : Set α
h : Nonempty α
⊢ Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))

Tactic:
le_antisymm
      (map_le_iff_le_comap.2 <|
        le_trans (supported_mono <| Set.subset_preimage_image _ _)
          (supported_comap_lmapDomain M R _ _))
      ?_

Premises used: Iff.mpr, Finsupp.supported_comap_lmapDomain, le_antisymm, Finsupp.supported_mono, Submodule.map_le_iff_le_comap, Set.subset_preimage_image, le_trans
-- 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
f : α → α'
s : Set α
h : Nonempty α
inr : LE.le (α := Submodule R (α' →₀ M)) (supported M R (f '' s)) (map (lmapDomain M R f) (supported M R s))
⊢ Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))

Tactic:
refine
    le_antisymm
      (map_le_iff_le_comap.2 <|
        le_trans (supported_mono <| Set.subset_preimage_image _ _)
          (supported_comap_lmapDomain M R _ _))
      ?_

Premises used: Iff.mpr, Finsupp.supported_comap_lmapDomain, le_antisymm, Finsupp.supported_mono, Submodule.map_le_iff_le_comap, Set.subset_preimage_image, le_trans
-- 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
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
⊢ Membership.mem (γ := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) l

Tactic:
⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩

Premises used: Function.invFunOn, Set.Mem, setOf, Finsupp.lmapDomain, And.intro, Exists.intro, Set.image, DFunLike.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
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
inr :
  ∀ (x : α)
    (hx :
      x ∈
        (↑(support.{u_1, u_2} (M := M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l)) : Set α)),
    x ∈ s
inr₁ :
  (lmapDomain M R f : (a : α →₀ M) → α' →₀ M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l) = l
⊢ Membership.mem (γ := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) l

Tactic:
refine ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩
-- 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
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
x : α
hx : x ∈ (↑(support.{u_1, u_2} (M := M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l)) : Set α)
inr :
  ∀ (c : α') (hc : c ∈ l.support)
    (hx :
      Function.invFunOn f s c ∈
        (↑(support.{u_1, u_2} (M := M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l)) : Set α)),
    Function.invFunOn f s c ∈ s
⊢ x ∈ s

Tactic:
rcases Finset.mem_image.1 (mapDomain_support hx) with ⟨c, hc, rfl⟩

Premises used: Finset.mem_image, Finsupp.mapDomain_support, Iff.mp, 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
α' : Type u_7
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
c : α'
hc : c ∈ l.support
hx :
  Function.invFunOn f s c ∈
    (↑(support.{u_1, u_2} (M := M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l)) : Set α)
⊢ ∃ a ∈ s, f a = c

Tactic:
simpa using hl hc
-- 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
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
c : α'
hc : c ∈ l.support
hx :
  Function.invFunOn f s c ∈
    (↑(support.{u_1, u_2} (M := M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l)) : Set α)
⊢ Function.invFunOn f s c ∈ s

Tactic:
exact Function.invFunOn_mem (by simpa using hl hc)

Premises used: Function.invFunOn_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
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
inr : (lmapDomain M R (f ∘ Function.invFunOn f s) : (a : α' →₀ M) → α' →₀ M) l = l
⊢ (lmapDomain M R f : (a : α →₀ M) → α' →₀ M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l) = l

Tactic:
rw [← LinearMap.comp_apply, ← lmapDomain_comp]

Premises used: Finsupp.lmapDomain_comp, LinearMap.comp_apply
-- 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
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
⊢ (lmapDomain M R (f ∘ Function.invFunOn f s) : (a : α' →₀ M) → α' →₀ M) l = l

Tactic:
(mapDomain_congr fun c hc => ?_).trans mapDomain_id

Premises used: Multiset.sum, Multiset.foldr, Finsupp.mapDomain, Finsupp.sum, Finsupp.mapDomain_id, Finsupp.mapDomain_congr, Finset.sum, Eq.trans
-- 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
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
inr : ∀ (c : α') (hc : c ∈ l.support), (f ∘ Function.invFunOn f s) c = _root_.id c
⊢ (lmapDomain M R (f ∘ Function.invFunOn f s) : (a : α' →₀ M) → α' →₀ M) l = l

Tactic:
refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id

Premises used: Finsupp.mapDomain_id, Finsupp.mapDomain_congr, Eq.trans
-- 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
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
c : α'
hc : c ∈ l.support
⊢ ∃ a ∈ s, f a = c

Tactic:
simpa using hl hc
-- 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
f : α → α'
s : Set α
h : Nonempty α
l : α' →₀ M
hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l
c : α'
hc : c ∈ l.support
⊢ (f ∘ Function.invFunOn f s) c = _root_.id c

Tactic:
exact Function.invFunOn_eq (by simpa using hl hc)

Premises used: Function.invFunOn_eq
-- 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
f : α → α'
s : Set α
inl : IsEmpty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
inr inr₁ :
  Nonempty α → Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))
inr₂ :
  Nonempty α → LE.le (α := Submodule R (α' →₀ M)) (supported M R (f '' s)) (map (lmapDomain M R f) (supported M R s))
inr₃ :
  Nonempty α →
    ∀ ⦃l : α' →₀ M⦄ (hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l),
      Membership.mem (γ := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) l
inr₄ :
  ∀ (h : Nonempty α) ⦃l : α' →₀ M⦄ (hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l) (x : α)
    (hx :
      x ∈
        (↑(support.{u_1, u_2} (M := M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l)) : Set α)),
    x ∈ s
inr₅ inr₆ :
  ∀ (h : Nonempty α) ⦃l : α' →₀ M⦄ (hl : Membership.mem (γ := Submodule R (α' →₀ M)) (supported M R (f '' s)) l),
    (lmapDomain M R f : (a : α →₀ M) → α' →₀ M) ((lmapDomain M R (Function.invFunOn f s) : (a : α' →₀ M) → α →₀ M) l) =
      l
⊢ Eq (α := Submodule R (α' →₀ M)) (map (lmapDomain M R f) (supported M R s)) (supported M R (f '' s))

Tactic:
classical
  cases isEmpty_or_nonempty α
  · simp [s.eq_empty_of_isEmpty]
  refine
    le_antisymm
      (map_le_iff_le_comap.2 <|
        le_trans (supported_mono <| Set.subset_preimage_image _ _)
          (supported_comap_lmapDomain M R _ _))
      ?_
  intro l hl
  refine ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => ?_, ?_⟩
  · rcases Finset.mem_image.1 (mapDomain_support hx) with ⟨c, hc, rfl⟩
    exact Function.invFunOn_mem (by simpa using hl hc)
  · rw [← LinearMap.comp_apply, ← lmapDomain_comp]
    refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id
    exact Function.invFunOn_eq (by simpa using hl hc)

Premises used: Iff.mpr, Finsupp.lmapDomain_comp, Function.invFunOn_mem, Finsupp.supported_comap_lmapDomain, LinearMap.comp_apply, isEmpty_or_nonempty, Finsupp.mapDomain_id, Finsupp.mapDomain_congr, Function.invFunOn_eq, le_antisymm, Finsupp.supported_mono, Submodule.map_le_iff_le_comap, Set.subset_preimage_image, rfl, Eq.trans, le_trans
-- 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
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
rw : LE.le (α := Submodule R (α →₀ M)) (supported M R s ⊓ ker (lmapDomain M R f)) ⊥
⊢ Disjoint (α := Submodule R (α →₀ M)) (supported M R s) (ker (lmapDomain M R f))

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_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
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : l ∈ (↑(ker (lmapDomain M R f)) : Set (α →₀ M))
⊢ Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0

Tactic:
rw [SetLike.mem_coe, mem_ker, lmapDomain_apply, mapDomain] at h₂

Premises used: Finsupp.mapDomain, LinearMap.mem_ker, SetLike.mem_coe, Finsupp.lmapDomain_apply
-- 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
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
h : ∀ (x : α), Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
⊢ l = 0

Tactic:
ext x
-- 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
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
h :
  ∀ (this : DecidablePred fun (x : α) ↦ x ∈ s),
    Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)

Tactic:
haveI := Classical.decPred fun x => x ∈ 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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this : DecidablePred fun (x : α) ↦ x ∈ s
pos : ∀ (xs : x ∈ s), Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
neg : ∀ (xs : x ∉ s), Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)

Tactic:
by_cases xs : x ∈ 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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
rw : Eq.{u_2 + 1} (α := M) ((0 : (a : α') → M) (f x) : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := M) ((l.sum fun (a : α) ↦ single (f a) : (a : α') → M) (f x) : M) (0 : M)

Tactic:
rw [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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
⊢ Eq.{u_2 + 1} (α := M) ((0 : (a : α') → M) (f x) : M) (0 : M)

Tactic:
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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
⊢ Eq.{u_2 + 1} (α := M) ((l.sum fun (a : α) ↦ single (f a) : (a : α') → M) (f x) : M) (0 : M)

Tactic:
have : Finsupp.sum l (fun a => Finsupp.single (f a)) (f x) = 0 := by
      rw [h₂]
      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
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
this : Eq.{u_2 + 1} (α := M) ((l.sum fun (a : α) ↦ single (f a) : (a : α') → M) (f x) : M) (0 : M)
pos :
  ∀ (this : Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) (0 : M)),
    Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)
pos₁ :
  ∀ (this : Eq (α := M) (l.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : α') → M) (f x)) 0) (b : α),
    Ne.{u_2 + 1} (α := M) ((l : (a : α) → M) b : M) (0 : M) →
      b ≠ x → Eq.{u_2 + 1} (α := M) (((single (f b) ((l : (a : α) → M) b) : α' →₀ M) : (a : α') → M) (f x) : M) (0 : M)
pos₂ :
  ∀ (this : Eq (α := M) (l.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : α') → M) (f x)) 0),
    Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) (0 : M) →
      Eq.{u_2 + 1} (α := M) ((single (f x) 0 : (a : α') → M) (f x) : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)

Tactic:
rw [Finsupp.sum_apply, Finsupp.sum_eq_single x, single_eq_same] at this

Premises used: Finsupp.single_eq_same, Finsupp.sum_eq_single, Finsupp.sum_apply
-- 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
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
this : Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)

Tactic:
simpa
-- 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
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
this : Eq (α := M) (l.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : α') → M) (f x)) 0
y : α
hy : Ne.{u_2 + 1} (α := M) ((l : (a : α) → M) y : M) (0 : M)
xy : y ≠ x
⊢ ∀ (x : α), Ne.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) (0 : M) → x ∈ s

Tactic:
simp only [SetLike.mem_coe, mem_supported, subset_def, mem_support_iff] at h₁

Premises used: Finsupp.mem_support_iff, Finsupp.mem_supported, Set.subset_def, SetLike.mem_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
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
this : Eq (α := M) (l.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : α') → M) (f x)) 0
y : α
hy : Ne.{u_2 + 1} (α := M) ((l : (a : α) → M) y : M) (0 : M)
xy : y ≠ x
h₁ : ∀ (x : α), Ne.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) (0 : M) → x ∈ s
⊢ Eq.{u_2 + 1} (α := M) (((single (f y) ((l : (a : α) → M) y) : α' →₀ M) : (a : α') → M) (f x) : M) (0 : M)

Tactic:
simp [mt (H _ (h₁ _ hy) _ xs) xy]

Premises used: mt
-- 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
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this_1 : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∈ s
this : Eq (α := M) (l.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : α') → M) (f x)) 0
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) (0 : M) →
    Eq.{u_2 + 1} (α := M) ((single (f x) 0 : (a : α') → M) (f x) : M) (0 : M)

Tactic:
simp +contextual
-- 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
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ (↑(supported M R s) : Set (α →₀ M))
h₂ : Eq (α := α' →₀ M) (l.sum fun (a : α) ↦ single (f a)) 0
x : α
this : DecidablePred fun (x : α) ↦ x ∈ s
xs : x ∉ s
neg : ∀ (h : ¬Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)), False
⊢ Eq.{u_2 + 1} (α := M) ((l : (a : α) → M) x : M) ((0 : (a : α) → M) x : M)

Tactic:
by_contra h