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 : 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
h2₁ :
  Membership.mem (γ := Set Γ')
    (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a
⊢ a1 +ᵥ a2 = a1 +ᵥ a

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

Premises used: IsCancelVAdd.left_cancel
-- 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)) a
h1 : a1 +ᵥ a2 = a1 +ᵥ a
⊢ False

Tactic:
h2 hx
-- 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)) a
h1 : a1 +ᵥ a2 = a1 +ᵥ a
⊢ False

Tactic:
exact h2 hx
-- 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
trans :
  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))
    (∑ ij ∈ {(b, a)},
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) ij.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) ij.2))
trans₁ :
  ∑ ij ∈ {(b, a)},
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) ij.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) ij.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:
trans ∑ ij ∈ {(b, a)},
    (HahnSeries.single b r).coeff ij.fst • ((of R).symm x).coeff ij.snd

Premises used: Prod.mk
-- 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
apply :
  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) ⋯)
    {(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))
    (∑ ij ∈ {(b, a)},
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) ij.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) ij.2))

Tactic:
apply sum_congr _ fun _ _ => rfl

Premises used: 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 (Γ × Γ')) {(b, a)} (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) ⋯)
    {(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 ↔
    a1 = b ∧ a2 = 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 (Γ × Γ')) {(b, a)} (a1, a2)

Tactic:
simp only [Set.mem_singleton_iff, Prod.mk_inj, mem_vaddAntidiagonal, mem_singleton]

Premises used: Finset.mem_singleton, Finset.mem_vaddAntidiagonal, Prod.mk_inj, Set.mem_singleton_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
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 →
    a1 = b ∧ a2 = a
h₁ :
  a1 = b ∧ a2 = a →
    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
⊢ 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 ↔
    a1 = b ∧ a2 = a

Tactic:
constructor
-- 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 : Γ'
left :
  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
⊢ a1 = a1 ∧ a2 = a

Tactic:
⟨rfl, IsCancelVAdd.left_cancel a1 a2 a h1⟩

Premises used: IsCancelVAdd.left_cancel, And.intro, 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 : Γ'
hr : ¬r = 0
hx : ¬Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
a1 : Γ
a2 : Γ'
left :
  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
⊢ a1 = a1 ∧ a2 = a

Tactic:
exact ⟨rfl, IsCancelVAdd.left_cancel a1 a2 a h1⟩
-- 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
hr : ¬r = 0
a1 : Γ
a2 : Γ'
hx : ¬Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a2) 0
⊢ Membership.mem (γ := Set Γ')
    (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a2

Tactic:
hx

Premises used: HahnSeries.support, Set.Mem, setOf, Function.support, Not
-- 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
hr : ¬r = 0
a1 : Γ
a2 : Γ'
hx : ¬Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a2) 0
⊢ Membership.mem (γ := Set Γ')
    (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a2

Tactic:
exact hx
-- 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
hr : ¬r = 0
a1 : Γ
a2 : Γ'
hx : ¬Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a2) 0
⊢ a1 = a1 ∧
    Membership.mem (γ := Set Γ')
        (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a2 ∧
      a1 +ᵥ a2 = a1 +ᵥ a2

Tactic:
exact ⟨rfl, by exact hx, 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
⊢ ∑ ij ∈ {(b, a)},
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) ij.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) ij.2) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ'
inst_1 : AddCommMonoid V
Γ : Type u_6
inst_2 : AddCommMonoid Γ
inst_3 : PartialOrder Γ
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : MulZeroClass R
inst_7 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
nth_rw :
  coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      (HVAdd.hVAdd.{u_6, u_2, u_2} (α := Γ) 0 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 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      a =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)

Tactic:
nth_rw 1 [← zero_vadd Γ a]

Premises used: zero_vadd
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ'
inst_1 : AddCommMonoid V
Γ : Type u_6
inst_2 : AddCommMonoid Γ
inst_3 : PartialOrder Γ
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : MulZeroClass R
inst_7 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
⊢ coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      (HVAdd.hVAdd.{u_6, u_2, u_2} (α := Γ) 0 a) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)

Tactic:
coeff_single_smul_vadd

Premises used: HahnModule.coeff_single_smul_vadd
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ'
inst_1 : AddCommMonoid V
Γ : Type u_6
inst_2 : AddCommMonoid Γ
inst_3 : PartialOrder Γ
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : MulZeroClass R
inst_7 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
⊢ coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      (HVAdd.hVAdd.{u_6, u_2, u_2} (α := Γ) 0 a) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)

Tactic:
exact coeff_single_smul_vadd

Premises used: HahnModule.coeff_single_smul_vadd
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ'
inst_1 : AddCommMonoid V
Γ : Type u_6
inst_2 : AddCommMonoid Γ
inst_3 : PartialOrder Γ
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : MulZeroClass R
inst_7 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
h :
  ∀ (x_1 : Γ'),
    Eq.{u_5 + 1} (α := V)
      (coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
          (HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
        x_1)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (r • x)) x_1)
⊢ HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x = r • x

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ'
inst_1 : AddCommMonoid V
Γ : Type u_6
inst_2 : AddCommMonoid Γ
inst_3 : PartialOrder Γ
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : MulZeroClass R
inst_7 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
x_1 : Γ'
⊢ Eq.{u_5 + 1} (α := V)
    (coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      x_1)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (r • x)) x_1)

Tactic:
coeff_single_zero_smul

Premises used: HahnModule.coeff_single_zero_smul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ'
inst_1 : AddCommMonoid V
Γ : Type u_6
inst_2 : AddCommMonoid Γ
inst_3 : PartialOrder Γ
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : MulZeroClass R
inst_7 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
x_1 : Γ'
⊢ Eq.{u_5 + 1} (α := V)
    (coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      x_1)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (r • x)) x_1)

Tactic:
exact coeff_single_zero_smul

Premises used: HahnModule.coeff_single_zero_smul
-- 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 : HahnModule Γ' R V
h :
  ∀ (x_1 : Γ'),
    Eq.{u_5 + 1} (α := V)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (HSMul.hSMul (α := R⟦Γ⟧) 0 x)) x_1)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) 0) x_1)
⊢ HSMul.hSMul (α := R⟦Γ⟧) 0 x = 0

Tactic:
ext
-- 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 : HahnModule Γ' R V
x_1 : Γ'
⊢ Eq.{u_5 + 1} (α := V)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (HSMul.hSMul (α := R⟦Γ⟧) 0 x)) x_1)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) 0) x_1)

Tactic:
simp [coeff_smul]

Premises used: HahnModule.coeff_smul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ'
inst_1 : AddCommMonoid V
Γ : Type u_6
inst_2 : AddCommMonoid Γ
inst_3 : PartialOrder Γ
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : MonoidWithZero R
inst_7 : MulActionWithZero R V
x : HahnModule Γ' R V
h :
  ∀ (g : Γ'),
    Eq.{u_5 + 1} (α := V)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (HSMul.hSMul (α := R⟦Γ⟧) 1 x)) g)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) g)
⊢ HSMul.hSMul (α := R⟦Γ⟧) 1 x = x

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ'
inst_1 : AddCommMonoid V
Γ : Type u_6
inst_2 : AddCommMonoid Γ
inst_3 : PartialOrder Γ
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : MonoidWithZero R
inst_7 : MulActionWithZero R V
x : HahnModule Γ' R V
g : Γ'
⊢ Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (HSMul.hSMul (α := R⟦Γ⟧) 1 x)) g)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) g)

Tactic:
coeff_single_zero_smul.trans (one_smul R (x.coeff g))

Premises used: one_smul, HahnModule.coeff_single_zero_smul, HahnSeries.coeff, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ'
inst_1 : AddCommMonoid V
Γ : Type u_6
inst_2 : AddCommMonoid Γ
inst_3 : PartialOrder Γ
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : MonoidWithZero R
inst_7 : MulActionWithZero R V
x : HahnModule Γ' R V
g : Γ'
⊢ Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (HSMul.hSMul (α := R⟦Γ⟧) 1 x)) g)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) g)

Tactic:
exact coeff_single_zero_smul.trans (one_smul R (x.coeff g))

Premises used: one_smul, HahnModule.coeff_single_zero_smul, HahnSeries.coeff, Eq.trans
-- 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
x : R⟦Γ⟧
y : HahnModule Γ' R V
⊢ HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y)) ⊆
    HVAdd.hVAdd (β := Set Γ') x.support
      (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y))

Tactic:
Set.Subset.trans (fun x hx => ?_) (support_vaddAntidiagonal_subset_vadd
    fun a ↦ Set.VAddAntidiagonal.finite_of_isPWO x.isPWO_support ((of R).symm y).isPWO_support a)

Premises used: HahnSeries.isPWO_support, Finset.support_vaddAntidiagonal_subset_vadd, Set.Subset.trans, Set.VAddAntidiagonal.finite_of_isPWO, HahnModule.of, 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
x : R⟦Γ⟧
y : HahnModule Γ' R V
refine :
  ∀ (x_1 : Γ')
    (hx :
      Membership.mem (γ := Set Γ')
        (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))) x_1),
    Membership.mem (γ := Set Γ')
      {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
            ⋯).Nonempty}
      x_1
⊢ HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y)) ⊆
    HVAdd.hVAdd (β := Set Γ') x.support
      (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y))

Tactic:
refine Set.Subset.trans (fun x hx => ?_) (support_vaddAntidiagonal_subset_vadd
    fun a ↦ Set.VAddAntidiagonal.finite_of_isPWO x.isPWO_support ((of R).symm y).isPWO_support a)

Premises used: HahnSeries.isPWO_support, Finset.support_vaddAntidiagonal_subset_vadd, Set.Subset.trans, Set.VAddAntidiagonal.finite_of_isPWO, HahnModule.of, 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
x_1 : R⟦Γ⟧
y : HahnModule Γ' R V
x : Γ'
hx :
  Membership.mem (γ := Set Γ')
    (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x_1 • y))) x
contrapose! :
  ∀
    (hx :
      VAddAntidiagonal (s := x_1.support) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) x ⋯ =
        ∅),
    x ∉ HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x_1 • y))
⊢ (VAddAntidiagonal (s := x_1.support) (t :=
      HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) x ⋯).Nonempty

Tactic:
contrapose! hx
-- 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
x_1 : R⟦Γ⟧
y : HahnModule Γ' R V
x : Γ'
hx :
  VAddAntidiagonal (s := x_1.support) (t :=
      HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) x ⋯ =
    ∅
⊢ x ∉ HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x_1 • y))

Tactic:
simp [coeff_smul, hx]

Premises used: HahnModule.coeff_smul