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} [Decidable p] (h : decide p = true) : p = True

theorem eq_false_of_decide {p : Prop} {x✝ : Decidable p} (h : decide p = false) : p = False

@[simp]

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

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

theorem iff_congr {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ ↔ p₂) (h₂ : q₁ ↔ q₂) : (p₁ ↔ q₁) ↔ (p₂ ↔ q₂)

theorem implies_dep_congr_ctx {p₁ p₂ 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₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ = p₂) (h₂ : p₂ → q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂)

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

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

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

theorem pi_congr {α : Sort u} {β β' : α → Sort v} (h : ∀ (a : α), β a = β' a) : ((a : α) → β a) = ((a : α) → β' 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 b' : (a : α) → β a} (a : α) (h : ∀ (x : α), b x = b' x) : (let x := a; b x) = let x := a; b' x

theorem letFun_unused {α : Sort u} {β : Sort v} (a : α) {b b' : β} (h : b = b') : (let_fun x := a; b) = b'

theorem letFun_congr {α : Sort u} {β : Sort v} {a a' : α} {f f' : α → β} (h₁ : a = a') (h₂ : ∀ (x : α), f x = f' x) : letFun a f = letFun a' f'

theorem letFun_body_congr {α : Sort u} {β : Sort v} (a : α) {f f' : α → β} (h : ∀ (x : α), f x = f' x) : letFun a f = letFun a f'

theorem letFun_val_congr {α : Sort u} {β : Sort v} {a a' : α} {f : α → β} (h : a = a') : letFun a f = letFun a' f

theorem ite_congr {α : Sort u_1} {b 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 q : Prop} (h₁ : p = q) (h₂ : q) : p

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

theorem dite_congr {b c : Prop} {α : Sort u_1} {x✝ : Decidable b} [Decidable c] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h₁ : b = c) (h₂ : ∀ (h : c), x ⋯ = u h) (h₃ : ∀ (h : ¬c), y ⋯ = v h) : dite b x 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 : α) (h : c = True) : (if c then a else b) = a

theorem ite_cond_eq_false {α : Sort u} {c : Prop} {x✝ : Decidable c} (a b : α) (h : 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 ⋯

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

@[simp]

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

@[simp]

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

@[simp]

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

instance instLawfulIdentityAndTrue : Std.LawfulIdentity And True

@[simp]

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

@[simp]

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

@[simp]

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

instance instIdempotentOpAnd : Std.IdempotentOp And

@[simp]

theorem and_not_self {a : Prop} : ¬(a ∧ ¬a)

@[simp]

theorem not_and_self {a : Prop} : ¬(¬a ∧ a)

@[simp]

theorem and_imp {a b c : Prop} : a ∧ b → c ↔ a → b → c

@[simp]

theorem not_and {a b : Prop} : ¬(a ∧ b) ↔ a → ¬b

@[simp]

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

instance instIdempotentOpOr : Std.IdempotentOp Or

@[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

instance instLawfulIdentityOrFalse : Std.LawfulIdentity Or False

@[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 forall_false (p : False → Prop) : (∀ (h : False), p h) = 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 not_iff_self {a : Prop} : ¬(¬a ↔ a)

and

theorem and_congr_right {a b c : Prop} (h : a → (b ↔ c)) : a ∧ b ↔ a ∧ c

theorem and_congr_left {c a b : Prop} (h : c → (a ↔ b)) : a ∧ c ↔ b ∧ c

theorem and_assoc {a b c : Prop} : (a ∧ b) ∧ c ↔ a ∧ b ∧ c

instance instAssociativeAnd : Std.Associative And

@[simp]

theorem and_self_left {a b : Prop} : a ∧ a ∧ b ↔ a ∧ b

@[simp]

theorem and_self_right {a b : Prop} : (a ∧ b) ∧ b ↔ a ∧ b

@[simp]

theorem and_congr_right_iff {a b c : Prop} : (a ∧ b ↔ a ∧ c) ↔ a → (b ↔ c)

@[simp]

theorem and_congr_left_iff {a c b : Prop} : (a ∧ c ↔ b ∧ c) ↔ c → (a ↔ b)

theorem and_iff_left_of_imp {a b : Prop} (h : a → b) : a ∧ b ↔ a

theorem and_iff_right_of_imp {b a : Prop} (h : b → a) : a ∧ b ↔ b

@[simp]

theorem and_iff_left_iff_imp {a b : Prop} : (a ∧ b ↔ a) ↔ a → b

@[simp]

theorem and_iff_right_iff_imp {a b : Prop} : (a ∧ b ↔ b) ↔ b → a

@[simp]

theorem iff_self_and {p q : Prop} : (p ↔ p ∧ q) ↔ p → q

@[simp]

theorem iff_and_self {p q : Prop} : (p ↔ q ∧ p) ↔ p → q

or

theorem Or.imp {a c b d : Prop} (f : a → c) (g : b → d) (h : a ∨ b) : c ∨ d

theorem Or.imp_left {a b c : Prop} (f : a → b) : a ∨ c → b ∨ c

theorem Or.imp_right {b c a : Prop} (f : b → c) : a ∨ b → a ∨ c

theorem or_assoc {a b c : Prop} : (a ∨ b) ∨ c ↔ a ∨ b ∨ c

instance instAssociativeOr : Std.Associative Or

@[simp]

theorem or_self_left {a b : Prop} : a ∨ a ∨ b ↔ a ∨ b

@[simp]

theorem or_self_right {a b : Prop} : (a ∨ b) ∨ b ↔ a ∨ b

theorem or_iff_right_of_imp {a b : Prop} (ha : a → b) : a ∨ b ↔ b

theorem or_iff_left_of_imp {b a : Prop} (hb : b → a) : a ∨ b ↔ a

@[simp]

theorem or_iff_left_iff_imp {a b : Prop} : (a ∨ b ↔ a) ↔ b → a

@[simp]

theorem or_iff_right_iff_imp {a b : Prop} : (a ∨ b ↔ b) ↔ a → b

@[simp]

theorem iff_self_or {a b : Prop} : (a ↔ a ∨ b) ↔ b → a

@[simp]

theorem iff_or_self {a b : Prop} : (b ↔ a ∨ b) ↔ a → b

@[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

instance instLawfulIdentityBoolOrFalse : Std.LawfulIdentity (fun (x1 x2 : Bool) => x1 || x2) false

@[simp]

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

@[simp]

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

instance instIdempotentOpBoolOr : Std.IdempotentOp fun (x1 x2 : Bool) => x1 || x2

@[simp]

theorem Bool.or_eq_true (a 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

instance instLawfulIdentityBoolAndTrue : Std.LawfulIdentity (fun (x1 x2 : Bool) => x1 && x2) true

@[simp]

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

instance instIdempotentOpBoolAnd : Std.IdempotentOp fun (x1 x2 : Bool) => x1 && x2

@[simp]

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

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

instance instAssociativeBoolAnd : Std.Associative fun (x1 x2 : Bool) => x1 && x2

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

instance instAssociativeBoolOr : Std.Associative fun (x1 x2 : Bool) => x1 || x2

@[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 beq_true (b : Bool) : (b == true) = b

@[simp]

theorem beq_false (b : Bool) : (b == false) = !b

@[simp]

theorem Bool.not_eq_eq_eq_not {a b : Bool} : (!a) = b ↔ a = !b

We move ! from the left hand side of an equality to the right hand side. This helps confluence, and also helps combining pairs of !s.

@[simp]

theorem Bool.not_eq_not {a b : Bool} : ¬a = !b ↔ a = b

theorem Bool.not_not_eq {a b : Bool} : ¬(!a) = b ↔ a = b

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

theorem Bool.not_eq_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 decide_eq_true_eq {p : Prop} [Decidable p] : (decide p = true) = p

@[simp]

theorem decide_eq_false_iff_not {p : Prop} {x✝ : Decidable p} : decide p = false ↔ ¬p

@[simp]

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

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

@[simp]

theorem heq_eq_eq {α : Sort u_1} (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

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

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

@[reducible, inline, deprecated decide_false (since := "2024-11-05")]

abbrev decide_False (h : Decidable False) : decide False = false

Equations

• decide_False = decide_false

@[reducible, inline, deprecated decide_true (since := "2024-11-05")]

abbrev decide_True (h : Decidable True) : decide True = true

Equations

• decide_True = decide_true

@[simp]

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

@[simp]

theorem beq_eq_false_iff_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} : (a == b) = false ↔ a ≠ b

@[simp]

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

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

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

@[simp]

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