theorem of_eq_true {p : Prop} (h : p = True) : p

theorem of_eq_false {p : Prop} (h : p = False) : ¬p

theorem eq_true {p : Prop} (h : p) : p = True

theorem eq_false {p : Prop} (h : ¬p) : p = False

theorem eq_false' {p : Prop} (h : p → False) : p = False

theorem eq_true_of_decide {p : Prop} : ∀ {x : Decidable p}, decide p = true → p = True

theorem eq_false_of_decide {p : Prop} : ∀ {x : Decidable p}, decide p = false → p = False

@[simp]

theorem eq_self {α : Sort u_1} (a : α) : (a = a) = True

theorem implies_congr {p₁ : Sort u} {p₂ : Sort u} {q₁ : Sort v} {q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂)

theorem implies_dep_congr_ctx {p₁ : Prop} {p₂ : Prop} {q₁ : Prop} (h₁ : p₁ = p₂) {q₂ : p₂ → Prop} (h₂ : ∀ (h : p₂), q₁ = q₂ h) : (p₁ → q₁) = ∀ (h : p₂), q₂ h

theorem implies_congr_ctx {p₁ : Prop} {p₂ : Prop} {q₁ : Prop} {q₂ : Prop} (h₁ : p₁ = p₂) (h₂ : p₂ → q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂)

theorem forall_congr {α : Sort u} {p : α → Prop} {q : α → Prop} (h : ∀ (a : α), p a = q a) : (∀ (a : α), p a) = ∀ (a : α), q a

theorem forall_prop_domain_congr {p₁ : Prop} {p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop} (h₁ : p₁ = p₂) (h₂ : ∀ (a : p₂), q₁ (_ : p₁) = q₂ a) : (∀ (a : p₁), q₁ a) = ∀ (a : p₂), q₂ a

theorem let_congr {α : Sort u} {β : Sort v} {a : α} {a' : α} {b : α → β} {b' : α → β} (h₁ : a = a') (h₂ : ∀ (x : α), b x = b' x) : (let x := a; b x) = let x := a'; b' x

theorem let_val_congr {α : Sort u} {β : Sort v} {a : α} {a' : α} (b : α → β) (h : a = a') : (let x := a; b x) = let x := a'; b x

theorem let_body_congr {α : Sort u} {β : α → Sort v} {b : (a : α) → β a} {b' : (a : α) → β a} (a : α) (h : ∀ (x : α), b x = b' x) : (let x := a; b x) = let x := a; b' x

theorem ite_congr {α : Sort u_1} {b : Prop} {c : Prop} {x : α} {y : α} {u : α} {v : α} {s : Decidable b} [Decidable c] (h₁ : b = c) (h₂ : c → x = u) (h₃ : ¬c → y = v) : (if b then x else y) = if c then u else v

theorem Eq.mpr_prop {p : Prop} {q : Prop} (h₁ : p = q) (h₂ : q) : p

theorem Eq.mpr_not {p : Prop} {q : Prop} (h₁ : p = q) (h₂ : ¬q) : ¬p

theorem dite_congr {b : Prop} {c : Prop} {α : Sort u_1} : ∀ {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h₁ : b = c), (∀ (h : c), x_1 (_ : b) = u h) → (∀ (h : ¬c), y (_ : ¬b) = v h) → dite b x_1 y = dite c u v

@[simp]

theorem ne_eq {α : Sort u_1} (a : α) (b : α) : (a ≠ b) = ¬a = b

@[simp]

theorem ite_true {α : Sort u_1} (a : α) (b : α) : (if True then a else b) = a

@[simp]

theorem ite_false {α : Sort u_1} (a : α) (b : α) : (if False then a else b) = b

@[simp]

theorem dite_true {α : Sort u} {t : True → α} {e : ¬True → α} : dite True t e = t True.intro

@[simp]

theorem dite_false {α : Sort u} {t : False → α} {e : ¬False → α} : dite False t e = e not_false

theorem ite_cond_eq_true {α : Sort u} {c : Prop} : ∀ {x : Decidable c} (a b : α), c = True → (if c then a else b) = a

theorem ite_cond_eq_false {α : Sort u} {c : Prop} : ∀ {x : Decidable c} (a b : α), c = False → (if c then a else b) = b

theorem dite_cond_eq_true {α : Sort u} {c : Prop} : ∀ {x : Decidable c} {t : c → α} {e : ¬c → α} (h : c = True), dite c t e = t (_ : c)

theorem dite_cond_eq_false {α : Sort u} {c : Prop} : ∀ {x : Decidable c} {t : c → α} {e : ¬c → α} (h : c = False), dite c t e = e (_ : ¬c)

@[simp]

theorem ite_self {α : Sort u} {c : Prop} {d : Decidable c} (a : α) : (if c then a else a) = a

@[simp]

theorem and_self (p : Prop) : (p ∧ p) = p

@[simp]

theorem and_true (p : Prop) : (p ∧ True) = p

@[simp]

theorem true_and (p : Prop) : (True ∧ p) = p

@[simp]

theorem and_false (p : Prop) : (p ∧ False) = False

@[simp]

theorem false_and (p : Prop) : (False ∧ p) = False

@[simp]

theorem or_self (p : Prop) : (p ∨ p) = p

@[simp]

theorem or_true (p : Prop) : (p ∨ True) = True

@[simp]

theorem true_or (p : Prop) : (True ∨ p) = True

@[simp]

theorem or_false (p : Prop) : (p ∨ False) = p

@[simp]

theorem false_or (p : Prop) : (False ∨ p) = p

@[simp]

theorem iff_self (p : Prop) : (p ↔ p) = True

@[simp]

theorem iff_true (p : Prop) : (p ↔ True) = p

@[simp]

theorem true_iff (p : Prop) : (True ↔ p) = p

@[simp]

theorem iff_false (p : Prop) : (p ↔ False) = ¬p

@[simp]

theorem false_iff (p : Prop) : (False ↔ p) = ¬p

@[simp]

theorem false_implies (p : Prop) : (False → p) = True

@[simp]

theorem implies_true (α : Sort u) : (α → True) = True

@[simp]

theorem true_implies (p : Prop) : (True → p) = p

@[simp]

theorem not_false_eq_true : (¬False) = True

@[simp]

theorem not_true_eq_false : (¬True) = False

@[simp]

theorem Bool.or_false (b : Bool) : (b || false) = b

@[simp]

theorem Bool.or_true (b : Bool) : (b || true) = true

@[simp]

theorem Bool.false_or (b : Bool) : (false || b) = b

@[simp]

theorem Bool.true_or (b : Bool) : (true || b) = true

@[simp]

theorem Bool.or_self (b : Bool) : (b || b) = b

@[simp]

theorem Bool.or_eq_true (a : Bool) (b : Bool) : ((a || b) = true) = (a = true ∨ b = true)

@[simp]

theorem Bool.and_false (b : Bool) : (b && false) = false

@[simp]

theorem Bool.and_true (b : Bool) : (b && true) = b

@[simp]

theorem Bool.false_and (b : Bool) : (false && b) = false

@[simp]

theorem Bool.true_and (b : Bool) : (true && b) = b

@[simp]

theorem Bool.and_self (b : Bool) : (b && b) = b

@[simp]

theorem Bool.and_eq_true (a : Bool) (b : Bool) : ((a && b) = true) = (a = true ∧ b = true)

theorem Bool.and_assoc (a : Bool) (b : Bool) (c : Bool) : (a && b && c) = (a && (b && c))

theorem Bool.or_assoc (a : Bool) (b : Bool) (c : Bool) : (a || b || c) = (a || (b || c))

@[simp]

theorem Bool.not_not (b : Bool) : (!!b) = b

@[simp]

theorem Bool.not_true : (!true) = false

@[simp]

theorem Bool.not_false : (!false) = true

@[simp]

theorem Bool.not_beq_true (b : Bool) : (!b == true) = (b == false)

@[simp]

theorem Bool.not_beq_false (b : Bool) : (!b == false) = (b == true)

@[simp]

theorem Bool.not_eq_true' (b : Bool) : ((!b) = true) = (b = false)

@[simp]

theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true)

@[simp]

theorem Bool.beq_to_eq (a : Bool) (b : Bool) : ((a == b) = true) = (a = b)

@[simp]

theorem Bool.not_beq_to_not_eq (a : Bool) (b : Bool) : ((!a == b) = true) = ¬a = b

@[simp]

theorem Bool.not_eq_true (b : Bool) : (¬b = true) = (b = false)

@[simp]

theorem Bool.not_eq_false (b : Bool) : (¬b = false) = (b = true)

@[simp]

theorem decide_eq_true_eq {p : Prop} : ∀ {x : Decidable p}, (decide p = true) = p

@[simp]

theorem decide_not {p : Prop} {h : Decidable p} : (decide ¬p) = !decide p

@[simp]

theorem not_decide_eq_true {p : Prop} {h : Decidable p} : ((!decide p) = true) = ¬p

@[simp]

theorem heq_eq_eq {α : Sort u} (a : α) (b : α) : HEq a b = (a = b)

@[simp]

theorem cond_true {α : Type u_1} (a : α) (b : α) : (bif true then a else b) = a

@[simp]

theorem cond_false {α : Type u_1} (a : α) (b : α) : (bif false then a else b) = b

@[simp]

theorem beq_self_eq_true {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) : (a == a) = true

@[simp]

theorem beq_self_eq_true' {α : Type u_1} [DecidableEq α] (a : α) : (a == a) = true

@[simp]

theorem bne_self_eq_false {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) : (a != a) = false

@[simp]

theorem bne_self_eq_false' {α : Type u_1} [DecidableEq α] (a : α) : (a != a) = false

@[simp]

theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0)

@[simp]

theorem decide_False : decide False = false

@[simp]

theorem decide_True : decide True = true

@[simp]

theorem bne_iff_ne {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (b : α) : (a != b) = true ↔ a ≠ b