-- Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean
theorem mul_apply_mul_eq_mul_of_uniqueMul [Mul A] {f g : MonoidAlgebra R A} {a0 b0 : A}
    (h : UniqueMul f.support g.support a0 b0) :
    (f * g) (a0 * b0) = f a0 * g b0

Proof state:
case refine_2.inl
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
hnmem : ¬(a0 ∈ f.support ∧ b0 ∈ g.support)
x✝ : True
af : a0 ∉ f.support
⊢ f a0 * g b0 = 0

Tactic:
rw [not_mem_support_iff.mp af, zero_mul]

Result:
no goals

Proof state:
case refine_1.refine_1
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
ab : A × A
hab : ab.1 ∈ f.support ∧ ab.2 ∈ g.support
hne : ab ≠ (a0, b0)
he : ab.1 * ab.2 = a0 * b0
⊢ ab.1 = (a0, b0).1

case refine_1.refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
ab : A × A
hab : ab.1 ∈ f.support ∧ ab.2 ∈ g.support
hne : ab ≠ (a0, b0)
he : ab.1 * ab.2 = a0 * b0
⊢ ab.2 = (a0, b0).2

Tactic:
exacts [(h hab.1 hab.2 he).1, (h hab.1 hab.2 he).2]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
⊢ (f * g) (a0 * b0) = f a0 * g b0

Tactic:
simp_rw [mul_apply, sum, ← Finset.sum_product']

Result:
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
⊢ (∑ x ∈ f.support ×ˢ g.support, if x.1 * x.2 = a0 * b0 then f x.1 * g x.2 else 0) = f a0 * g b0

Proof state:
case refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
⊢ ¬(a0 ∈ f.support ∧ b0 ∈ g.support) → (if True then f a0 * g b0 else 0) = 0

Tactic:
refine fun hnmem => ite_eq_right_iff.mpr (fun _ => ?_)

Result:
case refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
hnmem : ¬(a0 ∈ f.support ∧ b0 ∈ g.support)
x✝ : True
⊢ f a0 * g b0 = 0

Proof state:
case refine_1
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
⊢ ∀ (b : A × A),
    b.1 ∈ f.support ∧ b.2 ∈ g.support → b ≠ (a0, b0) → (if b.1 * b.2 = a0 * b0 then f b.1 * g b.2 else 0) = 0

Tactic:
refine fun ab hab hne => if_neg (fun he => hne <| Prod.ext ?_ ?_)

Result:
case refine_1.refine_1
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
ab : A × A
hab : ab.1 ∈ f.support ∧ ab.2 ∈ g.support
hne : ab ≠ (a0, b0)
he : ab.1 * ab.2 = a0 * b0
⊢ ab.1 = (a0, b0).1

case refine_1.refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
ab : A × A
hab : ab.1 ∈ f.support ∧ ab.2 ∈ g.support
hne : ab ≠ (a0, b0)
he : ab.1 * ab.2 = a0 * b0
⊢ ab.2 = (a0, b0).2

Proof state:
case refine_2.inr
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
hnmem : ¬(a0 ∈ f.support ∧ b0 ∈ g.support)
x✝ : True
bg : b0 ∉ g.support
⊢ f a0 * g b0 = 0

Tactic:
rw [not_mem_support_iff.mp bg, mul_zero]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
⊢ (∑ x ∈ f.support ×ˢ g.support, if x.1 * x.2 = a0 * b0 then f x.1 * g x.2 else 0) = f a0 * g b0

Tactic:
refine (Finset.sum_eq_single (a0, b0) ?_ ?_).trans (if_pos rfl) <;> simp_rw [Finset.mem_product]

Result:
case refine_1
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
⊢ ∀ (b : A × A),
    b.1 ∈ f.support ∧ b.2 ∈ g.support → b ≠ (a0, b0) → (if b.1 * b.2 = a0 * b0 then f b.1 * g b.2 else 0) = 0

case refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
⊢ ¬(a0 ∈ f.support ∧ b0 ∈ g.support) → (if True then f a0 * g b0 else 0) = 0

Proof state:
case refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
hnmem : ¬(a0 ∈ f.support ∧ b0 ∈ g.support)
x✝ : True
⊢ f a0 * g b0 = 0

Tactic:
rcases not_and_or.mp hnmem with af | bg

Result:
case refine_2.inl
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
hnmem : ¬(a0 ∈ f.support ∧ b0 ∈ g.support)
x✝ : True
af : a0 ∉ f.support
⊢ f a0 * g b0 = 0

case refine_2.inr
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : MonoidAlgebra R A
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
hnmem : ¬(a0 ∈ f.support ∧ b0 ∈ g.support)
x✝ : True
bg : b0 ∉ g.support
⊢ f a0 * g b0 = 0