awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
r : α → α → Prop
x y : α
inst : IsTrans α r
inst_1 : Std.Trichotomous r
inst_2 : DecidableRel r
a : α
ha : ¬r x a
b : α
hb : ¬r x b
⊢ r
      ((Equiv.trans (Equiv.sumComm { x_1 : α // ¬r x x_1 } (Subtype (r x))) (Equiv.sumCompl (r x)) :
          (a : { x_1 : α // ¬r x x_1 } ⊕ Subtype (r x)) → α)
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x x_1) a ha)))
      ((Equiv.trans (Equiv.sumComm { x_1 : α // ¬r x x_1 } (Subtype (r x))) (Equiv.sumCompl (r x)) :
          (a : { x_1 : α // ¬r x x_1 } ⊕ Subtype (r x)) → α)
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x x_1) b hb))) ↔
    Sum.Lex (α := { x_1 : α // ¬r x x_1 }) (β := Subtype (r x)) (Subrel r fun (x_1 : α) ↦ ¬r x x_1) (Subrel r (r x))
      (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x x_1) a ha))
      (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x x_1) b hb))

Tactic:
simp
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
r : α → α → Prop
x y : α
inst : IsTrans α r
inst_1 : Std.Trichotomous r
inst_2 : DecidableRel r
a : α
ha : ¬r x a
b : α
hb : r x b
⊢ r
      ((Equiv.trans (Equiv.sumComm { x_1 : α // ¬r x x_1 } (Subtype (r x))) (Equiv.sumCompl (r x)) :
          (a : { x_1 : α // ¬r x x_1 } ⊕ Subtype (r x)) → α)
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x x_1) a ha)))
      ((Equiv.trans (Equiv.sumComm { x_1 : α // ¬r x x_1 } (Subtype (r x))) (Equiv.sumCompl (r x)) :
          (a : { x_1 : α // ¬r x x_1 } ⊕ Subtype (r x)) → α)
        (Sum.inr (Subtype.mk (p := r x) b hb))) ↔
    Sum.Lex (α := { x_1 : α // ¬r x x_1 }) (Subrel r fun (x_1 : α) ↦ ¬r x x_1) (Subrel r (r x))
      (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x x_1) a ha)) (Sum.inr (Subtype.mk (p := r x) b hb))

Tactic:
simpa using trans_trichotomous_left ha hb

Premises used: trans_trichotomous_left
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
r : α → α → Prop
x y : α
inst : IsTrans α r
inst_1 : Std.Trichotomous r
inst_2 : DecidableRel r
a : α
ha : r x a
b : α
hb : ¬r x b
⊢ r
      ((Equiv.trans (Equiv.sumComm { x_1 : α // ¬r x x_1 } (Subtype (r x))) (Equiv.sumCompl (r x)) :
          (a : { x_1 : α // ¬r x x_1 } ⊕ Subtype (r x)) → α)
        (Sum.inr (Subtype.mk (p := r x) a ha)))
      ((Equiv.trans (Equiv.sumComm { x_1 : α // ¬r x x_1 } (Subtype (r x))) (Equiv.sumCompl (r x)) :
          (a : { x_1 : α // ¬r x x_1 } ⊕ Subtype (r x)) → α)
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x x_1) b hb))) ↔
    Sum.Lex (α := { x_1 : α // ¬r x x_1 }) (Subrel r fun (x_1 : α) ↦ ¬r x x_1) (Subrel r (r x))
      (Sum.inr (Subtype.mk (p := r x) a ha)) (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ ¬r x x_1) b hb))

Tactic:
simpa using fun h ↦ hb <| trans ha h

Premises used: trans
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
r : α → α → Prop
x y : α
inst : IsTrans α r
inst_1 : Std.Trichotomous r
inst_2 : DecidableRel r
a : α
ha : r x a
b : α
hb : r x b
⊢ r
      ((Equiv.trans (Equiv.sumComm { x_1 : α // ¬r x x_1 } (Subtype (r x))) (Equiv.sumCompl (r x)) :
          (a : { x_1 : α // ¬r x x_1 } ⊕ Subtype (r x)) → α)
        (Sum.inr (Subtype.mk (p := r x) a ha)))
      ((Equiv.trans (Equiv.sumComm { x_1 : α // ¬r x x_1 } (Subtype (r x))) (Equiv.sumCompl (r x)) :
          (a : { x_1 : α // ¬r x x_1 } ⊕ Subtype (r x)) → α)
        (Sum.inr (Subtype.mk (p := r x) b hb))) ↔
    Sum.Lex (α := { x_1 : α // ¬r x x_1 }) (Subrel r fun (x_1 : α) ↦ ¬r x x_1) (Subrel r (r x))
      (Sum.inr (Subtype.mk (p := r x) a ha)) (Sum.inr (Subtype.mk (p := r x) b hb))

Tactic:
simp
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
r : α → α → Prop
x : α
inst : IsTrans α r
inst_1 : Std.Trichotomous r
inst_2 : DecidableRel r
a : { x_1 : α // ¬r x x_1 } ⊕ Subtype (r x)
⊢ Eq (α := α) ((sumLexComplRight r x : (a : { x_1 : α // ¬r x x_1 } ⊕ Subtype (r x)) → α) a : α)
    ((Equiv.sumCompl (r x) : (a : { a : α // r x a } ⊕ { a : α // ¬r x a }) → α) a.swap : α)

Tactic:
rfl

Premises used: Sum.swap, rfl, Sum.elim
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : ∀ (x_1 : α), x_1 ∈ Ici x ↔ Membership.mem (γ := Set α) {y : α | ¬y < x} x_1
⊢ Ici x = {y : α | ¬y < x}

Tactic:
ext
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x y x_1 : α
⊢ x_1 ∈ Ici x ↔ Membership.mem (γ := Set α) {y : α | ¬y < x} x_1

Tactic:
simp
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x : α
a : (↑(Iio x) : Type u_1)
⊢ (sumLexIioIci x : (a : Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) → α)
      ((toLex :
            (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
          (Sum.inl a) :
        Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) =
    (↑a : α)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x : α
a : (↑(Ici x) : Type u_1)
⊢ (sumLexIioIci x : (a : Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) → α)
      ((toLex :
            (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
          (Sum.inr a) :
        Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) =
    (↑a : α)

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, Not, rfl, Sum.elim
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : y < x
rw :
  y =
    (sumLexIioIci x : (a : Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) → α)
      ((toLex :
            (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
          (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iio x) y h)) :
        Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
rw₁ rw₂ : y = (↑(Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iio x) y h) : α)
⊢ Eq (α := Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((symm (sumLexIioIci x) : (a : α) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) y :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((toLex : (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iio x) y h)) :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))

Tactic:
rw [symm_apply_eq, sumLexIioIci_apply_inl]

Premises used: OrderIso.symm_apply_eq, OrderIso.sumLexIioIci_apply_inl
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : x ≤ y
rw :
  y =
    (sumLexIioIci x : (a : Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) → α)
      ((toLex :
            (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
          (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ici x) y h)) :
        Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
rw₁ rw₂ : y = (↑(Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ici x) y h) : α)
⊢ Eq (α := Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((symm (sumLexIioIci x) : (a : α) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) y :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((toLex : (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
        (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ici x) y h)) :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))

Tactic:
rw [symm_apply_eq, sumLexIioIci_apply_inr]

Premises used: OrderIso.symm_apply_eq, OrderIso.sumLexIioIci_apply_inr
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x : α
a : (↑(Iio x) : Type u_1)
⊢ Eq (α := Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((symm (sumLexIioIci x) : (a : α) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) (↑a : α) :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((toLex : (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
        (Sum.inl a) :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))

Tactic:
sumLexIioIci_symm_apply_of_lt a.2

Premises used: OrderIso.sumLexIioIci_symm_apply_of_lt, Subtype.property
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x : α
a : (↑(Ici x) : Type u_1)
⊢ Eq (α := Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((symm (sumLexIioIci x) : (a : α) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1))) (↑a : α) :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
    ((toLex : (a : (↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)) → Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))
        (Sum.inr a) :
      Lex ((↑(Iio x) : Type u_1) ⊕ (↑(Ici x) : Type u_1)))

Tactic:
sumLexIioIci_symm_apply_of_ge a.2

Premises used: OrderIso.sumLexIioIci_symm_apply_of_ge, Subtype.property
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : ∀ (x_1 : α), x_1 ∈ Iic x ↔ Membership.mem (γ := Set α) {y : α | ¬x < y} x_1
⊢ Iic x = {y : α | ¬x < y}

Tactic:
ext
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x y x_1 : α
⊢ x_1 ∈ Iic x ↔ Membership.mem (γ := Set α) {y : α | ¬x < y} x_1

Tactic:
simp
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x : α
a : (↑(Iic x) : Type u_1)
⊢ (sumLexIicIoi x : (a : Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) → α)
      ((toLex :
            (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
          (Sum.inl a) :
        Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) =
    (↑a : α)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.Iic, Not, rfl, Sum.elim
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x : α
a : (↑(Ioi x) : Type u_1)
⊢ (sumLexIicIoi x : (a : Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) → α)
      ((toLex :
            (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
          (Sum.inr a) :
        Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) =
    (↑a : α)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : y ≤ x
rw :
  y =
    (sumLexIicIoi x : (a : Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) → α)
      ((toLex :
            (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
          (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iic x) y h)) :
        Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
rw₁ rw₂ : y = (↑(Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iic x) y h) : α)
⊢ Eq (α := Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((symm (sumLexIicIoi x) : (a : α) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) y :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((toLex : (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
        (Sum.inl (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Iic x) y h)) :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))

Tactic:
rw [symm_apply_eq, sumLexIicIoi_apply_inl]

Premises used: OrderIso.symm_apply_eq, OrderIso.sumLexIicIoi_apply_inl
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : x < y
rw :
  y =
    (sumLexIicIoi x : (a : Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) → α)
      ((toLex :
            (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
          (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ioi x) y h)) :
        Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
rw₁ rw₂ : y = (↑(Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ioi x) y h) : α)
⊢ Eq (α := Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((symm (sumLexIicIoi x) : (a : α) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) y :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((toLex : (a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
        (Sum.inr (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Ioi x) y h)) :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))

Tactic:
rw [symm_apply_eq, sumLexIicIoi_apply_inr]

Premises used: OrderIso.symm_apply_eq, OrderIso.sumLexIicIoi_apply_inr
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x : α
a : (↑(Iic x) : Type u_1)
⊢ Eq (α := Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((symm (sumLexIicIoi x) : (a : α) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) (↑a : α) :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    (Sum.inl a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))

Tactic:
sumLexIicIoi_symm_apply_of_le a.2

Premises used: OrderIso.sumLexIicIoi_symm_apply_of_le, Subtype.property
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_1
inst : LinearOrder α
x : α
a : (↑(Ioi x) : Type u_1)
⊢ Eq (α := Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    ((symm (sumLexIicIoi x) : (a : α) → Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))) (↑a : α) :
      Lex ((↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1)))
    (Sum.inr a : (↑(Iic x) : Type u_1) ⊕ (↑(Ioi x) : Type u_1))

Tactic:
sumLexIicIoi_symm_apply_of_lt a.2

Premises used: OrderIso.sumLexIicIoi_symm_apply_of_lt, Subtype.property
-- Module: Mathlib.Order.Hom.Lex
Goal:
α_1 : Type u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Unique β
x : Lex (α × β)
x_1 : α × β
a : α
b : β
⊢ Eq (α := Lex (α × β))
    ((fun (x : α) ↦ ((toLex : (a : α × β) → Lex (α × β)) (x, default) : Lex (α × β)))
        ((fun (x : Lex (α × β)) ↦ (((ofLex : (a : Lex (α × β)) → α × β) x).1 : α))
          ((toLex : (a : α × β) → Lex (α × β)) (a, b))) :
      Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (a, b) : Lex (α × β))

Tactic:
simpa using Unique.default_eq b

Premises used: Unique.default_eq
-- Module: Mathlib.Order.Hom.Lex
Goal:
α_1 : Type u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Unique β
x : α
⊢ (fun (x : Lex (α × β)) ↦ (((ofLex : (a : Lex (α × β)) → α × β) x).1 : α))
      ((fun (x : α) ↦ ((toLex : (a : α × β) → Lex (α × β)) (x, default) : Lex (α × β))) x) =
    x

Tactic:
simp
-- Module: Mathlib.Order.Hom.Lex
Goal:
α_1 : Type u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Unique β
a_1 b_1 : Lex (α × β)
a b : α × β
⊢ LE.le.{u_2} (α := α)
      (({ toFun := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1,
              invFun := fun (x : α) ↦ (toLex : (a : α × β) → Lex (α × β)) (x, default), left_inv := ⋯,
              right_inv := ⋯ } :
            (a : Lex (α × β)) → α)
          ((toLex : (a : α × β) → Lex (α × β)) a : Lex (α × β)) :
        α)
      (({ toFun := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1,
              invFun := fun (x : α) ↦ (toLex : (a : α × β) → Lex (α × β)) (x, default), left_inv := ⋯,
              right_inv := ⋯ } :
            (a : Lex (α × β)) → α)
          ((toLex : (a : α × β) → Lex (α × β)) b : Lex (α × β)) :
        α) ↔
    LE.le (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) a : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) b : Lex (α × β))

Tactic:
simpa [Prod.Lex.toLex_le_toLex] using le_iff_lt_or_eq

Premises used: le_iff_lt_or_eq, Prod.Lex.toLex_le_toLex
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : Unique β
x : Lex (α × β)
⊢ Eq.{u_2 + 1} (α := α) ((prodUnique α β : (a : Lex (α × β)) → α) x : α) (((ofLex : (a : Lex (α × β)) → α × β) x).1 : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lex
Goal:
α_1 : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Unique α
inst_2 : LE β
x : Lex (α × β)
x_1 : α × β
a : α
b : β
⊢ Eq (α := Lex (α × β))
    ((fun (x : β) ↦ ((toLex : (a : α × β) → Lex (α × β)) (default, x) : Lex (α × β)))
        ((fun (x : Lex (α × β)) ↦ (((ofLex : (a : Lex (α × β)) → α × β) x).2 : β))
          ((toLex : (a : α × β) → Lex (α × β)) (a, b))) :
      Lex (α × β))
    ((toLex : (a : α × β) → Lex (α × β)) (a, b) : Lex (α × β))

Tactic:
simpa using Unique.default_eq a

Premises used: Unique.default_eq
-- Module: Mathlib.Order.Hom.Lex
Goal:
α_1 : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Unique α
inst_2 : LE β
x : β
⊢ (fun (x : Lex (α × β)) ↦ (((ofLex : (a : Lex (α × β)) → α × β) x).2 : β))
      ((fun (x : β) ↦ ((toLex : (a : α × β) → Lex (α × β)) (default, x) : Lex (α × β))) x) =
    x

Tactic:
simp
-- Module: Mathlib.Order.Hom.Lex
Goal:
α_1 : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Unique α
inst_2 : LE β
a_1 b_1 : Lex (α × β)
a b : α × β
⊢ a.1 = b.1

Tactic:
have heq : a.1 = b.1 := Subsingleton.allEq _ _
-- Module: Mathlib.Order.Hom.Lex
Goal:
α_1 : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Unique α
inst_2 : LE β
a_1 b_1 : Lex (α × β)
a b : α × β
heq : a.1 = b.1
⊢ LE.le.{u_3} (α := β)
      (({ toFun := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2,
              invFun := fun (x : β) ↦ (toLex : (a : α × β) → Lex (α × β)) (default, x), left_inv := ⋯,
              right_inv := ⋯ } :
            (a : Lex (α × β)) → β)
          ((toLex : (a : α × β) → Lex (α × β)) a : Lex (α × β)) :
        β)
      (({ toFun := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2,
              invFun := fun (x : β) ↦ (toLex : (a : α × β) → Lex (α × β)) (default, x), left_inv := ⋯,
              right_inv := ⋯ } :
            (a : Lex (α × β)) → β)
          ((toLex : (a : α × β) → Lex (α × β)) b : Lex (α × β)) :
        β) ↔
    LE.le (α := Lex (α × β)) ((toLex : (a : α × β) → Lex (α × β)) a : Lex (α × β))
      ((toLex : (a : α × β) → Lex (α × β)) b : Lex (α × β))

Tactic:
simp [Prod.Lex.toLex_le_toLex, heq]

Premises used: Prod.Lex.toLex_le_toLex
-- Module: Mathlib.Order.Hom.Lex
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Unique α
inst_2 : LE β
x : Lex (α × β)
⊢ Eq.{u_3 + 1} (α := β) ((uniqueProd α β : (a : Lex (α × β)) → β) x : β) (((ofLex : (a : Lex (α × β)) → α × β) x).2 : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Lex
Goal:
α_1 : Type u_1
α_2 : Type u_2
β_1 : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ {a b : Lex (Lex (α × β) × γ)},
    LE.le (α := Lex (α × Lex (β × γ)))
        ((Equiv.trans ofLex
                (Equiv.trans (Equiv.prodCongr ofLex (Equiv.refl γ))
                  ((Equiv.prodAssoc α β γ).trans (Equiv.trans ((Equiv.refl α).prodCongr toLex) toLex))) :
              (a : Lex (Lex (α × β) × γ)) → Lex (α × Lex (β × γ)))
            a :
          Lex (α × Lex (β × γ)))
        ((Equiv.trans ofLex
                (Equiv.trans (Equiv.prodCongr ofLex (Equiv.refl γ))
                  ((Equiv.prodAssoc α β γ).trans (Equiv.trans ((Equiv.refl α).prodCongr toLex) toLex))) :
              (a : Lex (Lex (α × β) × γ)) → Lex (α × Lex (β × γ)))
            b :
          Lex (α × Lex (β × γ))) ↔
      a ≤ b

Tactic:
simp only [Prod.Lex.le_iff, Prod.Lex.lt_iff, Equiv.trans_apply, Equiv.prodCongr_apply,
      Equiv.prodAssoc_apply]

Premises used: Equiv.trans_apply, Equiv.prodAssoc_apply, Prod.Lex.le_iff, Equiv.prodCongr_apply, Prod.Lex.lt_iff
-- Module: Mathlib.Order.Hom.Lex
Goal:
α_1 : Type u_1
α_2 : Type u_2
β_1 : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
grind [EmbeddingLike.apply_eq_iff_eq, ofLex_toLex]

Premises used: ofLex_toLex, EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.Order.Hom.Lex
Goal:
α_1 : Type u_1
α_2 : Type u_2
β_1 : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
⊢ ∀ {a b : Lex (Lex (α ⊕ β) × γ)},
    LE.le (α := Lex (Lex (α × γ) ⊕ Lex (β × γ)))
        ((Equiv.trans ofLex
                (Equiv.trans (Equiv.prodCongr ofLex (Equiv.refl γ))
                  ((Equiv.sumProdDistrib α β γ).trans (Equiv.trans (Equiv.sumCongr toLex toLex) toLex))) :
              (a : Lex (Lex (α ⊕ β) × γ)) → Lex (Lex (α × γ) ⊕ Lex (β × γ)))
            a :
          Lex (Lex (α × γ) ⊕ Lex (β × γ)))
        ((Equiv.trans ofLex
                (Equiv.trans (Equiv.prodCongr ofLex (Equiv.refl γ))
                  ((Equiv.sumProdDistrib α β γ).trans (Equiv.trans (Equiv.sumCongr toLex toLex) toLex))) :
              (a : Lex (Lex (α ⊕ β) × γ)) → Lex (Lex (α × γ) ⊕ Lex (β × γ)))
            b :
          Lex (Lex (α × γ) ⊕ Lex (β × γ))) ↔
      a ≤ b

Tactic:
simp [Prod.Lex.le_iff]

Premises used: Prod.Lex.le_iff
-- Module: Mathlib.Order.Hom.Lex
Goal:
α_1 : Type u_1
α_2 : Type u_2
β_1 : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
δ : Type u_7
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
inst_3 : Preorder δ
ea : α ≃o β
eb : γ ≃o δ
⊢ ∀ {a b : Lex (α × γ)},
    LE.le (α := Lex (β × δ))
        ((Equiv.trans ofLex (((↑ea : α ≃ β).prodCongr (↑eb : γ ≃ δ)).trans toLex) : (a : Lex (α × γ)) → Lex (β × δ)) a :
          Lex (β × δ))
        ((Equiv.trans ofLex (((↑ea : α ≃ β).prodCongr (↑eb : γ ≃ δ)).trans toLex) : (a : Lex (α × γ)) → Lex (β × δ)) b :
          Lex (β × δ)) ↔
      a ≤ b

Tactic:
simp [Prod.Lex.le_iff]

Premises used: Prod.Lex.le_iff
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : SemilatticeSup β
f g : α →o β
⊢ Eq (α := (a : α) → β) (⇑(f ⊔ g) : (a : α) → β) ((⇑f : (a : α) → β) ⊔ (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : SemilatticeInf β
f g : α →o β
⊢ Eq (α := (a : α) → β) (⇑(f ⊓ g) : (a : α) → β) ((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : CompleteLattice β
s : Set (α →o β)
x : α
⊢ Eq.{u_2 + 1} (α := β) ((sInf s : (a : α) → β) x : β) (⨅ f ∈ s, (f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: iInf, rfl
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
ι : Sort u_3
inst_1 : CompleteLattice β
f : ι → α →o β
x : α
⊢ Eq.{u_2 + 1} (α := β) ((⨅ (i : ι), f i : (a : α) → β) x : β) (⨅ (i : ι), (f i : (a : α) → β) x : β)

Tactic:
(sInf_apply _ _).trans iInf_range

Premises used: iInf_range, OrderHom.sInf_apply, Eq.trans
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
ι : Sort u_3
inst_1 : CompleteLattice β
f : ι → α →o β
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((⨅ (i : ι), f i : (a : α) → β) x : β) ((⨅ (i : ι), (⇑(f i) : (a : α) → β)) x : β)
⊢ Eq (α := (a : α) → β) (⇑(⨅ (i : ι), f i) : (a : α) → β) (⨅ (i : ι), (⇑(f i) : (a : α) → β))

Tactic:
funext x
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
ι : Sort u_3
inst_1 : CompleteLattice β
f : ι → α →o β
x : α
⊢ Eq.{u_2 + 1} (α := β) ((⨅ (i : ι), f i : (a : α) → β) x : β) ((⨅ (i : ι), (⇑(f i) : (a : α) → β)) x : β)

Tactic:
simp [iInf_apply]

Premises used: OrderHom.iInf_apply
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : CompleteLattice β
s : Set (α →o β)
x : α
⊢ Eq.{u_2 + 1} (α := β) ((sSup s : (a : α) → β) x : β) (⨆ f ∈ s, (f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: iSup, rfl
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
ι : Sort u_3
inst_1 : CompleteLattice β
f : ι → α →o β
x : α
⊢ Eq.{u_2 + 1} (α := β) ((⨆ (i : ι), f i : (a : α) → β) x : β) (⨆ (i : ι), (f i : (a : α) → β) x : β)

Tactic:
(sSup_apply _ _).trans iSup_range

Premises used: OrderHom.sSup_apply, iSup_range, Eq.trans
-- Module: Mathlib.Order.Hom.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
ι : Sort u_3
inst_1 : CompleteLattice β
f : ι → α →o β
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((⨆ (i : ι), f i : (a : α) → β) x : β) ((⨆ (i : ι), (⇑(f i) : (a : α) → β)) x : β)
⊢ Eq (α := (a : α) → β) (⇑(⨆ (i : ι), f i) : (a : α) → β) (⨆ (i : ι), (⇑(f i) : (a : α) → β))

Tactic:
funext x