/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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 → Prop
Implies (
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop) := 
a: Prop
a → 
b: Prop
b

/-- 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 → r
Implies.trans {
p: Prop
p 
q: Prop
q 
r: Prop
r : 
Prop: Type
Prop} (
h₁: p → q
h₁ : 
p: Prop
p → 
q: Prop
q) (
h₂: q → r
h₂ : 
q: Prop
q → 
r: Prop
r) :
    
p: Prop
p → 
r: Prop
r := fun 
hp: ?m.48
hp ↦ 
h₂: q → r
h₂ (
h₁: p → q
h₁ 
hp: ?m.48
hp)

/- Not -/

@[deprecated] def 
NonContradictory: Prop → Prop
NonContradictory (
a: Prop
a : 
Prop: Type
Prop) : 
Prop: Type
Prop := ¬¬
a: Prop
a

#align non_contradictory_intro 
not_not_intro: ∀ {p : Prop}, p → ¬¬p
not_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 a
congrFun ← 
congr_fun: ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congr_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 c
trans_rel_left {
α: Sort u
α : 
Sort u: Type u
Sort
Sort u: Type u
 u} {
a: α
a 
b: α
b 
c: α
c : 
α: Sort u
α}
    (
r: α → α → Prop
r : 
α: Sort u
α → 
α: Sort u
α → 
Prop: Type
Prop) (
h₁: r a b
h₁ : 
r: α → α → Prop
r 
a: α
a 
b: α
b) (
h₂: b = c
h₂ : 
b: α
b = 
c: α
c) : 
r: α → α → Prop
r 
a: α
a 
c: α
c := 
h₂: b = c
h₂ ▸ 
h₁: r a b
h₁

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

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

theorem 
cast_proof_irrel: ∀ {α β : Sort u_1} (h₁ h₂ : α = β) (a : α), cast h₁ a = cast h₂ a
cast_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 = a
rfl

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

/- Ne -/

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

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

/- HEq -/

alias 
eqRec_heq: ∀ {α : Sort u} {φ : α → Sort v} {a a' : α} (h : a = a') (p : φ a), HEq (Eq.recOn h p) p
eqRec_heq ← 
eq_rec_heq: ∀ {α : Sort u} {φ : α → Sort v} {a a' : α} (h : a = a') (p : φ a), HEq (Eq.recOn h p) p
eq_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 a
HEq.symm
attribute [trans] 
HEq.trans: ∀ {α β φ : Sort u} {a : α} {b : β} {c : φ}, HEq a b → HEq b c → HEq a c
HEq.trans
attribute [trans] 
heq_of_eq_of_heq: ∀ {α β : Sort u} {a a' : α} {b : β}, a = a' → HEq a' b → HEq a b
heq_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 v
Sort
Sort v: Type v
 v} {
a: α
a 
a': α
a' : 
α: ?m.311
α} {
p₁: φ a
p₁ : 
φ: α → 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 t
Eq.rec (motive := fun 
a: ?m.352
a 
_: ?m.355
_ ↦ 
φ: α → Sort v
φ 
a: ?m.352
a) 
p₁: φ a
p₁ 
e: a = a'
e = 
p₂: φ a'
p₂) → 
HEq: {α : Sort ?u.369} → α → {β : Sort ?u.369} → β → Prop
HEq 
p₁: φ a
p₁ 
p₂: φ a'
p₂
  | 
rfl: ∀ {α : Sort ?u.555} {a : α}, a = a
rfl, 
rfl: ∀ {α : Sort ?u.559} {a : α}, a = a
rfl => 
HEq.rfl: ∀ {α : Sort ?u.603} {a : α}, HEq a a
HEq.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 v
Sort
Sort v: Type v
 v} {
a: α
a 
a': α
a' : 
α: ?m.905
α} {
p₁: φ a
p₁ : 
φ: α → Sort v
φ 
a: α
a} {
p₂: φ a'
p₂ : 
φ: α → Sort v
φ 
a': α
a'} :
    (
e: a' = a
e : 
a': α
a' = 
a: α
a) → (
h₂: p₁ = e ▸ p₂
h₂ : 
p₁: φ a
p₁ = 
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 t
Eq.rec (motive := fun 
a: ?m.946
a 
_: ?m.949
_ ↦ 
φ: α → Sort v
φ 
a: ?m.946
a) 
p₂: φ a'
p₂ 
e: a' = a
e) → 
HEq: {α : Sort ?u.963} → α → {β : Sort ?u.963} → β → Prop
HEq 
p₁: φ a
p₁ 
p₂: φ a'
p₂
  | 
rfl: ∀ {α : Sort u_1} {a : α}, a = a
rfl, 
rfl: ∀ {α : Sort ?u.1153} {a : α}, a = a
rfl => 
HEq.rfl: ∀ {α : Sort ?u.1196} {a : α}, HEq a a
HEq.rfl

theorem 
of_heq_true: ∀ {a : Prop}, HEq a True → a
of_heq_true {
a: Prop
a : 
Prop: Type
Prop} (
h: HEq a True
h : 
HEq: {α : Sort ?u.1498} → α → {β : Sort ?u.1498} → β → Prop
HEq 
a: Prop
a 
True: Prop
True) : 
a: Prop
a := 
of_eq_true: ∀ {p : Prop}, p = True → p
of_eq_true (
eq_of_heq: ∀ {α : Sort ?u.1507} {a a' : α}, HEq a a' → a = a'
eq_of_heq 
h: HEq a True
h)

theorem 
eq_rec_compose: ∀ {α β φ : Sort u} (p₁ : β = φ) (p₂ : α = β) (a : α), Eq.recOn p₁ (Eq.recOn p₂ a) = Eq.recOn (_ : α = φ) a
eq_rec_compose {
α: Sort u
α 
β: Sort u
β 
φ: Sort u
φ : 
Sort u: Type u
Sort
Sort 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 t
Eq.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 t
Eq.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 t
Eq.recOn (
Eq.trans: ∀ {α : Sort ?u.1674} {a b c : α}, a = b → b = c → a = c
Eq.trans 
p₂: α = β
p₂ 
p₁: β = φ
p₁) 
a: α
a
  | 
rfl: ∀ {α : Sort ?u.2023} {a : α}, a = a
rfl, 
rfl: ∀ {α : Sort ?u.2027} {a : α}, a = a
rfl, _ => 
rfl: ∀ {α : Sort ?u.2072} {a : α}, a = a
rfl

/- and -/

variable {
a: Prop
a 
b: Prop
b 
c: Prop
c 
d: Prop
d : 
Prop: Type
Prop}

#align and.symm 
And.symm: ∀ {a b : Prop}, a ∧ b → b ∧ a
And.symm
#align and.swap 
And.symm: ∀ {a b : Prop}, a ∧ b → b ∧ a
And.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 ∨ a
Or.symm
#align or.swap 
Or.symm: ∀ {a b : Prop}, a ∨ b → b ∨ a
Or.symm

/- xor -/

def 
Xor': (a b : Prop) → ?m.2374 a b
Xor' (
a: Prop
a 
b: Prop
b : 
Prop: Type
Prop) := (
a: Prop
a ∧ ¬ 
b: Prop
b) ∨ (
b: Prop
b ∧ ¬ 
a: Prop
a)
#align xor 
Xor': Prop → Prop → Prop
Xor'

/- iff -/

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

attribute [refl] 
Iff.refl: ∀ (a : Prop), a ↔ a
Iff.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 Iff
instance : 
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 → Prop
Iff 
Iff: Prop → Prop → Prop
Iff 
Iff: Prop → Prop → Prop
Iff where
  trans := fun 
p: ?m.2468
p 
q: ?m.2471
q ↦ 
p: ?m.2468
p.
trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans 
q: ?m.2471
q

#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 ↔ ¬a
not_not_not

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

-- FIXME
-- attribute [congr] not_congr

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

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

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

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

variable (
p: ?m.2789
p)

-- FIXME: remove _iff and add _eq for the lean 4 core versions
theorem 
and_true_iff: p ∧ True ↔ p
and_true_iff : 
p: ?m.2693
p ∧ 
True: Prop
True ↔ 
p: ?m.2693
p := 
iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)
iff_of_eq (
and_true: ∀ (p : Prop), (p ∧ True) = p
and_true 
_: Prop
_)
#align and_true 
and_true_iff: ∀ (p : Prop), p ∧ True ↔ p
and_true_iff
theorem 
true_and_iff: True ∧ p ↔ p
true_and_iff : 
True: Prop
True ∧ 
p: ?m.2717
p ↔ 
p: ?m.2717
p := 
iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)
iff_of_eq (
true_and: ∀ (p : Prop), (True ∧ p) = p
true_and 
_: Prop
_)
#align true_and 
true_and_iff: ∀ (p : Prop), True ∧ p ↔ p
true_and_iff
theorem 
and_false_iff: ∀ (p : Prop), p ∧ False ↔ False
and_false_iff : 
p: ?m.2741
p ∧ 
False: Prop
False ↔ 
False: Prop
False := 
iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)
iff_of_eq (
and_false: ∀ (p : Prop), (p ∧ False) = False
and_false 
_: Prop
_)
#align and_false 
and_false_iff: ∀ (p : Prop), p ∧ False ↔ False
and_false_iff
theorem 
false_and_iff: ∀ (p : Prop), False ∧ p ↔ False
false_and_iff : 
False: Prop
False ∧ 
p: ?m.2765
p ↔ 
False: Prop
False := 
iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)
iff_of_eq (
false_and: ∀ (p : Prop), (False ∧ p) = False
false_and 
_: Prop
_)
#align false_and 
false_and_iff: ∀ (p : Prop), False ∧ p ↔ False
false_and_iff
#align not_and_self 
not_and_self_iff: ∀ (a : Prop), ¬a ∧ a ↔ False
not_and_self_iff
#align and_not_self 
and_not_self_iff: ∀ (a : Prop), a ∧ ¬a ↔ False
and_not_self_iff
theorem 
and_self_iff: p ∧ p ↔ p
and_self_iff : 
p: ?m.2789
p ∧ 
p: ?m.2789
p ↔ 
p: ?m.2789
p := 
iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)
iff_of_eq (
and_self: ∀ (p : Prop), (p ∧ p) = p
and_self 
_: Prop
_)
#align and_self 
and_self_iff: ∀ (p : Prop), p ∧ p ↔ p
and_self_iff

#align or.imp 
Or.impₓ: ∀ {a c b d : Prop}, (a → c) → (b → d) → a ∨ b → c ∨ d
Or.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 = True
eq_true
#align eq_false_intro 
eq_false: ∀ {p : Prop}, ¬p → p = False
eq_false

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

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

#align or_left_comm 
or_left_comm: ∀ {a b c : Prop}, a ∨ b ∨ c ↔ b ∨ a ∨ c
or_left_comm
#align or.left_comm 
or_left_comm: ∀ {a b c : Prop}, a ∨ b ∨ c ↔ b ∨ a ∨ c
or_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 ↔ True
true_or_iff : 
True: Prop
True ∨ 
p: ?m.2873
p ↔ 
True: Prop
True := 
iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)
iff_of_eq (
true_or: ∀ (p : Prop), (True ∨ p) = True
true_or 
_: Prop
_)
#align true_or 
true_or_iff: ∀ (p : Prop), True ∨ p ↔ True
true_or_iff
theorem 
or_true_iff: p ∨ True ↔ True
or_true_iff : 
p: ?m.2897
p ∨ 
True: Prop
True ↔ 
True: Prop
True := 
iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)
iff_of_eq (
or_true: ∀ (p : Prop), (p ∨ True) = True
or_true 
_: Prop
_)
#align or_true 
or_true_iff: ∀ (p : Prop), p ∨ True ↔ True
or_true_iff
theorem 
false_or_iff: ∀ (p : Prop), False ∨ p ↔ p
false_or_iff : 
False: Prop
False ∨ 
p: ?m.2921
p ↔ 
p: ?m.2921
p := 
iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)
iff_of_eq (
false_or: ∀ (p : Prop), (False ∨ p) = p
false_or 
_: Prop
_)
#align false_or 
false_or_iff: ∀ (p : Prop), False ∨ p ↔ p
false_or_iff
theorem 
or_false_iff: p ∨ False ↔ p
or_false_iff : 
p: ?m.2945
p ∨ 
False: Prop
False ↔ 
p: ?m.2945
p := 
iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)
iff_of_eq (
or_false: ∀ (p : Prop), (p ∨ False) = p
or_false 
_: Prop
_)
#align or_false 
or_false_iff: ∀ (p : Prop), p ∨ False ↔ p
or_false_iff
theorem 
or_self_iff: p ∨ p ↔ p
or_self_iff : 
p: ?m.2969
p ∨ 
p: ?m.2969
p ↔ 
p: ?m.2969
p := 
iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)
iff_of_eq (
or_self: ∀ (p : Prop), (p ∨ p) = p
or_self 
_: Prop
_)
#align or_self 
or_self_iff: ∀ (p : Prop), p ∨ p ↔ p
or_self_iff

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

theorem 
iff_true_iff: (a ↔ True) ↔ a
iff_true_iff : (
a: Prop
a ↔ 
True: Prop
True) ↔ 
a: Prop
a := 
iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)
iff_of_eq (
iff_true: ∀ (p : Prop), (p ↔ True) = p
iff_true 
_: Prop
_)
#align iff_true 
iff_true_iff: ∀ {a : Prop}, (a ↔ True) ↔ a
iff_true_iff
theorem 
true_iff_iff: ∀ {a : Prop}, (True ↔ a) ↔ a
true_iff_iff : (
True: Prop
True ↔ 
a: Prop
a) ↔ 
a: Prop
a := 
iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)
iff_of_eq (
true_iff: ∀ (p : Prop), (True ↔ p) = p
true_iff 
_: Prop
_)
#align true_iff 
true_iff_iff: ∀ {a : Prop}, (True ↔ a) ↔ a
true_iff_iff

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

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

theorem 
iff_self_iff: ∀ (a : Prop), (a ↔ a) ↔ True
iff_self_iff (
a: Prop
a : 
Prop: Type
Prop) : (
a: Prop
a ↔ 
a: Prop
a) ↔ 
True: Prop
True := 
iff_of_eq: ∀ {a b : Prop}, a = b → (a ↔ b)
iff_of_eq (
iff_self: ∀ (p : Prop), (p ↔ p) = True
iff_self 
_: Prop
_)
#align iff_self 
iff_self_iff: ∀ (a : Prop), (a ↔ a) ↔ True
iff_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 ↔ True
imp_true_iff
#align false_implies_iff 
false_imp_iff: ∀ (a : Prop), False → a ↔ True
false_imp_iff
#align true_implies_iff 
true_imp_iff: ∀ (α : Prop), True → α ↔ α
true_imp_iff

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

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

/- exists unique -/

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

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

/-- Pretty-printing for `ExistsUnique`, following the same pattern as pretty printing
    for `Exists`. -/
@[app_unexpander 
ExistsUnique: {α : Sort u_1} → (α → Prop) → Prop
ExistsUnique] def 
unexpandExistsUnique: Lean.PrettyPrinter.Unexpander
unexpandExistsUnique : 
Lean.PrettyPrinter.Unexpander: Type
Lean.PrettyPrinter.Unexpander
  | `($(_) fun $
x: ?m.5187
x:ident ↦ ∃! $
xs: ?m.5180
xs:binderIdent*, $
b: ?m.5171
b) => `(∃! $
x: ?m.5187
x:ident $
xs: ?m.5180
xs:binderIdent*, $
b: ?m.5171
b)
  | `($(_) fun $
x: ?m.5715
x:ident ↦ $
b: ?m.5708
b)                      => `(∃! $
x: ?m.6364
x:ident, $
b: ?m.6357
b)
  | `($(_) fun ($
x: ?m.7180
x:ident : $
t: ?m.7173
t) ↦ $
b: ?m.7166
b)               => `(∃! ($
x: ?m.7180
x:ident : $
t: ?m.7173
t), $
b: ?m.7166
b)
  | _                                               => 
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 x
ExistsUnique.intro {
p: α → Prop
p : 
α: ?m.24288
α → 
Prop: Type
Prop} (
w: α
w : 
α: ?m.24288
α)
    (
h₁: p w
h₁ : 
p: α → Prop
p 
w: α
w) (
h₂: ∀ (y : α), p y → y = w
h₂ : ∀ 
y: ?m.24300
y, 
p: α → Prop
p 
y: ?m.24300
y → 
y: ?m.24300
y = 
w: α
w) : ∃! 
x: ?m.24312
x, 
p: α → Prop
p 
x: ?m.24312
x := ⟨
w: α
w, 
h₁: p w
h₁, 
h₂: ∀ (y : α), p y → y = w
h₂⟩

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

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

theorem 
ExistsUnique.exists: ∀ {α : Sort u_1} {p : α → Prop}, (∃! x, p x) → ∃ x, p x
ExistsUnique.exists {
p: α → Prop
p : 
α: ?m.24609
α → 
Prop: Type
Prop} : (∃! 
x: ?m.24620
x, 
p: α → Prop
p 
x: ?m.24620
x) → ∃ 
x: ?m.24628
x, 
p: α → Prop
p 
x: ?m.24628
x | ⟨
x: α
x, 
h: (fun x => p x) x
h, _⟩ => ⟨
x: α
x, 
h: (fun x => p x) x
h⟩
#align exists_of_exists_unique 
ExistsUnique.exists: ∀ {α : Sort u_1} {p : α → Prop}, (∃! x, p x) → ∃ x, p x
ExistsUnique.exists
#align exists_unique.exists 
ExistsUnique.exists: ∀ {α : Sort u_1} {p : α → Prop}, (∃! x, p x) → ∃ x, p x
ExistsUnique.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 u
Sort
Sort u: Type u
 u} {
p: α → Prop
p : 
α: Sort u
α → 
Prop: Type
Prop}
    (
h: ∃! x, p x
h : ∃! 
x: ?m.24901
x, 
p: α → Prop
p 
x: ?m.24901
x) {
y₁: α
y₁ 
y₂: α
y₂ : 
α: Sort u
α} (
py₁: p y₁
py₁ : 
p: α → Prop
p 
y₁: α
y₁) (
py₂: p y₂
py₂ : 
p: α → Prop
p 
y₂: α
y₂) : 
y₁: α
y₁ = 
y₂: α
y₂ :=
  let ⟨
_: α
_, _, 
hy: ∀ (y : α), (fun x => p x) y → y = w✝
hy⟩ := 
h: ∃! x, p x
h; (
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 = c
trans (
hy: ∀ (y : α), (fun x => p x) y → y = w✝
hy 
_: α
_ 
py₂: p y₂
py₂).
symm: ∀ {α : Sort ?u.25023} {a b : α}, a = b → b = a
symm
#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 a
Exists.imp
#align exists_imp_exists 
Exists.imp: ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (a : α), p a → q a) → (∃ a, p a) → ∃ a, q a
Exists.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: α → Prop
p 
q: α → Prop
q : 
α: ?m.25215
α → 
Prop: Type
Prop} (
h: ∀ (a : α), p a ↔ q a
h : ∀ 
a: ?m.25227
a, 
p: α → Prop
p 
a: ?m.25227
a ↔ 
q: α → Prop
q 
a: ?m.25227
a) : (∃! 
a: ?m.25235
a, 
p: α → Prop
p 
a: ?m.25235
a) ↔ ∃! 
a: ?m.25242
a, 
q: α → Prop
q 
a: ?m.25242
a :=
  
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 a
h 
_: α
_) $ 
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 a
h 
_: α
_)

/- decidable -/

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

theorem 
decide_True': ∀ (h : Decidable True), decide True = true
decide_True' (
h: Decidable True
h : 
Decidable: Prop → Type
Decidable 
True: Prop
True) : 
decide: (p : Prop) → [h : Decidable p] → Bool
decide 
True: Prop
True = 
true: Bool
true := by
Goals accomplished! 🐙 
a, b, c, d: Prop

p: ?m.25343

h: Decidable True

decide True = truesimp
Goals accomplished! 🐙
#align to_bool_true_eq_tt 
decide_True': ∀ (h : Decidable True), decide True = true
decide_True'

theorem 
decide_False': ∀ (h : Decidable False), decide False = false
decide_False' (
h: Decidable False
h : 
Decidable: Prop → Type
Decidable 
False: Prop
False) : 
decide: (p : Prop) → [h : Decidable p] → Bool
decide 
False: Prop
False = 
false: Bool
false := by
Goals accomplished! 🐙 
a, b, c, d: Prop

p: ?m.25417

h: Decidable False

decide False = falsesimp
Goals accomplished! 🐙
#align to_bool_false_eq_ff 
decide_False': ∀ (h : Decidable False), decide False = false
decide_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 p
h : 
Decidable: Prop → Type
Decidable 
p: ?m.25511
p] {
h₁: p → Sort u
h₁ : 
p: ?m.25511
p → 
Sort u: Type u
Sort
Sort u: Type u
 u} {
h₂: ¬p → Sort u
h₂ : ¬
p: ?m.25511
p → 
Sort u: Type u
Sort
Sort u: Type u
 u}
    (
h₃: p
h₃ : 
p: ?m.25511
p) (
h₄: h₁ h₃
h₄ : 
h₁: p → Sort u
h₁ 
h₃: p
h₃) : 
Decidable.recOn: {p : Prop} →
  {motive : Decidable p → Sort ?u.25528} →
    (t : Decidable p) → ((h : ¬p) → motive (isFalse h)) → ((h : p) → motive (isTrue h)) → motive t
Decidable.recOn 
h: Decidable p
h 
h₂: ¬p → Sort u
h₂ 
h₁: p → Sort u
h₁ :=
  
cast: {α β : Sort ?u.25569} → α = β → α → β
cast (by
Goals accomplished! 🐙 
a, b, c, d, p: Prop

h: Decidable p

h₁: p → Sort u

h₂: ¬p → Sort u

h₃: p

h₄: h₁ h₃

h₁ h₃ = Decidable.recOn h h₂ h₁match 
h: Decidable p
h with 
a, b, c, d, p: Prop

h: Decidable p

h₁: p → Sort u

h₂: ¬p → Sort u

h₃: p

h₄: h₁ h₃

h₁ h₃ = Decidable.recOn h h₂ h₁| 
.isTrue: {p : Prop} → p → Decidable p
.isTrue _ =>
a, b, c, d, p: Prop

h: Decidable p

h₁: p → Sort u

h₂: ¬p → Sort u

h₃: p

h₄: h₁ h₃

h✝: p

h₁ h₃ = Decidable.recOn (isTrue h✝) h₂ h₁ 
a, b, c, d, p: Prop

h: Decidable p

h₁: p → Sort u

h₂: ¬p → Sort u

h₃: p

h₄: h₁ h₃

h₁ h₃ = Decidable.recOn h h₂ h₁rfl
Goals 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 p
h : 
Decidable: Prop → Type
Decidable 
p: ?m.25773
p] {
h₁: p → Sort u
h₁ : 
p: ?m.25773
p → 
Sort u: Type u
Sort
Sort u: Type u
 u} {
h₂: ¬p → Sort u
h₂ : ¬
p: ?m.25773
p → 
Sort u: Type u
Sort
Sort u: Type u
 u} (
h₃: ¬p
h₃ : ¬
p: ?m.25773
p) (
h₄: h₂ h₃
h₄ : 
h₂: ¬p → Sort u
h₂ 
h₃: ¬p
h₃) :
    
Decidable.recOn: {p : Prop} →
  {motive : Decidable p → Sort ?u.25791} →
    (t : Decidable p) → ((h : ¬p) → motive (isFalse h)) → ((h : p) → motive (isTrue h)) → motive t
Decidable.recOn 
h: Decidable p
h 
h₂: ¬p → Sort u
h₂ 
h₁: p → Sort u
h₁ :=
  
cast: {α β : Sort ?u.25832} → α = β → α → β
cast (by
Goals accomplished! 🐙 
a, b, c, d, p: Prop

h: Decidable p

h₁: p → Sort u

h₂: ¬p → Sort u

h₃: ¬p

h₄: h₂ h₃

h₂ h₃ = Decidable.recOn h h₂ h₁match 
h: Decidable p
h with 
a, b, c, d, p: Prop

h: Decidable p

h₁: p → Sort u

h₂: ¬p → Sort u

h₃: ¬p

h₄: h₂ h₃

h₂ h₃ = Decidable.recOn h h₂ h₁| 
.isFalse: {p : Prop} → ¬p → Decidable p
.isFalse _ =>
a, b, c, d, p: Prop

h: Decidable p

h₁: p → Sort u

h₂: ¬p → Sort u

h₃: ¬p

h₄: h₂ h₃

h✝: ¬p

h₂ h₃ = Decidable.recOn (isFalse h✝) h₂ h₁ 
a, b, c, d, p: Prop

h: Decidable p

h₁: p → Sort u

h₂: ¬p → Sort u

h₃: ¬p

h₄: h₂ h₃

h₂ h₃ = Decidable.recOn h h₂ h₁rfl
Goals 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) → q
byCases ← 
by_cases: {p : Prop} → {q : Sort u} → [dec : Decidable p] → (p → q) → (¬p → q) → q
by_cases
alias 
byContradiction: ∀ {p : Prop} [dec : Decidable p], (¬p → False) → p
byContradiction ← 
by_contradiction: ∀ {p : Prop} [dec : Decidable p], (¬p → False) → p
by_contradiction
alias 
not_not: ∀ {p : Prop} [inst : Decidable p], ¬¬p ↔ p
not_not ← 
not_not_iff: ∀ {p : Prop} [inst : Decidable p], ¬¬p ↔ p
not_not_iff

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

end Decidable

#align decidable_of_decidable_of_iff 
decidable_of_decidable_of_iff: {p q : Prop} → [inst : Decidable p] → (p ↔ q) → Decidable q
decidable_of_decidable_of_iff
#align decidable_of_decidable_of_eq 
decidable_of_decidable_of_eq: {p q : Prop} → [inst : Decidable p] → p = q → Decidable q
decidable_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 ¬p
instDecidableNot ← 
Not.decidable: {p : Prop} → [dp : Decidable p] → Decidable ¬p
Not.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 True
instDecidableTrue ← 
decidableTrue: Decidable True
decidableTrue
alias 
instDecidableFalse: Decidable False
instDecidableFalse ← 
decidableFalse: Decidable False
decidableFalse

#align decidable.true 
decidableTrue: Decidable True
decidableTrue
#align decidable.false 
decidableFalse: Decidable False
decidableFalse
#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 ¬p
Not.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 → Type
Decidable 
p: ?m.26454
p] [
Decidable: Prop → Type
Decidable 
q: ?m.26460
q] : 
Decidable: Prop → Type
Decidable (
Xor': Prop → Prop → Prop
Xor' 
p: ?m.26454
p 
q: ?m.26460
q) := 
inferInstanceAs: (α : Sort ?u.26471) → [i : α] → α
inferInstanceAs (
Decidable: Prop → Type
Decidable (
Or: Prop → Prop → Prop
Or ..))

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

def 
decidableEq_of_bool_pred: {α : Sort u} → {p : α → α → Bool} → IsDecEq p → IsDecRefl p → DecidableEq α
decidableEq_of_bool_pred {
α: Sort u
α : 
Sort u: Type u
Sort
Sort u: Type u
 u} {
p: α → α → Bool
p : 
α: Sort u
α → 
α: Sort u
α → 
Bool: Type
Bool} (
h₁: IsDecEq p
h₁ : 
IsDecEq: {α : Sort ?u.27003} → (α → α → Bool) → Prop
IsDecEq 
p: α → α → Bool
p)
    (
h₂: IsDecRefl p
h₂ : 
IsDecRefl: {α : Sort ?u.27013} → (α → α → Bool) → Prop
IsDecRefl 
p: α → α → Bool
p) : 
DecidableEq: Sort ?u.27023 → Sort (max1?u.27023)
DecidableEq 
α: Sort u
α
  | 
x: α
x, 
y: α
y =>
    if 
hp: ?m.27088
hp : 
p: α → α → Bool
p 
x: α
x 
y: α
y = 
true: Bool
true then 
isTrue: {p : Prop} → p → Decidable p
isTrue (
h₁: IsDecEq p
h₁ 
hp: ?m.27074
hp)
    else 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse (λ 
hxy: x = y
hxy : 
x: α
x = 
y: α
y => 
absurd: ∀ {a : Prop} {b : Sort ?u.27095}, a → ¬a → b
absurd (
h₂: IsDecRefl p
h₂ 
y: α
y) (by
Goals accomplished! 🐙 
a, b, c, d: Prop

p✝: ?m.26992

α: Sort u

p: α → α → Bool

h₁: IsDecEq p

h₂: IsDecRefl p

x, y: α

hp: ¬p x y = true

hxy: x = y

¬p y y = truerwa [
a, b, c, d: Prop

p✝: ?m.26992

α: Sort u

p: α → α → Bool

h₁: IsDecEq p

h₂: IsDecRefl p

x, y: α

hp: ¬p x y = true

hxy: x = y

¬p y y = true
hxy: x = y
hxy
a, b, c, d: Prop

p✝: ?m.26992

α: Sort u

p: α → α → Bool

h₁: IsDecEq p

h₂: IsDecRefl p

x, y: α

hp: ¬p y y = true

hxy: x = y

¬p y y = true]
a, b, c, d: Prop

p✝: ?m.26992

α: Sort u

p: α → α → Bool

h₁: IsDecEq p

h₂: IsDecRefl p

x, y: α

hp: ¬p y y = true

hxy: x = y

¬p y y = true at 
hp: ¬p x y = true
hp
Goals 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 u
Sort
Sort 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 p
isTrue (
Eq.refl: ∀ {α : Sort ?u.27360} (a : α), a = a
Eq.refl 
a: α
a) :=
  match 
h: DecidableEq α
h 
a: α
a 
a: α
a with
  | 
isTrue: {p : Prop} → p → Decidable p
isTrue _ => 
rfl: ∀ {α : Sort ?u.27387} {a : α}, a = a
rfl

theorem 
decidableEq_inr_neg: ∀ {α : Sort u} [h : DecidableEq α] {a b : α} (n : a ≠ b), h a b = isFalse n
decidableEq_inr_neg {
α: Sort u
α : 
Sort u: Type u
Sort
Sort 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 ≠ b
n : 
a: α
a ≠ 
b: α
b) : 
h: DecidableEq α
h 
a: α
a 
b: α
b = 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse 
n: a ≠ b
n :=
  match 
h: DecidableEq α
h 
a: α
a 
b: α
b with
  | 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse _ => 
rfl: ∀ {α : Sort ?u.27517} {a : α}, a = a
rfl

#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: Prop
p : 
Prop: Type
Prop} [
h: Decidable p
h : 
Decidable: Prop → Type
Decidable 
p: Prop
p] {
h₁: p → Sort u
h₁ : 
p: Prop
p → 
Sort u: Type u
Sort
Sort u: Type u
 u} {
h₂: ¬p → Sort u
h₂ : ¬
p: Prop
p → 
Sort u: Type u
Sort
Sort u: Type u
 u}
    [
h₃: ∀ (h : p), Subsingleton (h₁ h)
h₃ : ∀ 
h: p
h : 
p: Prop
p, 
Subsingleton: Sort ?u.27734 → Prop
Subsingleton (
h₁: p → Sort u
h₁ 
h: p
h)] [
h₄: ∀ (h : ¬p), Subsingleton (h₂ h)
h₄ : ∀ 
h: ¬p
h : ¬
p: Prop
p, 
Subsingleton: Sort ?u.27741 → Prop
Subsingleton (
h₂: ¬p → Sort u
h₂ 
h: ¬p
h)] :
    
Subsingleton: Sort ?u.27746 → Prop
Subsingleton (
Decidable.recOn: {p : Prop} →
  {motive : Decidable p → Sort ?u.27747} →
    (t : Decidable p) → ((h : ¬p) → motive (isFalse h)) → ((h : p) → motive (isTrue h)) → motive t
Decidable.recOn 
h: Decidable p
h 
h₂: ¬p → Sort u
h₂ 
h₁: p → Sort u
h₁) :=
  match 
h: Decidable p
h with
  | 
isTrue: {p : Prop} → p → Decidable p
isTrue 
h: p
h => 
h₃: ∀ (h : p), Subsingleton (h₁ h)
h₃ 
h: p
h
  | 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse 
h: ¬p
h => 
h₄: ∀ (h : ¬p), Subsingleton (h₂ h)
h₄ 
h: ¬p
h

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

theorem 
imp_of_if_pos: ∀ {c t e : Prop} [inst : Decidable c], (if c then t else e) → c → t
imp_of_if_pos {
c: Prop
c 
t: Prop
t 
e: Prop
e : 
Prop: Type
Prop} [
Decidable: Prop → Type
Decidable 
c: Prop
c] (
h: if c then t else e
h : 
ite: {α : Sort ?u.27961} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
c: Prop
c 
t: Prop
t 
e: Prop
e) (
hc: c
hc : 
c: Prop
c) : 
t: Prop
t :=
  by
Goals accomplished! 🐙 
a, b, c✝, d: Prop

p: ?m.27950

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hc: c

thave := 
if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.27984} {t e : α}, (if c then t else e) = t
if_pos 
hc: c
hc ▸ 
h: if c then t else e
h
a, b, c✝, d: Prop

p: ?m.27950

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hc: c

this: t

t;
a, b, c✝, d: Prop

p: ?m.27950

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hc: c

this: t

t 
a, b, c✝, d: Prop

p: ?m.27950

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hc: c

texact 
this: ?m.27979
this
Goals accomplished! 🐙
#align implies_of_if_pos 
imp_of_if_pos: ∀ {c t e : Prop} [inst : Decidable c], (if c then t else e) → c → t
imp_of_if_pos

theorem 
imp_of_if_neg: ∀ {c t e : Prop} [inst : Decidable c], (if c then t else e) → ¬c → e
imp_of_if_neg {
c: Prop
c 
t: Prop
t 
e: Prop
e : 
Prop: Type
Prop} [
Decidable: Prop → Type
Decidable 
c: Prop
c] (
h: if c then t else e
h : 
ite: {α : Sort ?u.28032} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
c: Prop
c 
t: Prop
t 
e: Prop
e) (
hnc: ¬c
hnc : ¬
c: Prop
c) : 
e: Prop
e :=
  by
Goals accomplished! 🐙 
a, b, c✝, d: Prop

p: ?m.28021

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hnc: ¬c

ehave := 
if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.28055} {t e : α}, (if c then t else e) = e
if_neg 
hnc: ¬c
hnc ▸ 
h: if c then t else e
h
a, b, c✝, d: Prop

p: ?m.28021

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hnc: ¬c

this: e

e;
a, b, c✝, d: Prop

p: ?m.28021

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hnc: ¬c

this: e

e 
a, b, c✝, d: Prop

p: ?m.28021

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hnc: ¬c

eexact 
this: ?m.28050
this
Goals accomplished! 🐙
#align implies_of_if_neg 
imp_of_if_neg: ∀ {c t e : Prop} [inst : Decidable c], (if c then t else e) → ¬c → e
imp_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 v
if_ctx_congr {
α: Sort u
α : 
Sort u: Type u
Sort
Sort u: Type u
 u} {
b: Prop
b 
c: Prop
c : 
Prop: Type
Prop} [
dec_b: Decidable b
dec_b : 
Decidable: Prop → Type
Decidable 
b: Prop
b] [
dec_c: Decidable c
dec_c : 
Decidable: Prop → Type
Decidable 
c: Prop
c]
    {
x: α
x 
y: α
y 
u: α
u 
v: α
v : 
α: Sort u
α} (
h_c: b ↔ c
h_c : 
b: Prop
b ↔ 
c: Prop
c) (
h_t: c → x = u
h_t : 
c: Prop
c → 
x: α
x = 
u: α
u) (
h_e: ¬c → y = v
h_e : ¬
c: Prop
c → 
y: α
y = 
v: α
v) : 
ite: {α : Sort ?u.28130} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
b: Prop
b 
x: α
x 
y: α
y = 
ite: {α : Sort ?u.28135} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
c: Prop
c 
u: α
u 
v: α
v :=
  match 
dec_b: Decidable b
dec_b, 
dec_c: Decidable c
dec_c with
  | 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse _,  
isFalse: {p : Prop} → ¬p → Decidable p
isFalse 
h₂: ¬c
h₂ => 
h_e: ¬c → y = v
h_e 
h₂: ¬c
h₂
  | 
isTrue: {p : Prop} → p → Decidable p
isTrue _,   
isTrue: {p : Prop} → p → Decidable p
isTrue 
h₂: c
h₂  => 
h_t: c → x = u
h_t 
h₂: c
h₂
  | 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse 
h₁: ¬b
h₁, 
isTrue: {p : Prop} → p → Decidable p
isTrue 
h₂: c
h₂  => 
absurd: ∀ {a : Prop} {b : Sort ?u.28232}, a → ¬a → b
absurd 
h₂: c
h₂ (
Iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
Iff.mp (
not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not_congr 
h_c: b ↔ c
h_c) 
h₁: ¬b
h₁)
  | 
isTrue: {p : Prop} → p → Decidable p
isTrue 
h₁: b
h₁,  
isFalse: {p : Prop} → ¬p → Decidable p
isFalse 
h₂: ¬c
h₂ => 
absurd: ∀ {a : Prop} {b : Sort ?u.28267}, a → ¬a → b
absurd 
h₁: b
h₁ (
Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
Iff.mpr (
not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not_congr 
h_c: b ↔ c
h_c) 
h₂: ¬c
h₂)

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 v
if_congr {
α: Sort u
α : 
Sort u: Type u
Sort
Sort u: Type u
 u} {
b: Prop
b 
c: Prop
c : 
Prop: Type
Prop} [
Decidable: Prop → Type
Decidable 
b: Prop
b] [
Decidable: Prop → Type
Decidable 
c: Prop
c]
    {
x: α
x 
y: α
y 
u: α
u 
v: α
v : 
α: Sort u
α} (
h_c: b ↔ c
h_c : 
b: Prop
b ↔ 
c: Prop
c) (
h_t: x = u
h_t : 
x: α
x = 
u: α
u) (
h_e: y = v
h_e : 
y: α
y = 
v: α
v) : 
ite: {α : Sort ?u.28509} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
b: Prop
b 
x: α
x 
y: α
y = 
ite: {α : Sort ?u.28514} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
c: Prop
c 
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 v
if_ctx_congr 
h_c: b ↔ c
h_c (λ 
_: ?m.28618
_ => 
h_t: x = u
h_t) (λ 
_: ?m.28623
_ => 
h_e: y = v
h_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: Prop
b 
c: Prop
c 
x: Prop
x 
y: Prop
y 
u: Prop
u 
v: Prop
v : 
Prop: Type
Prop} [
dec_b: Decidable b
dec_b : 
Decidable: Prop → Type
Decidable 
b: Prop
b] [
dec_c: Decidable c
dec_c : 
Decidable: Prop → Type
Decidable 
c: Prop
c]
    (
h_c: b ↔ c
h_c : 
b: Prop
b ↔ 
c: Prop
c) (
h_t: c → (x ↔ u)
h_t : 
c: Prop
c → (
x: Prop
x ↔ 
u: Prop
u)) (
h_e: ¬c → (y ↔ v)
h_e : ¬
c: Prop
c → (
y: Prop
y ↔ 
v: Prop
v)) : 
ite: {α : Sort ?u.28682} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
b: Prop
b 
x: Prop
x 
y: Prop
y ↔ 
ite: {α : Sort ?u.28687} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
c: Prop
c 
u: Prop
u 
v: Prop
v :=
  match 
dec_b: Decidable b
dec_b, 
dec_c: Decidable c
dec_c with
  | 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse _,  
isFalse: {p : Prop} → ¬p → Decidable p
isFalse 
h₂: ¬c
h₂ => 
h_e: ¬c → (y ↔ v)
h_e 
h₂: ¬c
h₂
  | 
isTrue: {p : Prop} → p → Decidable p
isTrue _,   
isTrue: {p : Prop} → p → Decidable p
isTrue 
h₂: c
h₂  => 
h_t: c → (x ↔ u)
h_t 
h₂: c
h₂
  | 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse 
h₁: ¬b
h₁, 
isTrue: {p : Prop} → p → Decidable p
isTrue 
h₂: c
h₂  => 
absurd: ∀ {a : Prop} {b : Sort ?u.28781}, a → ¬a → b
absurd 
h₂: c
h₂ (
Iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
Iff.mp (
not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not_congr 
h_c: b ↔ c
h_c) 
h₁: ¬b
h₁)
  | 
isTrue: {p : Prop} → p → Decidable p
isTrue 
h₁: b
h₁,  
isFalse: {p : Prop} → ¬p → Decidable p
isFalse 
h₂: ¬c
h₂ => 
absurd: ∀ {a : Prop} {b : Sort ?u.28814}, a → ¬a → b
absurd 
h₁: b
h₁ (
Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
Iff.mpr (
not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not_congr 
h_c: b ↔ c
h_c) 
h₂: ¬c
h₂)

-- @[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: Prop
b 
c: Prop
c 
x: Prop
x 
y: Prop
y 
u: Prop
u 
v: Prop
v : 
Prop: Type
Prop} [
Decidable: Prop → Type
Decidable 
b: Prop
b] [
Decidable: Prop → Type
Decidable 
c: Prop
c] (
h_c: b ↔ c
h_c : 
b: Prop
b ↔ 
c: Prop
c) (
h_t: x ↔ u
h_t : 
x: Prop
x ↔ 
u: Prop
u)
    (
h_e: y ↔ v
h_e : 
y: Prop
y ↔ 
v: Prop
v) : 
ite: {α : Sort ?u.29029} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
b: Prop
b 
x: Prop
x 
y: Prop
y ↔ 
ite: {α : Sort ?u.29034} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
c: Prop
c 
u: Prop
u 
v: Prop
v :=
  
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 ↔ c
h_c (λ 
_: ?m.29131
_ => 
h_t: x ↔ u
h_t) (λ 
_: ?m.29136
_ => 
h_e: y ↔ v
h_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: Prop
b 
c: Prop
c 
x: Prop
x 
y: Prop
y 
u: Prop
u 
v: Prop
v : 
Prop: Type
Prop} [
Decidable: Prop → Type
Decidable 
b: Prop
b] (
h_c: b ↔ c
h_c : 
b: Prop
b ↔ 
c: Prop
c) (
h_t: c → (x ↔ u)
h_t : 
c: Prop
c → (
x: Prop
x ↔ 
u: Prop
u))
    -- 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: Prop
c → (
y: Prop
y ↔ 
v: Prop
v)) : 
ite: {α : Sort ?u.29192} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
b: Prop
b 
x: Prop
x 
y: Prop
y ↔ @
ite: {α : Sort ?u.29196} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
_: Sort ?u.29196
_ 
c: Prop
c (
decidable_of_decidable_of_iff: {p q : Prop} → [inst : Decidable p] → (p ↔ q) → Decidable q
decidable_of_decidable_of_iff 
h_c: b ↔ c
h_c) 
u: Prop
u 
v: Prop
v :=
  
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 q
decidable_of_decidable_of_iff 
h_c: b ↔ c
h_c) 
h_c: b ↔ c
h_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: Prop
b 
c: Prop
c 
x: Prop
x 
y: Prop
y 
u: Prop
u 
v: Prop
v : 
Prop: Type
Prop} [
Decidable: Prop → Type
Decidable 
b: Prop
b] (
h_c: b ↔ c
h_c : 
b: Prop
b ↔ 
c: Prop
c) (
h_t: x ↔ u
h_t : 
x: Prop
x ↔ 
u: Prop
u)
    -- 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 ↔ v
h_e : 
y: Prop
y ↔ 
v: Prop
v) : 
ite: {α : Sort ?u.29379} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
b: Prop
b 
x: Prop
x 
y: Prop
y ↔ (@
ite: {α : Sort ?u.29383} → (c : Prop) → [h : Decidable c] → α → α → α
ite 
_: Sort ?u.29383
_ 
c: Prop
c (
decidable_of_decidable_of_iff: {p q : Prop} → [inst : Decidable p] → (p ↔ q) → Decidable q
decidable_of_decidable_of_iff 
h_c: b ↔ c
h_c) 
u: Prop
u 
v: Prop
v) :=
  
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 ↔ c
h_c (λ 
_: ?m.29449
_ => 
h_t: x ↔ u
h_t) (λ 
_: ?m.29454
_ => 
h_e: y ↔ v
h_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 v
dif_ctx_congr {
α: Sort u
α : 
Sort u: Type u
Sort
Sort u: Type u
 u} {
b: Prop
b 
c: Prop
c : 
Prop: Type
Prop} [
dec_b: Decidable b
dec_b : 
Decidable: Prop → Type
Decidable 
b: Prop
b] [
dec_c: Decidable c
dec_c : 
Decidable: Prop → Type
Decidable 
c: Prop
c]
    {
x: b → α
x : 
b: Prop
b → 
α: Sort u
α} {
u: c → α
u : 
c: Prop
c → 
α: Sort u
α} {
y: ¬b → α
y : ¬
b: Prop
b → 
α: Sort u
α} {
v: ¬c → α
v : ¬
c: Prop
c → 
α: Sort u
α}
    (
h_c: b ↔ c
h_c : 
b: Prop
b ↔ 
c: Prop
c) (
h_t: ∀ (h : c), x (_ : b) = u h
h_t : ∀ 
h: c
h : 
c: Prop
c, 
x: b → α
x (
Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
Iff.mpr 
h_c: b ↔ c
h_c 
h: c
h) = 
u: c → α
u 
h: c
h)
    (
h_e: ∀ (h : ¬c), y (_ : ¬b) = v h
h_e : ∀ 
h: ¬c
h : ¬
c: Prop
c, 
y: ¬b → α
y (
Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
Iff.mpr (
not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not_congr 
h_c: b ↔ c
h_c) 
h: ¬c
h) = 
v: ¬c → α
v 
h: ¬c
h) :
    @
dite: {α : Sort ?u.29538} → (c : Prop) → [h : Decidable c] → (c → α) → (¬c → α) → α
dite 
α: Sort u
α 
b: Prop
b 
dec_b: Decidable b
dec_b 
x: b → α
x 
y: ¬b → α
y = @
dite: {α : Sort ?u.29541} → (c : Prop) → [h : Decidable c] → (c → α) → (¬c → α) → α
dite 
α: Sort u
α 
c: Prop
c 
dec_c: Decidable c
dec_c 
u: c → α
u 
v: ¬c → α
v :=
  match 
dec_b: Decidable b
dec_b, 
dec_c: Decidable c
dec_c with
  | 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse _, 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse 
h₂: ¬c
h₂ => 
h_e: ∀ (h : ¬c), y (_ : ¬b) = v h
h_e 
h₂: ¬c
h₂
  | 
isTrue: {p : Prop} → p → Decidable p
isTrue _, 
isTrue: {p : Prop} → p → Decidable p
isTrue 
h₂: c
h₂ => 
h_t: ∀ (h : c), x (_ : b) = u h
h_t 
h₂: c
h₂
  | 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse 
h₁: ¬b
h₁, 
isTrue: {p : Prop} → p → Decidable p
isTrue 
h₂: c
h₂ => 
absurd: ∀ {a : Prop} {b : Sort ?u.29639}, a → ¬a → b
absurd 
h₂: c
h₂ (
Iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
Iff.mp (
not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not_congr 
h_c: b ↔ c
h_c) 
h₁: ¬b
h₁)
  | 
isTrue: {p : Prop} → p → Decidable p
isTrue 
h₁: b
h₁, 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse 
h₂: ¬c
h₂ => 
absurd: ∀ {a : Prop} {b : Sort ?u.29672}, a → ¬a → b
absurd 
h₁: b
h₁ (
Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
Iff.mpr (
not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not_congr 
h_c: b ↔ c
h_c) 
h₂: ¬c
h₂)

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 v
dif_ctx_simp_congr {
α: Sort u
α : 
Sort u: Type u
Sort
Sort u: Type u
 u} {
b: Prop
b 
c: Prop
c : 
Prop: Type
Prop} [
Decidable: Prop → Type
Decidable 
b: Prop
b]
    {
x: b → α
x : 
b: Prop
b → 
α: Sort u
α} {
u: c → α
u : 
c: Prop
c → 
α: Sort u
α} {
y: ¬b → α
y : ¬
b: Prop
b → 
α: Sort u
α} {
v: ¬c → α
v : ¬
c: Prop
c → 
α: Sort u
α}
    (
h_c: b ↔ c
h_c : 
b: Prop
b ↔ 
c: Prop
c) (
h_t: ∀ (h : c), x (_ : b) = u h
h_t : ∀ 
h: c
h : 
c: Prop
c, 
x: b → α
x (
Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
Iff.mpr 
h_c: b ↔ c
h_c 
h: c
h) = 
u: c → α
u 
h: c
h)
    (
h_e: ∀ (h : ¬c), y (_ : ¬b) = v h
h_e : ∀ 
h: ¬c
h : ¬
c: Prop
c, 
y: ¬b → α
y (
Iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
Iff.mpr (
not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not_congr 
h_c: b ↔ c
h_c) 
h: ¬c
h) = 
v: ¬c → α
v 
h: ¬c
h) :
    -- 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: Prop
b 
x: b → α
x 
y: ¬b → α
y = @
dite: {α : Sort ?u.29933} → (c : Prop) → [h : Decidable c] → (c → α) → (¬c → α) → α
dite 
_: Sort ?u.29933
_ 
c: Prop
c (
decidable_of_decidable_of_iff: {p q : Prop} → [inst : Decidable p] → (p ↔ q) → Decidable q
decidable_of_decidable_of_iff 
h_c: b ↔ c
h_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 v
dif_ctx_congr (dec_c := 
decidable_of_decidable_of_iff: {p q : Prop} → [inst : Decidable p] → (p ↔ q) → Decidable q
decidable_of_decidable_of_iff 
h_c: b ↔ c
h_c) 
h_c: b ↔ c
h_c 
h_t: ∀ (h : c), x (_ : b) = u h
h_t 
h_e: ∀ (h : ¬c), y (_ : ¬b) = v h
h_e

def 
AsTrue: (c : Prop) → [inst : Decidable c] → Prop
AsTrue (
c: Prop
c : 
Prop: Type
Prop) [
Decidable: Prop → Type
Decidable 
c: Prop
c] : 
Prop: Type
Prop := if 
c: Prop
c then 
True: Prop
True else 
False: Prop
False

def 
AsFalse: (c : Prop) → [inst : Decidable c] → Prop
AsFalse (
c: Prop
c : 
Prop: Type
Prop) [
Decidable: Prop → Type
Decidable 
c: Prop
c] : 
Prop: Type
Prop := if 
c: Prop
c then 
False: Prop
False else 
True: Prop
True

theorem 
AsTrue.get: ∀ {c : Prop} [h₁ : Decidable c], AsTrue c → c
AsTrue.get {
c: Prop
c : 
Prop: Type
Prop} [
h₁: Decidable c
h₁ : 
Decidable: Prop → Type
Decidable 
c: Prop
c] (
_: AsTrue c
_ : 
AsTrue: (c : Prop) → [inst : Decidable c] → Prop
AsTrue 
c: Prop
c) : 
c: Prop
c :=
  match 
h₁: Decidable c
h₁ with
  | 
isTrue: {p : Prop} → p → Decidable p
isTrue 
h_c: c
h_c => 
h_c: c
h_c
#align of_as_true 
AsTrue.get: ∀ {c : Prop} [h₁ : Decidable c], AsTrue c → c
AsTrue.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 u
PLift
#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 x
let_value_eq {
α: Sort u
α : 
Sort u: Type u
Sort
Sort u: Type u
 u} {
β: Sort v
β : 
Sort v: Type v
Sort
Sort 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 v
Sort
Sort v: Type v
 v} {
β: α → Sort u
β : 
α: Sort v
α → 
Sort u: Type u
Sort
Sort u: Type u
 u} {
a₁: α
a₁ 
a₂: α
a₂ : 
α: Sort v
α} (
b: (x : α) → β x
b : ∀ 
x: α
x : 
α: Sort v
α, 
β: α → Sort u
β 
x: α
x)
    (
h: a₁ = a₂
h : 
a₁: α
a₁ = 
a₂: α
a₂) : 
HEq: {α : Sort ?u.30416} → α → {β : Sort ?u.30416} → β → Prop
HEq (let 
x: α
x : 
α: Sort v
α := 
a₁: α
a₁; 
b: (x : α) → β x
b 
x: α
x) (let 
x: α
x : 
α: Sort v
α := 
a₂: α
a₂; 
b: (x : α) → β x
b 
x: α
x) := by
Goals accomplished! 🐙 
a, b✝, c, d: Prop

p: ?m.30394

α: Sort v

β: α → Sort u

a₁, a₂: α

b: (x : α) → β x

h: a₁ = a₂

HEq
  (let x := a₁;
  b x)
  (let x := a₂;
  b x)cases 
h: a₁ = a₂
h
a, b✝, c, d: Prop

p: ?m.30394

α: Sort v

β: α → Sort u

a₁: α

b: (x : α) → β x

refl
HEq
  (let x := a₁;
  b x)
  (let x := a₁;
  b x);
a, b✝, c, d: Prop

p: ?m.30394

α: Sort v

β: α → Sort u

a₁: α

b: (x : α) → β x

refl
HEq
  (let x := a₁;
  b x)
  (let x := a₁;
  b x) 
a, b✝, c, d: Prop

p: ?m.30394

α: Sort v

β: α → Sort u

a₁, a₂: α

b: (x : α) → β x

h: a₁ = a₂

HEq
  (let x := a₁;
  b x)
  (let x := a₂;
  b x)rfl
Goals 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₂ x
let_body_eq {
α: Sort v
α : 
Sort v: Type v
Sort
Sort v: Type v
 v} {
β: α → Sort u
β : 
α: Sort v
α → 
Sort u: Type u
Sort
Sort u: Type u
 u} (
a: α
a : 
α: Sort v
α) {
b₁: (x : α) → β x
b₁ 
b₂: (x : α) → β x
b₂ : ∀ 
x: α
x : 
α: Sort v
α, 
β: α → Sort u
β 
x: α
x}
    (
h: ∀ (x : α), b₁ x = b₂ x
h : ∀ 
x: ?m.30572
x, 
b₁: (x : α) → β x
b₁ 
x: ?m.30572
x = 
b₂: (x : α) → β x
b₂ 
x: ?m.30572
x) : (let 
x: α
x : 
α: Sort v
α := 
a: α
a; 
b₁: (x : α) → β x
b₁ 
x: α
x) = (let 
x: α
x : 
α: Sort v
α := 
a: α
a; 
b₂: (x : α) → β x
b₂ 
x: α
x) := by
Goals accomplished! 🐙 
a✝, b, c, d: Prop

p: ?m.30550

α: Sort v

β: α → Sort u

a: α

b₁, b₂: (x : α) → β x

h: ∀ (x : α), b₁ x = b₂ x

(let x := a;
  b₁ x) =   let x := a;
  b₂ xexact 
h: ∀ (x : α), b₁ x = b₂ x
h 
_: α
_ ▸ 
rfl: ∀ {α : Sort ?u.30599} {a : α}, a = a
rfl
Goals 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 x
let_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₂ x
let_eq {
α: Sort v
α : 
Sort v: Type v
Sort
Sort v: Type v
 v} {
β: Sort u
β : 
Sort u: Type u
Sort
Sort 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₂ x
h₂ : ∀ 
x: ?m.30661
x, 
b₁: α → β
b₁ 
x: ?m.30661
x = 
b₂: α → β
b₂ 
x: ?m.30661
x) :
    (let 
x: α
x : 
α: Sort v
α := 
a₁: α
a₁; 
b₁: α → β
b₁ 
x: α
x) = (let 
x: α
x : 
α: Sort v
α := 
a₂: α
a₂; 
b₂: α → β
b₂ 
x: α
x) := by
Goals accomplished! 🐙 
a, b, c, d: Prop

p: ?m.30637

α: Sort v

β: Sort u

a₁, 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₂ x
h₂]
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₂ x
let_eq -- FIXME: mathport thinks this is a dubious translation

section Relation

variable {
α: Sort u
α : 
Sort u: Type u
Sort
Sort u: Type u
 u} {
β: Sort v
β : 
Sort v: Type v
Sort
Sort v: Type v
 v} (
r: β → β → Prop
r : 
β: Sort v
β → 
β: Sort v
β → 
Prop: Type
Prop)

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

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

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

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

lemma 
Equivalence.reflexive: ∀ {r : β → β → Prop}, Equivalence r → Reflexive r
Equivalence.reflexive {
r: β → β → Prop
r : 
β: Sort v
β → 
β: Sort v
β → 
Prop: Type
Prop} (
h: Equivalence r
h : 
Equivalence: {α : Sort ?u.33049} → (α → α → Prop) → Prop
Equivalence 
r: β → β → Prop
r) : 
Reflexive: {β : Sort ?u.33059} → (β → β → Prop) → Prop
Reflexive 
r: β → β → Prop
r := 
h: Equivalence r
h.
refl: ∀ {α : Sort ?u.33072} {r : α → α → Prop}, Equivalence r → ∀ (x : α), r x x
refl

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

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

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

#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 r
Equivalence.mk

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

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