[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then q else True) = (¬p ∨ q)
[PROOFSTEP]
by_cases p
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then q else True) = (¬p ∨ q)
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p : Prop
h✝ : Decidable p
q : Prop
h : p
⊢ (if p then q else True) = (¬p ∨ q)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
p : Prop
h✝ : Decidable p
q : Prop
h : ¬p
⊢ (if p then q else True) = (¬p ∨ q)
[PROOFSTEP]
simp [h]
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then True else q) = (p ∨ q)
[PROOFSTEP]
by_cases p
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then True else q) = (p ∨ q)
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p : Prop
h✝ : Decidable p
q : Prop
h : p
⊢ (if p then True else q) = (p ∨ q)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
p : Prop
h✝ : Decidable p
q : Prop
h : ¬p
⊢ (if p then True else q) = (p ∨ q)
[PROOFSTEP]
simp [h]
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then q else False) = (p ∧ q)
[PROOFSTEP]
by_cases p
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then q else False) = (p ∧ q)
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p : Prop
h✝ : Decidable p
q : Prop
h : p
⊢ (if p then q else False) = (p ∧ q)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
p : Prop
h✝ : Decidable p
q : Prop
h : ¬p
⊢ (if p then q else False) = (p ∧ q)
[PROOFSTEP]
simp [h]
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then False else q) = (¬p ∧ q)
[PROOFSTEP]
by_cases p
[GOAL]
p : Prop
h : Decidable p
q : Prop
⊢ (if p then False else q) = (¬p ∧ q)
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p : Prop
h✝ : Decidable p
q : Prop
h : p
⊢ (if p then False else q) = (¬p ∧ q)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
p : Prop
h✝ : Decidable p
q : Prop
h : ¬p
⊢ (if p then False else q) = (¬p ∧ q)
[PROOFSTEP]
simp [h]
