awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃ β
map_rel_iff' : ∀ {a b : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β) ↔ a ≤ b
⊢ symm (RelIso.mk (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2) e @map_rel_iff') =
    RelIso.mk (r := fun (x1 x2 : β) ↦ x1 ≤ x2) (s := fun (x1 x2 : α) ↦ x1 ≤ x2) e.symm ⋯

Tactic:
rfl

Premises used: RelIso.symm, OrderIso.symm, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
x : β
⊢ (e : (a : α) → β) ((e.symm : (a : β) → α) x : α) = x

Tactic:
e.toEquiv.apply_symm_apply x

Premises used: Equiv.apply_symm_apply, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
x : α
⊢ (e.symm : (a : β) → α) ((e : (a : α) → β) x : β) = x

Tactic:
e.toEquiv.symm_apply_apply x

Premises used: Equiv.symm_apply_apply, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
inst : LE α
⊢ Eq (α := α ≃o α) (symm (refl α)) (refl α)

Tactic:
rfl

Premises used: RelIso.refl, RelIso.symm, Equiv.symm, Equiv.refl, rfl, OrderIso.refl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
x : α
y : β
⊢ (e : (a : α) → β) x = y ↔ x = (e.symm : (a : β) → α) y

Tactic:
e.toEquiv.apply_eq_iff_eq_symm_apply

Premises used: RelIso.toEquiv, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
x : α
y : β
⊢ (e.symm : (a : β) → α) y = x ↔ y = (e : (a : α) → β) x

Tactic:
e.toEquiv.symm_apply_eq

Premises used: Equiv.symm_apply_eq, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: RelIso.symm, OrderIso.symm, Equiv.symm, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
⊢ Function.Bijective (α := α ≃o β) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, OrderIso.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
⊢ Function.Injective (α := α ≃o β) symm

Tactic:
symm_bijective.injective

Premises used: OrderIso.symm_bijective, Function.Bijective.injective
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
⊢ e.symm.toEquiv (r := fun (x1 x2 : β) ↦ x1 ≤ x2) (s := fun (x1 x2 : α) ↦ x1 ≤ x2) =
    e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).symm

Tactic:
rfl

Premises used: Equiv.symm, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
⊢ Eq (α := (a : α) → β) (⇑(e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2)) : (a : α) → β)
    (⇑e : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
⊢ Eq (α := (a : β) → α)
    (⇑e.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).symm : (a : β) → α)
    (⇑e.symm : (a : β) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : LE α
inst_1 : LE β
inst_2 : LE γ
e : α ≃o β
e' : β ≃o γ
⊢ Eq (α := (a : α) → γ) (⇑(e.trans e') : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑e' : (a : β) → γ) (⇑e : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : LE α
inst_1 : LE β
inst_2 : LE γ
e : α ≃o β
e' : β ≃o γ
x : α
⊢ Eq.{u_4 + 1} (α := γ) ((e.trans e' : (a : α) → γ) x : γ) ((e' : (a : β) → γ) ((e : (a : α) → β) x : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((trans (refl α) e : (a : α) → β) x : β) ((e : (a : α) → β) x : β)
⊢ trans (refl α) e = e

Tactic:
ext x
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
x : α
⊢ Eq.{u_3 + 1} (α := β) ((trans (refl α) e : (a : α) → β) x : β) ((e : (a : α) → β) x : β)

Tactic:
rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((e.trans (refl β) : (a : α) → β) x : β) ((e : (a : α) → β) x : β)
⊢ e.trans (refl β) = e

Tactic:
ext x
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
x : α
⊢ Eq.{u_3 + 1} (α := β) ((e.trans (refl β) : (a : α) → β) x : β) ((e : (a : α) → β) x : β)

Tactic:
rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : LE α
inst_1 : LE β
inst_2 : LE γ
e₁ : α ≃o β
e₂ : β ≃o γ
c : γ
⊢ Eq.{u_2 + 1} (α := α) (((e₁.trans e₂).symm : (a : γ) → α) c : α)
    ((e₁.symm : (a : β) → α) ((e₂.symm : (a : γ) → β) c : β) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : LE α
inst_1 : LE β
inst_2 : LE γ
e₁ : α ≃o β
e₂ : β ≃o γ
⊢ (e₁.trans e₂).symm = e₂.symm.trans e₁.symm

Tactic:
rfl

Premises used: Equiv.trans, RelIso.symm, RelIso.trans, Equiv.symm, rfl, OrderIso.trans
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
⊢ e.trans e.symm = refl α

Tactic:
RelIso.self_trans_symm e

Premises used: RelIso.self_trans_symm, OrderIso.symm, OrderIso.refl, OrderIso.trans
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
⊢ e.symm.trans e = refl β

Tactic:
RelIso.symm_trans_self e

Premises used: OrderIso.symm, RelIso.symm_trans_self, OrderIso.refl, OrderIso.trans
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : LE α
inst_1 : LE β
inst_2 : LE γ
inst_3 : LE δ
f : α ≃o β
g : β ≃o γ
h : γ ≃o δ
⊢ (f.trans g).trans h = f.trans (g.trans h)

Tactic:
rfl

Premises used: Equiv.trans, RelIso.trans, rfl, OrderIso.trans
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ_1 : Type u_5
inst : LE α_1
inst_1 : LE β_1
inst_2 : LE γ_1
inst_3 : LE δ_1
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst_4 : Preorder α
inst_5 : Preorder β
inst_6 : Preorder γ
inst_7 : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : α →o β
change :
  Eq (α := α → β)
    (Function.comp (β := β)
      (Function.comp.{u_7 + 1, u_9 + 1, u_7 + 1} (β := δ) (⇑g.symm : (a : δ) → β) (⇑g : (a : β) → δ))
      (Function.comp (β := α) (⇑p : (a : α) → β)
        (Function.comp.{u_6 + 1, u_8 + 1, u_6 + 1} (β := γ) (⇑f.symm : (a : γ) → α) (⇑f : (a : α) → γ))))
    (⇑p : (a : α) → β)
⊢ Eq (α := (a : α) → β)
    ((fun (f : α →o β) ↦ ((⇑f : (a : α) → β) : (a : α) → β))
      ((fun (p : γ →o δ) ↦ (OrderHom.comp (↑g.symm : δ →o β) (p.comp (↑f : α →o γ)) : α →o β))
        ((fun (p : α →o β) ↦ (OrderHom.comp (↑g : β →o δ) (p.comp (↑f.symm : γ →o α)) : γ →o δ)) p)))
    ((fun (f : α →o β) ↦ ((⇑f : (a : α) → β) : (a : α) → β)) p)

Tactic:
change (g.symm ∘ g) ∘ p ∘ (f.symm ∘ f) = p

Premises used: Function.comp, OrderIso.symm, DFunLike.coe
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ_1 : Type u_5
inst : LE α_1
inst_1 : LE β_1
inst_2 : LE γ_1
inst_3 : LE δ_1
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst_4 : Preorder α
inst_5 : Preorder β
inst_6 : Preorder γ
inst_7 : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : α →o β
⊢ Eq (α := α → β)
    (Function.comp (β := β)
      (Function.comp.{u_7 + 1, u_9 + 1, u_7 + 1} (β := δ) (⇑g.symm : (a : δ) → β) (⇑g : (a : β) → δ))
      (Function.comp (β := α) (⇑p : (a : α) → β)
        (Function.comp.{u_6 + 1, u_8 + 1, u_6 + 1} (β := γ) (⇑f.symm : (a : γ) → α) (⇑f : (a : α) → γ))))
    (⇑p : (a : α) → β)

Tactic:
simp only [← OrderIso.coe_trans, Function.id_comp,
               OrderIso.self_trans_symm, OrderIso.coe_refl, Function.comp_id]

Premises used: Function.comp_id, OrderIso.coe_refl, OrderIso.coe_trans, OrderIso.self_trans_symm, Function.id_comp
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ_1 : Type u_5
inst : LE α_1
inst_1 : LE β_1
inst_2 : LE γ_1
inst_3 : LE δ_1
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst_4 : Preorder α
inst_5 : Preorder β
inst_6 : Preorder γ
inst_7 : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : γ →o δ
change :
  Eq (α := γ → δ)
    (Function.comp (β := δ)
      (Function.comp.{u_9 + 1, u_7 + 1, u_9 + 1} (β := β) (⇑g : (a : β) → δ) (⇑g.symm : (a : δ) → β))
      (Function.comp (β := γ) (⇑p : (a : γ) → δ)
        (Function.comp.{u_8 + 1, u_6 + 1, u_8 + 1} (β := α) (⇑f : (a : α) → γ) (⇑f.symm : (a : γ) → α))))
    (⇑p : (a : γ) → δ)
⊢ Eq (α := (a : γ) → δ)
    ((fun (f : γ →o δ) ↦ ((⇑f : (a : γ) → δ) : (a : γ) → δ))
      ((fun (p : α →o β) ↦ (OrderHom.comp (↑g : β →o δ) (p.comp (↑f.symm : γ →o α)) : γ →o δ))
        ((fun (p : γ →o δ) ↦ (OrderHom.comp (↑g.symm : δ →o β) (p.comp (↑f : α →o γ)) : α →o β)) p)))
    ((fun (f : γ →o δ) ↦ ((⇑f : (a : γ) → δ) : (a : γ) → δ)) p)

Tactic:
change (g ∘ g.symm) ∘ p ∘ (f ∘ f.symm) = p

Premises used: Function.comp, OrderIso.symm, DFunLike.coe
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ_1 : Type u_5
inst : LE α_1
inst_1 : LE β_1
inst_2 : LE γ_1
inst_3 : LE δ_1
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst_4 : Preorder α
inst_5 : Preorder β
inst_6 : Preorder γ
inst_7 : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : γ →o δ
⊢ Eq (α := γ → δ)
    (Function.comp (β := δ)
      (Function.comp.{u_9 + 1, u_7 + 1, u_9 + 1} (β := β) (⇑g : (a : β) → δ) (⇑g.symm : (a : δ) → β))
      (Function.comp (β := γ) (⇑p : (a : γ) → δ)
        (Function.comp.{u_8 + 1, u_6 + 1, u_8 + 1} (β := α) (⇑f : (a : α) → γ) (⇑f.symm : (a : γ) → α))))
    (⇑p : (a : γ) → δ)

Tactic:
simp only [← OrderIso.coe_trans, Function.id_comp,
               OrderIso.symm_trans_self, OrderIso.coe_refl, Function.comp_id]

Premises used: Function.comp_id, OrderIso.coe_refl, OrderIso.symm_trans_self, OrderIso.coe_trans, Function.id_comp
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ_1 : Type u_5
inst : LE α_1
inst_1 : LE β_1
inst_2 : LE γ_1
inst_3 : LE δ_1
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst_4 : Preorder α
inst_5 : Preorder β
inst_6 : Preorder γ
inst_7 : Preorder δ
f : α ≃o γ
g : β ≃o δ
p q : α →o β
simp :
  (∀ (x : γ),
      LE.le.{u_7} (α := β) ((p : (a : α) → β) ((f.symm : (a : γ) → α) x : α) : β)
        ((q : (a : α) → β) ((f.symm : (a : γ) → α) x : α) : β)) ↔
    ∀ (x : α), LE.le.{u_7} (α := β) ((p : (a : α) → β) x : β) ((q : (a : α) → β) x : β)
⊢ LE.le (α := γ →o δ)
      (({ toFun := fun (p : α →o β) ↦ OrderHom.comp (↑g : β →o δ) (p.comp (↑f.symm : γ →o α)),
              invFun := fun (p : γ →o δ) ↦ OrderHom.comp (↑g.symm : δ →o β) (p.comp (↑f : α →o γ)), left_inv := ⋯,
              right_inv := ⋯ } :
            (a : α →o β) → γ →o δ)
          p :
        γ →o δ)
      (({ toFun := fun (p : α →o β) ↦ OrderHom.comp (↑g : β →o δ) (p.comp (↑f.symm : γ →o α)),
              invFun := fun (p : γ →o δ) ↦ OrderHom.comp (↑g.symm : δ →o β) (p.comp (↑f : α →o γ)), left_inv := ⋯,
              right_inv := ⋯ } :
            (a : α →o β) → γ →o δ)
          q :
        γ →o δ) ↔
    p ≤ q

Tactic:
simp only [Equiv.coe_fn_mk, OrderHom.le_def, OrderHom.comp_coe,
               OrderHomClass.coe_coe, Function.comp_apply, map_le_map_iff]

Premises used: OrderIsoClass.map_le_map_iff, OrderHom.le_def, OrderHom.comp_coe, OrderHomClass.coe_coe, Equiv.coe_fn_mk, Function.comp_apply
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ_1 : Type u_5
inst : LE α_1
inst_1 : LE β_1
inst_2 : LE γ_1
inst_3 : LE δ_1
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst_4 : Preorder α
inst_5 : Preorder β
inst_6 : Preorder γ
inst_7 : Preorder δ
f : α ≃o γ
g : β ≃o δ
p q : α →o β
⊢ (∀ (x : γ),
      LE.le.{u_7} (α := β) ((p : (a : α) → β) ((f.symm : (a : γ) → α) x : α) : β)
        ((q : (a : α) → β) ((f.symm : (a : γ) → α) x : α) : β)) ↔
    ∀ (x : α), LE.le.{u_7} (α := β) ((p : (a : α) → β) x : β) ((q : (a : α) → β) x : β)

Tactic:
Iff.symm f.forall_congr_left

Premises used: Equiv.forall_congr_left, RelIso.toEquiv, Iff.symm
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ_1 : Type u_5
inst : LE α_1
inst_1 : LE β_1
inst_2 : LE γ_1
inst_3 : LE δ_1
α : Type u_6
β : Type u_7
γ : Type u_8
δ : Type u_9
inst_4 : Preorder α
inst_5 : Preorder β
inst_6 : Preorder γ
inst_7 : Preorder δ
f : α ≃o γ
g : β ≃o δ
p q : α →o β
⊢ (∀ (x : γ),
      LE.le.{u_7} (α := β) ((p : (a : α) → β) ((f.symm : (a : γ) → α) x : α) : β)
        ((q : (a : α) → β) ((f.symm : (a : γ) → α) x : α) : β)) ↔
    ∀ (x : α), LE.le.{u_7} (α := β) ((p : (a : α) → β) x : β) ((q : (a : α) → β) x : β)

Tactic:
exact Iff.symm f.forall_congr_left

Premises used: Equiv.forall_congr_left, RelIso.toEquiv, Iff.symm
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ : Type u_5
inst : LE α_1
inst_1 : LE β_1
inst_2 : LE γ_1
inst_3 : LE δ
α : Type u_6
β : Type u_7
γ : Type u_8
inst_4 : LE α
inst_5 : LE β
inst_6 : LE γ
x x_1 : (α × β) × γ
fst : α
snd : β
snd_1 : γ
fst_1 : α
snd_2 : β
snd_3 : γ
⊢ LE.le (α := α × β × γ) ((Equiv.prodAssoc α β γ : (a : (α × β) × γ) → α × β × γ) ((fst, snd), snd_1) : α × β × γ)
      ((Equiv.prodAssoc α β γ : (a : (α × β) × γ) → α × β × γ) ((fst_1, snd_2), snd_3) : α × β × γ) ↔
    ((fst, snd), snd_1) ≤ ((fst_1, snd_2), snd_3)

Tactic:
simp [Equiv.prodAssoc, and_assoc]

Premises used: and_assoc, Equiv.prodAssoc
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
⊢ Eq (α := (a : α × β) → β × α) (⇑prodComm : (a : α × β) → β × α) Prod.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
⊢ Eq (α := β × α ≃o α × β) (symm prodComm) prodComm

Tactic:
rfl

Premises used: OrderIso.prodComm, Equiv.prodComm, RelIso.symm, Prod.swap, Equiv.symm, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : LE α
⊢ Eq (α := (a : α) → αᵒᵈᵒᵈ) (⇑(dualDual α) : (a : α) → αᵒᵈᵒᵈ)
    (Function.comp (β := αᵒᵈ) (⇑toDual : (a : αᵒᵈ) → αᵒᵈᵒᵈ) (⇑toDual : (a : α) → αᵒᵈ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : LE α
⊢ Eq (α := (a : αᵒᵈᵒᵈ) → α) (⇑(symm (dualDual α)) : (a : αᵒᵈᵒᵈ) → α)
    (Function.comp (β := αᵒᵈ) (⇑ofDual : (a : αᵒᵈ) → α) (⇑ofDual : (a : αᵒᵈᵒᵈ) → αᵒᵈ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : LE α
a : α
⊢ Eq (α := αᵒᵈᵒᵈ) ((dualDual α : (a : α) → αᵒᵈᵒᵈ) a : αᵒᵈᵒᵈ)
    ((toDual : (a : αᵒᵈ) → αᵒᵈᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) : αᵒᵈᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : LE α
a : αᵒᵈᵒᵈ
⊢ Eq (α := α) ((symm (dualDual α) : (a : αᵒᵈᵒᵈ) → α) a : α)
    ((ofDual : (a : αᵒᵈ) → α) ((ofDual : (a : αᵒᵈᵒᵈ) → αᵒᵈ) a : αᵒᵈ) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
x y : α
⊢ LE.le.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
e.map_rel_iff

Premises used: RelIso.map_rel_iff
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
x : α
y : β
⊢ x ≤ (e.symm : (a : β) → α) y ↔ (e : (a : α) → β) x ≤ y

Tactic:
e.rel_symm_apply

Premises used: RelIso.rel_symm_apply
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ Monotone.{u_2, u_3} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.toOrderEmbedding.monotone

Premises used: OrderEmbedding.monotone, OrderIso.toOrderEmbedding
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ StrictMono.{u_2, u_3} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.toOrderEmbedding.strictMono

Premises used: OrderIso.toOrderEmbedding, OrderEmbedding.strictMono
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
x y : α
⊢ LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
e.toOrderEmbedding.lt_iff_lt

Premises used: OrderIso.toOrderEmbedding, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
x : α
y : β
rw :
  LT.lt.{u_3} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) ((e.symm : (a : β) → α) y : α) : β) ↔
    (e : (a : α) → β) x < y
rw₁ rw₂ : (e : (a : α) → β) x < y ↔ (e : (a : α) → β) x < y
⊢ x < (e.symm : (a : β) → α) y ↔ (e : (a : α) → β) x < y

Tactic:
rw [← e.lt_iff_lt, e.apply_symm_apply]

Premises used: OrderIso.lt_iff_lt, OrderIso.apply_symm_apply
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
x : α
⊢ Eq.{u_3 + 1} (α := β) ((e.toRelIsoLT : (a : α) → β) x : β) ((e : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ e.symm.toRelIsoLT = e.toRelIsoLT.symm (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2)

Tactic:
rfl

Premises used: OrderIso.toRelIsoLT, RelIso.symm, Equiv.symm, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ Eq (α := (a : α) → β) (⇑e.toRelIsoLT : (a : α) → β) (⇑e : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ Eq (α := (a : β) → α)
    (⇑(e.toRelIsoLT.symm (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2)) : (a : β) → α)
    (⇑e.symm : (a : β) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : PartialOrder α
inst_3 : PartialOrder β
e : (fun (x1 x2 : α) ↦ x1 < x2) ≃r fun (x1 x2 : β) ↦ x1 < x2
⊢ ∀ {a b : α},
    LE.le.{u_7} (α := β)
        ((e.toEquiv (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a : β)
        ((e.toEquiv (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) b : β) ↔
      a ≤ b

Tactic:
simp [le_iff_eq_or_lt, e.map_rel_iff, e.injective.eq_iff]

Premises used: le_iff_eq_or_lt, Function.Injective.eq_iff, RelIso.injective, RelIso.map_rel_iff
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : PartialOrder α
inst_1 : PartialOrder β
e : (fun (x1 x2 : α) ↦ x1 < x2) ≃r fun (x1 x2 : β) ↦ x1 < x2
x : α
⊢ Eq.{u_7 + 1} (α := β) ((ofRelIsoLT e : (a : α) → β) x : β) ((e : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : PartialOrder α
inst_1 : PartialOrder β
e : (fun (x1 x2 : α) ↦ x1 < x2) ≃r fun (x1 x2 : β) ↦ x1 < x2
⊢ (ofRelIsoLT e).symm = ofRelIsoLT (e.symm (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2))

Tactic:
rfl

Premises used: RelIso.symm, OrderIso.symm, OrderIso.ofRelIsoLT, Equiv.symm, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : PartialOrder α
inst_1 : PartialOrder β
e : α ≃o β
h : ∀ (x : α), Eq.{u_7 + 1} (α := β) ((ofRelIsoLT e.toRelIsoLT : (a : α) → β) x : β) ((e : (a : α) → β) x : β)
⊢ ofRelIsoLT e.toRelIsoLT = e

Tactic:
ext
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : PartialOrder α
inst_1 : PartialOrder β
e : α ≃o β
x : α
⊢ Eq.{u_7 + 1} (α := β) ((ofRelIsoLT e.toRelIsoLT : (a : α) → β) x : β) ((e : (a : α) → β) x : β)

Tactic:
simp
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : PartialOrder α
inst_1 : PartialOrder β
e : (fun (x1 x2 : α) ↦ x1 < x2) ≃r fun (x1 x2 : β) ↦ x1 < x2
h : ∀ (x : α), Eq.{u_7 + 1} (α := β) (((ofRelIsoLT e).toRelIsoLT : (a : α) → β) x : β) ((e : (a : α) → β) x : β)
⊢ (ofRelIsoLT e).toRelIsoLT = e

Tactic:
ext
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : PartialOrder α
inst_1 : PartialOrder β
e : (fun (x1 x2 : α) ↦ x1 < x2) ≃r fun (x1 x2 : β) ↦ x1 < x2
x : α
⊢ Eq.{u_7 + 1} (α := β) (((ofRelIsoLT e).toRelIsoLT : (a : α) → β) x : β) ((e : (a : α) → β) x : β)

Tactic:
simp
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
a : α
rw : cmp a (g (f a)) = Ordering.eq
rw₁ : cmp (f a) (f a) = Ordering.eq
rw₂ rw₃ : Ordering.eq = Ordering.eq
⊢ a = g (f a)

Tactic:
rw [← cmp_eq_eq_iff, h, cmp_self_eq_eq]

Premises used: cmp_self_eq_eq, cmp_eq_eq_iff
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
x : β
rw : cmp (f (g x)) x = Ordering.eq
rw₁ : cmp (g x) (g x) = Ordering.eq
rw₂ rw₃ : Ordering.eq = Ordering.eq
⊢ f (g x) = x

Tactic:
rw [← cmp_eq_eq_iff, ← h, cmp_self_eq_eq]

Premises used: cmp_self_eq_eq, cmp_eq_eq_iff
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
h₁ :
  cmp.{u_7} (α := β) (({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : α ≃ β } : (a : α) → β) a : β)
      (({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : α ≃ β } : (a : α) → β) b : β) =
    cmp a b
⊢ LE.le.{u_7} (α := β) (({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : α ≃ β } : (a : α) → β) a : β)
      (({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : α ≃ β } : (a : α) → β) b : β) ↔
    a ≤ b

Tactic:
apply le_iff_le_of_cmp_eq_cmp

Premises used: le_iff_le_of_cmp_eq_cmp
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
⊢ cmp (f a) (f b) = cmp a (g (f b))

Tactic:
(h a (f b)).symm

Premises used: Eq.symm
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a b : α
h₁ : b = g (f b)
⊢ cmp.{u_7} (α := β) (({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : α ≃ β } : (a : α) → β) a : β)
      (({ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ : α ≃ β } : (a : α) → β) b : β) =
    cmp a b

Tactic:
convert! (h a (f b)).symm

Premises used: Eq.symm
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α_1 : Type u_2
β_1 : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α_1
inst_1 : Preorder β_1
α : Type u_6
β : Type u_7
inst_2 : LinearOrder α
inst_3 : 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)

Tactic:
apply gf