case H
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.57854
ε : Type ?u.57857
ι : Type ?u.57860
f✝ : α →. β
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ c ∈ Part.bind a (comp f g) ↔ c ∈ Part.bind (Part.bind a g) f
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.57854
ε : Type ?u.57857
ι : Type ?u.57860
f✝ : α →. β
f : β →. γ
g : α →. β
a : Part α
⊢ Part.bind a (comp f g) = Part.bind (Part.bind a g) f
ext c
case H
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.57854
ε : Type ?u.57857
ι : Type ?u.57860
f✝ : α →. β
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ (∃ a_1 x, a_1 ∈ a ∧ x ∈ g a_1 ∧ c ∈ f x) ↔ ∃ a_1 x, (x ∈ a ∧ a_1 ∈ g x) ∧ c ∈ f a_1
case H
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.57854
ε : Type ?u.57857
ι : Type ?u.57860
f✝ : α →. β
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ c ∈ Part.bind a (comp f g) ↔ c ∈ Part.bind (Part.bind a g) f
simp_rw [Part.mem_bind_iff, 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.57854
ε : Type ?u.57857
ι : Type ?u.57860
f✝ : α →. β
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ (∃ b a_1, a_1 ∈ a ∧ b ∈ g a_1 ∧ c ∈ f b) ↔ ∃ a_1 x, (x ∈ a ∧ a_1 ∈ g x) ∧ c ∈ f a_1
case H
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.57854
ε : Type ?u.57857
ι : Type ?u.57860
f✝ : α →. β
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ (∃ a_1 x, a_1 ∈ a ∧ x ∈ g a_1 ∧ c ∈ f x) ↔ ∃ a_1 x, (x ∈ a ∧ a_1 ∈ g x) ∧ c ∈ f a_1
rw [exists_comm]
no goals
case H
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.57854
ε : Type ?u.57857
ι : Type ?u.57860
f✝ : α →. β
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ (∃ b a_1, a_1 ∈ a ∧ b ∈ g a_1 ∧ c ∈ f b) ↔ ∃ a_1 x, (x ∈ a ∧ a_1 ∈ g x) ∧ c ∈ f a_1
simp_rw [and_assoc]