R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ (sum f fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) = ↑f a0 * ↑g b0
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ ↑(f * g) (a0 + b0) = ↑f a0 * ↑g b0
rw [mul_apply]
case refine'_1
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ ∀ (b : A),
    b ∈ f.support → b ≠ a0 → (fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) b (↑f b) = 0

case refine'_2
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ ¬a0 ∈ f.support → (fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) a0 (↑f a0) = 0

case refine'_3
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ (fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) a0 (↑f a0) = ↑f a0 * ↑g b0
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ (sum f fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) = ↑f a0 * ↑g b0
refine' (Finset.sum_eq_single a0 _ _).trans _
no goals
case refine'_1
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ ∀ (b : A),
    b ∈ f.support → b ≠ a0 → (fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) b (↑f b) = 0
exact fun b H hb => Finset.sum_eq_zero fun x H1 => if_neg (h H H1 (Or.inl hb))
no goals
case refine'_2
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ ¬a0 ∈ f.support → (fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) a0 (↑f a0) = 0
exact fun af0 => by simp [not_mem_support_iff.mp af0]
no goals
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
af0 : ¬a0 ∈ f.support
⊢ (fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) a0 (↑f a0) = 0
simp [not_mem_support_iff.mp af0]
case refine'_3.refine'_1
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0✝ : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0✝ → a + b ≠ a0 + b0✝
b : A
bg : b ∈ g.support
b0 : b ≠ b0✝
⊢ (fun a₂ b₂ => if a0 + a₂ = a0 + b0✝ then ↑f a0 * b₂ else 0) b (↑g b) = 0

case refine'_3.refine'_2
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ ¬b0 ∈ g.support → (fun a₂ b₂ => if a0 + a₂ = a0 + b0 then ↑f a0 * b₂ else 0) b0 (↑g b0) = 0
case refine'_3
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ (fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ + a₂ = a0 + b0 then b₁ * b₂ else 0) a0 (↑f a0) = ↑f a0 * ↑g b0
refine' (Finset.sum_eq_single b0 (fun b bg b0 => _) _).trans (if_pos rfl)
case pos
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0✝ : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0✝ → a + b ≠ a0 + b0✝
b : A
bg : b ∈ g.support
b0 : b ≠ b0✝
af : a0 ∈ f.support
⊢ (fun a₂ b₂ => if a0 + a₂ = a0 + b0✝ then ↑f a0 * b₂ else 0) b (↑g b) = 0

case neg
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0✝ : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0✝ → a + b ≠ a0 + b0✝
b : A
bg : b ∈ g.support
b0 : b ≠ b0✝
af : ¬a0 ∈ f.support
⊢ (fun a₂ b₂ => if a0 + a₂ = a0 + b0✝ then ↑f a0 * b₂ else 0) b (↑g b) = 0
case refine'_3.refine'_1
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0✝ : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0✝ → a + b ≠ a0 + b0✝
b : A
bg : b ∈ g.support
b0 : b ≠ b0✝
⊢ (fun a₂ b₂ => if a0 + a₂ = a0 + b0✝ then ↑f a0 * b₂ else 0) b (↑g b) = 0
by_cases af : a0 ∈ f.support
no goals
case pos
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0✝ : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0✝ → a + b ≠ a0 + b0✝
b : A
bg : b ∈ g.support
b0 : b ≠ b0✝
af : a0 ∈ f.support
⊢ (fun a₂ b₂ => if a0 + a₂ = a0 + b0✝ then ↑f a0 * b₂ else 0) b (↑g b) = 0
exact if_neg (h af bg (Or.inr b0))
no goals
case neg
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0✝ : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0✝ → a + b ≠ a0 + b0✝
b : A
bg : b ∈ g.support
b0 : b ≠ b0✝
af : ¬a0 ∈ f.support
⊢ (fun a₂ b₂ => if a0 + a₂ = a0 + b0✝ then ↑f a0 * b₂ else 0) b (↑g b) = 0
simp only [not_mem_support_iff.mp af, MulZeroClass.zero_mul, ite_self]
no goals
case refine'_3.refine'_2
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
⊢ ¬b0 ∈ g.support → (fun a₂ b₂ => if a0 + a₂ = a0 + b0 then ↑f a0 * b₂ else 0) b0 (↑g b0) = 0
exact fun bf0 => by simp [not_mem_support_iff.mp bf0]
no goals
R : Type u_2
A : Type u_1
inst✝¹ : Semiring R
inst✝ : Add A
f g : AddMonoidAlgebra R A
a0 b0 : A
h : ∀ {a b : A}, a ∈ f.support → b ∈ g.support → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
bf0 : ¬b0 ∈ g.support
⊢ (fun a₂ b₂ => if a0 + a₂ = a0 + b0 then ↑f a0 * b₂ else 0) b0 (↑g b0) = 0
simp [not_mem_support_iff.mp bf0]