-- 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 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)

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

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
⊢ ∃ a b, (x.coeff a ≠ 0 ∧ y.coeff b ≠ 0 ∧ a + b = g) ∧ Prod.map ⇑f.toEmbedding ⇑f.toEmbedding (a, b) = (f i, f j)

Proof state:
case neg
Γ : 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 : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f x * embDomain f y).coeff g = 0

Tactic:
contrapose! hg

Result:
case neg
Γ : 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 : Γ'
hg : (embDomain f x * embDomain f y).coeff g ≠ 0
⊢ g ∈ Set.range ⇑f

Proof state:
case hf.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 : Γ
fst✝ snd✝ : Γ'
h1 : (fst✝, snd✝) ∈ addAntidiagonal ⋯ ⋯ (f g)
h2 : (embDomain f x).coeff (fst✝, snd✝).1 * (embDomain f y).coeff (fst✝, snd✝).2 ≠ 0
⊢ (fst✝, snd✝) ∈ Finset.map (f.prodMap f.toEmbedding) (addAntidiagonal ⋯ ⋯ g)

Tactic:
obtain ⟨i, _, rfl⟩ := support_embDomain_subset (ne_zero_and_ne_zero_of_mul h2).1

Result:
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)

Proof state:
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
⊢ ∃ a b, (x.coeff a ≠ 0 ∧ y.coeff b ≠ 0 ∧ a + b = g) ∧ Prod.map ⇑f.toEmbedding ⇑f.toEmbedding (a, b) = (f i, f j)

Tactic:
simp only [mem_addAntidiagonal, embDomain_coeff, mem_support, ← hf,
  OrderEmbedding.eq_iff_eq] at h1

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
h2 : (embDomain f x).coeff (f i, f j).1 * (embDomain f y).coeff (f i, f j).2 ≠ 0
h1 : x.coeff i ≠ 0 ∧ y.coeff j ≠ 0 ∧ i + j = g
⊢ ∃ a b, (x.coeff a ≠ 0 ∧ y.coeff b ≠ 0 ∧ a + b = g) ∧ Prod.map ⇑f.toEmbedding ⇑f.toEmbedding (a, b) = (f i, f j)

Proof state:
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

Tactic:
rintro ⟨_, _⟩ h1 h2

Result:
case hf.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 : Γ
fst✝ snd✝ : Γ'
h1 : (fst✝, snd✝) ∈ addAntidiagonal ⋯ ⋯ (f g)
h2 : (fst✝, snd✝) ∉ Finset.map (f.prodMap f.toEmbedding) (addAntidiagonal ⋯ ⋯ g)
⊢ (embDomain f x).coeff (fst✝, snd✝).1 * (embDomain f y).coeff (fst✝, snd✝).2 = 0

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 : ∃ 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)

Tactic:
obtain ⟨i, j, ⟨hx, hy, rfl⟩, rfl, rfl⟩ := hij

Result:
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))

Proof state:
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

Tactic:
by_cases hg : g ∈ Set.range f

Result:
case pos
Γ : 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 : Γ'
hg : g ∈ Set.range ⇑f
⊢ (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g

case neg
Γ : 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 : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g