case intro
F : Type ?u.128418
α : Type u_1
β : Type u_2
γ : Type ?u.128427
δ : Type ?u.128430
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
f : α ≃o β
inst✝ : ComplementedLattice α
x : β
y : α
hy : IsCompl (↑(symm f) x) y
⊢ ∃ b, IsCompl x b
F : Type ?u.128418
α : Type u_1
β : Type u_2
γ : Type ?u.128427
δ : Type ?u.128430
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
f : α ≃o β
inst✝ : ComplementedLattice α
x : β
⊢ ∃ b, IsCompl x b
obtain ⟨y, hy⟩ := exists_isCompl (f.symm x)
case intro
F : Type ?u.128418
α : Type u_1
β : Type u_2
γ : Type ?u.128427
δ : Type ?u.128430
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
f : α ≃o β
inst✝ : ComplementedLattice α
x : β
y : α
hy : IsCompl (↑(symm f) x) (↑(symm f) (↑f y))
⊢ ∃ b, IsCompl x b
case intro
F : Type ?u.128418
α : Type u_1
β : Type u_2
γ : Type ?u.128427
δ : Type ?u.128430
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
f : α ≃o β
inst✝ : ComplementedLattice α
x : β
y : α
hy : IsCompl (↑(symm f) x) y
⊢ ∃ b, IsCompl x b
rw [← f.symm_apply_apply y] at hy
no goals
case intro
F : Type ?u.128418
α : Type u_1
β : Type u_2
γ : Type ?u.128427
δ : Type ?u.128430
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
f : α ≃o β
inst✝ : ComplementedLattice α
x : β
y : α
hy : IsCompl (↑(symm f) x) (↑(symm f) (↑f y))
⊢ ∃ b, IsCompl x b
exact ⟨f y, f.symm.isCompl_iff.2 hy⟩