no goals
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x (_ : b) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬b) = v h
⊢ dite b x y = dite c u v
cases Decidable.em c with
| inl h => rw [dif_pos h]; subst b; rw [dif_pos h]; exact h₂ h
| inr h => rw [dif_neg h]; subst b; rw [dif_neg h]; exact h₃ h
case inl
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x (_ : b) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬b) = v h
h : c
⊢ dite b x y = u h
case inl
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x (_ : b) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬b) = v h
h : c
⊢ dite b x y = dite c u v
rw [dif_pos h]
case inl
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x (_ : c) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬c) = v h
⊢ dite c x y = u h
case inl
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x (_ : b) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬b) = v h
h : c
⊢ dite b x y = u h
subst b
case inl
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x (_ : c) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬c) = v h
⊢ x h = u h
case inl
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x (_ : c) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬c) = v h
⊢ dite c x y = u h
rw [dif_pos h]
no goals
case inl
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x (_ : c) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬c) = v h
⊢ x h = u h
exact h₂ h
case inr
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x (_ : b) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬b) = v h
h : ¬c
⊢ dite b x y = v h
case inr
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x (_ : b) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬b) = v h
h : ¬c
⊢ dite b x y = dite c u v
rw [dif_neg h]
case inr
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : ¬c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x (_ : c) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬c) = v h
⊢ dite c x y = v h
case inr
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x (_ : b) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬b) = v h
h : ¬c
⊢ dite b x y = v h
subst b
case inr
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : ¬c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x (_ : c) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬c) = v h
⊢ y h = v h
case inr
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : ¬c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x (_ : c) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬c) = v h
⊢ dite c x y = v h
rw [dif_neg h]
no goals
case inr
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : ¬c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x (_ : c) = u h
h₃ : ∀ (h : ¬c), y (_ : ¬c) = v h
⊢ y h = v h
exact h₃ h