-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem single_mul_single {a b : Γ} {r s : R} :
    single a r * single b s = single (a + b) (r * s)

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ∀ (x_1 : Γ × Γ),
    x_1.1 ∈ ((single a) r).support ∧ x_1.2 ∈ ((single b) s).support ∧ x_1.1 + x_1.2 = x →
      ((single a) r).coeff x_1.1 * ((single b) s).coeff x_1.2 = 0

Tactic:
rintro ⟨y, z⟩ ⟨hy, hz, rfl⟩

Result:
case neg.mk.intro.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
y z : Γ
hy : (y, z).1 ∈ ((single a) r).support
hz : (y, z).2 ∈ ((single b) s).support
h : ¬(y, z).1 + (y, z).2 = a + b
⊢ ((single a) r).coeff (y, z).1 * ((single b) s).coeff (y, z).2 = 0

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
⊢ ((single a) r * (single b) s).coeff x = ((single (a + b)) (r * s)).coeff x

Tactic:
by_cases h : x = a + b

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ ((single a) r * (single b) s).coeff x = ((single (a + b)) (r * s)).coeff x

case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ((single a) r * (single b) s).coeff x = ((single (a + b)) (r * s)).coeff x

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ ((single a) r).coeff a * s = ((single (a + b)) (r * s)).coeff (a + b)

Tactic:
simp

Result:
no goals

Proof state:
case neg.mk.intro.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
y z : Γ
hy : (y, z).1 ∈ ((single a) r).support
hz : (y, z).2 ∈ ((single b) s).support
h : ¬(y, z).1 + (y, z).2 = a + b
⊢ ((single a) r).coeff (y, z).1 * ((single b) s).coeff (y, z).2 = 0

Tactic:
rw [eq_of_mem_support_single hy, eq_of_mem_support_single hz] at h

Result:
case neg.mk.intro.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
y z : Γ
hy : (y, z).1 ∈ ((single a) r).support
hz : (y, z).2 ∈ ((single b) s).support
h : ¬a + b = a + b
⊢ ((single a) r).coeff (y, z).1 * ((single b) s).coeff (y, z).2 = 0

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

Tactic:
rw [coeff_single_of_ne h, coeff_mul, sum_eq_zero]

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

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

Tactic:
simp_rw [mem_addAntidiagonal]

Result:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ∀ (x_1 : Γ × Γ),
    x_1.1 ∈ ((single a) r).support ∧ x_1.2 ∈ ((single b) s).support ∧ x_1.1 + x_1.2 = x →
      ((single a) r).coeff x_1.1 * ((single b) s).coeff x_1.2 = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
⊢ (single a) r * (single b) s = (single (a + b)) (r * s)

Tactic:
ext x

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
⊢ ((single a) r * (single b) s).coeff x = ((single (a + b)) (r * s)).coeff x

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ ((single a) r * (single b) s).coeff x = ((single (a + b)) (r * s)).coeff x

Tactic:
rw [h, coeff_mul_single_add]

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ ((single a) r).coeff a * s = ((single (a + b)) (r * s)).coeff (a + b)

Proof state:
case neg.mk.intro.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
y z : Γ
hy : (y, z).1 ∈ ((single a) r).support
hz : (y, z).2 ∈ ((single b) s).support
h : ¬a + b = a + b
⊢ ((single a) r).coeff (y, z).1 * ((single b) s).coeff (y, z).2 = 0

Tactic:
exact (h rfl).elim

Result:
no goals