[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : sSupHomClass F α β
f : F
g : ι → α
⊢ ↑f (⨆ (i : ι), g i) = ⨆ (i : ι), ↑f (g i)
[PROOFSTEP]
simp [iSup, ← Set.range_comp, Function.comp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : sSupHomClass F α β
f : F
g : (i : ι) → κ i → α
⊢ ↑f (⨆ (i : ι) (j : κ i), g i j) = ⨆ (i : ι) (j : κ i), ↑f (g i j)
[PROOFSTEP]
simp_rw [map_iSup]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : InfSet α
inst✝¹ : InfSet β
inst✝ : sInfHomClass F α β
f : F
g : ι → α
⊢ ↑f (⨅ (i : ι), g i) = ⨅ (i : ι), ↑f (g i)
[PROOFSTEP]
simp [iInf, ← Set.range_comp, Function.comp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : InfSet α
inst✝¹ : InfSet β
inst✝ : sInfHomClass F α β
f : F
g : (i : ι) → κ i → α
⊢ ↑f (⨅ (i : ι) (j : κ i), g i j) = ⨅ (i : ι) (j : κ i), ↑f (g i j)
[PROOFSTEP]
simp_rw [map_iInf]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
src✝ : sSupHomClass F α β := inst✝
f : F
a b : α
⊢ ↑f (a ⊔ b) = ↑f a ⊔ ↑f b
[PROOFSTEP]
rw [← sSup_pair, map_sSup]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
src✝ : sSupHomClass F α β := inst✝
f : F
a b : α
⊢ sSup (↑f '' {a, b}) = ↑f a ⊔ ↑f b
[PROOFSTEP]
simp only [Set.image_pair, sSup_insert, sSup_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
src✝ : sSupHomClass F α β := inst✝
f : F
⊢ ↑f ⊥ = ⊥
[PROOFSTEP]
rw [← sSup_empty, map_sSup, Set.image_empty]
  -- Porting note: rw [sSup_empty] does not work, but exact sSup_empty does?
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
src✝ : sSupHomClass F α β := inst✝
f : F
⊢ sSup ∅ = ⊥
[PROOFSTEP]
exact sSup_empty
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sInfHomClass F α β
src✝ : sInfHomClass F α β := inst✝
f : F
a b : α
⊢ ↑f (a ⊓ b) = ↑f a ⊓ ↑f b
[PROOFSTEP]
rw [← sInf_pair, map_sInf, Set.image_pair]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sInfHomClass F α β
src✝ : sInfHomClass F α β := inst✝
f : F
a b : α
⊢ sInf {↑f a, ↑f b} = ↑f a ⊓ ↑f b
[PROOFSTEP]
simp only [Set.image_pair, sInf_insert, sInf_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sInfHomClass F α β
src✝ : sInfHomClass F α β := inst✝
f : F
⊢ ↑f ⊤ = ⊤
[PROOFSTEP]
rw [← sInf_empty, map_sInf, Set.image_empty]
  -- Porting note: rw [sInf_empty] does not work, but exact sInf_empty does?
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sInfHomClass F α β
src✝ : sInfHomClass F α β := inst✝
f : F
⊢ sInf ∅ = ⊤
[PROOFSTEP]
exact sInf_empty
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : OrderIsoClass F α β
src✝ : OrderHomClass F α β :=
  let_fun this := inferInstance;
  this
f : F
s : Set α
c : (fun x => β) (sSup s)
⊢ ↑f (sSup s) ≤ c ↔ sSup (↑f '' s) ≤ c
[PROOFSTEP]
simp only [← le_map_inv_iff, sSup_le_iff, Set.ball_image_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : OrderIsoClass F α β
src✝ : OrderHomClass F α β :=
  let_fun this := inferInstance;
  this
f : F
s : Set α
c : (fun x => β) (sInf s)
⊢ c ≤ ↑f (sInf s) ↔ c ≤ sInf (↑f '' s)
[PROOFSTEP]
simp only [← map_inv_le_iff, le_sInf_iff, Set.ball_image_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
f g : sSupHom α β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
g : sSupHom α β
toFun✝ : α → β
map_sSup'✝ : ∀ (s : Set α), toFun✝ (sSup s) = sSup (toFun✝ '' s)
h : { toFun := toFun✝, map_sSup' := map_sSup'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_sSup' := map_sSup'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
toFun✝¹ : α → β
map_sSup'✝¹ : ∀ (s : Set α), toFun✝¹ (sSup s) = sSup (toFun✝¹ '' s)
toFun✝ : α → β
map_sSup'✝ : ∀ (s : Set α), toFun✝ (sSup s) = sSup (toFun✝ '' s)
h : { toFun := toFun✝¹, map_sSup' := map_sSup'✝¹ }.toFun = { toFun := toFun✝, map_sSup' := map_sSup'✝ }.toFun
⊢ { toFun := toFun✝¹, map_sSup' := map_sSup'✝¹ } = { toFun := toFun✝, map_sSup' := map_sSup'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
s : Set α
⊢ id (sSup s) = sSup (id '' s)
[PROOFSTEP]
rw [id, Set.image_id]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
f : sSupHom β γ
g : sSupHom α β
s : Set α
⊢ (↑f ∘ ↑g) (sSup s) = sSup (↑f ∘ ↑g '' s)
[PROOFSTEP]
rw [comp_apply, map_sSup, map_sSup, Set.image_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
f : sSupHom β γ
g : sSupHom α β
s : Set α
⊢ sSup ((fun x => ↑f (↑g x)) '' s) = sSup (↑f ∘ ↑g '' s)
[PROOFSTEP]
simp only [Function.comp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
g : sSupHom β γ
f₁ f₂ : sSupHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝ : SupSet α
x✝ : CompleteLattice β
s : Set α
⊢ (fun x => ⊥) (sSup s) = sSup ((fun x => ⊥) '' s)
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝ : SupSet α
x✝ : CompleteLattice β
⊢ (fun x => ⊥) (sSup ∅) = sSup ((fun x => ⊥) '' ∅)
[PROOFSTEP]
rw [Set.image_empty, sSup_empty]
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝ : SupSet α
x✝ : CompleteLattice β
s : Set α
hs : Set.Nonempty s
⊢ (fun x => ⊥) (sSup s) = sSup ((fun x => ⊥) '' s)
[PROOFSTEP]
rw [hs.image_const, sSup_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
f g : sInfHom α β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
g : sInfHom α β
toFun✝ : α → β
map_sInf'✝ : ∀ (s : Set α), toFun✝ (sInf s) = sInf (toFun✝ '' s)
h : { toFun := toFun✝, map_sInf' := map_sInf'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_sInf' := map_sInf'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
toFun✝¹ : α → β
map_sInf'✝¹ : ∀ (s : Set α), toFun✝¹ (sInf s) = sInf (toFun✝¹ '' s)
toFun✝ : α → β
map_sInf'✝ : ∀ (s : Set α), toFun✝ (sInf s) = sInf (toFun✝ '' s)
h : { toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ }.toFun = { toFun := toFun✝, map_sInf' := map_sInf'✝ }.toFun
⊢ { toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ } = { toFun := toFun✝, map_sInf' := map_sInf'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
s : Set α
⊢ id (sInf s) = sInf (id '' s)
[PROOFSTEP]
rw [id, Set.image_id]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
f : sInfHom β γ
g : sInfHom α β
s : Set α
⊢ (↑f ∘ ↑g) (sInf s) = sInf (↑f ∘ ↑g '' s)
[PROOFSTEP]
rw [comp_apply, map_sInf, map_sInf, Set.image_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
f : sInfHom β γ
g : sInfHom α β
s : Set α
⊢ sInf ((fun x => ↑f (↑g x)) '' s) = sInf (↑f ∘ ↑g '' s)
[PROOFSTEP]
simp only [Function.comp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
g : sInfHom β γ
f₁ f₂ : sInfHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : InfSet α
inst✝ : CompleteLattice β
s : Set α
⊢ (fun x => ⊤) (sInf s) = sInf ((fun x => ⊤) '' s)
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : InfSet α
inst✝ : CompleteLattice β
⊢ (fun x => ⊤) (sInf ∅) = sInf ((fun x => ⊤) '' ∅)
[PROOFSTEP]
rw [Set.image_empty, sInf_empty]
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : InfSet α
inst✝ : CompleteLattice β
s : Set α
hs : Set.Nonempty s
⊢ (fun x => ⊤) (sInf s) = sInf ((fun x => ⊤) '' s)
[PROOFSTEP]
rw [hs.image_const, sInf_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
f g : FrameHom α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
[GOAL]
case mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
g : FrameHom α β
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
map_top'✝ : InfHom.toFun { toFun := toFun✝, map_inf' := map_inf'✝ } ⊤ = ⊤
map_sSup'✝ :
  ∀ (s : Set α),
    InfHom.toFun { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ }.toInfHom (sSup s) =
      sSup ({ toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ }.toInfHom.toFun '' s)
h :
  (fun f => f.toFun)
      { toInfTopHom := { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ },
        map_sSup' := map_sSup'✝ } =
    (fun f => f.toFun) g
⊢ { toInfTopHom := { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ },
      map_sSup' := map_sSup'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
toFun✝¹ : α → β
map_inf'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊓ b) = toFun✝¹ a ⊓ toFun✝¹ b
map_top'✝¹ : InfHom.toFun { toFun := toFun✝¹, map_inf' := map_inf'✝¹ } ⊤ = ⊤
map_sSup'✝¹ :
  ∀ (s : Set α),
    InfHom.toFun { toInfHom := { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }, map_top' := map_top'✝¹ }.toInfHom
        (sSup s) =
      sSup ({ toInfHom := { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }, map_top' := map_top'✝¹ }.toInfHom.toFun '' s)
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
map_top'✝ : InfHom.toFun { toFun := toFun✝, map_inf' := map_inf'✝ } ⊤ = ⊤
map_sSup'✝ :
  ∀ (s : Set α),
    InfHom.toFun { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ }.toInfHom (sSup s) =
      sSup ({ toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ }.toInfHom.toFun '' s)
h :
  (fun f => f.toFun)
      { toInfTopHom := { toInfHom := { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }, map_top' := map_top'✝¹ },
        map_sSup' := map_sSup'✝¹ } =
    (fun f => f.toFun)
      { toInfTopHom := { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ },
        map_sSup' := map_sSup'✝ }
⊢ { toInfTopHom := { toInfHom := { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }, map_top' := map_top'✝¹ },
      map_sSup' := map_sSup'✝¹ } =
    { toInfTopHom := { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ },
      map_sSup' := map_sSup'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
g : FrameHom β γ
f₁ f₂ : FrameHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
f g : CompleteLatticeHom α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
g : CompleteLatticeHom α β
toFun✝ : α → β
map_sInf'✝ : ∀ (s : Set α), toFun✝ (sInf s) = sInf (toFun✝ '' s)
map_sSup'✝ :
  ∀ (s : Set α),
    sInfHom.toFun { toFun := toFun✝, map_sInf' := map_sInf'✝ } (sSup s) =
      sSup ({ toFun := toFun✝, map_sInf' := map_sInf'✝ }.toFun '' s)
h :
  (fun f => f.toFun) { tosInfHom := { toFun := toFun✝, map_sInf' := map_sInf'✝ }, map_sSup' := map_sSup'✝ } =
    (fun f => f.toFun) g
⊢ { tosInfHom := { toFun := toFun✝, map_sInf' := map_sInf'✝ }, map_sSup' := map_sSup'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
toFun✝¹ : α → β
map_sInf'✝¹ : ∀ (s : Set α), toFun✝¹ (sInf s) = sInf (toFun✝¹ '' s)
map_sSup'✝¹ :
  ∀ (s : Set α),
    sInfHom.toFun { toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ } (sSup s) =
      sSup ({ toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ }.toFun '' s)
toFun✝ : α → β
map_sInf'✝ : ∀ (s : Set α), toFun✝ (sInf s) = sInf (toFun✝ '' s)
map_sSup'✝ :
  ∀ (s : Set α),
    sInfHom.toFun { toFun := toFun✝, map_sInf' := map_sInf'✝ } (sSup s) =
      sSup ({ toFun := toFun✝, map_sInf' := map_sInf'✝ }.toFun '' s)
h :
  (fun f => f.toFun) { tosInfHom := { toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ }, map_sSup' := map_sSup'✝¹ } =
    (fun f => f.toFun) { tosInfHom := { toFun := toFun✝, map_sInf' := map_sInf'✝ }, map_sSup' := map_sSup'✝ }
⊢ { tosInfHom := { toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ }, map_sSup' := map_sSup'✝¹ } =
    { tosInfHom := { toFun := toFun✝, map_sInf' := map_sInf'✝ }, map_sSup' := map_sSup'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
g : CompleteLatticeHom β γ
f₁ f₂ : CompleteLatticeHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set β)
⊢ ⋂ (t : Set β) (_ : t ∈ s), f ⁻¹' t = sInf (preimage f '' s)
[PROOFSTEP]
simp only [Set.sInf_eq_sInter, Set.sInter_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set β)
⊢ ⋃ (t : Set β) (_ : t ∈ s), (fun x => f x) ⁻¹' t =
    sSup
      ({ toFun := preimage f, map_sInf' := (_ : ∀ (s : Set (Set β)), f ⁻¹' ⋂₀ s = sInf (preimage f '' s)) }.toFun '' s)
[PROOFSTEP]
simp only [Set.sSup_eq_sUnion, Set.sUnion_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
⊢ f '' sSup s = sSup (image f '' s)
[PROOFSTEP]
ext b
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
b : β
⊢ b ∈ f '' sSup s ↔ b ∈ sSup (image f '' s)
[PROOFSTEP]
simp only [sSup_eq_sUnion, mem_image, mem_sUnion, exists_prop, sUnion_image, mem_iUnion]
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
b : β
⊢ (∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = b) ↔ ∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = b
[PROOFSTEP]
constructor
[GOAL]
case h.mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
b : β
⊢ (∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = b) → ∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = b
[PROOFSTEP]
rintro ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
a : α
t : Set α
ht₁ : t ∈ s
ht₂ : a ∈ t
⊢ ∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = f a
[PROOFSTEP]
exact ⟨t, ht₁, a, ht₂, rfl⟩
[GOAL]
case h.mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
b : β
⊢ (∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = b) → ∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = b
[PROOFSTEP]
rintro ⟨t, ht₁, a, ht₂, rfl⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
t : Set α
ht₁ : t ∈ s
a : α
ht₂ : a ∈ t
⊢ ∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = f a
[PROOFSTEP]
exact ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
e : α ≃ β
s : Set α
⊢ (fun s => ↑e.symm '' s) ((fun s => ↑e '' s) s) = s
[PROOFSTEP]
simp only [← image_comp, Equiv.symm_comp_self, id.def, image_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
e : α ≃ β
s : Set β
⊢ (fun s => ↑e '' s) ((fun s => ↑e.symm '' s) s) = s
[PROOFSTEP]
simp only [← image_comp, Equiv.self_comp_symm, id.def, image_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
e : α ≃ β
a✝ b✝ : Set α
h :
  ↑{ toFun := fun s => ↑e '' s, invFun := fun s => ↑e.symm '' s,
          left_inv := (_ : ∀ (s : Set α), ↑e.symm '' (fun s => ↑e '' s) s = s),
          right_inv := (_ : ∀ (s : Set β), ↑e '' (fun s => ↑e.symm '' s) s = s) }
      a✝ ≤
    ↑{ toFun := fun s => ↑e '' s, invFun := fun s => ↑e.symm '' s,
          left_inv := (_ : ∀ (s : Set α), ↑e.symm '' (fun s => ↑e '' s) s = s),
          right_inv := (_ : ∀ (s : Set β), ↑e '' (fun s => ↑e.symm '' s) s = s) }
      b✝
⊢ a✝ ≤ b✝
[PROOFSTEP]
simpa using @monotone_image _ _ e.symm _ _ h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝ : CompleteLattice α
x : α × α
s : Set (α × α)
⊢ (fun x => x.fst ⊔ x.snd) (sSup s) = sSup ((fun x => x.fst ⊔ x.snd) '' s)
[PROOFSTEP]
simp_rw [Prod.fst_sSup, Prod.snd_sSup, sSup_image, iSup_sup_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝ : CompleteLattice α
x : α × α
s : Set (α × α)
⊢ (fun x => x.fst ⊓ x.snd) (sInf s) = sInf ((fun x => x.fst ⊓ x.snd) '' s)
[PROOFSTEP]
simp_rw [Prod.fst_sInf, Prod.snd_sInf, sInf_image, iInf_inf_eq]
