[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : HeytingAlgebra α
x✝ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
src✝ : HeytingHomClass F α β := inst✝
f : F
⊢ ↑f ⊤ = ⊤
[PROOFSTEP]
rw [← @himp_self α _ ⊥, ← himp_self, map_himp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
src✝ : CoheytingHomClass F α β := inst✝
f : F
⊢ ↑f ⊥ = ⊥
[PROOFSTEP]
rw [← @sdiff_self α _ ⊤, ← sdiff_self, map_sdiff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : BiheytingHomClass F α β
src✝ : BiheytingHomClass F α β := inst✝
f : F
⊢ ↑f ⊥ = ⊥
[PROOFSTEP]
rw [← @sdiff_self α _ ⊤, ← sdiff_self, BiheytingHomClass.map_sdiff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : BiheytingHomClass F α β
src✝ : BiheytingHomClass F α β := inst✝
f : F
⊢ ↑f ⊤ = ⊤
[PROOFSTEP]
rw [← @himp_self α _ ⊥, ← himp_self, map_himp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : HeytingAlgebra α
x✝ : HeytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : BoundedLatticeHomClass F α β := toBoundedLatticeHomClass
f : F
a b : α
c : (fun x => β) (a ⇨ b)
⊢ c ≤ ↑f (a ⇨ b) ↔ c ≤ ↑f a ⇨ ↑f b
[PROOFSTEP]
simp only [← map_inv_le_iff, le_himp_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : HeytingAlgebra α
x✝ : HeytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : BoundedLatticeHomClass F α β := toBoundedLatticeHomClass
f : F
a b : α
c : (fun x => β) (a ⇨ b)
⊢ EquivLike.inv f c ⊓ a ≤ b ↔ EquivLike.inv f (c ⊓ ↑f a) ≤ b
[PROOFSTEP]
rw [← OrderIsoClass.map_le_map_iff f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : HeytingAlgebra α
x✝ : HeytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : BoundedLatticeHomClass F α β := toBoundedLatticeHomClass
f : F
a b : α
c : (fun x => β) (a ⇨ b)
⊢ ↑f (EquivLike.inv f c ⊓ a) ≤ ↑f b ↔ EquivLike.inv f (c ⊓ ↑f a) ≤ b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : BoundedLatticeHomClass F α β := toBoundedLatticeHomClass
f : F
a b : α
c : (fun x => β) (a \ b)
⊢ ↑f (a \ b) ≤ c ↔ ↑f a \ ↑f b ≤ c
[PROOFSTEP]
simp only [← le_map_inv_iff, sdiff_le_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : BoundedLatticeHomClass F α β := toBoundedLatticeHomClass
f : F
a b : α
c : (fun x => β) (a \ b)
⊢ a ≤ b ⊔ EquivLike.inv f c ↔ a ≤ EquivLike.inv f (↑f b ⊔ c)
[PROOFSTEP]
rw [← OrderIsoClass.map_le_map_iff f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : BoundedLatticeHomClass F α β := toBoundedLatticeHomClass
f : F
a b : α
c : (fun x => β) (a \ b)
⊢ ↑f a ≤ ↑f (b ⊔ EquivLike.inv f c) ↔ a ≤ EquivLike.inv f (↑f b ⊔ c)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : LatticeHomClass F α β := toLatticeHomClass
f : F
a b : α
c : (fun x => β) (a ⇨ b)
⊢ c ≤ ↑f (a ⇨ b) ↔ c ≤ ↑f a ⇨ ↑f b
[PROOFSTEP]
simp only [← map_inv_le_iff, le_himp_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : LatticeHomClass F α β := toLatticeHomClass
f : F
a b : α
c : (fun x => β) (a ⇨ b)
⊢ EquivLike.inv f c ⊓ a ≤ b ↔ EquivLike.inv f (c ⊓ ↑f a) ≤ b
[PROOFSTEP]
rw [← OrderIsoClass.map_le_map_iff f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : LatticeHomClass F α β := toLatticeHomClass
f : F
a b : α
c : (fun x => β) (a ⇨ b)
⊢ ↑f (EquivLike.inv f c ⊓ a) ≤ ↑f b ↔ EquivLike.inv f (c ⊓ ↑f a) ≤ b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : LatticeHomClass F α β := toLatticeHomClass
f : F
a b : α
c : (fun x => β) (a \ b)
⊢ ↑f (a \ b) ≤ c ↔ ↑f a \ ↑f b ≤ c
[PROOFSTEP]
simp only [← le_map_inv_iff, sdiff_le_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : LatticeHomClass F α β := toLatticeHomClass
f : F
a b : α
c : (fun x => β) (a \ b)
⊢ a ≤ b ⊔ EquivLike.inv f c ↔ a ≤ EquivLike.inv f (↑f b ⊔ c)
[PROOFSTEP]
rw [← OrderIsoClass.map_le_map_iff f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
src✝ : LatticeHomClass F α β := toLatticeHomClass
f : F
a b : α
c : (fun x => β) (a \ b)
⊢ ↑f a ≤ ↑f (b ⊔ EquivLike.inv f c) ↔ a ≤ EquivLike.inv f (↑f b ⊔ c)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
src✝ : BoundedLatticeHomClass F α β := inst✝
f : F
a b : α
⊢ ↑f (a ⇨ b) = ↑f a ⇨ ↑f b
[PROOFSTEP]
rw [himp_eq, himp_eq, map_sup, (isCompl_compl.map _).compl_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
src✝ : BoundedLatticeHomClass F α β := inst✝
f : F
a b : α
⊢ ↑f (a \ b) = ↑f a \ ↑f b
[PROOFSTEP]
rw [sdiff_eq, sdiff_eq, map_inf, (isCompl_compl.map _).compl_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a : α
⊢ ↑f aᶜ = (↑f a)ᶜ
[PROOFSTEP]
rw [← himp_bot, ← himp_bot, map_himp, map_bot]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a b : α
⊢ ↑f (a ⇔ b) = ↑f a ⇔ ↑f b
[PROOFSTEP]
simp_rw [bihimp, map_inf, map_himp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a : α
⊢ ↑f (￢a) = ￢↑f a
[PROOFSTEP]
rw [← top_sdiff', ← top_sdiff', map_sdiff, map_top]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a b : α
⊢ ↑f (a ∆ b) = ↑f a ∆ ↑f b
[PROOFSTEP]
simp_rw [symmDiff, map_sup, map_sdiff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f g : HeytingHom α β
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
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
g : HeytingHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
map_bot'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊥ = ⊥
map_himp'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a ⇨ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a ⇨
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_bot' := map_bot'✝, map_himp' := map_himp'✝ } =
    (fun f => f.toFun) g
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_bot' := map_bot'✝, map_himp' := map_himp'✝ } =
    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
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_inf'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } a ⊓
        SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } b
map_bot'✝¹ :
  SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom ⊥ = ⊥
map_himp'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom (a ⇨ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom a ⇨
        SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
map_bot'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊥ = ⊥
map_himp'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a ⇨ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a ⇨
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
        map_bot' := map_bot'✝¹, map_himp' := map_himp'✝¹ } =
    (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_bot' := map_bot'✝, map_himp' := map_himp'✝ }
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
      map_bot' := map_bot'✝¹, map_himp' := map_himp'✝¹ } =
    { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_bot' := map_bot'✝, map_himp' := map_himp'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b
[PROOFSTEP]
simpa only [h] using map_sup f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } b
[PROOFSTEP]
simpa only [h] using map_inf f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ↑f
⊢ SupHom.toFun
      { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                  SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } b) }.toSupHom
      ⊥ =
    ⊥
[PROOFSTEP]
simpa only [h] using map_bot f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun
        { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                        b) }.toSupHom
        (a ⇨ b) =
      SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          a ⇨
        SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          b
[PROOFSTEP]
simpa only [h] using map_himp f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom β γ
g : HeytingHom α β
src✝ : LatticeHom α γ := LatticeHom.comp f.toLatticeHom g.toLatticeHom
⊢ SupHom.toFun
      {
          toSupHom :=
            { toFun := ↑f ∘ ↑g,
              map_sup' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun src✝.toSupHom (a ⊔ b) = SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun src✝.toSupHom (a ⊓ b) =
                  SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
      ⊥ =
    ⊥
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom β γ
g : HeytingHom α β
src✝ : LatticeHom α γ := LatticeHom.comp f.toLatticeHom g.toLatticeHom
a b : α
⊢ SupHom.toFun
      {
          toSupHom :=
            { toFun := ↑f ∘ ↑g,
              map_sup' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun src✝.toSupHom (a ⊔ b) = SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun src✝.toSupHom (a ⊓ b) =
                  SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
      (a ⇨ b) =
    SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        a ⇨
      SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f f₁ f₂ : HeytingHom α β
g g₁ g₂ : HeytingHom β γ
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
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f g : CoheytingHom α β
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
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
g : CoheytingHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
map_top'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊤ = ⊤
map_sdiff'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a \ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a \
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_top' := map_top'✝, map_sdiff' := map_sdiff'✝ } =
    (fun f => f.toFun) g
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_top' := map_top'✝, map_sdiff' := map_sdiff'✝ } =
    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
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_inf'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } a ⊓
        SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } b
map_top'✝¹ :
  SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom ⊤ = ⊤
map_sdiff'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom (a \ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom a \
        SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
map_top'✝ :
  SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom ⊤ = ⊤
map_sdiff'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a \ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a \
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
        map_top' := map_top'✝¹, map_sdiff' := map_sdiff'✝¹ } =
    (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_top' := map_top'✝, map_sdiff' := map_sdiff'✝ }
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
      map_top' := map_top'✝¹, map_sdiff' := map_sdiff'✝¹ } =
    { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_top' := map_top'✝, map_sdiff' := map_sdiff'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b
[PROOFSTEP]
simpa only [h] using map_sup f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } b
[PROOFSTEP]
simpa only [h] using map_inf f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ↑f
⊢ SupHom.toFun
      { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                  SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } b) }.toSupHom
      ⊤ =
    ⊤
[PROOFSTEP]
simpa only [h] using map_top f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun
        { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                        b) }.toSupHom
        (a \ b) =
      SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          a \
        SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          b
[PROOFSTEP]
simpa only [h] using map_sdiff f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom β γ
g : CoheytingHom α β
src✝ : LatticeHom α γ := LatticeHom.comp f.toLatticeHom g.toLatticeHom
⊢ SupHom.toFun
      {
          toSupHom :=
            { toFun := ↑f ∘ ↑g,
              map_sup' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun src✝.toSupHom (a ⊔ b) = SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun src✝.toSupHom (a ⊓ b) =
                  SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
      ⊤ =
    ⊤
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom β γ
g : CoheytingHom α β
src✝ : LatticeHom α γ := LatticeHom.comp f.toLatticeHom g.toLatticeHom
a b : α
⊢ SupHom.toFun
      {
          toSupHom :=
            { toFun := ↑f ∘ ↑g,
              map_sup' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun src✝.toSupHom (a ⊔ b) = SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun src✝.toSupHom (a ⊓ b) =
                  SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
      (a \ b) =
    SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        a \
      SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f f₁ f₂ : CoheytingHom α β
g g₁ g₂ : CoheytingHom β γ
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
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f g : BiheytingHom α β
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
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
g : BiheytingHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
map_himp'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a ⇨ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a ⇨
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
map_sdiff'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a \ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a \
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_himp' := map_himp'✝, map_sdiff' := map_sdiff'✝ } =
    (fun f => f.toFun) g
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_himp' := map_himp'✝, map_sdiff' := map_sdiff'✝ } =
    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
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_inf'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } a ⊓
        SupHom.toFun { toFun := toFun✝¹, map_sup' := map_sup'✝¹ } b
map_himp'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom (a ⇨ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom a ⇨
        SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom b
map_sdiff'✝¹ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom (a \ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom a \
        SupHom.toFun { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ }.toSupHom b
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } (a ⊓ b) =
      SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } a ⊓
        SupHom.toFun { toFun := toFun✝, map_sup' := map_sup'✝ } b
map_himp'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a ⇨ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a ⇨
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
map_sdiff'✝ :
  ∀ (a b : α),
    SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom (a \ b) =
      SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom a \
        SupHom.toFun { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ }.toSupHom b
h :
  (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
        map_himp' := map_himp'✝¹, map_sdiff' := map_sdiff'✝¹ } =
    (fun f => f.toFun)
      { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
        map_himp' := map_himp'✝, map_sdiff' := map_sdiff'✝ }
⊢ { toLatticeHom := { toSupHom := { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }, map_inf' := map_inf'✝¹ },
      map_himp' := map_himp'✝¹, map_sdiff' := map_sdiff'✝¹ } =
    { toLatticeHom := { toSupHom := { toFun := toFun✝, map_sup' := map_sup'✝ }, map_inf' := map_inf'✝ },
      map_himp' := map_himp'✝, map_sdiff' := map_sdiff'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b
[PROOFSTEP]
simpa only [h] using map_sup f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } b
[PROOFSTEP]
simpa only [h] using map_inf f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun
        { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                        b) }.toSupHom
        (a ⇨ b) =
      SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          a ⇨
        SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          b
[PROOFSTEP]
simpa only [h] using map_himp f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ (a b : α),
    SupHom.toFun
        { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                        b) }.toSupHom
        (a \ b) =
      SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          a \
        SupHom.toFun
          { toSupHom := { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) },
              map_inf' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } (a ⊓ b) =
                      SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) } a ⊓
                        SupHom.toFun { toFun := f', map_sup' := (_ : ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b) }
                          b) }.toSupHom
          b
[PROOFSTEP]
simpa only [h] using map_sdiff f
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom β γ
g : BiheytingHom α β
src✝ : LatticeHom α γ := LatticeHom.comp f.toLatticeHom g.toLatticeHom
a b : α
⊢ SupHom.toFun
      {
          toSupHom :=
            { toFun := ↑f ∘ ↑g,
              map_sup' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun src✝.toSupHom (a ⊔ b) = SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun src✝.toSupHom (a ⊓ b) =
                  SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
      (a ⇨ b) =
    SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        a ⇨
      SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom β γ
g : BiheytingHom α β
src✝ : LatticeHom α γ := LatticeHom.comp f.toLatticeHom g.toLatticeHom
a b : α
⊢ SupHom.toFun
      {
          toSupHom :=
            { toFun := ↑f ∘ ↑g,
              map_sup' :=
                (_ :
                  ∀ (a b : α),
                    SupHom.toFun src✝.toSupHom (a ⊔ b) = SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
          map_inf' :=
            (_ :
              ∀ (a b : α),
                SupHom.toFun src✝.toSupHom (a ⊓ b) =
                  SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
      (a \ b) =
    SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        a \
      SupHom.toFun
        {
            toSupHom :=
              { toFun := ↑f ∘ ↑g,
                map_sup' :=
                  (_ :
                    ∀ (a b : α),
                      SupHom.toFun src✝.toSupHom (a ⊔ b) =
                        SupHom.toFun src✝.toSupHom a ⊔ SupHom.toFun src✝.toSupHom b) },
            map_inf' :=
              (_ :
                ∀ (a b : α),
                  SupHom.toFun src✝.toSupHom (a ⊓ b) =
                    SupHom.toFun src✝.toSupHom a ⊓ SupHom.toFun src✝.toSupHom b) }.toSupHom
        b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f f₁ f₂ : BiheytingHom α β
g g₁ g₂ : BiheytingHom β γ
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]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
⊢ IsEquipartition P ↔
    ∀ (a : Finset α),
      a ∈ P.parts →
        Finset.card a = Finset.card s / Finset.card P.parts ∨ Finset.card a = Finset.card s / Finset.card P.parts + 1
[PROOFSTEP]
simp_rw [IsEquipartition, Finset.equitableOn_iff, P.sum_card_parts]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : IsEquipartition P
ht : t ∈ P.parts
⊢ Finset.card s / Finset.card P.parts ≤ Finset.card t
[PROOFSTEP]
rw [← P.sum_card_parts]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : IsEquipartition P
ht : t ∈ P.parts
⊢ (Finset.sum P.parts fun i => Finset.card i) / Finset.card P.parts ≤ Finset.card t
[PROOFSTEP]
exact Finset.EquitableOn.le hP ht
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : IsEquipartition P
ht : t ∈ P.parts
⊢ Finset.card t ≤ Finset.card s / Finset.card P.parts + 1
[PROOFSTEP]
rw [← P.sum_card_parts]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : IsEquipartition P
ht : t ∈ P.parts
⊢ Finset.card t ≤ (Finset.sum P.parts fun i => Finset.card i) / Finset.card P.parts + 1
[PROOFSTEP]
exact Finset.EquitableOn.le_add_one hP ht
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
⊢ ∀ (a : Finset α), a ∈ ↑⊥.parts → Finset.card a = 1 ∨ Finset.card a = 1 + 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hs : s ≠ ∅
⊢ IsEquipartition (indiscrete hs)
[PROOFSTEP]
rw [IsEquipartition, indiscrete_parts, coe_singleton]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hs : s ≠ ∅
⊢ Set.EquitableOn {s} Finset.card
[PROOFSTEP]
exact Set.equitableOn_singleton s _


[GOAL]
⊢ ConcreteCategory ωCPO
[PROOFSTEP]
unfold ωCPO
[GOAL]
⊢ ConcreteCategory (Bundled OmegaCompletePartialOrder)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ NatTrans.app (product f).π j = NatTrans.app s.π j
⊢ m =
    (fun s =>
        {
          toOrderHom :=
            { toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
              monotone' :=
                (_ :
                  ∀ (x y : ↑s.pt),
                    x ≤ y → ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) },
          cont :=
            (_ :
              ∀ (x : Chain ↑s.pt),
                ↑{ toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                        monotone' :=
                          (_ :
                            ∀ (x y : ↑s.pt),
                              x ≤ y →
                                ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) }
                    (ωSup x) =
                  ωSup
                    (Chain.map x
                      { toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                        monotone' :=
                          (_ :
                            ∀ (x y : ↑s.pt),
                              x ≤ y →
                                ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) })) })
      s
[PROOFSTEP]
ext t
[GOAL]
case w
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ NatTrans.app (product f).π j = NatTrans.app s.π j
t : (forget ωCPO).obj s.pt
⊢ ↑m t =
    ↑((fun s =>
            {
              toOrderHom :=
                { toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                  monotone' :=
                    (_ :
                      ∀ (x y : ↑s.pt),
                        x ≤ y → ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) },
              cont :=
                (_ :
                  ∀ (x : Chain ↑s.pt),
                    ↑{ toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                            monotone' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  x ≤ y →
                                    ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) }
                        (ωSup x) =
                      ωSup
                        (Chain.map x
                          { toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                            monotone' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  x ≤ y →
                                    ∀ (j : J),
                                      ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) })) })
          s)
      t
[PROOFSTEP]
funext j
[GOAL]
case w.h
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ NatTrans.app (product f).π j = NatTrans.app s.π j
t : (forget ωCPO).obj s.pt
j : J
⊢ ↑m t j =
    ↑((fun s =>
            {
              toOrderHom :=
                { toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                  monotone' :=
                    (_ :
                      ∀ (x y : ↑s.pt),
                        x ≤ y → ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) },
              cont :=
                (_ :
                  ∀ (x : Chain ↑s.pt),
                    ↑{ toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                            monotone' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  x ≤ y →
                                    ∀ (j : J), ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) }
                        (ωSup x) =
                      ωSup
                        (Chain.map x
                          { toFun := fun t j => OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t,
                            monotone' :=
                              (_ :
                                ∀ (x y : ↑s.pt),
                                  x ≤ y →
                                    ∀ (j : J),
                                      ↑(NatTrans.app s.π { as := j }) x ≤ ↑(NatTrans.app s.π { as := j }) y) })) })
          s)
      t j
[PROOFSTEP]
change m.toFun t j = (s.π.app ⟨j⟩).toFun t
[GOAL]
case w.h
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ NatTrans.app (product f).π j = NatTrans.app s.π j
t : (forget ωCPO).obj s.pt
j : J
⊢ OrderHom.toFun m.toOrderHom t j = OrderHom.toFun (NatTrans.app s.π { as := j }).toOrderHom t
[PROOFSTEP]
rw [← w ⟨j⟩]
[GOAL]
case w.h
J : Type v
f : J → ωCPO
s : Cone (Discrete.functor f)
m : s.pt ⟶ (product f).pt
w : ∀ (j : Discrete J), m ≫ NatTrans.app (product f).π j = NatTrans.app s.π j
t : (forget ωCPO).obj s.pt
j : J
⊢ OrderHom.toFun m.toOrderHom t j = OrderHom.toFun (m ≫ NatTrans.app (product f).π { as := j }).toOrderHom t
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ (i : α), i ∈ c → ↑f i = ↑g i
⊢ ↑f (ωSup c) = ↑g (ωSup c)
[PROOFSTEP]
rw [f.continuous, g.continuous]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ (i : α), i ∈ c → ↑f i = ↑g i
⊢ ωSup (Chain.map c ↑f) = ωSup (Chain.map c ↑g)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ (i : α), i ∈ c → ↑f i = ↑g i
⊢ Chain.map c ↑f = Chain.map c ↑g
[PROOFSTEP]
apply OrderHom.ext
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ (i : α), i ∈ c → ↑f i = ↑g i
⊢ ↑(Chain.map c ↑f) = ↑(Chain.map c ↑g)
[PROOFSTEP]
funext x
[GOAL]
case e_a.h.h
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f g : α →𝒄 β
c : Chain α
hc : ∀ (i : α), i ∈ c → ↑f i = ↑g i
x : ℕ
⊢ ↑(Chain.map c ↑f) x = ↑(Chain.map c ↑g) x
[PROOFSTEP]
apply hc _ ⟨_, rfl⟩
[GOAL]
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
x : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)
⊢ OrderHom.toFun f.toOrderHom (OrderHom.toFun (Fork.ι s).toOrderHom x) =
    OrderHom.toFun g.toOrderHom (OrderHom.toFun (Fork.ι s).toOrderHom x)
[PROOFSTEP]
apply ContinuousHom.congr_fun s.condition
[GOAL]
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
⊢ {
        toOrderHom :=
          {
            toFun := fun x =>
              { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
            monotone' :=
              (_ :
                ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                  x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) },
        cont :=
          (_ :
            ∀ (x : Chain ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
              ↑{
                      toFun := fun x =>
                        { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                          property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                      monotone' :=
                        (_ :
                          ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                            x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) }
                  (ωSup x) =
                ωSup
                  (Chain.map x
                    {
                      toFun := fun x =>
                        { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                          property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                      monotone' :=
                        (_ :
                          ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                            x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) })) } ≫
      Fork.ι (equalizer f g) =
    Fork.ι s
[PROOFSTEP]
ext
[GOAL]
case w
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
x✝ : (forget ωCPO).obj (((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)
⊢ ↑({
            toOrderHom :=
              {
                toFun := fun x =>
                  { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                    property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                monotone' :=
                  (_ :
                    ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                      x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) },
            cont :=
              (_ :
                ∀ (x : Chain ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                  ↑{
                          toFun := fun x =>
                            { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                              property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                          monotone' :=
                            (_ :
                              ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                                x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) }
                      (ωSup x) =
                    ωSup
                      (Chain.map x
                        {
                          toFun := fun x =>
                            { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                              property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                          monotone' :=
                            (_ :
                              ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                                x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) })) } ≫
          Fork.ι (equalizer f g))
      x✝ =
    ↑(Fork.ι s) x✝
[PROOFSTEP]
rfl
[GOAL]
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (equalizer f g).pt).obj WalkingParallelPair.zero
hm : m✝ ≫ Fork.ι (equalizer f g) = Fork.ι s
⊢ m✝ =
    {
      toOrderHom :=
        {
          toFun := fun x =>
            { val := OrderHom.toFun (Fork.ι s).toOrderHom x, property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
          monotone' :=
            (_ :
              ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) },
      cont :=
        (_ :
          ∀ (x : Chain ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
            ↑{
                    toFun := fun x =>
                      { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                        property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                    monotone' :=
                      (_ :
                        ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                          x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) }
                (ωSup x) =
              ωSup
                (Chain.map x
                  {
                    toFun := fun x =>
                      { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                        property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                    monotone' :=
                      (_ :
                        ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                          x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) })) }
[PROOFSTEP]
apply
  ContinuousHom.ext _ _ fun x =>
    Subtype.ext
      ?_
        -- Porting note: Originally `ext`
[GOAL]
X Y : ωCPO
f g : X ⟶ Y
s : Fork f g
m✝ :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (equalizer f g).pt).obj WalkingParallelPair.zero
hm : m✝ ≫ Fork.ι (equalizer f g) = Fork.ι s
x : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)
⊢ ↑(↑m✝ x) =
    ↑(↑{
            toOrderHom :=
              {
                toFun := fun x =>
                  { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                    property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                monotone' :=
                  (_ :
                    ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                      x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) },
            cont :=
              (_ :
                ∀ (x : Chain ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                  ↑{
                          toFun := fun x =>
                            { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                              property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                          monotone' :=
                            (_ :
                              ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                                x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) }
                      (ωSup x) =
                    ωSup
                      (Chain.map x
                        {
                          toFun := fun x =>
                            { val := OrderHom.toFun (Fork.ι s).toOrderHom x,
                              property := (_ : ↑(Fork.ι s ≫ f) x = ↑(Fork.ι s ≫ g) x) },
                          monotone' :=
                            (_ :
                              ∀ (x y : ↑(((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero)),
                                x ≤ y → ↑(Fork.ι s) x ≤ ↑(Fork.ι s) y) })) }
        x)
[PROOFSTEP]
apply ContinuousHom.congr_fun hm


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ EquivLike.inv f b ≤ a ↔ b ≤ ↑f a
[PROOFSTEP]
convert (@map_le_map_iff _ _ _ _ _ _ f (EquivLike.inv f b) a).symm
[GOAL]
case h.e'_2.h.e'_3
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ b = ↑f (EquivLike.inv f b)
[PROOFSTEP]
exact (EquivLike.right_inv f _).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ a ≤ EquivLike.inv f b ↔ ↑f a ≤ b
[PROOFSTEP]
convert (@map_le_map_iff _ _ _ _ _ _ f a (EquivLike.inv f b)).symm
[GOAL]
case h.e'_2.h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ b = ↑f (EquivLike.inv f b)
[PROOFSTEP]
exact (EquivLike.right_inv _ _).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ EquivLike.inv f b < a ↔ b < ↑f a
[PROOFSTEP]
rw [← map_lt_map_iff f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ ↑f (EquivLike.inv f b) < ↑f a ↔ b < ↑f a
[PROOFSTEP]
simp only [EquivLike.apply_inv_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ a < EquivLike.inv f b ↔ ↑f a < b
[PROOFSTEP]
rw [← map_lt_map_iff f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ ↑f a < ↑f (EquivLike.inv f b) ↔ ↑f a < b
[PROOFSTEP]
simp only [EquivLike.apply_inv_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f g : α →o β
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
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
g : α →o β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
h : { toFun := toFun✝, monotone' := monotone'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, monotone' := monotone'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
h : { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun = { toFun := toFun✝, monotone' := monotone'✝ }.toFun
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹ } = { toFun := toFun✝, monotone' := monotone'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
⊢ ∀ {a b : α × β →o γ},
    ↑{
              toFun := fun f =>
                {
                  toFun := fun x =>
                    { toFun := Function.curry (↑f) x,
                      monotone' := (_ : ∀ (x_1 x_2 : β), x_1 ≤ x_2 → ↑f (x, x_1) ≤ ↑f (x, x_2)) },
                  monotone' := (_ : ∀ (x x_1 : α), x ≤ x_1 → ∀ (x_2 : β), ↑f (x, x_2) ≤ ↑f (x_1, x_2)) },
              invFun := fun f =>
                { toFun := Function.uncurry fun x => ↑(↑f x),
                  monotone' :=
                    (_ : ∀ (x y : α × β), x ≤ y → toFun (↑f x.fst) x.snd ≤ Function.uncurry (fun x => ↑(↑f x)) y) },
              left_inv :=
                (_ :
                  ∀ (x : α × β →o γ),
                    (fun f =>
                          { toFun := Function.uncurry fun x => ↑(↑f x),
                            monotone' :=
                              (_ :
                                ∀ (x y : α × β),
                                  x ≤ y → toFun (↑f x.fst) x.snd ≤ Function.uncurry (fun x => ↑(↑f x)) y) })
                        ((fun f =>
                            {
                              toFun := fun x =>
                                { toFun := Function.curry (↑f) x,
                                  monotone' := (_ : ∀ (x_1 x_2 : β), x_1 ≤ x_2 → ↑f (x, x_1) ≤ ↑f (x, x_2)) },
                              monotone' := (_ : ∀ (x x_1 : α), x ≤ x_1 → ∀ (x_2 : β), ↑f (x, x_2) ≤ ↑f (x_1, x_2)) })
                          x) =
                      (fun f =>
                          { toFun := Function.uncurry fun x => ↑(↑f x),
                            monotone' :=
                              (_ :
                                ∀ (x y : α × β),
                                  x ≤ y → toFun (↑f x.fst) x.snd ≤ Function.uncurry (fun x => ↑(↑f x)) y) })
                        ((fun f =>
                            {
                              toFun := fun x =>
                                { toFun := Function.curry (↑f) x,
                                  monotone' := (_ : ∀ (x_1 x_2 : β), x_1 ≤ x_2 → ↑f (x, x_1) ≤ ↑f (x, x_2)) },
                              monotone' := (_ : ∀ (x x_1 : α), x ≤ x_1 → ∀ (x_2 : β), ↑f (x, x_2) ≤ ↑f (x_1, x_2)) })
                          x)),
              right_inv :=
                (_ :
                  ∀ (x : α →o β →o γ),
                    (fun f =>
                          {
                            toFun := fun x =>
                              { toFun := Function.curry (↑f) x,
                                monotone' := (_ : ∀ (x_1 x_2 : β), x_1 ≤ x_2 → ↑f (x, x_1) ≤ ↑f (x, x_2)) },
                            monotone' := (_ : ∀ (x x_1 : α), x ≤ x_1 → ∀ (x_2 : β), ↑f (x, x_2) ≤ ↑f (x_1, x_2)) })
                        ((fun f =>
                            { toFun := Function.uncurry fun x => ↑(↑f x),
                              monotone' :=
                                (_ :
                                  ∀ (x y : α × β),
                                    x ≤ y → toFun (↑f x.fst) x.snd ≤ Function.uncurry (fun x => ↑(↑f x)) y) })
                          x) =
                      (fun f =>
                          {
                            toFun := fun x =>
                              { toFun := Function.curry (↑f) x,
                                monotone' := (_ : ∀ (x_1 x_2 : β), x_1 ≤ x_2 → ↑f (x, x_1) ≤ ↑f (x, x_2)) },
                            monotone' := (_ : ∀ (x x_1 : α), x ≤ x_1 → ∀ (x_2 : β), ↑f (x, x_2) ≤ ↑f (x_1, x_2)) })
                        ((fun f =>
                            { toFun := Function.uncurry fun x => ↑(↑f x),
                              monotone' :=
                                (_ :
                                  ∀ (x y : α × β),
                                    x ≤ y → toFun (↑f x.fst) x.snd ≤ Function.uncurry (fun x => ↑(↑f x)) y) })
                          x)) }
          a ≤
        ↑{
              toFun := fun f =>
                {
                  toFun := fun x =>
                    { toFun := Function.curry (↑f) x,
                      monotone' := (_ : ∀ (x_1 x_2 : β), x_1 ≤ x_2 → ↑f (x, x_1) ≤ ↑f (x, x_2)) },
                  monotone' := (_ : ∀ (x x_1 : α), x ≤ x_1 → ∀ (x_2 : β), ↑f (x, x_2) ≤ ↑f (x_1, x_2)) },
              invFun := fun f =>
                { toFun := Function.uncurry fun x => ↑(↑f x),
                  monotone' :=
                    (_ : ∀ (x y : α × β), x ≤ y → toFun (↑f x.fst) x.snd ≤ Function.uncurry (fun x => ↑(↑f x)) y) },
              left_inv :=
                (_ :
                  ∀ (x : α × β →o γ),
                    (fun f =>
                          { toFun := Function.uncurry fun x => ↑(↑f x),
                            monotone' :=
                              (_ :
                                ∀ (x y : α × β),
                                  x ≤ y → toFun (↑f x.fst) x.snd ≤ Function.uncurry (fun x => ↑(↑f x)) y) })
                        ((fun f =>
                            {
                              toFun := fun x =>
                                { toFun := Function.curry (↑f) x,
                                  monotone' := (_ : ∀ (x_1 x_2 : β), x_1 ≤ x_2 → ↑f (x, x_1) ≤ ↑f (x, x_2)) },
                              monotone' := (_ : ∀ (x x_1 : α), x ≤ x_1 → ∀ (x_2 : β), ↑f (x, x_2) ≤ ↑f (x_1, x_2)) })
                          x) =
                      (fun f =>
                          { toFun := Function.uncurry fun x => ↑(↑f x),
                            monotone' :=
                              (_ :
                                ∀ (x y : α × β),
                                  x ≤ y → toFun (↑f x.fst) x.snd ≤ Function.uncurry (fun x => ↑(↑f x)) y) })
                        ((fun f =>
                            {
                              toFun := fun x =>
                                { toFun := Function.curry (↑f) x,
                                  monotone' := (_ : ∀ (x_1 x_2 : β), x_1 ≤ x_2 → ↑f (x, x_1) ≤ ↑f (x, x_2)) },
                              monotone' := (_ : ∀ (x x_1 : α), x ≤ x_1 → ∀ (x_2 : β), ↑f (x, x_2) ≤ ↑f (x_1, x_2)) })
                          x)),
              right_inv :=
                (_ :
                  ∀ (x : α →o β →o γ),
                    (fun f =>
                          {
                            toFun := fun x =>
                              { toFun := Function.curry (↑f) x,
                                monotone' := (_ : ∀ (x_1 x_2 : β), x_1 ≤ x_2 → ↑f (x, x_1) ≤ ↑f (x, x_2)) },
                            monotone' := (_ : ∀ (x x_1 : α), x ≤ x_1 → ∀ (x_2 : β), ↑f (x, x_2) ≤ ↑f (x_1, x_2)) })
                        ((fun f =>
                            { toFun := Function.uncurry fun x => ↑(↑f x),
                              monotone' :=
                                (_ :
                                  ∀ (x y : α × β),
                                    x ≤ y → toFun (↑f x.fst) x.snd ≤ Function.uncurry (fun x => ↑(↑f x)) y) })
                          x) =
                      (fun f =>
                          {
                            toFun := fun x =>
                              { toFun := Function.curry (↑f) x,
                                monotone' := (_ : ∀ (x_1 x_2 : β), x_1 ≤ x_2 → ↑f (x, x_1) ≤ ↑f (x, x_2)) },
                            monotone' := (_ : ∀ (x x_1 : α), x ≤ x_1 → ∀ (x_2 : β), ↑f (x, x_2) ≤ ↑f (x_1, x_2)) })
                        ((fun f =>
                            { toFun := Function.uncurry fun x => ↑(↑f x),
                              monotone' :=
                                (_ :
                                  ∀ (x y : α × β),
                                    x ≤ y → toFun (↑f x.fst) x.snd ≤ Function.uncurry (fun x => ↑(↑f x)) y) })
                          x)) }
          b ↔
      a ≤ b
[PROOFSTEP]
simp [le_def]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α →o β
⊢ comp f id = f
[PROOFSTEP]
ext
[GOAL]
case h.h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α →o β
x✝ : α
⊢ ↑(comp f id) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α →o β
⊢ comp id f = f
[PROOFSTEP]
ext
[GOAL]
case h.h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α →o β
x✝ : α
⊢ ↑(comp id f) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
⊢ OrderHom.prod fst snd = id
[PROOFSTEP]
ext ⟨x, y⟩ : 2
[GOAL]
case h.h.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
x : α
y : β
⊢ ↑(OrderHom.prod fst snd) (x, y) = ↑id (x, y)
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Preorder γ
inst✝¹ : Preorder δ
ι : Type u_6
π : ι → Type u_7
inst✝ : (i : ι) → Preorder (π i)
p q : α → Prop
h : ∀ (a : α), p a → q a
src✝ : { x // p x } ↪ { x // q x } := Subtype.impEmbedding (fun x => p x) (fun x => q x) h
⊢ ∀ {a b : { x // p x }},
    ↑{ toFun := src✝.toFun, inj' := (_ : Function.Injective src✝.toFun) } a ≤
        ↑{ toFun := src✝.toFun, inj' := (_ : Function.Injective src✝.toFun) } b ↔
      a ≤ b
[PROOFSTEP]
aesop
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x x_1 => x < x_1) ↪r fun x x_1 => x < x_1
⊢ ∀ {a b : α}, ↑f.toEmbedding a ≤ ↑f.toEmbedding b ↔ a ≤ b
[PROOFSTEP]
intros
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x x_1 => x < x_1) ↪r fun x x_1 => x < x_1
a✝ b✝ : α
⊢ ↑f.toEmbedding a✝ ≤ ↑f.toEmbedding b✝ ↔ a✝ ≤ b✝
[PROOFSTEP]
simp [le_iff_lt_or_eq, f.map_rel_iff, f.injective.eq_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
⊢ ∀ {a b : α}, ↑f.toEmbedding a < ↑f.toEmbedding b ↔ a < b
[PROOFSTEP]
intros
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
a✝ b✝ : α
⊢ ↑f.toEmbedding a✝ < ↑f.toEmbedding b✝ ↔ a✝ < b✝
[PROOFSTEP]
simp [lt_iff_le_not_le, f.map_rel_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
f g : α ≃o β
h₁ : (fun f => f.toFun) f = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) f = (fun f => f.invFun) 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
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
g : α ≃o β
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : Function.LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_rel_iff'✝ :
  ∀ {a b : α},
    ↑{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } a ≤
        ↑{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } b ↔
      a ≤ b
h₁ :
  (fun f => f.toFun)
      { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_rel_iff' := map_rel_iff'✝ } =
    (fun f => f.toFun) g
h₂ :
  (fun f => f.invFun)
      { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_rel_iff' := map_rel_iff'✝ } =
    (fun f => f.invFun) g
⊢ { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
      map_rel_iff' := map_rel_iff'✝ } =
    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
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
toFun✝¹ : α → β
invFun✝¹ : β → α
left_inv✝¹ : Function.LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : Function.RightInverse invFun✝¹ toFun✝¹
map_rel_iff'✝¹ :
  ∀ {a b : α},
    ↑{ toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } a ≤
        ↑{ toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } b ↔
      a ≤ b
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : Function.LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
map_rel_iff'✝ :
  ∀ {a b : α},
    ↑{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } a ≤
        ↑{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } b ↔
      a ≤ b
h₁ :
  (fun f => f.toFun)
      { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
        map_rel_iff' := map_rel_iff'✝¹ } =
    (fun f => f.toFun)
      { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_rel_iff' := map_rel_iff'✝ }
h₂ :
  (fun f => f.invFun)
      { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
        map_rel_iff' := map_rel_iff'✝¹ } =
    (fun f => f.invFun)
      { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
        map_rel_iff' := map_rel_iff'✝ }
⊢ { toEquiv := { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ },
      map_rel_iff' := map_rel_iff'✝¹ } =
    { toEquiv := { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ },
      map_rel_iff' := map_rel_iff'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
e : α ≃o β
⊢ symm (symm e) = e
[PROOFSTEP]
ext
[GOAL]
case h.h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
e : α ≃o β
x✝ : α
⊢ ↑(symm (symm e)) x✝ = ↑e x✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
e e' : α ≃o β
h : symm e = symm e'
⊢ e = e'
[PROOFSTEP]
rw [← e.symm_symm, h, e'.symm_symm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
e : α ≃o β
⊢ trans (refl α) e = e
[PROOFSTEP]
ext x
[GOAL]
case h.h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
e : α ≃o β
x : α
⊢ ↑(trans (refl α) e) x = ↑e x
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
e : α ≃o β
⊢ trans e (refl β) = e
[PROOFSTEP]
ext x
[GOAL]
case h.h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
e : α ≃o β
x : α
⊢ ↑(trans e (refl β)) x = ↑e x
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type ?u.90717
β : Type ?u.90720
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x x_1 => x < x_1) ≃r fun x x_1 => x < x_1
⊢ ∀ {a b : α}, ↑e.toEquiv a ≤ ↑e.toEquiv b ↔ a ≤ b
[PROOFSTEP]
simp [le_iff_eq_or_lt, e.map_rel_iff, e.injective.eq_iff]
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : α ≃o β
⊢ ofRelIsoLT (toRelIsoLT e) = e
[PROOFSTEP]
ext
[GOAL]
case h.h
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : α ≃o β
x✝ : α
⊢ ↑(ofRelIsoLT (toRelIsoLT e)) x✝ = ↑e x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x x_1 => x < x_1) ≃r fun x x_1 => x < x_1
⊢ toRelIsoLT (ofRelIsoLT e) = e
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x x_1 => x < x_1) ≃r fun x x_1 => x < x_1
x✝ : α
⊢ ↑(toRelIsoLT (ofRelIsoLT e)) x✝ = ↑e x✝
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type ?u.94646
β : Type ?u.94649
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
⊢ ∀ (a : α), a = g (f a)
[PROOFSTEP]
intro
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type ?u.94646
β : Type ?u.94649
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
a✝ : α
⊢ a✝ = g (f a✝)
[PROOFSTEP]
rw [← cmp_eq_eq_iff, h, cmp_self_eq_eq]
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type ?u.94646
β : Type ?u.94649
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
⊢ Function.RightInverse g f
[PROOFSTEP]
intro
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type ?u.94646
β : Type ?u.94649
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
x✝ : β
⊢ f (g x✝) = x✝
[PROOFSTEP]
rw [← cmp_eq_eq_iff, ← h, cmp_self_eq_eq]
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type ?u.94646
β : Type ?u.94649
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
⊢ ∀ {a b : α},
    ↑{ toFun := f, invFun := g, left_inv := (_ : ∀ (a : α), g (f a) = a), right_inv := (_ : ∀ (x : β), f (g x) = x) }
          a ≤
        ↑{ toFun := f, invFun := g, left_inv := (_ : ∀ (a : α), g (f a) = a),
              right_inv := (_ : ∀ (x : β), f (g x) = x) }
          b ↔
      a ≤ b
[PROOFSTEP]
intros a b
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type ?u.94646
β : Type ?u.94649
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
⊢ ↑{ toFun := f, invFun := g, left_inv := (_ : ∀ (a : α), g (f a) = a), right_inv := (_ : ∀ (x : β), f (g x) = x) } a ≤
      ↑{ toFun := f, invFun := g, left_inv := (_ : ∀ (a : α), g (f a) = a), right_inv := (_ : ∀ (x : β), f (g x) = x) }
        b ↔
    a ≤ b
[PROOFSTEP]
apply le_iff_le_of_cmp_eq_cmp
[GOAL]
case h
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type ?u.94646
β : Type ?u.94649
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
⊢ cmp
      (↑{ toFun := f, invFun := g, left_inv := (_ : ∀ (a : α), g (f a) = a), right_inv := (_ : ∀ (x : β), f (g x) = x) }
        a)
      (↑{ toFun := f, invFun := g, left_inv := (_ : ∀ (a : α), g (f a) = a), right_inv := (_ : ∀ (x : β), f (g x) = x) }
        b) =
    cmp a b
[PROOFSTEP]
convert (h a (f b)).symm
[GOAL]
case h.e'_3.h.e'_5
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type ?u.94646
β : Type ?u.94649
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
⊢ b = g (f b)
[PROOFSTEP]
apply gf
[GOAL]
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Preorder γ
F : Type u_6
G : Type u_7
inst✝¹ : OrderHomClass F α β
inst✝ : OrderHomClass G β α
f : F
g : G
h₁ : OrderHom.comp ↑f ↑g = OrderHom.id
h₂ : OrderHom.comp ↑g ↑f = OrderHom.id
a b : α
h :
  ↑{ toFun := ↑f, invFun := ↑g, left_inv := (_ : ∀ (x : α), ↑(OrderHom.comp ↑g ↑f) x = ↑OrderHom.id x),
          right_inv := (_ : ∀ (x : β), ↑(OrderHom.comp ↑f ↑g) x = ↑OrderHom.id x) }
      a ≤
    ↑{ toFun := ↑f, invFun := ↑g, left_inv := (_ : ∀ (x : α), ↑(OrderHom.comp ↑g ↑f) x = ↑OrderHom.id x),
          right_inv := (_ : ∀ (x : β), ↑(OrderHom.comp ↑f ↑g) x = ↑OrderHom.id x) }
      b
⊢ a ≤ b
[PROOFSTEP]
replace h := map_rel g h
[GOAL]
F✝ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Preorder γ
F : Type u_6
G : Type u_7
inst✝¹ : OrderHomClass F α β
inst✝ : OrderHomClass G β α
f : F
g : G
h₁ : OrderHom.comp ↑f ↑g = OrderHom.id
h₂ : OrderHom.comp ↑g ↑f = OrderHom.id
a b : α
h :
  ↑g
      (↑{ toFun := ↑f, invFun := ↑g, left_inv := (_ : ∀ (x : α), ↑(OrderHom.comp ↑g ↑f) x = ↑OrderHom.id x),
            right_inv := (_ : ∀ (x : β), ↑(OrderHom.comp ↑f ↑g) x = ↑OrderHom.id x) }
        a) ≤
    ↑g
      (↑{ toFun := ↑f, invFun := ↑g, left_inv := (_ : ∀ (x : α), ↑(OrderHom.comp ↑g ↑f) x = ↑OrderHom.id x),
            right_inv := (_ : ∀ (x : β), ↑(OrderHom.comp ↑f ↑g) x = ↑OrderHom.id x) }
        b)
⊢ a ≤ b
[PROOFSTEP]
rwa [Equiv.coe_fn_mk, show g (f a) = (g : β →o α).comp (f : α →o β) a from rfl,
  show g (f b) = (g : β →o α).comp (f : α →o β) b from rfl, h₂] at h
[GOAL]
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Preorder α✝
inst✝³ : Preorder β✝
inst✝² : Preorder γ
α : Type u_6
β : Type u_7
inst✝¹ : Unique α
inst✝ : Preorder β
⊢ ∀ {a b : α → β}, ↑(Equiv.funUnique α β) a ≤ ↑(Equiv.funUnique α β) b ↔ a ≤ b
[PROOFSTEP]
simp [Pi.le_def, Unique.forall_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃ β
h₁ : Monotone ↑e
h₂ : Monotone ↑e.symm
a✝ b✝ : α
h : ↑e a✝ ≤ ↑e b✝
⊢ a✝ ≤ b✝
[PROOFSTEP]
simpa only [e.symm_apply_apply] using h₂ h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ ↑f x = y
[PROOFSTEP]
refine' le_antisymm _ (hy _)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ ↑f x ≤ y
[PROOFSTEP]
rw [← f.apply_symm_apply y, f.map_rel_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ x ≤ ↑(symm f) y
[PROOFSTEP]
apply hx
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ ↑f (x ⊓ y) = ↑f x ⊓ ↑f y
[PROOFSTEP]
refine' (f.toOrderEmbedding.map_inf_le x y).antisymm _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ ↑(toOrderEmbedding f) x ⊓ ↑(toOrderEmbedding f) y ≤ ↑(toOrderEmbedding f) (x ⊓ y)
[PROOFSTEP]
apply f.symm.le_iff_le.1
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ ↑(symm f) (↑(toOrderEmbedding f) x ⊓ ↑(toOrderEmbedding f) y) ≤ ↑(symm f) (↑(toOrderEmbedding f) (x ⊓ y))
[PROOFSTEP]
simpa using f.symm.toOrderEmbedding.map_inf_le (f x) (f y)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ Disjoint (↑f a) (↑f b)
[PROOFSTEP]
rw [disjoint_iff_inf_le, ← f.map_inf, ← f.map_bot]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ ↑f (a ⊓ b) ≤ ↑f ⊥
[PROOFSTEP]
exact f.monotone ha.le_bot
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ Codisjoint (↑f a) (↑f b)
[PROOFSTEP]
rw [codisjoint_iff_le_sup, ← f.map_sup, ← f.map_top]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ ↑f ⊤ ≤ ↑f (a ⊔ b)
[PROOFSTEP]
exact f.monotone ha.top_le
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
f : α ≃o β
inst✝ : ComplementedLattice α
x : β
⊢ ∃ b, IsCompl x b
[PROOFSTEP]
obtain ⟨y, hy⟩ := exists_isCompl (f.symm x)
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
f : α ≃o β
inst✝ : ComplementedLattice α
x : β
y : α
hy : IsCompl (↑(symm f) x) y
⊢ ∃ b, IsCompl x b
[PROOFSTEP]
rw [← f.symm_apply_apply y] at hy
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
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
[PROOFSTEP]
exact ⟨f y, f.symm.isCompl_iff.2 hy⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ ComplementedLattice α → ComplementedLattice β
[PROOFSTEP]
intro
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
a✝ : ComplementedLattice α
⊢ ComplementedLattice β
[PROOFSTEP]
exact f.complementedLattice
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ ComplementedLattice β → ComplementedLattice α
[PROOFSTEP]
intro
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
a✝ : ComplementedLattice β
⊢ ComplementedLattice α
[PROOFSTEP]
exact f.symm.complementedLattice