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, Floris van Doorn
-/
import Std.Tactic.Ext
import Std.Tactic.Lint.Basic
import Std.Logic
import Std.WF
import Mathlib.Tactic.Alias
import Mathlib.Tactic.Basic
import Mathlib.Tactic.Relation.Rfl
import Mathlib.Tactic.Relation.Symm
import Mathlib.Mathport.Attributes
import Mathlib.Mathport.Rename
import Mathlib.Tactic.Relation.Trans

#align opt_param_eq optParam_eq: ∀ (α : Sort u) (default : α), optParam α default = αoptParam_eq

/- Implication -/

@[deprecated] def Implies: Prop → Prop → PropImplies (a: Propa b: Propb : Prop: TypeProp) := a: Propa → b: Propb

/-- Implication `→` is transitive. If `P → Q` and `Q → R` then `P → R`. -/
-- FIXME This should have `@[trans]`, but the `trans` attribute PR'd in #253 rejects it.
-- Note that it is still rejected after #857.
@[deprecated] theorem Implies.trans: ∀ {p q r : Prop}, (p → q) → (q → r) → p → rImplies.trans {p: Propp q: Propq r: Propr : Prop: TypeProp} (h₁: p → qh₁ : p: Propp → q: Propq) (h₂: q → rh₂ : q: Propq → r: Propr) :
p: Propp → r: Propr := fun hp: ?m.48hp ↦ h₂: q → rh₂ (h₁: p → qh₁ hp: ?m.48hp)

/- Not -/

@[deprecated] def NonContradictory: Prop → PropNonContradictory (a: Propa : Prop: TypeProp) : Prop: TypeProp := ¬¬a: Propa

#align non_contradictory_intro not_not_intro: ∀ {p : Prop}, p → ¬¬pnot_not_intro

/- Eq -/

alias proofIrrel: ∀ {a : Prop} (h₁ h₂ : a), h₁ = h₂proofIrrel ← proof_irrel: ∀ {a : Prop} (h₁ h₂ : a), h₁ = h₂proof_irrel
alias congrFun: ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g acongrFun ← congr_fun: ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g acongr_fun
alias congrArg: ∀ {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂congrArg ← congr_arg: ∀ {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂congr_arg

@[deprecated] theorem trans_rel_left: ∀ {α : Sort u} {a b c : α} (r : α → α → Prop), r a b → b = c → r a ctrans_rel_left {α: Sort uα : Sort u: Type uSortSort u: Type u u} {a: αa b: αb c: αc : α: Sort uα}
(r: α → α → Propr : α: Sort uα → α: Sort uα → Prop: TypeProp) (h₁: r a bh₁ : r: α → α → Propr a: αa b: αb) (h₂: b = ch₂ : b: αb = c: αc) : r: α → α → Propr a: αa c: αc := h₂: b = ch₂ ▸ h₁: r a bh₁

@[deprecated] theorem trans_rel_right: ∀ {α : Sort u} {a b c : α} (r : α → α → Prop), a = b → r b c → r a ctrans_rel_right {α: Sort uα : Sort u: Type uSortSort u: Type u u} {a: αa b: αb c: αc : α: Sort uα}
(r: α → α → Propr : α: Sort uα → α: Sort uα → Prop: TypeProp) (h₁: a = bh₁ : a: αa = b: αb) (h₂: r b ch₂ : r: α → α → Propr b: αb c: αc) : r: α → α → Propr a: αa c: αc := h₁: a = bh₁ ▸ h₂: r b ch₂

theorem not_of_eq_false: ∀ {p : Prop}, p = False → ¬pnot_of_eq_false {p: Propp : Prop: TypeProp} (h: p = Falseh : p: Propp = False: PropFalse) : ¬p: Propp := fun hp: ?m.171hp ↦ h: p = Falseh ▸ hp: ?m.171hp

theorem cast_proof_irrel: ∀ {α β : Sort u_1} (h₁ h₂ : α = β) (a : α), cast h₁ a = cast h₂ acast_proof_irrel (h₁: α = βh₁ h₂: α = βh₂ : α: ?m.188α = β: ?m.193β) (a: αa : α: ?m.188α) : cast: {α β : Sort ?u.209} → α = β → α → βcast h₁: α = βh₁ a: αa = cast: {α β : Sort ?u.218} → α = β → α → βcast h₂: α = βh₂ a: αa := rfl: ∀ {α : Sort ?u.231} {a : α}, a = arfl

attribute [symm] Eq.symm: ∀ {α : Sort u} {a b : α}, a = b → b = aEq.symm

/- Ne -/

theorem Ne.def: ∀ {α : Sort u} (a b : α), (a ≠ b) = ¬a = bNe.def {α: Sort uα : Sort u: Type uSortSort u: Type u u} (a: αa b: αb : α: Sort uα) : (a: αa ≠ b: αb) = ¬ (a: αa = b: αb) := rfl: ∀ {α : Sort ?u.268} {a : α}, a = arfl

attribute [symm] Ne.symm: ∀ {α : Sort u} {a b : α}, a ≠ b → b ≠ aNe.symm

/- HEq -/

alias eqRec_heq: ∀ {α : Sort u} {φ : α → Sort v} {a a' : α} (h : a = a') (p : φ a), HEq (Eq.recOn h p) peqRec_heq ← eq_rec_heq: ∀ {α : Sort u} {φ : α → Sort v} {a a' : α} (h : a = a') (p : φ a), HEq (Eq.recOn h p) peq_rec_heq

-- FIXME This is still rejected after #857
-- attribute [refl] HEq.refl
attribute [symm] HEq.symm: ∀ {α β : Sort u} {a : α} {b : β}, HEq a b → HEq b aHEq.symm
attribute [trans] HEq.trans: ∀ {α β φ : Sort u} {a : α} {b : β} {c : φ}, HEq a b → HEq b c → HEq a cHEq.trans
attribute [trans] heq_of_eq_of_heq: ∀ {α β : Sort u} {a a' : α} {b : β}, a = a' → HEq a' b → HEq a bheq_of_eq_of_heq

theorem heq_of_eq_rec_left: ∀ {α : Sort u_1} {φ : α → Sort v} {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a'), e ▸ p₁ = p₂ → HEq p₁ p₂heq_of_eq_rec_left {φ: α → Sort vφ : α: ?m.311α → Sort v: Type vSortSort v: Type v v} {a: αa a': αa' : α: ?m.311α} {p₁: φ ap₁ : φ: α → Sort vφ a: αa} {p₂: φ a'p₂ : φ: α → Sort vφ a': αa'} :
(e: a = a'e : a: αa = a': αa') → (h₂: e ▸ p₁ = p₂h₂ : Eq.rec: {α : Sort ?u.333} →
{a : α} →
{motive : (a_1 : α) → a = a_1 → Sort ?u.334} → motive a (_ : a = a) → {a_1 : α} → (t : a = a_1) → motive a_1 tEq.rec (motive := fun a: ?m.352a _: ?m.355_ ↦ φ: α → Sort vφ a: ?m.352a) p₁: φ ap₁ e: a = a'e = p₂: φ a'p₂) → HEq: {α : Sort ?u.369} → α → {β : Sort ?u.369} → β → PropHEq p₁: φ ap₁ p₂: φ a'p₂
| rfl: ∀ {α : Sort ?u.555} {a : α}, a = arfl, rfl: ∀ {α : Sort ?u.559} {a : α}, a = arfl => HEq.rfl: ∀ {α : Sort ?u.603} {a : α}, HEq a aHEq.rfl

theorem heq_of_eq_rec_right: ∀ {α : Sort u_1} {φ : α → Sort v} {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a), p₁ = e ▸ p₂ → HEq p₁ p₂heq_of_eq_rec_right {φ: α → Sort vφ : α: ?m.905α → Sort v: Type vSortSort v: Type v v} {a: αa a': αa' : α: ?m.905α} {p₁: φ ap₁ : φ: α → Sort vφ a: αa} {p₂: φ a'p₂ : φ: α → Sort vφ a': αa'} :
(e: a' = ae : a': αa' = a: αa) → (h₂: p₁ = e ▸ p₂h₂ : p₁: φ ap₁ = Eq.rec: {α : Sort ?u.927} →
{a : α} →
{motive : (a_1 : α) → a = a_1 → Sort ?u.928} → motive a (_ : a = a) → {a_1 : α} → (t : a = a_1) → motive a_1 tEq.rec (motive := fun a: ?m.946a _: ?m.949_ ↦ φ: α → Sort vφ a: ?m.946a) p₂: φ a'p₂ e: a' = ae) → HEq: {α : Sort ?u.963} → α → {β : Sort ?u.963} → β → PropHEq p₁: φ ap₁ p₂: φ a'p₂
| rfl: ∀ {α : Sort u_1} {a : α}, a = arfl, rfl: ∀ {α : Sort ?u.1153} {a : α}, a = arfl => HEq.rfl: ∀ {α : Sort ?u.1196} {a : α}, HEq a aHEq.rfl

theorem of_heq_true: ∀ {a : Prop}, HEq a True → aof_heq_true {a: Propa : Prop: TypeProp} (h: HEq a Trueh : HEq: {α : Sort ?u.1498} → α → {β : Sort ?u.1498} → β → PropHEq a: Propa True: PropTrue) : a: Propa := of_eq_true: ∀ {p : Prop}, p = True → pof_eq_true (eq_of_heq: ∀ {α : Sort ?u.1507} {a a' : α}, HEq a a' → a = a'eq_of_heq h: HEq a Trueh)

theorem eq_rec_compose: ∀ {α β φ : Sort u} (p₁ : β = φ) (p₂ : α = β) (a : α), Eq.recOn p₁ (Eq.recOn p₂ a) = Eq.recOn (_ : α = φ) aeq_rec_compose {α: Sort uα β: Sort uβ φ: Sort uφ : Sort u: Type uSortSort u: Type u u} :
∀ (p₁: β = φp₁ : β: Sort uβ = φ: Sort uφ) (p₂: α = βp₂ : α: Sort uα = β: Sort uβ) (a: αa : α: Sort uα),
(Eq.recOn: {α : Sort ?u.1540} →
{a : α} →
{motive : (a_1 : α) → a = a_1 → Sort ?u.1541} → {a_1 : α} → (t : a = a_1) → motive a (_ : a = a) → motive a_1 tEq.recOn p₁: β = φp₁ (Eq.recOn: {α : Sort ?u.1578} →
{a : α} →
{motive : (a_1 : α) → a = a_1 → Sort ?u.1579} → {a_1 : α} → (t : a = a_1) → motive a (_ : a = a) → motive a_1 tEq.recOn p₂: α = βp₂ a: αa : β: Sort uβ) : φ: Sort uφ) = Eq.recOn: {α : Sort ?u.1648} →
{a : α} →
{motive : (a_1 : α) → a = a_1 → Sort ?u.1649} → {a_1 : α} → (t : a = a_1) → motive a (_ : a = a) → motive a_1 tEq.recOn (Eq.trans: ∀ {α : Sort ?u.1674} {a b c : α}, a = b → b = c → a = cEq.trans p₂: α = βp₂ p₁: β = φp₁) a: αa
| rfl: ∀ {α : Sort ?u.2023} {a : α}, a = arfl, rfl: ∀ {α : Sort ?u.2027} {a : α}, a = arfl, _ => rfl: ∀ {α : Sort ?u.2072} {a : α}, a = arfl

/- and -/

variable {a: Propa b: Propb c: Propc d: Propd : Prop: TypeProp}

#align and.symm And.symm: ∀ {a b : Prop}, a ∧ b → b ∧ aAnd.symm
#align and.swap And.symm: ∀ {a b : Prop}, a ∧ b → b ∧ aAnd.symm

/- or -/

#align non_contradictory_em not_not_em: ∀ (a : Prop), ¬¬(a ∨ ¬a)not_not_em
#align or.symm Or.symm: ∀ {a b : Prop}, a ∨ b → b ∨ aOr.symm
#align or.swap Or.symm: ∀ {a b : Prop}, a ∨ b → b ∨ aOr.symm

/- xor -/

def Xor': (a b : Prop) → ?m.2374 a bXor' (a: Propa b: Propb : Prop: TypeProp) := (a: Propa ∧ ¬ b: Propb) ∨ (b: Propb ∧ ¬ a: Propa)
#align xor Xor': Prop → Prop → PropXor'

/- iff -/

#align iff.mp Iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → bIff.mp
#align iff.elim_left Iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → bIff.mp
#align iff.mpr Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → aIff.mpr
#align iff.elim_right Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → aIff.mpr

attribute [refl] Iff.refl: ∀ (a : Prop), a ↔ aIff.refl
attribute [trans] Iff.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)Iff.trans
attribute [symm] Iff.symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)Iff.symm

-- This is needed for `calc` to work with `iff`.
instance: Trans Iff Iff Iffinstance : Trans: {α : Sort ?u.2406} →
{β : Sort ?u.2405} →
{γ : Sort ?u.2404} →
(α → β → Sort ?u.2409) →
(β → γ → Sort ?u.2408) →
outParam (α → γ → Sort ?u.2407) →
Sort (max(max(max(max(max(max1?u.2409)?u.2406)?u.2405)?u.2404)?u.2408)?u.2407)Trans Iff: Prop → Prop → PropIff Iff: Prop → Prop → PropIff Iff: Prop → Prop → PropIff where
trans := fun p: ?m.2468p q: ?m.2471q ↦ p: ?m.2468p.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)trans q: ?m.2471q

#align not_congr not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)not_congr
#align not_iff_not_of_iff not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)not_congr
#align not_non_contradictory_iff_absurd not_not_not: ∀ {a : Prop}, ¬¬¬a ↔ ¬anot_not_not

alias not_not_not: ∀ {a : Prop}, ¬¬¬a ↔ ¬anot_not_not ↔ not_of_not_not_not: ∀ {a : Prop}, ¬¬¬a → ¬anot_of_not_not_not _

-- FIXME
-- attribute [congr] not_congr

@[deprecated and_comm: ∀ {a b : Prop}, a ∧ b ↔ b ∧ aand_comm] theorem and_comm': ∀ (a b : Prop), a ∧ b ↔ b ∧ aand_comm' (a: Propa b: ?m.2631b) : a: ?m.2628a ∧ b: ?m.2631b ↔ b: ?m.2631b ∧ a: ?m.2628a := and_comm: ∀ {a b : Prop}, a ∧ b ↔ b ∧ aand_comm
#align and.comm and_comm: ∀ {a b : Prop}, a ∧ b ↔ b ∧ aand_comm
#align and_comm and_comm': ∀ (a b : Prop), a ∧ b ↔ b ∧ aand_comm'

@[deprecated and_assoc: ∀ {a b c : Prop}, (a ∧ b) ∧ c ↔ a ∧ b ∧ cand_assoc] theorem and_assoc': ∀ (a b : Prop), (a ∧ b) ∧ c ↔ a ∧ b ∧ cand_assoc' (a: ?m.2654a b: Propb) : (a: ?m.2654a ∧ b: ?m.2657b) ∧ c: Propc ↔ a: ?m.2654a ∧ (b: ?m.2657b ∧ c: Propc) := and_assoc: ∀ {a b c : Prop}, (a ∧ b) ∧ c ↔ a ∧ b ∧ cand_assoc
#align and_assoc and_assoc': ∀ {c : Prop} (a b : Prop), (a ∧ b) ∧ c ↔ a ∧ b ∧ cand_assoc'
#align and.assoc and_assoc: ∀ {a b c : Prop}, (a ∧ b) ∧ c ↔ a ∧ b ∧ cand_assoc

#align and.left_comm and_left_comm: ∀ {a b c : Prop}, a ∧ b ∧ c ↔ b ∧ a ∧ cand_left_comm

#align and_iff_left and_iff_leftₓ: ∀ {b a : Prop}, b → (a ∧ b ↔ a)and_iff_leftₓ -- reorder implicits

variable (p: ?m.2789p)

-- FIXME: remove _iff and add _eq for the lean 4 core versions
theorem and_true_iff: p ∧ True ↔ pand_true_iff : p: ?m.2693p ∧ True: PropTrue ↔ p: ?m.2693p := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (and_true: ∀ (p : Prop), (p ∧ True) = pand_true _: Prop_)
#align and_true and_true_iff: ∀ (p : Prop), p ∧ True ↔ pand_true_iff
theorem true_and_iff: True ∧ p ↔ ptrue_and_iff : True: PropTrue ∧ p: ?m.2717p ↔ p: ?m.2717p := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (true_and: ∀ (p : Prop), (True ∧ p) = ptrue_and _: Prop_)
#align true_and true_and_iff: ∀ (p : Prop), True ∧ p ↔ ptrue_and_iff
theorem and_false_iff: ∀ (p : Prop), p ∧ False ↔ Falseand_false_iff : p: ?m.2741p ∧ False: PropFalse ↔ False: PropFalse := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (and_false: ∀ (p : Prop), (p ∧ False) = Falseand_false _: Prop_)
#align and_false and_false_iff: ∀ (p : Prop), p ∧ False ↔ Falseand_false_iff
theorem false_and_iff: ∀ (p : Prop), False ∧ p ↔ Falsefalse_and_iff : False: PropFalse ∧ p: ?m.2765p ↔ False: PropFalse := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (false_and: ∀ (p : Prop), (False ∧ p) = Falsefalse_and _: Prop_)
#align false_and false_and_iff: ∀ (p : Prop), False ∧ p ↔ Falsefalse_and_iff
#align not_and_self not_and_self_iff: ∀ (a : Prop), ¬a ∧ a ↔ Falsenot_and_self_iff
#align and_not_self and_not_self_iff: ∀ (a : Prop), a ∧ ¬a ↔ Falseand_not_self_iff
theorem and_self_iff: p ∧ p ↔ pand_self_iff : p: ?m.2789p ∧ p: ?m.2789p ↔ p: ?m.2789p := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (and_self: ∀ (p : Prop), (p ∧ p) = pand_self _: Prop_)
#align and_self and_self_iff: ∀ (p : Prop), p ∧ p ↔ pand_self_iff

#align or.imp Or.impₓ: ∀ {a c b d : Prop}, (a → c) → (b → d) → a ∨ b → c ∨ dOr.impₓ -- reorder implicits

#align and.elim And.elimₓ: {a b : Prop} → {α : Sort u_1} → (a → b → α) → a ∧ b → αAnd.elimₓ
#align iff.elim Iff.elimₓ: {a b : Prop} → {α : Sort u_1} → ((a → b) → (b → a) → α) → (a ↔ b) → αIff.elimₓ
#align imp_congr imp_congrₓ: ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a → b ↔ c → d)imp_congrₓ
#align imp_congr_ctx imp_congr_ctxₓ: ∀ {a c b d : Prop}, (a ↔ c) → (c → (b ↔ d)) → (a → b ↔ c → d)imp_congr_ctxₓ
#align imp_congr_right imp_congr_rightₓ: ∀ {a : Sort u_1} {b c : Prop}, (a → (b ↔ c)) → (a → b ↔ a → c)imp_congr_rightₓ

#align eq_true_intro eq_true: ∀ {p : Prop}, p → p = Trueeq_true
#align eq_false_intro eq_false: ∀ {p : Prop}, ¬p → p = Falseeq_false

@[deprecated or_comm: ∀ {a b : Prop}, a ∨ b ↔ b ∨ aor_comm] theorem or_comm': ∀ (a b : Prop), a ∨ b ↔ b ∨ aor_comm' (a: Propa b: ?m.2819b) : a: ?m.2816a ∨ b: ?m.2819b ↔ b: ?m.2819b ∨ a: ?m.2816a := or_comm: ∀ {a b : Prop}, a ∨ b ↔ b ∨ aor_comm
#align or.comm or_comm: ∀ {a b : Prop}, a ∨ b ↔ b ∨ aor_comm
#align or_comm or_comm': ∀ (a b : Prop), a ∨ b ↔ b ∨ aor_comm'

@[deprecated or_assoc: ∀ {a b c : Prop}, (a ∨ b) ∨ c ↔ a ∨ b ∨ cor_assoc] theorem or_assoc': ∀ {c : Prop} (a b : Prop), (a ∨ b) ∨ c ↔ a ∨ b ∨ cor_assoc' (a: Propa b: ?m.2848b) : (a: ?m.2845a ∨ b: ?m.2848b) ∨ c: Propc ↔ a: ?m.2845a ∨ (b: ?m.2848b ∨ c: Propc) := or_assoc: ∀ {a b c : Prop}, (a ∨ b) ∨ c ↔ a ∨ b ∨ cor_assoc
#align or.assoc or_assoc: ∀ {a b c : Prop}, (a ∨ b) ∨ c ↔ a ∨ b ∨ cor_assoc
#align or_assoc or_assoc': ∀ {c : Prop} (a b : Prop), (a ∨ b) ∨ c ↔ a ∨ b ∨ cor_assoc'

#align or_left_comm or_left_comm: ∀ {a b c : Prop}, a ∨ b ∨ c ↔ b ∨ a ∨ cor_left_comm
#align or.left_comm or_left_comm: ∀ {a b c : Prop}, a ∨ b ∨ c ↔ b ∨ a ∨ cor_left_comm

#align or_iff_left_of_imp or_iff_left_of_impₓ: ∀ {b a : Prop}, (b → a) → (a ∨ b ↔ a)or_iff_left_of_impₓ -- reorder implicits

theorem true_or_iff: True ∨ p ↔ Truetrue_or_iff : True: PropTrue ∨ p: ?m.2873p ↔ True: PropTrue := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (true_or: ∀ (p : Prop), (True ∨ p) = Truetrue_or _: Prop_)
#align true_or true_or_iff: ∀ (p : Prop), True ∨ p ↔ Truetrue_or_iff
theorem or_true_iff: p ∨ True ↔ Trueor_true_iff : p: ?m.2897p ∨ True: PropTrue ↔ True: PropTrue := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (or_true: ∀ (p : Prop), (p ∨ True) = Trueor_true _: Prop_)
#align or_true or_true_iff: ∀ (p : Prop), p ∨ True ↔ Trueor_true_iff
theorem false_or_iff: ∀ (p : Prop), False ∨ p ↔ pfalse_or_iff : False: PropFalse ∨ p: ?m.2921p ↔ p: ?m.2921p := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (false_or: ∀ (p : Prop), (False ∨ p) = pfalse_or _: Prop_)
#align false_or false_or_iff: ∀ (p : Prop), False ∨ p ↔ pfalse_or_iff
theorem or_false_iff: p ∨ False ↔ por_false_iff : p: ?m.2945p ∨ False: PropFalse ↔ p: ?m.2945p := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (or_false: ∀ (p : Prop), (p ∨ False) = por_false _: Prop_)
#align or_false or_false_iff: ∀ (p : Prop), p ∨ False ↔ por_false_iff
theorem or_self_iff: p ∨ p ↔ por_self_iff : p: ?m.2969p ∨ p: ?m.2969p ↔ p: ?m.2969p := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (or_self: ∀ (p : Prop), (p ∨ p) = por_self _: Prop_)
#align or_self or_self_iff: ∀ (p : Prop), p ∨ p ↔ por_self_iff

theorem not_or_of_not: ∀ {a b : Prop}, ¬a → ¬b → ¬(a ∨ b)not_or_of_not : ¬a: Propa → ¬b: Propb → ¬(a: Propa ∨ b: Propb) := fun h1: ?m.3004h1 h2: ?m.3007h2 ↦ not_or: ∀ {p q : Prop}, ¬(p ∨ q) ↔ ¬p ∧ ¬qnot_or.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 ⟨h1: ?m.3004h1, h2: ?m.3007h2⟩
#align not_or not_or_of_not: ∀ {a b : Prop}, ¬a → ¬b → ¬(a ∨ b)not_or_of_not

theorem iff_true_iff: (a ↔ True) ↔ aiff_true_iff : (a: Propa ↔ True: PropTrue) ↔ a: Propa := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (iff_true: ∀ (p : Prop), (p ↔ True) = piff_true _: Prop_)
#align iff_true iff_true_iff: ∀ {a : Prop}, (a ↔ True) ↔ aiff_true_iff
theorem true_iff_iff: ∀ {a : Prop}, (True ↔ a) ↔ atrue_iff_iff : (True: PropTrue ↔ a: Propa) ↔ a: Propa := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (true_iff: ∀ (p : Prop), (True ↔ p) = ptrue_iff _: Prop_)
#align true_iff true_iff_iff: ∀ {a : Prop}, (True ↔ a) ↔ atrue_iff_iff

theorem iff_false_iff: ∀ {a : Prop}, (a ↔ False) ↔ ¬aiff_false_iff : (a: Propa ↔ False: PropFalse) ↔ ¬a: Propa := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (iff_false: ∀ (p : Prop), (p ↔ False) = ¬piff_false _: Prop_)
#align iff_false iff_false_iff: ∀ {a : Prop}, (a ↔ False) ↔ ¬aiff_false_iff

theorem false_iff_iff: (False ↔ a) ↔ ¬afalse_iff_iff : (False: PropFalse ↔ a: Propa) ↔ ¬a: Propa := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (false_iff: ∀ (p : Prop), (False ↔ p) = ¬pfalse_iff _: Prop_)
#align false_iff false_iff_iff: ∀ {a : Prop}, (False ↔ a) ↔ ¬afalse_iff_iff

theorem iff_self_iff: ∀ (a : Prop), (a ↔ a) ↔ Trueiff_self_iff (a: Propa : Prop: TypeProp) : (a: Propa ↔ a: Propa) ↔ True: PropTrue := iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)iff_of_eq (iff_self: ∀ (p : Prop), (p ↔ p) = Trueiff_self _: Prop_)
#align iff_self iff_self_iff: ∀ (a : Prop), (a ↔ a) ↔ Trueiff_self_iff

#align iff_congr iff_congrₓ: ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → ((a ↔ b) ↔ (c ↔ d))iff_congrₓ -- reorder implicits

#align implies_true_iff imp_true_iff: ∀ (α : Sort u), α → True ↔ Trueimp_true_iff
#align false_implies_iff false_imp_iff: ∀ (a : Prop), False → a ↔ Truefalse_imp_iff
#align true_implies_iff true_imp_iff: ∀ (α : Prop), True → α ↔ αtrue_imp_iff

#align Exists Exists: {α : Sort u} → (α → Prop) → PropExists -- otherwise it would get the name ExistsCat

-- TODO
-- attribute [intro] Exists.intro

/- exists unique -/

def ExistsUnique: {α : Sort ?u.3168} → (p : α → Prop) → ?m.3173 pExistsUnique (p: α → Propp : α: ?m.3165α → Prop: TypeProp) := ∃ x: ?m.3184x, p: α → Propp x: ?m.3184x ∧ ∀ y: ?m.3187y, p: α → Propp y: ?m.3187y → y: ?m.3187y = x: ?m.3184x

open Lean TSyntax.Compat in
macro "∃! " xs: ?m.3358xs:explicitBinders: ParserDescrexplicitBinders ", " b: ?m.3346b:term: Parser.Categoryterm : term: Parser.Categoryterm => expandExplicitBinders: Name → Syntax → Syntax → MacroM SyntaxexpandExplicitBinders ``ExistsUnique: {α : Sort u_1} → (α → Prop) → PropExistsUnique xs: ?m.3358xs b: ?m.3346b

/-- Pretty-printing for `ExistsUnique`, following the same pattern as pretty printing
for `Exists`. -/
@[app_unexpander ExistsUnique: {α : Sort u_1} → (α → Prop) → PropExistsUnique] def unexpandExistsUnique: Lean.PrettyPrinter.UnexpanderunexpandExistsUnique : Lean.PrettyPrinter.Unexpander: TypeLean.PrettyPrinter.Unexpander
| `(\$(_) fun \$x: ?m.5187x:ident ↦ ∃! \$xs: ?m.5180xs:binderIdent*, \$b: ?m.5171b) => `(∃! \$x: ?m.5187x:ident \$xs: ?m.5180xs:binderIdent*, \$b: ?m.5171b)
| `(\$(_) fun \$x: ?m.5715x:ident ↦ \$b: ?m.5708b)                      => `(∃! \$x: ?m.6364x:ident, \$b: ?m.6357b)
| `(\$(_) fun (\$x: ?m.7180x:ident : \$t: ?m.7173t) ↦ \$b: ?m.7166b)               => `(∃! (\$x: ?m.7180x:ident : \$t: ?m.7173t), \$b: ?m.7166b)
| _                                               => throw: {ε : outParam (Type ?u.7860)} →
{m : Type ?u.7859 → Type ?u.7858} → [self : MonadExcept ε m] → {α : Type ?u.7859} → ε → m αthrow (): Unit()

-- @[intro] -- TODO
theorem ExistsUnique.intro: ∀ {α : Sort u_1} {p : α → Prop} (w : α), p w → (∀ (y : α), p y → y = w) → ∃! x, p xExistsUnique.intro {p: α → Propp : α: ?m.24288α → Prop: TypeProp} (w: αw : α: ?m.24288α)
(h₁: p wh₁ : p: α → Propp w: αw) (h₂: ∀ (y : α), p y → y = wh₂ : ∀ y: ?m.24300y, p: α → Propp y: ?m.24300y → y: ?m.24300y = w: αw) : ∃! x: ?m.24312x, p: α → Propp x: ?m.24312x := ⟨w: αw, h₁: p wh₁, h₂: ∀ (y : α), p y → y = wh₂⟩

theorem ExistsUnique.elim: ∀ {α : Sort u} {p : α → Prop} {b : Prop}, (∃! x, p x) → (∀ (x : α), p x → (∀ (y : α), p y → y = x) → b) → bExistsUnique.elim {α: Sort uα : Sort u: Type uSortSort u: Type u u} {p: α → Propp : α: Sort uα → Prop: TypeProp} {b: Propb : Prop: TypeProp}
(h₂: ∃! x, p xh₂ : ∃! x: ?m.24393x, p: α → Propp x: ?m.24393x) (h₁: ∀ (x : α), p x → (∀ (y : α), p y → y = x) → bh₁ : ∀ x: ?m.24400x, p: α → Propp x: ?m.24400x → (∀ y: ?m.24407y, p: α → Propp y: ?m.24407y → y: ?m.24407y = x: ?m.24400x) → b: Propb) : b: Propb :=
Exists.elim: ∀ {α : Sort ?u.24423} {p : α → Prop} {b : Prop}, (∃ x, p x) → (∀ (a : α), p a → b) → bExists.elim h₂: ∃! x, p xh₂ (λ w: ?m.24434w hw: ?m.24437hw => h₁: ∀ (x : α), p x → (∀ (y : α), p y → y = x) → bh₁ w: ?m.24434w (And.left: ∀ {a b : Prop}, a ∧ b → aAnd.left hw: ?m.24437hw) (And.right: ∀ {a b : Prop}, a ∧ b → bAnd.right hw: ?m.24437hw))

theorem exists_unique_of_exists_of_unique: ∀ {α : Sort u} {p : α → Prop}, (∃ x, p x) → (∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂) → ∃! x, p xexists_unique_of_exists_of_unique {α: Sort uα : Sort u: Type uSortSort u: Type u u} {p: α → Propp : α: Sort uα → Prop: TypeProp}
(hex: ∃ x, p xhex : ∃ x: ?m.24502x, p: α → Propp x: ?m.24502x) (hunique: ∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂hunique : ∀ y₁: ?m.24509y₁ y₂: ?m.24512y₂, p: α → Propp y₁: ?m.24509y₁ → p: α → Propp y₂: ?m.24512y₂ → y₁: ?m.24509y₁ = y₂: ?m.24512y₂) : ∃! x: ?m.24526x, p: α → Propp x: ?m.24526x :=
Exists.elim: ∀ {α : Sort ?u.24538} {p : α → Prop} {b : Prop}, (∃ x, p x) → (∀ (a : α), p a → b) → bExists.elim hex: ∃ x, p xhex (λ x: ?m.24552x px: ?m.24555px => ExistsUnique.intro: ∀ {α : Sort ?u.24557} {p : α → Prop} (w : α), p w → (∀ (y : α), p y → y = w) → ∃! x, p xExistsUnique.intro x: ?m.24552x px: ?m.24555px (λ y: ?m.24566y (h: p yh : p: α → Propp y: ?m.24566y) => hunique: ∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂hunique y: ?m.24566y x: ?m.24552x h: p yh px: ?m.24555px))

theorem ExistsUnique.exists: ∀ {α : Sort u_1} {p : α → Prop}, (∃! x, p x) → ∃ x, p xExistsUnique.exists {p: α → Propp : α: ?m.24609α → Prop: TypeProp} : (∃! x: ?m.24620x, p: α → Propp x: ?m.24620x) → ∃ x: ?m.24628x, p: α → Propp x: ?m.24628x | ⟨x: αx, h: (fun x => p x) xh, _⟩ => ⟨x: αx, h: (fun x => p x) xh⟩
#align exists_of_exists_unique ExistsUnique.exists: ∀ {α : Sort u_1} {p : α → Prop}, (∃! x, p x) → ∃ x, p xExistsUnique.exists
#align exists_unique.exists ExistsUnique.exists: ∀ {α : Sort u_1} {p : α → Prop}, (∃! x, p x) → ∃ x, p xExistsUnique.exists

theorem ExistsUnique.unique: ∀ {α : Sort u} {p : α → Prop}, (∃! x, p x) → ∀ {y₁ y₂ : α}, p y₁ → p y₂ → y₁ = y₂ExistsUnique.unique {α: Sort uα : Sort u: Type uSortSort u: Type u u} {p: α → Propp : α: Sort uα → Prop: TypeProp}
(h: ∃! x, p xh : ∃! x: ?m.24901x, p: α → Propp x: ?m.24901x) {y₁: αy₁ y₂: αy₂ : α: Sort uα} (py₁: p y₁py₁ : p: α → Propp y₁: αy₁) (py₂: p y₂py₂ : p: α → Propp y₂: αy₂) : y₁: αy₁ = y₂: αy₂ :=
let ⟨_: α_, _, hy: ∀ (y : α), (fun x => p x) y → y = w✝hy⟩ := h: ∃! x, p xh; (hy: ∀ (y : α), (fun x => p x) y → y = w✝hy _: α_ py₁: p y₁py₁).trans: ∀ {α : Sort ?u.25008} {a b c : α}, a = b → b = c → a = ctrans (hy: ∀ (y : α), (fun x => p x) y → y = w✝hy _: α_ py₂: p y₂py₂).symm: ∀ {α : Sort ?u.25023} {a b : α}, a = b → b = asymm
#align unique_of_exists_unique ExistsUnique.unique: ∀ {α : Sort u} {p : α → Prop}, (∃! x, p x) → ∀ {y₁ y₂ : α}, p y₁ → p y₂ → y₁ = y₂ExistsUnique.unique
#align exists_unique.unique ExistsUnique.unique: ∀ {α : Sort u} {p : α → Prop}, (∃! x, p x) → ∀ {y₁ y₂ : α}, p y₁ → p y₂ → y₁ = y₂ExistsUnique.unique

/- exists, forall, exists unique congruences -/

-- TODO
-- attribute [congr] forall_congr'
-- attribute [congr] exists_congr'
#align forall_congr forall_congr': ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a ↔ q a) → ((∀ (a : α), p a) ↔ ∀ (a : α), q a)forall_congr'

#align Exists.imp Exists.imp: ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∃ a, p a) → ∃ a, q aExists.imp
#align exists_imp_exists Exists.imp: ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∃ a, p a) → ∃ a, q aExists.imp

-- @[congr]
theorem exists_unique_congr: ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a ↔ q a) → ((∃! a, p a) ↔ ∃! a, q a)exists_unique_congr {p: α → Propp q: α → Propq : α: ?m.25215α → Prop: TypeProp} (h: ∀ (a : α), p a ↔ q ah : ∀ a: ?m.25227a, p: α → Propp a: ?m.25227a ↔ q: α → Propq a: ?m.25227a) : (∃! a: ?m.25235a, p: α → Propp a: ?m.25235a) ↔ ∃! a: ?m.25242a, q: α → Propq a: ?m.25242a :=
exists_congr: ∀ {α : Sort ?u.25251} {p q : α → Prop}, (∀ (a : α), p a ↔ q a) → ((∃ a, p a) ↔ ∃ a, q a)exists_congr fun _: ?m.25267_ ↦ and_congr: ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∧ b ↔ c ∧ d)and_congr (h: ∀ (a : α), p a ↔ q ah _: α_) \$ forall_congr': ∀ {α : Sort ?u.25284} {p q : α → Prop}, (∀ (a : α), p a ↔ q a) → ((∀ (a : α), p a) ↔ ∀ (a : α), q a)forall_congr' fun _: ?m.25297_ ↦ imp_congr_left: ∀ {a b c : Prop}, (a ↔ b) → (a → c ↔ b → c)imp_congr_left (h: ∀ (a : α), p a ↔ q ah _: α_)

/- decidable -/

#align decidable.to_bool Decidable.decide: (p : Prop) → [h : Decidable p] → BoolDecidable.decide

theorem decide_True': ∀ (h : Decidable True), decide True = truedecide_True' (h: Decidable Trueh : Decidable: Prop → TypeDecidable True: PropTrue) : decide: (p : Prop) → [h : Decidable p] → Booldecide True: PropTrue = true: Booltrue := byGoals accomplished! 🐙 a, b, c, d: Propp: ?m.25343h: Decidable Truedecide True = truesimpGoals accomplished! 🐙
#align to_bool_true_eq_tt decide_True': ∀ (h : Decidable True), decide True = truedecide_True'

theorem decide_False': ∀ (h : Decidable False), decide False = falsedecide_False' (h: Decidable Falseh : Decidable: Prop → TypeDecidable False: PropFalse) : decide: (p : Prop) → [h : Decidable p] → Booldecide False: PropFalse = false: Boolfalse := byGoals accomplished! 🐙 a, b, c, d: Propp: ?m.25417h: Decidable Falsedecide False = falsesimpGoals accomplished! 🐙
#align to_bool_false_eq_ff decide_False': ∀ (h : Decidable False), decide False = falsedecide_False'

namespace Decidable

def recOn_true: [h : Decidable p] → {h₁ : p → Sort u} → {h₂ : ¬p → Sort u} → (h₃ : p) → h₁ h₃ → Decidable.recOn h h₂ h₁recOn_true [h: Decidable ph : Decidable: Prop → TypeDecidable p: ?m.25511p] {h₁: p → Sort uh₁ : p: ?m.25511p → Sort u: Type uSortSort u: Type u u} {h₂: ¬p → Sort uh₂ : ¬p: ?m.25511p → Sort u: Type uSortSort u: Type u u}
(h₃: ph₃ : p: ?m.25511p) (h₄: h₁ h₃h₄ : h₁: p → Sort uh₁ h₃: ph₃) : Decidable.recOn: {p : Prop} →
{motive : Decidable p → Sort ?u.25528} →
(t : Decidable p) → ((h : ¬p) → motive (isFalse h)) → ((h : p) → motive (isTrue h)) → motive tDecidable.recOn h: Decidable ph h₂: ¬p → Sort uh₂ h₁: p → Sort uh₁ :=
cast: {α β : Sort ?u.25569} → α = β → α → βcast (byGoals accomplished! 🐙 a, b, c, d, p: Proph: Decidable ph₁: p → Sort uh₂: ¬p → Sort uh₃: ph₄: h₁ h₃h₁ h₃ = Decidable.recOn h h₂ h₁match h: Decidable ph with a, b, c, d, p: Proph: Decidable ph₁: p → Sort uh₂: ¬p → Sort uh₃: ph₄: h₁ h₃h₁ h₃ = Decidable.recOn h h₂ h₁| .isTrue: {p : Prop} → p → Decidable p.isTrue _ =>a, b, c, d, p: Proph: Decidable ph₁: p → Sort uh₂: ¬p → Sort uh₃: ph₄: h₁ h₃h✝: ph₁ h₃ = Decidable.recOn (isTrue h✝) h₂ h₁ a, b, c, d, p: Proph: Decidable ph₁: p → Sort uh₂: ¬p → Sort uh₃: ph₄: h₁ h₃h₁ h₃ = Decidable.recOn h h₂ h₁rflGoals accomplished! 🐙) h₄: h₁ h₃h₄
#align decidable.rec_on_true Decidable.recOn_true: (p : Prop) → [h : Decidable p] → {h₁ : p → Sort u} → {h₂ : ¬p → Sort u} → (h₃ : p) → h₁ h₃ → Decidable.recOn h h₂ h₁Decidable.recOn_true

def recOn_false: [h : Decidable p] → {h₁ : p → Sort u} → {h₂ : ¬p → Sort u} → (h₃ : ¬p) → h₂ h₃ → Decidable.recOn h h₂ h₁recOn_false [h: Decidable ph : Decidable: Prop → TypeDecidable p: ?m.25773p] {h₁: p → Sort uh₁ : p: ?m.25773p → Sort u: Type uSortSort u: Type u u} {h₂: ¬p → Sort uh₂ : ¬p: ?m.25773p → Sort u: Type uSortSort u: Type u u} (h₃: ¬ph₃ : ¬p: ?m.25773p) (h₄: h₂ h₃h₄ : h₂: ¬p → Sort uh₂ h₃: ¬ph₃) :
Decidable.recOn: {p : Prop} →
{motive : Decidable p → Sort ?u.25791} →
(t : Decidable p) → ((h : ¬p) → motive (isFalse h)) → ((h : p) → motive (isTrue h)) → motive tDecidable.recOn h: Decidable ph h₂: ¬p → Sort uh₂ h₁: p → Sort uh₁ :=
cast: {α β : Sort ?u.25832} → α = β → α → βcast (byGoals accomplished! 🐙 a, b, c, d, p: Proph: Decidable ph₁: p → Sort uh₂: ¬p → Sort uh₃: ¬ph₄: h₂ h₃h₂ h₃ = Decidable.recOn h h₂ h₁match h: Decidable ph with a, b, c, d, p: Proph: Decidable ph₁: p → Sort uh₂: ¬p → Sort uh₃: ¬ph₄: h₂ h₃h₂ h₃ = Decidable.recOn h h₂ h₁| .isFalse: {p : Prop} → ¬p → Decidable p.isFalse _ =>a, b, c, d, p: Proph: Decidable ph₁: p → Sort uh₂: ¬p → Sort uh₃: ¬ph₄: h₂ h₃h✝: ¬ph₂ h₃ = Decidable.recOn (isFalse h✝) h₂ h₁ a, b, c, d, p: Proph: Decidable ph₁: p → Sort uh₂: ¬p → Sort uh₃: ¬ph₄: h₂ h₃h₂ h₃ = Decidable.recOn h h₂ h₁rflGoals accomplished! 🐙) h₄: h₂ h₃h₄
#align decidable.rec_on_false Decidable.recOn_false: (p : Prop) → [h : Decidable p] → {h₁ : p → Sort u} → {h₂ : ¬p → Sort u} → (h₃ : ¬p) → h₂ h₃ → Decidable.recOn h h₂ h₁Decidable.recOn_false

alias byCases: {p : Prop} → {q : Sort u} → [dec : Decidable p] → (p → q) → (¬p → q) → qbyCases ← by_cases: {p : Prop} → {q : Sort u} → [dec : Decidable p] → (p → q) → (¬p → q) → qby_cases
alias byContradiction: ∀ {p : Prop} [dec : Decidable p], (¬p → False) → pbyContradiction ← by_contradiction: ∀ {p : Prop} [dec : Decidable p], (¬p → False) → pby_contradiction
alias not_not: ∀ {p : Prop} [inst : Decidable p], ¬¬p ↔ pnot_not ← not_not_iff: ∀ {p : Prop} [inst : Decidable p], ¬¬p ↔ pnot_not_iff

@[deprecated not_or: ∀ {p q : Prop}, ¬(p ∨ q) ↔ ¬p ∧ ¬qnot_or] theorem not_or_iff_and_not: ∀ (p q : Prop) [inst : Decidable p] [inst : Decidable q], ¬(p ∨ q) ↔ ¬p ∧ ¬qnot_or_iff_and_not (p: Propp q: ?m.26150q) [Decidable: Prop → TypeDecidable p: ?m.26147p] [Decidable: Prop → TypeDecidable q: ?m.26150q] :
¬(p: ?m.26147p ∨ q: ?m.26150q) ↔ ¬p: ?m.26147p ∧ ¬q: ?m.26150q := not_or: ∀ {p q : Prop}, ¬(p ∨ q) ↔ ¬p ∧ ¬qnot_or

end Decidable

#align decidable_of_decidable_of_iff decidable_of_decidable_of_iff: {p q : Prop} → [inst : Decidable p] → (p ↔ q) → Decidable qdecidable_of_decidable_of_iff
#align decidable_of_decidable_of_eq decidable_of_decidable_of_eq: {p q : Prop} → [inst : Decidable p] → p = q → Decidable qdecidable_of_decidable_of_eq
#align or.by_cases Or.by_cases: {p q : Prop} → [inst : Decidable p] → {α : Sort u} → p ∨ q → (p → α) → (q → α) → αOr.by_cases

alias instDecidableOr: {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∨ q)instDecidableOr ← Or.decidable: {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∨ q)Or.decidable
alias instDecidableAnd: {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)instDecidableAnd ← And.decidable: {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)And.decidable
alias instDecidableNot: {p : Prop} → [dp : Decidable p] → Decidable ¬pinstDecidableNot ← Not.decidable: {p : Prop} → [dp : Decidable p] → Decidable ¬pNot.decidable
alias instDecidableIff: {p q : Prop} → [inst : Decidable p] → [inst : Decidable q] → Decidable (p ↔ q)instDecidableIff ← Iff.decidable: {p q : Prop} → [inst : Decidable p] → [inst : Decidable q] → Decidable (p ↔ q)Iff.decidable
alias instDecidableTrue: Decidable TrueinstDecidableTrue ← decidableTrue: Decidable TruedecidableTrue
alias instDecidableFalse: Decidable FalseinstDecidableFalse ← decidableFalse: Decidable FalsedecidableFalse

#align decidable.true decidableTrue: Decidable TruedecidableTrue
#align decidable.false decidableFalse: Decidable FalsedecidableFalse
#align or.decidable Or.decidable: {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∨ q)Or.decidable
#align and.decidable And.decidable: {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)And.decidable
#align not.decidable Not.decidable: {p : Prop} → [dp : Decidable p] → Decidable ¬pNot.decidable
#align iff.decidable Iff.decidable: {p q : Prop} → [inst : Decidable p] → [inst : Decidable q] → Decidable (p ↔ q)Iff.decidable

instance: (p : Prop) → {q : Prop} → [inst : Decidable p] → [inst : Decidable q] → Decidable (Xor' p q)instance [Decidable: Prop → TypeDecidable p: ?m.26454p] [Decidable: Prop → TypeDecidable q: ?m.26460q] : Decidable: Prop → TypeDecidable (Xor': Prop → Prop → PropXor' p: ?m.26454p q: ?m.26460q) := inferInstanceAs: (α : Sort ?u.26471) → [i : α] → αinferInstanceAs (Decidable: Prop → TypeDecidable (Or: Prop → Prop → PropOr ..))

def IsDecEq: {α : Sort u} → (α → α → Bool) → PropIsDecEq {α: Sort uα : Sort u: Type uSortSort u: Type u u} (p: α → α → Boolp : α: Sort uα → α: Sort uα → Bool: TypeBool) : Prop: TypeProp := ∀ ⦃x: αx y: αy : α: Sort uα⦄, p: α → α → Boolp x: αx y: αy = true: Booltrue → x: αx = y: αy
def IsDecRefl: {α : Sort u} → (α → α → Bool) → PropIsDecRefl {α: Sort uα : Sort u: Type uSortSort u: Type u u} (p: α → α → Boolp : α: Sort uα → α: Sort uα → Bool: TypeBool) : Prop: TypeProp := ∀ x: ?m.26967x, p: α → α → Boolp x: ?m.26967x x: ?m.26967x = true: Booltrue

def decidableEq_of_bool_pred: {α : Sort u} → {p : α → α → Bool} → IsDecEq p → IsDecRefl p → DecidableEq αdecidableEq_of_bool_pred {α: Sort uα : Sort u: Type uSortSort u: Type u u} {p: α → α → Boolp : α: Sort uα → α: Sort uα → Bool: TypeBool} (h₁: IsDecEq ph₁ : IsDecEq: {α : Sort ?u.27003} → (α → α → Bool) → PropIsDecEq p: α → α → Boolp)
(h₂: IsDecRefl ph₂ : IsDecRefl: {α : Sort ?u.27013} → (α → α → Bool) → PropIsDecRefl p: α → α → Boolp) : DecidableEq: Sort ?u.27023 → Sort (max1?u.27023)DecidableEq α: Sort uα
| x: αx, y: αy =>
if hp: ?m.27088hp : p: α → α → Boolp x: αx y: αy = true: Booltrue then isTrue: {p : Prop} → p → Decidable pisTrue (h₁: IsDecEq ph₁ hp: ?m.27074hp)
else isFalse: {p : Prop} → ¬p → Decidable pisFalse (λ hxy: x = yhxy : x: αx = y: αy => absurd: ∀ {a : Prop} {b : Sort ?u.27095}, a → ¬a → babsurd (h₂: IsDecRefl ph₂ y: αy) (byGoals accomplished! 🐙 a, b, c, d: Propp✝: ?m.26992α: Sort up: α → α → Boolh₁: IsDecEq ph₂: IsDecRefl px, y: αhp: ¬p x y = truehxy: x = y¬p y y = truerwa [a, b, c, d: Propp✝: ?m.26992α: Sort up: α → α → Boolh₁: IsDecEq ph₂: IsDecRefl px, y: αhp: ¬p x y = truehxy: x = y¬p y y = truehxy: x = yhxya, b, c, d: Propp✝: ?m.26992α: Sort up: α → α → Boolh₁: IsDecEq ph₂: IsDecRefl px, y: αhp: ¬p y y = truehxy: x = y¬p y y = true]a, b, c, d: Propp✝: ?m.26992α: Sort up: α → α → Boolh₁: IsDecEq ph₂: IsDecRefl px, y: αhp: ¬p y y = truehxy: x = y¬p y y = true at hp: ¬p x y = truehpGoals accomplished! 🐙))
#align decidable_eq_of_bool_pred decidableEq_of_bool_pred: {α : Sort u} → {p : α → α → Bool} → IsDecEq p → IsDecRefl p → DecidableEq αdecidableEq_of_bool_pred

theorem decidableEq_inl_refl: ∀ {α : Sort u} [h : DecidableEq α] (a : α), h a a = isTrue (_ : a = a)decidableEq_inl_refl {α: Sort uα : Sort u: Type uSortSort u: Type u u} [h: DecidableEq αh : DecidableEq: Sort ?u.27347 → Sort (max1?u.27347)DecidableEq α: Sort uα] (a: αa : α: Sort uα) :
h: DecidableEq αh a: αa a: αa = isTrue: {p : Prop} → p → Decidable pisTrue (Eq.refl: ∀ {α : Sort ?u.27360} (a : α), a = aEq.refl a: αa) :=
match h: DecidableEq αh a: αa a: αa with
| isTrue: {p : Prop} → p → Decidable pisTrue _ => rfl: ∀ {α : Sort ?u.27387} {a : α}, a = arfl

theorem decidableEq_inr_neg: ∀ {α : Sort u} [h : DecidableEq α] {a b : α} (n : a ≠ b), h a b = isFalse ndecidableEq_inr_neg {α: Sort uα : Sort u: Type uSortSort u: Type u u} [h: DecidableEq αh : DecidableEq: Sort ?u.27472 → Sort (max1?u.27472)DecidableEq α: Sort uα] {a: αa b: αb : α: Sort uα}
(n: a ≠ bn : a: αa ≠ b: αb) : h: DecidableEq αh a: αa b: αb = isFalse: {p : Prop} → ¬p → Decidable pisFalse n: a ≠ bn :=
match h: DecidableEq αh a: αa b: αb with
| isFalse: {p : Prop} → ¬p → Decidable pisFalse _ => rfl: ∀ {α : Sort ?u.27517} {a : α}, a = arfl

#align inhabited.default Inhabited.default: {α : Sort u} → [self : Inhabited α] → αInhabited.default
#align arbitrary Inhabited.default: {α : Sort u} → [self : Inhabited α] → αInhabited.default
#align nonempty_of_inhabited instNonempty: ∀ {α : Sort u} [inst : Inhabited α], Nonempty αinstNonempty

/- subsingleton -/

theorem rec_subsingleton: ∀ {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)]
[h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)], Subsingleton (Decidable.recOn h h₂ h₁)rec_subsingleton {p: Propp : Prop: TypeProp} [h: Decidable ph : Decidable: Prop → TypeDecidable p: Propp] {h₁: p → Sort uh₁ : p: Propp → Sort u: Type uSortSort u: Type u u} {h₂: ¬p → Sort uh₂ : ¬p: Propp → Sort u: Type uSortSort u: Type u u}
[h₃: ∀ (h : p), Subsingleton (h₁ h)h₃ : ∀ h: ph : p: Propp, Subsingleton: Sort ?u.27734 → PropSubsingleton (h₁: p → Sort uh₁ h: ph)] [h₄: ∀ (h : ¬p), Subsingleton (h₂ h)h₄ : ∀ h: ¬ph : ¬p: Propp, Subsingleton: Sort ?u.27741 → PropSubsingleton (h₂: ¬p → Sort uh₂ h: ¬ph)] :
Subsingleton: Sort ?u.27746 → PropSubsingleton (Decidable.recOn: {p : Prop} →
{motive : Decidable p → Sort ?u.27747} →
(t : Decidable p) → ((h : ¬p) → motive (isFalse h)) → ((h : p) → motive (isTrue h)) → motive tDecidable.recOn h: Decidable ph h₂: ¬p → Sort uh₂ h₁: p → Sort uh₁) :=
match h: Decidable ph with
| isTrue: {p : Prop} → p → Decidable pisTrue h: ph => h₃: ∀ (h : p), Subsingleton (h₁ h)h₃ h: ph
| isFalse: {p : Prop} → ¬p → Decidable pisFalse h: ¬ph => h₄: ∀ (h : ¬p), Subsingleton (h₂ h)h₄ h: ¬ph

@[deprecated ite_self: ∀ {α : Sort u} {c : Prop} {d : Decidable c} (a : α), (if c then a else a) = aite_self]
theorem if_t_t: ∀ (c : Prop) [inst : Decidable c] {α : Sort u} (t : α), (if c then t else t) = tif_t_t (c: Propc : Prop: TypeProp) [Decidable: Prop → TypeDecidable c: Propc] {α: Sort uα : Sort u: Type uSortSort u: Type u u} (t: αt : α: Sort uα) : ite: {α : Sort ?u.27913} → (c : Prop) → [h : Decidable c] → α → α → αite c: Propc t: αt t: αt = t: αt := ite_self: ∀ {α : Sort ?u.27923} {c : Prop} {d : Decidable c} (a : α), (if c then a else a) = aite_self _: ?m.27924_

theorem imp_of_if_pos: ∀ {c t e : Prop} [inst : Decidable c], (if c then t else e) → c → timp_of_if_pos {c: Propc t: Propt e: Prope : Prop: TypeProp} [Decidable: Prop → TypeDecidable c: Propc] (h: if c then t else eh : ite: {α : Sort ?u.27961} → (c : Prop) → [h : Decidable c] → α → α → αite c: Propc t: Propt e: Prope) (hc: chc : c: Propc) : t: Propt :=
byGoals accomplished! 🐙 a, b, c✝, d: Propp: ?m.27950c, t, e: Propinst✝: Decidable ch: if c then t else ehc: cthave := if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.27984} {t e : α}, (if c then t else e) = tif_pos hc: chc ▸ h: if c then t else eha, b, c✝, d: Propp: ?m.27950c, t, e: Propinst✝: Decidable ch: if c then t else ehc: cthis: tt;a, b, c✝, d: Propp: ?m.27950c, t, e: Propinst✝: Decidable ch: if c then t else ehc: cthis: tt a, b, c✝, d: Propp: ?m.27950c, t, e: Propinst✝: Decidable ch: if c then t else ehc: ctexact this: ?m.27979thisGoals accomplished! 🐙
#align implies_of_if_pos imp_of_if_pos: ∀ {c t e : Prop} [inst : Decidable c], (if c then t else e) → c → timp_of_if_pos

theorem imp_of_if_neg: ∀ {c t e : Prop} [inst : Decidable c], (if c then t else e) → ¬c → eimp_of_if_neg {c: Propc t: Propt e: Prope : Prop: TypeProp} [Decidable: Prop → TypeDecidable c: Propc] (h: if c then t else eh : ite: {α : Sort ?u.28032} → (c : Prop) → [h : Decidable c] → α → α → αite c: Propc t: Propt e: Prope) (hnc: ¬chnc : ¬c: Propc) : e: Prope :=
byGoals accomplished! 🐙 a, b, c✝, d: Propp: ?m.28021c, t, e: Propinst✝: Decidable ch: if c then t else ehnc: ¬cehave := if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.28055} {t e : α}, (if c then t else e) = eif_neg hnc: ¬chnc ▸ h: if c then t else eha, b, c✝, d: Propp: ?m.28021c, t, e: Propinst✝: Decidable ch: if c then t else ehnc: ¬cthis: ee;a, b, c✝, d: Propp: ?m.28021c, t, e: Propinst✝: Decidable ch: if c then t else ehnc: ¬cthis: ee a, b, c✝, d: Propp: ?m.28021c, t, e: Propinst✝: Decidable ch: if c then t else ehnc: ¬ceexact this: ?m.28050thisGoals accomplished! 🐙
#align implies_of_if_neg imp_of_if_neg: ∀ {c t e : Prop} [inst : Decidable c], (if c then t else e) → ¬c → eimp_of_if_neg

theorem if_ctx_congr: ∀ {α : Sort u} {b c : Prop} [dec_b : Decidable b] [dec_c : Decidable c] {x y u v : α},
(b ↔ c) → (c → x = u) → (¬c → y = v) → (if b then x else y) = if c then u else vif_ctx_congr {α: Sort uα : Sort u: Type uSortSort u: Type u u} {b: Propb c: Propc : Prop: TypeProp} [dec_b: Decidable bdec_b : Decidable: Prop → TypeDecidable b: Propb] [dec_c: Decidable cdec_c : Decidable: Prop → TypeDecidable c: Propc]
{x: αx y: αy u: αu v: αv : α: Sort uα} (h_c: b ↔ ch_c : b: Propb ↔ c: Propc) (h_t: c → x = uh_t : c: Propc → x: αx = u: αu) (h_e: ¬c → y = vh_e : ¬c: Propc → y: αy = v: αv) : ite: {α : Sort ?u.28130} → (c : Prop) → [h : Decidable c] → α → α → αite b: Propb x: αx y: αy = ite: {α : Sort ?u.28135} → (c : Prop) → [h : Decidable c] → α → α → αite c: Propc u: αu v: αv :=
match dec_b: Decidable bdec_b, dec_c: Decidable cdec_c with
| isFalse: {p : Prop} → ¬p → Decidable pisFalse _,  isFalse: {p : Prop} → ¬p → Decidable pisFalse h₂: ¬ch₂ => h_e: ¬c → y = vh_e h₂: ¬ch₂
| isTrue: {p : Prop} → p → Decidable pisTrue _,   isTrue: {p : Prop} → p → Decidable pisTrue h₂: ch₂  => h_t: c → x = uh_t h₂: ch₂
| isFalse: {p : Prop} → ¬p → Decidable pisFalse h₁: ¬bh₁, isTrue: {p : Prop} → p → Decidable pisTrue h₂: ch₂  => absurd: ∀ {a : Prop} {b : Sort ?u.28232}, a → ¬a → babsurd h₂: ch₂ (Iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → bIff.mp (not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)not_congr h_c: b ↔ ch_c) h₁: ¬bh₁)
| isTrue: {p : Prop} → p → Decidable pisTrue h₁: bh₁,  isFalse: {p : Prop} → ¬p → Decidable pisFalse h₂: ¬ch₂ => absurd: ∀ {a : Prop} {b : Sort ?u.28267}, a → ¬a → babsurd h₁: bh₁ (Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → aIff.mpr (not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)not_congr h_c: b ↔ ch_c) h₂: ¬ch₂)

theorem if_congr: ∀ {α : Sort u} {b c : Prop} [inst : Decidable b] [inst_1 : Decidable c] {x y u v : α},
(b ↔ c) → x = u → y = v → (if b then x else y) = if c then u else vif_congr {α: Sort uα : Sort u: Type uSortSort u: Type u u} {b: Propb c: Propc : Prop: TypeProp} [Decidable: Prop → TypeDecidable b: Propb] [Decidable: Prop → TypeDecidable c: Propc]
{x: αx y: αy u: αu v: αv : α: Sort uα} (h_c: b ↔ ch_c : b: Propb ↔ c: Propc) (h_t: x = uh_t : x: αx = u: αu) (h_e: y = vh_e : y: αy = v: αv) : ite: {α : Sort ?u.28509} → (c : Prop) → [h : Decidable c] → α → α → αite b: Propb x: αx y: αy = ite: {α : Sort ?u.28514} → (c : Prop) → [h : Decidable c] → α → α → αite c: Propc u: αu v: αv :=
if_ctx_congr: ∀ {α : Sort ?u.28532} {b c : Prop} [dec_b : Decidable b] [dec_c : Decidable c] {x y u v : α},
(b ↔ c) → (c → x = u) → (¬c → y = v) → (if b then x else y) = if c then u else vif_ctx_congr h_c: b ↔ ch_c (λ _: ?m.28618_ => h_t: x = uh_t) (λ _: ?m.28623_ => h_e: y = vh_e)

theorem if_ctx_congr_prop: ∀ {b c x y u v : Prop} [dec_b : Decidable b] [dec_c : Decidable c],
(b ↔ c) → (c → (x ↔ u)) → (¬c → (y ↔ v)) → ((if b then x else y) ↔ if c then u else v)if_ctx_congr_prop {b: Propb c: Propc x: Propx y: Propy u: Propu v: Propv : Prop: TypeProp} [dec_b: Decidable bdec_b : Decidable: Prop → TypeDecidable b: Propb] [dec_c: Decidable cdec_c : Decidable: Prop → TypeDecidable c: Propc]
(h_c: b ↔ ch_c : b: Propb ↔ c: Propc) (h_t: c → (x ↔ u)h_t : c: Propc → (x: Propx ↔ u: Propu)) (h_e: ¬c → (y ↔ v)h_e : ¬c: Propc → (y: Propy ↔ v: Propv)) : ite: {α : Sort ?u.28682} → (c : Prop) → [h : Decidable c] → α → α → αite b: Propb x: Propx y: Propy ↔ ite: {α : Sort ?u.28687} → (c : Prop) → [h : Decidable c] → α → α → αite c: Propc u: Propu v: Propv :=
match dec_b: Decidable bdec_b, dec_c: Decidable cdec_c with
| isFalse: {p : Prop} → ¬p → Decidable pisFalse _,  isFalse: {p : Prop} → ¬p → Decidable pisFalse h₂: ¬ch₂ => h_e: ¬c → (y ↔ v)h_e h₂: ¬ch₂
| isTrue: {p : Prop} → p → Decidable pisTrue _,   isTrue: {p : Prop} → p → Decidable pisTrue h₂: ch₂  => h_t: c → (x ↔ u)h_t h₂: ch₂
| isFalse: {p : Prop} → ¬p → Decidable pisFalse h₁: ¬bh₁, isTrue: {p : Prop} → p → Decidable pisTrue h₂: ch₂  => absurd: ∀ {a : Prop} {b : Sort ?u.28781}, a → ¬a → babsurd h₂: ch₂ (Iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → bIff.mp (not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)not_congr h_c: b ↔ ch_c) h₁: ¬bh₁)
| isTrue: {p : Prop} → p → Decidable pisTrue h₁: bh₁,  isFalse: {p : Prop} → ¬p → Decidable pisFalse h₂: ¬ch₂ => absurd: ∀ {a : Prop} {b : Sort ?u.28814}, a → ¬a → babsurd h₁: bh₁ (Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → aIff.mpr (not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)not_congr h_c: b ↔ ch_c) h₂: ¬ch₂)

-- @[congr]
theorem if_congr_prop: ∀ {b c x y u v : Prop} [inst : Decidable b] [inst_1 : Decidable c],
(b ↔ c) → (x ↔ u) → (y ↔ v) → ((if b then x else y) ↔ if c then u else v)if_congr_prop {b: Propb c: Propc x: Propx y: Propy u: Propu v: Propv : Prop: TypeProp} [Decidable: Prop → TypeDecidable b: Propb] [Decidable: Prop → TypeDecidable c: Propc] (h_c: b ↔ ch_c : b: Propb ↔ c: Propc) (h_t: x ↔ uh_t : x: Propx ↔ u: Propu)
(h_e: y ↔ vh_e : y: Propy ↔ v: Propv) : ite: {α : Sort ?u.29029} → (c : Prop) → [h : Decidable c] → α → α → αite b: Propb x: Propx y: Propy ↔ ite: {α : Sort ?u.29034} → (c : Prop) → [h : Decidable c] → α → α → αite c: Propc u: Propu v: Propv :=
if_ctx_congr_prop: ∀ {b c x y u v : Prop} [dec_b : Decidable b] [dec_c : Decidable c],
(b ↔ c) → (c → (x ↔ u)) → (¬c → (y ↔ v)) → ((if b then x else y) ↔ if c then u else v)if_ctx_congr_prop h_c: b ↔ ch_c (λ _: ?m.29131_ => h_t: x ↔ uh_t) (λ _: ?m.29136_ => h_e: y ↔ vh_e)

theorem if_ctx_simp_congr_prop: ∀ {b c x y u v : Prop} [inst : Decidable b] (h_c : b ↔ c),
(c → (x ↔ u)) → (¬c → (y ↔ v)) → ((if b then x else y) ↔ if c then u else v)if_ctx_simp_congr_prop {b: Propb c: Propc x: Propx y: Propy u: Propu v: Propv : Prop: TypeProp} [Decidable: Prop → TypeDecidable b: Propb] (h_c: b ↔ ch_c : b: Propb ↔ c: Propc) (h_t: c → (x ↔ u)h_t : c: Propc → (x: Propx ↔ u: Propu))
-- FIXME: after https://github.com/leanprover/lean4/issues/1867 is fixed,
-- this should be changed back to:
-- (h_e : ¬c → (y ↔ v)) : ite b x y ↔ ite c (h := decidable_of_decidable_of_iff h_c) u v :=
(h_e: ¬c → (y ↔ v)h_e : ¬c: Propc → (y: Propy ↔ v: Propv)) : ite: {α : Sort ?u.29192} → (c : Prop) → [h : Decidable c] → α → α → αite b: Propb x: Propx y: Propy ↔ @ite: {α : Sort ?u.29196} → (c : Prop) → [h : Decidable c] → α → α → αite _: Sort ?u.29196_ c: Propc (decidable_of_decidable_of_iff: {p q : Prop} → [inst : Decidable p] → (p ↔ q) → Decidable qdecidable_of_decidable_of_iff h_c: b ↔ ch_c) u: Propu v: Propv :=
if_ctx_congr_prop: ∀ {b c x y u v : Prop} [dec_b : Decidable b] [dec_c : Decidable c],
(b ↔ c) → (c → (x ↔ u)) → (¬c → (y ↔ v)) → ((if b then x else y) ↔ if c then u else v)if_ctx_congr_prop (dec_c := decidable_of_decidable_of_iff: {p q : Prop} → [inst : Decidable p] → (p ↔ q) → Decidable qdecidable_of_decidable_of_iff h_c: b ↔ ch_c) h_c: b ↔ ch_c h_t: c → (x ↔ u)h_t h_e: ¬c → (y ↔ v)h_e

theorem if_simp_congr_prop: ∀ {b c x y u v : Prop} [inst : Decidable b] (h_c : b ↔ c),
(x ↔ u) → (y ↔ v) → ((if b then x else y) ↔ if c then u else v)if_simp_congr_prop {b: Propb c: Propc x: Propx y: Propy u: Propu v: Propv : Prop: TypeProp} [Decidable: Prop → TypeDecidable b: Propb] (h_c: b ↔ ch_c : b: Propb ↔ c: Propc) (h_t: x ↔ uh_t : x: Propx ↔ u: Propu)
-- FIXME: after https://github.com/leanprover/lean4/issues/1867 is fixed,
-- this should be changed back to:
-- (h_e : y ↔ v) : ite b x y ↔ (ite c (h := decidable_of_decidable_of_iff h_c) u v) :=
(h_e: y ↔ vh_e : y: Propy ↔ v: Propv) : ite: {α : Sort ?u.29379} → (c : Prop) → [h : Decidable c] → α → α → αite b: Propb x: Propx y: Propy ↔ (@ite: {α : Sort ?u.29383} → (c : Prop) → [h : Decidable c] → α → α → αite _: Sort ?u.29383_ c: Propc (decidable_of_decidable_of_iff: {p q : Prop} → [inst : Decidable p] → (p ↔ q) → Decidable qdecidable_of_decidable_of_iff h_c: b ↔ ch_c) u: Propu v: Propv) :=
if_ctx_simp_congr_prop: ∀ {b c x y u v : Prop} [inst : Decidable b] (h_c : b ↔ c),
(c → (x ↔ u)) → (¬c → (y ↔ v)) → ((if b then x else y) ↔ if c then u else v)if_ctx_simp_congr_prop h_c: b ↔ ch_c (λ _: ?m.29449_ => h_t: x ↔ uh_t) (λ _: ?m.29454_ => h_e: y ↔ vh_e)

-- @[congr]
theorem dif_ctx_congr: ∀ {α : Sort u} {b c : Prop} [dec_b : Decidable b] [dec_c : Decidable c] {x : b → α} {u : c → α} {y : ¬b → α}
{v : ¬c → α} (h_c : b ↔ c), (∀ (h : c), x (_ : b) = u h) → (∀ (h : ¬c), y (_ : ¬b) = v h) → dite b x y = dite c u vdif_ctx_congr {α: Sort uα : Sort u: Type uSortSort u: Type u u} {b: Propb c: Propc : Prop: TypeProp} [dec_b: Decidable bdec_b : Decidable: Prop → TypeDecidable b: Propb] [dec_c: Decidable cdec_c : Decidable: Prop → TypeDecidable c: Propc]
{x: b → αx : b: Propb → α: Sort uα} {u: c → αu : c: Propc → α: Sort uα} {y: ¬b → αy : ¬b: Propb → α: Sort uα} {v: ¬c → αv : ¬c: Propc → α: Sort uα}
(h_c: b ↔ ch_c : b: Propb ↔ c: Propc) (h_t: ∀ (h : c), x (_ : b) = u hh_t : ∀ h: ch : c: Propc, x: b → αx (Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → aIff.mpr h_c: b ↔ ch_c h: ch) = u: c → αu h: ch)
(h_e: ∀ (h : ¬c), y (_ : ¬b) = v hh_e : ∀ h: ¬ch : ¬c: Propc, y: ¬b → αy (Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → aIff.mpr (not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)not_congr h_c: b ↔ ch_c) h: ¬ch) = v: ¬c → αv h: ¬ch) :
@dite: {α : Sort ?u.29538} → (c : Prop) → [h : Decidable c] → (c → α) → (¬c → α) → αdite α: Sort uα b: Propb dec_b: Decidable bdec_b x: b → αx y: ¬b → αy = @dite: {α : Sort ?u.29541} → (c : Prop) → [h : Decidable c] → (c → α) → (¬c → α) → αdite α: Sort uα c: Propc dec_c: Decidable cdec_c u: c → αu v: ¬c → αv :=
match dec_b: Decidable bdec_b, dec_c: Decidable cdec_c with
| isFalse: {p : Prop} → ¬p → Decidable pisFalse _, isFalse: {p : Prop} → ¬p → Decidable pisFalse h₂: ¬ch₂ => h_e: ∀ (h : ¬c), y (_ : ¬b) = v hh_e h₂: ¬ch₂
| isTrue: {p : Prop} → p → Decidable pisTrue _, isTrue: {p : Prop} → p → Decidable pisTrue h₂: ch₂ => h_t: ∀ (h : c), x (_ : b) = u hh_t h₂: ch₂
| isFalse: {p : Prop} → ¬p → Decidable pisFalse h₁: ¬bh₁, isTrue: {p : Prop} → p → Decidable pisTrue h₂: ch₂ => absurd: ∀ {a : Prop} {b : Sort ?u.29639}, a → ¬a → babsurd h₂: ch₂ (Iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → bIff.mp (not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)not_congr h_c: b ↔ ch_c) h₁: ¬bh₁)
| isTrue: {p : Prop} → p → Decidable pisTrue h₁: bh₁, isFalse: {p : Prop} → ¬p → Decidable pisFalse h₂: ¬ch₂ => absurd: ∀ {a : Prop} {b : Sort ?u.29672}, a → ¬a → babsurd h₁: bh₁ (Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → aIff.mpr (not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)not_congr h_c: b ↔ ch_c) h₂: ¬ch₂)

theorem dif_ctx_simp_congr: ∀ {α : Sort u} {b c : Prop} [inst : Decidable b] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h_c : b ↔ c),
(∀ (h : c), x (_ : b) = u h) → (∀ (h : ¬c), y (_ : ¬b) = v h) → dite b x y = dite c u vdif_ctx_simp_congr {α: Sort uα : Sort u: Type uSortSort u: Type u u} {b: Propb c: Propc : Prop: TypeProp} [Decidable: Prop → TypeDecidable b: Propb]
{x: b → αx : b: Propb → α: Sort uα} {u: c → αu : c: Propc → α: Sort uα} {y: ¬b → αy : ¬b: Propb → α: Sort uα} {v: ¬c → αv : ¬c: Propc → α: Sort uα}
(h_c: b ↔ ch_c : b: Propb ↔ c: Propc) (h_t: ∀ (h : c), x (_ : b) = u hh_t : ∀ h: ch : c: Propc, x: b → αx (Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → aIff.mpr h_c: b ↔ ch_c h: ch) = u: c → αu h: ch)
(h_e: ∀ (h : ¬c), y (_ : ¬b) = v hh_e : ∀ h: ¬ch : ¬c: Propc, y: ¬b → αy (Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → aIff.mpr (not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)not_congr h_c: b ↔ ch_c) h: ¬ch) = v: ¬c → αv h: ¬ch) :
-- FIXME: after https://github.com/leanprover/lean4/issues/1867 is fixed,
-- this should be changed back to:
-- dite b x y = dite c (h := decidable_of_decidable_of_iff h_c) u v :=
dite: {α : Sort ?u.29923} → (c : Prop) → [h : Decidable c] → (c → α) → (¬c → α) → αdite b: Propb x: b → αx y: ¬b → αy = @dite: {α : Sort ?u.29933} → (c : Prop) → [h : Decidable c] → (c → α) → (¬c → α) → αdite _: Sort ?u.29933_ c: Propc (decidable_of_decidable_of_iff: {p q : Prop} → [inst : Decidable p] → (p ↔ q) → Decidable qdecidable_of_decidable_of_iff h_c: b ↔ ch_c) u: c → αu v: ¬c → αv :=
dif_ctx_congr: ∀ {α : Sort ?u.29991} {b c : Prop} [dec_b : Decidable b] [dec_c : Decidable c] {x : b → α} {u : c → α} {y : ¬b → α}
{v : ¬c → α} (h_c : b ↔ c), (∀ (h : c), x (_ : b) = u h) → (∀ (h : ¬c), y (_ : ¬b) = v h) → dite b x y = dite c u vdif_ctx_congr (dec_c := decidable_of_decidable_of_iff: {p q : Prop} → [inst : Decidable p] → (p ↔ q) → Decidable qdecidable_of_decidable_of_iff h_c: b ↔ ch_c) h_c: b ↔ ch_c h_t: ∀ (h : c), x (_ : b) = u hh_t h_e: ∀ (h : ¬c), y (_ : ¬b) = v hh_e

def AsTrue: (c : Prop) → [inst : Decidable c] → PropAsTrue (c: Propc : Prop: TypeProp) [Decidable: Prop → TypeDecidable c: Propc] : Prop: TypeProp := if c: Propc then True: PropTrue else False: PropFalse

def AsFalse: (c : Prop) → [inst : Decidable c] → PropAsFalse (c: Propc : Prop: TypeProp) [Decidable: Prop → TypeDecidable c: Propc] : Prop: TypeProp := if c: Propc then False: PropFalse else True: PropTrue

theorem AsTrue.get: ∀ {c : Prop} [h₁ : Decidable c], AsTrue c → cAsTrue.get {c: Propc : Prop: TypeProp} [h₁: Decidable ch₁ : Decidable: Prop → TypeDecidable c: Propc] (_: AsTrue c_ : AsTrue: (c : Prop) → [inst : Decidable c] → PropAsTrue c: Propc) : c: Propc :=
match h₁: Decidable ch₁ with
| isTrue: {p : Prop} → p → Decidable pisTrue h_c: ch_c => h_c: ch_c
#align of_as_true AsTrue.get: ∀ {c : Prop} [h₁ : Decidable c], AsTrue c → cAsTrue.get

#align ulift ULift: Type s → Type (maxsr)ULift
#align ulift.up ULift.up: {α : Type s} → α → ULift αULift.up
#align ulift.down ULift.down: {α : Type s} → ULift α → αULift.down
#align plift PLift: Sort u → Type uPLift
#align plift.up PLift.up: {α : Sort u} → α → PLift αPLift.up
#align plift.down PLift.down: {α : Sort u} → PLift α → αPLift.down

/- Equalities for rewriting let-expressions -/
theorem let_value_eq: ∀ {α : Sort u} {β : Sort v} {a₁ a₂ : α} (b : α → β),
a₁ = a₂ →
(let x := a₁;
b x) =       let x := a₂;
b xlet_value_eq {α: Sort uα : Sort u: Type uSortSort u: Type u u} {β: Sort vβ : Sort v: Type vSortSort v: Type v v} {a₁: αa₁ a₂: αa₂ : α: Sort uα} (b: α → βb : α: Sort uα → β: Sort vβ)
(h: a₁ = a₂h : a₁: αa₁ = a₂: αa₂) : (let x: αx : α: Sort uα := a₁: αa₁; b: α → βb x: αx) = (let x: αx : α: Sort uα := a₂: αa₂; b: α → βb x: αx) := congrArg: ∀ {α : Sort ?u.30363} {β : Sort ?u.30362} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂congrArg b: α → βb h: a₁ = a₂h

theorem let_value_heq: ∀ {α : Sort v} {β : α → Sort u} {a₁ a₂ : α} (b : (x : α) → β x),
a₁ = a₂ →
HEq
(let x := a₁;
b x)
(let x := a₂;
b x)let_value_heq {α: Sort vα : Sort v: Type vSortSort v: Type v v} {β: α → Sort uβ : α: Sort vα → Sort u: Type uSortSort u: Type u u} {a₁: αa₁ a₂: αa₂ : α: Sort vα} (b: (x : α) → β xb : ∀ x: αx : α: Sort vα, β: α → Sort uβ x: αx)
(h: a₁ = a₂h : a₁: αa₁ = a₂: αa₂) : HEq: {α : Sort ?u.30416} → α → {β : Sort ?u.30416} → β → PropHEq (let x: αx : α: Sort vα := a₁: αa₁; b: (x : α) → β xb x: αx) (let x: αx : α: Sort vα := a₂: αa₂; b: (x : α) → β xb x: αx) := byGoals accomplished! 🐙 a, b✝, c, d: Propp: ?m.30394α: Sort vβ: α → Sort ua₁, a₂: αb: (x : α) → β xh: a₁ = a₂HEq
(let x := a₁;
b x)
(let x := a₂;
b x)cases h: a₁ = a₂ha, b✝, c, d: Propp: ?m.30394α: Sort vβ: α → Sort ua₁: αb: (x : α) → β xreflHEq
(let x := a₁;
b x)
(let x := a₁;
b x);a, b✝, c, d: Propp: ?m.30394α: Sort vβ: α → Sort ua₁: αb: (x : α) → β xreflHEq
(let x := a₁;
b x)
(let x := a₁;
b x) a, b✝, c, d: Propp: ?m.30394α: Sort vβ: α → Sort ua₁, a₂: αb: (x : α) → β xh: a₁ = a₂HEq
(let x := a₁;
b x)
(let x := a₂;
b x)rflGoals accomplished! 🐙
#align let_value_heq let_value_heq: ∀ {α : Sort v} {β : α → Sort u} {a₁ a₂ : α} (b : (x : α) → β x),
a₁ = a₂ →
HEq
(let x := a₁;
b x)
(let x := a₂;
b x)let_value_heq -- FIXME: mathport thinks this is a dubious translation

theorem let_body_eq: ∀ {α : Sort v} {β : α → Sort u} (a : α) {b₁ b₂ : (x : α) → β x},
(∀ (x : α), b₁ x = b₂ x) →
(let x := a;
b₁ x) =       let x := a;
b₂ xlet_body_eq {α: Sort vα : Sort v: Type vSortSort v: Type v v} {β: α → Sort uβ : α: Sort vα → Sort u: Type uSortSort u: Type u u} (a: αa : α: Sort vα) {b₁: (x : α) → β xb₁ b₂: (x : α) → β xb₂ : ∀ x: αx : α: Sort vα, β: α → Sort uβ x: αx}
(h: ∀ (x : α), b₁ x = b₂ xh : ∀ x: ?m.30572x, b₁: (x : α) → β xb₁ x: ?m.30572x = b₂: (x : α) → β xb₂ x: ?m.30572x) : (let x: αx : α: Sort vα := a: αa; b₁: (x : α) → β xb₁ x: αx) = (let x: αx : α: Sort vα := a: αa; b₂: (x : α) → β xb₂ x: αx) := byGoals accomplished! 🐙 a✝, b, c, d: Propp: ?m.30550α: Sort vβ: α → Sort ua: αb₁, b₂: (x : α) → β xh: ∀ (x : α), b₁ x = b₂ x(let x := a;
b₁ x) =   let x := a;
b₂ xexact h: ∀ (x : α), b₁ x = b₂ xh _: α_ ▸ rfl: ∀ {α : Sort ?u.30599} {a : α}, a = arflGoals accomplished! 🐙
#align let_value_eq let_value_eq: ∀ {α : Sort u} {β : Sort v} {a₁ a₂ : α} (b : α → β),
a₁ = a₂ →
(let x := a₁;
b x) =       let x := a₂;
b xlet_value_eq -- FIXME: mathport thinks this is a dubious translation

theorem let_eq: ∀ {α : Sort v} {β : Sort u} {a₁ a₂ : α} {b₁ b₂ : α → β},
a₁ = a₂ →
(∀ (x : α), b₁ x = b₂ x) →
(let x := a₁;
b₁ x) =         let x := a₂;
b₂ xlet_eq {α: Sort vα : Sort v: Type vSortSort v: Type v v} {β: Sort uβ : Sort u: Type uSortSort u: Type u u} {a₁: αa₁ a₂: αa₂ : α: Sort vα} {b₁: α → βb₁ b₂: α → βb₂ : α: Sort vα → β: Sort uβ}
(h₁: a₁ = a₂h₁ : a₁: αa₁ = a₂: αa₂) (h₂: ∀ (x : α), b₁ x = b₂ xh₂ : ∀ x: ?m.30661x, b₁: α → βb₁ x: ?m.30661x = b₂: α → βb₂ x: ?m.30661x) :
(let x: αx : α: Sort vα := a₁: αa₁; b₁: α → βb₁ x: αx) = (let x: αx : α: Sort vα := a₂: αa₂; b₂: α → βb₂ x: αx) := byGoals accomplished! 🐙 a, b, c, d: Propp: ?m.30637α: Sort vβ: Sort ua₁, a₂: αb₁, b₂: α → βh₁: a₁ = a₂h₂: ∀ (x : α), b₁ x = b₂ x(let x := a₁;
b₁ x) =   let x := a₂;
b₂ xsimp [h₁: a₁ = a₂h₁, h₂: ∀ (x : α), b₁ x = b₂ xh₂]Goals accomplished! 🐙
#align let_eq let_eq: ∀ {α : Sort v} {β : Sort u} {a₁ a₂ : α} {b₁ b₂ : α → β},
a₁ = a₂ →
(∀ (x : α), b₁ x = b₂ x) →
(let x := a₁;
b₁ x) =         let x := a₂;
b₂ xlet_eq -- FIXME: mathport thinks this is a dubious translation

section Relation

variable {α: Sort uα : Sort u: Type uSortSort u: Type u u} {β: Sort vβ : Sort v: Type vSortSort v: Type v v} (r: β → β → Propr : β: Sort vβ → β: Sort vβ → Prop: TypeProp)

/-- Local notation for an arbitrary binary relation `r`. -/
local infix:50 " ≺ " => r

/-- A reflexive relation relates every element to itself. -/
def Reflexive: ?m.32893Reflexive := ∀ x: ?m.32896x, x: ?m.32896x ≺ x: ?m.32896x

/-- A relation is symmetric if `x ≺ y` implies `y ≺ x`. -/
def Symmetric: ?m.32932Symmetric := ∀ ⦃x: ?m.32935x y: ?m.32938y⦄, x: ?m.32935x ≺ y: ?m.32938y → y: ?m.32938y ≺ x: ?m.32935x

/-- A relation is transitive if `x ≺ y` and `y ≺ z` together imply `x ≺ z`. -/
def Transitive: ?m.32982Transitive := ∀ ⦃x: ?m.32985x y: ?m.32988y z: ?m.32991z⦄, x: ?m.32985x ≺ y: ?m.32988y → y: ?m.32988y ≺ z: ?m.32991z → x: ?m.32985x ≺ z: ?m.32991z

lemma Equivalence.reflexive: ∀ {r : β → β → Prop}, Equivalence r → Reflexive rEquivalence.reflexive {r: β → β → Propr : β: Sort vβ → β: Sort vβ → Prop: TypeProp} (h: Equivalence rh : Equivalence: {α : Sort ?u.33049} → (α → α → Prop) → PropEquivalence r: β → β → Propr) : Reflexive: {β : Sort ?u.33059} → (β → β → Prop) → PropReflexive r: β → β → Propr := h: Equivalence rh.refl: ∀ {α : Sort ?u.33072} {r : α → α → Prop}, Equivalence r → ∀ (x : α), r x xrefl

lemma Equivalence.symmetric: ∀ {β : Sort v} {r : β → β → Prop}, Equivalence r → Symmetric rEquivalence.symmetric {r: β → β → Propr : β: Sort vβ → β: Sort vβ → Prop: TypeProp} (h: Equivalence rh : Equivalence: {α : Sort ?u.33115} → (α → α → Prop) → PropEquivalence r: β → β → Propr) : Symmetric: {β : Sort ?u.33125} → (β → β → Prop) → PropSymmetric r: β → β → Propr := λ _: ?m.33139_ _: ?m.33142_ => h: Equivalence rh.symm: ∀ {α : Sort ?u.33144} {r : α → α → Prop}, Equivalence r → ∀ {x y : α}, r x y → r y xsymm

lemma Equivalence.transitive: ∀ {r : β → β → Prop}, Equivalence r → Transitive rEquivalence.transitive  {r: β → β → Propr : β: Sort vβ → β: Sort vβ → Prop: TypeProp}(h: Equivalence rh : Equivalence: {α : Sort ?u.33197} → (α → α → Prop) → PropEquivalence r: β → β → Propr) : Transitive: {β : Sort ?u.33207} → (β → β → Prop) → PropTransitive r: β → β → Propr :=
λ _: ?m.33221_ _: ?m.33224_ _: ?m.33227_ => h: Equivalence rh.trans: ∀ {α : Sort ?u.33229} {r : α → α → Prop}, Equivalence r → ∀ {x y z : α}, r x y → r y z → r x ztrans

/-- A relation is total if for all `x` and `y`, either `x ≺ y` or `y ≺ x`. -/
def Total: ?m.33282Total := ∀ x: ?m.33285x y: ?m.33288y, x: ?m.33285x ≺ y: ?m.33288y ∨ y: ?m.33288y ≺ x: ?m.33285x

#align mk_equivalence Equivalence.mk: ∀ {α : Sort u} {r : α → α → Prop},
(∀ (x : α), r x x) → (∀ {x y : α}, r x y → r y x) → (∀ {x y z : α}, r x y → r y z → r x z) → Equivalence rEquivalence.mk

/-- Irreflexive means "not reflexive". -/
def Irreflexive: {β : Sort v} → (β → β → Prop) → PropIrreflexive := ∀ x: ?m.33330x, ¬ x: ?m.33330x ≺ x: ?m.33330x

/-- A relation is antisymmetric if `x ≺ y` and `y ≺ x` together imply that `x = y`. -/
def AntiSymmetric: ?m.33366AntiSymmetric := ∀ ⦃x: ?m.33369x y: ?m.33372y⦄, x: ?m.33369x ≺ y: ?m.33372y → y: ?m.33372y```