case h
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.54232
ε : Type ?u.54235
ι : Type ?u.54238
f✝ : α →. β
f : β →. γ
g : α →. β
x✝ : α
⊢ x✝ ∈ Dom (comp f g) ↔ x✝ ∈ preimage g (Dom f)
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.54232
ε : Type ?u.54235
ι : Type ?u.54238
f✝ : α →. β
f : β →. γ
g : α →. β
⊢ Dom (comp f g) = preimage g (Dom f)
ext
case h
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.54232
ε : Type ?u.54235
ι : Type ?u.54238
f✝ : α →. β
f : β →. γ
g : α →. β
x✝ : α
⊢ (∃ y a, a ∈ g x✝ ∧ y ∈ f a) ↔ ∃ y x, x ∈ f y ∧ y ∈ g x✝
case h
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.54232
ε : Type ?u.54235
ι : Type ?u.54238
f✝ : α →. β
f : β →. γ
g : α →. β
x✝ : α
⊢ x✝ ∈ Dom (comp f g) ↔ x✝ ∈ preimage g (Dom f)
simp_rw [mem_preimage, mem_dom, comp_apply, Part.mem_bind_iff, ← exists_and_right]
case h
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.54232
ε : Type ?u.54235
ι : Type ?u.54238
f✝ : α →. β
f : β →. γ
g : α →. β
x✝ : α
⊢ (∃ b a, b ∈ g x✝ ∧ a ∈ f b) ↔ ∃ y x, x ∈ f y ∧ y ∈ g x✝
case h
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.54232
ε : Type ?u.54235
ι : Type ?u.54238
f✝ : α →. β
f : β →. γ
g : α →. β
x✝ : α
⊢ (∃ y a, a ∈ g x✝ ∧ y ∈ f a) ↔ ∃ y x, x ∈ f y ∧ y ∈ g x✝
rw [exists_comm]
no goals
case h
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.54232
ε : Type ?u.54235
ι : Type ?u.54238
f✝ : α →. β
f : β →. γ
g : α →. β
x✝ : α
⊢ (∃ b a, b ∈ g x✝ ∧ a ∈ f b) ↔ ∃ y x, x ∈ f y ∧ y ∈ g x✝
simp_rw [and_comm]