awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
b : ℤ
hb : x < (↑b : K)
hn : Set.Nonempty (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
refine : ∀ (r : ℝ) (hr : Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} r), (↑a : ℝ) ≤ r
⊢ BddBelow (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}

Tactic:
refine ⟨a, fun r hr ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
b : ℤ
hb : x < (↑b : K)
hn : Set.Nonempty (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
r : ℝ
hr : Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} r
by_contra! : ∀ (hra : r < (↑a : ℝ)), False
⊢ (↑a : ℝ) ≤ r

Tactic:
by_contra! hra
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
b : ℤ
hb : x < (↑b : K)
hn : Set.Nonempty (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
r : ℝ
hr : Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} r
hra : r < (↑a : ℝ)
⊢ (↑(↑f.toRingHom : ℝ →* K) : OneHom ℝ K).toFun (↑a : ℝ) < (↑(↑f.toRingHom : ℝ →* K) : OneHom ℝ K).toFun r

Tactic:
simpa using ha.trans hr

Premises used: LT.lt.trans
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
b : ℤ
hb : x < (↑b : K)
hn : Set.Nonempty (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
r : ℝ
hr : Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} r
hra : r < (↑a : ℝ)
⊢ False

Tactic:
exact (f.monotone' hra.le).not_gt (by simpa using ha.trans hr)

Premises used: LT.lt.le, OrderRingHom.monotone', LE.le.not_gt
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
b : ℤ
hb : x < (↑b : K)
hn : Set.Nonempty (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
⊢ BddBelow (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}

Tactic:
have hb : BddBelow {r | x < f r} := by
      refine ⟨a, fun r hr ↦ ?_⟩
      by_contra! hra
      exact (f.monotone' hra.le).not_gt (by simpa using ha.trans hr)
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
b : ℤ
hb_1 : x < (↑b : K)
hn : Set.Nonempty (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
hb : BddBelow (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
inl : ∀ s < sInf {r : ℝ | x < (f : (a : ℝ) → K) r}, (f : (a : ℝ) → K) s ≤ x
inl₁ : ∀ s > sInf {r : ℝ | x < (f : (a : ℝ) → K) r}, x ≤ (f : (a : ℝ) → K) s
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}

Tactic:
apply stdPart_eq f

Premises used: ArchimedeanClass.stdPart_eq
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
b : ℤ
hb_1 : x < (↑b : K)
hn : Set.Nonempty (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
hb : BddBelow (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
r : ℝ
hr : r < sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
⊢ (f : (a : ℝ) → K) r ≤ x

Tactic:
simpa using notMem_of_lt_csInf hr hb

Premises used: notMem_of_lt_csInf
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
b : ℤ
hb_1 : x < (↑b : K)
hn : Set.Nonempty (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
hb : BddBelow (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
r : ℝ
hr : r > sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
inl :
  ∀ (s : ℝ) (hs : Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} s) (hs' : s < r),
    x ≤ (f : (a : ℝ) → K) r
⊢ x ≤ (f : (a : ℝ) → K) r

Tactic:
obtain ⟨s, hs, hs'⟩ := (csInf_lt_iff hb hn).1 hr

Premises used: csInf_lt_iff, Iff.mp
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
b : ℤ
hb_1 : x < (↑b : K)
hn : Set.Nonempty (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
hb : BddBelow (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
r : ℝ
hr : r > sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
s : ℝ
hs : Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} s
hs' : s < r
⊢ x ≤ (f : (a : ℝ) → K) r

Tactic:
hs.le.trans (f.monotone' hs'.le)

Premises used: LT.lt.le, OrderRingHom.monotone', LE.le.trans
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
b : ℤ
hb_1 : x < (↑b : K)
hn : Set.Nonempty (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
hb : BddBelow (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
r : ℝ
hr : r > sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
s : ℝ
hs : Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} s
hs' : s < r
⊢ x ≤ (f : (a : ℝ) → K) r

Tactic:
exact hs.le.trans (f.monotone' hs'.le)

Premises used: LT.lt.le, OrderRingHom.monotone', LE.le.trans
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LT.lt (α := ArchimedeanClass K) (mk x) 0
inr : Eq (α := ℝ) 0 (sInf {r : ℝ | x < (f : (a : ℝ) → K) r})
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}

Tactic:
rw [stdPart_of_mk_ne_zero hx.ne]

Premises used: ArchimedeanClass.stdPart_of_mk_ne_zero, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LT.lt (α := ArchimedeanClass K) (mk x) 0
⊢ ∀ {r : ℝ}, LT.lt (α := ArchimedeanClass K) (mk x) (mk ((f : (a : ℝ) → K) r))

Tactic:
have hr {r} := hx.trans_le (mk_map_nonneg_of_archimedean f r)
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LT.lt (α := ArchimedeanClass K) (mk x) 0
hr : ∀ {r : ℝ}, LT.lt (α := ArchimedeanClass K) (mk x) (mk ((f : (a : ℝ) → K) r))
inr : ∀ (h : 0 ≤ x), Eq (α := ℝ) 0 (sInf {r : ℝ | x < (f : (a : ℝ) → K) r})
inr₁ : ∀ (h : x < 0), Eq (α := ℝ) 0 (sInf {r : ℝ | x < (f : (a : ℝ) → K) r})
⊢ Eq (α := ℝ) 0 (sInf {r : ℝ | x < (f : (a : ℝ) → K) r})

Tactic:
obtain h | h := le_or_gt 0 x

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LT.lt (α := ArchimedeanClass K) (mk x) 0
hr : ∀ {r : ℝ}, LT.lt (α := ArchimedeanClass K) (mk x) (mk ((f : (a : ℝ) → K) r))
h : 0 ≤ x
⊢ Eq (α := ℝ) 0 (sInf ∅)

Tactic:
Real.sInf_empty.symm

Premises used: Real.sInf_empty, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LT.lt (α := ArchimedeanClass K) (mk x) 0
hr : ∀ {r : ℝ}, LT.lt (α := ArchimedeanClass K) (mk x) (mk ((f : (a : ℝ) → K) r))
h : 0 ≤ x
h₁ : Eq (α := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} ∅
⊢ Eq (α := ℝ) 0 (sInf {r : ℝ | x < (f : (a : ℝ) → K) r})

Tactic:
convert! Real.sInf_empty.symm

Premises used: Real.sInf_empty, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LT.lt (α := ArchimedeanClass K) (mk x) 0
hr : ∀ {r : ℝ}, LT.lt (α := ArchimedeanClass K) (mk x) (mk ((f : (a : ℝ) → K) r))
h : 0 ≤ x
h₁ : ∀ (x_1 : ℝ), x_1 ∉ {r : ℝ | x < (f : (a : ℝ) → K) r}
⊢ Eq (α := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LT.lt (α := ArchimedeanClass K) (mk x) 0
hr : ∀ {r : ℝ}, LT.lt (α := ArchimedeanClass K) (mk x) (mk ((f : (a : ℝ) → K) r))
h : 0 ≤ x
⊢ ∀ (x_1 : ℝ), x_1 ∉ {r : ℝ | x < (f : (a : ℝ) → K) r}

Tactic:
fun r ↦ (lt_of_mk_lt_mk_of_nonneg hr h).not_gt

Premises used: Set.Mem, setOf, LT.lt.not_gt, ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LT.lt (α := ArchimedeanClass K) (mk x) 0
hr : ∀ {r : ℝ}, LT.lt (α := ArchimedeanClass K) (mk x) (mk ((f : (a : ℝ) → K) r))
h : 0 ≤ x
⊢ ∀ (x_1 : ℝ), x_1 ∉ {r : ℝ | x < (f : (a : ℝ) → K) r}

Tactic:
exact fun r ↦ (lt_of_mk_lt_mk_of_nonneg hr h).not_gt

Premises used: LT.lt.not_gt, ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LT.lt (α := ArchimedeanClass K) (mk x) 0
hr : ∀ {r : ℝ}, LT.lt (α := ArchimedeanClass K) (mk x) (mk ((f : (a : ℝ) → K) r))
h : x < 0
⊢ Eq (α := ℝ) 0 (sInf Set.univ)

Tactic:
Real.sInf_univ.symm

Premises used: Real.sInf_univ, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LT.lt (α := ArchimedeanClass K) (mk x) 0
hr : ∀ {r : ℝ}, LT.lt (α := ArchimedeanClass K) (mk x) (mk ((f : (a : ℝ) → K) r))
h : x < 0
h₁ : Eq (α := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} Set.univ
⊢ Eq (α := ℝ) 0 (sInf {r : ℝ | x < (f : (a : ℝ) → K) r})

Tactic:
convert! Real.sInf_univ.symm

Premises used: Real.sInf_univ, Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LT.lt (α := ArchimedeanClass K) (mk x) 0
hr : ∀ {r : ℝ}, LT.lt (α := ArchimedeanClass K) (mk x) (mk ((f : (a : ℝ) → K) r))
h : x < 0
h₁ : ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} x_1
⊢ Eq (α := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LT.lt (α := ArchimedeanClass K) (mk x) 0
hr : ∀ {r : ℝ}, LT.lt (α := ArchimedeanClass K) (mk x) (mk ((f : (a : ℝ) → K) r))
h : x < 0
⊢ ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} x_1

Tactic:
fun r ↦ lt_of_mk_lt_mk_of_nonpos hr h.le

Premises used: Set.Mem, setOf, LT.lt.le, ArchimedeanClass.lt_of_mk_lt_mk_of_nonpos
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LT.lt (α := ArchimedeanClass K) (mk x) 0
hr : ∀ {r : ℝ}, LT.lt (α := ArchimedeanClass K) (mk x) (mk ((f : (a : ℝ) → K) r))
h : x < 0
⊢ ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} x_1

Tactic:
exact fun r ↦ lt_of_mk_lt_mk_of_nonpos hr h.le

Premises used: LT.lt.le, ArchimedeanClass.lt_of_mk_lt_mk_of_nonpos
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
rw : Eq (α := ℝ) (sInf {r : ℝ | -x < (f : (a : ℝ) → K) r}) (sInf (-{r : ℝ | (f : (a : ℝ) → K) r < x}))
⊢ stdPart x = sSup {r : ℝ | (f : (a : ℝ) → K) r < x}

Tactic:
rw [← neg_inj, ← stdPart_neg, stdPart_eq_sInf f, ← Real.sInf_neg]

Premises used: ArchimedeanClass.stdPart_eq_sInf, Real.sInf_neg, ArchimedeanClass.stdPart_neg, neg_inj
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
e_a : Eq (α := Set ℝ) {r : ℝ | -x < (f : (a : ℝ) → K) r} (-{r : ℝ | (f : (a : ℝ) → K) r < x})
⊢ Eq (α := ℝ) (sInf {r : ℝ | -x < (f : (a : ℝ) → K) r}) (sInf (-{r : ℝ | (f : (a : ℝ) → K) r < x}))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
e_a :
  ∀ (x_1 : ℝ),
    Membership.mem (γ := Set ℝ) {r : ℝ | -x < (f : (a : ℝ) → K) r} x_1 ↔
      Membership.mem (γ := Set ℝ) (-{r : ℝ | (f : (a : ℝ) → K) r < x}) x_1
⊢ Eq (α := Set ℝ) {r : ℝ | -x < (f : (a : ℝ) → K) r} (-{r : ℝ | (f : (a : ℝ) → K) r < x})

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
x_1 : ℝ
⊢ Membership.mem (γ := Set ℝ) {r : ℝ | -x < (f : (a : ℝ) → K) r} x_1 ↔
    Membership.mem (γ := Set ℝ) (-{r : ℝ | (f : (a : ℝ) → K) r < x}) x_1

Tactic:
simp [neg_lt]

Premises used: neg_lt
-- Module: Mathlib.Algebra.Order.Ring.Star
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : StarRing R
inst_4 : StarOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
rw : x * y = star (y * x)
rw₁ : x * y = star x * star y
rw₂ : x * y = x * star y
rw₃ rw₄ : x * y = x * y
⊢ x * y = y * x

Tactic:
rw [← IsSelfAdjoint.of_nonneg (mul_nonneg hy hx), star_mul, IsSelfAdjoint.of_nonneg hx,
    IsSelfAdjoint.of_nonneg hy]

Premises used: mul_nonneg, IsSelfAdjoint.of_nonneg, StarMul.star_mul
-- Module: Mathlib.Algebra.Order.Ring.Synonym
Goal:
R : Type u_1
inst : NatCast R
n : ℕ
⊢ Eq.{u_1 + 1} (α := Rᵒᵈ) ((toDual : (a : R) → Rᵒᵈ) (↑n : R) : Rᵒᵈ) ((↑n : Rᵒᵈ) : Rᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Synonym
Goal:
R : Type u_1
inst : NatCast R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := Rᵒᵈ) ((toDual : (a : R) → Rᵒᵈ) (OfNat.ofNat n) : Rᵒᵈ) (OfNat.ofNat n : Rᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Synonym
Goal:
R : Type u_1
inst : NatCast R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) ((ofDual : (a : Rᵒᵈ) → R) (↑n : Rᵒᵈ) : R) ((↑n : R) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Synonym
Goal:
R : Type u_1
inst : NatCast R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := R) ((ofDual : (a : Rᵒᵈ) → R) (OfNat.ofNat n) : R) (OfNat.ofNat n : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Synonym
Goal:
R : Type u_1
inst : IntCast R
n : ℤ
⊢ Eq.{u_1 + 1} (α := Rᵒᵈ) ((toDual : (a : R) → Rᵒᵈ) (↑n : R) : Rᵒᵈ) ((↑n : Rᵒᵈ) : Rᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Synonym
Goal:
R : Type u_1
inst : IntCast R
n : ℤ
⊢ Eq.{u_1 + 1} (α := R) ((ofDual : (a : Rᵒᵈ) → R) (↑n : Rᵒᵈ) : R) ((↑n : R) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Synonym
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
h : LeftDistribClass R
⊢ LeftDistribClass.{u_1} (Lex R)

Tactic:
h

Premises used: Lex
-- Module: Mathlib.Algebra.Order.Ring.Synonym
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
h : RightDistribClass R
⊢ RightDistribClass.{u_1} (Lex R)

Tactic:
h

Premises used: Lex
-- Module: Mathlib.Algebra.Order.Ring.Synonym
Goal:
R : Type u_1
inst : Ring R
h : IsDomain R
⊢ IsDomain.{u_1} (Lex R)

Tactic:
h

Premises used: Lex
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : LE R
inst_1 : NonAssocSemiring R
inst_2 : AddLeftMono R
a : R
a1 : 1 ≤ a
⊢ a + 1 ≤ a + a

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b : R
inst_2 : ZeroLEOneClass R
inst_3 : MulPosMono R
inst_4 : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
bc : b ≤ a * b
⊢ a + (2 + b) ≤ a + (a + a * b)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b : R
inst_2 : ZeroLEOneClass R
inst_3 : MulPosMono R
inst_4 : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ b ≤ a * b

Tactic:
le_mul_of_one_le_left b0 <| one_le_two.trans a2

Premises used: le_mul_of_one_le_left, one_le_two, LE.le.trans
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b : R
inst_2 : ZeroLEOneClass R
inst_3 : MulPosMono R
inst_4 : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ b ≤ a * b

Tactic:
exact le_mul_of_one_le_left b0 <| one_le_two.trans a2

Premises used: le_mul_of_one_le_left, one_le_two, LE.le.trans
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b : R
inst_2 : ZeroLEOneClass R
inst_3 : MulPosMono R
inst_4 : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
rw : a + (a + a * b) ≤ a * 2 + a * b
rw₁ : a + (a + a * b) ≤ a + a + a * b
rw₂ rw₃ : a + (a + a * b) ≤ a + (a + a * b)
⊢ a + (a + a * b) ≤ a * (2 + b)

Tactic:
rw [mul_add, mul_two, add_assoc]

Premises used: add_assoc, mul_add, mul_two
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
obtain : ∀ (d : R) (hcd : 0 = c + d), c * a ≤ c * b
⊢ c * a ≤ c * b

Tactic:
obtain ⟨d, hcd⟩ := exists_add_of_le hc

Premises used: ExistsAddOfLE.exists_add_of_le
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ c * a ≤ c * b

Tactic:
le_of_add_le_add_right (a := d * b + d * a) ?_

Premises used: le_of_add_le_add_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
refine : c * a + (d * b + d * a) ≤ c * b + (d * b + d * a)
⊢ c * a ≤ c * b

Tactic:
refine le_of_add_le_add_right (a := d * b + d * a) ?_

Premises used: le_of_add_le_add_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
rw : d * b + (c * a + d * a) = d * b
rw₁ : d * b + (c + d) * a = d * b
rw₂ : d * b + 0 * a = d * b
rw₃ : d * b + 0 = d * b
rw₄ rw₅ : d * b = d * b
⊢ c * a + (d * b + d * a) = d * b

Tactic:
rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]

Premises used: add_mul, add_left_comm, MulZeroClass.zero_mul, add_zero
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
ha : 0 ≤ d
⊢ d * b ≤ d * a

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ 0 ≤ d

Tactic:
hcd.trans_le <| add_le_of_nonpos_left hc

Premises used: add_le_of_nonpos_left, Eq.trans_le
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ 0 ≤ d

Tactic:
exact hcd.trans_le <| add_le_of_nonpos_left hc

Premises used: add_le_of_nonpos_left, Eq.trans_le
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
rw : d * a = c * b + d * b + d * a
rw₁ : d * a = (c + d) * b + d * a
rw₂ : d * a = 0 * b + d * a
rw₃ : d * a = 0 + d * a
rw₄ rw₅ : d * a = d * a
⊢ d * a = c * b + (d * b + d * a)

Tactic:
rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

Premises used: add_mul, add_assoc, MulZeroClass.zero_mul, zero_add
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : PosMulMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
_ : c * a + (d * b + d * a) = d * b
_₁ : d * b ≤ d * a
_₂ : d * a = c * b + (d * b + d * a)
⊢ c * a + (d * b + d * a) ≤ c * b + (d * b + d * a)

Tactic:
calc
    _ = d * b := by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
    _ ≤ d * a := by gcongr; exact hcd.trans_le <| add_le_of_nonpos_left hc
    _ = _ := by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
obtain : ∀ (d : R) (hcd : 0 = c + d), a * c ≤ b * c
⊢ a * c ≤ b * c

Tactic:
obtain ⟨d, hcd⟩ := exists_add_of_le hc

Premises used: ExistsAddOfLE.exists_add_of_le
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * c ≤ b * c

Tactic:
le_of_add_le_add_right (a := b * d + a * d) ?_

Premises used: le_of_add_le_add_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
refine : a * c + (b * d + a * d) ≤ b * c + (b * d + a * d)
⊢ a * c ≤ b * c

Tactic:
refine le_of_add_le_add_right (a := b * d + a * d) ?_

Premises used: le_of_add_le_add_right
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
rw : b * d + (a * c + a * d) = b * d
rw₁ : b * d + a * (c + d) = b * d
rw₂ : b * d + a * 0 = b * d
rw₃ : b * d + 0 = b * d
rw₄ rw₅ : b * d = b * d
⊢ a * c + (b * d + a * d) = b * d

Tactic:
rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]

Premises used: add_left_comm, MulZeroClass.mul_zero, mul_add, add_zero
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
ha : 0 ≤ d
⊢ b * d ≤ a * d

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ 0 ≤ d

Tactic:
hcd.trans_le <| add_le_of_nonpos_left hc

Premises used: add_le_of_nonpos_left, Eq.trans_le
-- Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Preorder R
a b c : R
inst_2 : ExistsAddOfLE R
inst_3 : MulPosMono R
inst_4 : AddRightMono R
inst_5 : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ 0 ≤ d

Tactic:
exact hcd.trans_le <| add_le_of_nonpos_left hc

Premises used: add_le_of_nonpos_left, Eq.trans_le