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