awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
inl :
  ∀ (c : α) (ha : LT.lt (α := α ⊕ β) (Sum.inl a) (Sum.inl c)) (hb : LT.lt (α := α ⊕ β) (Sum.inl c) (Sum.inl b)),
    ∃ (a_1 : α), a < a_1 ∧ a_1 < b
inr : ∀ (c : β) (ha : Sum.inl a < Sum.inr c) (hb : Sum.inr c < Sum.inl b), ∃ (a_1 : α), a < a_1 ∧ a_1 < b
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inl_lt_inl_iff.2 h)

Premises used: Iff.mpr, exists_between, Sum.inl_lt_inl_iff
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : α
ha : LT.lt (α := α ⊕ β) (inl a) (inl c)
hb : LT.lt (α := α ⊕ β) (inl c) (inl b)
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b

Tactic:
⟨c, inl_lt_inl_iff.1 ha, inl_lt_inl_iff.1 hb⟩

Premises used: And.intro, Exists.intro, Iff.mp, Sum.inl_lt_inl_iff
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : α
ha : LT.lt (α := α ⊕ β) (inl a) (inl c)
hb : LT.lt (α := α ⊕ β) (inl c) (inl b)
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b

Tactic:
exact ⟨c, inl_lt_inl_iff.1 ha, inl_lt_inl_iff.1 hb⟩
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : β
ha : inl a < inr c
hb : inr c < inl b
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b

Tactic:
(not_inl_lt_inr ha).elim

Premises used: False.elim, Sum.not_inl_lt_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
c : β
ha : inl a < inr c
hb : inr c < inl b
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b

Tactic:
exact (not_inl_lt_inr ha).elim

Premises used: False.elim, Sum.not_inl_lt_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
inl : ∀ (c : α) (ha : Sum.inr a < Sum.inl c) (hb : Sum.inl c < Sum.inr b), ∃ (a_1 : β), a < a_1 ∧ a_1 < b
inr :
  ∀ (c : β) (ha : LT.lt (α := α ⊕ β) (Sum.inr a) (Sum.inr c)) (hb : LT.lt (α := α ⊕ β) (Sum.inr c) (Sum.inr b)),
    ∃ (a_1 : β), a < a_1 ∧ a_1 < b
⊢ ∃ (a_1 : β), a < a_1 ∧ a_1 < b

Tactic:
obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inr_lt_inr_iff.2 h)

Premises used: Iff.mpr, Sum.inr_lt_inr_iff, exists_between
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : α
ha : inr a < inl c
hb : inl c < inr b
⊢ ∃ (a_1 : β), a < a_1 ∧ a_1 < b

Tactic:
(not_inl_lt_inr hb).elim

Premises used: False.elim, Sum.not_inl_lt_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : α
ha : inr a < inl c
hb : inl c < inr b
⊢ ∃ (a_1 : β), a < a_1 ∧ a_1 < b

Tactic:
exact (not_inl_lt_inr hb).elim

Premises used: False.elim, Sum.not_inl_lt_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : β
ha : LT.lt (α := α ⊕ β) (inr a) (inr c)
hb : LT.lt (α := α ⊕ β) (inr c) (inr b)
⊢ ∃ (a_1 : β), a < a_1 ∧ a_1 < b

Tactic:
⟨c, inr_lt_inr_iff.1 ha, inr_lt_inr_iff.1 hb⟩

Premises used: Sum.inr_lt_inr_iff, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
c : β
ha : LT.lt (α := α ⊕ β) (inr a) (inr c)
hb : LT.lt (α := α ⊕ β) (inr c) (inr b)
⊢ ∃ (a_1 : β), a < a_1 ∧ a_1 < b

Tactic:
exact ⟨c, inr_lt_inr_iff.1 ha, inr_lt_inr_iff.1 hb⟩
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
a b : α ⊕ β
⊢ a.swap ≤ b.swap ↔ a ≤ b

Tactic:
liftRel_swap_iff

Premises used: Sum.liftRel_swap_iff
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
a b : α ⊕ β
⊢ a.swap < b.swap ↔ a < b

Tactic:
liftRel_swap_iff

Premises used: Sum.liftRel_swap_iff
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
a b : α ⊕ β
⊢ LE.le (α := _root_.Lex (α ⊕ β)) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) a : _root_.Lex (α ⊕ β))
      ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) b : _root_.Lex (α ⊕ β)) ↔
    Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : β) ↦ x1 ≤ x2) a b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
a b : α ⊕ β
⊢ LT.lt (α := _root_.Lex (α ⊕ β)) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) a : _root_.Lex (α ⊕ β))
      ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) b : _root_.Lex (α ⊕ β)) ↔
    Lex (fun (x1 x2 : α) ↦ x1 < x2) (fun (x1 x2 : β) ↦ x1 < x2) a b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
a b : _root_.Lex (α ⊕ β)
⊢ a ≤ b ↔
    Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : β) ↦ x1 ≤ x2) ((ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) a)
      ((ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) b)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
a b : _root_.Lex (α ⊕ β)
⊢ a < b ↔
    Lex (fun (x1 x2 : α) ↦ x1 < x2) (fun (x1 x2 : β) ↦ x1 < x2) ((ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) a)
      ((ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) b)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
a b : α
⊢ LE.le (α := _root_.Lex (α ⊕ β)) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl a) : _root_.Lex (α ⊕ β))
      ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl b) : _root_.Lex (α ⊕ β)) ↔
    a ≤ b

Tactic:
lex_inl_inl

Premises used: Sum.lex_inl_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
a b : β
⊢ LE.le (α := _root_.Lex (α ⊕ β)) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inr a) : _root_.Lex (α ⊕ β))
      ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inr b) : _root_.Lex (α ⊕ β)) ↔
    a ≤ b

Tactic:
lex_inr_inr

Premises used: Sum.lex_inr_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
a b : α
⊢ LT.lt (α := _root_.Lex (α ⊕ β)) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl a) : _root_.Lex (α ⊕ β))
      ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl b) : _root_.Lex (α ⊕ β)) ↔
    a < b

Tactic:
lex_inl_inl

Premises used: Sum.lex_inl_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
a b : β
⊢ LT.lt (α := _root_.Lex (α ⊕ β)) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inr a) : _root_.Lex (α ⊕ β))
      ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inr b) : _root_.Lex (α ⊕ β)) ↔
    a < b

Tactic:
lex_inr_inr

Premises used: Sum.lex_inr_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
a : α
b : β
⊢ LE.le (α := _root_.Lex (α ⊕ β)) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl a) : _root_.Lex (α ⊕ β))
    ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inr b) : _root_.Lex (α ⊕ β))

Tactic:
Lex.sep _ _

Premises used: Sum.Lex.sep
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
a : α
b : β
⊢ LT.lt (α := _root_.Lex (α ⊕ β)) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl a) : _root_.Lex (α ⊕ β))
    ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inr b) : _root_.Lex (α ⊕ β))

Tactic:
Lex.sep _ _

Premises used: Sum.Lex.sep
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
a : α
b : β
⊢ ¬LE.le (α := _root_.Lex (α ⊕ β)) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inr b) : _root_.Lex (α ⊕ β))
      ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl a) : _root_.Lex (α ⊕ β))

Tactic:
lex_inr_inl

Premises used: Sum.lex_inr_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
a : α
b : β
⊢ ¬LT.lt (α := _root_.Lex (α ⊕ β)) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inr b) : _root_.Lex (α ⊕ β))
      ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl a) : _root_.Lex (α ⊕ β))

Tactic:
lex_inr_inl

Premises used: Sum.lex_inr_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
⊢ Eq (α := (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (⇑toLexRelIsoLT : (a : α ⊕ β) → _root_.Lex (α ⊕ β))
    (⇑toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
⊢ Eq (α := (a : _root_.Lex (α ⊕ β)) → α ⊕ β)
    (⇑(RelIso.symm (r := Lex (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2) (s :=
          fun (x1 x2 : _root_.Lex (α ⊕ β)) ↦ x1 < x2) toLexRelIsoLT) :
      (a : _root_.Lex (α ⊕ β)) → α ⊕ β)
    (⇑ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β)

Tactic:
rfl

Premises used: Lex, rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
⊢ Eq (α := (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (⇑toLexRelIsoLE : (a : α ⊕ β) → _root_.Lex (α ⊕ β))
    (⇑toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
⊢ Eq (α := (a : _root_.Lex (α ⊕ β)) → α ⊕ β)
    (⇑(RelIso.symm (r := Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x1 x2 : β) ↦ x1 ≤ x2) (s :=
          fun (x1 x2 : _root_.Lex (α ⊕ β)) ↦ x1 ≤ x2) toLexRelIsoLE) :
      (a : _root_.Lex (α ⊕ β)) → α ⊕ β)
    (⇑ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β)

Tactic:
rfl

Premises used: Lex, rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
a b : _root_.Lex (α ⊕ β)
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, ?_⟩, ?_⟩

Premises used: le_of_lt, Sum.Lex.mono, And.intro, Iff.intro
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
a b : _root_.Lex (α ⊕ β)
refine_1 : ∀ (hab : a < b), ¬b ≤ a
refine_2 : a ≤ b ∧ ¬b ≤ a → a < b
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
refine ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, ?_⟩, ?_⟩
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
hba : a₁ ≤ a₂
hab : LT.lt (α := _root_.Lex (α ⊕ β)) (inl a₂) (inl a₁)
⊢ False

Tactic:
hba.not_gt (inl_lt_inl_iff.1 hab)

Premises used: Sum.Lex.inl_lt_inl_iff, LE.le.not_gt, Iff.mp
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
hba : a₁ ≤ a₂
hab : LT.lt (α := _root_.Lex (α ⊕ β)) (inl a₂) (inl a₁)
⊢ False

Tactic:
exact hba.not_gt (inl_lt_inl_iff.1 hab)

Premises used: Sum.Lex.inl_lt_inl_iff, LE.le.not_gt, Iff.mp
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
b₁ b₂ : β
hba : b₁ ≤ b₂
hab : LT.lt (α := _root_.Lex (α ⊕ β)) (inr b₂) (inr b₁)
⊢ False

Tactic:
hba.not_gt (inr_lt_inr_iff.1 hab)

Premises used: LE.le.not_gt, Iff.mp, Sum.Lex.inr_lt_inr_iff
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
b₁ b₂ : β
hba : b₁ ≤ b₂
hab : LT.lt (α := _root_.Lex (α ⊕ β)) (inr b₂) (inr b₁)
⊢ False

Tactic:
exact hba.not_gt (inr_lt_inr_iff.1 hab)

Premises used: LE.le.not_gt, Iff.mp, Sum.Lex.inr_lt_inr_iff
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
b : α
a : β
hab : inr a < inl b
⊢ False

Tactic:
not_inr_lt_inl hab

Premises used: Sum.Lex.not_inr_lt_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
b : α
a : β
hab : inr a < inl b
⊢ False

Tactic:
exact not_inr_lt_inl hab

Premises used: Sum.Lex.not_inr_lt_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
hab : a₁ ≤ a₂
hba : ¬LE.le (α := _root_.Lex (α ⊕ β)) (inl a₂) (inl a₁)
⊢ LT.lt (α := _root_.Lex (α ⊕ β)) (inl a₁) (inl a₂)

Tactic:
Lex.inl (hab.lt_of_not_ge fun h => hba <| Lex.inl h)

Premises used: LE.le.lt_of_not_ge, Sum.Lex.inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
hab : a₁ ≤ a₂
hba : ¬LE.le (α := _root_.Lex (α ⊕ β)) (inl a₂) (inl a₁)
⊢ LT.lt (α := _root_.Lex (α ⊕ β)) (inl a₁) (inl a₂)

Tactic:
exact Lex.inl (hab.lt_of_not_ge fun h => hba <| Lex.inl h)

Premises used: LE.le.lt_of_not_ge, Sum.Lex.inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
b₁ b₂ : β
hab : b₁ ≤ b₂
hba : ¬LE.le (α := _root_.Lex (α ⊕ β)) (inr b₂) (inr b₁)
⊢ LT.lt (α := _root_.Lex (α ⊕ β)) (inr b₁) (inr b₂)

Tactic:
Lex.inr (hab.lt_of_not_ge fun h => hba <| Lex.inr h)

Premises used: LE.le.lt_of_not_ge, Sum.Lex.inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
b₁ b₂ : β
hab : b₁ ≤ b₂
hba : ¬LE.le (α := _root_.Lex (α ⊕ β)) (inr b₂) (inr b₁)
⊢ LT.lt (α := _root_.Lex (α ⊕ β)) (inr b₁) (inr b₂)

Tactic:
exact Lex.inr (hab.lt_of_not_ge fun h => hba <| Lex.inr h)

Premises used: LE.le.lt_of_not_ge, Sum.Lex.inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
a : α
b : β
hba : ¬inr b ≤ inl a
⊢ inl a < inr b

Tactic:
Lex.sep _ _

Premises used: Sum.Lex.sep
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
a : α
b : β
hba : ¬inr b ≤ inl a
⊢ inl a < inr b

Tactic:
exact Lex.sep _ _

Premises used: Sum.Lex.sep
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ Monotone (α := α ⊕ β) (β := _root_.Lex (α ⊕ β)) (⇑toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β))

Tactic:
fun _ _ h => h.lex

Premises used: Monotone, Sum.LiftRel.lex
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ StrictMono (α := α ⊕ β) (β := _root_.Lex (α ⊕ β)) (⇑toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β))

Tactic:
fun _ _ h => h.lex

Premises used: StrictMono, Sum.LiftRel.lex
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ Monotone (α := α) (β := _root_.Lex (α ⊕ β))
    (Function.comp (β := α ⊕ β) (⇑toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) inl)

Tactic:
toLex_mono.comp Sum.inl_mono

Premises used: Monotone.comp, Sum.inl_mono, Sum.Lex.toLex_mono
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ Monotone (α := β) (β := _root_.Lex (α ⊕ β))
    (Function.comp (β := α ⊕ β) (⇑toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) inr)

Tactic:
toLex_mono.comp Sum.inr_mono

Premises used: Monotone.comp, Sum.inr_mono, Sum.Lex.toLex_mono
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ StrictMono (α := α) (β := _root_.Lex (α ⊕ β))
    (Function.comp (β := α ⊕ β) (⇑toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) inl)

Tactic:
toLex_strictMono.comp Sum.inl_strictMono

Premises used: Sum.inl_strictMono, StrictMono.comp, Sum.Lex.toLex_strictMono
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ StrictMono (α := β) (β := _root_.Lex (α ⊕ β))
    (Function.comp (β := α ⊕ β) (⇑toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) inr)

Tactic:
toLex_strictMono.comp Sum.inr_strictMono

Premises used: Sum.inr_strictMono, StrictMono.comp, Sum.Lex.toLex_strictMono
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : OrderBot α
inst_2 : LE β
a : α
⊢ LE.le (α := _root_.Lex (α ⊕ β)) (inl ⊥) (inl a)

Tactic:
Lex.inl bot_le

Premises used: Sum.Lex.inl, bot_le
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : OrderBot α
inst_2 : LE β
a : α
⊢ LE.le (α := _root_.Lex (α ⊕ β)) (inl ⊥) (inl a)

Tactic:
exact Lex.inl bot_le

Premises used: Sum.Lex.inl, bot_le
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : OrderBot α
inst_2 : LE β
b : β
⊢ LE.le (α := _root_.Lex (α ⊕ β)) (inl ⊥) (inr b)

Tactic:
Lex.sep _ _

Premises used: Sum.Lex.sep
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : OrderBot α
inst_2 : LE β
b : β
⊢ LE.le (α := _root_.Lex (α ⊕ β)) (inl ⊥) (inr b)

Tactic:
exact Lex.sep _ _

Premises used: Sum.Lex.sep
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : OrderBot α
inst_2 : LE β
⊢ Eq (α := _root_.Lex (α ⊕ β)) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl ⊥) : _root_.Lex (α ⊕ β))
    (⊥ : _root_.Lex (α ⊕ β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : LE β
inst_2 : OrderTop β
a : α
⊢ LE.le (α := _root_.Lex (α ⊕ β)) (inl a) (inr ⊤)

Tactic:
Lex.sep _ _

Premises used: Sum.Lex.sep
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : LE β
inst_2 : OrderTop β
a : α
⊢ LE.le (α := _root_.Lex (α ⊕ β)) (inl a) (inr ⊤)

Tactic:
exact Lex.sep _ _

Premises used: Sum.Lex.sep
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : LE β
inst_2 : OrderTop β
b : β
⊢ LE.le (α := _root_.Lex (α ⊕ β)) (inr b) (inr ⊤)

Tactic:
Lex.inr le_top

Premises used: Sum.Lex.inr, le_top
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : LE β
inst_2 : OrderTop β
b : β
⊢ LE.le (α := _root_.Lex (α ⊕ β)) (inr b) (inr ⊤)

Tactic:
exact Lex.inr le_top

Premises used: Sum.Lex.inr, le_top
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
inst_2 : OrderTop β
⊢ Eq (α := _root_.Lex (α ⊕ β)) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inr ⊤) : _root_.Lex (α ⊕ β))
    (⊤ : _root_.Lex (α ⊕ β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LT α
inst_1 : LT β
inst_2 : NoMinOrder α
inst_3 : NoMinOrder β
⊢ NoMinOrder (_root_.Lex (α ⊕ β))

Tactic:
⟨fun a =>
    match a with
    | inl a =>
      let ⟨b, h⟩ := exists_lt a
      ⟨toLex (inl b), inl_lt_inl_iff.2 h⟩
    | inr a =>
      let ⟨b, h⟩ := exists_lt a
      ⟨toLex (inr b), inr_lt_inr_iff.2 h⟩⟩

Premises used: Iff.mpr, _private.0.Sum.Lex.noMinOrder.match_1, Exists, Sum.inl, NoMinOrder.mk, Sum.Lex.inl_lt_inl_iff, Sum.inr, LT.lt, Exists.intro, NoMinOrder.exists_lt, _private.0.Sum.noMinOrder.match_1, Sum.Lex.inr_lt_inr_iff, DFunLike.coe, toLex
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LT α
inst_1 : LT β
inst_2 : NoMaxOrder α
inst_3 : NoMaxOrder β
⊢ NoMaxOrder (_root_.Lex (α ⊕ β))

Tactic:
⟨fun a =>
    match a with
    | inl a =>
      let ⟨b, h⟩ := exists_gt a
      ⟨toLex (inl b), inl_lt_inl_iff.2 h⟩
    | inr a =>
      let ⟨b, h⟩ := exists_gt a
      ⟨toLex (inr b), inr_lt_inr_iff.2 h⟩⟩

Premises used: Iff.mpr, _private.0.Sum.Lex.noMinOrder.match_1, Exists, NoMaxOrder.mk, Sum.inl, NoMaxOrder.exists_gt, Sum.Lex.inl_lt_inl_iff, Sum.inr, LT.lt, Exists.intro, Sum.Lex.inr_lt_inr_iff, DFunLike.coe, _private.0.Sum.noMaxOrder.match_1, toLex
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LT α
inst_1 : LT β
inst_2 : NoMinOrder α
inst_3 : Nonempty α
⊢ NoMinOrder (_root_.Lex (α ⊕ β))

Tactic:
⟨fun a =>
    match a with
    | inl a =>
      let ⟨b, h⟩ := exists_lt a
      ⟨toLex (inl b), inl_lt_inl_iff.2 h⟩
    | inr _ => ⟨toLex (inl <| Classical.arbitrary α), inl_lt_inr _ _⟩⟩

Premises used: Iff.mpr, _private.0.Sum.Lex.noMinOrder.match_1, Exists, Sum.inl, NoMinOrder.mk, Sum.Lex.inl_lt_inl_iff, Sum.Lex.inl_lt_inr, LT.lt, Exists.intro, Classical.arbitrary, NoMinOrder.exists_lt, _private.0.Sum.noMinOrder.match_1, DFunLike.coe, toLex
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LT α
inst_1 : LT β
inst_2 : NoMaxOrder β
inst_3 : Nonempty β
⊢ NoMaxOrder (_root_.Lex (α ⊕ β))

Tactic:
⟨fun a =>
    match a with
    | inl _ => ⟨toLex (inr <| Classical.arbitrary β), inl_lt_inr _ _⟩
    | inr a =>
      let ⟨b, h⟩ := exists_gt a
      ⟨toLex (inr b), inr_lt_inr_iff.2 h⟩⟩

Premises used: Iff.mpr, _private.0.Sum.Lex.noMinOrder.match_1, Exists, NoMaxOrder.mk, NoMaxOrder.exists_gt, Sum.inr, Sum.Lex.inl_lt_inr, LT.lt, Exists.intro, Classical.arbitrary, Sum.Lex.inr_lt_inr_iff, DFunLike.coe, _private.0.Sum.noMaxOrder.match_1, toLex
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LT α
inst_1 : LT β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
inst_4 : NoMaxOrder α
⊢ DenselyOrdered (_root_.Lex (α ⊕ β))

Tactic:
⟨fun a b h =>
    match a, b, h with
    | inl _, inl _, Lex.inl h =>
      let ⟨c, ha, hb⟩ := exists_between h
      ⟨toLex (inl c), inl_lt_inl_iff.2 ha, inl_lt_inl_iff.2 hb⟩
    | inl a, inr _, Lex.sep _ _ =>
      let ⟨c, h⟩ := exists_gt a
      ⟨toLex (inl c), inl_lt_inl_iff.2 h, inl_lt_inr _ _⟩
    | inr _, inr _, Lex.inr h =>
      let ⟨c, ha, hb⟩ := exists_between h
      ⟨toLex (inr c), inr_lt_inr_iff.2 ha, inr_lt_inr_iff.2 hb⟩⟩

Premises used: Iff.mpr, Exists, Sum.inl, NoMaxOrder.exists_gt, exists_between, DenselyOrdered.mk, And, Sum.Lex.inl_lt_inl_iff, Sum.inr, _private.0.Sum.denselyOrdered.match_1, And.intro, Sum.Lex.inl_lt_inr, LT.lt, Exists.intro, _private.0.Sum.Lex.denselyOrdered_of_noMaxOrder.match_1, Sum.Lex.inr_lt_inr_iff, DFunLike.coe, _private.0.Sum.noMaxOrder.match_1, toLex
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LT α
inst_1 : LT β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
inst_4 : NoMinOrder β
⊢ DenselyOrdered (_root_.Lex (α ⊕ β))

Tactic:
⟨fun a b h =>
    match a, b, h with
    | inl _, inl _, Lex.inl h =>
      let ⟨c, ha, hb⟩ := exists_between h
      ⟨toLex (inl c), inl_lt_inl_iff.2 ha, inl_lt_inl_iff.2 hb⟩
    | inl _, inr b, Lex.sep _ _ =>
      let ⟨c, h⟩ := exists_lt b
      ⟨toLex (inr c), inl_lt_inr _ _, inr_lt_inr_iff.2 h⟩
    | inr _, inr _, Lex.inr h =>
      let ⟨c, ha, hb⟩ := exists_between h
      ⟨toLex (inr c), inr_lt_inr_iff.2 ha, inr_lt_inr_iff.2 hb⟩⟩

Premises used: Iff.mpr, Exists, Sum.inl, exists_between, DenselyOrdered.mk, And, Sum.Lex.inl_lt_inl_iff, Sum.inr, _private.0.Sum.denselyOrdered.match_1, And.intro, Sum.Lex.inl_lt_inr, LT.lt, Exists.intro, NoMinOrder.exists_lt, _private.0.Sum.noMinOrder.match_1, _private.0.Sum.Lex.denselyOrdered_of_noMaxOrder.match_1, Sum.Lex.inr_lt_inr_iff, DFunLike.coe, toLex
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst : LE α
inst_1 : LE β
inst_2 : LE γ
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a : α
b : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
⊢ ∀ {a b : α₁ ⊕ β₁},
    LE.le (α := α₂ ⊕ β₂) (((↑ea : α₁ ≃ α₂).sumCongr (↑eb : β₁ ≃ β₂) : (a : α₁ ⊕ β₁) → α₂ ⊕ β₂) a : α₂ ⊕ β₂)
        (((↑ea : α₁ ≃ α₂).sumCongr (↑eb : β₁ ≃ β₂) : (a : α₁ ⊕ β₁) → α₂ ⊕ β₂) b : α₂ ⊕ β₂) ↔
      a ≤ b

Tactic:
aesop
-- Module: Mathlib.Data.Sum.Order
Goal:
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst : LE α₁
inst_1 : LE α₂
inst_2 : LE β₁
inst_3 : LE β₂
inst_4 : LE γ₁
inst_5 : LE γ₂
e₁ : α₁ ≃o β₁
e₂ : α₂ ≃o β₂
f₁ : β₁ ≃o γ₁
f₂ : β₂ ≃o γ₂
h :
  ∀ (x : α₁ ⊕ α₂),
    Eq (α := γ₁ ⊕ γ₂) (((e₁.sumCongr e₂).trans (f₁.sumCongr f₂) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) x : γ₁ ⊕ γ₂)
      (((e₁.trans f₁).sumCongr (e₂.trans f₂) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) x : γ₁ ⊕ γ₂)
⊢ (e₁.sumCongr e₂).trans (f₁.sumCongr f₂) = (e₁.trans f₁).sumCongr (e₂.trans f₂)

Tactic:
ext