awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : Zero R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.support ⊆ s
b : Γ × Γ'
hb :
  (b.1 ∈ s ∧
      Ne.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) 0 ∧ b.1 +ᵥ b.2 = a) ∧
    (Ne.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) 0 ∧ b.1 +ᵥ b.2 = a →
      x.coeff b.1 = 0)
rw :
  HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) 0
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) =
    0
rw₁ rw₂ : Eq.{u_5 + 1} (α := V) 0 0
⊢ HSMul.hSMul (β := V) (x.coeff b.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) = 0

Tactic:
rw [hb.2 ⟨hb.1.2.1, hb.1.2.2⟩, zero_smul]

Premises used: zero_smul, And.right, And.left, And.intro
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : Zero R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.support ⊆ s
rw rw₁ rw₂ :
  Eq.{u_5 + 1} (α := V)
    (∑
      ij ∈
        VAddAntidiagonal (s := x.support) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a ⋯,
      HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ij.2))
    (∑
      ij ∈
        VAddAntidiagonal (s := s) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a ⋯,
      HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ij.2))
rw₃ rw₄ :
  ∀ (b : Γ × Γ')
    (hb :
      b ∈
        VAddAntidiagonal (s := s) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a ⋯ \
          VAddAntidiagonal (s := x.support) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a ⋯),
    HSMul.hSMul (β := V) (x.coeff b.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) = 0
rw₅ :
  ∀ (b : Γ × Γ')
    (hb :
      (b.1 ∈ s ∧
          Ne.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) 0 ∧
            b.1 +ᵥ b.2 = a) ∧
        (Ne.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) 0 ∧
            b.1 +ᵥ b.2 = a →
          x.coeff b.1 = 0)),
    HSMul.hSMul (β := V) (x.coeff b.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) = 0
⊢ Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y)) a)
    (∑
      ij ∈
        VAddAntidiagonal (s := s) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a ⋯,
      HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ij.2))

Tactic:
classical
  rw [coeff_smul]
  apply sum_subset_zero_on_sdiff (vaddAntidiagonal_mono_left _ hxs _ _) _ fun _ _ => rfl
  intro b hb
  simp only [not_and', mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_ne_iff] at hb
  rw [hb.2 ⟨hb.1.2.1, hb.1.2.2⟩, zero_smul]

Premises used: Finset.vaddAntidiagonal_mono_left, Finset.mem_vaddAntidiagonal, not_ne_iff, Finset.mem_sdiff, HahnModule.coeff_smul, zero_smul, not_and', rfl, HahnSeries.mem_support, Finset.sum_subset_zero_on_sdiff
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : AddCommMonoid R
inst_6 : SMulWithZero R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
h₁ :
  ∀ (a : Γ'),
    Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) ((x + y) • z)) a)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • z + y • z)) a)
⊢ (x + y) • z = x • z + y • z

Tactic:
ext a
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : AddCommMonoid R
inst_6 : SMulWithZero R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
⊢ (x.support ∪ y.support).IsPWO

Tactic:
have hwf := x.isPWO_support.union y.isPWO_support
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : AddCommMonoid R
inst_6 : SMulWithZero R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
h₁ :
  ∑
      ij ∈
        VAddAntidiagonal (s := x.support ∪ y.support) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a ⋯,
      HSMul.hSMul (β := V) ((x.coeff + y.coeff) ij.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) ij.2) =
    (HAdd.hAdd (α := V⟦Γ'⟧) (β := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • z) : V⟦Γ'⟧)
          ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (y • z) : V⟦Γ'⟧)).coeff
      a
h₂ : (x + y).support ⊆ x.support ∪ y.support
⊢ Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) ((x + y) • z)) a)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • z + y • z)) a)

Tactic:
rw [coeff_smul_left hwf, HahnSeries.coeff_add', of_symm_add]

Premises used: HahnModule.of_symm_add, HahnModule.coeff_smul_left, HahnSeries.coeff_add'
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : AddCommMonoid R
inst_6 : SMulWithZero R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
h₁ :
  ∑
      x_1 ∈
        VAddAntidiagonal (s := x.support ∪ y.support) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a ⋯,
      (HSMul.hSMul (β := V) (x.coeff x_1.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) x_1.2) +
        HSMul.hSMul (β := V) (y.coeff x_1.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) x_1.2)) =
    HAdd.hAdd (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • z)) a)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (y • z)) a)
⊢ ∑
      ij ∈
        VAddAntidiagonal (s := x.support ∪ y.support) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a ⋯,
      HSMul.hSMul (β := V) ((x.coeff + y.coeff) ij.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) ij.2) =
    (HAdd.hAdd (α := V⟦Γ'⟧) (β := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • z) : V⟦Γ'⟧)
          ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (y • z) : V⟦Γ'⟧)).coeff
      a

Tactic:
simp_all only [Pi.add_apply, HahnSeries.coeff_add']

Premises used: Pi.add_apply, HahnSeries.coeff_add'
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : AddCommMonoid R
inst_6 : SMulWithZero R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
h₁ :
  ∑
      x_1 ∈
        VAddAntidiagonal (s := x.support ∪ y.support) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a ⋯,
      (HSMul.hSMul (β := V) (x.coeff x_1.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) x_1.2) +
        HSMul.hSMul (β := V) (y.coeff x_1.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) x_1.2)) =
    HAdd.hAdd (α := V)
      (∑
        ij ∈
          VAddAntidiagonal (s := x.support ∪ y.support) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a ⋯,
        HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) ij.2))
      (∑
        ij ∈
          VAddAntidiagonal (s := x.support ∪ y.support) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a ⋯,
        HSMul.hSMul (β := V) (y.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) ij.2))
⊢ ∑
      x_1 ∈
        VAddAntidiagonal (s := x.support ∪ y.support) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a ⋯,
      (HSMul.hSMul (β := V) (x.coeff x_1.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) x_1.2) +
        HSMul.hSMul (β := V) (y.coeff x_1.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) x_1.2)) =
    HAdd.hAdd (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • z)) a)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (y • z)) a)

Tactic:
rw [coeff_smul_left hwf Set.subset_union_right,
      coeff_smul_left hwf Set.subset_union_left]

Premises used: Set.subset_union_right, Set.subset_union_left, HahnModule.coeff_smul_left
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : AddCommMonoid R
inst_6 : SMulWithZero R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ ∑
      x_1 ∈
        VAddAntidiagonal (s := x.support ∪ y.support) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a ⋯,
      (HSMul.hSMul (β := V) (x.coeff x_1.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) x_1.2) +
        HSMul.hSMul (β := V) (y.coeff x_1.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) x_1.2)) =
    HAdd.hAdd (α := V)
      (∑
        ij ∈
          VAddAntidiagonal (s := x.support ∪ y.support) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a ⋯,
        HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) ij.2))
      (∑
        ij ∈
          VAddAntidiagonal (s := x.support ∪ y.support) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a ⋯,
        HSMul.hSMul (β := V) (y.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) ij.2))

Tactic:
simp only [sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : AddCommMonoid R
inst_6 : SMulWithZero R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ (x + y).support ⊆ x.support ∪ y.support

Tactic:
support_add_subset _ _

Premises used: HahnSeries.support_add_subset
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : AddCommMonoid R
inst_6 : SMulWithZero R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ (x + y).support ⊆ x.support ∪ y.support

Tactic:
exact support_add_subset _ _

Premises used: HahnSeries.support_add_subset
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
pos :
  ∀ (hr : r = 0),
    coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
          (HSMul.hSMul (α := R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
        (b +ᵥ a) =
      HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
neg :
  ∀ (hr : ¬r = 0),
    coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
          (HSMul.hSMul (α := R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
        (b +ᵥ a) =
      HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
⊢ coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      (b +ᵥ a) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : r = 0
⊢ coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      (b +ᵥ a) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)

Tactic:
simp_all only [map_zero, zero_smul, coeff_smul, HahnSeries.support_zero, HahnSeries.coeff_zero,
    sum_const_zero]

Premises used: map_zero, Finset.sum_const_zero, HahnModule.coeff_smul, zero_smul, HahnSeries.coeff_zero, HahnSeries.support_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
neg :
  ∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
⊢ coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      (b +ᵥ a) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)

Tactic:
simp only [hr, coeff_smul, coeff_smul, HahnSeries.support_single_of_ne, ne_eq, not_false_iff]

Premises used: ne_eq, HahnModule.coeff_smul, HahnSeries.support_single_of_ne, not_false_iff
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
pos :
  ∀ (hx : Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0),
    ∑
        x_1 ∈
          VAddAntidiagonal (s := {b}) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a)
            ⋯,
        HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
          (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
      HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
neg :
  ∀ (hx : ¬Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0),
    ∑
        x_1 ∈
          VAddAntidiagonal (s := {b}) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a)
            ⋯,
        HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
          (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
      HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
⊢ ∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)

Tactic:
by_cases hx : ((of R).symm x).coeff a = 0

Premises used: HahnModule.of, HahnSeries.coeff, Equiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
pos :
  Eq.{u_5 + 1} (α := V)
    (∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2))
    0
⊢ ∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)

Tactic:
simp only [hx, smul_zero]

Premises used: smul_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
rw :
  Eq (α := Finset (Γ × Γ'))
    (VAddAntidiagonal (s := {b}) (t :=
      HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯)
    ∅
⊢ Eq.{u_5 + 1} (α := V)
    (∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2))
    0

Tactic:
rw [sum_congr _ fun _ _ => rfl, sum_empty]

Premises used: Finset.sum_empty, Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
h :
  ∀ (a1 : Γ) (a2 : Γ'),
    Membership.mem (γ := Finset (Γ × Γ'))
        (VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯)
        (a1, a2) ↔
      Membership.mem (γ := Finset (Γ × Γ')) ∅ (a1, a2)
⊢ Eq (α := Finset (Γ × Γ'))
    (VAddAntidiagonal (s := {b}) (t :=
      HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯)
    ∅

Tactic:
ext ⟨a1, a2⟩
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
a1 : Γ
a2 : Γ'
h :
  a1 = b →
    Membership.mem (γ := Set Γ')
        (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a2 →
      ¬a1 +ᵥ a2 = b +ᵥ a
⊢ Membership.mem (γ := Finset (Γ × Γ'))
      (VAddAntidiagonal (s := {b}) (t :=
        HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯)
      (a1, a2) ↔
    Membership.mem (γ := Finset (Γ × Γ')) ∅ (a1, a2)

Tactic:
simp only [notMem_empty, not_and, Set.mem_singleton_iff,
      mem_vaddAntidiagonal, iff_false]

Premises used: iff_false, Finset.mem_vaddAntidiagonal, Finset.notMem_empty, Set.mem_singleton_iff, not_and
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
hr : ¬r = 0
hx : Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
a1 : Γ
a2 : Γ'
h2 :
  Membership.mem (γ := Set Γ')
    (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a2
h1 : a1 +ᵥ a2 = a1 +ᵥ a
⊢ Membership.mem (γ := Set Γ')
    (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a

Tactic:
rw [IsCancelVAdd.left_cancel a1 a2 a h1] at h2

Premises used: IsCancelVAdd.left_cancel