-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem embDomain_mul [NonUnitalNonAssocSemiring R] (f : Γ ↪o Γ')
    (hf : ∀ x y, f (x + y) = f x + f y) (x y : HahnSeries Γ R) :
    embDomain f (x * y) = embDomain f x * embDomain f y

Proof state:
case h.mk
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
g : Γ
i j : Γ'
hij : (i, j) ∈ Finset.map (f.prodMap f.toEmbedding) (addAntidiagonal ⋯ ⋯ g)
⊢ (i, j) ∈ addAntidiagonal ⋯ ⋯ (f g)

Tactic:
simp only [exists_prop, mem_map, Prod.mk.inj_iff, mem_addAntidiagonal,
  Function.Embedding.coe_prodMap, mem_support, Prod.exists] at hij

Result:
case h.mk
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
g : Γ
i j : Γ'
hij : ∃ a b, (x.coeff a ≠ 0 ∧ y.coeff b ≠ 0 ∧ a + b = g) ∧ Prod.map ⇑f.toEmbedding ⇑f.toEmbedding (a, b) = (i, j)
⊢ (i, j) ∈ addAntidiagonal ⋯ ⋯ (f g)

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
⊢ embDomain f (x * y) = embDomain f x * embDomain f y

Tactic:
ext g

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
g : Γ'
⊢ (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g

Proof state:
case pos.intro
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
g : Γ
⊢ ∑ ij ∈ addAntidiagonal ⋯ ⋯ g, x.coeff ij.1 * y.coeff ij.2 =
    ∑ ij ∈ addAntidiagonal ⋯ ⋯ (f g), (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2

Tactic:
trans
  ∑ ij ∈
    (addAntidiagonal x.isPWO_support y.isPWO_support g).map
      (f.toEmbedding.prodMap f.toEmbedding),
    (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2

Result:
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
g : Γ
⊢ ∑ ij ∈ addAntidiagonal ⋯ ⋯ g, x.coeff ij.1 * y.coeff ij.2 =
    ∑ ij ∈ Finset.map (f.prodMap f.toEmbedding) (addAntidiagonal ⋯ ⋯ g),
      (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2

Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
g : Γ
⊢ ∑ ij ∈ Finset.map (f.prodMap f.toEmbedding) (addAntidiagonal ⋯ ⋯ g),
      (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2 =
    ∑ ij ∈ addAntidiagonal ⋯ ⋯ (f g), (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2

Proof state:
case neg.intro.intro.intro.intro.intro.intro.intro.intro
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
i : Γ
left✝¹ : i ∈ x.support
hi : f i ∈ (embDomain f x).support
j : Γ
left✝ : j ∈ y.support
hj : f j ∈ (embDomain f y).support
hg : (embDomain f x * embDomain f y).coeff ((fun x1 x2 => x1 + x2) (f i) (f j)) ≠ 0
⊢ (fun x1 x2 => x1 + x2) (f i) (f j) ∈ Set.range ⇑f

Tactic:
exact ⟨i + j, hf i j⟩

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
g : Γ
⊢ ∑ ij ∈ Finset.map (f.prodMap f.toEmbedding) (addAntidiagonal ⋯ ⋯ g),
      (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2 =
    ∑ ij ∈ addAntidiagonal ⋯ ⋯ (f g), (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2

Tactic:
apply sum_subset

Result:
case h
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
g : Γ
⊢ Finset.map (f.prodMap f.toEmbedding) (addAntidiagonal ⋯ ⋯ g) ⊆ addAntidiagonal ⋯ ⋯ (f g)

case hf
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
g : Γ
⊢ ∀ x_1 ∈ addAntidiagonal ⋯ ⋯ (f g),
    x_1 ∉ Finset.map (f.prodMap f.toEmbedding) (addAntidiagonal ⋯ ⋯ g) →
      (embDomain f x).coeff x_1.1 * (embDomain f y).coeff x_1.2 = 0

Proof state:
case hf.mk.intro.intro
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
g : Γ
snd✝ : Γ'
i : Γ
left✝ : i ∈ x.support
h1 : (f i, snd✝) ∈ addAntidiagonal ⋯ ⋯ (f g)
h2 : (embDomain f x).coeff (f i, snd✝).1 * (embDomain f y).coeff (f i, snd✝).2 ≠ 0
⊢ (f i, snd✝) ∈ Finset.map (f.prodMap f.toEmbedding) (addAntidiagonal ⋯ ⋯ g)

Tactic:
obtain ⟨j, _, rfl⟩ := support_embDomain_subset (ne_zero_and_ne_zero_of_mul h2).2

Result:
case hf.mk.intro.intro.intro.intro
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
g i : Γ
left✝¹ : i ∈ x.support
j : Γ
left✝ : j ∈ y.support
h1 : (f i, f j) ∈ addAntidiagonal ⋯ ⋯ (f g)
h2 : (embDomain f x).coeff (f i, f j).1 * (embDomain f y).coeff (f i, f j).2 ≠ 0
⊢ (f i, f j) ∈ Finset.map (f.prodMap f.toEmbedding) (addAntidiagonal ⋯ ⋯ g)

Proof state:
case h.mk.intro.intro.intro.intro.intro.refl
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
i j : Γ
hx : x.coeff i ≠ 0
hy : y.coeff j ≠ 0
⊢ (f.toEmbedding i, f.toEmbedding j) ∈ addAntidiagonal ⋯ ⋯ (f (i + j))

Tactic:
simp [hx, hy, hf]

Result:
no goals

Proof state:
case pos.intro
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
g : Γ
⊢ (embDomain f (x * y)).coeff (f g) = (embDomain f x * embDomain f y).coeff (f g)

Tactic:
simp only [coeff_mul, embDomain_coeff]

Result:
case pos.intro
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : HahnSeries Γ R
g : Γ
⊢ ∑ ij ∈ addAntidiagonal ⋯ ⋯ g, x.coeff ij.1 * y.coeff ij.2 =
    ∑ ij ∈ addAntidiagonal ⋯ ⋯ (f g), (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2