no goals
b : Prop
a : Sort u_1
c : Prop
inst✝ : Decidable b
h : b
⊢ a → b ∨ c ↔ (a → b) ∨ (a → c)
simp [h]
b : Prop
a : Sort u_1
c : Prop
inst✝ : Decidable b
h : ¬b
⊢ a → c ↔ (a → False) ∨ (a → c)
b : Prop
a : Sort u_1
c : Prop
inst✝ : Decidable b
h : ¬b
⊢ a → b ∨ c ↔ (a → b) ∨ (a → c)
rw [eq_false h, false_or]
no goals
b : Prop
a : Sort u_1
c : Prop
inst✝ : Decidable b
h : ¬b
⊢ a → c ↔ (a → False) ∨ (a → c)
exact (or_iff_right_of_imp fun hx x => (hx x).elim).symm