Documentation

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

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

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

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

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

theorem eq_true_of_decide {p : Prop} :

theorem eq_false_of_decide {p : Prop} :

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

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

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

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

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

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

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

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

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

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

theorem dite_congr {b : Prop} {c : Prop} {α : Sort u_1} {s : Decidable b} [inst : Decidable c] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h₁ : b = c) (h₂ : ∀ (h : c), x (Eq.mpr_prop h₁ h) = u h) (h₃ : ∀ (h : ¬c), y (_ : ¬b) = v h) :

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

theorem ite_true {α : Sort u_1} (a : α) (b : α) :

theorem ite_false {α : Sort u_1} (a : α) (b : α) :

theorem dite_true {α : Sort u} {t : True → α} {e : ¬True → α} :

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

theorem ite_self {α : Sort u} {c : Prop} {d : Decidable c} (a : α) :

theorem and_self (p : Prop) :

theorem and_true (p : Prop) :

theorem true_and (p : Prop) :

theorem and_false (p : Prop) :

theorem false_and (p : Prop) :

theorem or_self (p : Prop) :

theorem or_true (p : Prop) :

theorem true_or (p : Prop) :

theorem or_false (p : Prop) :

theorem false_or (p : Prop) :

theorem iff_self (p : Prop) :

theorem iff_true (p : Prop) :

theorem true_iff (p : Prop) :

theorem iff_false (p : Prop) :

theorem false_iff (p : Prop) :

theorem false_implies (p : Prop) :

theorem implies_true (α : Sort u) :

theorem true_implies (p : Prop) :

theorem Bool.or_false (b : Bool) :

theorem Bool.or_true (b : Bool) :

theorem Bool.false_or (b : Bool) :

theorem Bool.true_or (b : Bool) :

theorem Bool.or_self (b : Bool) :

theorem Bool.or_eq_true (a : Bool) (b : Bool) :

theorem Bool.and_false (b : Bool) :

theorem Bool.and_true (b : Bool) :

theorem Bool.false_and (b : Bool) :

theorem Bool.true_and (b : Bool) :

theorem Bool.and_self (b : Bool) :

theorem Bool.and_eq_true (a : Bool) (b : Bool) :

theorem Bool.not_not (b : Bool) :

theorem Bool.not_true :

theorem Bool.not_false :

theorem Bool.not_beq_true (b : Bool) :

theorem Bool.not_beq_false (b : Bool) :

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

theorem Bool.not_beq_to_not_eq (a : Bool) (b : Bool) :

theorem Bool.not_eq_true (b : Bool) :

theorem Bool.not_eq_false (b : Bool) :

theorem decide_eq_true_eq {p : Prop} [inst : Decidable p] :

theorem decide_not {p : Prop} [h : Decidable p] :

theorem not_decide_eq_true {p : Prop} [h : Decidable p] :

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

theorem cond_true {α : Type u_1} (a : α) (b : α) :

theorem cond_false {α : Type u_1} (a : α) (b : α) :

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

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

theorem Nat.le_zero_eq (a : Nat) :

theorem decide_False :

theorem decide_True :