awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ Eq.{w + 1} (α := γ)
    (∏ x ∈ g.support (β := β₁),
      h x
        ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
              f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
            (a : ι) → β₂ a)
          x))
    (g.prod (β := β₁) fun (i : ι) (b : β₁ i) ↦ h i (f i b))
have refine_2 : ∀ x ∈ g.support (β := β₁),
  h x
      ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
            f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
          (a : ι) → β₂ a)
        x) =
    (fun (i : ι) (b : β₁ i) ↦ h i (f i b)) x ((g : (a : ι) → β₁ a) x)
Tactic: refine Finset.prod_congr rfl ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
i : ι
h1 : i ∈ g.support (β := β₁)
⊢ h i
      ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
            f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
          (a : ι) → β₂ a)
        i) =
    (fun (i : ι) (b : β₁ i) ↦ h i (f i b)) i ((g : (a : ι) → β₁ a) i)
have h1₁ : ¬(g : (a : ι) → β₁ a) i = 0
Tactic: simp only [mem_support_toFun, ne_eq] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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 γ
i : ι
b : β i
h : (i : ι) → β i → γ
h_zero : h i 0 = 1
⊢ prod (β := β) (single (β := β) i b) h = h i b
have pos : ∀ (h_1 : b ≠ 0), prod (β := β) (single (β := β) i b) h = h i b
Tactic: by_cases h : b ≠ 0
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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 γ
i : ι
b : β i
h : (i : ι) → β i → γ
h_zero : h i 0 = 1
pos : ∀ (h_1 : b ≠ 0), prod (β := β) (single (β := β) i b) h = h i b
⊢ prod (β := β) (single (β := β) i b) h = h i b
have neg : ∀ (h_1 : ¬b ≠ 0), prod (β := β) (single (β := β) i b) h = h i b
Tactic: by_cases h : b ≠ 0
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
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 γ
i : ι
b : β i
h_1 : (i : ι) → β i → γ
h_zero : h_1 i 0 = 1
h : ¬b ≠ 0
⊢ prod (β := β) (single (β := β) i b) h_1 = h_1 i b
have h₁ : b = 0
Tactic: rw [not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
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 γ
i : ι
b : β i
h_1 : (i : ι) → β i → γ
h_zero : h_1 i 0 = 1
h : b = 0
⊢ prod (β := β) (single (β := β) i b) h_1 = h_1 i b
have neg : prod (β := β) 0 h_1 = 1
Tactic: simp [h, h_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
ι₁ : Type u₁
inst_1 : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst_2 : (i₁ : ι₁) → Zero (β₁ i₁)
inst_3 : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → AddCommMonoid (β i)
inst_5 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
⊢ (f.sum (β := β₁) g).support (β := β) ⊆
    f.support (β := β₁).biUnion fun (i : ι₁) ↦ (g i ((f : (a : ι₁) → β₁ a) i)).support (β := β)
have this : ∀ (i₁ : ι),
  Ne.{v + 1} (α := β i₁) (f.sum (β := β₁) fun (i : ι₁) (b : β₁ i) ↦ (g i b : (a : ι) → β a) i₁) 0 →
    ∃ (i : ι₁), (f : (a : ι₁) → β₁ a) i ≠ 0 ∧ ¬(g i ((f : (a : ι₁) → β₁ a) i) : (a : ι) → β a) i₁ = 0
Tactic: have :
    ∀ i₁ : ι,
      (f.sum fun (i : ι₁) (b : β₁ i) => (g i b) i₁) ≠ 0 → ∃ i : ι₁, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0 :=
    fun i₁ h =>
    let ⟨i, hi, Ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
    ⟨i, mem_support_iff.1 hi, Ne⟩
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
f_eq : ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f : (a : ι) → β a) i) = f.prod (β := β) h
g_eq : ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i) = g.prod (β := β) h
⊢ HMul.hMul (α := γ) (∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f : (a : ι) → β a) i))
      (∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i)) =
    f.prod (β := β) h * g.prod (β := β) h
have rw : f.prod (β := β) h * ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i) =
  f.prod (β := β) h * g.prod (β := β) h
Tactic: rw [f_eq, g_eq]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
f_eq : ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f : (a : ι) → β a) i) = f.prod (β := β) h
g_eq : ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i) = g.prod (β := β) h
rw :
  f.prod (β := β) h * ∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i) =
    f.prod (β := β) h * g.prod (β := β) h
⊢ HMul.hMul (α := γ) (∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((f : (a : ι) → β a) i))
      (∏ i ∈ f.support (β := β) ∪ g.support (β := β), h i ((g : (a : ι) → β a) i)) =
    f.prod (β := β) h * g.prod (β := β) h
have rw₁ : f.prod (β := β) h * g.prod (β := β) h = f.prod (β := β) h * g.prod (β := β) h
Tactic: rw [f_eq, g_eq]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_4 : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
⊢ v.prod (β := β) f = ∏ i : ι, f i ((equivFunOnFintype (β := β) : (a : Π₀ (i : ι), β i) → (i : ι) → β i) v i)
have suffices : Eq.{w + 1} (α := γ) (∏ i ∈ v.support (β := β), f i ((v : (a : ι) → β a) i)) (∏ i : ι, f i ((v : (a : ι) → β a) i))
Tactic: suffices (∏ i ∈ v.support, f i (v i)) = ∏ i, f i (v i) by simp [DFinsupp.prod, this]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_4 : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
⊢ Eq.{w + 1} (α := γ) (∏ i ∈ v.support (β := β), f i ((v : (a : ι) → β a) i)) (∏ i : ι, f i ((v : (a : ι) → β a) i))
have apply : ∀ (x : ι), Membership.mem (γ := Finset ι) Finset.univ x → x ∉ v.support (β := β) → f x ((v : (a : ι) → β a) x) = 1
Tactic: apply Finset.prod_subset v.support.subset_univ
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_4 : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
hi : i ∉ v.support (β := β)
⊢ f i ((v : (a : ι) → β a) i) = 1
have hi₁ : (v : (a : ι) → β a) i = 0
Tactic: rw [mem_support_iff, not_not] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_4 : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
hi : (v : (a : ι) → β a) i = 0
⊢ f i ((v : (a : ι) → β a) i) = 1
have rw : f i 0 = 1
Tactic: rw [hi, hf]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_4 : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
hi : (v : (a : ι) → β a) i = 0
rw : f i 0 = 1
⊢ f i ((v : (a : ι) → β a) i) = 1
have rw₁ : Eq.{w + 1} (α := γ) 1 1
Tactic: rw [hi, hf]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
⊢ Eq.{w + 1} (α := γ)
    ((fun (s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }) ↦
        (∑ i ∈ (↑s : Multiset ι).toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ))
      (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0) sx hx))
    ((fun (s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0 }) ↦
        (∑ i ∈ (↑s : Multiset ι).toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ))
      (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0) sy hy))
have dsimp : Eq.{w + 1} (α := γ) (∑ i ∈ sx.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
  (∑ i ∈ sy.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
Tactic: dsimp only [Subtype.coe_mk, toFun_eq_coe] at *
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
⊢ Eq.{w + 1} (α := γ) (∑ i ∈ sx.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
    (∑ i ∈ sy.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
have H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
Tactic: have H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset := Finset.inter_subset_left
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
⊢ Eq.{w + 1} (α := γ) (∑ i ∈ sx.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
    (∑ i ∈ sy.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
have H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
Tactic: have H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset := Finset.inter_subset_right
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ Eq.{w + 1} (α := γ) (∑ i ∈ sx.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
    (∑ i ∈ sy.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
have refine_1 : ∀ x ∈ sx.toFinset,
  x ∉ sx.toFinset ∩ sy.toFinset → Eq.{w + 1} (α := γ) ((φ x : (a : β x) → γ) ((f : (a : ι) → β a) x) : γ) (0 : γ)
Tactic: refine
        (Finset.sum_subset H1 ?_).symm.trans
          ((Finset.sum_congr rfl ?_).trans (Finset.sum_subset H2 ?_))
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
refine_1 :
  ∀ x ∈ sx.toFinset,
    x ∉ sx.toFinset ∩ sy.toFinset → Eq.{w + 1} (α := γ) ((φ x : (a : β x) → γ) ((f : (a : ι) → β a) x) : γ) (0 : γ)
⊢ Eq.{w + 1} (α := γ) (∑ i ∈ sx.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
    (∑ i ∈ sy.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
have refine_2 : ∀ x ∈ sx.toFinset ∩ sy.toFinset,
  Eq.{w + 1} (α := γ) ((φ x : (a : β x) → γ) ((f : (a : ι) → β a) x) : γ)
    ((φ x : (a : β x) → γ) ((f : (a : ι) → β a) x) : γ)
Tactic: refine
        (Finset.sum_subset H1 ?_).symm.trans
          ((Finset.sum_congr rfl ?_).trans (Finset.sum_subset H2 ?_))
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
refine_1 :
  ∀ x ∈ sx.toFinset,
    x ∉ sx.toFinset ∩ sy.toFinset → Eq.{w + 1} (α := γ) ((φ x : (a : β x) → γ) ((f : (a : ι) → β a) x) : γ) (0 : γ)
refine_2 :
  ∀ x ∈ sx.toFinset ∩ sy.toFinset,
    Eq.{w + 1} (α := γ) ((φ x : (a : β x) → γ) ((f : (a : ι) → β a) x) : γ)
      ((φ x : (a : β x) → γ) ((f : (a : ι) → β a) x) : γ)
⊢ Eq.{w + 1} (α := γ) (∑ i ∈ sx.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
    (∑ i ∈ sy.toFinset, (φ i : (a : β i) → γ) ((f : (a : ι) → β a) i))
have refine_3 : ∀ x ∈ sy.toFinset,
  x ∉ sx.toFinset ∩ sy.toFinset → Eq.{w + 1} (α := γ) ((φ x : (a : β x) → γ) ((f : (a : ι) → β a) x) : γ) (0 : γ)
Tactic: refine
        (Finset.sum_subset H1 ?_).symm.trans
          ((Finset.sum_congr rfl ?_).trans (Finset.sum_subset H2 ?_))
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx.toFinset
H2 : i ∉ sx.toFinset ∩ sy.toFinset
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ) (0 : γ)
have H2₁ : ¬(i ∈ sx.toFinset ∧ i ∈ sy.toFinset)
Tactic: rw [Finset.mem_inter] at H2
Cleared hypotheses: H2
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx.toFinset
H2 : ¬(i ∈ sx.toFinset ∧ i ∈ sy.toFinset)
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ) (0 : γ)
have H1₁ : i ∈ sx
Tactic: simp only [Multiset.mem_toFinset] at H1 H2
Cleared hypotheses: H1, H2
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx.toFinset
H2 : ¬(i ∈ sx.toFinset ∧ i ∈ sy.toFinset)
H1₁ : i ∈ sx
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ) (0 : γ)
have H2₁ : ¬(i ∈ sx ∧ i ∈ sy)
Tactic: simp only [Multiset.mem_toFinset] at H1 H2
Cleared hypotheses: H1, H2
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sx
H2 : ¬(i ∈ sx ∧ i ∈ sy)
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ) (0 : γ)
have h : (f : (a : ι) → β a) i = 0
Tactic: convert! map_zero (φ i)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy.toFinset
H2 : i ∉ sx.toFinset ∩ sy.toFinset
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ) (0 : γ)
have H2₁ : ¬(i ∈ sx.toFinset ∧ i ∈ sy.toFinset)
Tactic: rw [Finset.mem_inter] at H2
Cleared hypotheses: H2
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy.toFinset
H2 : ¬(i ∈ sx.toFinset ∧ i ∈ sy.toFinset)
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ) (0 : γ)
have H1₁ : i ∈ sy
Tactic: simp only [Multiset.mem_toFinset] at H1 H2
Cleared hypotheses: H1, H2
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy.toFinset
H2 : ¬(i ∈ sx.toFinset ∧ i ∈ sy.toFinset)
H1₁ : i ∈ sy
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ) (0 : γ)
have H2₁ : ¬(i ∈ sx ∧ i ∈ sy)
Tactic: simp only [Multiset.mem_toFinset] at H1 H2
Cleared hypotheses: H1, H2
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun (β := fun (i : ι) ↦ β i) i = 0
H1_1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2_1 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
H1 : i ∈ sy
H2 : ¬(i ∈ sx ∧ i ∈ sy)
⊢ Eq.{w + 1} (α := γ) ((φ i : (a : β i) → γ) ((f : (a : ι) → β a) i) : γ) (0 : γ)
have h : (f : (a : ι) → β a) i = 0
Tactic: convert! map_zero (φ i)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : AddCommMonoid γ
φ : (i : ι) → ZeroHom.{v, w} (β i) γ
⊢ Eq.{w + 1} (α := γ)
    ((fun
          (c :
            ∀
              (a b :
                { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (toFun (β := fun (i : ι) ↦ β i) 0 i) 0 }),
              Eq.{w + 1} (α := γ)
                ((fun
                      (s :
                        { s : Multiset ι //
                          ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (toFun (β := fun (i : ι) ↦ β i) 0 i) 0 }) ↦
                    (∑ i ∈ (↑s : Multiset ι).toFinset, (φ i : (a : β i) → γ) ((0 : (a : ι) → β a) i) : γ))
                  a)
                ((fun
                      (s :
                        { s : Multiset ι //
                          ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (toFun (β := fun (i : ι) ↦ β i) 0 i) 0 }) ↦
                    (∑ i ∈ (↑s : Multiset ι).toFinset, (φ i : (a : β i) → γ) ((0 : (a : ι) → β a) i) : γ))
                  b)) ↦
        Trunc.lift
          (fun
              (s :
                { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (toFun (β := fun (i : ι) ↦ β i) 0 i) 0 }) ↦
            ∑ i ∈ (↑s : Multiset ι).toFinset, (φ i : (a : β i) → γ) ((0 : (a : ι) → β a) i))
          c (support' (β := fun (i : ι) ↦ β i) 0))
      ⋯)
    0
have simp : Eq.{w + 1} (α := γ)
  (Trunc.lift.{u + 1, w + 1} (α := { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) 0 0 })
    (fun (s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) 0 0 }) ↦ (0 : γ)) sorry
    (support' (β := fun (i : ι) ↦ β i) 0 :
      Trunc { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ Eq.{v + 1} (α := β i) (toFun (β := fun (i : ι) ↦ β i) 0 i) 0 }))
  0
Tactic: simp only [toFun_eq_coe, coe_zero, Pi.zero_apply, map_zero, Finset.sum_const_zero]