Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
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 apropDecidable
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 = FalsepropComplete ← prop_complete: ∀ (a : Prop), a = True ∨ a = Falseprop_complete -- TODO: fix in core

@[elab_as_elim] theorem cases_true_false: ∀ (p : Prop → Prop), p True → p False → ∀ (a : Prop), p acases_true_false (p: Prop → Propp : Prop: TypeProp → Prop: TypeProp)
(h1: p Trueh1 : p: Prop → Propp True: PropTrue) (h2: p Falseh2 : p: Prop → Propp False: PropFalse) (a: Propa : Prop: TypeProp) : p: Prop → Propp a: Propa :=
Or.elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → cOr.elim (prop_complete: ∀ (a : Prop), a = True ∨ a = Falseprop_complete a: Propa) (fun ht: a = Trueht : a: Propa = True: PropTrue ↦ ht: a = Trueht.symm: ∀ {α : Sort ?u.40} {a b : α}, a = b → b = asymm ▸ h1: p Trueh1) fun hf: a = Falsehf : a: Propa = False: PropFalse ↦ hf: a = Falsehf.symm: ∀ {α : Sort ?u.61} {a b : α}, a = b → b = asymm ▸ h2: p Falseh2

theorem cases_on: ∀ (a : Prop) {p : Prop → Prop}, p True → p False → p acases_on (a: Propa : Prop: TypeProp) {p: Prop → Propp : Prop: TypeProp → Prop: TypeProp} (h1: p Trueh1 : p: Prop → Propp True: PropTrue) (h2: p Falseh2 : p: Prop → Propp False: PropFalse) : p: Prop → Propp a: Propa :=
@cases_true_false: ∀ (p : Prop → Prop), p True → p False → ∀ (a : Prop), p acases_true_false p: Prop → Propp h1: p Trueh1 h2: p Falseh2 a: Propa

theorem cases: ∀ {p : Prop → Prop}, p True → p False → ∀ (a : Prop), p acases {p: Prop → Propp : Prop: TypeProp → Prop: TypeProp} (h1: p Trueh1 : p: Prop → Propp True: PropTrue) (h2: p Falseh2 : p: Prop → Propp False: PropFalse) (a: Propa) : p: Prop → Propp a: ?m.128a := cases_on: ∀ (a : Prop) {p : Prop → Prop}, p True → p False → p acases_on a: Propa h1: p Trueh1 h2: p Falseh2
#align classical.cases Classical.cases: ∀ {p : Prop → Prop}, p True → p False → ∀ (a : Prop), p aClassical.cases

alias byCases: ∀ {p q : Prop}, (p → q) → (¬p → q) → qbyCases ← by_cases: ∀ {p q : Prop}, (p → q) → (¬p → q) → qby_cases