Skip to content

Instantly share code, notes, and snippets.

@ammkrn

ammkrn/notes.lean

Created August 30, 2024 01:45
Show Gist options
  • Save ammkrn/1688038761909b609b44fd411ec62c22 to your computer and use it in GitHub Desktop.
Save ammkrn/1688038761909b609b44fd411ec62c22 to your computer and use it in GitHub Desktop.
Download ZIP
SF Lean meeting notes 8/29
Raw
notes.lean
import Mathlib.Tactic
-- Click `apply`
example (n : Nat) : n ≠ 0 → n / 2 ^ 1 < n := by apply?
example (n : Nat) : n ≠ 0 → n / 2 ^ 1 < n := by omega
example (p q r : Prop) : (q ∧ p) → (p → r) → r ∧ q := by tauto
-- rcases + refine
example (a b c d p : Prop) (hp: p) (h : (a ∧ b) ∨ (c ∧ d)) : p ∧ (a ∨ c) := by
refine And.intro ?l ?r
case l => exact hp
case r =>
rcases h with ⟨ha, _hb⟩ | ⟨hc, _hd⟩
. exact Or.inl ha
. exact Or.inr hc
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment