-- Mathlib/Order/LiminfLimsup.lean
theorem OrderIso.limsup_apply {γ} [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ]
    {f : Filter α} {u : α → β} (g : β ≃o γ)
    (hu : f.IsBoundedUnder (· ≤ ·) u

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hf : u = fun i => g.symm (g (u i))
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g.symm (g (u x))

Tactic:
simp_rw [g.symm_apply_apply]

Result:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hf : u = fun i => g.symm (g (u i))
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => u x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
⊢ g (limsup u f) = limsup (fun x => g (u x)) f

Tactic:
refine le_antisymm ((OrderIso.to_galoisConnection g).l_limsup_le hgu hu_co) ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
⊢ limsup (fun x => g (u x)) f ≤ g (limsup u f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hf : u = fun i => g.symm (g (u i))
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => u x

Tactic:
exact hu

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
⊢ g.symm (limsup (fun x => g (u x)) f) ≤ limsup u f

Tactic:
have hf : u = fun i => g.symm (g (u i)) := funext fun i => (g.symm_apply_apply (u i)).symm

Result:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hf : u = fun i => g.symm (g (u i))
⊢ g.symm (limsup (fun x => g (u x)) f) ≤ limsup u f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
⊢ g (g.symm (limsup (fun x => g (u x)) f)) ≤ g (limsup u f)

Tactic:
refine g.monotone ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
⊢ g.symm (limsup (fun x => g (u x)) f) ≤ limsup u f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
⊢ limsup (fun x => g (u x)) f ≤ g (limsup u f)

Tactic:
rw [← g.symm.symm_apply_apply <| limsup (fun x => g (u x)) f, g.symm_symm]

Result:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
⊢ g (g.symm (limsup (fun x => g (u x)) f)) ≤ g (limsup u f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hf : u = fun i => g.symm (g (u i))
⊢ g.symm (limsup (fun x => g (u x)) f) ≤ limsup u f

Tactic:
nth_rw 2 [hf]

Result:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x)) _auto✝
hf : u = fun i => g.symm (g (u i))
⊢ g.symm (limsup (fun x => g (u x)) f) ≤ limsup (fun i => g.symm (g (u i))) f