Theorem: Sublattice.le_pi (LeanCamCombi/Mathlib/Order/Sublattice.lean)

State before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
L✝ M✝ : Sublattice α
f : LatticeHom α β
s✝ t : Set α
a : α
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ M ≤ pi s L ↔ ∀ i ∈ s, M ≤ comap (Pi.evalLatticeHom π i) (L i)
Tactic:
simp [SetLike.le_def]
State after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
L✝ M✝ : Sublattice α
f : LatticeHom α β
s✝ t : Set α
a : α
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ (∀ ⦃x : (i : κ) → π i⦄, x ∈ M → ∀ i ∈ s, x i ∈ L i) ↔ ∀ i ∈ s, ∀ ⦃x : (i : κ) → π i⦄, x ∈ M → x i ∈ L i

State before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
L✝ M✝ : Sublattice α
f : LatticeHom α β
s✝ t : Set α
a : α
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ (∀ ⦃x : (i : κ) → π i⦄, x ∈ M → ∀ i ∈ s, x i ∈ L i) ↔ ∀ i ∈ s, ∀ ⦃x : (i : κ) → π i⦄, x ∈ M → x i ∈ L i
Tactic:
aesop
State after:
no goals