case refine'_1
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Sort ?u.273159
ι' : Sort ?u.273162
ι₂ : Sort ?u.273165
κ : ι → Sort ?u.273170
κ₁ : ι → Sort ?u.273175
κ₂ : ι → Sort ?u.273180
κ' : ι' → Sort ?u.273185
s : Set (β → γ)
t : Set (α → β)
u : Set α
c : γ
⊢ c ∈ seq s (seq t u) → c ∈ seq (seq ((fun x x_1 => x ∘ x_1) '' s) t) u

case refine'_2
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Sort ?u.273159
ι' : Sort ?u.273162
ι₂ : Sort ?u.273165
κ : ι → Sort ?u.273170
κ₁ : ι → Sort ?u.273175
κ₂ : ι → Sort ?u.273180
κ' : ι' → Sort ?u.273185
s : Set (β → γ)
t : Set (α → β)
u : Set α
c : γ
⊢ c ∈ seq (seq ((fun x x_1 => x ∘ x_1) '' s) t) u → c ∈ seq s (seq t u)
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Sort ?u.273159
ι' : Sort ?u.273162
ι₂ : Sort ?u.273165
κ : ι → Sort ?u.273170
κ₁ : ι → Sort ?u.273175
κ₂ : ι → Sort ?u.273180
κ' : ι' → Sort ?u.273185
s : Set (β → γ)
t : Set (α → β)
u : Set α
⊢ seq s (seq t u) = seq (seq ((fun x x_1 => x ∘ x_1) '' s) t) u
refine' Set.ext fun c => Iff.intro _ _
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Sort ?u.273159
ι' : Sort ?u.273162
ι₂ : Sort ?u.273165
κ : ι → Sort ?u.273170
κ₁ : ι → Sort ?u.273175
κ₂ : ι → Sort ?u.273180
κ' : ι' → Sort ?u.273185
s : Set (β → γ)
t : Set (α → β)
u : Set α
f : β → γ
hfs : f ∈ s
g : α → β
hg : g ∈ t
a : α
hau : a ∈ u
⊢ f (g a) ∈ seq (seq ((fun x x_1 => x ∘ x_1) '' s) t) u
case refine'_1
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Sort ?u.273159
ι' : Sort ?u.273162
ι₂ : Sort ?u.273165
κ : ι → Sort ?u.273170
κ₁ : ι → Sort ?u.273175
κ₂ : ι → Sort ?u.273180
κ' : ι' → Sort ?u.273185
s : Set (β → γ)
t : Set (α → β)
u : Set α
c : γ
⊢ c ∈ seq s (seq t u) → c ∈ seq (seq ((fun x x_1 => x ∘ x_1) '' s) t) u
rintro ⟨f, hfs, b, ⟨g, hg, a, hau, rfl⟩, rfl⟩
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Sort ?u.273159
ι' : Sort ?u.273162
ι₂ : Sort ?u.273165
κ : ι → Sort ?u.273170
κ₁ : ι → Sort ?u.273175
κ₂ : ι → Sort ?u.273180
κ' : ι' → Sort ?u.273185
s : Set (β → γ)
t : Set (α → β)
u : Set α
f : β → γ
hfs : f ∈ s
g : α → β
hgt : g ∈ t
a : α
ha : a ∈ u
⊢ (fun x x_1 => x ∘ x_1) f g a ∈ seq s (seq t u)
case refine'_2
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Sort ?u.273159
ι' : Sort ?u.273162
ι₂ : Sort ?u.273165
κ : ι → Sort ?u.273170
κ₁ : ι → Sort ?u.273175
κ₂ : ι → Sort ?u.273180
κ' : ι' → Sort ?u.273185
s : Set (β → γ)
t : Set (α → β)
u : Set α
c : γ
⊢ c ∈ seq (seq ((fun x x_1 => x ∘ x_1) '' s) t) u → c ∈ seq s (seq t u)
rintro ⟨fg, ⟨fc, ⟨f, hfs, rfl⟩, g, hgt, rfl⟩, a, ha, rfl⟩
no goals
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Sort ?u.273159
ι' : Sort ?u.273162
ι₂ : Sort ?u.273165
κ : ι → Sort ?u.273170
κ₁ : ι → Sort ?u.273175
κ₂ : ι → Sort ?u.273180
κ' : ι' → Sort ?u.273185
s : Set (β → γ)
t : Set (α → β)
u : Set α
f : β → γ
hfs : f ∈ s
g : α → β
hgt : g ∈ t
a : α
ha : a ∈ u
⊢ (fun x x_1 => x ∘ x_1) f g a ∈ seq s (seq t u)
exact ⟨f, hfs, g a, ⟨g, hgt, a, ha, rfl⟩, rfl⟩