awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Int
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 : ℤ)
rwa₁ : LE.le (α := ℤ) (↑(p * q) : ℤ) (↑n : ℤ)
rwa₂ rwa₃ rwa₄ rwa₅ : p * q ≤ n
⊢ HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1 ≤ HSub.hSub (α := ℤ) (↑n : ℤ) 1

Tactic:
rwa [sub_le_sub_iff_right, ← Nat.cast_mul, Nat.cast_le]

Premises used: sub_le_sub_iff_right, Nat.cast_mul, Nat.cast_le
-- Module: Mathlib.Algebra.Order.Ring.Int
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 : ℤ)) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑n : ℤ) 1 < (↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Ring.Int
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
calc₃ : HSub.hSub (α := ℤ) (↑n : ℤ) 1 < (↑n : ℤ)
⊢ LT.lt (α := ℤ) (↑n : ℤ) (↑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

Premises used: Eq.symm, Nat.succ
-- Module: Mathlib.Algebra.Order.Ring.Interval
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))
⊢ m - 1 < k ∧ k < n + 1

Tactic:
simp only [Set.mem_Ioo, mul_lt_mul_iff_right₀ hr, Int.cast_lt] at h

Premises used: Set.mem_Ioo, Int.cast_lt, mul_lt_mul_iff_right₀
-- Module: Mathlib.Algebra.Order.Ring.Interval
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 : m - 1 < k ∧ k < n + 1
⊢ k ∈ Finset.Icc m n

Tactic:
grind [Int.lt_iff_add_one_le]

Premises used: Int.lt_iff_add_one_le
-- Module: Mathlib.Algebra.Order.Ring.Interval
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
r : R
hr : 0 < r
k m : ℤ
h : r * (↑k : R) ∈ Set.Ioo (r * (↑(m - 1) : R)) (r * (↑(m + 1) : R))
⊢ k = m

Tactic:
simpa using int_mem_Icc_of_mul_mem_Ioo hr h

Premises used: IsStrictOrderedRing.int_mem_Icc_of_mul_mem_Ioo
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : α
apply : max (f a) (f b) ≤ f a + f b
⊢ f (a + b) ≤ f a + f b

Tactic:
apply le_trans (hna _ _)

Premises used: le_trans
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : α
rw : 0 ≤ f b ∧ 0 ≤ f a
⊢ max (f a) (f b) ≤ f a + f b

Tactic:
rw [max_le_iff, le_add_iff_nonneg_right, le_add_iff_nonneg_left]

Premises used: le_add_iff_nonneg_right, max_le_iff, le_add_iff_nonneg_left
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : α
⊢ 0 ≤ f b ∧ 0 ≤ f a

Tactic:
⟨hf _, hf _⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : α
⊢ 0 ≤ f b ∧ 0 ≤ f a

Tactic:
exact ⟨hf _, hf _⟩
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : α
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (HSMul.hSMul (α := ℕ) 0 a) : R) ((f : (a : α) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
succ : LE.le.{u_1} (α := R) ((f : (a : α) → R) (n • a + HSMul.hSMul (α := ℕ) 1 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:
rw [add_nsmul]

Premises used: add_nsmul
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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)
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (n • a + HSMul.hSMul (α := ℕ) 1 a) : R) ((f : (a : α) → R) a : R)

Tactic:
apply le_trans <| hna (n • a) (1 • a)

Premises used: HSMul.hSMul, OfNat.ofNat, le_trans
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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) (max ((f : (a : α) → R) (n • a)) ((f : (a : α) → R) (HSMul.hSMul (α := ℕ) 1 a)) : R)
    ((f : (a : α) → R) a : R)

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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)
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (n • 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

Premises used: HSMul.hSMul, OfNat.ofNat, add_nsmul, le_trans
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : α
rw : 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) : R) ((f : (a : α) → R) a : R)

Tactic:
rw [← nsmul_eq_mul]

Premises used: nsmul_eq_mul
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)

Tactic:
nsmul_le hna

Premises used: IsNonarchimedean.nsmul_le
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)

Tactic:
exact nsmul_le hna

Premises used: IsNonarchimedean.nsmul_le
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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 : ℕ
rw : LE.le.{u_1} (α := R) ((f : (a : α) → R) (HSMul.hSMul (β := α) n 1) : R) ((f : (a : α) → R) 1 : R)
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (↑n : α) : R) (1 : R)

Tactic:
rw [← nsmul_one n, ← map_one f]

Premises used: map_one, nsmul_one
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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) (HSMul.hSMul (β := α) n 1) : R) ((f : (a : α) → R) 1 : R)

Tactic:
nsmul_le hna

Premises used: IsNonarchimedean.nsmul_le
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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) (HSMul.hSMul (β := α) n 1) : R) ((f : (a : α) → R) 1 : R)

Tactic:
exact nsmul_le hna

Premises used: IsNonarchimedean.nsmul_le
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
inr : ∀ (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)

Tactic:
obtain ⟨a, rfl | rfl⟩ := Int.eq_nat_or_neg n

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
a : ℕ
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (↑(↑a : ℤ) : α) : R) (1 : R)

Tactic:
simp [apply_natCast_le_one hna]

Premises used: IsNonarchimedean.apply_natCast_le_one
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
a : ℕ
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (↑(-(↑a : ℤ)) : α) : R) (1 : R)

Tactic:
simp [apply_natCast_le_one hna]

Premises used: IsNonarchimedean.apply_natCast_le_one
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
by_contra! : ∀ (h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)), False
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) y : R)

Tactic:
by_contra! h
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
⊢ 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)
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
apply : LT.lt.{u_1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) y : R)
⊢ False

Tactic:
apply lt_irrefl (f y)

Premises used: lt_irrefl, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) y : R) ((f : (a : α) → R) (-x + (x + y)) : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (-x + (x + y)) : R)
    (max ((f : (a : α) → R) (-x)) ((f : (a : α) → R) (x + y)) : R)

Tactic:
hna (-x) (x + y)

Premises used: HAdd.hAdd, Neg.neg
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
rw : LT.lt.{u_1} (α := R) (max ((f : (a : α) → R) x) ((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)

Tactic:
rw [max_self, map_neg_eq_map]

Premises used: AddGroupSeminormClass.map_neg_eq_map, max_self
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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) ((f : (a : α) → R) y : R)

Tactic:
max_lt h_lt <| lt_of_le_of_ne h1 h

Premises used: max_lt, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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) ((f : (a : α) → R) y : R)

Tactic:
exact max_lt h_lt <| lt_of_le_of_ne h1 h

Premises used: max_lt, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
⊢ Eq.{u_1 + 1} (α := R) (max ((f : (a : α) → R) y) ((f : (a : α) → R) y) : R) ((f : (a : α) → R) y : R)

Tactic:
max_self (f y)

Premises used: max_self, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
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)
⊢ LT.lt.{u_1} (α := R) ((f : (a : α) → R) y : R) ((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)

Premises used: max_self, HAdd.hAdd, Max.max, DFunLike.coe, Neg.neg
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
by_contra! : ∀ (h : Ne.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)), False
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) (x + y) : R) ((f : (a : α) → R) x : R)

Tactic:
by_contra! h
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
⊢ 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)
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
apply : LT.lt.{u_1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) x : R)
⊢ False

Tactic:
apply lt_irrefl (f x)

Premises used: lt_irrefl, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : α) → R) x : R) ((f : (a : α) → R) (x + y + -y) : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean
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)
⊢ LE.le.{u_1} (α := R) ((f : (a : α) → R) (x + y + -y) : R)
    (max ((f : (a : α) → R) (x + y)) ((f : (a : α) → R) (-y)) : R)

Tactic:
hna (x + y) (-y)

Premises used: HAdd.hAdd, Neg.neg