mathlib documentation

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

theorem imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) :

theorem imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → b = d) :

theorem eq_true_intro {a : Prop} (h : a) :

theorem eq_false_intro {a : Prop} (h : ¬a) :

theorem iff.to_eq {a b : Prop} (h : a ↔ b) :

theorem iff_eq_eq {a b : Prop} :

theorem eq_false {a : Prop} :

theorem eq_true {a : Prop} :