[GOAL]
α : Type u
b : Bool
a : α
⊢ (bif b then a else a) = a
[PROOFSTEP]
cases b
[GOAL]
case false
α : Type u
a : α
⊢ (bif false then a else a) = a
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u
a : α
⊢ (bif true then a else a) = a
[PROOFSTEP]
rfl
[GOAL]
b : Bool
⊢ xor b b = false
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ xor false false = false
[PROOFSTEP]
simp
[GOAL]
case true
⊢ xor true true = false
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ xor b true = !b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ xor false true = !false
[PROOFSTEP]
simp
[GOAL]
case true
⊢ xor true true = !true
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ xor b false = b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ xor false false = false
[PROOFSTEP]
simp
[GOAL]
case true
⊢ xor true false = true
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ xor true b = !b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ xor true false = !false
[PROOFSTEP]
simp
[GOAL]
case true
⊢ xor true true = !true
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ xor false b = b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ xor false false = false
[PROOFSTEP]
simp
[GOAL]
case true
⊢ xor false true = true
[PROOFSTEP]
simp
[GOAL]
⊢ ¬true = false
[PROOFSTEP]
decide
[GOAL]
⊢ ¬false = true
[PROOFSTEP]
decide
[GOAL]
b : Bool
⊢ (¬b = true) = (b = false)
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ (¬b = false) = (b = true)
[PROOFSTEP]
simp
[GOAL]
a b : Bool
⊢ ((a && b) = true) = (a = true ∧ b = true)
[PROOFSTEP]
simp
[GOAL]
a b : Bool
⊢ ((a || b) = true) = (a = true ∨ b = true)
[PROOFSTEP]
simp
[GOAL]
a : Bool
⊢ ((!a) = true) = (a = false)
[PROOFSTEP]
cases a
[GOAL]
case false
⊢ ((!false) = true) = (false = false)
[PROOFSTEP]
simp
[GOAL]
case true
⊢ ((!true) = true) = (true = false)
[PROOFSTEP]
simp
[GOAL]
a b : Bool
⊢ ((a && b) = false) = (a = false ∨ b = false)
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
⊢ ((false && b) = false) = (false = false ∨ b = false)
[PROOFSTEP]
cases b
[GOAL]
case true
b : Bool
⊢ ((true && b) = false) = (true = false ∨ b = false)
[PROOFSTEP]
cases b
[GOAL]
case false.false
⊢ ((false && false) = false) = (false = false ∨ false = false)
[PROOFSTEP]
simp
[GOAL]
case false.true
⊢ ((false && true) = false) = (false = false ∨ true = false)
[PROOFSTEP]
simp
[GOAL]
case true.false
⊢ ((true && false) = false) = (true = false ∨ false = false)
[PROOFSTEP]
simp
[GOAL]
case true.true
⊢ ((true && true) = false) = (true = false ∨ true = false)
[PROOFSTEP]
simp
[GOAL]
a b : Bool
⊢ ((a || b) = false) = (a = false ∧ b = false)
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
⊢ ((false || b) = false) = (false = false ∧ b = false)
[PROOFSTEP]
cases b
[GOAL]
case true
b : Bool
⊢ ((true || b) = false) = (true = false ∧ b = false)
[PROOFSTEP]
cases b
[GOAL]
case false.false
⊢ ((false || false) = false) = (false = false ∧ false = false)
[PROOFSTEP]
simp
[GOAL]
case false.true
⊢ ((false || true) = false) = (false = false ∧ true = false)
[PROOFSTEP]
simp
[GOAL]
case true.false
⊢ ((true || false) = false) = (true = false ∧ false = false)
[PROOFSTEP]
simp
[GOAL]
case true.true
⊢ ((true || true) = false) = (true = false ∧ true = false)
[PROOFSTEP]
simp
[GOAL]
a : Bool
⊢ ((!a) = false) = (a = true)
[PROOFSTEP]
cases a
[GOAL]
case false
⊢ ((!false) = false) = (false = true)
[PROOFSTEP]
simp
[GOAL]
case true
⊢ ((!true) = false) = (true = true)
[PROOFSTEP]
simp
[GOAL]
⊢ (false = true) = False
[PROOFSTEP]
simp
[GOAL]
⊢ (true = true) = True
[PROOFSTEP]
simp
[GOAL]
⊢ (false = true) = False
[PROOFSTEP]
simp
[GOAL]
⊢ (true = true) = True
[PROOFSTEP]
simp
[GOAL]
p : Prop
d : Decidable p
⊢ decide p = true ↔ p
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ ¬b = true ↔ b = false
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ ¬false = true ↔ false = false
[PROOFSTEP]
exact by decide
[GOAL]
⊢ ¬false = true ↔ false = false
[PROOFSTEP]
decide
[GOAL]
case true
⊢ ¬true = true ↔ true = false
[PROOFSTEP]
exact by decide
[GOAL]
⊢ ¬true = true ↔ true = false
[PROOFSTEP]
decide
[GOAL]
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
⊢ decide p = decide q
[PROOFSTEP]
cases h' : decide q with
| false => exact decide_false (mt h.1 <| of_decide_false h')
| true => exact decide_true (h.2 <| of_decide_true h')
[GOAL]
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
x✝ : Bool
h' : decide q = x✝
⊢ decide p = x✝
[PROOFSTEP]
cases h' : decide q with
| false => exact decide_false (mt h.1 <| of_decide_false h')
| true => exact decide_true (h.2 <| of_decide_true h')
[GOAL]
case false
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
h' : decide q = false
⊢ decide p = false
[PROOFSTEP]

| false => exact decide_false (mt h.1 <| of_decide_false h')
[GOAL]
case false
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
h' : decide q = false
⊢ decide p = false
[PROOFSTEP]
exact decide_false (mt h.1 <| of_decide_false h')
[GOAL]
case true
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
h' : decide q = true
⊢ decide p = true
[PROOFSTEP]

| true => exact decide_true (h.2 <| of_decide_true h')
[GOAL]
case true
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
h' : decide q = true
⊢ decide p = true
[PROOFSTEP]
exact decide_true (h.2 <| of_decide_true h')
[GOAL]
a b : Bool
⊢ (a || b) = true ↔ a = true ∨ b = true
[PROOFSTEP]
simp
[GOAL]
a b : Bool
⊢ (a && b) = true ↔ a = true ∧ b = true
[PROOFSTEP]
simp
[GOAL]
a b : Bool
⊢ xor a b = true ↔ Xor' (a = true) (b = true)
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
⊢ xor false b = true ↔ Xor' (false = true) (b = true)
[PROOFSTEP]
cases b
[GOAL]
case true
b : Bool
⊢ xor true b = true ↔ Xor' (true = true) (b = true)
[PROOFSTEP]
cases b
[GOAL]
case false.false
⊢ xor false false = true ↔ Xor' (false = true) (false = true)
[PROOFSTEP]
exact by decide
[GOAL]
⊢ xor false false = true ↔ Xor' (false = true) (false = true)
[PROOFSTEP]
decide
[GOAL]
case false.true
⊢ xor false true = true ↔ Xor' (false = true) (true = true)
[PROOFSTEP]
exact by decide
[GOAL]
⊢ xor false true = true ↔ Xor' (false = true) (true = true)
[PROOFSTEP]
decide
[GOAL]
case true.false
⊢ xor true false = true ↔ Xor' (true = true) (false = true)
[PROOFSTEP]
exact by decide
[GOAL]
⊢ xor true false = true ↔ Xor' (true = true) (false = true)
[PROOFSTEP]
decide
[GOAL]
case true.true
⊢ xor true true = true ↔ Xor' (true = true) (true = true)
[PROOFSTEP]
exact by decide
[GOAL]
⊢ xor true true = true ↔ Xor' (true = true) (true = true)
[PROOFSTEP]
decide
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Bool
⊢ ((if c then a else b) = true) = if c then a = true else b = true
[PROOFSTEP]
by_cases c
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Bool
⊢ ((if c then a else b) = true) = if c then a = true else b = true
[PROOFSTEP]
by_cases c
[GOAL]
case pos
c : Prop
inst✝ : Decidable c
a b : Bool
h : c
⊢ ((if c then a else b) = true) = if c then a = true else b = true
[PROOFSTEP]
simp [*]
[GOAL]
case neg
c : Prop
inst✝ : Decidable c
a b : Bool
h : ¬c
⊢ ((if c then a else b) = true) = if c then a = true else b = true
[PROOFSTEP]
simp [*]
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Bool
⊢ ((if c then a else b) = false) = if c then a = false else b = false
[PROOFSTEP]
by_cases c
[GOAL]
c : Prop
inst✝ : Decidable c
a b : Bool
⊢ ((if c then a else b) = false) = if c then a = false else b = false
[PROOFSTEP]
by_cases c
[GOAL]
case pos
c : Prop
inst✝ : Decidable c
a b : Bool
h : c
⊢ ((if c then a else b) = false) = if c then a = false else b = false
[PROOFSTEP]
simp [*]
[GOAL]
case neg
c : Prop
inst✝ : Decidable c
a b : Bool
h : ¬c
⊢ ((if c then a else b) = false) = if c then a = false else b = false
[PROOFSTEP]
simp [*]
