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

State before:
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
s✝ t✝ : Set α
a b : α
s : Set α
t : Set β
⊢ infClosure s ×ˢ infClosure t ≤ infClosure (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✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
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.inf' hu id, v.inf' hv id) ∈ infClosure (s ×ˢ t)

State before:
case mk.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
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.inf' hu id, v.inf' hv id) ∈ infClosure (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✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
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✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
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).inf' ⋯ id = (u.inf' hu id, v.inf' hv id)

State before:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
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✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
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).inf' ⋯ id = (u.inf' hu id, v.inf' hv id)
Tactic:
simp [prodMk_inf'_inf']
State after:
no goals