awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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⟦Γ⟧
⊢ embDomain f (x * y) = embDomain f x * embDomain f y
have coeff : ∀ (g : Γ'), (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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 : Γ'
⊢ (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g
have pos : ∀ (hg : Membership.mem (γ := Set Γ') (Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g),
  (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g
Tactic: by_cases hg : g ∈ Set.range f
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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 :
  ∀ (hg : Membership.mem (γ := Set Γ') (Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) g),
    (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g
⊢ (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g
have neg : ∀ (hg : g ∉ Set.range.{u_6, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')),
  (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g
Tactic: by_cases hg : g ∈ Set.range f
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g
have pos : ∀ (g : Γ),
  (embDomain f (x * y)).coeff ((f : (a : Γ) → Γ') g) = (embDomain f x * embDomain f y).coeff ((f : (a : Γ) → Γ') g)
Tactic: obtain ⟨g, rfl⟩ := hg
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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 : Γ
⊢ (embDomain f (x * y)).coeff ((f : (a : Γ) → Γ') g) = (embDomain f x * embDomain f y).coeff ((f : (a : Γ) → Γ') g)
have pos : Eq.{u_3 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := x.support) (t := y.support) sorry sorry g, x.coeff ij.1 * y.coeff ij.2)
  (∑ ij ∈ addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) sorry sorry ((f : (a : Γ) → Γ') g),
    (embDomain f x).coeff ij.1 * (embDomain f y).coeff ij.2)
Tactic: simp only [coeff_mul, embDomain_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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 ∈ 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)
have ij : Eq.{u_3 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := x.support) (t := y.support) sorry sorry 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) sorry sorry 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
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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)
⊢ 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)
have 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) sorry sorry 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) sorry sorry ((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
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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 ∈
        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)
have 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) sorry sorry g) ⊆
  addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) sorry sorry ((f : (a : Γ) → Γ') g)
Tactic: apply sum_subset
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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)
⊢ 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)
have hf₁ : ∀ x_1 ∈ addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) sorry sorry ((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) sorry sorry g) →
    (embDomain f x).coeff x_1.1 * (embDomain f y).coeff x_1.2 = 0
Tactic: apply sum_subset
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
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)
⊢ (i, j) ∈ addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g)
have 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)
Tactic: simp only [mem_map, mem_addAntidiagonal,
        Function.Embedding.coe_prodMap, mem_support, Prod.exists] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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)
⊢ (i, j) ∈ addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) ⋯ ⋯ ((f : (a : Γ) → Γ') g)
have 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) sorry sorry ((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: obtain ⟨i, j, ⟨hx, hy, rfl⟩, rfl, rfl⟩ := hij
Cleared hypotheses: g, i, j, hij
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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)
⊢ (embDomain f x).coeff (fst, snd).1 * (embDomain f y).coeff (fst, snd).2 = 0
have 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) sorry sorry g)
Tactic: contrapose! h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ (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)
have hf₁ : ∀ i ∈ x.support,
  ∀
    (h1 :
      Membership.mem (α := Γ' × Γ')
        (addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) sorry sorry ((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) sorry sorry g))
      (((f : (a : Γ) → Γ') i, snd) : Γ' × Γ')
Tactic: obtain ⟨i, _, rfl⟩ := support_embDomain_subset (ne_zero_and_ne_zero_of_mul h2).1
Cleared hypotheses: fst, h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ 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) : Γ' × Γ')
have hf₁ : ∀ j ∈ y.support,
  ∀
    (h1 :
      Membership.mem (α := Γ' × Γ')
        (addAntidiagonal (s := (embDomain f x).support) (t := (embDomain f y).support) sorry sorry ((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) sorry sorry g))
      (((f : (a : Γ) → Γ') i, (f : (a : Γ) → Γ') j) : Γ' × Γ')
Tactic: obtain ⟨j, _, rfl⟩ := support_embDomain_subset (ne_zero_and_ne_zero_of_mul h2).2
Cleared hypotheses: snd, h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ 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) : Γ' × Γ')
have 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) : Γ' × Γ')
Tactic: simp only [mem_map, mem_addAntidiagonal,
        Function.Embedding.coe_prodMap, mem_support, Prod.exists]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
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
⊢ ∃ (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) : Γ' × Γ')
have h1₁ : 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
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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 : Γ) → Γ')
⊢ (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g
have neg : (embDomain f x * embDomain f y).coeff g = 0
Tactic: rw [embDomain_notin_range hg, eq_comm]