[GOAL]
b : Bool
h : Decidable (b = true)
⊢ decide (b = true) = b
[PROOFSTEP]
cases b
[GOAL]
case false
h : Decidable (false = true)
⊢ decide (false = true) = false
[PROOFSTEP]
exact decide_eq_false $ λ j => by cases j
[GOAL]
h : Decidable (false = true)
j : false = true
⊢ False
[PROOFSTEP]
cases j
[GOAL]
case true
h : Decidable (true = true)
⊢ decide (true = true) = true
[PROOFSTEP]
exact decide_eq_true $ rfl
[GOAL]
p : Prop
inst✝ : Decidable p
⊢ (decide ¬p) = !decide p
[PROOFSTEP]
by_cases p
[GOAL]
p : Prop
inst✝ : Decidable p
⊢ (decide ¬p) = !decide p
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p : Prop
inst✝ : Decidable p
h : p
⊢ (decide ¬p) = !decide p
[PROOFSTEP]
simp [*]
[GOAL]
case neg
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ (decide ¬p) = !decide p
[PROOFSTEP]
simp [*]
[GOAL]
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
by_cases p
[GOAL]
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : ¬p
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : ¬p
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : p
h : q
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : p
h : ¬q
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
simp [*]
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : ¬p
h : q
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : ¬p
h : ¬q
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
simp [*]
[GOAL]
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
by_cases p
[GOAL]
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : ¬p
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : ¬p
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : p
h : q
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : p
h : ¬q
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
simp [*]
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : ¬p
h : q
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : ¬p
h : ¬q
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
simp [*]
[GOAL]
a b : Bool
⊢ a = b ↔ (a = true ↔ b = true)
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
⊢ false = b ↔ (false = true ↔ b = true)
[PROOFSTEP]
cases b
[GOAL]
case true
b : Bool
⊢ true = b ↔ (true = true ↔ b = true)
[PROOFSTEP]
cases b
[GOAL]
case false.false
⊢ false = false ↔ (false = true ↔ false = true)
[PROOFSTEP]
simp
  -- Porting note: new theorem
[GOAL]
case false.true
⊢ false = true ↔ (false = true ↔ true = true)
[PROOFSTEP]
simp
  -- Porting note: new theorem
[GOAL]
case true.false
⊢ true = false ↔ (true = true ↔ false = true)
[PROOFSTEP]
simp
  -- Porting note: new theorem
[GOAL]
case true.true
⊢ true = true ↔ (true = true ↔ true = true)
[PROOFSTEP]
simp
  -- Porting note: new theorem
[GOAL]
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = true ↔ (b == a) = true
[PROOFSTEP]
simp [@eq_comm α]
[GOAL]
b : Bool
⊢ b = false ∨ b = true
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ false = false ∨ false = true
[PROOFSTEP]
simp
[GOAL]
case true
⊢ true = false ∨ true = true
[PROOFSTEP]
simp
[GOAL]
p : Bool → Prop
h : ∀ (b : Bool), p b
⊢ p false ∧ p true
[PROOFSTEP]
simp [h]
[GOAL]
p : Bool → Prop
x✝ : p false ∧ p true
b : Bool
h₁ : p false
h₂ : p true
⊢ p b
[PROOFSTEP]
cases b
[GOAL]
case false
p : Bool → Prop
x✝ : p false ∧ p true
h₁ : p false
h₂ : p true
⊢ p false
[PROOFSTEP]
assumption
[GOAL]
case true
p : Bool → Prop
x✝ : p false ∧ p true
h₁ : p false
h₂ : p true
⊢ p true
[PROOFSTEP]
assumption
[GOAL]
p : Bool → Prop
x✝ : ∃ b, p b
b : Bool
h : p b
⊢ p false ∨ p true
[PROOFSTEP]
cases b
[GOAL]
case false
p : Bool → Prop
x✝ : ∃ b, p b
h : p false
⊢ p false ∨ p true
case true p : Bool → Prop x✝ : ∃ b, p b h : p true ⊢ p false ∨ p true
[PROOFSTEP]
exact Or.inl h
[GOAL]
case true
p : Bool → Prop
x✝ : ∃ b, p b
h : p true
⊢ p false ∨ p true
[PROOFSTEP]
exact Or.inr h
[GOAL]
α : Type u_1
b : Bool
t e : α
⊢ (bif b then t else e) = if b = true then t else e
[PROOFSTEP]
cases b
[GOAL]
case false
α : Type u_1
t e : α
⊢ (bif false then t else e) = if false = true then t else e
[PROOFSTEP]
simp
[GOAL]
case true
α : Type u_1
t e : α
⊢ (bif true then t else e) = if true = true then t else e
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
p : Prop
inst✝ : Decidable p
t e : α
⊢ (bif decide p then t else e) = if p then t else e
[PROOFSTEP]
by_cases p
[GOAL]
α : Type u_1
p : Prop
inst✝ : Decidable p
t e : α
⊢ (bif decide p then t else e) = if p then t else e
[PROOFSTEP]
by_cases p
[GOAL]
case pos
α : Type u_1
p : Prop
inst✝ : Decidable p
t e : α
h : p
⊢ (bif decide p then t else e) = if p then t else e
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
p : Prop
inst✝ : Decidable p
t e : α
h : ¬p
⊢ (bif decide p then t else e) = if p then t else e
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
b : Bool
t e : α
⊢ (bif !b then t else e) = bif b then e else t
[PROOFSTEP]
cases b
[GOAL]
case false
α : Type u_1
t e : α
⊢ (bif !false then t else e) = bif false then e else t
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u_1
t e : α
⊢ (bif !true then t else e) = bif true then e else t
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {a b : Bool}, (a = true ↔ b = true) ↔ a = b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a : Bool}, a ≠ false → a = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a : Bool}, a ≠ true → a = false
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), (a || b) = (b || a)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b c : Bool), (a || (b || c)) = (b || (a || c))
[PROOFSTEP]
decide
[GOAL]
a b : Bool
H : a = true
⊢ (a || b) = true
[PROOFSTEP]
simp [H]
[GOAL]
a b : Bool
H : b = true
⊢ (a || b) = true
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
H : b = true
⊢ (false || b) = true
[PROOFSTEP]
simp [H]
[GOAL]
case true
b : Bool
H : b = true
⊢ (true || b) = true
[PROOFSTEP]
simp [H]
[GOAL]
⊢ ∀ (a b : Bool), (a && b) = (b && a)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b c : Bool), (a && (b && c)) = (b && (a && c))
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, (a && b) = true → a = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, a = true → b = true → (a && b) = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, (a && b) = true → b = true
[PROOFSTEP]
decide
[GOAL]
a b c : Bool
⊢ (a && (b || c)) = (a && b || a && c)
[PROOFSTEP]
cases a
[GOAL]
case false
b c : Bool
⊢ (false && (b || c)) = (false && b || false && c)
[PROOFSTEP]
simp
[GOAL]
case true
b c : Bool
⊢ (true && (b || c)) = (true && b || true && c)
[PROOFSTEP]
simp
[GOAL]
a b c : Bool
⊢ ((a || b) && c) = (a && c || b && c)
[PROOFSTEP]
cases a
[GOAL]
case false
b c : Bool
⊢ ((false || b) && c) = (false && c || b && c)
[PROOFSTEP]
cases b
[GOAL]
case true
b c : Bool
⊢ ((true || b) && c) = (true && c || b && c)
[PROOFSTEP]
cases b
[GOAL]
case false.false
c : Bool
⊢ ((false || false) && c) = (false && c || false && c)
[PROOFSTEP]
cases c
[GOAL]
case false.true
c : Bool
⊢ ((false || true) && c) = (false && c || true && c)
[PROOFSTEP]
cases c
[GOAL]
case true.false
c : Bool
⊢ ((true || false) && c) = (true && c || false && c)
[PROOFSTEP]
cases c
[GOAL]
case true.true
c : Bool
⊢ ((true || true) && c) = (true && c || true && c)
[PROOFSTEP]
cases c
[GOAL]
case false.false.false
⊢ ((false || false) && false) = (false && false || false && false)
[PROOFSTEP]
simp
[GOAL]
case false.false.true
⊢ ((false || false) && true) = (false && true || false && true)
[PROOFSTEP]
simp
[GOAL]
case false.true.false
⊢ ((false || true) && false) = (false && false || true && false)
[PROOFSTEP]
simp
[GOAL]
case false.true.true
⊢ ((false || true) && true) = (false && true || true && true)
[PROOFSTEP]
simp
[GOAL]
case true.false.false
⊢ ((true || false) && false) = (true && false || false && false)
[PROOFSTEP]
simp
[GOAL]
case true.false.true
⊢ ((true || false) && true) = (true && true || false && true)
[PROOFSTEP]
simp
[GOAL]
case true.true.false
⊢ ((true || true) && false) = (true && false || true && false)
[PROOFSTEP]
simp
[GOAL]
case true.true.true
⊢ ((true || true) && true) = (true && true || true && true)
[PROOFSTEP]
simp
[GOAL]
a b c : Bool
⊢ (a || b && c) = ((a || b) && (a || c))
[PROOFSTEP]
cases a
[GOAL]
case false
b c : Bool
⊢ (false || b && c) = ((false || b) && (false || c))
[PROOFSTEP]
simp
[GOAL]
case true
b c : Bool
⊢ (true || b && c) = ((true || b) && (true || c))
[PROOFSTEP]
simp
[GOAL]
a b c : Bool
⊢ (a && b || c) = ((a || c) && (b || c))
[PROOFSTEP]
cases a
[GOAL]
case false
b c : Bool
⊢ (false && b || c) = ((false || c) && (b || c))
[PROOFSTEP]
cases b
[GOAL]
case true
b c : Bool
⊢ (true && b || c) = ((true || c) && (b || c))
[PROOFSTEP]
cases b
[GOAL]
case false.false
c : Bool
⊢ (false && false || c) = ((false || c) && (false || c))
[PROOFSTEP]
cases c
[GOAL]
case false.true
c : Bool
⊢ (false && true || c) = ((false || c) && (true || c))
[PROOFSTEP]
cases c
[GOAL]
case true.false
c : Bool
⊢ (true && false || c) = ((true || c) && (false || c))
[PROOFSTEP]
cases c
[GOAL]
case true.true
c : Bool
⊢ (true && true || c) = ((true || c) && (true || c))
[PROOFSTEP]
cases c
[GOAL]
case false.false.false
⊢ (false && false || false) = ((false || false) && (false || false))
[PROOFSTEP]
simp
[GOAL]
case false.false.true
⊢ (false && false || true) = ((false || true) && (false || true))
[PROOFSTEP]
simp
[GOAL]
case false.true.false
⊢ (false && true || false) = ((false || false) && (true || false))
[PROOFSTEP]
simp
[GOAL]
case false.true.true
⊢ (false && true || true) = ((false || true) && (true || true))
[PROOFSTEP]
simp
[GOAL]
case true.false.false
⊢ (true && false || false) = ((true || false) && (false || false))
[PROOFSTEP]
simp
[GOAL]
case true.false.true
⊢ (true && false || true) = ((true || true) && (false || true))
[PROOFSTEP]
simp
[GOAL]
case true.true.false
⊢ (true && true || false) = ((true || false) && (true || false))
[PROOFSTEP]
simp
[GOAL]
case true.true.true
⊢ (true && true || true) = ((true || true) && (true || true))
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ {a b : Bool}, a = !b ↔ a ≠ b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, (!decide (a = b)) = true ↔ a ≠ b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, ¬a = !b ↔ a = b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, ¬(!a) = b ↔ a = b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (b : Bool), (!b) ≠ b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (b : Bool), b ≠ !b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), a = b ∨ a = !b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {b : Bool}, (!b) = true ↔ ¬b = true
[PROOFSTEP]
simp
[GOAL]
a : Bool
⊢ (!decide (a = false)) = true → a = true
[PROOFSTEP]
cases a
[GOAL]
case false
⊢ (!decide (false = false)) = true → false = true
[PROOFSTEP]
decide
[GOAL]
case true
⊢ (!decide (true = false)) = true → true = true
[PROOFSTEP]
decide
[GOAL]
a : Bool
⊢ (!decide (a = true)) = true → a = false
[PROOFSTEP]
cases a
[GOAL]
case false
⊢ (!decide (false = true)) = true → false = false
[PROOFSTEP]
decide
[GOAL]
case true
⊢ (!decide (true = true)) = true → true = false
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x : Bool), (x && !x) = false
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x : Bool), (!x && x) = false
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x : Bool), (x || !x) = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x : Bool), (!x || x) = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), xor a b = xor b a
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b c : Bool), xor (xor a b) c = xor a (xor b c)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b c : Bool), xor a (xor b c) = xor b (xor a c)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a : Bool), xor (!a) a = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a : Bool), (xor a !a) = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), (xor (!a) !b) = xor a b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a : Bool), xor false a = a
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a : Bool), xor a false = a
[PROOFSTEP]
decide
[GOAL]
a b c : Bool
⊢ (a && xor b c) = xor (a && b) (a && c)
[PROOFSTEP]
cases a
[GOAL]
case false
b c : Bool
⊢ (false && xor b c) = xor (false && b) (false && c)
[PROOFSTEP]
simp
[GOAL]
case true
b c : Bool
⊢ (true && xor b c) = xor (true && b) (true && c)
[PROOFSTEP]
simp
[GOAL]
a b c : Bool
⊢ (xor a b && c) = xor (a && c) (b && c)
[PROOFSTEP]
cases a
[GOAL]
case false
b c : Bool
⊢ (xor false b && c) = xor (false && c) (b && c)
[PROOFSTEP]
cases b
[GOAL]
case true
b c : Bool
⊢ (xor true b && c) = xor (true && c) (b && c)
[PROOFSTEP]
cases b
[GOAL]
case false.false
c : Bool
⊢ (xor false false && c) = xor (false && c) (false && c)
[PROOFSTEP]
cases c
[GOAL]
case false.true
c : Bool
⊢ (xor false true && c) = xor (false && c) (true && c)
[PROOFSTEP]
cases c
[GOAL]
case true.false
c : Bool
⊢ (xor true false && c) = xor (true && c) (false && c)
[PROOFSTEP]
cases c
[GOAL]
case true.true
c : Bool
⊢ (xor true true && c) = xor (true && c) (true && c)
[PROOFSTEP]
cases c
[GOAL]
case false.false.false
⊢ (xor false false && false) = xor (false && false) (false && false)
[PROOFSTEP]
simp
[GOAL]
case false.false.true
⊢ (xor false false && true) = xor (false && true) (false && true)
[PROOFSTEP]
simp
[GOAL]
case false.true.false
⊢ (xor false true && false) = xor (false && false) (true && false)
[PROOFSTEP]
simp
[GOAL]
case false.true.true
⊢ (xor false true && true) = xor (false && true) (true && true)
[PROOFSTEP]
simp
[GOAL]
case true.false.false
⊢ (xor true false && false) = xor (true && false) (false && false)
[PROOFSTEP]
simp
[GOAL]
case true.false.true
⊢ (xor true false && true) = xor (true && true) (false && true)
[PROOFSTEP]
simp
[GOAL]
case true.true.false
⊢ (xor true true && false) = xor (true && false) (true && false)
[PROOFSTEP]
simp
[GOAL]
case true.true.true
⊢ (xor true true && true) = xor (true && true) (true && true)
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ {x y : Bool}, xor x y = true ↔ x ≠ y
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), (!(a && b)) = (!a || !b)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), (!(a || b)) = (!a && !b)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, (!a) = !b → a = b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a : Bool), a ≤ a
[PROOFSTEP]
unfold LE.le
[GOAL]
⊢ ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b c : Bool), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
unfold LE.le
[GOAL]
⊢ ∀ (a b c : Bool),
    { le := fun a b => a = false ∨ b = true }.1 a b →
      { le := fun a b => a = false ∨ b = true }.1 b c → { le := fun a b => a = false ∨ b = true }.1 a c
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
unfold LE.le Preorder.toLE
[GOAL]
⊢ ∀ (a b : Bool),
    (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
              (_ :
                ∀ (a b c : Bool),
                  { le := fun a b => a = false ∨ b = true }.1 a b →
                    { le := fun a b => a = false ∨ b = true }.1 b c →
                      { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
        a b →
      (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                (_ :
                  ∀ (a b c : Bool),
                    { le := fun a b => a = false ∨ b = true }.1 a b →
                      { le := fun a b => a = false ∨ b = true }.1 b c →
                        { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
          b a →
        a = b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), a ≤ b ∨ b ≤ a
[PROOFSTEP]
unfold LE.le Preorder.toLE PartialOrder.toPreorder
[GOAL]
⊢ ∀ (a b : Bool),
    (PartialOrder.mk
                (_ :
                  ∀ (a b : Bool),
                    (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                              (_ :
                                ∀ (a b c : Bool),
                                  { le := fun a b => a = false ∨ b = true }.1 a b →
                                    { le := fun a b => a = false ∨ b = true }.1 b c →
                                      { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
                        a b →
                      (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                                (_ :
                                  ∀ (a b c : Bool),
                                    { le := fun a b => a = false ∨ b = true }.1 a b →
                                      { le := fun a b => a = false ∨ b = true }.1 b c →
                                        { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
                          b a →
                        a = b)).1.1.1
        a b ∨
      (PartialOrder.mk
                (_ :
                  ∀ (a b : Bool),
                    (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                              (_ :
                                ∀ (a b c : Bool),
                                  { le := fun a b => a = false ∨ b = true }.1 a b →
                                    { le := fun a b => a = false ∨ b = true }.1 b c →
                                      { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
                        a b →
                      (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                                (_ :
                                  ∀ (a b c : Bool),
                                    { le := fun a b => a = false ∨ b = true }.1 a b →
                                      { le := fun a b => a = false ∨ b = true }.1 b c →
                                        { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
                          b a →
                        a = b)).1.1.1
        b a
[PROOFSTEP]
decide
[GOAL]
⊢ DecidableRel fun x x_1 => x ≤ x_1
[PROOFSTEP]
unfold LE.le Preorder.toLE PartialOrder.toPreorder
[GOAL]
⊢ DecidableRel fun x x_1 =>
    (PartialOrder.mk
              (_ :
                ∀ (a b : Bool),
                  (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                            (_ :
                              ∀ (a b c : Bool),
                                { le := fun a b => a = false ∨ b = true }.1 a b →
                                  { le := fun a b => a = false ∨ b = true }.1 b c →
                                    { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
                      a b →
                    (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                              (_ :
                                ∀ (a b c : Bool),
                                  { le := fun a b => a = false ∨ b = true }.1 a b →
                                    { le := fun a b => a = false ∨ b = true }.1 b c →
                                      { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
                        b a →
                      a = b)).1.1.1
      x x_1
[PROOFSTEP]
exact inferInstance
[GOAL]
a b : Bool
⊢ min a b = if a ≤ b then a else b
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
⊢ min false b = if false ≤ b then false else b
[PROOFSTEP]
cases b
[GOAL]
case true
b : Bool
⊢ min true b = if true ≤ b then true else b
[PROOFSTEP]
cases b
[GOAL]
case false.false
⊢ min false false = if false ≤ false then false else false
[PROOFSTEP]
decide
[GOAL]
case false.true
⊢ min false true = if false ≤ true then false else true
[PROOFSTEP]
decide
[GOAL]
case true.false
⊢ min true false = if true ≤ false then true else false
[PROOFSTEP]
decide
[GOAL]
case true.true
⊢ min true true = if true ≤ true then true else true
[PROOFSTEP]
decide
[GOAL]
a b : Bool
⊢ max a b = if a ≤ b then b else a
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
⊢ max false b = if false ≤ b then b else false
[PROOFSTEP]
cases b
[GOAL]
case true
b : Bool
⊢ max true b = if true ≤ b then b else true
[PROOFSTEP]
cases b
[GOAL]
case false.false
⊢ max false false = if false ≤ false then false else false
[PROOFSTEP]
decide
[GOAL]
case false.true
⊢ max false true = if false ≤ true then true else false
[PROOFSTEP]
decide
[GOAL]
case true.false
⊢ max true false = if true ≤ false then false else true
[PROOFSTEP]
decide
[GOAL]
case true.true
⊢ max true true = if true ≤ true then true else true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {x y : Bool}, x < y ↔ x = false ∧ y = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {x y : Bool}, x ≤ y ↔ x = true → y = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x y : Bool), (x && y) ≤ x
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x y : Bool), (x && y) ≤ y
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {x y z : Bool}, x ≤ y → x ≤ z → x ≤ (y && z)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x y : Bool), x ≤ (x || y)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x y : Bool), y ≤ (x || y)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {x y z : Bool}, x ≤ z → y ≤ z → (x || y) ≤ z
[PROOFSTEP]
decide
[GOAL]
n m : ℕ
h : n ≤ m
⊢ ofNat n ≤ ofNat m
[PROOFSTEP]
simp only [ofNat, ne_eq, _root_.decide_not]
[GOAL]
n m : ℕ
h : n ≤ m
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
cases Nat.decEq n 0 with
| isTrue hn => rw [decide_eq_true hn]; exact false_le
| isFalse hn =>
  cases Nat.decEq m 0 with
  | isFalse hm => rw [decide_eq_false hm]; exact le_true
  | isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
[GOAL]
n m : ℕ
h : n ≤ m
x✝ : Decidable (n = 0)
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
cases Nat.decEq n 0 with
| isTrue hn => rw [decide_eq_true hn]; exact false_le
| isFalse hn =>
  cases Nat.decEq m 0 with
  | isFalse hm => rw [decide_eq_false hm]; exact le_true
  | isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
[GOAL]
case isTrue
n m : ℕ
h : n ≤ m
hn : n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]

| isTrue hn => rw [decide_eq_true hn]; exact false_le
[GOAL]
case isTrue
n m : ℕ
h : n ≤ m
hn : n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
rw [decide_eq_true hn]
[GOAL]
case isTrue
n m : ℕ
h : n ≤ m
hn : n = 0
⊢ (!true) ≤ !decide (m = 0)
[PROOFSTEP]
exact false_le
[GOAL]
case isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]

| isFalse hn =>
  cases Nat.decEq m 0 with
  | isFalse hm => rw [decide_eq_false hm]; exact le_true
  | isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
[GOAL]
case isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
cases Nat.decEq m 0 with
| isFalse hm => rw [decide_eq_false hm]; exact le_true
| isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
[GOAL]
case isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
x✝ : Decidable (m = 0)
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
cases Nat.decEq m 0 with
| isFalse hm => rw [decide_eq_false hm]; exact le_true
| isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
[GOAL]
case isFalse.isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : ¬m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]

| isFalse hm => rw [decide_eq_false hm]; exact le_true
[GOAL]
case isFalse.isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : ¬m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
rw [decide_eq_false hm]
[GOAL]
case isFalse.isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : ¬m = 0
⊢ (!decide (n = 0)) ≤ !false
[PROOFSTEP]
exact le_true
[GOAL]
case isFalse.isTrue
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]

| isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
[GOAL]
case isFalse.isTrue
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
subst hm
[GOAL]
case isFalse.isTrue
n : ℕ
hn : ¬n = 0
h : n ≤ 0
⊢ (!decide (n = 0)) ≤ !decide (0 = 0)
[PROOFSTEP]
have h := le_antisymm h (Nat.zero_le n)
[GOAL]
case isFalse.isTrue
n : ℕ
hn : ¬n = 0
h✝ : n ≤ 0
h : n = 0
⊢ (!decide (n = 0)) ≤ !decide (0 = 0)
[PROOFSTEP]
contradiction
[GOAL]
b₀ b₁ : Bool
h : b₀ ≤ b₁
⊢ toNat b₀ ≤ toNat b₁
[PROOFSTEP]
cases h with
| inl h => subst h; exact Nat.zero_le _
| inr h => subst h; cases b₀ <;> simp
[GOAL]
b₀ b₁ : Bool
h : b₀ ≤ b₁
⊢ toNat b₀ ≤ toNat b₁
[PROOFSTEP]
cases h with
| inl h => subst h; exact Nat.zero_le _
| inr h => subst h; cases b₀ <;> simp
[GOAL]
case inl
b₀ b₁ : Bool
h : b₀ = false
⊢ toNat b₀ ≤ toNat b₁
[PROOFSTEP]

| inl h => subst h; exact Nat.zero_le _
[GOAL]
case inl
b₀ b₁ : Bool
h : b₀ = false
⊢ toNat b₀ ≤ toNat b₁
[PROOFSTEP]
subst h
[GOAL]
case inl
b₁ : Bool
⊢ toNat false ≤ toNat b₁
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
case inr
b₀ b₁ : Bool
h : b₁ = true
⊢ toNat b₀ ≤ toNat b₁
[PROOFSTEP]

| inr h => subst h; cases b₀ <;> simp
[GOAL]
case inr
b₀ b₁ : Bool
h : b₁ = true
⊢ toNat b₀ ≤ toNat b₁
[PROOFSTEP]
subst h
[GOAL]
case inr
b₀ : Bool
⊢ toNat b₀ ≤ toNat true
[PROOFSTEP]
cases b₀
[GOAL]
case inr.false
⊢ toNat false ≤ toNat true
[PROOFSTEP]
simp
[GOAL]
case inr.true
⊢ toNat true ≤ toNat true
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ ofNat (toNat b) = b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ ofNat (toNat false) = false
[PROOFSTEP]
rfl
[GOAL]
case true
⊢ ofNat (toNat true) = true
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
f : Bool → α
H : f false ≠ f true
x y : Bool
hxy : f x = f y
⊢ x = y
[PROOFSTEP]
cases x
[GOAL]
case false
α : Sort u_1
f : Bool → α
H : f false ≠ f true
y : Bool
hxy : f false = f y
⊢ false = y
[PROOFSTEP]
cases y
[GOAL]
case true
α : Sort u_1
f : Bool → α
H : f false ≠ f true
y : Bool
hxy : f true = f y
⊢ true = y
[PROOFSTEP]
cases y
[GOAL]
case false.false
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f false = f false
⊢ false = false
case false.true
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f false = f true
⊢ false = true
case true.false
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f true = f false
⊢ true = false
case true.true α : Sort u_1 f : Bool → α H : f false ≠ f true hxy : f true = f true ⊢ true = true
[PROOFSTEP]
exacts [rfl, (H hxy).elim, (H hxy.symm).elim, rfl]
[GOAL]
f : Bool → Bool
x : Bool
⊢ f (f (f x)) = f x
[PROOFSTEP]
cases x
[GOAL]
case false
f : Bool → Bool
⊢ f (f (f false)) = f false
[PROOFSTEP]
cases h₁ : f true
[GOAL]
case true
f : Bool → Bool
⊢ f (f (f true)) = f true
[PROOFSTEP]
cases h₁ : f true
[GOAL]
case false.false
f : Bool → Bool
h₁ : f true = false
⊢ f (f (f false)) = f false
[PROOFSTEP]
cases h₂ : f false
[GOAL]
case false.true
f : Bool → Bool
h₁ : f true = true
⊢ f (f (f false)) = f false
[PROOFSTEP]
cases h₂ : f false
[GOAL]
case true.false
f : Bool → Bool
h₁ : f true = false
⊢ f (f false) = false
[PROOFSTEP]
cases h₂ : f false
[GOAL]
case true.true
f : Bool → Bool
h₁ : f true = true
⊢ f (f true) = true
[PROOFSTEP]
cases h₂ : f false
[GOAL]
case false.false.false
f : Bool → Bool
h₁ : f true = false
h₂ : f false = false
⊢ f (f false) = false
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case false.false.true
f : Bool → Bool
h₁ : f true = false
h₂ : f false = true
⊢ f (f true) = true
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case false.true.false
f : Bool → Bool
h₁ : f true = true
h₂ : f false = false
⊢ f (f false) = false
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case false.true.true
f : Bool → Bool
h₁ : f true = true
h₂ : f false = true
⊢ f (f true) = true
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case true.false.false
f : Bool → Bool
h₁ : f true = false
h₂ : f false = false
⊢ f false = false
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case true.false.true
f : Bool → Bool
h₁ : f true = false
h₂ : f false = true
⊢ f true = false
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case true.true.false
f : Bool → Bool
h₁ : f true = true
h₂ : f false = false
⊢ f (f true) = true
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case true.true.true
f : Bool → Bool
h₁ : f true = true
h₂ : f false = true
⊢ f (f true) = true
[PROOFSTEP]
simp only [h₁, h₂]
