awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
⊢ False
have succ : LT.lt (α := ℤ) (↑n : ℤ) (↑n : ℤ)
Tactic: apply lt_irrefl (n : ℤ)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (hypothesis)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
⊢ LT.lt (α := ℤ) (↑n : ℤ) (↑n : ℤ)
have ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
Tactic: have ha := Int.emod_lt a_n (by lia : (q.succ : ℤ) ≠ 0)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
⊢ LT.lt (α := ℤ) (↑n : ℤ) (↑n : ℤ)
have succ : ∀ (le : p * q ≤ n) (a_n b_n : ℤ) (eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n),
  let a := a_n % (↑q.succ : ℤ);
  let b := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ);
  ∀ (this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)) (hb : b ≤ -1)
    (ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)), LT.lt (α := ℤ) (↑n : ℤ) (↑n : ℤ)
Tactic: rw [p.pred_succ, q.pred_succ] at le
Cleared hypotheses: le, a_n, b_n, eq, a, b, this, hb, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) ≤
    HMul.hMul (α := ℤ) (↑q : ℤ) (↑p.succ : ℤ) + HMul.hMul (α := ℤ) (-1) (↑q.succ : ℤ)
have h₁ : LE.le (α := ℤ) 0 (↑p.succ : ℤ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
h₁ : LE.le (α := ℤ) 0 (↑p.succ : ℤ)
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) ≤
    HMul.hMul (α := ℤ) (↑q : ℤ) (↑p.succ : ℤ) + HMul.hMul (α := ℤ) (-1) (↑q.succ : ℤ)
have h₂ : a ≤ (↑q : ℤ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
h₁ : LE.le (α := ℤ) 0 (↑p.succ : ℤ)
h₂ : a ≤ (↑q : ℤ)
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) ≤
    HMul.hMul (α := ℤ) (↑q : ℤ) (↑p.succ : ℤ) + HMul.hMul (α := ℤ) (-1) (↑q.succ : ℤ)
have h₃ : LE.le (α := ℤ) 0 (↑q.succ : ℤ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
⊢ HMul.hMul (α := ℤ) (↑q : ℤ) (↑p.succ : ℤ) + HMul.hMul (α := ℤ) (-1) (↑q.succ : ℤ) =
    HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
have simp_rw : HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) + HMul.hMul (α := ℤ) (↑q : ℤ) 1 +
    (HMul.hMul (α := ℤ) (↑q : ℤ) (-1) + HMul.hMul (α := ℤ) 1 (-1)) =
  HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
Tactic: simp_rw [Nat.cast_succ, mul_add, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
⊢ HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1 ≤ HSub.hSub (α := ℤ) (↑n : ℤ) 1
have rwa : HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) ≤ (↑n : ℤ)
Tactic: rwa [sub_le_sub_iff_right, ← Nat.cast_mul, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
rwa : HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) ≤ (↑n : ℤ)
⊢ HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1 ≤ HSub.hSub (α := ℤ) (↑n : ℤ) 1
have rwa₁ : LE.le (α := ℤ) (↑(p * q) : ℤ) (↑n : ℤ)
Tactic: rwa [sub_le_sub_iff_right, ← Nat.cast_mul, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
⊢ LT.lt (α := ℤ) (↑n : ℤ) (↑n : ℤ)
have calc : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) ≤
  HMul.hMul (α := ℤ) (↑q : ℤ) (↑p.succ : ℤ) + HMul.hMul (α := ℤ) (-1) (↑q.succ : ℤ)
Tactic: calc n = a * p.succ + b * q.succ := this.symm
       _ ≤ q * p.succ + -1 * q.succ := by gcongr <;> lia
       _ = p * q - 1 := by simp_rw [Nat.cast_succ, mul_add, mul_comm]; lia
       _ ≤ n - 1 := by rwa [sub_le_sub_iff_right, ← Nat.cast_mul, Nat.cast_le]
       _ < n := by lia
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
calc :
  a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) ≤
    HMul.hMul (α := ℤ) (↑q : ℤ) (↑p.succ : ℤ) + HMul.hMul (α := ℤ) (-1) (↑q.succ : ℤ)
⊢ LT.lt (α := ℤ) (↑n : ℤ) (↑n : ℤ)
have calc₁ : HMul.hMul (α := ℤ) (↑q : ℤ) (↑p.succ : ℤ) + HMul.hMul (α := ℤ) (-1) (↑q.succ : ℤ) =
  HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
Tactic: calc n = a * p.succ + b * q.succ := this.symm
       _ ≤ q * p.succ + -1 * q.succ := by gcongr <;> lia
       _ = p * q - 1 := by simp_rw [Nat.cast_succ, mul_add, mul_comm]; lia
       _ ≤ n - 1 := by rwa [sub_le_sub_iff_right, ← Nat.cast_mul, Nat.cast_le]
       _ < n := by lia
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
calc :
  a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) ≤
    HMul.hMul (α := ℤ) (↑q : ℤ) (↑p.succ : ℤ) + HMul.hMul (α := ℤ) (-1) (↑q.succ : ℤ)
calc₁ :
  HMul.hMul (α := ℤ) (↑q : ℤ) (↑p.succ : ℤ) + HMul.hMul (α := ℤ) (-1) (↑q.succ : ℤ) =
    HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
⊢ LT.lt (α := ℤ) (↑n : ℤ) (↑n : ℤ)
have calc₂ : HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1 ≤ HSub.hSub (α := ℤ) (↑n : ℤ) 1
Tactic: calc n = a * p.succ + b * q.succ := this.symm
       _ ≤ q * p.succ + -1 * q.succ := by gcongr <;> lia
       _ = p * q - 1 := by simp_rw [Nat.cast_succ, mul_add, mul_comm]; lia
       _ ≤ n - 1 := by rwa [sub_le_sub_iff_right, ← Nat.cast_mul, Nat.cast_le]
       _ < n := by lia
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
calc :
  a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) ≤
    HMul.hMul (α := ℤ) (↑q : ℤ) (↑p.succ : ℤ) + HMul.hMul (α := ℤ) (-1) (↑q.succ : ℤ)
calc₁ :
  HMul.hMul (α := ℤ) (↑q : ℤ) (↑p.succ : ℤ) + HMul.hMul (α := ℤ) (-1) (↑q.succ : ℤ) =
    HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
calc₂ : HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1 ≤ HSub.hSub (α := ℤ) (↑n : ℤ) 1
⊢ LT.lt (α := ℤ) (↑n : ℤ) (↑n : ℤ)
have calc₃ : HSub.hSub (α := ℤ) (↑n : ℤ) 1 < (↑n : ℤ)
Tactic: calc n = a * p.succ + b * q.succ := this.symm
       _ ≤ q * p.succ + -1 * q.succ := by gcongr <;> lia
       _ = p * q - 1 := by simp_rw [Nat.cast_succ, mul_add, mul_comm]; lia
       _ ≤ n - 1 := by rwa [sub_le_sub_iff_right, ← Nat.cast_mul, Nat.cast_le]
       _ < n := by lia
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Interval (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
r : R
hr : 0 < r
k m n : ℤ
h : r * (↑k : R) ∈ Set.Ioo (r * (↑(m - 1) : R)) (r * (↑(n + 1) : R))
⊢ k ∈ Finset.Icc m n
have h₁ : m - 1 < k ∧ k < n + 1
Tactic: simp only [Set.mem_Ioo, mul_lt_mul_iff_right₀ hr, Int.cast_lt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
α : Type u_2
inst_3 : Add α
f : α → R
hf : ∀ (x : α), 0 ≤ f x
hna : IsNonarchimedean f
a b : α
⊢ f (a + b) ≤ f a + f b
have apply : max (f a) (f b) ≤ f a + f b
Tactic: apply le_trans (hna _ _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
α : Type u_2
inst_3 : Add α
f : α → R
hf : ∀ (x : α), 0 ≤ f x
hna : IsNonarchimedean f
a b : α
⊢ max (f a) (f b) ≤ f a + f b
have rw : 0 ≤ f b ∧ 0 ≤ f a
Tactic: rw [max_le_iff, le_add_iff_nonneg_right, le_add_iff_nonneg_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddMonoid α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
a : α
n : ℕ
h : LE.le.{u_1} (α := R) ((f : (a : α) → R) (n • a) : R) ((f : (a : α) → R) a : R)
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) ((n + 1) • a) : R) ((f : (a : α) → R) a : R)
have succ : LE.le.{u_1} (α := R) ((f : (a : α) → R) (n • a + HSMul.hSMul (α := ℕ) 1 a) : R) ((f : (a : α) → R) a : R)
Tactic: rw [add_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddMonoid α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
a : α
n : ℕ
h : LE.le.{u_1} (α := R) ((f : (a : α) → R) (n • a) : R) ((f : (a : α) → R) a : R)
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (n • a + HSMul.hSMul (α := ℕ) 1 a) : R) ((f : (a : α) → R) a : R)
have succ : LE.le.{u_1} (α := R) (max ((f : (a : α) → R) (n • a)) ((f : (a : α) → R) (HSMul.hSMul (α := ℕ) 1 a)) : R)
  ((f : (a : α) → R) a : R)
Tactic: apply le_trans <| hna (n • a) (1 • a)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddMonoid α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
n : ℕ
a : α
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (n • a) : R) ((f : (a : α) → R) a : R)
have zero : LE.le.{u_1} (α := R) ((f : (a : α) → R) (HSMul.hSMul (α := ℕ) 0 a) : R) ((f : (a : α) → R) a : R)
Tactic: induction n with
  | zero => simp
  | succ n _ =>
    rw [add_nsmul]
    apply le_trans <| hna (n • a) (1 • a)
    simpa
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddMonoid α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
n : ℕ
a : α
zero : LE.le.{u_1} (α := R) ((f : (a : α) → R) (HSMul.hSMul (α := ℕ) 0 a) : R) ((f : (a : α) → R) a : R)
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (n • a) : R) ((f : (a : α) → R) a : R)
have succ : ∀ (n : ℕ),
  LE.le.{u_1} (α := R) ((f : (a : α) → R) (n • a) : R) ((f : (a : α) → R) a : R) →
    LE.le.{u_1} (α := R) ((f : (a : α) → R) ((n + 1) • a) : R) ((f : (a : α) → R) a : R)
Tactic: induction n with
  | zero => simp
  | succ n _ =>
    rw [add_nsmul]
    apply le_trans <| hna (n • a) (1 • a)
    simpa
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : NonAssocSemiring α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
n : ℕ
a : α
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) ((↑n : α) * a) : R) ((f : (a : α) → R) a : R)
have rw : LE.le.{u_1} (α := R) ((f : (a : α) → R) (n • a) : R) ((f : (a : α) → R) a : R)
Tactic: rw [← nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddMonoidWithOne α
inst_3 : FunLike F α R
inst_4 : ZeroHomClass F α R
inst_5 : NonnegHomClass F α R
inst_6 : OneHomClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
n : ℕ
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (↑n : α) : R) (1 : R)
have rw : LE.le.{u_1} (α := R) ((f : (a : α) → R) (HSMul.hSMul (β := α) n 1) : R) ((f : (a : α) → R) 1 : R)
Tactic: rw [← nsmul_one n, ← map_one f]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst_3 : AddGroupWithOne α
inst_4 : FunLike F α R
inst_5 : AddGroupSeminormClass F α R
inst_6 : OneHomClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
n : ℤ
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (↑n : α) : R) (1 : R)
have inl : ∀ (a : ℕ), LE.le.{u_1} (α := R) ((f : (a : α) → R) (↑(↑a : ℤ) : α) : R) (1 : R)
Tactic: obtain ⟨a, rfl | rfl⟩ := Int.eq_nat_or_neg n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst_3 : AddGroupWithOne α
inst_4 : FunLike F α R
inst_5 : AddGroupSeminormClass F α R
inst_6 : OneHomClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
n : ℤ
inl : ∀ (a : ℕ), LE.le.{u_1} (α := R) ((f : (a : α) → R) (↑(↑a : ℤ) : α) : R) (1 : R)
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (↑n : α) : R) (1 : R)
have inr : ∀ (a : ℕ), LE.le.{u_1} (α := R) ((f : (a : α) → R) (↑(-(↑a : ℤ)) : α) : R) (1 : R)
Tactic: obtain ⟨a, rfl | rfl⟩ := Int.eq_nat_or_neg n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) y : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)
have by_contra! : ∀ (h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) y : R)
h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)
⊢ False
have h1 : LE.le.{u_1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)
Tactic: have h1 : f (x + y) ≤ f y := (hna x y).trans_eq (max_eq_right_of_lt h_lt)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) y : R)
h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)
h1 : LE.le.{u_1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)
⊢ False
have apply : LT.lt.{u_1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) y : R)
Tactic: apply lt_irrefl (f y)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) y : R)
h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)
h1 : LE.le.{u_1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)
⊢ LT.lt.{u_1} (α := R) (max ((f : (a : α) → R) (-x)) ((f : (a : α) → R) (x + y)) : R)
    (max ((f : (a : α) → R) y) ((f : (a : α) → R) y) : R)
have rw : LT.lt.{u_1} (α := R) (max ((f : (a : α) → R) x) ((f : (a : α) → R) (x + y)) : R) ((f : (a : α) → R) y : R)
Tactic: rw [max_self, map_neg_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) y : R)
h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)
h1 : LE.le.{u_1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)
⊢ LT.lt.{u_1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) y : R)
have f₁ : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) (-x + (x + y)) : R)
Tactic: calc
    f y = f (-x + (x + y)) := by simp
    _   ≤ max (f (-x)) (f (x + y)) := hna (-x) (x + y)
    _   < max (f y) (f y) := by
      rw [max_self, map_neg_eq_map]
      exact max_lt h_lt <| lt_of_le_of_ne h1 h
    _   = f y := max_self (f y)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) y : R)
h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)
h1 : LE.le.{u_1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)
f₁ : Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) (-x + (x + y)) : R)
⊢ LT.lt.{u_1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) y : R)
have f₂ : LT.lt.{u_1} (α := R) (max ((f : (a : α) → R) (-x)) ((f : (a : α) → R) (x + y)) : R)
  (max ((f : (a : α) → R) y) ((f : (a : α) → R) y) : R)
Tactic: calc
    f y = f (-x + (x + y)) := by simp
    _   ≤ max (f (-x)) (f (x + y)) := hna (-x) (x + y)
    _   < max (f y) (f y) := by
      rw [max_self, map_neg_eq_map]
      exact max_lt h_lt <| lt_of_le_of_ne h1 h
    _   = f y := max_self (f y)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)
have by_contra! : ∀ (h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) x : R)
h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)
⊢ False
have h1 : LE.le.{u_1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)
Tactic: have h1 : f (x + y) ≤ f x := (hna x y).trans_eq (max_eq_left_of_lt h_lt)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.IsNonarchimedean (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
F : Type u_2
α : Type u_3
inst_2 : AddGroup α
inst_3 : FunLike F α R
inst_4 : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean.{u_1, u_3} (R := R) (α := α) (⇑f : (a : α) → R)
x y : α
h_lt : LT.lt.{u_1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) x : R)
h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)
h1 : LE.le.{u_1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)
⊢ False
have apply : LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) x : R)
Tactic: apply lt_irrefl (f x)