[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
