awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
x y : R⟦Γ⟧ˣ
hx : (↑x : R⟦Γ⟧).orderTop = 0 ∧ (↑x : R⟦Γ⟧).leadingCoeff = 1
hy : (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1
h : Nontrivial R
h1 : (↑x : R⟦Γ⟧).leadingCoeff * (↑y : R⟦Γ⟧).leadingCoeff = 1
⊢ (↑(x * y) : R⟦Γ⟧).leadingCoeff = 1
have inr : ((↑x : R⟦Γ⟧) * (↑y : R⟦Γ⟧)).leadingCoeff = 1
Tactic: rw [Units.val_mul, leadingCoeff_mul_of_ne_zero (h1 ▸ one_ne_zero), h1]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
x y : R⟦Γ⟧ˣ
hx : (↑x : R⟦Γ⟧).orderTop = 0 ∧ (↑x : R⟦Γ⟧).leadingCoeff = 1
hy : (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1
h : Nontrivial R
h1 : (↑x : R⟦Γ⟧).leadingCoeff * (↑y : R⟦Γ⟧).leadingCoeff = 1
inr : ((↑x : R⟦Γ⟧) * (↑y : R⟦Γ⟧)).leadingCoeff = 1
inr₁ : (↑x : R⟦Γ⟧).leadingCoeff * (↑y : R⟦Γ⟧).leadingCoeff = 1
⊢ (↑(x * y) : R⟦Γ⟧).leadingCoeff = 1
have inr₂ : Eq.{u_7 + 1} (α := R) 1 1
Tactic: rw [Units.val_mul, leadingCoeff_mul_of_ne_zero (h1 ▸ one_ne_zero), h1]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y⁻¹
have suffices : 0 < (y.inv - 1).orderTop
Tactic: suffices 0 < (y.inv - 1).orderTop by exact this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ 0 < (y.inv - 1).orderTop
have inl : Subsingleton R → 0 < (y.inv - 1).orderTop
Tactic: obtain (_ | _) := subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
inl : Subsingleton R → 0 < (y.inv - 1).orderTop
⊢ 0 < (y.inv - 1).orderTop
have inr : Nontrivial R → 0 < (y.inv - 1).orderTop
Tactic: obtain (_ | _) := subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
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
⊢ 0 < (y.inv - 1).orderTop
have this : 0 < ((↑y : R⟦Γ⟧) - 1).orderTop
Tactic: have : 0 < (y.val - 1).orderTop := h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
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
⊢ 0 < (y.inv - 1).orderTop
have this₁ : (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1
Tactic: rw [orderTop_self_sub_one_pos_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
have rw : y.inv.leadingCoeff ≠ 0
Tactic: rw [this.2, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
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
⊢ 0 < (y.inv - 1).orderTop
have nz : (↑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)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
have inr : y.inv.orderTop = 0
Tactic: refine y.inv.orderTop_self_sub_one_pos_iff.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ 0 < (y.inv - 1).orderTop
have inr₁ : y.inv.leadingCoeff = 1
Tactic: refine y.inv.orderTop_self_sub_one_pos_iff.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ (x * y) • z = x • y • z
have 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)
Tactic: ext b
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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 : Γ'
⊢ 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)
have 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 sorry,
    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 sorry,
    HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (y • z)) ij.2))
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]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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 : Γ'
⊢ 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))
have 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 sorry).sigma
        (α := fun (a : Γ × Γ') ↦ Γ × Γ) fun (a : Γ × Γ') ↦ addAntidiagonal (s := x.support) (t := y.support) sorry sorry 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 sorry).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 sorry,
    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))
Tactic: simp only [HahnSeries.coeff_mul, coeff_smul, sum_smul, smul_sum, sum_sigma']
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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 : Γ'
⊢ 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))
have h : ∀ (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 sorry).sigma
        (α := fun (a : Γ × Γ') ↦ Γ × Γ) fun (a : Γ × Γ') ↦ addAntidiagonal (s := x.support) (t := y.support) sorry sorry 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 sorry).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 sorry)
      (match (motive := (_ : Γ × Γ') × Γ × Γ → (_ : Γ × Γ') × Γ × Γ') a with
        | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ') ↦ Γ × Γ') (k, l +ᵥ j) (l, j) :
        (_ : Γ × Γ') × Γ × Γ')
Tactic: apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l +ᵥ j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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⟦Γ⟧
⊢ (r • s) • a = r • s • a
have coeff : ∀ (x : Γ), ((r • s) • a).coeff x = (r • s • a).coeff x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ (r • x) • a = r • x • a
have rw : HMul.hMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x • a = r • x • a
Tactic: rw [← HahnSeries.single_zero_mul_eq_smul, mul_smul', ← single_zero_smul_eq_smul Γ]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ (r • x) • a = r • x • a
have rw₁ : HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (x • a) = r • x • a
Tactic: rw [← HahnSeries.single_zero_mul_eq_smul, mul_smul', ← single_zero_smul_eq_smul Γ]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ (r • x) • a = r • x • a
have 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)
Tactic: rw [← HahnSeries.single_zero_mul_eq_smul, mul_smul', ← single_zero_smul_eq_smul Γ]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ r • x • y = x • r • y
have rw : HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (x • y) = x • r • y
Tactic: rw [← single_zero_smul_eq_smul Γ, ← mul_smul', mul_comm, mul_smul', single_zero_smul_eq_smul Γ]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ r • x • y = x • r • y
have rw₁ : HMul.hMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x • y = x • r • y
Tactic: rw [← single_zero_smul_eq_smul Γ, ← mul_smul', mul_comm, mul_smul', single_zero_smul_eq_smul Γ]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ r • x • y = x • r • y
have rw₂ : HMul.hMul (β := R⟦Γ⟧) x ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) • y = x • r • y
Tactic: rw [← single_zero_smul_eq_smul Γ, ← mul_smul', mul_comm, mul_smul', single_zero_smul_eq_smul Γ]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ r • x • y = x • r • y
have rw₃ : x • HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y = x • r • y
Tactic: rw [← single_zero_smul_eq_smul Γ, ← mul_smul', mul_comm, mul_smul', single_zero_smul_eq_smul Γ]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ r • x • y = x • r • y
have rw₄ : x • r • y = x • r • y
Tactic: rw [← single_zero_smul_eq_smul Γ, ← mul_smul', mul_comm, mul_smul', single_zero_smul_eq_smul Γ]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ x = 0 ∨ y = 0
have contrapose! : ∀ (hxy : x ≠ 0 ∧ y ≠ 0), x • y ≠ 0
Tactic: contrapose! hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
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
⊢ x • y ≠ 0
have 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)
Tactic: rw [ne_eq, HahnModule.ext_iff, funext_iff, not_forall]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
⊢ HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧) =
    (single (a + b) : (a : R) → R⟦Γ⟧) (r * s)
have coeff : ∀ (x : Γ),
  (HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff
      x =
    coeff ((single (a + b) : (a : R) → R⟦Γ⟧) (r * s)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
⊢ (HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff
      x =
    coeff ((single (a + b) : (a : R) → R⟦Γ⟧) (r * s)) x
have pos : ∀ (h : x = a + b),
  (HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff
      x =
    coeff ((single (a + b) : (a : R) → R⟦Γ⟧) (r * s)) x
Tactic: by_cases h : x = a + b