awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : NonAssocSemiring R
x : R⟦Γ⟧
⊢ 1 * x = x
have coeff : ∀ (x_1 : Γ), (1 * x).coeff x_1 = x.coeff x_1
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 : NonAssocSemiring R
x : R⟦Γ⟧
⊢ x * 1 = x
have coeff : ∀ (x_1 : Γ), (x * 1).coeff x_1 = x.coeff x_1
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 : NonUnitalCommSemiring R
x y : R⟦Γ⟧
⊢ x * y = y * x
have coeff : ∀ (x_1 : Γ), (x * y).coeff x_1 = (y * x).coeff x_1
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 : NonUnitalCommSemiring R
x y : R⟦Γ⟧
x_1 : Γ
⊢ (x * y).coeff x_1 = (y * x).coeff x_1
have coeff : Eq.{u_3 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := x.support) (t := y.support) sorry sorry x_1, x.coeff ij.1 * y.coeff ij.2)
  (∑ x_2 ∈ addAntidiagonal (s := y.support) (t := x.support) sorry sorry x_1, x.coeff x_2.2 * y.coeff x_2.1)
Tactic: simp_rw [coeff_mul, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
⊢ HSMul.hSMul (α := ℕ) 0 x.orderTop ≤ (HPow.hPow (β := ℕ) x 0).orderTop
have zero : LE.le.{u_1} (α := WithTop Γ) 0 (orderTop.{u_1, u_3} (R := R) 1)
Tactic: simp only [zero_smul, pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
⊢ LE.le.{u_1} (α := WithTop Γ) 0 (orderTop.{u_1, u_3} (R := R) 1)
have pos : ∀ (h : NeZero.{u_3} (R := R) 1), LE.le.{u_1} (α := WithTop Γ) 0 (orderTop.{u_1, u_3} (R := R) 1)
Tactic: by_cases h : NeZero (1 : R)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
pos : ∀ (h : NeZero.{u_3} (R := R) 1), LE.le.{u_1} (α := WithTop Γ) 0 (orderTop.{u_1, u_3} (R := R) 1)
⊢ LE.le.{u_1} (α := WithTop Γ) 0 (orderTop.{u_1, u_3} (R := R) 1)
have neg : ∀ (h : ¬NeZero.{u_3} (R := R) 1), LE.le.{u_1} (α := WithTop Γ) 0 (orderTop.{u_1, u_3} (R := R) 1)
Tactic: by_cases h : NeZero (1 : R)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
h : ¬NeZero.{u_3} (R := R) 1
⊢ LE.le.{u_1} (α := WithTop Γ) 0 (orderTop.{u_1, u_3} (R := R) 1)
have this : Subsingleton R
Tactic: have : Subsingleton R := not_nontrivial_iff_subsingleton.mp fun _ ↦ h NeZero.one
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ (n + 1) • x.orderTop ≤ (x ^ (n + 1)).orderTop
have succ : n • x.orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop ≤ (x ^ n * HPow.hPow (β := ℕ) x 1).orderTop
Tactic: rw [add_nsmul, pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ (x ^ n).orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop = (x ^ n).orderTop + x.orderTop
have rw : (x ^ n).orderTop + x.orderTop = (x ^ n).orderTop + x.orderTop
Tactic: rw [one_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ (x ^ n * x).orderTop ≤ (x ^ n * HPow.hPow (β := ℕ) x 1).orderTop
have rw : (x ^ n * x).orderTop ≤ (x ^ n * x).orderTop
Tactic: rw [pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ n • x.orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop ≤ (x ^ n * HPow.hPow (β := ℕ) x 1).orderTop
have n₁ : n • x.orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop ≤ (x ^ n).orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop
Tactic: calc
      n • x.orderTop + 1 • x.orderTop ≤ (x ^ n).orderTop + 1 • x.orderTop := by gcongr
      (x ^ n).orderTop + 1 • x.orderTop = (x ^ n).orderTop + x.orderTop := by rw [one_nsmul]
      (x ^ n).orderTop + x.orderTop ≤ (x ^ n * x).orderTop := orderTop_add_le_mul
      (x ^ n * x).orderTop ≤ (x ^ n * x ^ 1).orderTop := by rw [pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
n₁ : n • x.orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop ≤ (x ^ n).orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop
⊢ n • x.orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop ≤ (x ^ n * HPow.hPow (β := ℕ) x 1).orderTop
have n₂ : (x ^ n).orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop = (x ^ n).orderTop + x.orderTop
Tactic: calc
      n • x.orderTop + 1 • x.orderTop ≤ (x ^ n).orderTop + 1 • x.orderTop := by gcongr
      (x ^ n).orderTop + 1 • x.orderTop = (x ^ n).orderTop + x.orderTop := by rw [one_nsmul]
      (x ^ n).orderTop + x.orderTop ≤ (x ^ n * x).orderTop := orderTop_add_le_mul
      (x ^ n * x).orderTop ≤ (x ^ n * x ^ 1).orderTop := by rw [pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
n₁ : n • x.orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop ≤ (x ^ n).orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop
n₂ : (x ^ n).orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop = (x ^ n).orderTop + x.orderTop
⊢ n • x.orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop ≤ (x ^ n * HPow.hPow (β := ℕ) x 1).orderTop
have n₃ : (x ^ n * x).orderTop ≤ (x ^ n * HPow.hPow (β := ℕ) x 1).orderTop
Tactic: calc
      n • x.orderTop + 1 • x.orderTop ≤ (x ^ n).orderTop + 1 • x.orderTop := by gcongr
      (x ^ n).orderTop + 1 • x.orderTop = (x ^ n).orderTop + x.orderTop := by rw [one_nsmul]
      (x ^ n).orderTop + x.orderTop ≤ (x ^ n * x).orderTop := orderTop_add_le_mul
      (x ^ n * x).orderTop ≤ (x ^ n * x ^ 1).orderTop := by rw [pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
⊢ n • x.orderTop ≤ (x ^ n).orderTop
have zero : HSMul.hSMul (α := ℕ) 0 x.orderTop ≤ (HPow.hPow (β := ℕ) x 0).orderTop
Tactic: induction n with
  | zero =>
    simp only [zero_smul, pow_zero]
    by_cases h : NeZero (1 : R)
    · simp
    · have : Subsingleton R := not_nontrivial_iff_subsingleton.mp fun _ ↦ h NeZero.one
      simp
  | succ n ih =>
    rw [add_nsmul, pow_add]
    calc
      n • x.orderTop + 1 • x.orderTop ≤ (x ^ n).orderTop + 1 • x.orderTop := by gcongr
      (x ^ n).orderTop + 1 • x.orderTop = (x ^ n).orderTop + x.orderTop := by rw [one_nsmul]
      (x ^ n).orderTop + x.orderTop ≤ (x ^ n * x).orderTop := orderTop_add_le_mul
      (x ^ n * x).orderTop ≤ (x ^ n * x ^ 1).orderTop := by rw [pow_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
zero : HSMul.hSMul (α := ℕ) 0 x.orderTop ≤ (HPow.hPow (β := ℕ) x 0).orderTop
⊢ n • x.orderTop ≤ (x ^ n).orderTop
have succ : ∀ (n : ℕ) (ih : n • x.orderTop ≤ (x ^ n).orderTop), (n + 1) • x.orderTop ≤ (x ^ (n + 1)).orderTop
Tactic: induction n with
  | zero =>
    simp only [zero_smul, pow_zero]
    by_cases h : NeZero (1 : R)
    · simp
    · have : Subsingleton R := not_nontrivial_iff_subsingleton.mp fun _ ↦ h NeZero.one
      simp
  | succ n ih =>
    rw [add_nsmul, pow_add]
    calc
      n • x.orderTop + 1 • x.orderTop ≤ (x ^ n).orderTop + 1 • x.orderTop := by gcongr
      (x ^ n).orderTop + 1 • x.orderTop = (x ^ n).orderTop + x.orderTop := by rw [one_nsmul]
      (x ^ n).orderTop + x.orderTop ≤ (x ^ n * x).orderTop := orderTop_add_le_mul
      (x ^ n * x).orderTop ≤ (x ^ n * x ^ 1).orderTop := by rw [pow_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : NonAssocRing R
inst_3 : Nontrivial R
x : R⟦Γ⟧
⊢ 0 < (x - 1).orderTop ↔ x.orderTop = 0 ∧ x.leadingCoeff = 1
have mp : 0 < (x - 1).orderTop → x.orderTop = 0 ∧ x.leadingCoeff = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : NonAssocRing R
inst_3 : Nontrivial R
x : R⟦Γ⟧
mp : 0 < (x - 1).orderTop → x.orderTop = 0 ∧ x.leadingCoeff = 1
⊢ 0 < (x - 1).orderTop ↔ x.orderTop = 0 ∧ x.leadingCoeff = 1
have mpr : x.orderTop = 0 ∧ x.leadingCoeff = 1 → 0 < (x - 1).orderTop
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : NonAssocRing R
inst_3 : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
⊢ x.orderTop = 0 ∧ x.leadingCoeff = 1
have mp : x.orderTop = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : NonAssocRing R
inst_3 : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
mp : x.orderTop = 0
⊢ x.orderTop = 0 ∧ x.leadingCoeff = 1
have mp₁ : x.leadingCoeff = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : NonAssocRing R
inst_3 : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
⊢ x.orderTop = 0
have mp : (1 + (x - 1)).orderTop = orderTop.{u_1, u_3} (R := R) 1
Tactic: rw [← sub_add_cancel x 1, add_comm, ← orderTop_one (R := R)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : NonAssocRing R
inst_3 : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
⊢ x.leadingCoeff = 1
have mp : (1 + (x - 1)).leadingCoeff = leadingCoeff.{u_1, u_3} (Γ := Γ) 1
Tactic: rw [← sub_add_cancel x 1, add_comm, ← leadingCoeff_one (Γ := Γ) (R := R)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : NonAssocRing R
inst_3 : Nontrivial R
x : R⟦Γ⟧
h : x.orderTop = 0 ∧ x.leadingCoeff = 1
⊢ 0 < (x - 1).orderTop
have mpr : x.leadingCoeff = leadingCoeff.{u_1, u_3} (Γ := Γ) 1
Tactic: refine lt_of_le_of_ne (le_of_eq_of_le (by simp_all)
      (min_orderTop_le_orderTop_sub (Γ := Γ) (R := R))) <| Ne.symm <|
      orderTop_sub_ne h.1 orderTop_one ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : NonAssocRing R
inst_3 : Nontrivial R
x : R⟦Γ⟧
h : x.orderTop = 0 ∧ x.leadingCoeff = 1
⊢ x.leadingCoeff = leadingCoeff.{u_1, u_3} (Γ := Γ) 1
have mpr : Eq.{u_3 + 1} (α := R) 1 (leadingCoeff.{u_1, u_3} (Γ := Γ) 1)
Tactic: rw [h.2, leadingCoeff_one]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : LinearOrder Γ
inst_1 : Zero Γ
inst_2 : NonAssocRing R
inst_3 : Nontrivial R
x : R⟦Γ⟧
h : x.orderTop = 0 ∧ x.leadingCoeff = 1
mpr : Eq.{u_3 + 1} (α := R) 1 (leadingCoeff.{u_1, u_3} (Γ := Γ) 1)
⊢ x.leadingCoeff = leadingCoeff.{u_1, u_3} (Γ := Γ) 1
have mpr₁ : Eq.{u_3 + 1} (α := R) 1 1
Tactic: rw [h.2, leadingCoeff_one]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero Γ
inst_2 : AddCommGroup R
inst_3 : One R
g : Γ
hg : 0 < g
r : R
⊢ 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop
have pos : ∀ (hr : r = 0), 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero Γ
inst_2 : AddCommGroup R
inst_3 : One R
g : Γ
hg : 0 < g
r : R
pos :
  ∀ (hr : r = 0), 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop
⊢ 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop
have neg : ∀ (hr : ¬r = 0), 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop
Tactic: by_cases hr : r = 0
-- 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 : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} x
hy : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y
⊢ Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} (x * y)
have inl : Subsingleton R → Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} (x * y)
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
x y : R⟦Γ⟧ˣ
hx : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} x
hy : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y
inl : Subsingleton R → Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} (x * y)
⊢ Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} (x * y)
have inr : Nontrivial R → Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} (x * y)
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
x y : R⟦Γ⟧ˣ
hx : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} x
hy : Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y
h : Nontrivial R
⊢ Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} (x * y)
have inr : ∀ (hx : (↑x : R⟦Γ⟧).orderTop = 0 ∧ (↑x : R⟦Γ⟧).leadingCoeff = 1)
  (hy : (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1),
  Nontrivial R → (↑(x * y) : R⟦Γ⟧).orderTop = 0 ∧ (↑(x * y) : R⟦Γ⟧).leadingCoeff = 1
Tactic: simp_all only [Set.mem_setOf_eq, orderTop_self_sub_one_pos_iff]
Cleared hypotheses: hx, hy, h
-- 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
⊢ (↑x : R⟦Γ⟧).leadingCoeff * (↑y : R⟦Γ⟧).leadingCoeff = 1
have rw : 1 * (↑y : R⟦Γ⟧).leadingCoeff = 1
Tactic: rw [hx.2, hy.2, mul_one]
-- 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
rw : 1 * (↑y : R⟦Γ⟧).leadingCoeff = 1
⊢ (↑x : R⟦Γ⟧).leadingCoeff * (↑y : R⟦Γ⟧).leadingCoeff = 1
have rw₁ : HMul.hMul (α := R) 1 1 = 1
Tactic: rw [hx.2, hy.2, mul_one]
-- 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
rw : 1 * (↑y : R⟦Γ⟧).leadingCoeff = 1
rw₁ : HMul.hMul (α := R) 1 1 = 1
⊢ (↑x : R⟦Γ⟧).leadingCoeff * (↑y : R⟦Γ⟧).leadingCoeff = 1
have rw₂ : Eq.{u_7 + 1} (α := R) 1 1
Tactic: rw [hx.2, hy.2, mul_one]
-- 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
x y : R⟦Γ⟧ˣ
hx : (↑x : R⟦Γ⟧).orderTop = 0 ∧ (↑x : R⟦Γ⟧).leadingCoeff = 1
hy : (↑y : R⟦Γ⟧).orderTop = 0 ∧ (↑y : R⟦Γ⟧).leadingCoeff = 1
h : Nontrivial R
⊢ (↑(x * y) : R⟦Γ⟧).orderTop = 0 ∧ (↑(x * y) : R⟦Γ⟧).leadingCoeff = 1
have h1 : (↑x : R⟦Γ⟧).leadingCoeff * (↑y : R⟦Γ⟧).leadingCoeff = 1
Tactic: have h1 : x.val.leadingCoeff * y.val.leadingCoeff = 1 := by rw [hx.2, hy.2, mul_one]
-- 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⟦Γ⟧).orderTop = 0 ∧ (↑(x * y) : R⟦Γ⟧).leadingCoeff = 1
have inr : (↑(x * y) : R⟦Γ⟧).orderTop = 0
Tactic: constructor
-- 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 * y) : R⟦Γ⟧).orderTop = 0
⊢ (↑(x * y) : R⟦Γ⟧).orderTop = 0 ∧ (↑(x * y) : R⟦Γ⟧).leadingCoeff = 1
have inr₁ : (↑(x * y) : R⟦Γ⟧).leadingCoeff = 1
Tactic: constructor
-- 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⟦Γ⟧).orderTop = 0
have inr : ((↑x : R⟦Γ⟧) * (↑y : R⟦Γ⟧)).orderTop = 0
Tactic: rw [Units.val_mul, orderTop_mul_of_ne_zero (by simp [h1]), hx.1, hy.1, add_zero]
-- 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⟦Γ⟧)).orderTop = 0
⊢ (↑(x * y) : R⟦Γ⟧).orderTop = 0
have inr₁ : (↑x : R⟦Γ⟧).orderTop + (↑y : R⟦Γ⟧).orderTop = 0
Tactic: rw [Units.val_mul, orderTop_mul_of_ne_zero (by simp [h1]), hx.1, hy.1, add_zero]
-- 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⟦Γ⟧)).orderTop = 0
inr₁ : (↑x : R⟦Γ⟧).orderTop + (↑y : R⟦Γ⟧).orderTop = 0
⊢ (↑(x * y) : R⟦Γ⟧).orderTop = 0
have inr₂ : 0 + (↑y : R⟦Γ⟧).orderTop = 0
Tactic: rw [Units.val_mul, orderTop_mul_of_ne_zero (by simp [h1]), hx.1, hy.1, add_zero]
-- 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⟦Γ⟧)).orderTop = 0
inr₁ : (↑x : R⟦Γ⟧).orderTop + (↑y : R⟦Γ⟧).orderTop = 0
inr₂ : 0 + (↑y : R⟦Γ⟧).orderTop = 0
⊢ (↑(x * y) : R⟦Γ⟧).orderTop = 0
have inr₃ : HAdd.hAdd (α := WithTop Γ) 0 0 = 0
Tactic: rw [Units.val_mul, orderTop_mul_of_ne_zero (by simp [h1]), hx.1, hy.1, add_zero]
-- 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⟦Γ⟧)).orderTop = 0
inr₁ : (↑x : R⟦Γ⟧).orderTop + (↑y : R⟦Γ⟧).orderTop = 0
inr₂ : 0 + (↑y : R⟦Γ⟧).orderTop = 0
inr₃ : HAdd.hAdd (α := WithTop Γ) 0 0 = 0
⊢ (↑(x * y) : R⟦Γ⟧).orderTop = 0
have inr₄ : Eq.{u_6 + 1} (α := WithTop Γ) 0 0
Tactic: rw [Units.val_mul, orderTop_mul_of_ne_zero (by simp [h1]), hx.1, hy.1, add_zero]