awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f g : α →o β
⊢ f ≤ g ↔ ∀ (x : α), LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f g : α →o β
⊢ LE.le (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β) ↔ f ≤ g

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : Monotone f
hg : Monotone g
⊢ { toFun := f, monotone' := hf : α →o β } ≤ { toFun := g, monotone' := hg } ↔ f ≤ g

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f g : α →o β
x y : α
h₁ : f ≤ g
h₂ : x ≤ y
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) y : β)

Tactic:
(h₁ x).trans <| g.mono h₂

Premises used: OrderHom.mono, LE.le.trans
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
⊢ ∀ {a b : α × β →o γ},
    LE.le (α := α →o β →o γ)
        (({
                toFun := fun (f : α × β →o γ) ↦
                  { toFun := fun (x : α) ↦ { toFun := Function.curry (⇑f : (a : α × β) → γ) x, monotone' := ⋯ },
                    monotone' := ⋯ },
                invFun := fun (f : α →o β →o γ) ↦
                  { toFun := Function.uncurry fun (x : α) ↦ (⇑((f : (a : α) → β →o γ) x : β →o γ) : (a : β) → γ),
                    monotone' := ⋯ },
                left_inv := ⋯, right_inv := ⋯ } :
              (a : α × β →o γ) → α →o β →o γ)
            a :
          α →o β →o γ)
        (({
                toFun := fun (f : α × β →o γ) ↦
                  { toFun := fun (x : α) ↦ { toFun := Function.curry (⇑f : (a : α × β) → γ) x, monotone' := ⋯ },
                    monotone' := ⋯ },
                invFun := fun (f : α →o β →o γ) ↦
                  { toFun := Function.uncurry fun (x : α) ↦ (⇑((f : (a : α) → β →o γ) x : β →o γ) : (a : β) → γ),
                    monotone' := ⋯ },
                left_inv := ⋯, right_inv := ⋯ } :
              (a : α × β →o γ) → α →o β →o γ)
            b :
          α →o β →o γ) ↔
      a ≤ b

Tactic:
simp [le_def]

Premises used: OrderHom.le_def
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α × β →o γ
x : α
y : β
⊢ Eq.{u_4 + 1} (α := γ)
    ((((((curry : (a : α × β →o γ) → α →o β →o γ) f : α →o β →o γ) : (a : α) → β →o γ) x : β →o γ) : (a : β) → γ) y : γ)
    ((f : (a : α × β) → γ) (x, y) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α →o β →o γ
x : α × β
⊢ Eq.{u_4 + 1} (α := γ)
    ((((RelIso.symm (r := fun (x1 x2 : α × β →o γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : α →o β →o γ) ↦ x1 ≤ x2) curry :
                (a : α →o β →o γ) → α × β →o γ)
              f :
            α × β →o γ) :
          (a : α × β) → γ)
        x :
      γ)
    ((((f : (a : α) → β →o γ) x.1 : β →o γ) : (a : β) → γ) x.2 : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g₁ g₂ : β →o γ
hg : g₁ ≤ g₂
f₁ f₂ : α →o β
hf : f₁ ≤ f₂
⊢ g₁.comp f₁ ≤ g₂.comp f₂

Tactic:
fun _ => (hg _).trans (g₂.mono <| hf _)

Premises used: OrderHom.mono, LE.le.trans, DFunLike.coe
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
hg : Monotone g
hf : Monotone f
⊢ { toFun := g, monotone' := hg : β →o γ }.comp { toFun := f, monotone' := hf : α →o β } =
    { toFun := g ∘ f, monotone' := ⋯ }

Tactic:
rfl

Premises used: OrderHom.comp, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((f.comp id : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
⊢ f.comp id = f

Tactic:
ext
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
x : α
⊢ Eq.{u_3 + 1} (α := β) ((f.comp id : (a : α) → β) x : β) ((f : (a : α) → β) x : β)

Tactic:
rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((comp id f : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
⊢ comp id f = f

Tactic:
ext
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
x : α
⊢ Eq.{u_3 + 1} (α := β) ((comp id f : (a : α) → β) x : β) ((f : (a : α) → β) x : β)

Tactic:
rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
f : γ →o δ
g : β →o γ
h : α →o β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: OrderHom.comp, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α →o β
c : γ
⊢ Eq (α := α →o γ) (comp ((const β : (a : γ) → β →o γ) c) f) ((const α : (a : γ) → α →o γ) c)

Tactic:
rfl

Premises used: OrderHom.comp, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
γ : Type u_6
inst_2 : Preorder γ
f : α →o β
c : α
⊢ Eq (α := γ →o β) (f.comp ((const γ : (a : α) → γ →o α) c)) ((const γ : (a : β) → γ →o β) ((f : (a : α) → β) c))

Tactic:
rfl

Premises used: OrderHom.comp, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f₁ f₂ : α →o β
hf : f₁ ≤ f₂
g₁ g₂ : α →o γ
hg : g₁ ≤ g₂
⊢ f₁.prod g₁ ≤ f₂.prod g₂

Tactic:
fun _ => Prod.le_def.2 ⟨hf _, hg _⟩

Premises used: Iff.mpr, And.intro, Prod.le_def
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f₁ f₂ : β →o γ
g : α →o β
⊢ (f₁.comp g).prod (f₂.comp g) = (f₁.prod f₂).comp g

Tactic:
rfl

Premises used: OrderHom.comp, OrderHom.prod, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
h :
  ∀ (x : α) (y : β),
    Eq (α := α × β) ((OrderHom.prod fst snd : (a : α × β) → α × β) (x, y) : α × β)
      ((id : (a : α × β) → α × β) (x, y) : α × β)
⊢ Eq (α := α × β →o α × β) (OrderHom.prod fst snd) id

Tactic:
ext ⟨x, y⟩ : 2
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x : α
y : β
⊢ Eq (α := α × β) ((OrderHom.prod fst snd : (a : α × β) → α × β) (x, y) : α × β)
    ((id : (a : α × β) → α × β) (x, y) : α × β)

Tactic:
rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α →o β
g : α →o γ
⊢ comp fst (f.prod g) = f

Tactic:
ext _ _ rfl

Premises used: OrderHom.ext, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α →o β
g : α →o γ
⊢ comp snd (f.prod g) = g

Tactic:
ext _ _ rfl

Premises used: OrderHom.ext, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
ι : Type u_6
π : ι → Type u_7
inst_4 : (i : ι) → Preorder (π i)
p q : α → Prop
h : ∀ (a : α), p a → q a
⊢ ∀ {a b : { x : α // p x }},
    LE.le (α := { x : α // q x })
        ((Subtype.impEmbedding p q h : (a : { x : α // p x }) → { x : α // q x }) a : { x : α // q x })
        ((Subtype.impEmbedding p q h : (a : { x : α // p x }) → { x : α // q x }) b : { x : α // q x }) ↔
      a ≤ b

Tactic:
aesop
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Subsingleton α
g : α →o α
⊢ g = id

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : Preorder α
⊢ Eq.{u_2 + 1} (α := αᵒᵈ →o αᵒᵈ) ((OrderHom.dual : (a : α →o α) → αᵒᵈ →o αᵒᵈ) id : αᵒᵈ →o αᵒᵈ) (id : αᵒᵈ →o αᵒᵈ)

Tactic:
rfl

Premises used: OrderHom.id, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β →o γ
f : α →o β
⊢ Eq (α := OrderHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    ((OrderHom.dual : (a : α →o γ) → αᵒᵈ →o γᵒᵈ) (g.comp f) : OrderHom.{u_2, u_4} αᵒᵈ γᵒᵈ)
    (comp.{u_2, u_3, u_4} (β := βᵒᵈ) ((OrderHom.dual : (a : β →o γ) → βᵒᵈ →o γᵒᵈ) g)
        ((OrderHom.dual : (a : α →o β) → αᵒᵈ →o βᵒᵈ) f) :
      OrderHom.{u_2, u_4} αᵒᵈ γᵒᵈ)

Tactic:
rfl

Premises used: OrderHom.comp, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : Preorder α
⊢ Eq.{u_2 + 1} (α := α →o α) ((Equiv.symm OrderHom.dual : (a : αᵒᵈ →o αᵒᵈ) → α →o α) id : α →o α) (id : α →o α)

Tactic:
rfl

Premises used: OrderHom.id, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : OrderHom.{u_3, u_4} βᵒᵈ γᵒᵈ
f : OrderHom.{u_2, u_3} αᵒᵈ βᵒᵈ
⊢ Eq (α := α →o γ) ((Equiv.symm OrderHom.dual : (a : αᵒᵈ →o γᵒᵈ) → α →o γ) (g.comp f) : α →o γ)
    (comp.{u_2, u_3, u_4} (β := β) ((Equiv.symm OrderHom.dual : (a : βᵒᵈ →o γᵒᵈ) → β →o γ) g)
        ((Equiv.symm OrderHom.dual : (a : αᵒᵈ →o βᵒᵈ) → α →o β) f) :
      α →o γ)

Tactic:
rfl

Premises used: OrderHom.comp, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
⊢ f.uliftLeftMap.uliftRightMap = f.uliftMap

Tactic:
rfl

Premises used: OrderHom.uliftMap, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
⊢ f.uliftRightMap.uliftLeftMap = f.uliftMap

Tactic:
rfl

Premises used: OrderHom.uliftMap, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ↪r fun (x1 x2 : β) ↦ x1 < x2
⊢ ∀ {a b : α},
    LE.le.{u_3} (α := β)
        ((f.toEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a : β)
        ((f.toEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) b : β) ↔
      a ≤ b

Tactic:
simp [le_iff_lt_or_eq, f.map_rel_iff, f.injective.eq_iff]

Premises used: RelEmbedding.injective, Function.Injective.eq_iff, RelEmbedding.map_rel_iff, le_iff_lt_or_eq
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ↪r fun (x1 x2 : β) ↦ x1 < x2
x : α
⊢ Eq.{u_3 + 1} (α := β) ((f.orderEmbeddingOfLTEmbedding : (a : α) → β) x : β) ((f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : LE α
⊢ Eq (α := (a : α) → α) (⇑(id α) : (a : α) → α) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : LE α
⊢ RelEmbedding.toEmbedding (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : α) ↦ x1 ≤ x2) (id α) =
    Function.Embedding.refl α

Tactic:
rfl

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

Tactic:
rfl

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

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

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

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

Tactic:
rfl
-- 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.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: Function.Embedding.trans, RelEmbedding.trans, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
⊢ ∀ {a b : α},
    LT.lt.{u_3} (α := β)
        ((f.toEmbedding (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2) : (a : α) → β) a : β)
        ((f.toEmbedding (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2) : (a : α) → β) b : β) ↔
      a < b

Tactic:
simp [lt_iff_le_not_ge, f.map_rel_iff]

Premises used: lt_iff_le_not_ge, RelEmbedding.map_rel_iff
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
x : α
⊢ Eq.{u_3 + 1} (α := β) ((f.ltEmbedding : (a : α) → β) x : β) ((f : (a : α) → β) x : β)

Tactic:
rfl

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

Tactic:
f.map_rel_iff

Premises used: RelEmbedding.map_rel_iff
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
a b : α
⊢ LT.lt.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) ↔ a < b

Tactic:
f.ltEmbedding.map_rel_iff

Premises used: RelEmbedding.map_rel_iff, OrderEmbedding.ltEmbedding
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
a b : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) ↔ a = b

Tactic:
f.injective.eq_iff

Premises used: RelEmbedding.injective, Function.Injective.eq_iff
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
⊢ Monotone.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
OrderHomClass.monotone f

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

Tactic:
fun _ _ => f.lt_iff_lt.2

Premises used: Iff.mpr, StrictMono, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
a : α
⊢ Acc.{u_3 + 1} (α := β) (fun (x1 x2 : β) ↦ x1 < x2) ((f : (a : α) → β) a : β) → Acc (fun (x1 x2 : α) ↦ x1 < x2) a

Tactic:
f.ltEmbedding.acc a

Premises used: OrderEmbedding.ltEmbedding, RelEmbedding.acc
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α ↪o β
⊢ (WellFounded fun (x1 x2 : β) ↦ x1 < x2) → WellFounded fun (x1 x2 : α) ↦ x1 < x2

Tactic:
f.ltEmbedding.wellFounded

Premises used: RelEmbedding.wellFounded, OrderEmbedding.ltEmbedding
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : IsWellOrder β fun (x1 x2 : β) ↦ x1 < x2
f : α ↪o β
⊢ IsWellOrder α fun (x1 x2 : α) ↦ x1 < x2

Tactic:
f.ltEmbedding.isWellOrder

Premises used: RelEmbedding.isWellOrder, OrderEmbedding.ltEmbedding
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : PartialOrder α
inst_1 : Preorder β
f : α → β
h : ∀ (a b : α), f a ≤ f b ↔ a ≤ b
⊢ (⇑(ofMapLEIff f h) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
h : StrictMono f
⊢ (⇑(ofStrictMono f h) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : Preorder α
p : α → Prop
x : Subtype p
⊢ (subtype p : (a : Subtype p) → α) x = (↑x : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : Preorder α
p : α → Prop
⊢ Function.Injective (α := Subtype p) (β := α) (⇑(subtype p) : (a : Subtype p) → α)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : Preorder α
p : α → Prop
⊢ Eq (α := (a : Subtype p) → α) (⇑(subtype p) : (a : Subtype p) → α) (Subtype.val (p := p))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : IsEmpty α
⊢ Eq (α := (a : α) → β) (⇑ofIsEmpty : (a : α) → β) fun (a : α) ↦ isEmptyElim (p := fun (x : α) ↦ β) a

Tactic:
rfl

Premises used: isEmptyElim, False.elim, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
f : α ↪o β
inst_2 : OrderBot α
inst_3 : OrderBot β
a₁ a₂ : α
h : Disjoint.{u_3} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a₂ : β)
x : α
h₁ : x ≤ a₁
h₂ : x ≤ a₂
rw :
  ∀ (h₁ : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a₁ : β))
    (h₂ : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a₂ : β)),
    LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) ⊥ : β)
⊢ x ≤ ⊥

Tactic:
rw [← f.le_iff_le] at h₁ h₂ ⊢

Premises used: OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
f : α ↪o β
inst_2 : OrderBot α
inst_3 : OrderBot β
a₁ a₂ : α
h : Disjoint.{u_3} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a₂ : β)
x : α
h₁ : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a₁ : β)
h₂ : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a₂ : β)
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) (⊥ : β)

Tactic:
h h₁ h₂
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
f : α ↪o β
inst_2 : OrderBot α
inst_3 : OrderBot β
a₁ a₂ : α
h : Disjoint.{u_3} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a₂ : β)
x : α
h₁ : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a₁ : β)
h₂ : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a₂ : β)
⊢ LE.le.{u_3} (α := β) (⊥ : β) ((f : (a : α) → β) ⊥ : β)

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
f : α ↪o β
inst_2 : OrderBot α
inst_3 : OrderBot β
a₁ a₂ : α
h : Disjoint.{u_3} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a₂ : β)
x : α
h₁ : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a₁ : β)
h₂ : LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a₂ : β)
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) ⊥ : β)

Tactic:
calc
    f x ≤ ⊥ := h h₁ h₂
    _ ≤ f ⊥ := bot_le

Premises used: Bot.bot, DFunLike.coe, bot_le
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
f : α ↪o β
inst_2 : OrderTop α
inst_3 : OrderTop β
a₁ a₂ : α
⊢ Codisjoint.{u_3} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a₂ : β) → Codisjoint a₁ a₂

Tactic:
Disjoint.of_orderEmbedding (α := αᵒᵈ) (β := βᵒᵈ) f.dual

Premises used: Codisjoint, OrderDual, OrderEmbedding.dual, Disjoint.of_orderEmbedding
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
f : α ↪o β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
a₁ a₂ : α
⊢ IsCompl.{u_3} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a₂ : β) → IsCompl a₁ a₂

Tactic:
fun ⟨hd, hcd⟩ ↦
  ⟨Disjoint.of_orderEmbedding f hd, Codisjoint.of_orderEmbedding f hcd⟩

Premises used: IsCompl, _private.0.IsCompl.of_orderEmbedding.match_1, Codisjoint.of_orderEmbedding, IsCompl.mk, Disjoint.of_orderEmbedding
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ↪r fun (x1 x2 : β) ↦ x1 < x2
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β)
    (⇑f.toRelHom (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2).toOrderHom : (a : α) → β)

Tactic:
fun _ _ h => f.injective h

Premises used: RelEmbedding.injective, Function.Injective
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
f : α ≃o β
⊢ f.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2).toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
f g : α ≃o β
h : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
⊢ f = g

Tactic:
DFunLike.coe_injective h

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
⊢ Eq (α := (a : α) → β) (⇑e.toOrderEmbedding : (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 β
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.toEquiv.bijective

Premises used: Equiv.bijective, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.toEquiv.injective

Premises used: Equiv.injective, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.toEquiv.surjective

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

Tactic:
e.toEquiv.apply_eq_iff_eq

Premises used: RelIso.toEquiv, Equiv.apply_eq_iff_eq
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : LE α
⊢ Eq (α := (a : α) → α) (⇑(refl α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : LE α
x : α
⊢ (refl α : (a : α) → α) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
inst : LE α
⊢ RelIso.toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : α) ↦ x1 ≤ x2) (refl α) = Equiv.refl α

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : LE α
inst_1 : LE β
inst_2 : LE γ
inst_3 : LE δ
e : α ≃ β
map_rel_iff' : ∀ {a b : α}, LE.le.{u_3} (α := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β) ↔ a ≤ b
⊢ ∀ {a b : β}, LE.le.{u_2} (α := α) ((e.symm : (a : β) → α) a : α) ((e.symm : (a : β) → α) b : α) ↔ a ≤ b

Tactic:
simp [← map_rel_iff']