awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : AddMonoid R
⊢ ∀ (x y : Lex R⟦Γ⟧),
    OrderHom.toFun (OrderEmbedding.toOrderHom (embDomainOrderEmbedding f)) (x + y) =
      OrderHom.toFun (OrderEmbedding.toOrderHom (embDomainOrderEmbedding f)) x +
        OrderHom.toFun (OrderEmbedding.toOrderHom (embDomainOrderEmbedding f)) y

Tactic:
simp [embDomainOrderEmbedding, embDomain_add]

Premises used: HahnSeries.embDomainOrderEmbedding, HahnSeries.embDomain_add
-- Module: Mathlib.RingTheory.HahnSeries.Lex
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : AddMonoid R
⊢ Function.Injective (α := Lex R⟦Γ⟧) (β := Lex R⟦Γ'⟧) (⇑(embDomainOrderAddMonoidHom f) : (a : Lex R⟦Γ⟧) → Lex R⟦Γ'⟧)

Tactic:
(embDomainOrderEmbedding f).injective

Premises used: HahnSeries.embDomainOrderEmbedding, RelEmbedding.injective
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : Zero R
inst_3 : One R
a : Γ
⊢ Eq.{u_3 + 1} (α := R) (coeff 1 a) (if a = 0 then 1 else 0)

Tactic:
coeff_single

Premises used: HahnSeries.coeff_single
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : Zero R
inst_3 : One R
⊢ Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : Zero R
inst_3 : NatCast R
n : ℕ
⊢ Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (↑n : R)) (↑n : R⟦Γ⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : Zero R
inst_3 : IntCast R
z : ℤ
⊢ Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (↑z : R)) (↑z : R⟦Γ⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : Zero R
inst_3 : NNRatCast R
q : ℚ≥0
⊢ Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (↑q : R)) (↑q : R⟦Γ⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : Zero R
inst_3 : RatCast R
q : ℚ
⊢ Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (↑q : R)) (↑q : R⟦Γ⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : Zero R
inst_3 : NatCast R
n : ℕ
inst_4 : n.AtLeastTwo
⊢ Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : MulZeroOneClass R
inst_3 : Nontrivial R
⊢ Eq (α := Set Γ) (support.{u_1, u_3} (R := R) 1) {0}

Tactic:
support_single_of_ne one_ne_zero

Premises used: HahnSeries.support_single_of_ne, one_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : Zero R
inst_3 : One R
inst_4 : NeZero.{u_3} (R := R) 1
rw : Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((single 0 : (a : R) → R⟦Γ⟧) 1)) 0
rw₁ : Eq.{u_1 + 1} (α := WithTop Γ) (↑0 : WithTop Γ) 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := Γ) 0 0
⊢ Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_3} (R := R) 1) 0

Tactic:
rw [← single_zero_one, orderTop_single one_ne_zero, WithTop.coe_eq_zero]

Premises used: WithTop.coe_eq_zero, HahnSeries.single_zero_one, one_ne_zero, HahnSeries.orderTop_single
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : MulZeroOneClass R
inl : Subsingleton R → Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0
inr : Nontrivial R → Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : MulZeroOneClass R
h : Subsingleton R
inl : Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 0) 0
inl₁ inl₂ : Eq.{u_1 + 1} (α := Γ) 0 0
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0

Tactic:
rw [Subsingleton.elim (1 : R⟦Γ⟧) 0, order_zero]

Premises used: HahnSeries.order_zero, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : MulZeroOneClass R
h : Nontrivial R
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0

Tactic:
order_single one_ne_zero

Premises used: one_ne_zero, HahnSeries.order_single
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : MulZeroOneClass R
h : Nontrivial R
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0

Tactic:
exact order_single one_ne_zero

Premises used: one_ne_zero, HahnSeries.order_single
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : MulZeroOneClass R
⊢ Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_1, u_3} (Γ := Γ) 1) 1

Tactic:
simp [leadingCoeff_eq]

Premises used: HahnSeries.leadingCoeff_eq
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : MonoidWithZero R
inst_3 : MonoidWithZero S
f : R →*₀ S
⊢ Eq (α := S⟦Γ⟧) (map 1 f) 1

Tactic:
HahnSeries.map_single (a := (0 : Γ)) f.toZeroHom |>.trans <| congrArg _ <| f.map_one

Premises used: HahnSeries.map_single, congrArg, MonoidWithZeroHom.map_one, MonoidWithZeroHom.toZeroHom, HahnSeries.map, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : AddCommMonoidWithOne R
⊢ Eq (α := R⟦Γ⟧) (↑0) 0

Tactic:
simp [← single_zero_natCast]

Premises used: HahnSeries.single_zero_natCast
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : AddCommMonoidWithOne R
n : ℕ
⊢ ↑(n + 1) = HAdd.hAdd (α := R⟦Γ⟧) (↑n) 1

Tactic:
simp [← single_zero_natCast]

Premises used: HahnSeries.single_zero_natCast
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : AddCommGroupWithOne R
n : ℕ
⊢ Eq (α := R⟦Γ⟧) (IntCast.intCast (↑n : ℤ)) (↑n : R⟦Γ⟧)

Tactic:
simp [← single_zero_natCast, ← single_zero_intCast]

Premises used: HahnSeries.single_zero_natCast, HahnSeries.single_zero_intCast
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : AddCommGroupWithOne R
n : ℕ
⊢ Eq (α := R⟦Γ⟧) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : R⟦Γ⟧))

Tactic:
simp [← single_zero_natCast, ← single_zero_intCast]

Premises used: HahnSeries.single_zero_natCast, HahnSeries.single_zero_intCast
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : Zero V
inst_2 : SMul R V
x y : HahnModule Γ R V
h :
  Eq (α := Γ → V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) x))
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y))
⊢ x = y

Tactic:
(of R).symm.injective <| HahnSeries.coeff_inj.1 h

Premises used: HahnSeries.coeff_inj, HahnModule.of, Iff.mp, Equiv.injective, Equiv.symm
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : SMul R V
inst_2 : Zero V
⊢ Eq (α := HahnModule Γ R V) ((of R : (a : V⟦Γ⟧) → HahnModule Γ R V) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : SMul R V
inst_2 : AddCommMonoid V
x y : V⟦Γ⟧
⊢ (of R : (a : V⟦Γ⟧) → HahnModule Γ R V) (x + y) =
    HAdd.hAdd (α := HahnModule Γ R V) (β := HahnModule Γ R V)
      ((of R : (a : V⟦Γ⟧) → HahnModule Γ R V) x : HahnModule Γ R V)
      ((of R : (a : V⟦Γ⟧) → HahnModule Γ R V) y : HahnModule Γ R V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : SMul R V
inst_2 : AddCommGroup V
x y : V⟦Γ⟧
⊢ (of R : (a : V⟦Γ⟧) → HahnModule Γ R V) (x - y) =
    HSub.hSub (α := HahnModule Γ R V) (β := HahnModule Γ R V)
      ((of R : (a : V⟦Γ⟧) → HahnModule Γ R V) x : HahnModule Γ R V)
      ((of R : (a : V⟦Γ⟧) → HahnModule Γ R V) y : HahnModule Γ R V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : SMul R V
inst_2 : Zero V
⊢ Eq (α := V⟦Γ⟧) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : SMul R V
inst_2 : AddCommMonoid V
x y : HahnModule Γ R V
⊢ (Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x + y) =
    HAdd.hAdd (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) x : V⟦Γ⟧)
      ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y : V⟦Γ⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : SMul R V
inst_2 : AddCommGroup V
x y : HahnModule Γ R V
⊢ (Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x - y) =
    HSub.hSub (α := V⟦Γ⟧) (β := V⟦Γ⟧) ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) x : V⟦Γ⟧)
      ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) y : V⟦Γ⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : PartialOrder Γ
inst_1 : SMul R V
inst_2 : PartialOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : Zero R
inst_6 : AddCommMonoid V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
ha :
  Membership.mem (γ := Set Γ')
    {a : Γ' |
      Ne.{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))
        0}
    a
contrapose! :
  ∀
    (ha :
      VAddAntidiagonal (s := x.support) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a ⋯ =
        ∅),
    a ∉
      {a : Γ' |
        Ne.{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))
          0}
⊢ (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

Tactic:
contrapose! ha
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : PartialOrder Γ
inst_1 : SMul R V
inst_2 : PartialOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : Zero R
inst_6 : AddCommMonoid V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
ha :
  VAddAntidiagonal (s := x.support) (t :=
      HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a ⋯ =
    ∅
⊢ a ∉
    {a : Γ' |
      Ne.{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))
        0}

Tactic:
simp [ha]
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : SMul R V
inst_2 : PartialOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : Zero R
inst_6 : AddCommMonoid V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
⊢ Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y)) a)
    (∑
      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))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.sum, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
⊢ (of R : (a : V⟦Γ⟧) → HahnModule Γ R V) (r • x) =
    HSMul.hSMul (β := HahnModule Γ R V) r ((of R : (a : V⟦Γ⟧) → HahnModule Γ R V) x : HahnModule Γ R V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid V
inst_2 : SMulZeroClass R V
r : R
x : HahnModule Γ R V
⊢ (Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (r • x) =
    HSMul.hSMul (β := V⟦Γ⟧) r ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) x : V⟦Γ⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
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 : SMulZeroClass R V
x : R⟦Γ⟧
h :
  ∀ (x_1 : Γ'),
    Eq.{u_5 + 1} (α := V)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (HSMul.hSMul (β := HahnModule Γ' R V) x 0)) x_1)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) 0) x_1)
⊢ HSMul.hSMul (β := HahnModule Γ' R V) x 0 = 0

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
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 : SMulZeroClass R V
x : R⟦Γ⟧
x_1 : Γ'
⊢ Eq.{u_5 + 1} (α := V)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (HSMul.hSMul (β := HahnModule Γ' R V) x 0)) 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_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 : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ⊆ s
apply :
  ∀
    x_1 ∈
      VAddAntidiagonal (s := x.support) (t := s) 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 x_1.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) x_1.2) = 0
⊢ 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 := x.support) (t := s) a ⋯,
      HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ij.2))

Tactic:
apply sum_subset_zero_on_sdiff (vaddAntidiagonal_mono_right _ _ _ hys) _ fun _ _ => rfl

Premises used: Finset.vaddAntidiagonal_mono_right, rfl, 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 : Zero R
inst_6 : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ⊆ s
b : Γ × Γ'
hb :
  b ∈
    VAddAntidiagonal (s := x.support) (t := s) 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 ⋯
⊢ (x.coeff b.1 ≠ 0 ∧ b.2 ∈ s ∧ b.1 +ᵥ b.2 = a) ∧
    (x.coeff b.1 ≠ 0 →
      b.1 +ᵥ b.2 = a → Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) 0)

Tactic:
simp only [not_and, mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_imp_not] at hb

Premises used: Finset.mem_vaddAntidiagonal, Finset.mem_sdiff, not_and, HahnSeries.mem_support, not_imp_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 : Zero R
inst_6 : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ⊆ s
b : Γ × Γ'
hb :
  (x.coeff b.1 ≠ 0 ∧ b.2 ∈ s ∧ b.1 +ᵥ b.2 = a) ∧
    (x.coeff b.1 ≠ 0 →
      b.1 +ᵥ b.2 = a → Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) 0)
rw : HSMul.hSMul (β := V) (x.coeff b.1) 0 = 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.1 hb.1.2.2, smul_zero]

Premises used: smul_zero, And.right, And.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 : Zero R
inst_6 : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ⊆ 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 := x.support) (t := s) 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 := x.support) (t := s) 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 :
      (x.coeff b.1 ≠ 0 ∧ b.2 ∈ s ∧ b.1 +ᵥ b.2 = a) ∧
        (x.coeff b.1 ≠ 0 →
          b.1 +ᵥ b.2 = a →
            Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) 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 := x.support) (t := s) 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_right _ _ _ hys) _ fun _ _ => rfl
  intro b hb
  simp only [not_and, mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_imp_not] at hb
  rw [hb.2 hb.1.1 hb.1.2.2, smul_zero]

Premises used: Finset.mem_vaddAntidiagonal, smul_zero, Finset.mem_sdiff, HahnModule.coeff_smul, Finset.vaddAntidiagonal_mono_right, not_and, rfl, HahnSeries.mem_support, not_imp_not, 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 : Zero R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ
hs : s.IsPWO
hxs : x.support ⊆ s
apply :
  ∀
    x_1 ∈
      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 x_1.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) x_1.2) = 0
⊢ 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))

Tactic:
apply sum_subset_zero_on_sdiff (vaddAntidiagonal_mono_left _ hxs _ _) _ fun _ _ => rfl

Premises used: Finset.vaddAntidiagonal_mono_left, rfl, 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 : 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 ∈
    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 ⋯
⊢ (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)

Tactic:
simp only [not_and', mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_ne_iff] at hb

Premises used: Finset.mem_vaddAntidiagonal, not_ne_iff, Finset.mem_sdiff, not_and', HahnSeries.mem_support