awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ'
hg : Membership.mem (γ := Set Γ') (Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g
pos :
  ∀ (g : Γ),
    (embDomain f (x * y)).coeff ((f : (a : Γ) → Γ') g) = (embDomain f x * embDomain f y).coeff ((f : (a : Γ) → Γ') g)
⊢ (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g

Tactic:
obtain ⟨g, rfl⟩ := hg

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ
pos :
  Eq.{u_3 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g, x.coeff ij.1 * y.coeff ij.2)
    (∑ ij ∈ addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g),
      (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2)
⊢ (embDomain f (x * y)).coeff ((f : (a : Γ) → Γ') g) = (embDomain f x * embDomain f y).coeff ((f : (a : Γ) → Γ') g)

Tactic:
simp only [coeff_mul, embDomain_coeff]

Premises used: HahnSeries.coeff_mul, HahnSeries.embDomain_coeff
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ
ij :
  Eq.{u_3 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g, x.coeff ij.1 * y.coeff ij.2)
    (∑
      ij ∈
        Finset.map
          (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
            (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
          (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g),
      (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2)
ij₁ :
  Eq.{u_3 + 1} (α := R)
    (∑
      ij ∈
        Finset.map
          (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
            (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
          (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g),
      (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2)
    (∑ ij ∈ addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g),
      (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2)
⊢ Eq.{u_3 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g, x.coeff ij.1 * y.coeff ij.2)
    (∑ ij ∈ addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') 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

Premises used: HahnSeries.isPWO_support, Finset.map, RelEmbedding.toEmbedding, Function.Embedding.prodMap, Finset.addAntidiagonal
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ
⊢ Eq.{u_3 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g, x.coeff ij.1 * y.coeff ij.2)
    (∑
      ij ∈
        Finset.map
          (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
            (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
          (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g),
      (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ
h :
  Finset.map
      (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
        (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
      (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g) ⊆
    addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g)
hf₁ :
  ∀ x_1 ∈ addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g),
    x_1 ∉
        Finset.map
          (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
            (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
          (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g) →
      (embDomain f x).coeff x_1.1 * (embDomain f y).coeff x_1.2 = 0
⊢ Eq.{u_3 + 1} (α := R)
    (∑
      ij ∈
        Finset.map
          (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
            (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
          (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g),
      (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2)
    (∑ ij ∈ addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g),
      (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2)

Tactic:
apply sum_subset

Premises used: Finset.sum_subset
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ
i j : Γ'
hij :
  (i, j) ∈
    Finset.map
      (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
        (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
      (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g)
⊢ ∃ (a : Γ) (b : Γ),
    (x.coeff a ≠ 0 ∧ y.coeff b ≠ 0 ∧ a + b = g) ∧
      Prod.map (⇑(f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)) : (a : Γ) → Γ')
          (⇑(f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)) : (a : Γ) → Γ') (a, b) =
        (i, j)

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

Premises used: Function.Embedding.coe_prodMap, Finset.mem_map, Prod.exists, HahnSeries.mem_support, Finset.mem_addAntidiagonal
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ
i j : Γ'
hij :
  ∃ (a : Γ) (b : Γ),
    (x.coeff a ≠ 0 ∧ y.coeff b ≠ 0 ∧ a + b = g) ∧
      Prod.map (⇑(f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)) : (a : Γ) → Γ')
          (⇑(f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)) : (a : Γ) → Γ') (a, b) =
        (i, j)
h :
  ∀ (i j : Γ) (hx : x.coeff i ≠ 0) (hy : y.coeff j ≠ 0),
    Membership.mem (α := Γ' × Γ')
      (addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') (i + j)))
      (((f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2) : (a : Γ) → Γ') i,
          (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2) : (a : Γ) → Γ') j) :
        Γ' × Γ')
⊢ (i, j) ∈ addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g)

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

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
i j : Γ
hx : x.coeff i ≠ 0
hy : y.coeff j ≠ 0
⊢ Membership.mem (α := Γ' × Γ')
    (addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') (i + j)))
    (((f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2) : (a : Γ) → Γ') i,
        (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2) : (a : Γ) → Γ') j) :
      Γ' × Γ')

Tactic:
simp [hx, hy, hf]
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ
fst snd : Γ'
h1 :
  (fst, snd) ∈ addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g)
h2 :
  (fst, snd) ∉
    Finset.map
      (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
        (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
      (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g)
hf₁ :
  ∀ (h2 : (embDomain f x).coeff (fst, snd).1 * (embDomain f y).coeff (fst, snd).2 ≠ 0),
    (fst, snd) ∈
      Finset.map
        (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
          (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
        (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g)
⊢ (embDomain f x).coeff (fst, snd).1 * (embDomain f y).coeff (fst, snd).2 = 0

Tactic:
contrapose! h2
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ
fst snd : Γ'
h1 :
  (fst, snd) ∈ addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g)
h2 : (embDomain f x).coeff (fst, snd).1 * (embDomain f y).coeff (fst, snd).2 ≠ 0
hf₁ :
  ∀ i ∈ x.support,
    ∀
      (h1 :
        Membership.mem (α := Γ' × Γ')
          (addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g))
          (((f : (a : Γ) → Γ') i, snd) : Γ' × Γ'))
      (h2 :
        (embDomain f x).coeff ((f : (a : Γ) → Γ') i, snd).1 *
            (embDomain f y).coeff (((f : (a : Γ) → Γ') i, snd) : Γ' × Γ').2 ≠
          0),
      Membership.mem (α := Γ' × Γ')
        (Finset.map
          (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
            (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
          (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g))
        (((f : (a : Γ) → Γ') i, snd) : Γ' × Γ')
⊢ (fst, snd) ∈
    Finset.map
      (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
        (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
      (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g)

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

Premises used: And.left, ne_zero_and_ne_zero_of_mul, HahnSeries.support_embDomain_subset, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ
snd : Γ'
i : Γ
left : i ∈ x.support
h1 :
  Membership.mem (α := Γ' × Γ')
    (addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g))
    (((f : (a : Γ) → Γ') i, snd) : Γ' × Γ')
h2 :
  (embDomain f x).coeff ((f : (a : Γ) → Γ') i, snd).1 *
      (embDomain f y).coeff (((f : (a : Γ) → Γ') i, snd) : Γ' × Γ').2 ≠
    0
hf₁ :
  ∀ j ∈ y.support,
    ∀
      (h1 :
        Membership.mem (α := Γ' × Γ')
          (addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g))
          (((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j) : Γ' × Γ'))
      (h2 :
        (embDomain f x).coeff ((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j).1 *
            (embDomain f y).coeff ((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j).2 ≠
          0),
      Membership.mem (α := Γ' × Γ')
        (Finset.map
          (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
            (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
          (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g))
        (((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j) : Γ' × Γ')
⊢ Membership.mem (α := Γ' × Γ')
    (Finset.map
      (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
        (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
      (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g))
    (((f : (a : Γ) → Γ') i, snd) : Γ' × Γ')

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

Premises used: And.right, ne_zero_and_ne_zero_of_mul, HahnSeries.support_embDomain_subset, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g i : Γ
left : i ∈ x.support
j : Γ
left_1 : j ∈ y.support
h1 :
  Membership.mem (α := Γ' × Γ')
    (addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g))
    (((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j) : Γ' × Γ')
h2 :
  (embDomain f x).coeff ((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j).1 *
      (embDomain f y).coeff ((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j).2 ≠
    0
hf₁ :
  ∃ (a : Γ) (b : Γ),
    (x.coeff a ≠ 0 ∧ y.coeff b ≠ 0 ∧ a + b = g) ∧
      Eq.{u_6 + 1} (α := Γ' × Γ')
        (Prod.map (⇑(f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)) : (a : Γ) → Γ')
            (⇑(f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)) : (a : Γ) → Γ')
            (a, b) :
          Γ' × Γ')
        (((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j) : Γ' × Γ')
⊢ Membership.mem (α := Γ' × Γ')
    (Finset.map
      (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2).prodMap
        (f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)))
      (addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ g))
    (((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j) : Γ' × Γ')

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

Premises used: Function.Embedding.coe_prodMap, Finset.mem_map, Prod.exists, HahnSeries.mem_support, Finset.mem_addAntidiagonal
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g i : Γ
left : i ∈ x.support
j : Γ
left_1 : j ∈ y.support
h1 :
  Membership.mem (α := Γ' × Γ')
    (addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g))
    (((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j) : Γ' × Γ')
h2 :
  (embDomain f x).coeff ((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j).1 *
      (embDomain f y).coeff ((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j).2 ≠
    0
⊢ x.coeff i ≠ 0 ∧ y.coeff j ≠ 0 ∧ i + j = g

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

Premises used: HahnSeries.embDomain_coeff, HahnSeries.mem_support, Finset.mem_addAntidiagonal, OrderEmbedding.eq_iff_eq
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g i : Γ
left : i ∈ x.support
j : Γ
left_1 : j ∈ y.support
h2 :
  (embDomain f x).coeff ((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j).1 *
      (embDomain f y).coeff ((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') 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) ∧
      Eq.{u_6 + 1} (α := Γ' × Γ')
        (Prod.map (⇑(f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)) : (a : Γ) → Γ')
            (⇑(f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)) : (a : Γ) → Γ')
            (a, b) :
          Γ' × Γ')
        (((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j) : Γ' × Γ')

Tactic:
⟨i, j, h1, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g i : Γ
left : i ∈ x.support
j : Γ
left_1 : j ∈ y.support
h2 :
  (embDomain f x).coeff ((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j).1 *
      (embDomain f y).coeff ((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') 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) ∧
      Eq.{u_6 + 1} (α := Γ' × Γ')
        (Prod.map (⇑(f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)) : (a : Γ) → Γ')
            (⇑(f.toEmbedding (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)) : (a : Γ) → Γ')
            (a, b) :
          Γ' × Γ')
        (((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j) : Γ' × Γ')

Tactic:
exact ⟨i, j, h1, rfl⟩
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')
neg : (embDomain f x * embDomain f y).coeff g = 0
⊢ (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g

Tactic:
rw [embDomain_notin_range hg, eq_comm]

Premises used: HahnSeries.embDomain_notin_range, eq_comm
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst_3 : AddCommMonoid Γ'
inst_4 : PartialOrder Γ'
inst_5 : IsOrderedCancelAddMonoid Γ'
inst_6 : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf :
  ∀ (x y : Γ),
    (f : (a : Γ) → Γ') (x + y) = HAdd.hAdd (α := Γ') (β := Γ') ((f : (a : Γ) → Γ') x : Γ') ((f : (a : Γ) → Γ') y : Γ')
x y : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')
neg :
  ∀ (hg : (embDomain f x * embDomain f y).coeff g ≠ 0),
    Membership.mem (γ := Set Γ') (Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g
⊢ (embDomain f x * embDomain f y).coeff g = 0

Tactic:
contrapose! hg