You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
18 lines
368 B
Plaintext
18 lines
368 B
Plaintext
11 months ago
|
import GameServer.Tactic.LetIntros
|
||
|
|
|
||
|
|
set_option linter.unusedVariables false in
|
||
|
|
|
||
|
|
example (f : Nat) :
|
||
|
|
let f := fun x ↦ x + 1
|
||
|
|
let g : Nat → Nat := fun y ↦ y
|
||
|
|
∀ x : Nat, x ≤ f x := by
|
||
|
|
let_intros
|
||
|
|
/-
|
||
|
|
f✝ : Nat
|
||
|
|
f : Nat → Nat := fun x => x + 1
|
||
|
|
g : Nat → Nat := fun y => y
|
||
|
|
⊢ ∀ (x : Nat), x ≤ f x
|
||
|
|
-/
|
||
|
|
intro x
|
||
|
|
exact Nat.le_succ x
|