theorem Lean.Grind.rfl_true : true = true

def Lean.Grind.intro_with_eq (p p' : Prop) (q : Sort u) (he : p = p') (h : p' → q) : p → q

Equations

• Lean.Grind.intro_with_eq p p' q he h hp = h ⋯

def Lean.Grind.intro_with_eq' (p p' : Prop) (q : p → Sort u) (he : p = p') (h : (h : p') → q ⋯) (h✝ : p) : q h✝

Equations

• Lean.Grind.intro_with_eq' p p' q he h hp = h ⋯

And

theorem Lean.Grind.and_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∧ b) = b

theorem Lean.Grind.and_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a ∧ b) = a

theorem Lean.Grind.and_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a ∧ b) = False

theorem Lean.Grind.and_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∧ b) = False

theorem Lean.Grind.eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = True) : a = True

theorem Lean.Grind.eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = True) : b = True

theorem Lean.Grind.or_of_and_eq_false {a b : Prop} (h : (a ∧ b) = False) : ¬a ∨ ¬b

Or

theorem Lean.Grind.or_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∨ b) = True

theorem Lean.Grind.or_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a ∨ b) = True

theorem Lean.Grind.or_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a ∨ b) = b

theorem Lean.Grind.or_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∨ b) = a

theorem Lean.Grind.eq_false_of_or_eq_false_left {a b : Prop} (h : (a ∨ b) = False) : a = False

theorem Lean.Grind.eq_false_of_or_eq_false_right {a b : Prop} (h : (a ∨ b) = False) : b = False

Implies

theorem Lean.Grind.imp_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a → b) = True

theorem Lean.Grind.imp_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a → b) = True

theorem Lean.Grind.imp_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a → b) = b

theorem Lean.Grind.eq_false_of_imp_eq_true {a b : Prop} (h₁ : (a → b) = True) (h₂ : b = False) : a = False

theorem Lean.Grind.eq_true_of_imp_eq_false {a b : Prop} (h : (a → b) = False) : a = True

theorem Lean.Grind.eq_false_of_imp_eq_false {a b : Prop} (h : (a → b) = False) : b = False

Not

theorem Lean.Grind.not_eq_of_eq_true {a : Prop} (h : a = True) : (¬a) = False

theorem Lean.Grind.not_eq_of_eq_false {a : Prop} (h : a = False) : (¬a) = True

theorem Lean.Grind.eq_false_of_not_eq_true {a : Prop} (h : (¬a) = True) : a = False

theorem Lean.Grind.eq_true_of_not_eq_false {a : Prop} (h : (¬a) = False) : a = True

theorem Lean.Grind.false_of_not_eq_self {a : Prop} (h : (¬a) = a) : False

Eq

theorem Lean.Grind.eq_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a = b) = b

theorem Lean.Grind.eq_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a = b) = a

theorem Lean.Grind.eq_congr {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = a₂) (h₂ : b₁ = b₂) : (a₁ = b₁) = (a₂ = b₂)

theorem Lean.Grind.eq_congr' {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = b₂) (h₂ : b₁ = a₂) : (a₁ = b₁) = (a₂ = b₂)

theorem Lean.Grind.heq_congr {α β : Sort u} {a₁ b₁ : α} {a₂ b₂ : β} (h₁ : a₁ ≍ a₂) (h₂ : b₁ ≍ b₂) : (a₁ = b₁) = (a₂ = b₂)

theorem Lean.Grind.heq_congr' {α β : Sort u} {a₁ b₁ : α} {a₂ b₂ : β} (h₁ : a₁ ≍ b₂) (h₂ : b₁ ≍ a₂) : (a₁ = b₁) = (a₂ = b₂)

Ne

theorem Lean.Grind.ne_of_ne_of_eq_left {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c

theorem Lean.Grind.ne_of_ne_of_eq_right {α : Sort u} {a b c : α} (h₁ : a = c) (h₂ : b ≠ c) : b ≠ a

BEq

theorem Lean.Grind.beq_eq_true_of_eq {α : Type u} {x✝ : BEq α} : ∀ {x : LawfulBEq α} {a b : α} (h : a = b), (a == b) = true

theorem Lean.Grind.beq_eq_false_of_diseq {α : Type u} {x✝ : BEq α} : ∀ {x : LawfulBEq α} {a b : α} (h : ¬a = b), (a == b) = false

theorem Lean.Grind.eq_of_beq_eq_true {α : Type u} {x✝ : BEq α} : ∀ {x : LawfulBEq α} {a b : α} (h : (a == b) = true), a = b

theorem Lean.Grind.ne_of_beq_eq_false {α : Type u} {x✝ : BEq α} : ∀ {x : LawfulBEq α} {a b : α} (h : (a == b) = false), (a = b) = False

Bool.and

theorem Lean.Grind.Bool.and_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a && b) = b

theorem Lean.Grind.Bool.and_eq_of_eq_true_right {a b : Bool} (h : b = true) : (a && b) = a

theorem Lean.Grind.Bool.and_eq_of_eq_false_left {a b : Bool} (h : a = false) : (a && b) = false

theorem Lean.Grind.Bool.and_eq_of_eq_false_right {a b : Bool} (h : b = false) : (a && b) = false

theorem Lean.Grind.Bool.eq_true_of_and_eq_true_left {a b : Bool} (h : (a && b) = true) : a = true

theorem Lean.Grind.Bool.eq_true_of_and_eq_true_right {a b : Bool} (h : (a && b) = true) : b = true

Bool.or

theorem Lean.Grind.Bool.or_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a || b) = true

theorem Lean.Grind.Bool.or_eq_of_eq_true_right {a b : Bool} (h : b = true) : (a || b) = true

theorem Lean.Grind.Bool.or_eq_of_eq_false_left {a b : Bool} (h : a = false) : (a || b) = b

theorem Lean.Grind.Bool.or_eq_of_eq_false_right {a b : Bool} (h : b = false) : (a || b) = a

theorem Lean.Grind.Bool.eq_false_of_or_eq_false_left {a b : Bool} (h : (a || b) = false) : a = false

theorem Lean.Grind.Bool.eq_false_of_or_eq_false_right {a b : Bool} (h : (a || b) = false) : b = false

Bool.not

theorem Lean.Grind.Bool.not_eq_of_eq_true {a : Bool} (h : a = true) : (!a) = false

theorem Lean.Grind.Bool.not_eq_of_eq_false {a : Bool} (h : a = false) : (!a) = true

theorem Lean.Grind.Bool.eq_false_of_not_eq_true {a : Bool} (h : (!a) = true) : a = false

theorem Lean.Grind.Bool.eq_true_of_not_eq_false {a : Bool} (h : (!a) = false) : a = true

theorem Lean.Grind.Bool.eq_false_of_not_eq_true' {a : Bool} (h : ¬a = true) : a = false

theorem Lean.Grind.Bool.eq_true_of_not_eq_false' {a : Bool} (h : ¬a = false) : a = true

theorem Lean.Grind.Bool.false_of_not_eq_self {a : Bool} (h : (!a) = a) : False

theorem Lean.Grind.Bool.ne_of_eq_true_of_eq_false {a b : Bool} (h₁ : a = true) (h₂ : b = false) : (a = b) = False

theorem Lean.Grind.Bool.ne_of_eq_false_of_eq_true {a b : Bool} (h₁ : a = false) (h₂ : b = true) : (a = b) = False

theorem Lean.Grind.of_eq_eq_true {a b : Prop} (h : (a = b) = True) : a ∧ b ∨ ¬a ∧ ¬b

theorem Lean.Grind.of_eq_eq_false {a b : Prop} (h : (a = b) = False) : a ∧ ¬b ∨ ¬a ∧ b

Forall

theorem Lean.Grind.forall_propagator (p : Prop) (q : p → Prop) (q' : Prop) (h₁ : p = True) (h₂ : q ⋯ = q') : (∀ (hp : p), q hp) = q'

theorem Lean.Grind.of_forall_eq_false (α : Sort u) (p : α → Prop) (h : (∀ (x : α), p x) = False) : ∃ (x : α), ¬p x

dite

theorem Lean.Grind.dite_cond_eq_true' {α : Sort u} {c : Prop} {x✝ : Decidable c} {a : c → α} {b : ¬c → α} {r : α} (h₁ : c = True) (h₂ : a ⋯ = r) : dite c a b = r

theorem Lean.Grind.dite_cond_eq_false' {α : Sort u} {c : Prop} {x✝ : Decidable c} {a : c → α} {b : ¬c → α} {r : α} (h₁ : c = False) (h₂ : b ⋯ = r) : dite c a b = r

Casts

theorem Lean.Grind.eqRec_heq {α : Sort u_2} {a : α} {motive : (x : α) → a = x → Sort u_1} (v : motive a ⋯) {b : α} (h : a = b) : h ▸ v ≍ v

theorem Lean.Grind.eqRecOn_heq {α : Sort u_2} {a : α} {motive : (x : α) → a = x → Sort u_1} {b : α} (h : a = b) (v : motive a ⋯) : Eq.recOn h v ≍ v

theorem Lean.Grind.eqNDRec_heq {α : Sort u_2} {a : α} {motive : α → Sort u_1} (v : motive a) {b : α} (h : a = b) : h ▸ v ≍ v

decide

theorem Lean.Grind.of_decide_eq_true {p : Prop} {x✝ : Decidable p} : decide p = true → p = True

theorem Lean.Grind.of_decide_eq_false {p : Prop} {x✝ : Decidable p} : decide p = false → p = False

theorem Lean.Grind.decide_eq_true {p : Prop} {x✝ : Decidable p} : p = True → decide p = true

theorem Lean.Grind.decide_eq_false {p : Prop} {x✝ : Decidable p} : p = False → decide p = false

Lookahead

theorem Lean.Grind.of_lookahead (p : Prop) (h : ¬p → False) : p = True

Nat propagators

theorem Lean.Grind.Nat.and_congr {a b k₁ k₂ k : Nat} (h₁ : a = k₁) (h₂ : b = k₂) : (k == k₁ &&& k₂) = true → a &&& b = k

theorem Lean.Grind.Nat.xor_congr {a b k₁ k₂ k : Nat} (h₁ : a = k₁) (h₂ : b = k₂) : (k == k₁ ^^^ k₂) = true → a ^^^ b = k

theorem Lean.Grind.Nat.or_congr {a b k₁ k₂ k : Nat} (h₁ : a = k₁) (h₂ : b = k₂) : (k == k₁ ||| k₂) = true → a ||| b = k

theorem Lean.Grind.Nat.shiftLeft_congr {a b k₁ k₂ k : Nat} (h₁ : a = k₁) (h₂ : b = k₂) : (k == k₁ <<< k₂) = true → a <<< b = k

theorem Lean.Grind.Nat.shiftRight_congr {a b k₁ k₂ k : Nat} (h₁ : a = k₁) (h₂ : b = k₂) : (k == k₁ >>> k₂) = true → a >>> b = k

Literal evaluation propagators

theorem Lean.Grind.eval_congr₁ {α : Sort u} {β : Sort v} {f : α → β} {a a' : α} {b : β} (h₁ : a = a') (h₂ : f a' = b) : f a = b

theorem Lean.Grind.eval_congr₂ {α₁ : Sort u} {α₂ : Sort v} {β : Sort w} {f : α₁ → α₂ → β} {a₁ a₁' : α₁} {a₂ a₂' : α₂} {b : β} (h₁ : a₁ = a₁') (h₂ : a₂ = a₂') (h₃ : f a₁' a₂' = b) : f a₁ a₂ = b

theorem Lean.Grind.getElem_congr {coll : Type u} {idx : Type v} {elem : Type w} {valid : coll → idx → Prop} [GetElem coll idx elem valid] {as bs : coll} {i j : idx} {w₁ : valid as i} {a : elem} (h₁ : as = bs) (h₂ : i = j) (h₃ : ∀ (w₂ : valid bs j), bs[j] = a) : as[i] = a

Semiring propagators

theorem Lean.Grind.Semiring.one_mul_congr {α : Type u_1} [Semiring α] {a b : α} (h : a = 1) : a * b = b

theorem Lean.Grind.Semiring.zero_mul_congr {α : Type u_1} [Semiring α] {a b : α} (h : a = 0) : a * b = 0

theorem Lean.Grind.Semiring.mul_one_congr {α : Type u_1} [Semiring α] {a b : α} (h : b = 1) : a * b = a

theorem Lean.Grind.Semiring.mul_zero_congr {α : Type u_1} [Semiring α] {a b : α} (h : b = 0) : a * b = 0