[GOAL]
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
⊢ (dite p a fun hp => dite q (b hp) (c hp)) = if hq : q then dite p a fun hp => b hp hq else dite p a fun hp => c hp hq
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : p
h✝ : q
⊢ a h✝¹ = a h✝¹
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : p
h✝ : ¬q
⊢ a h✝¹ = a h✝¹
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : ¬p
h✝ : q
⊢ b h✝¹ h✝ = b h✝¹ (_ : q)
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : ¬p
h✝ : ¬q
⊢ c h✝¹ h✝ = c h✝¹ (_ : ¬q)
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → q → α
b : p → ¬q → α
c : ¬p → α
⊢ dite p (fun hp => dite q (a hp) (b hp)) c =
    if hq : q then dite p (fun hp => a hp hq) c else dite p (fun hp => b hp hq) c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : p
h✝ : q
⊢ a h✝¹ h✝ = a h✝¹ (_ : q)
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : p
h✝ : ¬q
⊢ b h✝¹ h✝ = b h✝¹ (_ : ¬q)
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : ¬p
h✝ : q
⊢ c h✝¹ = c h✝¹
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : ¬p
h✝ : ¬q
⊢ c h✝¹ = c h✝¹
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a b c : α
f : Prop → Prop
⊢ f True ∧ f False → ∀ (p : Prop), f p
[PROOFSTEP]
rintro ⟨h₁, h₀⟩ p
[GOAL]
case intro
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
⊢ f p
[PROOFSTEP]
by_cases hp : p
[GOAL]
case pos
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : p
⊢ f p
[PROOFSTEP]
simp only [hp]
[GOAL]
case neg
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : ¬p
⊢ f p
[PROOFSTEP]
simp only [hp]
[GOAL]
case pos
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : p
⊢ f True
[PROOFSTEP]
assumption
[GOAL]
case neg
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : ¬p
⊢ f False
[PROOFSTEP]
assumption
[GOAL]
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ f True ∨ f False
[PROOFSTEP]
refine' (em p).imp _ _
[GOAL]
case refine'_1
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ p → f True
[PROOFSTEP]
intro H
[GOAL]
case refine'_2
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ ¬p → f False
[PROOFSTEP]
intro H
[GOAL]
case refine'_1
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : p
⊢ f True
[PROOFSTEP]
convert h
[GOAL]
case refine'_2
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : ¬p
⊢ f False
[PROOFSTEP]
convert h
[GOAL]
case h.e'_1.a
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : p
⊢ True ↔ p
[PROOFSTEP]
simp [H]
[GOAL]
case h.e'_1.a
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : ¬p
⊢ False ↔ p
[PROOFSTEP]
simp [H]
[GOAL]
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a b c : α
f : Prop → Prop
⊢ f True ∨ f False → ∃ p, f p
[PROOFSTEP]
rintro (h | h)
[GOAL]
case inl
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h : f True
⊢ ∃ p, f p
[PROOFSTEP]
exact ⟨_, h⟩
[GOAL]
case inr
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h : f False
⊢ ∃ p, f p
[PROOFSTEP]
exact ⟨_, h⟩
