awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
f g : α ↪o β
rw : Eq (α := α → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β) ↔ f = g
rw₁ rw₂ : f = g ↔ f = g
⊢ Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      (range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β)) ↔
    f = g

Tactic:
rw [f.strictMono.range_inj g.strictMono, DFunLike.coe_fn_eq]

Premises used: OrderEmbedding.strictMono, StrictMono.range_inj, DFunLike.coe_fn_eq
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
⊢ Subsingleton (α ≃o β)

Tactic:
⟨fun f g ↦ ?_⟩

Premises used: Subsingleton.intro
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
refine : ∀ (f g : α ≃o β), f = g
⊢ Subsingleton (α ≃o β)

Tactic:
refine ⟨fun f g ↦ ?_⟩
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Preorder β
f g : α ≃o β
rw : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
rw₁ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g : (a : α) → β)
rw₂ : Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑g.toOrderEmbedding : (a : α) → β)
rw₃ : f.toOrderEmbedding = g.toOrderEmbedding
rw₄ :
  Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f.toOrderEmbedding : (a : α) → β))
    (range.{u_2, u_1 + 1} (ι := α) (⇑g.toOrderEmbedding : (a : α) → β))
rw₅ :
  Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (range.{u_2, u_1 + 1} (ι := α) (⇑g.toOrderEmbedding : (a : α) → β))
rw₆ :
  Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
rw₇ : Eq.{u_2 + 1} (α := Set β) univ (range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
rw₈ rw₉ : Eq.{u_2 + 1} (α := Set β) univ univ
⊢ f = g

Tactic:
rw [OrderIso.ext_iff, ← coe_toOrderEmbedding, ← coe_toOrderEmbedding, DFunLike.coe_fn_eq,
    ← OrderEmbedding.range_inj, coe_toOrderEmbedding, coe_toOrderEmbedding, range_eq, range_eq]

Premises used: OrderIso.range_eq, OrderIso.coe_toOrderEmbedding, DFunLike.coe_fn_eq, OrderEmbedding.range_inj, OrderIso.ext_iff
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedLT β
inst_2 : Preorder α
⊢ Subsingleton (α ≃o β)

Tactic:
⟨fun f g ↦ ?_⟩

Premises used: Subsingleton.intro
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedLT β
inst_2 : Preorder α
refine : ∀ (f g : α ≃o β), f = g
⊢ Subsingleton (α ≃o β)

Tactic:
refine ⟨fun f g ↦ ?_⟩
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedLT β
inst_2 : Preorder α
f g : α ≃o β
change : f.symm.symm = g.symm.symm
⊢ f = g

Tactic:
change f.symm.symm = g.symm.symm

Premises used: OrderIso.symm
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedLT β
inst_2 : Preorder α
f g : α ≃o β
rw : g.symm.symm = g.symm.symm
rw₁ : β ≃o α
rw₂ : g.symm.symm = g.symm.symm
rw₃ : β ≃o α
⊢ f.symm.symm = g.symm.symm

Tactic:
rw [Subsingleton.elim f.symm]

Premises used: OrderIso.symm, Subsingleton.elim
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedGT α
inst_2 : Preorder β
⊢ Subsingleton (α ≃o β)

Tactic:
⟨fun f g ↦ ?_⟩

Premises used: Subsingleton.intro
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedGT α
inst_2 : Preorder β
refine : ∀ (f g : α ≃o β), f = g
⊢ Subsingleton (α ≃o β)

Tactic:
refine ⟨fun f g ↦ ?_⟩
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedGT α
inst_2 : Preorder β
f g : α ≃o β
change : f.dual.dual = g.dual.dual
⊢ f = g

Tactic:
change f.dual.dual = g.dual.dual

Premises used: OrderIso.dual
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
inst_1 : WellFoundedGT α
inst_2 : Preorder β
f g : α ≃o β
rw : g.dual.dual = g.dual.dual
rw₁ : OrderIso.{u_1, u_2} αᵒᵈ βᵒᵈ
rw₂ : g.dual.dual = g.dual.dual
rw₃ : OrderIso.{u_1, u_2} αᵒᵈ βᵒᵈ
⊢ f.dual.dual = g.dual.dual

Tactic:
rw [Subsingleton.elim f.dual]

Premises used: OrderIso.dual, Subsingleton.elim
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedGT β
inst_2 : Preorder α
⊢ Subsingleton (α ≃o β)

Tactic:
⟨fun f g ↦ ?_⟩

Premises used: Subsingleton.intro
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedGT β
inst_2 : Preorder α
refine : ∀ (f g : α ≃o β), f = g
⊢ Subsingleton (α ≃o β)

Tactic:
refine ⟨fun f g ↦ ?_⟩
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedGT β
inst_2 : Preorder α
f g : α ≃o β
change : f.dual.dual = g.dual.dual
⊢ f = g

Tactic:
change f.dual.dual = g.dual.dual

Premises used: OrderIso.dual
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder β
inst_1 : WellFoundedGT β
inst_2 : Preorder α
f g : α ≃o β
rw : g.dual.dual = g.dual.dual
rw₁ : OrderIso.{u_1, u_2} αᵒᵈ βᵒᵈ
rw₂ : g.dual.dual = g.dual.dual
rw₃ : OrderIso.{u_1, u_2} αᵒᵈ βᵒᵈ
⊢ f.dual.dual = g.dual.dual

Tactic:
rw [Subsingleton.elim f.dual]

Premises used: OrderIso.dual, Subsingleton.elim
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x : α
y : (↑(Iic x) : Type u_1)
⊢ (fun (y : (↑(Iic ((e : (a : α) → β) x) : Set β) : Type u_2)) ↦
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iic x) ((e.symm : (a : β) → α) (↑y : β)) ⋯ :
          { x_1 : α // x_1 ∈ Iic x }))
      ((fun (y : (↑(Iic x) : Type u_1)) ↦
          (Subtype.mk (p := fun (x_1 : β) ↦ Membership.mem (γ := Set β) (Iic ((e : (a : α) → β) x) : Set β) x_1)
              ((e : (a : α) → β) (↑y : α)) ⋯ :
            { x_1 : β // Membership.mem (γ := Set β) (Iic ((e : (a : α) → β) x) : Set β) x_1 }))
        y) =
    y

Tactic:
simp
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x : α
y : (↑(Iic ((e : (a : α) → β) x) : Set β) : Type u_2)
⊢ (fun (y : (↑(Iic x) : Type u_1)) ↦
        (Subtype.mk (p := fun (x_1 : β) ↦ Membership.mem (γ := Set β) (Iic ((e : (a : α) → β) x) : Set β) x_1)
            ((e : (a : α) → β) (↑y : α)) ⋯ :
          { x_1 : β // Membership.mem (γ := Set β) (Iic ((e : (a : α) → β) x) : Set β) x_1 }))
      ((fun (y : (↑(Iic ((e : (a : α) → β) x) : Set β) : Type u_2)) ↦
          (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iic x) ((e.symm : (a : β) → α) (↑y : β)) ⋯ :
            { x_1 : α // x_1 ∈ Iic x }))
        y) =
    y

Tactic:
simp
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x : α
⊢ ∀ {a b : (↑(Iic x) : Type u_1)},
    LE.le.{u_2} (α := (↑(Iic ((e : (a : α) → β) x) : Set β) : Type u_2))
        (({
                toFun := fun (y : (↑(Iic x) : Type u_1)) ↦
                  Subtype.mk (p := fun (x_1 : β) ↦ Membership.mem (γ := Set β) (Iic ((e : (a : α) → β) x) : Set β) x_1)
                    ((e : (a : α) → β) (↑y : α)) ⋯,
                invFun := fun (y : (↑(Iic ((e : (a : α) → β) x) : Set β) : Type u_2)) ↦
                  Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iic x) ((e.symm : (a : β) → α) (↑y : β)) ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : (↑(Iic x) : Type u_1)) → (↑(Iic ((e : (a : α) → β) x)) : Type u_2))
            a :
          (↑(Iic ((e : (a : α) → β) x) : Set β) : Type u_2))
        (({
                toFun := fun (y : (↑(Iic x) : Type u_1)) ↦
                  Subtype.mk (p := fun (x_1 : β) ↦ Membership.mem (γ := Set β) (Iic ((e : (a : α) → β) x) : Set β) x_1)
                    ((e : (a : α) → β) (↑y : α)) ⋯,
                invFun := fun (y : (↑(Iic ((e : (a : α) → β) x) : Set β) : Type u_2)) ↦
                  Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iic x) ((e.symm : (a : β) → α) (↑y : β)) ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : (↑(Iic x) : Type u_1)) → (↑(Iic ((e : (a : α) → β) x)) : Type u_2))
            b :
          (↑(Iic ((e : (a : α) → β) x) : Set β) : Type u_2)) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x : α
y : (↑(Ici x) : Type u_1)
⊢ (fun (y : (↑(Ici ((e : (a : α) → β) x) : Set β) : Type u_2)) ↦
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ici x) ((e.symm : (a : β) → α) (↑y : β)) ⋯ :
          { x_1 : α // x_1 ∈ Ici x }))
      ((fun (y : (↑(Ici x) : Type u_1)) ↦
          (Subtype.mk (p := fun (x_1 : β) ↦ Membership.mem (γ := Set β) (Ici ((e : (a : α) → β) x) : Set β) x_1)
              ((e : (a : α) → β) (↑y : α)) ⋯ :
            { x_1 : β // Membership.mem (γ := Set β) (Ici ((e : (a : α) → β) x) : Set β) x_1 }))
        y) =
    y

Tactic:
simp
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x : α
y : (↑(Ici ((e : (a : α) → β) x) : Set β) : Type u_2)
⊢ (fun (y : (↑(Ici x) : Type u_1)) ↦
        (Subtype.mk (p := fun (x_1 : β) ↦ Membership.mem (γ := Set β) (Ici ((e : (a : α) → β) x) : Set β) x_1)
            ((e : (a : α) → β) (↑y : α)) ⋯ :
          { x_1 : β // Membership.mem (γ := Set β) (Ici ((e : (a : α) → β) x) : Set β) x_1 }))
      ((fun (y : (↑(Ici ((e : (a : α) → β) x) : Set β) : Type u_2)) ↦
          (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ici x) ((e.symm : (a : β) → α) (↑y : β)) ⋯ :
            { x_1 : α // x_1 ∈ Ici x }))
        y) =
    y

Tactic:
simp
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x : α
⊢ ∀ {a b : (↑(Ici x) : Type u_1)},
    LE.le.{u_2} (α := (↑(Ici ((e : (a : α) → β) x) : Set β) : Type u_2))
        (({
                toFun := fun (y : (↑(Ici x) : Type u_1)) ↦
                  Subtype.mk (p := fun (x_1 : β) ↦ Membership.mem (γ := Set β) (Ici ((e : (a : α) → β) x) : Set β) x_1)
                    ((e : (a : α) → β) (↑y : α)) ⋯,
                invFun := fun (y : (↑(Ici ((e : (a : α) → β) x) : Set β) : Type u_2)) ↦
                  Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ici x) ((e.symm : (a : β) → α) (↑y : β)) ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : (↑(Ici x) : Type u_1)) → (↑(Ici ((e : (a : α) → β) x)) : Type u_2))
            a :
          (↑(Ici ((e : (a : α) → β) x) : Set β) : Type u_2))
        (({
                toFun := fun (y : (↑(Ici x) : Type u_1)) ↦
                  Subtype.mk (p := fun (x_1 : β) ↦ Membership.mem (γ := Set β) (Ici ((e : (a : α) → β) x) : Set β) x_1)
                    ((e : (a : α) → β) (↑y : α)) ⋯,
                invFun := fun (y : (↑(Ici ((e : (a : α) → β) x) : Set β) : Type u_2)) ↦
                  Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ici x) ((e.symm : (a : β) → α) (↑y : β)) ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : (↑(Ici x) : Type u_1)) → (↑(Ici ((e : (a : α) → β) x)) : Type u_2))
            b :
          (↑(Ici ((e : (a : α) → β) x) : Set β) : Type u_2)) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x y : α
z : (↑(Icc x y) : Type u_1)
simp : x ≤ (↑z : α) ∧ (↑z : α) ≤ y
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β)
    ((e : (a : α) → β) (↑z : α) : β)

Tactic:
simp only [mem_Icc, map_le_map_iff]

Premises used: OrderIsoClass.map_le_map_iff, Set.mem_Icc
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x y : α
z : (↑(Icc x y) : Type u_1)
⊢ x ≤ (↑z : α) ∧ (↑z : α) ≤ y

Tactic:
z.property

Premises used: Set.Mem, setOf, Set.Icc, Subtype.property
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x y : α
z : (↑(Icc x y) : Type u_1)
⊢ x ≤ (↑z : α) ∧ (↑z : α) ≤ y

Tactic:
exact z.property

Premises used: Subtype.property
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x y : α
z : (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) : Type u_2)
simp : (e : (a : α) → β) x ≤ (↑z : β) ∧ (↑z : β) ≤ (e : (a : α) → β) y
⊢ Membership.mem (α := α) (Icc x y) ((e.symm : (a : β) → α) (↑z : β) : α)

Tactic:
simp only [mem_Icc, e.le_symm_apply, e.symm_apply_le]

Premises used: OrderIso.symm_apply_le, OrderIso.le_symm_apply, Set.mem_Icc
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x y : α
z : (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) : Type u_2)
⊢ (e : (a : α) → β) x ≤ (↑z : β) ∧ (↑z : β) ≤ (e : (a : α) → β) y

Tactic:
z.property

Premises used: Set.Mem, setOf, Set.Icc, Subtype.property
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x y : α
z : (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) : Type u_2)
⊢ (e : (a : α) → β) x ≤ (↑z : β) ∧ (↑z : β) ≤ (e : (a : α) → β) y

Tactic:
exact z.property

Premises used: Subtype.property
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x y_1 : α
y : (↑(Icc x y_1) : Type u_1)
⊢ (fun (z : (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y_1) : Set β) : Type u_2)) ↦
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Icc x y_1) ((e.symm : (a : β) → α) (↑z : β)) ⋯ :
          { x_1 : α // x_1 ∈ Icc x y_1 }))
      ((fun (z : (↑(Icc x y_1) : Type u_1)) ↦
          (Subtype.mk (p := fun (x_1 : β) ↦
              Membership.mem (γ := Set β) (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y_1) : Set β) x_1)
              ((e : (a : α) → β) (↑z : α)) ⋯ :
            { x_1 : β // Membership.mem (γ := Set β) (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y_1) : Set β) x_1 }))
        y) =
    y

Tactic:
simp
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x y_1 : α
y : (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y_1) : Set β) : Type u_2)
⊢ (fun (z : (↑(Icc x y_1) : Type u_1)) ↦
        (Subtype.mk (p := fun (x_1 : β) ↦
            Membership.mem (γ := Set β) (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y_1) : Set β) x_1)
            ((e : (a : α) → β) (↑z : α)) ⋯ :
          { x_1 : β // Membership.mem (γ := Set β) (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y_1) : Set β) x_1 }))
      ((fun (z : (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y_1) : Set β) : Type u_2)) ↦
          (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Icc x y_1) ((e.symm : (a : β) → α) (↑z : β)) ⋯ :
            { x_1 : α // x_1 ∈ Icc x y_1 }))
        y) =
    y

Tactic:
simp
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
e : α ≃o β
x y : α
⊢ ∀ {a b : (↑(Icc x y) : Type u_1)},
    LE.le.{u_2} (α := (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) : Type u_2))
        (({
                toFun := fun (z : (↑(Icc x y) : Type u_1)) ↦
                  Subtype.mk (p := fun (x_1 : β) ↦
                    Membership.mem (γ := Set β) (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) x_1)
                    ((e : (a : α) → β) (↑z : α)) ⋯,
                invFun := fun (z : (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) : Type u_2)) ↦
                  Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Icc x y) ((e.symm : (a : β) → α) (↑z : β)) ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : (↑(Icc x y) : Type u_1)) → (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y)) : Type u_2))
            a :
          (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) : Type u_2))
        (({
                toFun := fun (z : (↑(Icc x y) : Type u_1)) ↦
                  Subtype.mk (p := fun (x_1 : β) ↦
                    Membership.mem (γ := Set β) (Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) x_1)
                    ((e : (a : α) → β) (↑z : α)) ⋯,
                invFun := fun (z : (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) : Type u_2)) ↦
                  Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Icc x y) ((e.symm : (a : β) → α) (↑z : β)) ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : (↑(Icc x y) : Type u_1)) → (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y)) : Type u_2))
            b :
          (↑(Icc ((e : (a : α) → β) x) ((e : (a : α) → β) y) : Set β) : Type u_2)) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
inst : BooleanAlgebra α
⊢ StrictAnti.{u_1, u_1} (α := α) compl

Tactic:
(OrderIso.compl α).strictMono

Premises used: OrderIso.strictMono, StrictAnti, OrderIso.compl
-- Module: Mathlib.Order.Hom.Set
Goal:
α : Type u_1
inst : BooleanAlgebra α
⊢ Antitone.{u_1, u_1} (α := α) compl

Tactic:
(OrderIso.compl α).monotone

Premises used: OrderIso.monotone, Antitone, OrderIso.compl
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : LE α
a : α
⊢ Eq (α := (WithBot α)ᵒᵈ)
    ((WithTop.toDualBotEquiv : (a : WithTop αᵒᵈ) → (WithBot α)ᵒᵈ)
        ((↑((toDual : (a : α) → αᵒᵈ) a) : WithTop αᵒᵈ) : WithTop αᵒᵈ) :
      (WithBot α)ᵒᵈ)
    ((toDual : (a : WithBot α) → (WithBot α)ᵒᵈ) (↑a : WithBot α) : (WithBot α)ᵒᵈ)

Tactic:
rfl

Premises used: WithBot.some, WithTop.some, OrderDual, rfl
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : LE α
a : α
⊢ Eq (α := WithTop αᵒᵈ)
    ((OrderIso.symm WithTop.toDualBotEquiv : (a : (WithBot α)ᵒᵈ) → WithTop αᵒᵈ)
        ((toDual : (a : WithBot α) → (WithBot α)ᵒᵈ) (↑a : WithBot α) : (WithBot α)ᵒᵈ) :
      WithTop αᵒᵈ)
    ((↑((toDual : (a : α) → αᵒᵈ) a) : WithTop αᵒᵈ) : WithTop αᵒᵈ)

Tactic:
rfl

Premises used: WithBot.some, WithTop.some, OrderDual, rfl
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : LE α
⊢ Eq.{u_1 + 1} (α := (WithBot α)ᵒᵈ) ((WithTop.toDualBotEquiv : (a : WithTop αᵒᵈ) → (WithBot α)ᵒᵈ) ⊤ : (WithBot α)ᵒᵈ)
    (⊤ : (WithBot α)ᵒᵈ)

Tactic:
rfl

Premises used: OrderDual, rfl
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : LE α
⊢ Eq.{u_1 + 1} (α := WithTop αᵒᵈ)
    ((OrderIso.symm WithTop.toDualBotEquiv : (a : (WithBot α)ᵒᵈ) → WithTop αᵒᵈ) ⊤ : WithTop αᵒᵈ) (⊤ : WithTop αᵒᵈ)

Tactic:
rfl

Premises used: OrderDual, rfl
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : LE α
⊢ Eq.{u_1 + 1} (α := (a : WithTop αᵒᵈ) → (WithBot α)ᵒᵈ) (⇑WithTop.toDualBotEquiv : (a : WithTop αᵒᵈ) → (WithBot α)ᵒᵈ)
    (Function.comp (β := WithBot α) (⇑toDual : (a : WithBot α) → (WithBot α)ᵒᵈ)
      (⇑WithTop.ofDual : (a : WithTop αᵒᵈ) → WithBot α))

Tactic:
funext fun _ => rfl

Premises used: funext, rfl
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
a : α
h : a ≠ ⊤
⊢ Eq (α := WithTop { a : α // a ≠ ⊤ })
    ((fun (a : α) ↦
        (if h : a = ⊤ then ⊤ else (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ }) :
          WithTop { a : α // a ≠ ⊤ }))
      ((fun (a : WithTop { a : α // a ≠ ⊤ }) ↦ untopD ⊤ (map (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤)) a))
        (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ })))
    (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ })

Tactic:
simp [h]
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
⊢ Eq.{u_1 + 1} (α := WithTop { a : α // a ≠ ⊤ })
    ((fun (a : α) ↦
        (if h : a = ⊤ then ⊤ else (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ }) :
          WithTop { a : α // a ≠ ⊤ }))
      ((fun (a : WithTop { a : α // a ≠ ⊤ }) ↦ untopD ⊤ (map (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤)) a)) ⊤))
    ⊤

Tactic:
simp
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
a : α
pos : a = ⊤ → untopD ⊤ (map (α := { a : α // a ≠ ⊤ }) (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤)) ⊤) = a
neg :
  ∀ (h : ¬a = ⊤),
    untopD ⊤
        (map (α := { a : α // a ≠ ⊤ }) (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤))
          (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ })) =
      a
⊢ untopD ⊤
      (map (α := { a : α // a ≠ ⊤ }) (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤))
        (if h : a = ⊤ then ⊤ else (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ }))) =
    a

Tactic:
split_ifs
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
a : α
h : a = ⊤
⊢ untopD ⊤ (map (α := { a : α // a ≠ ⊤ }) (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤)) ⊤) = a

Tactic:
simp [*]
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
a : α
h : ¬a = ⊤
⊢ untopD ⊤
      (map (α := { a : α // a ≠ ⊤ }) (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤))
        (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ })) =
    a

Tactic:
simp [*]
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
a_1 b_1 : WithTop { a : α // a ≠ ⊤ }
a b : { a : α // a ≠ ⊤ }
⊢ LE.le (α := α)
      (({ toFun := fun (a : WithTop { a : α // a ≠ ⊤ }) ↦ untopD ⊤ (map (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤)) a),
              invFun := fun (a : α) ↦
                if h : a = ⊤ then ⊤ else (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ }),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : WithTop { a : α // a ≠ ⊤ }) → α)
          (↑a : WithTop { a : α // a ≠ ⊤ }) :
        α)
      (({ toFun := fun (a : WithTop { a : α // a ≠ ⊤ }) ↦ untopD ⊤ (map (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤)) a),
              invFun := fun (a : α) ↦
                if h : a = ⊤ then ⊤ else (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ }),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : WithTop { a : α // a ≠ ⊤ }) → α)
          (↑b : WithTop { a : α // a ≠ ⊤ }) :
        α) ↔
    (↑a : WithTop { a : α // a ≠ ⊤ }) ≤ (↑b : WithTop { a : α // a ≠ ⊤ })

Tactic:
simp