/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
-/
import Mathlib.Tactic.Alias
import Mathlib.Tactic.IrreducibleDef
import Mathlib.Mathport.Rename
import Mathlib.Init.Logic

/-! ### alignments from lean 3 `init.classical` -/

namespace Classical

#align classical.inhabited_of_nonempty 
Classical.inhabited_of_nonempty: {α : Sort u} → Nonempty α → Inhabited α
Classical.inhabited_of_nonempty
#align classical.inhabited_of_exists 
Classical.inhabited_of_exists: {α : Sort u} → {p : α → Prop} → (∃ x, p x) → Inhabited α
Classical.inhabited_of_exists

attribute [local instance] 
propDecidable: (a : Prop) → Decidable a
propDecidable
attribute [local instance] 
decidableInhabited: (a : Prop) → Inhabited (Decidable a)
decidableInhabited

alias 
axiomOfChoice: ∀ {α : Sort u} {β : α → Sort v} {r : (x : α) → β x → Prop}, (∀ (x : α), ∃ y, r x y) → ∃ f, ∀ (x : α), r x (f x)
axiomOfChoice ← 
axiom_of_choice: ∀ {α : Sort u} {β : α → Sort v} {r : (x : α) → β x → Prop}, (∀ (x : α), ∃ y, r x y) → ∃ f, ∀ (x : α), r x (f x)
axiom_of_choice -- TODO: fix in core
alias 
propComplete: ∀ (a : Prop), a = True ∨ a = False
propComplete ← 
prop_complete: ∀ (a : Prop), a = True ∨ a = False
prop_complete -- TODO: fix in core

@[elab_as_elim] theorem 
cases_true_false: ∀ (p : Prop → Prop), p True → p False → ∀ (a : Prop), p a
cases_true_false (
p: Prop → Prop
p : 
Prop: Type
Prop → 
Prop: Type
Prop)
    (
h1: p True
h1 : 
p: Prop → Prop
p 
True: Prop
True) (
h2: p False
h2 : 
p: Prop → Prop
p 
False: Prop
False) (
a: Prop
a : 
Prop: Type
Prop) : 
p: Prop → Prop
p 
a: Prop
a :=
  
Or.elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
Or.elim (
prop_complete: ∀ (a : Prop), a = True ∨ a = False
prop_complete 
a: Prop
a) (fun 
ht: a = True
ht : 
a: Prop
a = 
True: Prop
True ↦ 
ht: a = True
ht.
symm: ∀ {α : Sort ?u.40} {a b : α}, a = b → b = a
symm ▸ 
h1: p True
h1) fun 
hf: a = False
hf : 
a: Prop
a = 
False: Prop
False ↦ 
hf: a = False
hf.
symm: ∀ {α : Sort ?u.61} {a b : α}, a = b → b = a
symm ▸ 
h2: p False
h2

theorem 
cases_on: ∀ (a : Prop) {p : Prop → Prop}, p True → p False → p a
cases_on (
a: Prop
a : 
Prop: Type
Prop) {
p: Prop → Prop
p : 
Prop: Type
Prop → 
Prop: Type
Prop} (
h1: p True
h1 : 
p: Prop → Prop
p 
True: Prop
True) (
h2: p False
h2 : 
p: Prop → Prop
p 
False: Prop
False) : 
p: Prop → Prop
p 
a: Prop
a :=
  @
cases_true_false: ∀ (p : Prop → Prop), p True → p False → ∀ (a : Prop), p a
cases_true_false 
p: Prop → Prop
p 
h1: p True
h1 
h2: p False
h2 
a: Prop
a

theorem 
cases: ∀ {p : Prop → Prop}, p True → p False → ∀ (a : Prop), p a
cases {
p: Prop → Prop
p : 
Prop: Type
Prop → 
Prop: Type
Prop} (
h1: p True
h1 : 
p: Prop → Prop
p 
True: Prop
True) (
h2: p False
h2 : 
p: Prop → Prop
p 
False: Prop
False) (
a: Prop
a) : 
p: Prop → Prop
p 
a: ?m.128
a := 
cases_on: ∀ (a : Prop) {p : Prop → Prop}, p True → p False → p a
cases_on 
a: Prop
a 
h1: p True
h1 
h2: p False
h2
#align classical.cases 
Classical.cases: ∀ {p : Prop → Prop}, p True → p False → ∀ (a : Prop), p a
Classical.cases

alias 
byCases: ∀ {p q : Prop}, (p → q) → (¬p → q) → q
byCases ← 
by_cases: ∀ {p q : Prop}, (p → q) → (¬p → q) → q
by_cases
alias 
byContradiction: ∀ {p : Prop}, (¬p → False) → p
byContradiction ← 
by_contradiction: ∀ {p : Prop}, (¬p → False) → p
by_contradiction

theorem 
eq_false_or_eq_true: ∀ (a : Prop), a = False ∨ a = True
eq_false_or_eq_true (
a: Prop
a : 
Prop: Type
Prop) : 
a: Prop
a = 
False: Prop
False ∨ 
a: Prop
a = 
True: Prop
True := (
prop_complete: ∀ (a : Prop), a = True ∨ a = False
prop_complete 
a: Prop
a).
symm: ∀ {a b : Prop}, a ∨ b → b ∨ a
symm

end Classical