case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Sort ?u.7054
ι' : Sort ?u.7057
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, Set.Nonempty (Ixx a b) → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)
s t : Set α
l₁ : α
hls₁ : l₁ ∈ s
u₁ : α
hut₁ : u₁ ∈ t
left✝¹ : p l₁ u₁
l₂ : α
hls₂ : l₂ ∈ s
u₂ : α
hut₂ : u₂ ∈ t
left✝ : p l₂ u₂
⊢ Set.Nonempty (Ixx l₁ u₁ ∩ Ixx l₂ u₂) → Ixx l₁ u₁ ∩ Ixx l₂ u₂ ∈ {S | ∃ l, l ∈ s ∧ ∃ u, u ∈ t ∧ p l u ∧ Ixx l u = S}
α : Type u_1
ι : Sort ?u.7054
ι' : Sort ?u.7057
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, Set.Nonempty (Ixx a b) → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)
s t : Set α
⊢ IsPiSystem {S | ∃ l, l ∈ s ∧ ∃ u, u ∈ t ∧ p l u ∧ Ixx l u = S}
rintro _ ⟨l₁, hls₁, u₁, hut₁, _, rfl⟩ _ ⟨l₂, hls₂, u₂, hut₂, _, rfl⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Sort ?u.7054
ι' : Sort ?u.7057
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, Set.Nonempty (Ixx a b) → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)
s t : Set α
l₁ : α
hls₁ : l₁ ∈ s
u₁ : α
hut₁ : u₁ ∈ t
left✝¹ : p l₁ u₁
l₂ : α
hls₂ : l₂ ∈ s
u₂ : α
hut₂ : u₂ ∈ t
left✝ : p l₂ u₂
⊢ Set.Nonempty (Ixx (max l₁ l₂) (min u₁ u₂)) →
    Ixx (max l₁ l₂) (min u₁ u₂) ∈ {S | ∃ l, l ∈ s ∧ ∃ u, u ∈ t ∧ p l u ∧ Ixx l u = S}
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Sort ?u.7054
ι' : Sort ?u.7057
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, Set.Nonempty (Ixx a b) → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)
s t : Set α
l₁ : α
hls₁ : l₁ ∈ s
u₁ : α
hut₁ : u₁ ∈ t
left✝¹ : p l₁ u₁
l₂ : α
hls₂ : l₂ ∈ s
u₂ : α
hut₂ : u₂ ∈ t
left✝ : p l₂ u₂
⊢ Set.Nonempty (Ixx l₁ u₁ ∩ Ixx l₂ u₂) → Ixx l₁ u₁ ∩ Ixx l₂ u₂ ∈ {S | ∃ l, l ∈ s ∧ ∃ u, u ∈ t ∧ p l u ∧ Ixx l u = S}
simp only [Hi]
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Sort ?u.7054
ι' : Sort ?u.7057
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, Set.Nonempty (Ixx a b) → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)
s t : Set α
l₁ : α
hls₁ : l₁ ∈ s
u₁ : α
hut₁ : u₁ ∈ t
left✝¹ : p l₁ u₁
l₂ : α
hls₂ : l₂ ∈ s
u₂ : α
hut₂ : u₂ ∈ t
left✝ : p l₂ u₂
⊢ Set.Nonempty (Ixx (max l₁ l₂) (min u₁ u₂)) →
    Ixx (max l₁ l₂) (min u₁ u₂) ∈ {S | ∃ l, l ∈ s ∧ ∃ u, u ∈ t ∧ p l u ∧ Ixx l u = S}
exact fun H => ⟨l₁ ⊔ l₂, sup_ind l₁ l₂ hls₁ hls₂, u₁ ⊓ u₂, inf_ind u₁ u₂ hut₁ hut₂, Hne H, rfl⟩