-- 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
Γ : 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

Tactic:
contrapose! 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 : (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)

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

Tactic:
exact ⟨i, j, h1, rfl⟩

Result:
no goals

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 * y)).coeff g = (embDomain f x * embDomain f y).coeff g

Tactic:
rw [embDomain_notin_range hg, eq_comm]

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

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

Tactic:
obtain ⟨g, rfl⟩ := hg

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 : Γ
⊢ (embDomain f (x * y)).coeff (f g) = (embDomain f x * embDomain f y).coeff (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
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

Tactic:
simp

Result:
no goals

Proof state:
case neg.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
w✝ : Γ'
hj : w✝ ∈ (embDomain f y).support
i : Γ
left✝ : i ∈ x.support
hi : f i ∈ (embDomain f x).support
hg : (embDomain f x * embDomain f y).coeff ((fun x1 x2 => x1 + x2) (f i) w✝) ≠ 0
⊢ (fun x1 x2 => x1 + x2) (f i) w✝ ∈ Set.range ⇑f

Tactic:
obtain ⟨j, _, rfl⟩ := support_embDomain_subset hj

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

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

Tactic:
rintro ⟨i, j⟩ 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 : (i, j) ∈ Finset.map (f.prodMap f.toEmbedding) (addAntidiagonal ⋯ ⋯ g)
⊢ (i, j) ∈ addAntidiagonal ⋯ ⋯ (f g)

Proof state:
case neg.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
w✝¹ : Γ'
hi : w✝¹ ∈ (embDomain f x).support
w✝ : Γ'
hj : w✝ ∈ (embDomain f y).support
hg : (embDomain f x * embDomain f y).coeff ((fun x1 x2 => x1 + x2) w✝¹ w✝) ≠ 0
⊢ (fun x1 x2 => x1 + x2) w✝¹ w✝ ∈ Set.range ⇑f

Tactic:
obtain ⟨i, _, rfl⟩ := support_embDomain_subset hi

Result:
case neg.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
w✝ : Γ'
hj : w✝ ∈ (embDomain f y).support
i : Γ
left✝ : i ∈ x.support
hi : f i ∈ (embDomain f x).support
hg : (embDomain f x * embDomain f y).coeff ((fun x1 x2 => x1 + x2) (f i) w✝) ≠ 0
⊢ (fun x1 x2 => x1 + x2) (f i) w✝ ∈ Set.range ⇑f

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

Tactic:
obtain ⟨_, hi, _, hj, rfl⟩ := support_mul_subset_add_support ((mem_support _ _).2 hg)

Result:
case neg.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
w✝¹ : Γ'
hi : w✝¹ ∈ (embDomain f x).support
w✝ : Γ'
hj : w✝ ∈ (embDomain f y).support
hg : (embDomain f x * embDomain f y).coeff ((fun x1 x2 => x1 + x2) w✝¹ w✝) ≠ 0
⊢ (fun x1 x2 => x1 + x2) w✝¹ w✝ ∈ Set.range ⇑f