import Mathlib

open Real

#check
π : ℝ 
π: ℝ
π

#check
rexp 1 : ℝ 
rexp: ℝ → ℝ
rexp 
1: ℝ
1

#check
Irrational (rexp 1 + π) : Prop 
Irrational: ℝ → Prop
Irrational (
rexp: ℝ → ℝ
rexp 
1: ℝ
1 + 
π: ℝ
π)

example: ∀ (a b c : ℕ), a + b * c = c * b + a
example (
a: ℕ
a 
b: ℕ
b 
c: ℕ
c : 
ℕ: Type
ℕ) : 
a: ℕ
a + 
b: ℕ
b * 
c: ℕ
c = 
c: ℕ
c * 
b: ℕ
b + 
a: ℕ
a := by
Goals accomplished! 🐙 ring
Goals accomplished! 🐙

example: ∀ (a b c : ℕ), a + b * c = c * b + a
example (
a: ℕ
a 
b: ℕ
b 
c: ℕ
c : 
ℕ: Type
ℕ) : 
a: ℕ
a + 
b: ℕ
b * 
c: ℕ
c = 
c: ℕ
c * 
b: ℕ
b + 
a: ℕ
a := by
Goals accomplished! 🐙 show_term
Try this: exact Mathlib.Tactic.Ring.of_eq
  (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf a)
    (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf b) (Mathlib.Tactic.Ring.atom_pf c)
      (Mathlib.Tactic.Ring.add_mul
        (Mathlib.Tactic.Ring.mul_add
          (Mathlib.Tactic.Ring.mul_pf_left b (Nat.rawCast 1)
            (Mathlib.Tactic.Ring.mul_pf_right c (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))
          (Mathlib.Tactic.Ring.mul_zero (b ^ Nat.rawCast 1 * Nat.rawCast 1))
          (Mathlib.Tactic.Ring.add_pf_add_zero (b ^ Nat.rawCast 1 * (c ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))
        (Mathlib.Tactic.Ring.zero_mul (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
        (Mathlib.Tactic.Ring.add_pf_add_zero (b ^ Nat.rawCast 1 * (c ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))
    (Mathlib.Tactic.Ring.add_pf_add_lt (a ^ Nat.rawCast 1 * Nat.rawCast 1)
      (Mathlib.Tactic.Ring.add_pf_zero_add (b ^ Nat.rawCast 1 * (c ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))
  (Mathlib.Tactic.Ring.add_congr
    (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf c) (Mathlib.Tactic.Ring.atom_pf b)
      (Mathlib.Tactic.Ring.add_mul
        (Mathlib.Tactic.Ring.mul_add
          (Mathlib.Tactic.Ring.mul_pf_right b (Nat.rawCast 1)
            (Mathlib.Tactic.Ring.mul_pf_left c (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))
          (Mathlib.Tactic.Ring.mul_zero (c ^ Nat.rawCast 1 * Nat.rawCast 1))
          (Mathlib.Tactic.Ring.add_pf_add_zero (b ^ Nat.rawCast 1 * (c ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))
        (Mathlib.Tactic.Ring.zero_mul (b ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
        (Mathlib.Tactic.Ring.add_pf_add_zero (b ^ Nat.rawCast 1 * (c ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))
    (Mathlib.Tactic.Ring.atom_pf a)
    (Mathlib.Tactic.Ring.add_pf_add_gt (a ^ Nat.rawCast 1 * Nat.rawCast 1)
      (Mathlib.Tactic.Ring.add_pf_add_zero (b ^ Nat.rawCast 1 * (c ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))
a, b, c: ℕ
a + b * c = c * b + a ring
Goals accomplished! 🐙

example: 24 ^ 9 < 9 ^ 25
example : 
24: ℕ
24 ^ 
9: ℕ
9 < 
9: ℕ
9 ^ 
25: ℕ
25 := by
Goals accomplished! 🐙 show_term
Try this: exact of_eq_true
  (eq_true
    (Mathlib.Meta.NormNum.isNat_lt_true
      (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 24))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))
        (Mathlib.Meta.NormNum.IsNatPowT.run
          (Mathlib.Meta.NormNum.IsNatPowT.trans
            (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
              Mathlib.Meta.NormNum.IsNatPowT.bit0)
            Mathlib.Meta.NormNum.IsNatPowT.bit1)))
      (Mathlib.Meta.NormNum.isNat_pow (Eq.refl HPow.hPow) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))
        (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 25))
        (Mathlib.Meta.NormNum.IsNatPowT.run
          (Mathlib.Meta.NormNum.IsNatPowT.trans
            (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit1
              Mathlib.Meta.NormNum.IsNatPowT.bit0)
            (Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0
              Mathlib.Meta.NormNum.IsNatPowT.bit1))))
      (Eq.refl false)))
24 ^ 9 < 9 ^ 25 norm_num
Goals accomplished! 🐙

example: ∀ (a b c : ℕ), a + b * c = c * b + a
example (
a: ℕ
a 
b: ℕ
b 
c: ℕ
c : 
ℕ: Type
ℕ) : 
a: ℕ
a + 
b: ℕ
b * 
c: ℕ
c = 
c: ℕ
c * 
b: ℕ
b + 
a: ℕ
a := by
Goals accomplished! 🐙
  rw [
a, b, c: ℕ
a + b * c = c * b + a
Nat.add_comm: ∀ (n m : ℕ), n + m = m + n
Nat.add_comm,
a, b, c: ℕ
b * c + a = c * b + a @
Nat.add_right_cancel_iff: ∀ {m k n : ℕ}, m + n = k + n ↔ m = k
Nat.add_right_cancel_iff,
a, b, c: ℕ
b * c = c * b 
Nat.mul_comm: ∀ (n m : ℕ), n * m = m * n
Nat.mul_comm
a, b, c: ℕ
c * b = c * b]
Goals accomplished! 🐙

example: ∀ {b : ℤ}, 0 ≤ max (-3) (b ^ 2)
example {
b: ℤ
b : 
ℤ: Type
ℤ} : 
0: ℤ
0 ≤ 
max: {α : Type} → [self : Max α] → α → α → α
max (-
3: ℤ
3) (
b: ℤ
b ^ 
2: ℕ
2) := by
Goals accomplished! 🐙 positivity
Goals accomplished! 🐙

noncomputable def 
chooseNat: (∃ x, x > 4) → ℕ
chooseNat (
h: ∃ x, x > 4
h : ∃ (
x: ℕ
x : 
ℕ: Type
ℕ), 
x: ℕ
x > 
4: ℕ
4) : 
ℕ: Type
ℕ := 
Nat.find: {p : ℕ → Prop} → [inst : DecidablePred p] → (∃ n, p n) → ℕ
Nat.find 
h: ∃ x, x > 4
h

noncomputable def 
chooseNat': (∃ x, x > 4) → ℕ
chooseNat' (
h: ∃ x, x > 4
h : ∃ (
x: ℕ
x : 
ℕ: Type
ℕ), 
x: ℕ
x > 
4: ℕ
4) : 
ℕ: Type
ℕ := 
Exists.choose: {α : Type} → {p : α → Prop} → (∃ a, p a) → α
Exists.choose 
h: ∃ x, x > 4
h

variable {
f: ℝ → ℝ
f : 
ℝ: Type
ℝ → 
ℝ: Type
ℝ}

def 
fnUB: (ℝ → ℝ) → ℝ → Prop
fnUB (
f: ℝ → ℝ
f : 
ℝ: Type
ℝ → 
ℝ: Type
ℝ) (
a: ℝ
a : 
ℝ: Type
ℝ) := ∀ 
x: ℝ
x, 
f: ℝ → ℝ
f 
x: ℝ
x ≤ 
a: ℝ
a

def 
fnHasUB: (ℝ → ℝ) → Prop
fnHasUB (
f: ℝ → ℝ
f : 
ℝ: Type
ℝ → 
ℝ: Type
ℝ) := ∃ 
a: ℝ
a, 
fnUB: (ℝ → ℝ) → ℝ → Prop
fnUB 
f: ℝ → ℝ
f 
a: ℝ
a

example: ∀ {f : ℝ → ℝ}, (∀ (a : ℝ), ∃ x, f x > a) → ¬fnHasUB f
example (
h: ∀ (a : ℝ), ∃ x, f x > a
h : ∀ 
a: ℝ
a, ∃ 
x: ℝ
x, 
f: ℝ → ℝ
f 
x: ℝ
x > 
a: ℝ
a) : ¬ 
fnHasUB: (ℝ → ℝ) → Prop
fnHasUB 
f: ℝ → ℝ
f := by
Goals accomplished! 🐙
  simp only [
fnHasUB: (ℝ → ℝ) → Prop
fnHasUB, 
fnUB: (ℝ → ℝ) → ℝ → Prop
fnUB] at *
f: ℝ → ℝ
h: ∀ (a : ℝ), ∃ x, f x > a
¬∃ a, ∀ (x : ℝ), f x ≤ a
  -- intro hh
  -- obtain ⟨a, ha⟩ := hh
  rintro 
⟨a, ha⟩: ∃ a, ∀ (x : ℝ), f x ≤ a
⟨
a: ℝ
a
⟨a, ha⟩: ∃ a, ∀ (x : ℝ), f x ≤ a
, 
ha: ∀ (x : ℝ), f x ≤ a
ha
⟨a, ha⟩: ∃ a, ∀ (x : ℝ), f x ≤ a
⟩
f: ℝ → ℝ
h: ∀ (a : ℝ), ∃ x, f x > a
a: ℝ
ha: ∀ (x : ℝ), f x ≤ a
intro
False
  specialize 
h: ∀ (a : ℝ), ∃ x, f x > a
h 
a: ℝ
a
f: ℝ → ℝ
a: ℝ
ha: ∀ (x : ℝ), f x ≤ a
h: ∃ x, f x > a
intro
False
  obtain 
⟨b, hb⟩: ∃ x, f x > a
⟨
b: ℝ
b
⟨b, hb⟩: ∃ x, f x > a
, 
hb: f b > a
hb
⟨b, hb⟩: ∃ x, f x > a
⟩ := 
h: ∃ x, f x > a
h
f: ℝ → ℝ
a: ℝ
ha: ∀ (x : ℝ), f x ≤ a
b: ℝ
hb: f b > a
intro.intro
False
  specialize 
ha: ∀ (x : ℝ), f x ≤ a
ha 
b: ℝ
b
f: ℝ → ℝ
a, b: ℝ
hb: f b > a
ha: f b ≤ a
intro.intro
False
  rw [
f: ℝ → ℝ
a, b: ℝ
hb: f b > a
ha: f b ≤ a
intro.intro
False<- 
not_lt: ∀ {α : Type ?u.6077} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ a
not_lt
f: ℝ → ℝ
a, b: ℝ
hb: f b > a
ha: ¬a < f b
intro.intro
False]
f: ℝ → ℝ
a, b: ℝ
hb: f b > a
ha: ¬a < f b
intro.intro
False at 
ha: f b ≤ a
ha
f: ℝ → ℝ
a, b: ℝ
hb: f b > a
ha: ¬a < f b
intro.intro
False
  contradiction
Goals accomplished! 🐙

example: ∀ {f : ℝ → ℝ}, ¬fnHasUB f → ∀ (a : ℝ), ∃ x, f x > a
example (
h: ¬fnHasUB f
h : ¬
fnHasUB: (ℝ → ℝ) → Prop
fnHasUB 
f: ℝ → ℝ
f) : ∀ 
a: ℝ
a, ∃ 
x: ℝ
x, 
f: ℝ → ℝ
f 
x: ℝ
x > 
a: ℝ
a := by
Goals accomplished! 🐙
  simp only [
fnHasUB: (ℝ → ℝ) → Prop
fnHasUB, 
fnUB: (ℝ → ℝ) → ℝ → Prop
fnUB] at *
f: ℝ → ℝ
h: ¬∃ a, ∀ (x : ℝ), f x ≤ a
∀ (a : ℝ), ∃ x, f x > a
  contrapose! 
h: ∃ a, ∀ (x : ℝ), f x ≤ a
h
f: ℝ → ℝ
h: ∃ a, ∀ (x : ℝ), f x ≤ a
∃ a, ∀ (x : ℝ), f x ≤ a
  obtain 
⟨a, ha⟩: ∃ a, ∀ (x : ℝ), f x ≤ a
⟨
a: ℝ
a
⟨a, ha⟩: ∃ a, ∀ (x : ℝ), f x ≤ a
, 
ha: ∀ (x : ℝ), f x ≤ a
ha
⟨a, ha⟩: ∃ a, ∀ (x : ℝ), f x ≤ a
⟩ := 
h: ∃ a, ∀ (x : ℝ), f x ≤ a
h
f: ℝ → ℝ
a: ℝ
ha: ∀ (x : ℝ), f x ≤ a
intro
∃ a, ∀ (x : ℝ), f x ≤ a
  use 
a: ℝ
a
Goals accomplished! 🐙

-- this file seems to be following https://github.com/lftcm2023/lftcm2023/blob/master/LftCM/C02_Logic/Logic.lean