awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : NonUnitalCommSemiring R
x y : R⟦Γ⟧
coeff : ∀ (x_1 : Γ), (x * y).coeff x_1 = (y * x).coeff x_1
⊢ x * y = y * x

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 : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalCommSemiring R
x y : R⟦Γ⟧
x_1 : Γ
coeff :
  Eq.{u_3 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ x_1, x.coeff ij.1 * y.coeff ij.2)
    (∑ x_2 ∈ addAntidiagonal (s := y.support) (t := x.support) ⋯ ⋯ x_1, x.coeff x_2.2 * y.coeff x_2.1)
⊢ (x * y).coeff x_1 = (y * x).coeff x_1

Tactic:
simp_rw [coeff_mul, mul_comm]

Premises used: HahnSeries.coeff_mul, mul_comm
-- 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 : NonUnitalCommSemiring R
x y : R⟦Γ⟧
x_1 : Γ
⊢ ∀ i ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ x_1,
    x.coeff i.1 * y.coeff i.2 =
      x.coeff ((Equiv.prodComm Γ Γ : (a : Γ × Γ) → Γ × Γ) i).2 *
        y.coeff ((Equiv.prodComm Γ Γ : (a : Γ × Γ) → Γ × Γ) i).1

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 : NonUnitalCommSemiring R
x y : R⟦Γ⟧
x_1 : Γ
⊢ Eq.{u_3 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ x_1, x.coeff ij.1 * y.coeff ij.2)
    (∑ x_2 ∈ addAntidiagonal (s := y.support) (t := x.support) ⋯ ⋯ x_1, x.coeff x_2.2 * y.coeff x_2.1)

Tactic:
exact Finset.sum_equiv (Equiv.prodComm _ _) (fun _ ↦ swap_mem_addAntidiagonal.symm) <| by simp

Premises used: Equiv.prodComm, Finset.swap_mem_addAntidiagonal, Finset.sum_equiv, Iff.symm
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
zero : LE.le.{u_1} (α := WithTop Γ) 0 (orderTop.{u_1, u_3} (R := R) 1)
⊢ HSMul.hSMul (α := ℕ) 0 x.orderTop ≤ (HPow.hPow (β := ℕ) x 0).orderTop

Tactic:
simp only [zero_smul, pow_zero]

Premises used: pow_zero, zero_smul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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)
neg : ∀ (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)

Tactic:
by_cases h : NeZero (1 : R)

Premises used: NeZero, OfNat.ofNat
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
⊢ Subsingleton R

Tactic:
have : Subsingleton R := not_nontrivial_iff_subsingleton.mp fun _ ↦ h NeZero.one
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
this : Subsingleton R
⊢ LE.le.{u_1} (α := WithTop Γ) 0 (orderTop.{u_1, u_3} (R := R) 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
succ : n • x.orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop ≤ (x ^ n * HPow.hPow (β := ℕ) x 1).orderTop
⊢ (n + 1) • x.orderTop ≤ (x ^ (n + 1)).orderTop

Tactic:
rw [add_nsmul, pow_add]

Premises used: pow_add, add_nsmul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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).orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop

Tactic:
gcongr
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
rw rw₁ : (x ^ n).orderTop + x.orderTop = (x ^ n).orderTop + x.orderTop
⊢ (x ^ n).orderTop + HSMul.hSMul (α := ℕ) 1 x.orderTop = (x ^ n).orderTop + x.orderTop

Tactic:
rw [one_nsmul]

Premises used: one_nsmul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 + x.orderTop ≤ (x ^ n * x).orderTop

Tactic:
orderTop_add_le_mul

Premises used: HahnSeries.orderTop_add_le_mul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
rw rw₁ : (x ^ n * x).orderTop ≤ (x ^ n * x).orderTop
⊢ (x ^ n * x).orderTop ≤ (x ^ n * HPow.hPow (β := ℕ) x 1).orderTop

Tactic:
rw [pow_one]

Premises used: pow_one
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 ^ n * x).orderTop ≤ (x ^ n * HPow.hPow (β := ℕ) x 1).orderTop
⊢ n • x.orderTop + HSMul.hSMul (α := ℕ) 1 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]

Premises used: HMul.hMul, HahnSeries.orderTop, HPow.hPow, HahnSeries.orderTop_add_le_mul, OfNat.ofNat
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
succ : ∀ (n : ℕ) (ih : n • x.orderTop ≤ (x ^ n).orderTop), (n + 1) • x.orderTop ≤ (x ^ (n + 1)).orderTop
⊢ n • x.orderTop ≤ (x ^ n).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]

Premises used: HMul.hMul, HahnSeries.orderTop, pow_add, pow_zero, zero_smul, HPow.hPow, HahnSeries.orderTop_add_le_mul, NeZero, OfNat.ofNat, add_nsmul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
mpr : x.orderTop = 0 ∧ x.leadingCoeff = 1 → 0 < (x - 1).orderTop
⊢ 0 < (x - 1).orderTop ↔ x.orderTop = 0 ∧ x.leadingCoeff = 1

Tactic:
constructor
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
mp₁ : x.leadingCoeff = 1
⊢ x.orderTop = 0 ∧ x.leadingCoeff = 1

Tactic:
constructor
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : (1 + (x - 1)).orderTop = orderTop.{u_1, u_3} (R := R) 1
⊢ x.orderTop = 0

Tactic:
rw [← sub_add_cancel x 1, add_comm, ← orderTop_one (R := R)]

Premises used: HahnSeries.orderTop_one, add_comm, OfNat.ofNat, sub_add_cancel
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
⊢ (1 + (x - 1)).orderTop = orderTop.{u_1, u_3} (R := R) 1

Tactic:
orderTop_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)

Premises used: HahnSeries.orderTop_one, Eq.rec, HahnSeries.orderTop_add_eq_left, Eq.symm
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
⊢ (1 + (x - 1)).orderTop = orderTop.{u_1, u_3} (R := R) 1

Tactic:
exact orderTop_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)

Premises used: HahnSeries.orderTop_add_eq_left
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : (1 + (x - 1)).leadingCoeff = leadingCoeff.{u_1, u_3} (Γ := Γ) 1
⊢ x.leadingCoeff = 1

Tactic:
rw [← sub_add_cancel x 1, add_comm, ← leadingCoeff_one (Γ := Γ) (R := R)]

Premises used: add_comm, HahnSeries.leadingCoeff_one, OfNat.ofNat, sub_add_cancel
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
⊢ (1 + (x - 1)).leadingCoeff = leadingCoeff.{u_1, u_3} (Γ := Γ) 1

Tactic:
leadingCoeff_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)

Premises used: HahnSeries.orderTop_one, Eq.rec, Eq.symm, HahnSeries.leadingCoeff_add_eq_left
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
⊢ (1 + (x - 1)).leadingCoeff = leadingCoeff.{u_1, u_3} (Γ := Γ) 1

Tactic:
exact leadingCoeff_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)

Premises used: HahnSeries.leadingCoeff_add_eq_left
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 = min x.orderTop (orderTop.{u_1, u_3} (R := R) 1)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : x.leadingCoeff = leadingCoeff.{u_1, u_3} (Γ := Γ) 1
⊢ 0 < (x - 1).orderTop

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 ?_

Premises used: HahnSeries.orderTop_one, HahnSeries.orderTop_sub_ne, Ne.symm, And.left, le_of_eq_of_le, HahnSeries.min_orderTop_le_orderTop_sub, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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)
mpr₁ mpr₂ : Eq.{u_3 + 1} (α := R) 1 1
⊢ x.leadingCoeff = leadingCoeff.{u_1, u_3} (Γ := Γ) 1

Tactic:
rw [h.2, leadingCoeff_one]

Premises used: And.right, HahnSeries.leadingCoeff_one
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
neg :
  ∀ (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

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
hr : r = 0
⊢ 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop

Tactic:
simp [hr, hg]
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
hr : ¬r = 0
⊢ 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop

Tactic:
simp [hr, hg]
-- 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
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)
inr : Nontrivial 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)

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- 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
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 : Subsingleton R
⊢ Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} (x * y)

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
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
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
⊢ Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} (x * y)

Tactic:
simp_all only [Set.mem_setOf_eq, orderTop_self_sub_one_pos_iff]

Premises used: Set.mem_setOf_eq, 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
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
rw₂ rw₃ : Eq.{u_7 + 1} (α := R) 1 1
⊢ (↑x : R⟦Γ⟧).leadingCoeff * (↑y : R⟦Γ⟧).leadingCoeff = 1

Tactic:
rw [hx.2, hy.2, mul_one]

Premises used: And.right, mul_one
-- 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
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

Tactic:
have h1 : x.val.leadingCoeff * y.val.leadingCoeff = 1 := by rw [hx.2, hy.2, mul_one]
-- 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
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
inr₁ : (↑(x * y) : R⟦Γ⟧).leadingCoeff = 1
⊢ (↑(x * y) : R⟦Γ⟧).orderTop = 0 ∧ (↑(x * y) : R⟦Γ⟧).leadingCoeff = 1

Tactic:
constructor
-- 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
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 : R⟦Γ⟧).leadingCoeff * (↑y : R⟦Γ⟧).leadingCoeff ≠ 0

Tactic:
simp [h1]
-- 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
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
inr₄ inr₅ : Eq.{u_6 + 1} (α := WithTop Γ) 0 0
⊢ (↑(x * y) : R⟦Γ⟧).orderTop = 0

Tactic:
rw [Units.val_mul, orderTop_mul_of_ne_zero (by simp [h1]), hx.1, hy.1, add_zero]

Premises used: HahnSeries.orderTop_mul_of_ne_zero, And.left, add_zero, Units.val_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
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
inr₂ inr₃ : Eq.{u_7 + 1} (α := R) 1 1
⊢ (↑(x * y) : R⟦Γ⟧).leadingCoeff = 1

Tactic:
rw [Units.val_mul, leadingCoeff_mul_of_ne_zero (h1 ▸ one_ne_zero), h1]

Premises used: HahnSeries.leadingCoeff_mul_of_ne_zero, Units.val_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
⊢ Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} 1

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
this : 0 < (y.inv - 1).orderTop
⊢ Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y⁻¹

Tactic:
this

Premises used: Set.Mem, setOf
-- 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
this : 0 < (y.inv - 1).orderTop
⊢ Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y⁻¹

Tactic:
exact this
-- 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
suffices : 0 < (y.inv - 1).orderTop
⊢ Membership.mem (γ := Set R⟦Γ⟧ˣ) {x : R⟦Γ⟧ˣ | 0 < ((↑x : R⟦Γ⟧) - 1).orderTop} y⁻¹

Tactic:
suffices 0 < (y.inv - 1).orderTop by exact this
-- 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
inl : Subsingleton R → 0 < (y.inv - 1).orderTop
inr : Nontrivial R → 0 < (y.inv - 1).orderTop
⊢ 0 < (y.inv - 1).orderTop

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- 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 : Subsingleton R
⊢ 0 < (y.inv - 1).orderTop

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
⊢ 0 < ((↑y : R⟦Γ⟧) - 1).orderTop

Tactic:
have : 0 < (y.val - 1).orderTop := h