no goals
α : Sort u_1
β : Sort ?u.40743
σ : α → Sort ?u.40739
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
p : P
⊢ A p = if q : Q then B q else if p : P then A p else C p q
rw [dif_neg (h p), dif_pos p]
case e_e
α : Sort u_1
β : Sort ?u.40743
σ : α → Sort ?u.40739
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
⊢ (fun q => C np q) = fun q => if p : P then A p else C p q
α : Sort u_1
β : Sort ?u.40743
σ : α → Sort ?u.40739
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
⊢ (if q : Q then B q else C np q) = if q : Q then B q else if p : P then A p else C p q
congr
case e_e.h
α : Sort u_1
β : Sort ?u.40743
σ : α → Sort ?u.40739
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
x✝ : ¬Q
⊢ C np x✝ = if p : P then A p else C p x✝
case e_e
α : Sort u_1
β : Sort ?u.40743
σ : α → Sort ?u.40739
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
⊢ (fun q => C np q) = fun q => if p : P then A p else C p q
funext _
no goals
case e_e.h
α : Sort u_1
β : Sort ?u.40743
σ : α → Sort ?u.40739
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
x✝ : ¬Q
⊢ C np x✝ = if p : P then A p else C p x✝
rw [dif_neg np]