awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
hx : LT.lt (α := ArchimedeanClass R) 0 (mk x)
y : S
hy : 0 < y
h : LT.lt.{u_1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x : ArchimedeanClass R)
hpos : LE.le.{u_1} (α := R) (0 : R) ((f : (a : S) → R) y : R)
⊢ x < (f : (a : S) → R) y

Tactic:
apply lt_of_mk_lt_mk_of_nonneg

Premises used: ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
hx : LT.lt (α := ArchimedeanClass R) 0 (mk x)
y : S
hy : 0 < y
h h₁ h₂ h₃ : LT.lt (α := ArchimedeanClass R) 0 (mk x)
⊢ LT.lt.{u_1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x : ArchimedeanClass R)

Tactic:
rwa [mk_map_of_archimedean' f hy.ne']

Premises used: LT.lt.ne', ArchimedeanClass.mk_map_of_archimedean'
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
hx : LT.lt (α := ArchimedeanClass R) 0 (mk x)
y : S
hy : 0 < y
⊢ LE.le.{u_1} (α := R) (0 : R) ((f : (a : S) → R) y : R)

Tactic:
simpa using f.monotone' hy.le

Premises used: LT.lt.le, OrderRingHom.monotone'
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
hx : LT.lt (α := ArchimedeanClass R) 0 (mk x)
y : S
hy : y < 0
h : LT.lt.{u_1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x : ArchimedeanClass R)
hneg : LE.le.{u_1} (α := R) ((f : (a : S) → R) y : R) (0 : R)
⊢ (f : (a : S) → R) y < x

Tactic:
apply lt_of_mk_lt_mk_of_nonpos

Premises used: ArchimedeanClass.lt_of_mk_lt_mk_of_nonpos
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
hx : LT.lt (α := ArchimedeanClass R) 0 (mk x)
y : S
hy : y < 0
h h₁ h₂ h₃ : LT.lt (α := ArchimedeanClass R) 0 (mk x)
⊢ LT.lt.{u_1} (α := ArchimedeanClass R) (mk ((f : (a : S) → R) y) : ArchimedeanClass R) (mk x : ArchimedeanClass R)

Tactic:
rwa [mk_map_of_archimedean' f hy.ne]

Premises used: ArchimedeanClass.mk_map_of_archimedean', LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
hx : LT.lt (α := ArchimedeanClass R) 0 (mk x)
y : S
hy : y < 0
⊢ LE.le.{u_1} (α := R) ((f : (a : S) → R) y : R) (0 : R)

Tactic:
simpa using f.monotone' hy.le

Premises used: LT.lt.le, OrderRingHom.monotone'
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
n : ℤ
h : n ≠ 0
inl : Subsingleton S → Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk (↑n : S)) 0
inr : Nontrivial S → Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk (↑n : S)) 0
⊢ Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk (↑n : S)) 0

Tactic:
obtain _ | _ := subsingleton_or_nontrivial S

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
n : ℤ
h : n ≠ 0
h_1 : Subsingleton S
⊢ Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk (↑n : S)) 0

Tactic:
Subsingleton.allEq ..

Premises used: Subsingleton.allEq
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
n : ℤ
h : n ≠ 0
h_1 : Subsingleton S
⊢ Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk (↑n : S)) 0

Tactic:
exact Subsingleton.allEq ..

Premises used: Subsingleton.allEq
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
n : ℤ
h : n ≠ 0
h_1 : Nontrivial S
x : ℤ
⊢ ∀ ⦃b : ℤ⦄,
    x ≤ b →
      OneHom.toFun ((↑(↑(Int.castRingHom S) : ℤ →* S) : OneHom ℤ S) : OneHom ℤ S) x ≤
        OneHom.toFun ((↑(↑(Int.castRingHom S) : ℤ →* S) : OneHom ℤ S) : OneHom ℤ S) b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
n : ℤ
h : n ≠ 0
h_1 : Nontrivial S
⊢ Eq.{u_3 + 1} (α := ArchimedeanClass S) (mk (↑n : S)) 0

Tactic:
exact mk_map_of_archimedean' ⟨Int.castRingHom S, fun _ ↦ by simp⟩ h

Premises used: Int.castRingHom, OrderRingHom.mk, ArchimedeanClass.mk_map_of_archimedean'
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
n : ℤ
inl : LE.le.{u_3} (α := ArchimedeanClass S) 0 (mk (↑0 : S))
inr : ∀ (hn : n ≠ 0), LE.le.{u_3} (α := ArchimedeanClass S) 0 (mk (↑n : S))
⊢ LE.le.{u_3} (α := ArchimedeanClass S) 0 (mk (↑n : S))

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
⊢ LE.le.{u_3} (α := ArchimedeanClass S) 0 (mk (↑0 : S))

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
S : Type u_3
inst : LinearOrder S
inst_1 : CommRing S
inst_2 : IsStrictOrderedRing S
n : ℤ
hn : n ≠ 0
inr inr₁ : LE.le.{u_3} (α := ArchimedeanClass S) 0 0
⊢ LE.le.{u_3} (α := ArchimedeanClass S) 0 (mk (↑n : S))

Tactic:
rw [mk_intCast hn]

Premises used: ArchimedeanClass.mk_intCast
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
obtain :
  ∀ (n : ℕ)
    (hn :
      |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x : ArchimedeanOrder R)| ≤
        HSMul.hSMul (β := R) n
          (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
                ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) 1 : ArchimedeanOrder R)| :
            R)),
    ∃ (n : ℕ), x ≤ (↑n : R)
⊢ ∃ (n : ℕ), x ≤ (↑n : R)

Tactic:
obtain ⟨n, hn⟩ := hx
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) 1 : ArchimedeanOrder R)| :
        R)
⊢ ∃ (n : ℕ), x ≤ (↑n : R)

Tactic:
⟨n, le_of_abs_le ?_⟩

Premises used: le_of_abs_le, Exists.intro
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) 1 : ArchimedeanOrder R)| :
        R)
refine : |x| ≤ (↑n : R)
⊢ ∃ (n : ℕ), x ≤ (↑n : R)

Tactic:
refine ⟨n, le_of_abs_le ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
        ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) x : ArchimedeanOrder R)| ≤
    HSMul.hSMul (β := R) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder R) → R)
            ((ArchimedeanOrder.of : (a : R) → ArchimedeanOrder R) 1 : ArchimedeanOrder R)| :
        R)
⊢ |x| ≤ (↑n : R)

Tactic:
simpa using hn
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
obtain : ∀ (n : ℕ) (hn : x ≤ (↑n : R)), ∃ (n : ℕ), x < (↑n : R)
⊢ ∃ (n : ℕ), x < (↑n : R)

Tactic:
obtain ⟨n, hn⟩ := exists_nat_ge_of_mk_nonneg hx

Premises used: ArchimedeanClass.exists_nat_ge_of_mk_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : x ≤ (↑n : R)
⊢ ∃ (n : ℕ), x < (↑n : R)

Tactic:
⟨n + 1, hn.trans_lt ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat, LE.le.trans_lt
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : x ≤ (↑n : R)
refine : LT.lt.{u_1} (α := R) (↑n : R) (↑(n + 1) : R)
⊢ ∃ (n : ℕ), x < (↑n : R)

Tactic:
refine ⟨n + 1, hn.trans_lt ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : x ≤ (↑n : R)
⊢ LT.lt.{u_1} (α := R) (↑n : R) (↑(n + 1) : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
obtain : ∀ (n : ℕ) (hn : x ≤ (↑n : R)), ∃ (n : ℤ), x ≤ (↑n : R)
⊢ ∃ (n : ℤ), x ≤ (↑n : R)

Tactic:
obtain ⟨n, hn⟩ := exists_nat_ge_of_mk_nonneg hx

Premises used: ArchimedeanClass.exists_nat_ge_of_mk_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : x ≤ (↑n : R)
⊢ ∃ (n : ℤ), x ≤ (↑n : R)

Tactic:
⟨n, mod_cast hn⟩

Premises used: Int.cast_natCast, congrArg, cast, LE.le, Nat.cast, Exists.intro, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : x ≤ (↑n : R)
⊢ ∃ (n : ℤ), x ≤ (↑n : R)

Tactic:
exact ⟨n, mod_cast hn⟩
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
obtain : ∀ (n : ℕ) (hn : x < (↑n : R)), ∃ (n : ℤ), x < (↑n : R)
⊢ ∃ (n : ℤ), x < (↑n : R)

Tactic:
obtain ⟨n, hn⟩ := exists_nat_gt_of_mk_nonneg hx

Premises used: ArchimedeanClass.exists_nat_gt_of_mk_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : x < (↑n : R)
⊢ ∃ (n : ℤ), x < (↑n : R)

Tactic:
⟨n, mod_cast hn⟩

Premises used: Int.cast_natCast, congrArg, cast, Nat.cast, LT.lt, Exists.intro, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : x < (↑n : R)
⊢ ∃ (n : ℤ), x < (↑n : R)

Tactic:
exact ⟨n, mod_cast hn⟩
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
obtain : ∀ (n : ℕ) (hn : -x ≤ (↑n : R)), ∃ (n : ℤ), (↑n : R) ≤ x
⊢ ∃ (n : ℤ), (↑n : R) ≤ x

Tactic:
obtain ⟨n, hn⟩ := exists_nat_ge_of_mk_nonneg (mk_neg x ▸ hx)

Premises used: ArchimedeanClass.exists_nat_ge_of_mk_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : -x ≤ (↑n : R)
h : (↑(-(↑n : ℤ)) : R) ≤ x
⊢ ∃ (n : ℤ), (↑n : R) ≤ x

Tactic:
use -n
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : -x ≤ (↑n : R)
⊢ (↑(-(↑n : ℤ)) : R) ≤ x

Tactic:
simpa [neg_le]

Premises used: neg_le
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
obtain : ∀ (n : ℕ) (hn : -x < (↑n : R)), ∃ (n : ℤ), (↑n : R) < x
⊢ ∃ (n : ℤ), (↑n : R) < x

Tactic:
obtain ⟨n, hn⟩ := exists_nat_gt_of_mk_nonneg (mk_neg x ▸ hx)

Premises used: ArchimedeanClass.exists_nat_gt_of_mk_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : -x < (↑n : R)
h : (↑(-(↑n : ℤ)) : R) < x
⊢ ∃ (n : ℤ), (↑n : R) < x

Tactic:
use -n
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x : R
hx : LE.le (α := ArchimedeanClass R) 0 (mk x)
n : ℕ
hn : -x < (↑n : R)
⊢ (↑(-(↑n : ℤ)) : R) < x

Tactic:
simpa [neg_lt]

Premises used: neg_lt
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
r s : S
hr : (f : (a : S) → R) r ≤ x
hs : x ≤ (f : (a : S) → R) s
apply :
  LE.le.{u_1} (α := ArchimedeanClass R) (0 : ArchimedeanClass R)
    (min (mk ((f : (a : S) → R) r)) (mk ((f : (a : S) → R) s)) : ArchimedeanClass R)
⊢ LE.le (α := ArchimedeanClass R) 0 (mk x)

Tactic:
apply (min_le_mk_of_le_of_le hr hs).trans'

Premises used: ArchimedeanClass.min_le_mk_of_le_of_le, LE.le.trans'
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
S : Type u_3
inst_3 : LinearOrder S
inst_4 : CommRing S
inst_5 : IsStrictOrderedRing S
inst_6 : Archimedean S
f : S →+*o R
x : R
r s : S
hr : (f : (a : S) → R) r ≤ x
hs : x ≤ (f : (a : S) → R) s
⊢ LE.le.{u_1} (α := ArchimedeanClass R) (0 : ArchimedeanClass R)
    (min (mk ((f : (a : S) → R) r)) (mk ((f : (a : S) → R) s)) : ArchimedeanClass R)

Tactic:
simp [mk_map_nonneg_of_archimedean]

Premises used: ArchimedeanClass.mk_map_nonneg_of_archimedean
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x y z : ArchimedeanClass R
hx : x ≠ ⊤
h : x + y = x + z
⊢ y = z

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x y z : ArchimedeanClass R
hx : x ≠ ⊤
h : y + x = z + x
⊢ x + y = x + z

Tactic:
simp_rw [← add_comm x] at h

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x y z : ArchimedeanClass R
hx : x ≠ ⊤
h : x + y = x + z
⊢ y = z

Tactic:
add_left_cancel_of_ne_top hx h

Premises used: ArchimedeanClass.add_left_cancel_of_ne_top
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : CommRing R
inst_2 : IsStrictOrderedRing R
x y z : ArchimedeanClass R
hx : x ≠ ⊤
h : x + y = x + z
⊢ y = z

Tactic:
exact add_left_cancel_of_ne_top hx h

Premises used: ArchimedeanClass.add_left_cancel_of_ne_top
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
q : R
⊢ LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q

Tactic:
simpa using hf.lt_iff_lt (a := 0)

Premises used: StrictMono.lt_iff_lt
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q

Tactic:
have H {q} : 0 < f q ↔ 0 < q := by simpa using hf.lt_iff_lt (a := 0)
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
mp :
  LE.le (α := ArchimedeanClass S) (mk x) (mk y) →
    ∃ (q : R),
      LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
mpr :
  (∃ (q : R),
      LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|) →
    LE.le (α := ArchimedeanClass S) (mk x) (mk y)
⊢ LE.le (α := ArchimedeanClass S) (mk x) (mk y) ↔
    ∃ (q : R),
      LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
        ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) y : ArchimedeanOrder S)| ≤
    HSMul.hSMul (α := ℕ) (β := S) 0
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
            ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) x : ArchimedeanOrder S)| :
        S)
⊢ ∃ (q : R),
    LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|

Tactic:
simp_all [exists_zero_lt]

Premises used: exists_zero_lt
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
        ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) y : ArchimedeanOrder S)| ≤
    HSMul.hSMul (β := S) (n + 1)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
            ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) x : ArchimedeanOrder S)| :
        S)
mp :
  ∀ (q : R) (hq₀ : 0 < q) (hq : (n + 1) • q < 1),
    ∃ (q : R),
      LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|
⊢ ∃ (q : R),
    LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|

Tactic:
obtain ⟨q, hq₀, hq⟩ := exists_nsmul_lt_of_pos (one_pos (α := R)) (n + 1)

Premises used: exists_nsmul_lt_of_pos, HAdd.hAdd, OfNat.ofNat, one_pos
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
        ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) y : ArchimedeanOrder S)| ≤
    HSMul.hSMul (β := S) (n + 1)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
            ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) x : ArchimedeanOrder S)| :
        S)
q : R
hq₀ : 0 < q
hq : (n + 1) • q < 1
⊢ ∃ (q : R),
    LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|

Tactic:
⟨q, H.2 hq₀, le_of_mul_le_mul_left ?_ n.cast_add_one_pos⟩

Premises used: Iff.mpr, Nat.cast_add_one_pos, le_of_mul_le_mul_left, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
        ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) y : ArchimedeanOrder S)| ≤
    HSMul.hSMul (β := S) (n + 1)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
            ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) x : ArchimedeanOrder S)| :
        S)
q : R
hq₀ : 0 < q
hq : (n + 1) • q < 1
mp :
  HAdd.hAdd (α := S) (↑n : S) 1 * HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ HAdd.hAdd (α := S) (↑n : S) 1 * |x|
⊢ ∃ (q : R),
    LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ∧ HMul.hMul (α := S) ((f : (a : R) → S) q : S) |y| ≤ |x|

Tactic:
refine ⟨q, H.2 hq₀, le_of_mul_le_mul_left ?_ n.cast_add_one_pos⟩
-- Module: Mathlib.Algebra.Order.Ring.Archimedean
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : IsStrictOrderedRing R
inst_4 : Ring S
inst_5 : IsStrictOrderedRing S
inst_6 : DenselyOrdered R
inst_7 : Archimedean R
x y : S
f : R →+* S
hf : StrictMono.{u_1, u_2} (α := R) (β := S) (⇑f : (a : R) → S)
H : ∀ {q : R}, LT.lt.{u_2} (α := S) (0 : S) ((f : (a : R) → S) q : S) ↔ 0 < q
n : ℕ
hn :
  |(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
        ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) y : ArchimedeanOrder S)| ≤
    HSMul.hSMul (β := S) (n + 1)
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder S) → S)
            ((ArchimedeanOrder.of : (a : S) → ArchimedeanOrder S) x : ArchimedeanOrder S)| :
        S)
q : R
hq₀ : 0 < q
hq : (n + 1) • q < 1
⊢ LE.le.{u_2} (α := S) (0 : S) ((f : (a : R) → S) 1 : S)

Tactic:
simp