α : Type ?u.62585
β : Type ?u.62588
γ : Type ?u.62591
δ : Type ?u.62594
ι : Sort ?u.62597
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ s ∈ Filter.coprod (map m₁ f₁) (map m₂ f₂) → s ∈ map (Prod.map m₁ m₂) (Filter.coprod f₁ f₂)
α : Type ?u.62585
β : Type ?u.62588
γ : Type ?u.62591
δ : Type ?u.62594
ι : Sort ?u.62597
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
⊢ map (Prod.map m₁ m₂) (Filter.coprod f₁ f₂) ≤ Filter.coprod (map m₁ f₁) (map m₂ f₂)
intro s
α : Type ?u.62585
β : Type ?u.62588
γ : Type ?u.62591
δ : Type ?u.62594
ι : Sort ?u.62597
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ ((∃ t₁, m₁ ⁻¹' t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂, m₂ ⁻¹' t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ s) →
    (∃ t₁, t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂, t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s
α : Type ?u.62585
β : Type ?u.62588
γ : Type ?u.62591
δ : Type ?u.62594
ι : Sort ?u.62597
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ s ∈ Filter.coprod (map m₁ f₁) (map m₂ f₂) → s ∈ map (Prod.map m₁ m₂) (Filter.coprod f₁ f₂)
simp only [mem_map, mem_coprod_iff]
case intro.intro.intro.intro.intro
α : Type ?u.62585
β : Type ?u.62588
γ : Type ?u.62591
δ : Type ?u.62594
ι : Sort ?u.62597
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
⊢ (∃ t₁, t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂, t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s
α : Type ?u.62585
β : Type ?u.62588
γ : Type ?u.62591
δ : Type ?u.62594
ι : Sort ?u.62597
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ ((∃ t₁, m₁ ⁻¹' t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂, m₂ ⁻¹' t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ s) →
    (∃ t₁, t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂, t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s
rintro ⟨⟨u₁, hu₁, h₁⟩, u₂, hu₂, h₂⟩
no goals
case intro.intro.intro.intro.intro
α : Type ?u.62585
β : Type ?u.62588
γ : Type ?u.62591
δ : Type ?u.62594
ι : Sort ?u.62597
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
⊢ (∃ t₁, t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂, t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s
refine' ⟨⟨m₁ ⁻¹' u₁, hu₁, fun _ hx => h₁ _⟩, ⟨m₂ ⁻¹' u₂, hu₂, fun _ hx => h₂ _⟩⟩ <;> convert hx