Theorem: supClosure_prod (LeanCamCombi/Mathlib/Order/SupClosed.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
⊢ supClosure s ×ˢ supClosure t ≤ supClosure (s ×ˢ t)
Tactic:
rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩
State after:
case mk.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u.sup' hu id, v.sup' hv id) ∈ supClosure (s ×ˢ t)

State before:
case mk.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u.sup' hu id, v.sup' hv id) ∈ supClosure (s ×ˢ t)
Tactic:
refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
State after:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑(u ×ˢ v) ⊆ s ×ˢ t

case mk.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u ×ˢ v).sup' ⋯ id = (u.sup' hu id, v.sup' hv id)

State before:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑(u ×ˢ v) ⊆ s ×ˢ t
Tactic:
simpa only [coe_product] using Set.prod_mono hus hvt
State after:
no goals

State before:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u ×ˢ v).sup' ⋯ id = (u.sup' hu id, v.sup' hv id)
Tactic:
simp [prodMk_sup'_sup']
State after:
no goals