awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 β
g : β →o α
h₁ : f.comp g = OrderHom.id
h₂ : g.comp f = OrderHom.id
a b : α
h :
  LE.le.{u_3} (α := β)
    (({ toFun := (⇑f : (a : α) → β), invFun := (⇑g : (a : β) → α), left_inv := ⋯, right_inv := ⋯ : α ≃ β } :
          (a : α) → β)
        a :
      β)
    (({ toFun := (⇑f : (a : α) → β), invFun := (⇑g : (a : β) → α), left_inv := ⋯, right_inv := ⋯ : α ≃ β } :
          (a : α) → β)
        b :
      β)
⊢ a ≤ b

Tactic:
simpa [h₂] using show g.comp f _ ≤ g.comp f _ from map_rel g h

Premises used: RelHomClass.map_rel
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
f : α →o β
g : β →o α
h₁ : f.comp g = OrderHom.id
h₂ : g.comp f = OrderHom.id
a : β
⊢ Eq.{u_2 + 1} (α := α) (((ofHomInv f g h₁ h₂).symm : (a : β) → α) a : α) ((g : (a : β) → α) 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 : Unique α
inst_3 : Preorder β
⊢ ∀ {a b : α → β},
    LE.le.{u_7} (α := β) ((Equiv.funUnique α β : (a : α → β) → β) a : β)
        ((Equiv.funUnique α β : (a : α → β) → β) b : β) ↔
      a ≤ b

Tactic:
simp [Pi.le_def, Unique.forall_iff]

Premises used: Unique.forall_iff, Pi.le_def
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : Unique α
inst_1 : Preorder β
⊢ Eq (α := (a : β) → α → β) (⇑(symm (funUnique α β)) : (a : β) → α → β) (Function.const α)

Tactic:
rfl

Premises used: Eq.mpr, uniqueElim, 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 : Unique α
inst_3 : Unique β
inst_4 : Preorder α
inst_5 : Preorder β
⊢ ∀ {a b : α},
    LE.le.{u_7} (α := β) ((Equiv.ofUnique α β : (a : α) → β) a : β) ((Equiv.ofUnique α β : (a : α) → β) b : β) ↔ a ≤ b

Tactic:
simp
-- 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 β
e : α ≃ β
h₁ : Monotone.{u_2, u_3} (α := α) (β := β) (⇑e : (a : α) → β)
h₂ : Monotone.{u_3, u_2} (α := β) (β := α) (⇑e.symm : (a : β) → α)
a b : α
h : LE.le.{u_3} (α := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β)
⊢ a ≤ b

Tactic:
simpa only [e.symm_apply_apply] using h₂ h

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
e : α ≃ β
h₁ : Monotone.{u_2, u_3} (α := α) (β := β) (⇑e : (a : α) → β)
h₂ : Monotone.{u_3, u_2} (α := β) (β := α) (⇑e.symm : (a : β) → α)
⊢ Eq (α := (a : α) → β) (⇑(e.toOrderIso h₁ h₂) : (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 : α ≃ β
h₁ : Monotone.{u_2, u_3} (α := α) (β := β) (⇑e : (a : α) → β)
h₂ : Monotone.{u_3, u_2} (α := β) (β := α) (⇑e.symm : (a : β) → α)
⊢ (e.toOrderIso h₁ h₂).toEquiv (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (s := fun (x1 x2 : β) ↦ x1 ≤ x2) = e

Tactic:
rfl

Premises used: rfl
-- 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.dual : (a : αᵒᵈ) → βᵒᵈ) x : βᵒᵈ)
    ((toDual : (a : β) → βᵒᵈ) ((f : (a : α) → β) ((ofDual : (a : αᵒᵈ) → α) x : α) : β) : βᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
f : α ≃o β
x : βᵒᵈ
⊢ Eq.{u_2 + 1} (α := αᵒᵈ) ((f.dual.symm : (a : βᵒᵈ) → αᵒᵈ) x : αᵒᵈ)
    ((toDual : (a : α) → αᵒᵈ) ((f.symm : (a : β) → α) ((ofDual : (a : βᵒᵈ) → β) x : β) : α) : αᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
f : α ≃o β
⊢ f.symm.dual = f.dual.symm

Tactic:
rfl

Premises used: RelIso.symm, OrderIso.symm, OrderDual, Equiv.symm, rfl
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ (f : (a : α) → β) x = y

Tactic:
le_antisymm ?_ (hy _)

Premises used: le_antisymm
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
refine : (f : (a : α) → β) x ≤ y
⊢ (f : (a : α) → β) x = y

Tactic:
refine le_antisymm ?_ (hy _)

Premises used: le_antisymm
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
rw : x ≤ (f.symm : (a : β) → α) y
⊢ (f : (a : α) → β) x ≤ y

Tactic:
rw [← f.apply_symm_apply y, f.le_iff_le]

Premises used: OrderIso.apply_symm_apply, OrderIso.le_iff_le
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ x ≤ (f.symm : (a : β) → α) y

Tactic:
apply hx
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
f : α ≃o β
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
f.map_bot' (fun _ => bot_le) fun _ => bot_le

Premises used: OrderIso.map_bot', bot_le
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
f : α ↪o β
x y : α
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) (x ⊓ y) : β) ((f : (a : α) → β) x ⊓ (f : (a : α) → β) y : β)

Tactic:
f.monotone.map_inf_le x y

Premises used: OrderEmbedding.monotone, Monotone.map_inf_le
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
f : α ≃o β
x y : α
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (x ⊓ y) : β) ((f : (a : α) → β) x ⊓ (f : (a : α) → β) y : β)

Tactic:
(f.toOrderEmbedding.map_inf_le x y).antisymm ?_

Premises used: OrderIso.toOrderEmbedding, LE.le.antisymm, OrderEmbedding.map_inf_le
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
f : α ≃o β
x y : α
refine :
  LE.le.{u_3} (α := β) ((f.toOrderEmbedding : (a : α) → β) x ⊓ (f.toOrderEmbedding : (a : α) → β) y : β)
    ((f.toOrderEmbedding : (a : α) → β) (x ⊓ y) : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (x ⊓ y) : β) ((f : (a : α) → β) x ⊓ (f : (a : α) → β) y : β)

Tactic:
refine (f.toOrderEmbedding.map_inf_le x y).antisymm ?_

Premises used: OrderIso.toOrderEmbedding, LE.le.antisymm, OrderEmbedding.map_inf_le
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
f : α ≃o β
x y : α
apply :
  LE.le.{u_2} (α := α)
    ((f.symm : (a : β) → α) ((f.toOrderEmbedding : (a : α) → β) x ⊓ (f.toOrderEmbedding : (a : α) → β) y : β) : α)
    ((f.symm : (a : β) → α) ((f.toOrderEmbedding : (a : α) → β) (x ⊓ y) : β) : α)
⊢ LE.le.{u_3} (α := β) ((f.toOrderEmbedding : (a : α) → β) x ⊓ (f.toOrderEmbedding : (a : α) → β) y : β)
    ((f.toOrderEmbedding : (a : α) → β) (x ⊓ y) : β)

Tactic:
apply f.symm.le_iff_le.1

Premises used: OrderIso.le_iff_le, OrderIso.symm, Iff.mp
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
f : α ≃o β
x y : α
⊢ LE.le.{u_2} (α := α)
    ((f.symm : (a : β) → α) ((f.toOrderEmbedding : (a : α) → β) x ⊓ (f.toOrderEmbedding : (a : α) → β) y : β) : α)
    ((f.symm : (a : β) → α) ((f.toOrderEmbedding : (a : α) → β) (x ⊓ y) : β) : α)

Tactic:
simpa using f.symm.toOrderEmbedding.map_inf_le (f x) (f y)

Premises used: OrderIso.toOrderEmbedding, OrderIso.symm, OrderEmbedding.map_inf_le, DFunLike.coe
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
⊢ IsMax.{u_7} (α := β) ((f : (a : α) → β) x : β) ↔ IsMax x

Tactic:
⟨f.strictMono.isMax_of_apply, ?_⟩

Premises used: OrderIso.strictMono, StrictMono.isMax_of_apply, Iff.intro
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
refine : IsMax x → IsMax.{u_7} (α := β) ((f : (a : α) → β) x : β)
⊢ IsMax.{u_7} (α := β) ((f : (a : α) → β) x : β) ↔ IsMax x

Tactic:
refine ⟨f.strictMono.isMax_of_apply, ?_⟩
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
rw : IsMax.{u_6} (α := α) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β) : α)
| IsMax x

Tactic:
rw [← f.symm_apply_apply x]

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
conv_lhs :
  IsMax.{u_6} (α := α) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β) : α) →
    IsMax.{u_7} (α := β) ((f : (a : α) → β) x : β)
⊢ IsMax x → IsMax.{u_7} (α := β) ((f : (a : α) → β) x : β)

Tactic:
conv_lhs => rw [← f.symm_apply_apply x]

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
⊢ IsMax.{u_6} (α := α) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β) : α) →
    IsMax.{u_7} (α := β) ((f : (a : α) → β) x : β)

Tactic:
f.symm.strictMono.isMax_of_apply

Premises used: OrderIso.strictMono, StrictMono.isMax_of_apply, OrderIso.symm
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_6
β : Type u_7
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : α
⊢ IsMax.{u_6} (α := α) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β) : α) →
    IsMax.{u_7} (α := β) ((f : (a : α) → β) x : β)

Tactic:
exact f.symm.strictMono.isMax_of_apply

Premises used: OrderIso.strictMono, StrictMono.isMax_of_apply, OrderIso.symm
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : SemilatticeInf β
inst_3 : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
rw : LE.le.{u_3} (α := β) ((f : (a : α) → β) (a ⊓ b) : β) ((f : (a : α) → β) ⊥ : β)
⊢ Disjoint.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
rw [disjoint_iff_inf_le, ← f.map_inf, ← f.map_bot]

Premises used: OrderIso.map_inf, disjoint_iff_inf_le, OrderIso.map_bot
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : SemilatticeInf β
inst_3 : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) (a ⊓ b) : β) ((f : (a : α) → β) ⊥ : β)

Tactic:
f.monotone ha.le_bot

Premises used: Disjoint.le_bot, OrderIso.monotone
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : SemilatticeInf β
inst_3 : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) (a ⊓ b) : β) ((f : (a : α) → β) ⊥ : β)

Tactic:
exact f.monotone ha.le_bot

Premises used: Disjoint.le_bot, OrderIso.monotone
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderTop α
inst_2 : SemilatticeSup β
inst_3 : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
rw : LE.le.{u_3} (α := β) ((f : (a : α) → β) ⊤ : β) ((f : (a : α) → β) (a ⊔ b) : β)
⊢ Codisjoint.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)

Tactic:
rw [codisjoint_iff_le_sup, ← f.map_sup, ← f.map_top]

Premises used: codisjoint_iff_le_sup, OrderIso.map_top, OrderIso.map_sup
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderTop α
inst_2 : SemilatticeSup β
inst_3 : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) ⊤ : β) ((f : (a : α) → β) (a ⊔ b) : β)

Tactic:
f.monotone ha.top_le

Premises used: OrderIso.monotone, Codisjoint.top_le
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderTop α
inst_2 : SemilatticeSup β
inst_3 : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ LE.le.{u_3} (α := β) ((f : (a : α) → β) ⊤ : β) ((f : (a : α) → β) (a ⊔ b) : β)

Tactic:
exact f.monotone ha.top_le

Premises used: OrderIso.monotone, Codisjoint.top_le
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : SemilatticeInf β
inst_3 : OrderBot β
a b : α
f : α ≃o β
⊢ Disjoint.{u_3} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) ↔ Disjoint a b

Tactic:
⟨fun h => f.symm_apply_apply a ▸ f.symm_apply_apply b ▸ h.map_orderIso f.symm,
   fun h => h.map_orderIso f⟩

Premises used: Eq.rec, OrderIso.symm, Iff.intro, Disjoint.map_orderIso, OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : α ≃o β
x y : α
h : IsCompl x y
⊢ IsCompl.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
⟨h.1.map_orderIso _, h.2.map_orderIso _⟩

Premises used: Codisjoint.map_orderIso, Disjoint.map_orderIso, IsCompl.mk, IsCompl.codisjoint, IsCompl.disjoint
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : α ≃o β
x y : α
⊢ IsCompl x y ↔ IsCompl.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
⟨f.isCompl, fun h => f.symm_apply_apply x ▸ f.symm_apply_apply y ▸ f.symm.isCompl h⟩

Premises used: OrderIso.isCompl, Eq.rec, OrderIso.symm, Iff.intro, OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
inst_4 : ComplementedLattice α
f : α ≃o β
x : β
obtain : ∀ (y : α) (hy : IsCompl ((f.symm : (a : β) → α) x) y), ∃ (b : β), IsCompl x b
⊢ ∃ (b : β), IsCompl x b

Tactic:
obtain ⟨y, hy⟩ := exists_isCompl (f.symm x)

Premises used: ComplementedLattice.exists_isCompl, OrderIso.symm, DFunLike.coe
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
inst_4 : ComplementedLattice α
f : α ≃o β
x : β
y : α
hy : IsCompl ((f.symm : (a : β) → α) x) y
⊢ IsCompl.{u_2} (α := α) ((f.symm : (a : β) → α) x : α) ((f.symm : (a : β) → α) ((f : (a : α) → β) y : β) : α)

Tactic:
rw [← f.symm_apply_apply y] at hy

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
inst_4 : ComplementedLattice α
f : α ≃o β
x : β
y : α
hy : IsCompl.{u_2} (α := α) ((f.symm : (a : β) → α) x : α) ((f.symm : (a : β) → α) ((f : (a : α) → β) y : β) : α)
⊢ ∃ (b : β), IsCompl x b

Tactic:
⟨f y, f.symm.isCompl_iff.2 hy⟩

Premises used: Iff.mpr, OrderIso.symm, Exists.intro, DFunLike.coe, OrderIso.isCompl_iff
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
inst_4 : ComplementedLattice α
f : α ≃o β
x : β
y : α
hy : IsCompl.{u_2} (α := α) ((f.symm : (a : β) → α) x : α) ((f.symm : (a : β) → α) ((f : (a : α) → β) y : β) : α)
⊢ ∃ (b : β), IsCompl x b

Tactic:
exact ⟨f y, f.symm.isCompl_iff.2 hy⟩
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : α ≃o β
h : ComplementedLattice α
⊢ ComplementedLattice β

Tactic:
f.complementedLattice

Premises used: OrderIso.complementedLattice
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : α ≃o β
h : ComplementedLattice α
⊢ ComplementedLattice β

Tactic:
exact f.complementedLattice

Premises used: OrderIso.complementedLattice
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : α ≃o β
h : ComplementedLattice β
⊢ ComplementedLattice α

Tactic:
f.symm.complementedLattice

Premises used: OrderIso.complementedLattice, OrderIso.symm
-- Module: Mathlib.Order.Hom.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : α ≃o β
h : ComplementedLattice β
⊢ ComplementedLattice α

Tactic:
exact f.symm.complementedLattice

Premises used: OrderIso.complementedLattice, OrderIso.symm
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
inst : LinearOrder X
inst_1 : DenselyOrdered X
inst_2 : Preorder Y
f : X → Y
hf : StrictMono f
dense : ∀ (a₁ a₂ : (↑(Set.range f) : Type u_7)), a₁ < a₂ → ∃ (a : (↑(Set.range f) : Type u_7)), a₁ < a ∧ a < a₂
⊢ DenselyOrdered.{u_7} (↑(Set.range f) : Type u_7)

Tactic:
constructor
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
inst : LinearOrder X
inst_1 : DenselyOrdered X
inst_2 : Preorder Y
f : X → Y
hf : StrictMono f
⊢ ∀ (a₁ a₂ : (↑(Set.range f) : Type u_7)), a₁ < a₂ → ∃ (a : (↑(Set.range f) : Type u_7)), a₁ < a ∧ a < a₂

Tactic:
simpa [← exists_and_left, ← exists_and_right, exists_comm, hf.lt_iff_lt]
    using fun _ _ ↦ exists_between

Premises used: StrictMono.lt_iff_lt, exists_and_left, exists_between, exists_and_right, exists_comm
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
mp : DenselyOrdered X → DenselyOrdered Y
mpr : DenselyOrdered Y → DenselyOrdered X
⊢ DenselyOrdered X ↔ DenselyOrdered Y

Tactic:
constructor
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
⊢ DenselyOrdered Y

Tactic:
⟨fun a b h ↦ ?_⟩

Premises used: DenselyOrdered.mk
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
mp : ∀ (a b : Y) (h : a < b), ∃ (a_1 : Y), a < a_1 ∧ a_1 < b
⊢ DenselyOrdered Y

Tactic:
refine ⟨fun a b h ↦ ?_⟩
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
a b : Y
h : a < b
mp : ∀ (c : X) (hc : EquivLike.inv f a < c ∧ c < EquivLike.inv f b), ∃ (a_1 : Y), a < a_1 ∧ a_1 < b
⊢ ∃ (a_1 : Y), a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c, hc⟩ := exists_between ((map_inv_lt_map_inv_iff f).mpr h)

Premises used: Iff.mpr, exists_between, map_inv_lt_map_inv_iff
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
a b : Y
h : a < b
c : X
hc : EquivLike.inv f a < c ∧ c < EquivLike.inv f b
⊢ a < (f : (a : X) → Y) c ∧ (f : (a : X) → Y) c < b

Tactic:
simpa using hc
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered X
a b : Y
h : a < b
c : X
hc : EquivLike.inv f a < c ∧ c < EquivLike.inv f b
⊢ ∃ (a_1 : Y), a < a_1 ∧ a_1 < b

Tactic:
exact ⟨f c, by simpa using hc⟩
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
⊢ DenselyOrdered X

Tactic:
⟨fun a b h ↦ ?_⟩

Premises used: DenselyOrdered.mk
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
mpr : ∀ (a b : X) (h : a < b), ∃ (a_1 : X), a < a_1 ∧ a_1 < b
⊢ DenselyOrdered X

Tactic:
refine ⟨fun a b h ↦ ?_⟩
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
a b : X
h : a < b
mpr : ∀ (c : Y) (hc : (f : (a : X) → Y) a < c ∧ c < (f : (a : X) → Y) b), ∃ (a_1 : X), a < a_1 ∧ a_1 < b
⊢ ∃ (a_1 : X), a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c, hc⟩ := exists_between ((map_lt_map_iff f).mpr h)

Premises used: Iff.mpr, exists_between, map_lt_map_iff
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
a b : X
h : a < b
c : Y
hc : (f : (a : X) → Y) a < c ∧ c < (f : (a : X) → Y) b
⊢ a < EquivLike.inv f c ∧ EquivLike.inv f c < b

Tactic:
simpa using hc
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : Preorder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
inst_3 : OrderIsoClass F X Y
f : F
H : DenselyOrdered Y
a b : X
h : a < b
c : Y
hc : (f : (a : X) → Y) a < c ∧ c < (f : (a : X) → Y) b
⊢ ∃ (a_1 : X), a < a_1 ∧ a_1 < b

Tactic:
exact ⟨EquivLike.inv f c, by simpa using hc⟩
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : LinearOrder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
f : F
hf : StrictAnti.{u_6, u_7} (α := X) (β := Y) (⇑f : (a : X) → Y)
rw : DenselyOrdered.{u_6} Xᵒᵈ ↔ DenselyOrdered Y
⊢ DenselyOrdered X ↔ DenselyOrdered Y

Tactic:
rw [← denselyOrdered_orderDual]

Premises used: denselyOrdered_orderDual
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : LinearOrder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
f : F
hf : StrictAnti.{u_6, u_7} (α := X) (β := Y) (⇑f : (a : X) → Y)
refine_2 : DenselyOrdered.{u_6} Xᵒᵈ ↔ DenselyOrdered Y
refine_1 :
  ∀ {a b : Xᵒᵈ},
    LE.le.{u_7} (α := Y) ((Equiv.trans ofDual (↑f : X ≃ Y) : (a : Xᵒᵈ) → Y) a : Y)
        ((Equiv.trans ofDual (↑f : X ≃ Y) : (a : Xᵒᵈ) → Y) b : Y) ↔
      a ≤ b
⊢ DenselyOrdered.{u_6} Xᵒᵈ ↔ DenselyOrdered Y

Tactic:
let e : Xᵒᵈ ≃o Y := ⟨OrderDual.ofDual.trans (f : X ≃ Y), ?_⟩
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : LinearOrder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
f : F
hf : StrictAnti.{u_6, u_7} (α := X) (β := Y) (⇑f : (a : X) → Y)
e : OrderIso.{u_6, u_7} Xᵒᵈ Y :=
  RelIso.mk (r := fun (x1 x2 : Xᵒᵈ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Y) ↦ x1 ≤ x2) (Equiv.trans ofDual (↑f : X ≃ Y)) ⋯
⊢ DenselyOrdered.{u_6} Xᵒᵈ ↔ DenselyOrdered Y

Tactic:
denselyOrdered_iff_of_orderIsoClass e

Premises used: denselyOrdered_iff_of_orderIsoClass
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : LinearOrder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
f : F
hf : StrictAnti.{u_6, u_7} (α := X) (β := Y) (⇑f : (a : X) → Y)
e : OrderIso.{u_6, u_7} Xᵒᵈ Y :=
  RelIso.mk (r := fun (x1 x2 : Xᵒᵈ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Y) ↦ x1 ≤ x2) (Equiv.trans ofDual (↑f : X ≃ Y)) ⋯
⊢ DenselyOrdered.{u_6} Xᵒᵈ ↔ DenselyOrdered Y

Tactic:
exact denselyOrdered_iff_of_orderIsoClass e

Premises used: denselyOrdered_iff_of_orderIsoClass
-- Module: Mathlib.Order.Hom.Basic
Goal:
X : Type u_6
Y : Type u_7
F : Type u_8
inst : LinearOrder X
inst_1 : Preorder Y
inst_2 : EquivLike F X Y
f : F
hf : StrictAnti.{u_6, u_7} (α := X) (β := Y) (⇑f : (a : X) → Y)
refine_1 : ∀ (a a_1 : X), LE.le.{u_7} (α := Y) ((f : (a : X) → Y) a : Y) ((f : (a : X) → Y) a_1 : Y) ↔ a_1 ≤ a
⊢ ∀ {a b : Xᵒᵈ},
    LE.le.{u_7} (α := Y) ((Equiv.trans ofDual (↑f : X ≃ Y) : (a : Xᵒᵈ) → Y) a : Y)
        ((Equiv.trans ofDual (↑f : X ≃ Y) : (a : Xᵒᵈ) → Y) b : Y) ↔
      a ≤ b

Tactic:
simp only [Equiv.trans_apply, EquivLike.coe_coe, OrderDual.forall, OrderDual.ofDual_toDual,
      OrderDual.toDual_le_toDual]

Premises used: OrderDual.toDual_le_toDual, Equiv.trans_apply, OrderDual.forall, OrderDual.ofDual_toDual, EquivLike.coe_coe