Documentation

Init.SimpLemmas

theorem of_eq_true {p : Prop} (h : p = True) :
p
theorem of_eq_false {p : Prop} (h : p = False) :
theorem eq_true {p : Prop} (h : p) :
theorem eq_false {p : Prop} (h : ¬p) :
theorem eq_false' {p : Prop} (h : pFalse) :
theorem eq_true_of_decide {p : Prop} [Decidable p] (h : decide p = true) :
theorem eq_false_of_decide {p : Prop} :
∀ {x : Decidable p}, decide p = falsep = 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 iff_congr {p₁ : Prop} {p₂ : Prop} {q₁ : Prop} {q₂ : Prop} (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₁ = 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₂ : cx = u) (h₃ : ¬cy = 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) :
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 = u h)(∀ (h : ¬c), y = 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α} :
@[simp]
theorem dite_false {α : Sort u} {t : Falseα} {e : ¬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
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
@[simp]
theorem and_false (p : Prop) :
@[simp]
theorem false_and (p : Prop) :
@[simp]
theorem and_self (p : Prop) :
(p p) = p
@[simp]
theorem and_not_self {a : Prop} :
¬(a ¬a)
@[simp]
theorem not_and_self {a : Prop} :
¬(¬a a)
@[simp]
theorem and_imp {a : Prop} {b : Prop} {c : Prop} :
a bc abc
@[simp]
theorem not_and {a : Prop} {b : Prop} :
¬(a b) a¬b
@[simp]
theorem or_self (p : Prop) :
(p p) = p
@[simp]
theorem or_true (p : Prop) :
@[simp]
theorem true_or (p : Prop) :
@[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) :
(Falsep) = True
@[simp]
theorem forall_false (p : FalseProp) :
(∀ (h : False), p h) = True
@[simp]
theorem implies_true (α : Sort u) :
(αTrue) = True
@[simp]
theorem true_implies (p : Prop) :
(Truep) = p
@[simp]
theorem not_iff_self {a : Prop} :
¬(¬a a)

and #

theorem and_congr_right {a : Prop} {b : Prop} {c : Prop} (h : a(b c)) :
a b a c
theorem and_congr_left {c : Prop} {a : Prop} {b : Prop} (h : c(a b)) :
a c b c
theorem and_assoc {a : Prop} {b : Prop} {c : Prop} :
(a b) c a b c
@[simp]
theorem and_self_left {a : Prop} {b : Prop} :
a a b a b
@[simp]
theorem and_self_right {a : Prop} {b : Prop} :
(a b) b a b
@[simp]
theorem and_congr_right_iff {a : Prop} {b : Prop} {c : Prop} :
(a b a c) a(b c)
@[simp]
theorem and_congr_left_iff {a : Prop} {c : Prop} {b : Prop} :
(a c b c) c(a b)
theorem and_iff_left_of_imp {a : Prop} {b : Prop} (h : ab) :
a b a
theorem and_iff_right_of_imp {b : Prop} {a : Prop} (h : ba) :
a b b
@[simp]
theorem and_iff_left_iff_imp {a : Prop} {b : Prop} :
(a b a) ab
@[simp]
theorem and_iff_right_iff_imp {a : Prop} {b : Prop} :
(a b b) ba
@[simp]
theorem iff_self_and {p : Prop} {q : Prop} :
(p p q) pq
@[simp]
theorem iff_and_self {p : Prop} {q : Prop} :
(p q p) pq

or #

theorem Or.imp {a : Prop} {c : Prop} {b : Prop} {d : Prop} (f : ac) (g : bd) (h : a b) :
c d
theorem Or.imp_left {a : Prop} {b : Prop} {c : Prop} (f : ab) :
a cb c
theorem Or.imp_right {b : Prop} {c : Prop} {a : Prop} (f : bc) :
a ba c
theorem or_assoc {a : Prop} {b : Prop} {c : Prop} :
(a b) c a b c
@[simp]
theorem or_self_left {a : Prop} {b : Prop} :
a a b a b
@[simp]
theorem or_self_right {a : Prop} {b : Prop} :
(a b) b a b
theorem or_iff_right_of_imp {a : Prop} {b : Prop} (ha : ab) :
a b b
theorem or_iff_left_of_imp {b : Prop} {a : Prop} (hb : ba) :
a b a
@[simp]
theorem or_iff_left_iff_imp {a : Prop} {b : Prop} :
(a b a) ba
@[simp]
theorem or_iff_right_iff_imp {a : Prop} {b : Prop} :
(a b b) ab
@[simp]
theorem iff_self_or {a : Prop} {b : Prop} :
(a a b) ba
@[simp]
theorem iff_or_self {a : Prop} {b : Prop} :
(b a b) ab
@[simp]
theorem Bool.or_false (b : Bool) :
(b || false) = b
@[simp]
theorem Bool.or_true (b : Bool) :
@[simp]
theorem Bool.false_or (b : Bool) :
(false || b) = b
@[simp]
theorem Bool.true_or (b : Bool) :
@[simp]
theorem Bool.or_self (b : Bool) :
(b || b) = b
instance instIdempotentOpBoolOr :
Std.IdempotentOp fun (x1 x2 : Bool) => x1 || x2
Equations
@[simp]
theorem Bool.or_eq_true (a : Bool) (b : Bool) :
((a || b) = true) = (a = true b = true)
@[simp]
theorem Bool.and_false (b : Bool) :
@[simp]
theorem Bool.and_true (b : Bool) :
(b && true) = b
@[simp]
theorem Bool.false_and (b : Bool) :
@[simp]
theorem Bool.true_and (b : Bool) :
(true && b) = b
@[simp]
theorem Bool.and_self (b : Bool) :
(b && b) = b
instance instIdempotentOpBoolAnd :
Std.IdempotentOp fun (x1 x2 : Bool) => x1 && x2
Equations
@[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))
instance instAssociativeBoolAnd :
Std.Associative fun (x1 x2 : Bool) => x1 && x2
Equations
theorem Bool.or_assoc (a : Bool) (b : Bool) (c : Bool) :
(a || b || c) = (a || (b || c))
instance instAssociativeBoolOr :
Std.Associative fun (x1 x2 : Bool) => x1 || x2
Equations
@[simp]
theorem Bool.not_not (b : Bool) :
(!!b) = b
@[simp]
@[simp]
@[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 : Bool} {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 : Bool} {b : Bool} :
¬a = !b a = b
theorem Bool.not_not_eq {a : Bool} {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] :
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
@[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 : Bool) (b : Bool) :
((a == b) = true) = (a = b)
theorem Bool.not_beq_to_not_eq (a : Bool) (b : Bool) :
((!a == b) = true) = ¬a = b
@[simp]
theorem Nat.le_zero_eq (a : Nat) :
(a 0) = (a = 0)