Skip to content

Instantly share code, notes, and snippets.

@Ruben-VandeVelde

Ruben-VandeVelde/classical.lean Secret

Created September 8, 2020 12:43
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Ruben-VandeVelde/89dd1e210dd3ff14056062eb35da86ec to your computer and use it in GitHub Desktop.
Save Ruben-VandeVelde/89dd1e210dd3ff14056062eb35da86ec to your computer and use it in GitHub Desktop.
Download ZIP
TPL, Ex 4.6.2 b
Raw
classical.lean
example (α : Type*) (p : α → Prop) (s : Prop) : (∀ x, p x ∨ s) ↔ (∀ x, p x) ∨ s :=
begin
split,
{ intro h1,
by_cases s,
{ right, assumption },
{ left,
intro x,
have h2 := h1 x,
cases h2 with h3 h4,
{exact h3},
{contradiction} } },
{ intro h1,
cases h1,
{ intro x, left, apply h1, },
{ intro x, right, assumption } }
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment