case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type ?u.23
β : Type u_2
β' : Type ?u.29
γ : Type ?u.32
E : Type ?u.35
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ C
ht₁ : t₁ ∈ D
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ C
ht₂ : t₂ ∈ D
hst : Set.Nonempty ((fun x x_1 => x ×ˢ x_1) s₁ t₁ ∩ (fun x x_1 => x ×ˢ x_1) s₂ t₂)
⊢ (fun x x_1 => x ×ˢ x_1) s₁ t₁ ∩ (fun x x_1 => x ×ˢ x_1) s₂ t₂ ∈ image2 (fun x x_1 => x ×ˢ x_1) C D
α : Type u_1
α' : Type ?u.23
β : Type u_2
β' : Type ?u.29
γ : Type ?u.32
E : Type ?u.35
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
⊢ IsPiSystem (image2 (fun x x_1 => x ×ˢ x_1) C D)
rintro _ ⟨s₁, t₁, hs₁, ht₁, rfl⟩ _ ⟨s₂, t₂, hs₂, ht₂, rfl⟩ hst
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type ?u.23
β : Type u_2
β' : Type ?u.29
γ : Type ?u.32
E : Type ?u.35
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ C
ht₁ : t₁ ∈ D
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ C
ht₂ : t₂ ∈ D
hst : Set.Nonempty ((s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂))
⊢ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) ∈ image2 (fun x x_1 => x ×ˢ x_1) C D
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type ?u.23
β : Type u_2
β' : Type ?u.29
γ : Type ?u.32
E : Type ?u.35
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ C
ht₁ : t₁ ∈ D
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ C
ht₂ : t₂ ∈ D
hst : Set.Nonempty ((fun x x_1 => x ×ˢ x_1) s₁ t₁ ∩ (fun x x_1 => x ×ˢ x_1) s₂ t₂)
⊢ (fun x x_1 => x ×ˢ x_1) s₁ t₁ ∩ (fun x x_1 => x ×ˢ x_1) s₂ t₂ ∈ image2 (fun x x_1 => x ×ˢ x_1) C D
rw [prod_inter_prod] at hst ⊢
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type ?u.23
β : Type u_2
β' : Type ?u.29
γ : Type ?u.32
E : Type ?u.35
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ C
ht₁ : t₁ ∈ D
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ C
ht₂ : t₂ ∈ D
hst : Set.Nonempty (s₁ ∩ s₂) ∧ Set.Nonempty (t₁ ∩ t₂)
⊢ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) ∈ image2 (fun x x_1 => x ×ˢ x_1) C D
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type ?u.23
β : Type u_2
β' : Type ?u.29
γ : Type ?u.32
E : Type ?u.35
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ C
ht₁ : t₁ ∈ D
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ C
ht₂ : t₂ ∈ D
hst : Set.Nonempty ((s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂))
⊢ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) ∈ image2 (fun x x_1 => x ×ˢ x_1) C D
rw [prod_nonempty_iff] at hst
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type ?u.23
β : Type u_2
β' : Type ?u.29
γ : Type ?u.32
E : Type ?u.35
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ C
ht₁ : t₁ ∈ D
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ C
ht₂ : t₂ ∈ D
hst : Set.Nonempty (s₁ ∩ s₂) ∧ Set.Nonempty (t₁ ∩ t₂)
⊢ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) ∈ image2 (fun x x_1 => x ×ˢ x_1) C D
exact mem_image2_of_mem (hC _ hs₁ _ hs₂ hst.1) (hD _ ht₁ _ ht₂ hst.2)