case a.h
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ ↑(lowerClosure (s ⊼ t)) ↔ a ∈ ↑(lowerClosure s ⊓ lowerClosure t)
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
⊢ lowerClosure (s ⊼ t) = lowerClosure s ⊓ lowerClosure t
ext a
case a.h
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_1) ∧ a ≤ a_1) ↔ a ∈ lowerClosure s ⊓ lowerClosure t
case a.h
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ ↑(lowerClosure (s ⊼ t)) ↔ a ∈ ↑(lowerClosure s ⊓ lowerClosure t)
simp only [SetLike.mem_coe, mem_lowerClosure, Set.mem_infs, exists_and_left, exists_prop,
  LowerSet.coe_sup, Set.mem_inter_iff]
case a.h.mp
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_1) ∧ a ≤ a_1) → a ∈ lowerClosure s ⊓ lowerClosure t

case a.h.mpr
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ lowerClosure s ⊓ lowerClosure t → ∃ a_2, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_2) ∧ a ≤ a_2
case a.h
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_1) ∧ a ≤ a_1) ↔ a ∈ lowerClosure s ⊓ lowerClosure t
constructor
case a.h.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : a ≤ b ⊓ c
⊢ a ∈ lowerClosure s ⊓ lowerClosure t
case a.h.mp
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_1) ∧ a ≤ a_1) → a ∈ lowerClosure s ⊓ lowerClosure t
rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩
no goals
case a.h.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : a ≤ b ⊓ c
⊢ a ∈ lowerClosure s ⊓ lowerClosure t
exact ⟨⟨b, hb, ha.trans inf_le_left⟩, c, hc, ha.trans inf_le_right⟩
case a.h.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
hab : a ≤ b
c : α
hc : c ∈ t
hac : a ≤ c
⊢ ∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_1) ∧ a ≤ a_1
case a.h.mpr
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ lowerClosure s ⊓ lowerClosure t → ∃ a_2, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_2) ∧ a ≤ a_2
rintro ⟨⟨b, hb, hab⟩, c, hc, hac⟩
no goals
case a.h.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : SemilatticeInf α
s t : Set α
a b : α
hb : b ∈ s
hab : a ≤ b
c : α
hc : c ∈ t
hac : a ≤ c
⊢ ∃ a_1, (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ a ⊓ b = a_1) ∧ a ≤ a_1
exact ⟨_, ⟨b, hb, c, hc, rfl⟩, le_inf hab hac⟩