awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, (f : (a : ℝ) → K) s ≤ x
hr : ∀ s > r, x ≤ (f : (a : ℝ) → K) s
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
⊢ stdPart x = r
have inl : ∀ (h : stdPart x < r), stdPart x = r
Tactic: obtain h | rfl | h := lt_trichotomy (stdPart x) r
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, (f : (a : ℝ) → K) s ≤ x
hr : ∀ s > r, x ≤ (f : (a : ℝ) → K) s
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
inl : ∀ (h : stdPart x < r), stdPart x = r
⊢ stdPart x = r
have inr : ∀ (hl : ∀ s < stdPart x, (f : (a : ℝ) → K) s ≤ x) (hr : ∀ s > stdPart x, x ≤ (f : (a : ℝ) → K) s), stdPart x = stdPart x
Tactic: obtain h | rfl | h := lt_trichotomy (stdPart x) r
Cleared hypotheses: r, hl, hr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, (f : (a : ℝ) → K) s ≤ x
hr : ∀ s > r, x ≤ (f : (a : ℝ) → K) s
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
inl : ∀ (h : stdPart x < r), stdPart x = r
inr :
  ∀ (hl : ∀ s < stdPart x, (f : (a : ℝ) → K) s ≤ x) (hr : ∀ s > stdPart x, x ≤ (f : (a : ℝ) → K) s),
    stdPart x = stdPart x
⊢ stdPart x = r
have inr₁ : ∀ (h : r < stdPart x), stdPart x = r
Tactic: obtain h | rfl | h := lt_trichotomy (stdPart x) r
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, (f : (a : ℝ) → K) s ≤ x
hr : ∀ s > r, x ≤ (f : (a : ℝ) → K) s
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : stdPart x < r
⊢ stdPart x = r
have inl : ∀ (s : ℝ) (hs : stdPart x < s) (hs' : s < r), stdPart x = r
Tactic: obtain ⟨s, hs, hs'⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, (f : (a : ℝ) → K) s ≤ x
hr : ∀ s > r, x ≤ (f : (a : ℝ) → K) s
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : r < stdPart x
⊢ stdPart x = r
have inr : ∀ (s : ℝ) (hs : r < s) (hs' : s < stdPart x), stdPart x = r
Tactic: obtain ⟨s, hs, hs'⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
have inl : ∀ (hx : LE.le (α := ArchimedeanClass K) 0 (mk x)), stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
Tactic: obtain hx | hx := le_or_gt 0 (mk x)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
inl : ∀ (hx : LE.le (α := ArchimedeanClass K) 0 (mk x)), stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
have inr : ∀ (hx : LT.lt (α := ArchimedeanClass K) (mk x) 0), stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
Tactic: obtain hx | hx := le_or_gt 0 (mk x)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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)
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
have inl : ∀ (a : ℤ) (ha : (↑a : K) < x), stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
Tactic: obtain ⟨a, ha⟩ := exists_int_lt_of_mk_nonneg hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
have inl : ∀ (b : ℤ) (hb : x < (↑b : K)), stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
Tactic: obtain ⟨b, hb⟩ := exists_int_gt_of_mk_nonneg hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (hypothesis)
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)
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
have hn : Set.Nonempty (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
Tactic: have hn : {r | x < f r}.Nonempty := ⟨b, by simpa using hb⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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}
have refine : ∀ (r : ℝ) (hr : Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} r), (↑a : ℝ) ≤ r
Tactic: refine ⟨a, fun r hr ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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
⊢ (↑a : ℝ) ≤ r
have by_contra! : ∀ (hra : r < (↑a : ℝ)), False
Tactic: by_contra! hra
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (hypothesis)
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}
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
have hb₁ : 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)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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}
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
have inl : ∀ s < sInf {r : ℝ | x < (f : (a : ℝ) → K) r}, (f : (a : ℝ) → K) s ≤ x
Tactic: apply stdPart_eq f
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
have inl₁ : ∀ s > sInf {r : ℝ | x < (f : (a : ℝ) → K) r}, x ≤ (f : (a : ℝ) → K) s
Tactic: apply stdPart_eq f
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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}
⊢ x ≤ (f : (a : ℝ) → K) r
have inl : ∀ (s : ℝ) (hs : Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} s) (hs' : s < r), x ≤ (f : (a : ℝ) → K) r
Tactic: obtain ⟨s, hs, hs'⟩ := (csInf_lt_iff hb hn).1 hr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
have inr : Eq (α := ℝ) 0 (sInf {r : ℝ | x < (f : (a : ℝ) → K) r})
Tactic: rw [stdPart_of_mk_ne_zero hx.ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (hypothesis)
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
⊢ Eq (α := ℝ) 0 (sInf {r : ℝ | x < (f : (a : ℝ) → K) r})
have hr : ∀ {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)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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))
⊢ Eq (α := ℝ) 0 (sInf {r : ℝ | x < (f : (a : ℝ) → K) r})
have inr : ∀ (h : 0 ≤ x), Eq (α := ℝ) 0 (sInf {r : ℝ | x < (f : (a : ℝ) → K) r})
Tactic: obtain h | h := le_or_gt 0 x
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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})
⊢ Eq (α := ℝ) 0 (sInf {r : ℝ | x < (f : (a : ℝ) → K) r})
have inr₁ : ∀ (h : x < 0), Eq (α := ℝ) 0 (sInf {r : ℝ | x < (f : (a : ℝ) → K) r})
Tactic: obtain h | h := le_or_gt 0 x
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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 {r : ℝ | x < (f : (a : ℝ) → K) r})
have h₁ : Eq (α := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} ∅
Tactic: convert! Real.sInf_empty.symm
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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 (α := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} ∅
have h₁ : ∀ (x_1 : ℝ), x_1 ∉ {r : ℝ | x < (f : (a : ℝ) → K) r}
Tactic: rw [Set.eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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 {r : ℝ | x < (f : (a : ℝ) → K) r})
have h₁ : Eq (α := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} Set.univ
Tactic: convert! Real.sInf_univ.symm
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
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 (α := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} Set.univ
have h₁ : ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} x_1
Tactic: rw [Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
⊢ stdPart x = sSup {r : ℝ | (f : (a : ℝ) → K) r < x}
have rw : Eq (α := ℝ) (sInf {r : ℝ | -x < (f : (a : ℝ) → K) r}) (sInf (-{r : ℝ | (f : (a : ℝ) → K) r < x}))
Tactic: rw [← neg_inj, ← stdPart_neg, stdPart_eq_sInf f, ← Real.sInf_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
⊢ Eq (α := ℝ) (sInf {r : ℝ | -x < (f : (a : ℝ) → K) r}) (sInf (-{r : ℝ | (f : (a : ℝ) → K) r < x}))
have e_a : Eq (α := Set ℝ) {r : ℝ | -x < (f : (a : ℝ) → K) r} (-{r : ℝ | (f : (a : ℝ) → K) r < x})
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
⊢ Eq (α := Set ℝ) {r : ℝ | -x < (f : (a : ℝ) → K) r} (-{r : ℝ | (f : (a : ℝ) → K) r < x})
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Star (goal)
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
⊢ x * y = y * x
have rw : x * y = star (y * x)
Tactic: rw [← IsSelfAdjoint.of_nonneg (mul_nonneg hy hx), star_mul, IsSelfAdjoint.of_nonneg hx,
    IsSelfAdjoint.of_nonneg hy]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Star (goal)
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)
⊢ x * y = y * x
have rw₁ : x * y = star x * star y
Tactic: rw [← IsSelfAdjoint.of_nonneg (mul_nonneg hy hx), star_mul, IsSelfAdjoint.of_nonneg hx,
    IsSelfAdjoint.of_nonneg hy]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Star (goal)
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
⊢ x * y = y * x
have rw₂ : x * y = x * star y
Tactic: rw [← IsSelfAdjoint.of_nonneg (mul_nonneg hy hx), star_mul, IsSelfAdjoint.of_nonneg hx,
    IsSelfAdjoint.of_nonneg hy]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Star (goal)
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
⊢ x * y = y * x
have rw₃ : x * y = x * y
Tactic: rw [← IsSelfAdjoint.of_nonneg (mul_nonneg hy hx), star_mul, IsSelfAdjoint.of_nonneg hx,
    IsSelfAdjoint.of_nonneg hy]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ a + (2 + b) ≤ a + (a + a * b)
have bc : b ≤ a * b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ a + (a + a * b) ≤ a * (2 + b)
have rw : a + (a + a * b) ≤ a * 2 + a * b
Tactic: rw [mul_add, mul_two, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ a + (a + a * b) ≤ a * (2 + b)
have rw₁ : a + (a + a * b) ≤ a + a + a * b
Tactic: rw [mul_add, mul_two, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ a + (a + a * b) ≤ a * (2 + b)
have rw₂ : a + (a + a * b) ≤ a + (a + a * b)
Tactic: rw [mul_add, mul_two, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ c * a ≤ c * b
have obtain : ∀ (d : R) (hcd : 0 = c + d), c * a ≤ c * b
Tactic: obtain ⟨d, hcd⟩ := exists_add_of_le hc
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
have refine : c * a + (d * b + d * a) ≤ c * b + (d * b + d * a)
Tactic: refine le_of_add_le_add_right (a := d * b + d * a) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
have rw : d * b + (c * a + d * a) = d * b
Tactic: rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ c * a + (d * b + d * a) = d * b
have rw₁ : d * b + (c + d) * a = d * b
Tactic: rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ c * a + (d * b + d * a) = d * b
have rw₂ : d * b + 0 * a = d * b
Tactic: rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ c * a + (d * b + d * a) = d * b
have rw₃ : d * b + 0 = d * b
Tactic: rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ c * a + (d * b + d * a) = d * b
have rw₄ : d * b = d * b
Tactic: rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ d * b ≤ d * a
have ha : 0 ≤ d
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ d * a = c * b + (d * b + d * a)
have rw : d * a = c * b + d * b + d * a
Tactic: rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ d * a = c * b + (d * b + d * a)
have rw₁ : d * a = (c + d) * b + d * a
Tactic: rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ d * a = c * b + (d * b + d * a)
have rw₂ : d * a = 0 * b + d * a
Tactic: rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ d * a = c * b + (d * b + d * a)
have rw₃ : d * a = 0 + d * a
Tactic: rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ d * a = c * b + (d * b + d * a)
have rw₄ : d * a = d * a
Tactic: rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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) ≤ c * b + (d * b + d * a)
have _ : c * a + (d * b + d * a) = d * b
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ c * a + (d * b + d * a) ≤ c * b + (d * b + d * a)
have _₁ : 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Unbundled.Basic (goal)
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
⊢ c * a + (d * b + d * a) ≤ c * b + (d * b + d * a)
have _₂ : 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]