no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : 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₂
⊢ ∀ (x : ι), x ∈ support f ∪ support g → ¬x ∈ support f → h x (↑f x) = 1
simp (config := { contextual := true }) [mem_support_iff, h_zero]
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : 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 in support f ∪ support g, h i (↑f i) = prod f h
⊢ ∀ (x : ι), x ∈ support f ∪ support g → ¬x ∈ support g → h x (↑g x) = 1
simp (config := { contextual := true }) [mem_support_iff, h_zero]
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : 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 in support f ∪ support g, h i (↑f i) = prod f h
g_eq : ∏ i in support f ∪ support g, h i (↑g i) = prod g h
⊢ ∀ (x : ι), x ∈ support f ∪ support g → ¬x ∈ support (f + g) → h x (↑(f + g) x) = 1
simp (config := { contextual := true }) [mem_support_iff, h_zero]
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : 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 in support f ∪ support g, h i (↑f i) = prod f h
g_eq : ∏ i in support f ∪ support g, h i (↑g i) = prod g h
⊢ (∏ i in support f ∪ support g, h i (↑f i)) * ∏ i in support f ∪ support g, h i (↑g i) = prod f h * prod g h
rw [f_eq, g_eq]