awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h_1 : Nontrivial R
⊢ IsUnit.{u_3} (M := R) 1

Tactic:
isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h_1 : Nontrivial R
⊢ IsUnit.{u_3} (M := R) 1

Tactic:
exact isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h_1 : Nontrivial R
⊢ x.orderTop = 0

Tactic:
have := (x.orderTop_self_sub_one_pos_iff.mp h).1
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h_1 : Nontrivial R
this : x.orderTop = 0
⊢ x.order = 0

Tactic:
rw [← order_eq_orderTop_of_ne_zero
        (fun h ↦ WithTop.top_ne_zero (orderTop_eq_top.mpr h ▸ this)), WithTop.coe_eq_zero] at this

Premises used: WithTop.coe_eq_zero, HahnSeries.order_eq_orderTop_of_ne_zero, WithTop.top_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h_1 : Nontrivial R
this : x.order = 0
inr : IsAddUnit.{u_1} (M := Γ) 0
⊢ IsAddUnit x.order

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h_1 : Nontrivial R
this : x.order = 0
⊢ IsAddUnit.{u_1} (M := Γ) 0

Tactic:
isAddUnit_zero

Premises used: isAddUnit_zero
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h_1 : Nontrivial R
this : x.order = 0
⊢ IsAddUnit.{u_1} (M := Γ) 0

Tactic:
exact isAddUnit_zero

Premises used: isAddUnit_zero
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
mp : IsUnit x → IsUnit x.leadingCoeff
mpr : IsUnit x.leadingCoeff → IsUnit x
⊢ IsUnit x ↔ IsUnit x.leadingCoeff

Tactic:
constructor
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
⊢ IsUnit (↑{ val := u, inv := i, val_inv := ui, inv_val := iu : R⟦Γ⟧ˣ } : R⟦Γ⟧).leadingCoeff

Tactic:
.of_mul_eq_one (i.leadingCoeff)
        ((coeff_mul_order_add_order u i).symm.trans ?_)

Premises used: IsUnit.of_mul_eq_one, HahnSeries.coeff_mul_order_add_order, HahnSeries.leadingCoeff, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
mp : (u * i).coeff (u.order + i.order) = 1
⊢ IsUnit (↑{ val := u, inv := i, val_inv := ui, inv_val := iu : R⟦Γ⟧ˣ } : R⟦Γ⟧).leadingCoeff

Tactic:
refine
      .of_mul_eq_one (i.leadingCoeff)
        ((coeff_mul_order_add_order u i).symm.trans ?_)
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
mp : u.order + i.order = 0
⊢ (u * i).coeff (u.order + i.order) = 1

Tactic:
rw [ui, coeff_one, if_pos]

Premises used: if_pos, HahnSeries.coeff_one
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
mp : (u * i).order = 0
mp₁ : Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0
mp₂ mp₃ : Eq.{u_1 + 1} (α := Γ) 0 0
⊢ u.order + i.order = 0

Tactic:
rw [← order_mul (left_ne_zero_of_mul_eq_one ui) (right_ne_zero_of_mul_eq_one ui), ui, order_one]

Premises used: HahnSeries.order_mul, right_ne_zero_of_mul_eq_one, HahnSeries.order_one, left_ne_zero_of_mul_eq_one
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * u = 1
hx : (↑{ val := u, inv := i, val_inv := ui, inv_val := iu : Rˣ } : R) = x.leadingCoeff
⊢ u = x.leadingCoeff

Tactic:
rw [Units.val_mk] at hx

Premises used: Units.val_mk
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * u = 1
hx : u = x.leadingCoeff
⊢ i * x.leadingCoeff = 1

Tactic:
rw [hx] at iu
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * u = 1
hx : u = x.leadingCoeff
iu₁ : i * x.leadingCoeff = 1
⊢ u = x.leadingCoeff

Tactic:
rw [hx] at iu
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
⊢ (1 - (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)) *
      (SummableFamily.powers (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)).hsum =
    1

Tactic:
have h :=
      SummableFamily.one_sub_self_mul_hsum_powers (unit_aux x iu _ (neg_add_cancel x.order))
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
h :
  (1 - (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)) *
      (SummableFamily.powers (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)).hsum =
    1
⊢ HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x *
      (SummableFamily.powers (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)).hsum =
    1

Tactic:
rw [sub_sub_cancel] at h

Premises used: sub_sub_cancel
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
h :
  HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x *
      (SummableFamily.powers (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)).hsum =
    1
⊢ IsUnit x

Tactic:
isUnit_of_mul_isUnit_right (.of_mul_eq_one _ h)

Premises used: IsUnit.of_mul_eq_one, isUnit_of_mul_isUnit_right
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
h :
  HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x *
      (SummableFamily.powers (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)).hsum =
    1
⊢ IsUnit x

Tactic:
exact isUnit_of_mul_isUnit_right (.of_mul_eq_one _ h)

Premises used: IsUnit.of_mul_eq_one, isUnit_of_mul_isUnit_right
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
a : Γ
r : R
inl : Eq (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) 0)⁻¹ ((single (-a) : (a : R) → R⟦Γ⟧) 0⁻¹)
inr :
  ∀ (hr : r ≠ 0), Eq (α := R⟦Γ⟧) (((single a : (a : R) → R⟦Γ⟧) r)⁻¹ : R⟦Γ⟧) ((single (-a) : (a : R) → R⟦Γ⟧) r⁻¹ : R⟦Γ⟧)
⊢ Eq (α := R⟦Γ⟧) (((single a : (a : R) → R⟦Γ⟧) r)⁻¹ : R⟦Γ⟧) ((single (-a) : (a : R) → R⟦Γ⟧) r⁻¹ : R⟦Γ⟧)

Tactic:
obtain rfl | hr := eq_or_ne r 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
a : Γ
⊢ Eq (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) 0)⁻¹ ((single (-a) : (a : R) → R⟦Γ⟧) 0⁻¹)

Tactic:
simp [inv_def]

Premises used: HahnSeries.inv_def
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
a : Γ
r : R
hr : r ≠ 0
⊢ Eq (α := R⟦Γ⟧) (((single a : (a : R) → R⟦Γ⟧) r)⁻¹ : R⟦Γ⟧) ((single (-a) : (a : R) → R⟦Γ⟧) r⁻¹ : R⟦Γ⟧)

Tactic:
simp [inv_def, hr]

Premises used: HahnSeries.inv_def
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
a b : Γ
r s : R
rw :
  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)
rw₁ :
  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)
rw₂ :
  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⁻¹)
rw₃ :
  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⁻¹)
rw₄ rw₅ :
  Eq (α := R⟦Γ⟧) ((single (a + -b) : (a : R) → R⟦Γ⟧) (r * s⁻¹) : R⟦Γ⟧)
    ((single (a + -b) : (a : R) → R⟦Γ⟧) (r * s⁻¹) : R⟦Γ⟧)
⊢ HDiv.hDiv (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧) =
    (single (a - b) : (a : R) → R⟦Γ⟧) (r / s)

Tactic:
rw [div_eq_mul_inv, sub_eq_add_neg, div_eq_mul_inv, inv_single, single_mul_single]

Premises used: HahnSeries.single_mul_single, sub_eq_add_neg, div_eq_mul_inv, HahnSeries.inv_single
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
⊢ (1 - (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)) *
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1

Tactic:
have h :=
      SummableFamily.one_sub_self_mul_hsum_powers
        (unit_aux x (inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr x0)) _ (neg_add_cancel x.order))
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
h :
  (1 - (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)) *
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1
⊢ HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x *
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1

Tactic:
rw [sub_sub_cancel] at h

Premises used: sub_sub_cancel
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
h :
  HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x *
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1
rw :
  x *
      HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧)
        (SummableFamily.powers
            (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1
rw₁ :
  HMul.hMul (β := R⟦Γ⟧) x ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) *
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1
rw₂ :
  HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x *
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1
rw₃ rw₄ : Eq (α := R⟦Γ⟧) 1 1
⊢ x * x⁻¹ = 1

Tactic:
rw [inv_def, ← mul_assoc, mul_comm x, h]

Premises used: mul_assoc, HahnSeries.inv_def, mul_comm
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
⊢ Eq (α := R⟦Γ⟧) 0⁻¹ 0

Tactic:
simp [inv_def]

Premises used: HahnSeries.inv_def
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
q : ℚ≥0
⊢ (↑q : R⟦Γ⟧) = HDiv.hDiv (α := R⟦Γ⟧) (↑q.num : R⟦Γ⟧) (↑q.den : R⟦Γ⟧)

Tactic:
simp [← single_zero_nnratCast, ← single_zero_natCast, NNRat.cast_def]

Premises used: HahnSeries.single_zero_natCast, NNRat.cast_def, HahnSeries.single_zero_nnratCast
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
q : ℚ≥0
x : R⟦Γ⟧
coeff : ∀ (x_1 : Γ), (q • x).coeff x_1 = ((↑q : R⟦Γ⟧) * x).coeff x_1
⊢ q • x = (↑q : R⟦Γ⟧) * x

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
q : ℚ≥0
x : R⟦Γ⟧
x_1 : Γ
⊢ (q • x).coeff x_1 = ((↑q : R⟦Γ⟧) * x).coeff x_1

Tactic:
simp [← single_zero_nnratCast, NNRat.smul_def]

Premises used: HahnSeries.single_zero_nnratCast, NNRat.smul_def
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
q : ℚ
⊢ (↑q : R⟦Γ⟧) = HDiv.hDiv (α := R⟦Γ⟧) (↑q.num : R⟦Γ⟧) (↑q.den : R⟦Γ⟧)

Tactic:
simp [← single_zero_ratCast, ← single_zero_intCast, ← single_zero_natCast, Rat.cast_def]

Premises used: HahnSeries.single_zero_natCast, HahnSeries.single_zero_intCast, Rat.cast_def, HahnSeries.single_zero_ratCast
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
q : ℚ
x : R⟦Γ⟧
coeff : ∀ (x_1 : Γ), (q • x).coeff x_1 = ((↑q : R⟦Γ⟧) * x).coeff x_1
⊢ q • x = (↑q : R⟦Γ⟧) * x

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
q : ℚ
x : R⟦Γ⟧
x_1 : Γ
⊢ (q • x).coeff x_1 = ((↑q : R⟦Γ⟧) * x).coeff x_1

Tactic:
simp [← single_zero_ratCast, Rat.smul_def]

Premises used: HahnSeries.single_zero_ratCast, Rat.smul_def
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
⊢ Eq (α := SMul ℚ≥0 R⟦Γ⟧) instSMul NNRat.smulDivisionSemiring

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
⊢ Eq (α := SMul ℚ R⟦Γ⟧) instSMul Rat.smulDivisionRing

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
m : ℕ
e : Bool
s : ℕ
⊢ Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (OfScientific.ofScientific m e s)) (OfScientific.ofScientific m e s)

Tactic:
simpa using single_zero_ratCast (Γ := Γ) (R := R) (OfScientific.ofScientific m e s)

Premises used: OfScientific.ofScientific, HahnSeries.single_zero_ratCast
-- Module: Mathlib.RingTheory.HahnSeries.Valuation
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
pos : ∀ (hx : x = 0), (x * y).orderTop = x.orderTop + y.orderTop
neg : ∀ (hx : ¬x = 0), (x * y).orderTop = x.orderTop + y.orderTop
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.HahnSeries.Valuation
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
hx : x = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.HahnSeries.Valuation
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
pos : ∀ (hy : y = 0), (x * y).orderTop = x.orderTop + y.orderTop
neg : ∀ (hy : ¬y = 0), (x * y).orderTop = x.orderTop + y.orderTop
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.HahnSeries.Valuation
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
hy : y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
simp [hy]
-- Module: Mathlib.RingTheory.HahnSeries.Valuation
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
neg : (x * y).orderTop = (↑x.order : WithTop Γ) + y.orderTop
neg₁ : (x * y).orderTop = (↑x.order : WithTop Γ) + (↑y.order : WithTop Γ)
neg₂ : (↑(x * y).order : WithTop Γ) = (↑x.order : WithTop Γ) + (↑y.order : WithTop Γ)
neg₃ : (↑(x * y).order : WithTop Γ) = (↑(x.order + y.order) : WithTop Γ)
neg₄ : (x * y).order = x.order + y.order
neg₅ neg₆ : x.order + y.order = x.order + y.order
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
rw [← order_eq_orderTop_of_ne_zero hx, ← order_eq_orderTop_of_ne_zero hy,
      ← order_eq_orderTop_of_ne_zero (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
      order_mul hx hy]

Premises used: HahnSeries.order_mul, WithTop.coe_eq_coe, HahnSeries.order_eq_orderTop_of_ne_zero, mul_ne_zero, WithTop.coe_add
-- Module: Mathlib.RingTheory.HahnSeries.Valuation
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x : R⟦Γ⟧
⊢ (addVal Γ R : (a : R⟦Γ⟧) → WithTop Γ) x = x.orderTop

Tactic:
AddValuation.of_apply _

Premises used: AddValuation.of_apply
-- Module: Mathlib.RingTheory.HahnSeries.Valuation
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x : R⟦Γ⟧
hx : x ≠ 0
⊢ (addVal Γ R : (a : R⟦Γ⟧) → WithTop Γ) x = (↑x.order : WithTop Γ)

Tactic:
addVal_apply.trans (order_eq_orderTop_of_ne_zero hx).symm

Premises used: HahnSeries.order_eq_orderTop_of_ne_zero, Eq.symm, HahnSeries.addVal_apply, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.Valuation
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
⊢ (addVal Γ R : (a : R⟦Γ⟧) → WithTop Γ) x ≤ (↑g : WithTop Γ)

Tactic:
orderTop_le_of_coeff_ne_zero h

Premises used: HahnSeries.orderTop, HahnSeries.orderTop_le_of_coeff_ne_zero, dite
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
map_nonunit : ∀ (a : R), IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I) → IsUnit a
⊢ IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h_1 : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
rw :
  ∀ (h : ∃ (b : R ⧸ I), HMul.hMul (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I) b = 1),
    ∃ (b : HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)),
      HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
          ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
          b =
        1
⊢ IsUnit (M := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
    ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))

Tactic:
rw [isUnit_iff_exists_inv] at *

Premises used: isUnit_iff_exists_inv
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h_1 : I ≤ Ideal.jacobson ⊥
a : R
h : ∃ (b : R ⧸ I), HMul.hMul (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I) b = 1
obtain :
  ∀ (b : R ⧸ I) (hb : HMul.hMul (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I) b = 1),
    ∃ (b : HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)),
      HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
          ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
          b =
        1
⊢ ∃ (b : HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)),
    HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
        ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
          HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
        b =
      1

Tactic:
obtain ⟨b, hb⟩ := h