-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem coeff_mul_single_add [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ}
    {b : Γ} : (x * single b r).coeff (a + b) = x.coeff a * r

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
⊢ ∑ x_1 ∈ addAntidiagonal ⋯ ⋯ (a + b), x.coeff x_1.1 * ((single b) r).coeff x_1.2 =
    ∑ ij ∈ {(a, b)}, x.coeff ij.1 * ((single b) r).coeff ij.2

Tactic:
apply sum_congr _ fun _ _ => rfl

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
⊢ addAntidiagonal ⋯ ⋯ (a + b) = {(a, b)}

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
⊢ ∑ x_1 ∈ addAntidiagonal ⋯ ⋯ (a + b), x.coeff x_1.1 * ((single b) r).coeff x_1.2 = x.coeff a * r

Tactic:
trans ∑ ij ∈ {(a, b)}, x.coeff ij.fst * (single b r).coeff ij.snd

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
⊢ ∑ x_1 ∈ addAntidiagonal ⋯ ⋯ (a + b), x.coeff x_1.1 * ((single b) r).coeff x_1.2 =
    ∑ ij ∈ {(a, b)}, x.coeff ij.1 * ((single b) r).coeff ij.2

Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
⊢ ∑ ij ∈ {(a, b)}, x.coeff ij.1 * ((single b) r).coeff ij.2 = x.coeff a * r

Proof state:
case h.mk
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : x.coeff a = 0
a1 a2 : Γ
⊢ a1 ∈ x.support → a2 = b → ¬a1 + a2 = a + b

Tactic:
rintro h2 rfl h1

Result:
case h.mk
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
hr : ¬r = 0
hx : x.coeff a = 0
a1 a2 : Γ
h2 : a1 ∈ x.support
h1 : a1 + a2 = a + a2
⊢ False

Proof state:
case h.mk
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : x.coeff a = 0
a1 a2 : Γ
⊢ (a1, a2) ∈ addAntidiagonal ⋯ ⋯ (a + b) ↔ (a1, a2) ∈ ∅

Tactic:
simp only [not_mem_empty, not_and, Set.mem_singleton_iff, Classical.not_not,
  mem_addAntidiagonal, Set.mem_setOf_eq, iff_false]

Result:
case h.mk
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : x.coeff a = 0
a1 a2 : Γ
⊢ a1 ∈ x.support → a2 = b → ¬a1 + a2 = a + b

Proof state:
case h.mk.mp.intro.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
left✝ : a1 ∈ x.support
h1 : a1 + a2 = a + a2
⊢ a1 = a ∧ a2 = a2

Tactic:
exact ⟨add_right_cancel h1, rfl⟩

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
⊢ ∑ ij ∈ {(a, b)}, x.coeff ij.1 * ((single b) r).coeff ij.2 = x.coeff a * r

Tactic:
simp

Result:
no goals

Proof state:
case h.mk
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
hr : ¬r = 0
hx : x.coeff a = 0
a1 a2 : Γ
h2 : a1 ∈ x.support
h1 : a1 + a2 = a + a2
⊢ False

Tactic:
rw [← add_right_cancel h1] at hx

Result:
case h.mk
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
hr : ¬r = 0
a1 : Γ
hx : x.coeff a1 = 0
a2 : Γ
h2 : a1 ∈ x.support
h1 : a1 + a2 = a + a2
⊢ False

Proof state:
case h.mk.mpr
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
⊢ a1 = a ∧ a2 = b → a1 ∈ x.support ∧ a2 = b ∧ a1 + a2 = a + b

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case h.mk.mpr.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
hr : ¬r = 0
a1 a2 : Γ
hx : ¬x.coeff a1 = 0
⊢ a1 ∈ x.support ∧ a2 = a2 ∧ a1 + a2 = a1 + a2

Proof state:
case h.mk
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
⊢ a1 ∈ x.support ∧ a2 = b ∧ a1 + a2 = a + b ↔ a1 = a ∧ a2 = b

Tactic:
constructor

Result:
case h.mk.mp
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
⊢ a1 ∈ x.support ∧ a2 = b ∧ a1 + a2 = a + b → a1 = a ∧ a2 = b

case h.mk.mpr
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
⊢ a1 = a ∧ a2 = b → a1 ∈ x.support ∧ a2 = b ∧ a1 + a2 = a + b

Proof state:
case h.mk.mp
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
⊢ a1 ∈ x.support ∧ a2 = b ∧ a1 + a2 = a + b → a1 = a ∧ a2 = b

Tactic:
rintro ⟨_, rfl, h1⟩

Result:
case h.mk.mp.intro.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
left✝ : a1 ∈ x.support
h1 : a1 + a2 = a + a2
⊢ a1 = a ∧ a2 = a2

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
⊢ (x * (single b) r).coeff (a + b) = x.coeff a * r

Tactic:
simp only [hr, coeff_smul, coeff_mul, support_single_of_ne, Ne, not_false_iff, smul_eq_mul]

Result:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
⊢ ∑ x_1 ∈ addAntidiagonal ⋯ ⋯ (a + b), x.coeff x_1.1 * ((single b) r).coeff x_1.2 = x.coeff a * r

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
⊢ addAntidiagonal ⋯ ⋯ (a + b) = {(a, b)}

Tactic:
ext ⟨a1, a2⟩

Result:
case h.mk
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
⊢ (a1, a2) ∈ addAntidiagonal ⋯ ⋯ (a + b) ↔ (a1, a2) ∈ {(a, b)}

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : x.coeff a = 0
⊢ ∑ x_1 ∈ addAntidiagonal ⋯ ⋯ (a + b), x.coeff x_1.1 * ((single b) r).coeff x_1.2 = 0

Tactic:
rw [sum_congr _ fun _ _ => rfl, sum_empty]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a b : Γ
hr : ¬r = 0
hx : x.coeff a = 0
⊢ addAntidiagonal ⋯ ⋯ (a + b) = ∅