-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem mul_apply_antidiagonal [Mul G] (f g : MonoidAlgebra k G) (x : G) (s : Finset (G × G))
    (hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x) : (f * g) x = ∑ p ∈ s, f p.1 * g p.2

Proof state:
case pos
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f p.1 ≠ 0 → g p.2 = 0
h1 : f p.1 = 0
⊢ f p.1 * g p.2 = 0

Tactic:
rw [h1, zero_mul]

Result:
no goals

Proof state:
case h
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
⊢ Finset.filter (fun p => p.1 * p.2 = x) (f.support ×ˢ g.support) =
    Finset.filter (fun p => p.1 ∈ f.support ∧ p.2 ∈ g.support) s

Tactic:
ext

Result:
case h.h
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
a✝ : G × G
⊢ a✝ ∈ Finset.filter (fun p => p.1 * p.2 = x) (f.support ×ˢ g.support) ↔
    a✝ ∈ Finset.filter (fun p => p.1 ∈ f.support ∧ p.2 ∈ g.support) s

Proof state:
case h.h
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
a✝ : G × G
⊢ a✝ ∈ Finset.filter (fun p => p.1 * p.2 = x) (f.support ×ˢ g.support) ↔
    a✝ ∈ Finset.filter (fun p => p.1 ∈ f.support ∧ p.2 ∈ g.support) s

Tactic:
simp only [mem_filter, mem_product, hs, and_comm]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
⊢ ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) = ∑ p ∈ f.support ×ˢ g.support, F p

Tactic:
rw [Finset.sum_product]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
⊢ ∑ p ∈ Finset.filter (fun p => p.1 * p.2 = x) (f.support ×ˢ g.support), f p.1 * g p.2 =
    ∑ p ∈ Finset.filter (fun p => p.1 ∈ f.support ∧ p.2 ∈ g.support) s, f p.1 * g p.2

Tactic:
congr! 1

Result:
case h
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
⊢ Finset.filter (fun p => p.1 * p.2 = x) (f.support ×ˢ g.support) =
    Finset.filter (fun p => p.1 ∈ f.support ∧ p.2 ∈ g.support) s

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∉ Finset.filter (fun p => p.1 ∈ f.support ∧ p.2 ∈ g.support) s
⊢ f p.1 * g p.2 = 0

Tactic:
simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢

Result:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f p.1 ≠ 0 → g p.2 = 0
⊢ f p.1 * g p.2 = 0

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f p.1 ≠ 0 → g p.2 = 0
⊢ f p.1 * g p.2 = 0

Tactic:
by_cases h1 : f p.1 = 0

Result:
case pos
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f p.1 ≠ 0 → g p.2 = 0
h1 : f p.1 = 0
⊢ f p.1 * g p.2 = 0

case neg
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f p.1 ≠ 0 → g p.2 = 0
h1 : ¬f p.1 = 0
⊢ f p.1 * g p.2 = 0

Proof state:
case neg
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
f g : MonoidAlgebra k G
x : G
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f p.1 ≠ 0 → g p.2 = 0
h1 : ¬f p.1 = 0
⊢ f p.1 * g p.2 = 0

Tactic:
rw [hp hps h1, mul_zero]

Result:
no goals