-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
protected lemma map_mul [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S)
    {x y : HahnSeries Γ R} : (x * y).map f = (x.map f : HahnSeries Γ S) * (y.map f)

Proof state:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
⊢ (x * y).map f = x.map f * y.map f

Tactic:
ext

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
⊢ ((x * y).map f).coeff x✝ = (x.map f * y.map f).coeff x✝

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
⊢ ∑ x_1 ∈ addAntidiagonal ⋯ ⋯ x✝, f (x.coeff x_1.1) * f (y.coeff x_1.2) =
    ∑ x_1 ∈ addAntidiagonal ⋯ ⋯ x✝, f (x.coeff x_1.1) * f (y.coeff x_1.2)

Tactic:
refine Eq.symm (sum_subset (fun gh hgh => ?_) (fun gh hgh hz => ?_))

Result:
case coeff.h.refine_1
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
gh : Γ × Γ
hgh : gh ∈ addAntidiagonal ⋯ ⋯ x✝
⊢ gh ∈ addAntidiagonal ⋯ ⋯ x✝

case coeff.h.refine_2
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
gh : Γ × Γ
hgh : gh ∈ addAntidiagonal ⋯ ⋯ x✝
hz : gh ∉ addAntidiagonal ⋯ ⋯ x✝
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0

Proof state:
case coeff.h.refine_2
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x✝
hz : ¬f (x.coeff gh.1) = 0 → f (y.coeff gh.2) = 0
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0

Tactic:
by_cases h : f (x.coeff gh.1) = 0

Result:
case pos
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x✝
hz : ¬f (x.coeff gh.1) = 0 → f (y.coeff gh.2) = 0
h : f (x.coeff gh.1) = 0
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0

case neg
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x✝
hz : ¬f (x.coeff gh.1) = 0 → f (y.coeff gh.2) = 0
h : ¬f (x.coeff gh.1) = 0
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0

Proof state:
case coeff.h.refine_2
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
gh : Γ × Γ
hgh : gh ∈ addAntidiagonal ⋯ ⋯ x✝
hz : gh ∉ addAntidiagonal ⋯ ⋯ x✝
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0

Tactic:
simp_all only [mem_addAntidiagonal, mem_support, ne_eq, map_coeff, ZeroHom.coe_coe, and_true,
  not_and, not_not]

Result:
case coeff.h.refine_2
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x✝
hz : ¬f (x.coeff gh.1) = 0 → f (y.coeff gh.2) = 0
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0

Proof state:
case coeff.h.refine_1
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
gh : Γ × Γ
hgh : gh ∈ addAntidiagonal ⋯ ⋯ x✝
⊢ gh ∈ addAntidiagonal ⋯ ⋯ x✝

Tactic:
simp_all only [mem_addAntidiagonal, mem_support, map_coeff, ZeroHom.coe_coe, ne_eq, and_true]

Result:
case coeff.h.refine_1
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
gh : Γ × Γ
hgh : ¬f (x.coeff gh.1) = 0 ∧ ¬f (y.coeff gh.2) = 0 ∧ gh.1 + gh.2 = x✝
⊢ ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0

Proof state:
case pos
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x✝
hz : ¬f (x.coeff gh.1) = 0 → f (y.coeff gh.2) = 0
h : f (x.coeff gh.1) = 0
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0

Tactic:
exact mul_eq_zero_of_left h (f (y.coeff gh.2))

Result:
no goals

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
⊢ ((x * y).map f).coeff x✝ = (x.map f * y.map f).coeff x✝

Tactic:
simp only [map_coeff, coeff_mul, ZeroHom.coe_coe, map_sum, map_mul]

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
⊢ ∑ x_1 ∈ addAntidiagonal ⋯ ⋯ x✝, f (x.coeff x_1.1) * f (y.coeff x_1.2) =
    ∑ x_1 ∈ addAntidiagonal ⋯ ⋯ x✝, f (x.coeff x_1.1) * f (y.coeff x_1.2)

Proof state:
case neg
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x✝
hz : ¬f (x.coeff gh.1) = 0 → f (y.coeff gh.2) = 0
h : ¬f (x.coeff gh.1) = 0
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0

Tactic:
exact mul_eq_zero_of_right (f (x.coeff gh.1)) (hz h)

Result:
no goals

Proof state:
case coeff.h.refine_1
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : HahnSeries Γ R
x✝ : Γ
gh : Γ × Γ
hgh : ¬f (x.coeff gh.1) = 0 ∧ ¬f (y.coeff gh.2) = 0 ∧ gh.1 + gh.2 = x✝
⊢ ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0

Tactic:
exact ⟨fun h => hgh.1 (map_zero f ▸ congrArg f h), fun h => hgh.2.1 (map_zero f ▸ congrArg f h)⟩

Result:
no goals