Theorem: Sublattice.pi_univ_eq_bot (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)
L : (i : κ) → Sublattice (π i)
⊢ pi univ L = ⊥ ↔ ∃ i, L i = ⊥
Tactic:
simp_rw [← coe_inj]
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)
L : (i : κ) → Sublattice (π i)
⊢ ↑(pi univ L) = ↑⊥ ↔ ∃ 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)
L : (i : κ) → Sublattice (π i)
⊢ ↑(pi univ L) = ↑⊥ ↔ ∃ i, ↑(L i) = ↑⊥
Tactic:
simp
State after:
no goals