awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
i : ι
j : α i
h :
  ((f.sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j =
    (f : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j)
h₁ h₂ :
  Eq (α :=
    δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).fst (β := fun (x : ι) ↦ α x))
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).snd (β := fun (x : ι) ↦ α x)))
    ((f : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j))
    ((f : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j))
⊢ Eq (α :=
    δ ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).fst (β := fun (x : ι) ↦ α x))
      ((Sigma.mk (β := fun (x : ι) ↦ α x) i j).snd (β := fun (x : ι) ↦ α x)))
    ((f.sigmaCurry (α := α) (δ := δ).sigmaUncurry (α := α) (δ := δ) : (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j))
    ((f : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j))

Tactic:
rw [sigmaUncurry_apply, sigmaCurry_apply]

Premises used: DFinsupp.sigmaUncurry_apply, DFinsupp.sigmaCurry_apply
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
h :
  ∀ (i : ι) (j : α i),
    ((f.sigmaUncurry (α := α) (δ := δ).sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i :
          (a : α i) → δ i a)
        j =
      ((f : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j
⊢ f.sigmaUncurry (α := α) (δ := δ).sigmaCurry (α := α) (δ := δ) = f

Tactic:
ext i j
-- Module: Mathlib.Data.DFinsupp.Sigma
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
i : ι
j : α i
h :
  (f.sigmaUncurry (α := α) (δ := δ) : (a : (x : ι) × α x) → δ a.fst a.snd) (Sigma.mk (β := fun (x : ι) ↦ α x) i j) =
    ((f : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j
h₁ h₂ :
  ((f : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j =
    ((f : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j
⊢ ((f.sigmaUncurry (α := α) (δ := δ).sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i :
        (a : α i) → δ i a)
      j =
    ((f : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j

Tactic:
rw [sigmaCurry_apply, sigmaUncurry_apply]

Premises used: DFinsupp.sigmaUncurry_apply, DFinsupp.sigmaCurry_apply
-- Module: Mathlib.Data.DFinsupp.Small
Goal:
ι : Type u
π : ι → Type v
inst : (i : ι) → Zero (π i)
inst_1 : Small.{w, u} ι
inst_2 : ∀ (i : ι), Small.{w, v} (π i)
f f' : DFinsupp π
eq :
  Eq (α := (j : ι) → π j) ((fun (x : DFinsupp π) (j : ι) ↦ (x : (a : ι) → π a) j) f)
    ((fun (x : DFinsupp π) (j : ι) ↦ (x : (a : ι) → π a) j) f')
h : ∀ (j : ι), (f : (a : ι) → π a) j = (f' : (a : ι) → π a) j
⊢ f = f'

Tactic:
ext j
-- Module: Mathlib.Data.DFinsupp.Small
Goal:
ι : Type u
π : ι → Type v
inst : (i : ι) → Zero (π i)
inst_1 : Small.{w, u} ι
inst_2 : ∀ (i : ι), Small.{w, v} (π i)
f f' : DFinsupp π
eq :
  Eq (α := (j : ι) → π j) ((fun (x : DFinsupp π) (j : ι) ↦ (x : (a : ι) → π a) j) f)
    ((fun (x : DFinsupp π) (j : ι) ↦ (x : (a : ι) → π a) j) f')
j : ι
⊢ (f : (a : ι) → π a) j = (f' : (a : ι) → π a) j

Tactic:
congr_fun eq j

Premises used: congr_fun
-- Module: Mathlib.Data.DFinsupp.Small
Goal:
ι : Type u
π : ι → Type v
inst : (i : ι) → Zero (π i)
inst_1 : Small.{w, u} ι
inst_2 : ∀ (i : ι), Small.{w, v} (π i)
f f' : DFinsupp π
eq :
  Eq (α := (j : ι) → π j) ((fun (x : DFinsupp π) (j : ι) ↦ (x : (a : ι) → π a) j) f)
    ((fun (x : DFinsupp π) (j : ι) ↦ (x : (a : ι) → π a) j) f')
j : ι
⊢ (f : (a : ι) → π a) j = (f' : (a : ι) → π a) j

Tactic:
exact congr_fun eq j

Premises used: congr_fun
-- Module: Mathlib.Data.DFinsupp.Small
Goal:
ι : Type u
π : ι → Type v
inst : (i : ι) → Zero (π i)
σ : Type u_1
R : Type u_2
inst_1 : Zero R
inst_2 : Small.{u, u_2} R
inst_3 : Small.{u, u_1} σ
⊢ Small.{u, max u_2 u_1} (σ →₀ R)

Tactic:
small_map finsuppEquivDFinsupp

Premises used: finsuppEquivDFinsupp, small_map
-- Module: Mathlib.Data.DFinsupp.Small
Goal:
ι : Type u
π : ι → Type v
inst : (i : ι) → Zero (π i)
σ : Type u_1
R : Type u_2
inst_1 : Zero R
inst_2 : Small.{u, u_2} R
inst_3 : Small.{u, u_1} σ
⊢ Small.{u, max u_2 u_1} (σ →₀ R)

Tactic:
exact small_map finsuppEquivDFinsupp

Premises used: finsuppEquivDFinsupp, small_map
-- Module: Mathlib.Data.DFinsupp.Small
Goal:
ι : Type u
π : ι → Type v
inst : (i : ι) → Zero (π i)
σ : Type u_1
R : Type u_2
inst_1 : Zero R
inst_2 : Small.{u, u_2} R
inst_3 : Small.{u, u_1} σ
⊢ Small.{u, max u_2 u_1} (σ →₀ R)

Tactic:
classical
  exact small_map finsuppEquivDFinsupp

Premises used: finsuppEquivDFinsupp, small_map
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
S : Type u_1
inst_4 : SetLike S γ
inst_5 : SubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
h : ∀ (c : ι), (f : (a : ι) → β a) c ≠ 0 → g c ((f : (a : ι) → β a) c) ∈ s
⊢ f.prod (β := β) g ∈ s

Tactic:
prod_mem fun _ hi => h _ <| mem_support_iff.1 hi

Premises used: Set.Mem, DFinsupp.prod, DFinsupp.mem_support_iff, Iff.mp, prod_mem
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
S : Type u_1
inst_3 : SetLike S γ
inst_4 : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → AddMonoidHom.{v, w} (β i) γ
h :
  ∀ (c : ι),
    (f : (a : ι) → β a) c ≠ 0 → Membership.mem.{w, u_1} (α := γ) s ((g c : (a : β c) → γ) ((f : (a : ι) → β a) c) : γ)
rw : (f.sum (β := β) fun (x : ι) ↦ (⇑(g x) : (a : β x) → γ)) ∈ s
⊢ Membership.mem.{w, u_1} (α := γ) s ((sumAddHom (β := β) g : (a : Π₀ (i : ι), β i) → γ) f : γ)

Tactic:
rw [DFinsupp.sumAddHom_apply]

Premises used: DFinsupp.sumAddHom_apply
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
S : Type u_1
inst_3 : SetLike S γ
inst_4 : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → AddMonoidHom.{v, w} (β i) γ
h :
  ∀ (c : ι),
    (f : (a : ι) → β a) c ≠ 0 → Membership.mem.{w, u_1} (α := γ) s ((g c : (a : β c) → γ) ((f : (a : ι) → β a) c) : γ)
⊢ (f.sum (β := β) fun (x : ι) ↦ (⇑(g x) : (a : β x) → γ)) ∈ s

Tactic:
dfinsuppSum_mem s f (g ·) h

Premises used: dfinsuppSum_mem, DFunLike.coe
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
S : Type u_1
inst_3 : SetLike S γ
inst_4 : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → AddMonoidHom.{v, w} (β i) γ
h :
  ∀ (c : ι),
    (f : (a : ι) → β a) c ≠ 0 → Membership.mem.{w, u_1} (α := γ) s ((g c : (a : β c) → γ) ((f : (a : ι) → β a) c) : γ)
⊢ (f.sum (β := β) fun (x : ι) ↦ (⇑(g x) : (a : β x) → γ)) ∈ s

Tactic:
exact dfinsuppSum_mem s f (g ·) h

Premises used: dfinsuppSum_mem, DFunLike.coe
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
inst_2 : AddCommMonoid γ
S : Type u_1
inst_3 : SetLike S γ
inst_4 : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → AddMonoidHom.{v, w} (β i) γ
h :
  ∀ (c : ι),
    (f : (a : ι) → β a) c ≠ 0 → Membership.mem.{w, u_1} (α := γ) s ((g c : (a : β c) → γ) ((f : (a : ι) → β a) c) : γ)
rw rw₁ rw₂ : (f.sum (β := β) fun (x : ι) ↦ (⇑(g x) : (a : β x) → γ)) ∈ s
⊢ Membership.mem.{w, u_1} (α := γ) s ((sumAddHom (β := β) g : (a : Π₀ (i : ι), β i) → γ) f : γ)

Tactic:
classical
    rw [DFinsupp.sumAddHom_apply]
    exact dfinsuppSum_mem s f (g ·) h

Premises used: DFinsupp.sumAddHom_apply
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
a :
  iSup S ≤
    AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
a₁ :
  AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype) ≤
    iSup S
⊢ iSup S =
    AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
apply :
  ∀ (i : ι),
    S i ≤
      AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
        (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
⊢ iSup S ≤
    AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)

Tactic:
apply iSup_le _

Premises used: iSup_le
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
y : γ
hy : y ∈ S i
⊢ Membership.mem (γ := AddSubmonoid γ)
    (AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype))
    y

Tactic:
⟨DFinsupp.single i ⟨y, hy⟩, DFinsupp.sumAddHom_single _ _ _⟩

Premises used: DFinsupp.sumAddHom_single, Set.Mem, DFinsupp.single, setOf, Subtype.mk, Exists.intro, Set.range
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
y : γ
hy : y ∈ S i
⊢ Membership.mem (γ := AddSubmonoid γ)
    (AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype))
    y

Tactic:
exact ⟨DFinsupp.single i ⟨y, hy⟩, DFinsupp.sumAddHom_single _ _ _⟩
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
⊢ Membership.mem (α := γ) (iSup S)
    ((sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype : (a : Π₀ (i : ι), ↥(S i)) → γ) v : γ)

Tactic:
dfinsuppSumAddHom_mem _ v _ fun i _ => (le_iSup S i : S i ≤ _) (v i).prop

Premises used: Set.Mem, le_iSup, Subtype.prop, dfinsuppSumAddHom_mem, DFunLike.coe
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
⊢ Membership.mem (α := γ) (iSup S)
    ((sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype : (a : Π₀ (i : ι), ↥(S i)) → γ) v : γ)

Tactic:
exact dfinsuppSumAddHom_mem _ v _ fun i _ => (le_iSup S i : S i ≤ _) (v i).prop

Premises used: le_iSup, dfinsuppSumAddHom_mem
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
a :
  LE.le (α := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
        (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p)))
a₁ :
  LE.le (α := AddSubmonoid γ)
    (AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
        (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p)))
    (⨆ (i : ι), ⨆ (_ : p i), S i)
⊢ Eq (α := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
        (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p)))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ LE.le (α := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
        (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p)))

Tactic:
iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩

Premises used: iSup₂_le, Set.Mem, DFinsupp.single, Subtype.mk, Exists.intro
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
a :
  ∀ (i : ι) (hi : p i) (y : γ) (hy : y ∈ S i),
    (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
            (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p) :
          (a : Π₀ (i : ι), ↥(S i)) → γ)
        (single (β := fun (i : ι) ↦ ↥(S i)) i (Subtype.mk (p := fun (x : γ) ↦ x ∈ S i) y hy)) =
      y
⊢ LE.le (α := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (AddMonoidHom.mrange (F := (Π₀ (i : ι), ↥(S i)) →+ γ)
      (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
        (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p)))

Tactic:
refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩

Premises used: iSup₂_le
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
a :
  (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype : (a : Π₀ (i : ι), ↥(S i)) → γ)
      (single (β := fun (i : ι) ↦ ↥(S i)) i (Subtype.mk (p := fun (x : γ) ↦ x ∈ S i) y hy)) =
    y
⊢ (AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
          (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p) :
        (a : Π₀ (i : ι), ↥(S i)) → γ)
      (single (β := fun (i : ι) ↦ ↥(S i)) i (Subtype.mk (p := fun (x : γ) ↦ x ∈ S i) y hy)) =
    y

Tactic:
rw [AddMonoidHom.comp_apply, filterAddMonoidHom_apply, filter_single_pos _ _ hi]

Premises used: AddMonoidHom.comp_apply, DFinsupp.filter_single_pos, DFinsupp.filterAddMonoidHom_apply
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype : (a : Π₀ (i : ι), ↥(S i)) → γ)
      (single (β := fun (i : ι) ↦ ↥(S i)) i (Subtype.mk (p := fun (x : γ) ↦ x ∈ S i) y hy)) =
    y

Tactic:
sumAddHom_single _ _ _

Premises used: DFinsupp.sumAddHom_single
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype : (a : Π₀ (i : ι), ↥(S i)) → γ)
      (single (β := fun (i : ι) ↦ ↥(S i)) i (Subtype.mk (p := fun (x : γ) ↦ x ∈ S i) y hy)) =
    y

Tactic:
exact sumAddHom_single _ _ _

Premises used: DFinsupp.sumAddHom_single
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
⊢ Membership.mem.{w, w} (α := γ) (γ := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    ((AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
            (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p) :
          (a : Π₀ (i : ι), ↥(S i)) → γ)
        v :
      γ)

Tactic:
dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_

Premises used: Set.Mem, dfinsuppSumAddHom_mem, Trunc.lift
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
a :
  ∀ (i : ι),
    (((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i ≠
        0 →
      Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
        (((S i).subtype : (a : ↥(S i)) → γ)
            ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
                  Π₀ (i : ι), ↥(S i)) :
                (a : ι) → ↥(S a))
              i) :
          γ)
⊢ Membership.mem.{w, w} (α := γ) (γ := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    ((AddMonoidHom.comp (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype)
            (filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p) :
          (a : Π₀ (i : ι), ↥(S i)) → γ)
        v :
      γ)

Tactic:
refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_

Premises used: dfinsuppSumAddHom_mem
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
h :
  (((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
          Π₀ (i : ι), ↥(S i)) :
        (a : ι) → ↥(S a))
      i ≠
    0
⊢ Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (((S i).subtype : (a : ↥(S i)) → γ)
        ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      γ)

Tactic:
AddSubmonoid.mem_iSup_of_mem i ?_

Premises used: Set.Mem, AddSubmonoid.mem_iSup_of_mem
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
h :
  (((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
          Π₀ (i : ι), ↥(S i)) :
        (a : ι) → ↥(S a))
      i ≠
    0
a :
  Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (_ : p i), S i)
    (((S i).subtype : (a : ↥(S i)) → γ)
        ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      γ)
⊢ Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (i : ι), ⨆ (_ : p i), S i)
    (((S i).subtype : (a : ↥(S i)) → γ)
        ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      γ)

Tactic:
refine AddSubmonoid.mem_iSup_of_mem i ?_

Premises used: AddSubmonoid.mem_iSup_of_mem
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
h :
  (((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
          Π₀ (i : ι), ↥(S i)) :
        (a : ι) → ↥(S a))
      i ≠
    0
pos :
  ∀ (hp : p i),
    Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (_ : p i), S i)
      (((S i).subtype : (a : ↥(S i)) → γ)
          ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
                Π₀ (i : ι), ↥(S i)) :
              (a : ι) → ↥(S a))
            i) :
        γ)
neg :
  ∀ (hp : ¬p i),
    Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (_ : p i), S i)
      (((S i).subtype : (a : ↥(S i)) → γ)
          ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
                Π₀ (i : ι), ↥(S i)) :
              (a : ι) → ↥(S a))
            i) :
        γ)
⊢ Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (_ : p i), S i)
    (((S i).subtype : (a : ↥(S i)) → γ)
        ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      γ)

Tactic:
by_cases hp : p i
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
h :
  (((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
          Π₀ (i : ι), ↥(S i)) :
        (a : ι) → ↥(S a))
      i ≠
    0
hp : p i
⊢ Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (_ : p i), S i)
    (((S i).subtype : (a : ↥(S i)) → γ)
        ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      γ)

Tactic:
simp [hp]
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
p : ι → Prop
inst_1 : DecidablePred p
inst_2 : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
h :
  (((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
          Π₀ (i : ι), ↥(S i)) :
        (a : ι) → ↥(S a))
      i ≠
    0
hp : ¬p i
⊢ Membership.mem (α := γ) (γ := AddSubmonoid γ) (⨆ (_ : p i), S i)
    (((S i).subtype : (a : ↥(S i)) → γ)
        ((((filterAddMonoidHom (fun (i : ι) ↦ ↥(S i)) p : (a : Π₀ (i : ι), ↥(S i)) → Π₀ (i : ι), ↥(S i)) v :
              Π₀ (i : ι), ↥(S i)) :
            (a : ι) → ↥(S a))
          i) :
      γ)

Tactic:
simp [hp]
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
x : γ
⊢ x ∈ iSup S ↔
    ∃ (f : Π₀ (i : ι), ↥(S i)),
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype : (a : Π₀ (i : ι), ↥(S i)) → γ) f = x

Tactic:
SetLike.ext_iff.mp (AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom S) x

Premises used: Set.Mem, setOf, SetLike.ext_iff, AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom, Iff.mp, Set.range
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst_2 : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
rw :
  (∃ (f : Π₀ (i : ι), ↥(S i)),
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype : (a : Π₀ (i : ι), ↥(S i)) → γ) f = x) ↔
    ∃ (f : Π₀ (i : ι), ↥(S i)), (f.sum (β := fun (i : ι) ↦ ↥(S i)) fun (x : ι) (xi : ↥(S x)) ↦ (↑xi : γ)) = x
⊢ x ∈ iSup S ↔ ∃ (f : Π₀ (i : ι), ↥(S i)), (f.sum (β := fun (i : ι) ↦ ↥(S i)) fun (x : ι) (xi : ↥(S x)) ↦ (↑xi : γ)) = x

Tactic:
rw [AddSubmonoid.mem_iSup_iff_exists_dfinsupp]

Premises used: AddSubmonoid.mem_iSup_iff_exists_dfinsupp
-- Module: Mathlib.Data.DFinsupp.Submonoid
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
inst_1 : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst_2 : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
simp_rw :
  (∃ (f : Π₀ (i : ι), ↥(S i)),
      (f.sum (β := fun (i : ι) ↦ ↥(S i)) fun (x : ι) ↦ (⇑(S x).subtype : (a : ↥(S x)) → γ)) = x) ↔
    ∃ (f : Π₀ (i : ι), ↥(S i)), (f.sum (β := fun (i : ι) ↦ ↥(S i)) fun (x : ι) (xi : ↥(S x)) ↦ (↑xi : γ)) = x
⊢ (∃ (f : Π₀ (i : ι), ↥(S i)),
      (sumAddHom (β := fun (i : ι) ↦ ↥(S i)) fun (i : ι) ↦ (S i).subtype : (a : Π₀ (i : ι), ↥(S i)) → γ) f = x) ↔
    ∃ (f : Π₀ (i : ι), ↥(S i)), (f.sum (β := fun (i : ι) ↦ ↥(S i)) fun (x : ι) (xi : ↥(S x)) ↦ (↑xi : γ)) = x

Tactic:
simp_rw [sumAddHom_apply]

Premises used: DFinsupp.sumAddHom_apply