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
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:
support_smul_subset_vadd_support'

Premises used: HahnModule.support_smul_subset_vadd_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 : 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:
exact support_smul_subset_vadd_support'

Premises used: HahnModule.support_smul_subset_vadd_support'
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst_1 : LinearOrder Γ
inst_2 : LinearOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
inst_7 : VAdd.{u_6, u_7} (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), (↑(γ +ᵥ γ') : WithTop Γ') = (↑γ : WithTop Γ) +ᵥ (↑γ' : WithTop Γ')
pos :
  ∀ (hx : x = 0),
    HVAdd.hVAdd (β := WithTop Γ') x.orderTop
        (orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) ≤
      orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))
neg :
  ∀ (hx : ¬x = 0),
    HVAdd.hVAdd (β := WithTop Γ') x.orderTop
        (orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) ≤
      orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))
⊢ HVAdd.hVAdd (β := WithTop Γ') x.orderTop
      (orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) ≤
    orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst_1 : LinearOrder Γ
inst_2 : LinearOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
inst_7 : VAdd.{u_6, u_7} (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), (↑(γ +ᵥ γ') : WithTop Γ') = (↑γ : WithTop Γ) +ᵥ (↑γ' : WithTop Γ')
hx : x = 0
⊢ HVAdd.hVAdd (β := WithTop Γ') x.orderTop
      (orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) ≤
    orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))

Tactic:
simp_all
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst_1 : LinearOrder Γ
inst_2 : LinearOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
inst_7 : VAdd.{u_6, u_7} (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), (↑(γ +ᵥ γ') : WithTop Γ') = (↑γ : WithTop Γ) +ᵥ (↑γ' : WithTop Γ')
hx : ¬x = 0
pos :
  ∀ (hy : y = 0),
    HVAdd.hVAdd (β := WithTop Γ') x.orderTop
        (orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) ≤
      orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))
neg :
  ∀ (hy : ¬y = 0),
    HVAdd.hVAdd (β := WithTop Γ') x.orderTop
        (orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) ≤
      orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))
⊢ HVAdd.hVAdd (β := WithTop Γ') x.orderTop
      (orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) ≤
    orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst_1 : LinearOrder Γ
inst_2 : LinearOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
inst_7 : VAdd.{u_6, u_7} (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), (↑(γ +ᵥ γ') : WithTop Γ') = (↑γ : WithTop Γ) +ᵥ (↑γ' : WithTop Γ')
hx : ¬x = 0
hy : y = 0
⊢ HVAdd.hVAdd (β := WithTop Γ') x.orderTop
      (orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) ≤
    orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))

Tactic:
simp_all
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst_1 : LinearOrder Γ
inst_2 : LinearOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
inst_7 : VAdd.{u_6, u_7} (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), (↑(γ +ᵥ γ') : WithTop Γ') = (↑γ : WithTop Γ) +ᵥ (↑γ' : WithTop Γ')
hx : ¬x = 0
hy : ¬y = 0
⊢ Ne (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y : V⟦Γ'⟧) (0 : V⟦Γ'⟧)

Tactic:
have hhy : ((of R).symm y) ≠ 0 := hy
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst_1 : LinearOrder Γ
inst_2 : LinearOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
inst_7 : VAdd.{u_6, u_7} (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), (↑(γ +ᵥ γ') : WithTop Γ') = (↑γ : WithTop Γ) +ᵥ (↑γ' : WithTop Γ')
hx : ¬x = 0
hy : ¬y = 0
hhy : Ne (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
neg :
  (↑(Set.IsWF.min (s :=
          HVAdd.hVAdd (β := Set Γ') x.support
            (HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)))
          ⋯ ⋯) :
      WithTop Γ') ≤
    orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))
⊢ HVAdd.hVAdd (β := WithTop Γ') x.orderTop
      (orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) ≤
    orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))

Tactic:
rw [HahnSeries.orderTop_of_ne_zero hx, HahnSeries.orderTop_of_ne_zero hhy, ← h,
      ← Set.IsWF.min_vadd]

Premises used: HahnSeries.orderTop_of_ne_zero, Set.IsWF.min_vadd
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst_1 : LinearOrder Γ
inst_2 : LinearOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
inst_7 : VAdd.{u_6, u_7} (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), (↑(γ +ᵥ γ') : WithTop Γ') = (↑γ : WithTop Γ) +ᵥ (↑γ' : WithTop Γ')
hx : ¬x = 0
hy : ¬y = 0
hhy : Ne (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
pos :
  ∀ (hxy : Eq (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y) : V⟦Γ'⟧) (0 : V⟦Γ'⟧)),
    (↑(Set.IsWF.min (s :=
            HVAdd.hVAdd (β := Set Γ') x.support
              (HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)))
            ⋯ ⋯) :
        WithTop Γ') ≤
      orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))
neg :
  ∀ (hxy : ¬Eq (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y) : V⟦Γ'⟧) (0 : V⟦Γ'⟧)),
    (↑(Set.IsWF.min (s :=
            HVAdd.hVAdd (β := Set Γ') x.support
              (HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)))
            ⋯ ⋯) :
        WithTop Γ') ≤
      orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))
⊢ (↑(Set.IsWF.min (s :=
          HVAdd.hVAdd (β := Set Γ') x.support
            (HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)))
          ⋯ ⋯) :
      WithTop Γ') ≤
    orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))

Tactic:
by_cases hxy : (of R).symm (x • y) = 0

Premises used: HahnModule.of, HSMul.hSMul, Equiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst_1 : LinearOrder Γ
inst_2 : LinearOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
inst_7 : VAdd.{u_6, u_7} (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), (↑(γ +ᵥ γ') : WithTop Γ') = (↑γ : WithTop Γ) +ᵥ (↑γ' : WithTop Γ')
hx : ¬x = 0
hy : ¬y = 0
hhy : Ne (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
hxy : Eq (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y) : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
pos :
  (↑(Set.IsWF.min (s :=
          HVAdd.hVAdd (β := Set Γ') x.support
            (HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)))
          ⋯ ⋯) :
      WithTop Γ') ≤
    ⊤
⊢ (↑(Set.IsWF.min (s :=
          HVAdd.hVAdd (β := Set Γ') x.support
            (HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)))
          ⋯ ⋯) :
      WithTop Γ') ≤
    orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))

Tactic:
rw [hxy, HahnSeries.orderTop_zero]

Premises used: HahnSeries.orderTop_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst_1 : LinearOrder Γ
inst_2 : LinearOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
inst_7 : VAdd.{u_6, u_7} (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), (↑(γ +ᵥ γ') : WithTop Γ') = (↑γ : WithTop Γ) +ᵥ (↑γ' : WithTop Γ')
hx : ¬x = 0
hy : ¬y = 0
hhy : Ne (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
hxy : Eq (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y) : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
⊢ (↑(Set.IsWF.min (s :=
          HVAdd.hVAdd (β := Set Γ') x.support
            (HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)))
          ⋯ ⋯) :
      WithTop Γ') ≤
    ⊤

Tactic:
OrderTop.le_top (α := WithTop Γ') _

Premises used: OrderTop.le_top
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst_1 : LinearOrder Γ
inst_2 : LinearOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
inst_7 : VAdd.{u_6, u_7} (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), (↑(γ +ᵥ γ') : WithTop Γ') = (↑γ : WithTop Γ) +ᵥ (↑γ' : WithTop Γ')
hx : ¬x = 0
hy : ¬y = 0
hhy : Ne (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
hxy : Eq (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y) : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
⊢ (↑(Set.IsWF.min (s :=
          HVAdd.hVAdd (β := Set Γ') x.support
            (HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)))
          ⋯ ⋯) :
      WithTop Γ') ≤
    ⊤

Tactic:
exact OrderTop.le_top (α := WithTop Γ') _

Premises used: OrderTop.le_top
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst_1 : LinearOrder Γ
inst_2 : LinearOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
inst_7 : VAdd.{u_6, u_7} (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), (↑(γ +ᵥ γ') : WithTop Γ') = (↑γ : WithTop Γ) +ᵥ (↑γ' : WithTop Γ')
hx : ¬x = 0
hy : ¬y = 0
hhy : Ne (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
hxy : ¬Eq (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y) : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
neg :
  Set.IsWF.min (s :=
      HVAdd.hVAdd (β := Set Γ') x.support
        (HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)))
      ⋯ ⋯ ≤
    Set.IsWF.min (s :=
      HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))) ⋯ ⋯
⊢ (↑(Set.IsWF.min (s :=
          HVAdd.hVAdd (β := Set Γ') x.support
            (HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)))
          ⋯ ⋯) :
      WithTop Γ') ≤
    orderTop.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))

Tactic:
rw [HahnSeries.orderTop_of_ne_zero hxy, WithTop.coe_le_coe]

Premises used: HahnSeries.orderTop_of_ne_zero, WithTop.coe_le_coe
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst_1 : LinearOrder Γ
inst_2 : LinearOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
inst_7 : VAdd.{u_6, u_7} (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), (↑(γ +ᵥ γ') : WithTop Γ') = (↑γ : WithTop Γ) +ᵥ (↑γ' : WithTop Γ')
hx : ¬x = 0
hy : ¬y = 0
hhy : Ne (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
hxy : ¬Eq (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y) : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
⊢ Set.IsWF.min (s :=
      HVAdd.hVAdd (β := Set Γ') x.support
        (HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)))
      ⋯ ⋯ ≤
    Set.IsWF.min (s :=
      HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))) ⋯ ⋯

Tactic:
Set.IsWF.min_le_min_of_subset support_smul_subset_vadd_support

Premises used: Set.IsWF.min_le_min_of_subset, HahnModule.support_smul_subset_vadd_support
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst_1 : LinearOrder Γ
inst_2 : LinearOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
inst_7 : VAdd.{u_6, u_7} (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), (↑(γ +ᵥ γ') : WithTop Γ') = (↑γ : WithTop Γ) +ᵥ (↑γ' : WithTop Γ')
hx : ¬x = 0
hy : ¬y = 0
hhy : Ne (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
hxy : ¬Eq (α := V⟦Γ'⟧) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y) : V⟦Γ'⟧) (0 : V⟦Γ'⟧)
⊢ Set.IsWF.min (s :=
      HVAdd.hVAdd (β := Set Γ') x.support
        (HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)))
      ⋯ ⋯ ≤
    Set.IsWF.min (s :=
      HahnSeries.support.{u_7, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))) ⋯ ⋯

Tactic:
exact Set.IsWF.min_le_min_of_subset support_smul_subset_vadd_support

Premises used: Set.IsWF.min_le_min_of_subset, HahnModule.support_smul_subset_vadd_support
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
inst_1 : AddCommMonoid Γ
inst_2 : LinearOrder Γ
inst_3 : IsOrderedCancelAddMonoid Γ
inst_4 : Zero R
inst_5 : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
pos :
  ∀ (hx : x = 0),
    coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x • y))
        (x.order + order.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) =
      HSMul.hSMul (β := V) x.leadingCoeff
        (leadingCoeff.{u_6, u_5} (Γ := Γ) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y))
neg :
  ∀ (hx : ¬x = 0),
    coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x • y))
        (x.order + order.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) =
      HSMul.hSMul (β := V) x.leadingCoeff
        (leadingCoeff.{u_6, u_5} (Γ := Γ) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y))
⊢ coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x • y))
      (x.order + order.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) =
    HSMul.hSMul (β := V) x.leadingCoeff
      (leadingCoeff.{u_6, u_5} (Γ := Γ) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y))

Tactic:
by_cases hx : x = (0 : R⟦Γ⟧)

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
inst_1 : AddCommMonoid Γ
inst_2 : LinearOrder Γ
inst_3 : IsOrderedCancelAddMonoid Γ
inst_4 : Zero R
inst_5 : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : x = 0
⊢ coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x • y))
      (x.order + order.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) =
    HSMul.hSMul (β := V) x.leadingCoeff
      (leadingCoeff.{u_6, u_5} (Γ := Γ) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y))

Tactic:
simp [HahnSeries.coeff_zero, hx]

Premises used: HahnSeries.coeff_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
inst_1 : AddCommMonoid Γ
inst_2 : LinearOrder Γ
inst_3 : IsOrderedCancelAddMonoid Γ
inst_4 : Zero R
inst_5 : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
pos :
  ∀ (hy : Eq (α := V⟦Γ⟧) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y : V⟦Γ⟧) (0 : V⟦Γ⟧)),
    coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x • y))
        (x.order + order.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) =
      HSMul.hSMul (β := V) x.leadingCoeff
        (leadingCoeff.{u_6, u_5} (Γ := Γ) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y))
neg :
  ∀ (hy : ¬Eq (α := V⟦Γ⟧) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y : V⟦Γ⟧) (0 : V⟦Γ⟧)),
    coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x • y))
        (x.order + order.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) =
      HSMul.hSMul (β := V) x.leadingCoeff
        (leadingCoeff.{u_6, u_5} (Γ := Γ) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y))
⊢ coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x • y))
      (x.order + order.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) =
    HSMul.hSMul (β := V) x.leadingCoeff
      (leadingCoeff.{u_6, u_5} (Γ := Γ) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y))

Tactic:
by_cases hy : (of R).symm y = 0

Premises used: HahnModule.of, Equiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
inst_1 : AddCommMonoid Γ
inst_2 : LinearOrder Γ
inst_3 : IsOrderedCancelAddMonoid Γ
inst_4 : Zero R
inst_5 : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
hy : Eq (α := V⟦Γ⟧) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y : V⟦Γ⟧) (0 : V⟦Γ⟧)
⊢ coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x • y))
      (x.order + order.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) =
    HSMul.hSMul (β := V) x.leadingCoeff
      (leadingCoeff.{u_6, u_5} (Γ := Γ) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y))

Tactic:
simp [hy, coeff_smul]

Premises used: HahnModule.coeff_smul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
inst_1 : AddCommMonoid Γ
inst_2 : LinearOrder Γ
inst_3 : IsOrderedCancelAddMonoid Γ
inst_4 : Zero R
inst_5 : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬Eq (α := V⟦Γ⟧) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y : V⟦Γ⟧) (0 : V⟦Γ⟧)
neg :
  HSMul.hSMul (β := V)
      (x.coeff
        (⋯.min (s := x.support) ⋯,
            Set.IsWF.min (s :=
              HahnSeries.support.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) ⋯ ⋯).1)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)
        (⋯.min (s := x.support) ⋯,
            Set.IsWF.min (s :=
              HahnSeries.support.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) ⋯ ⋯).2) =
    HSMul.hSMul (β := V) (x.coeff (x.orderTop.untop ⋯))
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)
        (WithTop.untop (orderTop.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) ⋯))
⊢ coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x • y))
      (x.order + order.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) =
    HSMul.hSMul (β := V) x.leadingCoeff
      (leadingCoeff.{u_6, u_5} (Γ := Γ) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y))

Tactic:
rw [HahnSeries.order_of_ne hx, HahnSeries.order_of_ne hy, coeff_smul,
    HahnSeries.leadingCoeff_of_ne_zero hx, HahnSeries.leadingCoeff_of_ne_zero hy, ← vadd_eq_add,
    Finset.vaddAntidiagonal_min_vadd_min, Finset.sum_singleton]

Premises used: Finset.sum_singleton, HahnModule.coeff_smul, HahnSeries.order_of_ne, vadd_eq_add, Finset.vaddAntidiagonal_min_vadd_min, HahnSeries.leadingCoeff_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
R : Type u_3
V : Type u_5
inst : AddCommMonoid V
Γ : Type u_6
inst_1 : AddCommMonoid Γ
inst_2 : LinearOrder Γ
inst_3 : IsOrderedCancelAddMonoid Γ
inst_4 : Zero R
inst_5 : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬Eq (α := V⟦Γ⟧) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y : V⟦Γ⟧) (0 : V⟦Γ⟧)
⊢ HSMul.hSMul (β := V)
      (x.coeff
        (⋯.min (s := x.support) ⋯,
            Set.IsWF.min (s :=
              HahnSeries.support.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) ⋯ ⋯).1)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)
        (⋯.min (s := x.support) ⋯,
            Set.IsWF.min (s :=
              HahnSeries.support.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) ⋯ ⋯).2) =
    HSMul.hSMul (β := V) (x.coeff (x.orderTop.untop ⋯))
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)
        (WithTop.untop (orderTop.{u_6, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y)) ⋯))

Tactic:
simp [HahnSeries.orderTop, hx, hy]

Premises used: HahnSeries.orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ (Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
      (HSMul.hSMul (β := HahnModule Γ R R) x ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) y : HahnModule Γ R R)) =
    x * y

Tactic:
rfl

Premises used: rfl