awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ_1 : Type u_1
Γ' : Type u_2
R_1 : Type u_3
S : Type u_4
V : Type u_5
Γ : Type u_6
R : Type u_7
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
y : R⟦Γ⟧ˣ
h : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y
h_1 : Nontrivial R
this : 0 < ((↑y : R⟦Γ⟧) - 1).orderTop
⊢ (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1

Tactic:
rw [orderTop_self_sub_one_pos_iff] at this

Premises used: HahnSeries.orderTop_self_sub_one_pos_iff
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ_1 : Type u_1
Γ' : Type u_2
R_1 : Type u_3
S : Type u_4
V : Type u_5
Γ : Type u_6
R : Type u_7
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
y : R⟦Γ⟧ˣ
h : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y
h_1 : Nontrivial R
this : (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1
rw : y.inv.leadingCoeff ≠ 0
⊢ (↑y : R⟦Γ⟧).leadingCoeff * y.inv.leadingCoeff ≠ 0

Tactic:
rw [this.2, one_mul]

Premises used: And.right, one_mul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ_1 : Type u_1
Γ' : Type u_2
R_1 : Type u_3
S : Type u_4
V : Type u_5
Γ : Type u_6
R : Type u_7
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
y : R⟦Γ⟧ˣ
h : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y
h_1 : Nontrivial R
this : (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1
⊢ y.inv ≠ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ_1 : Type u_1
Γ' : Type u_2
R_1 : Type u_3
S : Type u_4
V : Type u_5
Γ : Type u_6
R : Type u_7
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
y : R⟦Γ⟧ˣ
h : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y
h_1 : Nontrivial R
this : (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1
⊢ y.inv.leadingCoeff ≠ 0

Tactic:
exact leadingCoeff_ne_zero.mpr (by simp)

Premises used: Iff.mpr, HahnSeries.leadingCoeff_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ_1 : Type u_1
Γ' : Type u_2
R_1 : Type u_3
S : Type u_4
V : Type u_5
Γ : Type u_6
R : Type u_7
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
y : R⟦Γ⟧ˣ
h : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y
h_1 : Nontrivial R
this : (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1
⊢ (↑y : R⟦Γ⟧).leadingCoeff * y.inv.leadingCoeff ≠ 0

Tactic:
have nz : y.val.leadingCoeff * y.inv.leadingCoeff ≠ 0 := by
        rw [this.2, one_mul]
        exact leadingCoeff_ne_zero.mpr (by simp)
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ_1 : Type u_1
Γ' : Type u_2
R_1 : Type u_3
S : Type u_4
V : Type u_5
Γ : Type u_6
R : Type u_7
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
y : R⟦Γ⟧ˣ
h : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y
h_1 : Nontrivial R
this : (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1
nz : (↑y : R⟦Γ⟧).leadingCoeff * y.inv.leadingCoeff ≠ 0
⊢ 0 < (y.inv - 1).orderTop

Tactic:
y.inv.orderTop_self_sub_one_pos_iff.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, And.intro, HahnSeries.orderTop_self_sub_one_pos_iff, Units.inv
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ_1 : Type u_1
Γ' : Type u_2
R_1 : Type u_3
S : Type u_4
V : Type u_5
Γ : Type u_6
R : Type u_7
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
y : R⟦Γ⟧ˣ
h : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y
h_1 : Nontrivial R
this : (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1
nz : (↑y : R⟦Γ⟧).leadingCoeff * y.inv.leadingCoeff ≠ 0
inr : y.inv.orderTop = 0
inr₁ : y.inv.leadingCoeff = 1
⊢ 0 < (y.inv - 1).orderTop

Tactic:
refine y.inv.orderTop_self_sub_one_pos_iff.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, And.intro, HahnSeries.orderTop_self_sub_one_pos_iff, Units.inv
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ_1 : Type u_1
Γ' : Type u_2
R_1 : Type u_3
S : Type u_4
V : Type u_5
Γ : Type u_6
R : Type u_7
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
y : R⟦Γ⟧ˣ
h : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y
h_1 : Nontrivial R
this : (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1
nz : (↑y : R⟦Γ⟧).leadingCoeff * y.inv.leadingCoeff ≠ 0
⊢ y.inv.orderTop = 0

Tactic:
simpa [this.1, y.val_inv] using (orderTop_mul_of_ne_zero nz).symm

Premises used: HahnSeries.orderTop_mul_of_ne_zero, And.left, Eq.symm, Units.val_inv
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ_1 : Type u_1
Γ' : Type u_2
R_1 : Type u_3
S : Type u_4
V : Type u_5
Γ : Type u_6
R : Type u_7
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
y : R⟦Γ⟧ˣ
h : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y
h_1 : Nontrivial R
this : (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1
nz : (↑y : R⟦Γ⟧).leadingCoeff * y.inv.leadingCoeff ≠ 0
⊢ y.inv.leadingCoeff = 1

Tactic:
simpa [this.2, y.val_inv] using (leadingCoeff_mul_of_ne_zero nz).symm

Premises used: HahnSeries.leadingCoeff_mul_of_ne_zero, And.right, Eq.symm, Units.val_inv
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧ˣ
⊢ Membership.mem (γ := Subgroup R⟦Γ⟧ˣ) (orderTopSubOnePos Γ R) x ↔ 0 < ((↑x : R⟦Γ⟧) - 1).orderTop

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : AddCommMonoid V
inst_7 : Semiring R
inst_8 : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h :
  ∀ (b : Γ'),
    Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) ((x * y) • z)) b)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y • z)) b)
⊢ (x * y) • z = x • y • z

Tactic:
ext b
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : AddCommMonoid V
inst_7 : Semiring R
inst_8 : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
h :
  Eq.{u_5 + 1} (α := 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)) b ⋯,
      HSMul.hSMul (β := V) ((x * y).coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) ij.2))
    (∑
      ij ∈
        VAddAntidiagonal (s := x.support) (t :=
          HVAdd.hVAdd (β := Set Γ') y.support
            (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)))
          b ⋯,
      HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (y • z)) ij.2))
⊢ Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) ((x * y) • z)) b)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y • z)) b)

Tactic:
rw [coeff_smul_left (x.isPWO_support.add y.isPWO_support)
    HahnSeries.support_mul_subset, coeff_smul_right
    (y.isPWO_support.vadd ((of R).symm z).isPWO_support) support_smul_subset_vadd_support]

Premises used: HahnSeries.isPWO_support, Set.IsPWO.vadd, HahnModule.of, Set.IsPWO.add, HahnSeries.support_mul_subset, HahnModule.support_smul_subset_vadd_support, HahnModule.coeff_smul_left, HahnModule.coeff_smul_right, 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 : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : AddCommMonoid V
inst_7 : Semiring R
inst_8 : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
h :
  Eq.{u_5 + 1} (α := V)
    (∑
      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)) b
              ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ) fun (a : Γ × Γ') ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1,
      HSMul.hSMul (β := V)
        (x.coeff x_1.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ).1 * y.coeff x_1.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ).2)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) x_1.fst (β := fun (i : Γ × Γ') ↦ Γ × Γ).2))
    (∑
      x_1 ∈
        (VAddAntidiagonal (s := x.support) (t :=
              HVAdd.hVAdd (β := Set Γ') y.support
                (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)))
              b ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ') fun (a : Γ × Γ') ↦
          VAddAntidiagonal (s := y.support) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a.2 ⋯,
      x.coeff x_1.fst (β := fun (i : Γ × Γ') ↦ Γ × Γ').1 •
        HSMul.hSMul (β := V) (y.coeff x_1.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ').1)
          (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) x_1.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ').2))
⊢ Eq.{u_5 + 1} (α := 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)) b ⋯,
      HSMul.hSMul (β := V) ((x * y).coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) ij.2))
    (∑
      ij ∈
        VAddAntidiagonal (s := x.support) (t :=
          HVAdd.hVAdd (β := Set Γ') y.support
            (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)))
          b ⋯,
      HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (y • z)) ij.2))

Tactic:
simp only [HahnSeries.coeff_mul, coeff_smul, sum_smul, smul_sum, sum_sigma']

Premises used: Finset.sum_smul, HahnSeries.coeff_mul, Finset.sum_sigma', HahnModule.coeff_smul, Finset.smul_sum
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : AddCommMonoid V
inst_7 : Semiring R
inst_8 : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∀ (a : (_ : Γ × Γ') × Γ × Γ),
    Membership.mem (γ := Finset ((_ : Γ × Γ') × Γ × Γ))
        ((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)) b
              ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ) fun (a : Γ × Γ') ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1)
        a →
      Membership.mem (α := (_ : Γ × Γ') × Γ × Γ') (γ := Finset ((_ : Γ × Γ') × Γ × Γ'))
        ((VAddAntidiagonal (s := x.support) (t :=
              HVAdd.hVAdd (β := Set Γ') y.support
                (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)))
              b ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ') fun (a : Γ × Γ') ↦
          VAddAntidiagonal (s := y.support) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a.2 ⋯)
        (match (motive := (_ : Γ × Γ') × Γ × Γ → (_ : Γ × Γ') × Γ × Γ') a with
          | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ') ↦ Γ × Γ') (k, l +ᵥ j) (l, j) :
          (_ : Γ × Γ') × Γ × Γ')

Tactic:
aesop (add safe [Set.vadd_mem_vadd, Set.add_mem_add]) (add simp [add_vadd, mul_smul])

Premises used: Set.vadd_mem_vadd, AddSemigroupAction.add_vadd, Set.add_mem_add, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : AddCommMonoid V
inst_7 : Semiring R
inst_8 : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∀ (a : (_ : Γ × Γ') × Γ × Γ'),
    Membership.mem (γ := Finset ((_ : Γ × Γ') × Γ × Γ'))
        ((VAddAntidiagonal (s := x.support) (t :=
              HVAdd.hVAdd (β := Set Γ') y.support
                (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)))
              b ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ') fun (a : Γ × Γ') ↦
          VAddAntidiagonal (s := y.support) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a.2 ⋯)
        a →
      Membership.mem (α := (_ : Γ × Γ') × Γ × Γ) (γ := Finset ((_ : Γ × Γ') × Γ × Γ))
        ((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)) b
              ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ) fun (a : Γ × Γ') ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1)
        (match (motive := (_ : Γ × Γ') × Γ × Γ' → (_ : Γ × Γ') × Γ × Γ) a with
          | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ') ↦ Γ × Γ) (i + k, l) (i, k) :
          (_ : Γ × Γ') × Γ × Γ)

Tactic:
aesop (add safe [Set.vadd_mem_vadd, Set.add_mem_add]) (add simp [add_vadd, mul_smul])

Premises used: Set.vadd_mem_vadd, AddSemigroupAction.add_vadd, Set.add_mem_add, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : AddCommMonoid V
inst_7 : Semiring R
inst_8 : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∀ (a : (_ : Γ × Γ') × Γ × Γ),
    Membership.mem (γ := Finset ((_ : Γ × Γ') × Γ × Γ))
        ((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)) b
              ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ) fun (a : Γ × Γ') ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1)
        a →
      (match (motive := (_ : Γ × Γ') × Γ × Γ' → (_ : Γ × Γ') × Γ × Γ)
          match (motive := (_ : Γ × Γ') × Γ × Γ → (_ : Γ × Γ') × Γ × Γ') a with
          | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ') ↦ Γ × Γ') (k, l +ᵥ j) (l, j) with
        | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ') ↦ Γ × Γ) (i + k, l) (i, k)) =
        a

Tactic:
aesop (add safe [Set.vadd_mem_vadd, Set.add_mem_add]) (add simp [add_vadd, mul_smul])

Premises used: Set.vadd_mem_vadd, AddSemigroupAction.add_vadd, Set.add_mem_add, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : AddCommMonoid V
inst_7 : Semiring R
inst_8 : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∀ (a : (_ : Γ × Γ') × Γ × Γ'),
    Membership.mem (γ := Finset ((_ : Γ × Γ') × Γ × Γ'))
        ((VAddAntidiagonal (s := x.support) (t :=
              HVAdd.hVAdd (β := Set Γ') y.support
                (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)))
              b ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ') fun (a : Γ × Γ') ↦
          VAddAntidiagonal (s := y.support) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a.2 ⋯)
        a →
      (match (motive := (_ : Γ × Γ') × Γ × Γ → (_ : Γ × Γ') × Γ × Γ')
          match (motive := (_ : Γ × Γ') × Γ × Γ' → (_ : Γ × Γ') × Γ × Γ) a with
          | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ') ↦ Γ × Γ) (i + k, l) (i, k) with
        | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ') ↦ Γ × Γ') (k, l +ᵥ j) (l, j)) =
        a

Tactic:
aesop (add safe [Set.vadd_mem_vadd, Set.add_mem_add]) (add simp [add_vadd, mul_smul])

Premises used: Set.vadd_mem_vadd, AddSemigroupAction.add_vadd, Set.add_mem_add, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : AddCommMonoid V
inst_7 : Semiring R
inst_8 : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∀ (a : (_ : Γ × Γ') × Γ × Γ),
    Membership.mem (γ := Finset ((_ : Γ × Γ') × Γ × Γ))
        ((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)) b
              ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ) fun (a : Γ × Γ') ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1)
        a →
      HSMul.hSMul (β := V)
          (x.coeff a.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ).1 * y.coeff a.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ).2)
          (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) a.fst (β := fun (i : Γ × Γ') ↦ Γ × Γ).2) =
        x.coeff
            (Sigma.fst (β := fun (i : Γ × Γ') ↦ Γ × Γ')
                (match (motive := (_ : Γ × Γ') × Γ × Γ → (_ : Γ × Γ') × Γ × Γ') a with
                | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ') ↦ Γ × Γ') (k, l +ᵥ j) (l, j))).1 •
          HSMul.hSMul (β := V)
            (y.coeff
              (Sigma.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ')
                    (match (motive := (_ : Γ × Γ') × Γ × Γ → (_ : Γ × Γ') × Γ × Γ') a with
                    | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ') ↦ Γ × Γ') (k, l +ᵥ j) (l, j)) :
                  Γ × Γ').1)
            (coeff.{u_2, u_5} (Γ := Γ') ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z : V⟦Γ'⟧)
              ((Sigma.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ')
                    (match (motive := (_ : Γ × Γ') × Γ × Γ → (_ : Γ × Γ') × Γ × Γ') a with
                    | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ') ↦ Γ × Γ') (k, l +ᵥ j) (l, j))).2 :
                Γ'))

Tactic:
aesop (add safe [Set.vadd_mem_vadd, Set.add_mem_add]) (add simp [add_vadd, mul_smul])

Premises used: Set.vadd_mem_vadd, AddSemigroupAction.add_vadd, Set.add_mem_add, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S_1 : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : AddCommMonoid V
inst_7 : Zero R
S : Type u_6
inst_8 : Zero S
inst_9 : SMul R S
inst_10 : SMulWithZero R V
inst_11 : SMulWithZero S V
inst_12 : IsScalarTower R S V
r : R
s : S
a : V⟦Γ⟧
coeff : ∀ (x : Γ), ((r • s) • a).coeff x = (r • s • a).coeff x
⊢ (r • s) • a = r • s • a

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S_1 : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : AddCommMonoid V
inst_7 : Zero R
S : Type u_6
inst_8 : Zero S
inst_9 : SMul R S
inst_10 : SMulWithZero R V
inst_11 : SMulWithZero S V
inst_12 : IsScalarTower R S V
r : R
s : S
a : V⟦Γ⟧
x : Γ
⊢ ((r • s) • a).coeff x = (r • s • a).coeff x

Tactic:
simp
-- 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 : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : AddCommMonoid V
inst_7 : Semiring R
inst_8 : Module R V
r : R
x : R⟦Γ⟧
a : HahnModule Γ' R V
rw : HMul.hMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x • a = r • x • a
rw₁ : HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (x • a) = r • x • a
rw₂ rw₃ :
  HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (x • a) =
    HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (x • a)
⊢ (r • x) • a = r • x • a

Tactic:
rw [← HahnSeries.single_zero_mul_eq_smul, mul_smul', ← single_zero_smul_eq_smul Γ]

Premises used: HahnSeries.single_zero_mul_eq_smul, _private.0.HahnModule.mul_smul', HahnModule.single_zero_smul_eq_smul
-- 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 : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : AddCommMonoid V
inst_7 : CommSemiring R
inst_8 : Module R V
r : R
x : R⟦Γ⟧
y : HahnModule Γ' R V
rw : HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (x • y) = x • r • y
rw₁ : HMul.hMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x • y = x • r • y
rw₂ : HMul.hMul (β := R⟦Γ⟧) x ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) • y = x • r • y
rw₃ : x • HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y = x • r • y
rw₄ rw₅ : x • r • y = x • r • y
⊢ r • x • y = x • r • y

Tactic:
rw [← single_zero_smul_eq_smul Γ, ← mul_smul', mul_comm, mul_smul', single_zero_smul_eq_smul Γ]

Premises used: _private.0.HahnModule.mul_smul', mul_comm, HahnModule.single_zero_smul_eq_smul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ_1 : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V_1 : Type u_5
inst : AddCommMonoid Γ_1
inst_1 : PartialOrder Γ_1
inst_2 : IsOrderedCancelAddMonoid Γ_1
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ_1 Γ'
inst_5 : IsOrderedCancelVAdd Γ_1 Γ'
inst_6 : AddCommMonoid V_1
Γ : Type u_6
V : Type u_7
inst_7 : Ring R
inst_8 : IsDomain R
inst_9 : AddCommGroup V
inst_10 : AddCommMonoid Γ
inst_11 : LinearOrder Γ
inst_12 : IsOrderedCancelAddMonoid Γ
inst_13 : Module R V
inst_14 : Module.IsTorsionFree R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hxy : x • y = 0
contrapose! : ∀ (hxy : x ≠ 0 ∧ y ≠ 0), x • y ≠ 0
⊢ x = 0 ∨ y = 0

Tactic:
contrapose! hxy
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ_1 : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V_1 : Type u_5
inst : AddCommMonoid Γ_1
inst_1 : PartialOrder Γ_1
inst_2 : IsOrderedCancelAddMonoid Γ_1
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ_1 Γ'
inst_5 : IsOrderedCancelVAdd Γ_1 Γ'
inst_6 : AddCommMonoid V_1
Γ : Type u_6
V : Type u_7
inst_7 : Ring R
inst_8 : IsDomain R
inst_9 : AddCommGroup V
inst_10 : AddCommMonoid Γ
inst_11 : LinearOrder Γ
inst_12 : IsOrderedCancelAddMonoid Γ
inst_13 : Module R V
inst_14 : Module.IsTorsionFree R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hxy : x ≠ 0 ∧ y ≠ 0
rw :
  ∃ (x_1 : Γ),
    ¬Eq.{u_7 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) (x • y)) x_1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ R V) → V⟦Γ⟧) 0) x_1)
⊢ x • y ≠ 0

Tactic:
rw [ne_eq, HahnModule.ext_iff, funext_iff, not_forall]

Premises used: funext_iff, ne_eq, HahnModule.ext_iff, Classical.not_forall