[GOAL]
α✝ β✝ : Type u
s✝ : Set α✝
f✝ : α✝ → Set β✝
g : Set (α✝ → β✝)
α β γ : Type u_1
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = Seq.seq (f <$> s) fun x => t
[PROOFSTEP]
ext
[GOAL]
case h
α✝ β✝ : Type u
s✝ : Set α✝
f✝ : α✝ → Set β✝
g : Set (α✝ → β✝)
α β γ : Type u_1
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ Seq.seq (f <$> s) fun x => t
[PROOFSTEP]
simp
[GOAL]
α β : Type u
s : Set α
f : α → Set β
g : Set (α → β)
α✝ β✝ γ✝ : Type ?u.7831
x✝² : Set α✝
x✝¹ : α✝ → Set β✝
x✝ : β✝ → Set γ✝
⊢ x✝² >>= x✝¹ >>= x✝ = x✝² >>= fun x => x✝¹ x >>= x✝
[PROOFSTEP]
simp only [bind_def, biUnion_iUnion]
[GOAL]
α β✝ : Type u
s : Set α
f : α → Set β✝
g : Set (α → β✝)
β : Set α
γ : Set ↑β
⊢ Lean.Internal.coeM γ ⊆ β
[PROOFSTEP]
intro _ ⟨_, ⟨⟨⟨_, ha⟩, rfl⟩, _, ⟨_, rfl⟩, _⟩⟩
[GOAL]
α β✝ : Type u
s : Set α
f : α → Set β✝
g : Set (α → β✝)
β : Set α
γ : Set ↑β
a✝ val✝ : α
ha : val✝ ∈ β
h✝ : { val := val✝, property := ha } ∈ γ
right✝ : a✝ ∈ (fun h => (fun a => pure (CoeT.coe a)) { val := val✝, property := ha }) h✝
⊢ a✝ ∈ β
[PROOFSTEP]
convert ha
[GOAL]
α β✝ : Type u
s : Set α
f : α → Set β✝
g : Set (α → β✝)
β : Set α
γ : Set ↑β
a : α
ha : a ∈ Lean.Internal.coeM γ
⊢ { val := a, property := (_ : a ∈ β) } ∈ γ
[PROOFSTEP]
rcases ha with ⟨_, ⟨_, rfl⟩, _, ⟨ha, rfl⟩, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α β✝ : Type u
s : Set α
f : α → Set β✝
g : Set (α → β✝)
β : Set α
γ : Set ↑β
a : α
w✝ : ↑β
ha : w✝ ∈ γ
right✝ : a ∈ (fun h => (fun a => pure (CoeT.coe a)) w✝) ha
⊢ { val := a, property := (_ : a ∈ β) } ∈ γ
[PROOFSTEP]
convert ha
