Lean 4: simple experiments with Nat

SimpleNat.lean

import Mathlib.Data.Nat.Factorization.Basic
import Mathlib.Data.Nat.Prime.Basic
open Nat
open Prime

section
-- BEGIN


def claim := ∀ p : Prop, ∀ q : Prop, p → (q → p)

#check claim
#print claim

theorem t : claim := by
  intro _ _
  exact imp_intro

#check t
#print t

theorem t0 : claim := fun {_ _} hp => fun _ => hp

#check t0
#print t0


theorem t1 {p : Prop} {q : Prop} (hp : p) : q → p := fun _ => hp

#check t1
#print t1


theorem t2 {p : Prop} {q : Prop} (hp : p) (_ : q) : p := hp

#check t2
#print t2


theorem t6 (hp : p) (hq : q) : p ∧ q := 
  And.intro hp hq


theorem t7 (hp : p) (hq : q) : p ∧ q := by
  apply And.intro
  . exact hp
  . exact hq


example : 2 = 2 := Eq.refl 2


example : 2 = 2 := by
  rfl
  
  
theorem t4 : 2 ∣ n → n ≠ 1 := by
  intro ⟨ c, h ⟩
  rw [h]
  simp [*]


lemma sq_of_even_is_even (n : Nat) : 2 ∣ n → 2 ∣ n^2 := by
  intro h -- move premise of goal into hypothesis
  obtain ⟨ k, hk ⟩ := h -- eliminate implicit existential in h
  rw [hk]
  rw [sq]
  rw [mul_assoc] -- after these rewrites, goal is 2 ∣ 2 * (k * (2 * k))
  exists k * (2 * k) -- provide witness for implicit existential in divisibility goal
-- simp [*, sq, mul_assoc]

#check sq_of_even_is_even


-- END
end