no goals
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
⊢ ite b x y = ite c u v
cases Decidable.em c with
| inl h => rw [if_pos h]; subst b; rw [if_pos h]; exact h₂ h
| inr h => rw [if_neg h]; subst b; rw [if_neg h]; exact h₃ h
case inl
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
⊢ ite b x y = u
case inl
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
⊢ ite b x y = ite c u v
rw [if_pos h]
case inl
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
s : Decidable c
⊢ ite c x y = u
case inl
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
⊢ ite b x y = u
subst b
case inl
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
s : Decidable c
⊢ x = u
case inl
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
s : Decidable c
⊢ ite c x y = u
rw [if_pos h]
no goals
case inl
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : c
s : Decidable c
⊢ x = u
exact h₂ h
case inr
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
⊢ ite b x y = v
case inr
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
⊢ ite b x y = ite c u v
rw [if_neg h]
case inr
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
s : Decidable c
⊢ ite c x y = v
case inr
α : Sort u_1
b c : Prop
x y u v : α
s : Decidable b
inst✝ : Decidable c
h₁ : b = c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
⊢ ite b x y = v
subst b
case inr
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
s : Decidable c
⊢ y = v
case inr
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
s : Decidable c
⊢ ite c x y = v
rw [if_neg h]
no goals
case inr
α : Sort u_1
c : Prop
x y u v : α
inst✝ : Decidable c
h₂ : c → x = u
h₃ : ¬c → y = v
h : ¬c
s : Decidable c
⊢ y = v
exact h₃ h