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 implies_congr_left {p₁ p₂ : Sort u} {q : Sort v} (h : p₁ = p₂) : (p₁ → q) = (p₂ → q)

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

def Lean.Arrow (α : Sort u) (β : Sort v) : Sort (imax u v)

Arrow α β is definitionally equal to α → β, but represented as a function application rather than Expr.forallE.

This representation is useful for proof automation that builds nested implications like pₙ → ... → p₂ → p₁. With Expr.forallE, each nesting level introduces a binder that bumps de Bruijn indices in subterms, destroying sharing even with hash-consing. For example, if p₁ contains #20, then at depth 2 it becomes #21, at depth 3 it becomes #22, etc., causing quadratic proof growth.

With arrow, both arguments are explicit (not under binders), so subterms remain identical across nesting levels and can be shared, yielding linear-sized proofs.

Equations

• Lean.Arrow α β = (α → β)

theorem Lean.arrow_congr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : Arrow p₁ q₁ = Arrow p₂ q₂

theorem Lean.arrow_congr_left {p₁ p₂ : Sort u} {q : Sort v} (h : p₁ = p₂) : Arrow p₁ q = Arrow p₂ q

theorem Lean.arrow_congr_right {p : Sort u} {q₁ q₂ : Sort v} (h : q₁ = q₂) : Arrow p q₁ = Arrow p q₂

theorem Lean.true_arrow (p : Prop) : Arrow True p = p

theorem Lean.true_arrow_congr_left (p q : Prop) : p = True → Arrow p q = q

theorem Lean.true_arrow_congr_right (q q' : Prop) : q = q' → Arrow True q = q'

theorem Lean.true_arrow_congr (p q q' : Prop) : p = True → q = q' → Arrow p q = q'

theorem Lean.false_arrow (p : Prop) : Arrow False p = True

theorem Lean.false_arrow_congr (p q : Prop) : p = False → Arrow p q = True

theorem Lean.arrow_true (α : Sort u) : Arrow α True = True

theorem Lean.arrow_true_congr (α : Sort u) (p : Prop) : p = True → Arrow α p = True

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) : (have x := a; b x) = have x := a'; b' x

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

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

Congruence lemmas for have have kernel performance issues when stated using have directly. Illustration of the problem: the kernel infers that the type of have_congr (fun x => b) (fun x => b') h₁ h₂ is (have x := a; (fun x => b) x) = (have x := a'; (fun x => b') x) rather than (have x := a; b x) = (have x := a'; b' x) That means the kernel will do whnf_core at every step of checking a sequence of these lemmas. Thus, we get quadratically many zeta reductions.

For reference, we have the have versions of the theorems in the following comment, and then after that we have the versions that simpHaveTelescope actually uses, which avoid this issue.

theorem have_unused' {α : Sort u} {β : Sort v} (a : α) {b b' : β} (h : b = b') : (fun (x : α) => b) a = b'

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

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

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

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

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

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 ite_cond_congr {α : Sort u_1} {b c : Prop} {s : Decidable b} [Decidable c] {x y : α} (h₁ : b = c) : (if b then x else y) = if c then x else y

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

theorem dite_cond_congr {α : Sort u_1} {b c : Prop} {s : Decidable b} [Decidable c] {x : b → α} {y : ¬b → α} (h₁ : b = c) : dite b x y = if h : c then x ⋯ else y ⋯

@[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) : (∀ (a : α), 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 : α) : (a ≍ b) = (a = b)

@[simp]

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

@[simp]

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

theorem beq_self_eq_true {α : Type u_1} [BEq α] [ReflBEq α] (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 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)