no goals
α : Type u_1
β : Type ?u.11101
γ : Type ?u.11104
δ : Type ?u.11107
r✝ : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
r : Prop → α → Prop
this : (fun x x_1 => x ↔ x_1) = fun x x_1 => x = x_1
⊢ (fun x x_1 => x ↔ x_1) ∘r r = r
rw [this, eq_comp]
case h.h
α : Type u_1
β : Type ?u.11101
γ : Type ?u.11104
δ : Type ?u.11107
r✝ : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
r : Prop → α → Prop
a b : Prop
⊢ (a ↔ b) = (a = b)
α : Type u_1
β : Type ?u.11101
γ : Type ?u.11104
δ : Type ?u.11107
r✝ : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
r : Prop → α → Prop
⊢ (fun x x_1 => x ↔ x_1) = fun x x_1 => x = x_1
funext a b
no goals
case h.h
α : Type u_1
β : Type ?u.11101
γ : Type ?u.11104
δ : Type ?u.11107
r✝ : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
r : Prop → α → Prop
a b : Prop
⊢ (a ↔ b) = (a = b)
exact iff_eq_eq