awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderTop α
inst_3 : Fintype β
inst_4 : LocallyFiniteOrderTop β
⊢ ∀ (a x : _root_.Lex (α ⊕ β)),
    Membership.mem (γ := Finset (_root_.Lex (α ⊕ β)))
        (comp (β := α ⊕ β)
          (Sum.elim (fun (x : α) ↦ map (Equiv.toEmbedding toLex) ((Ioi x).disjSum univ)) fun (x : β) ↦
            map (Embedding.trans Embedding.inr (Equiv.toEmbedding toLex)) (Ioi x))
          (⇑ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) a)
        x ↔
      a < x

Tactic:
simp
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderTop α
inst_3 : Fintype β
inst_4 : LocallyFiniteOrderTop β
a : α
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ici (inlₗ a)) (map (Equiv.toEmbedding toLex) ((Ici a).disjSum univ))

Tactic:
rfl

Premises used: Lex, Finset.map, Finset.Ici, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderTop α
inst_3 : Fintype β
inst_4 : LocallyFiniteOrderTop β
b : β
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ici (inrₗ b))
    (map (Embedding.trans Embedding.inr (Equiv.toEmbedding toLex)) (Ici b))

Tactic:
rfl

Premises used: Finset.map, Finset.Ici, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderTop α
inst_3 : Fintype β
inst_4 : LocallyFiniteOrderTop β
a : α
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioi (inlₗ a)) (map (Equiv.toEmbedding toLex) ((Ioi a).disjSum univ))

Tactic:
rfl

Premises used: Finset.Ioi, Lex, Finset.map, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderTop α
inst_3 : Fintype β
inst_4 : LocallyFiniteOrderTop β
b : β
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioi (inrₗ b))
    (map (Embedding.trans Embedding.inr (Equiv.toEmbedding toLex)) (Ioi b))

Tactic:
rfl

Premises used: Finset.Ioi, Finset.map, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
a₁ a₂ : α
⊢ Eq (α := _root_.Lex (α ⊕ β)) (inlₗ (a₁ ⊔ a₂)) (inlₗ a₁ ⊔ inlₗ a₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sum.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
b₁ b₂ : β
⊢ Eq (α := _root_.Lex (α ⊕ β)) (inrₗ (b₁ ⊔ b₂)) (inrₗ b₁ ⊔ inrₗ b₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sum.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
a₁ a₂ : α
⊢ Eq (α := _root_.Lex (α ⊕ β)) (inlₗ (a₁ ⊓ a₂)) (inlₗ a₁ ⊓ inlₗ a₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sum.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
b₁ b₂ : β
⊢ Eq (α := _root_.Lex (α ⊕ β)) (inrₗ (b₁ ⊓ b₂)) (inrₗ b₁ ⊓ inrₗ b₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sum.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : DistribLattice α
inst_1 : DistribLattice β
⊢ ∀ (x y z : _root_.Lex (α ⊕ β)), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
simp only [Lex.forall, Sum.forall, inr_le_inr_iff,
      le_sup_left, inl_le_inr, sup_of_le_right, and_self,
      inf_of_le_left, implies_true, inf_of_le_right, sup_of_le_left, ← inl_sup,
      ← inr_sup, ← inl_inf, ← inr_inf, sup_inf_left, le_rfl]

Premises used: Lex.forall, le_rfl, Sum.Lex.inr_le_inr_iff, le_sup_left, and_self, inf_of_le_left, inf_of_le_right, sup_inf_left, Sum.Lex.inr_inf, sup_of_le_right, implies_true, Sum.forall, Sum.Lex.inl_inf, Sum.Lex.inr_sup, sup_of_le_left, Sum.Lex.inl_sup, Sum.Lex.inl_le_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Refl r
inst_1 : Std.Refl s
⊢ Std.Refl (LiftRel r s)

Tactic:
⟨LiftRel.refl _ _⟩

Premises used: Std.Refl.mk, Sum.LiftRel.refl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl r
inst_1 : Std.Irrefl s
a : α
h : r a a
⊢ False

Tactic:
irrefl _ h

Premises used: irrefl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl r
inst_1 : Std.Irrefl s
a : α
h : r a a
⊢ False

Tactic:
exact irrefl _ h

Premises used: irrefl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl r
inst_1 : Std.Irrefl s
b : β
h : s b b
⊢ False

Tactic:
irrefl _ h

Premises used: irrefl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl r
inst_1 : Std.Irrefl s
b : β
h : s b b
⊢ False

Tactic:
exact irrefl _ h

Premises used: irrefl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : IsTrans α r
inst_1 : IsTrans β s
⊢ IsTrans (α ⊕ β) (LiftRel r s)

Tactic:
⟨fun _ _ _ => LiftRel.trans _ _⟩

Premises used: Sum.LiftRel.trans, IsTrans.mk
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Antisymm r
inst_1 : Std.Antisymm s
a c : α
hab : r a c
hba : r c a
inl inl₁ : Eq (α := α ⊕ β) (Sum.inl c) (Sum.inl c)
⊢ Eq (α := α ⊕ β) (Sum.inl a) (Sum.inl c)

Tactic:
rw [antisymm hab hba]

Premises used: antisymm
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Antisymm r
inst_1 : Std.Antisymm s
b d : β
hab : s b d
hba : s d b
inr inr₁ : Eq (α := α ⊕ β) (Sum.inr d) (Sum.inr d)
⊢ Eq (α := α ⊕ β) (Sum.inr b) (Sum.inr d)

Tactic:
rw [antisymm hab hba]

Premises used: antisymm
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Refl r
inst_1 : Std.Refl s
a : α
⊢ Lex r s (inl a) (inl a)

Tactic:
Lex.inl (refl _)

Premises used: Sum.Lex.inl, refl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Refl r
inst_1 : Std.Refl s
a : β
⊢ Lex r s (inr a) (inr a)

Tactic:
Lex.inr (refl _)

Premises used: Sum.Lex.inr, refl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Refl r
inst_1 : Std.Refl s
a : α
⊢ Lex r s (inl a) (inl a)

Tactic:
exacts [Lex.inl (refl _), Lex.inr (refl _)]

Premises used: Sum.Lex.inl, Sum.Lex.inr, refl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl r
inst_1 : Std.Irrefl s
a₁ : α
h : r a₁ a₁
⊢ False

Tactic:
irrefl _ h

Premises used: irrefl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl r
inst_1 : Std.Irrefl s
a₁ : α
h : r a₁ a₁
⊢ False

Tactic:
exact irrefl _ h

Premises used: irrefl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl r
inst_1 : Std.Irrefl s
b₁ : β
h : s b₁ b₁
⊢ False

Tactic:
irrefl _ h

Premises used: irrefl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Irrefl r
inst_1 : Std.Irrefl s
b₁ : β
h : s b₁ b₁
⊢ False

Tactic:
exact irrefl _ h

Premises used: irrefl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : IsTrans α r
inst_1 : IsTrans β s
a₁ a₂ : α
hab : r a₁ a₂
a₂_1 : α
hbc : r a₂ a₂_1
⊢ Lex r s (inl a₁) (inl a₂_1)

Tactic:
.inl (_root_.trans hab hbc)

Premises used: trans, Sum.Lex.inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : IsTrans α r
inst_1 : IsTrans β s
a₁ a₂ : α
hab : r a₁ a₂
b : β
⊢ Lex r s (inl a₁) (inr b)

Tactic:
.sep _ _

Premises used: Sum.Lex.sep
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : IsTrans α r
inst_1 : IsTrans β s
b₁ b₂ : β
hab : s b₁ b₂
b₂_1 : β
hbc : s b₂ b₂_1
⊢ Lex r s (inr b₁) (inr b₂_1)

Tactic:
.inr (_root_.trans hab hbc)

Premises used: trans, Sum.Lex.inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : IsTrans α r
inst_1 : IsTrans β s
a : α
b b₂ : β
hbc : s b b₂
⊢ Lex r s (inl a) (inr b₂)

Tactic:
.sep _ _

Premises used: Sum.Lex.sep
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : IsTrans α r
inst_1 : IsTrans β s
a₁ a₂ : α
hab : r a₁ a₂
a₂_1 : α
hbc : r a₂ a₂_1
⊢ Lex r s (inl a₁) (inl a₂_1)

Tactic:
exacts [.inl (_root_.trans hab hbc), .sep _ _, .inr (_root_.trans hab hbc), .sep _ _]
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Antisymm r
inst_1 : Std.Antisymm s
a₁ a₂ : α
hab : r a₁ a₂
hba : r a₂ a₁
inl inl₁ : Eq (α := α ⊕ β) (Sum.inl a₂) (Sum.inl a₂)
⊢ Eq (α := α ⊕ β) (Sum.inl a₁) (Sum.inl a₂)

Tactic:
rw [antisymm hab hba]

Premises used: antisymm
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Antisymm r
inst_1 : Std.Antisymm s
b₁ b₂ : β
hab : s b₁ b₂
hba : s b₂ b₁
inr inr₁ : Eq (α := α ⊕ β) (Sum.inr b₂) (Sum.inr b₂)
⊢ Eq (α := α ⊕ β) (Sum.inr b₁) (Sum.inr b₂)

Tactic:
rw [antisymm hab hba]

Premises used: antisymm
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Total r
inst_1 : Std.Total s
⊢ Std.Total (Lex r s)

Tactic:
⟨fun a b =>
    match a, b with
    | inl a, inl b => (total_of r a b).imp Lex.inl Lex.inl
    | inl _, inr _ => Or.inl (Lex.sep _ _)
    | inr _, inl _ => Or.inr (Lex.sep _ _)
    | inr a, inr b => (total_of s a b).imp Lex.inr Lex.inr⟩

Premises used: total_of, Sum.Lex.inl, _private.0.Sum.instTotalLex.match_1, Sum.Lex.sep, Sum.Lex.inr, Or.inl, Or, Std.Total.mk, Or.imp, Or.inr, Sum.Lex
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Trichotomous r
inst_1 : Std.Trichotomous s
⊢ Std.Trichotomous (Lex r s)

Tactic:
grind [Std.Trichotomous, Lex]

Premises used: Std.Trichotomous, Sum.Lex
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
a b : α ⊕ β
⊢ a ≤ b ↔ LiftRel (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 : α ⊕ β
⊢ a < b ↔ LiftRel (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 : α
⊢ LE.le (α := α ⊕ β) (inl a) (inl b) ↔ a ≤ b

Tactic:
liftRel_inl_inl

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

Tactic:
liftRel_inr_inr

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

Tactic:
liftRel_inl_inl

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

Tactic:
liftRel_inr_inr

Premises used: Sum.liftRel_inr_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
a : α
b : β
⊢ ¬inl b ≤ inr a

Tactic:
not_liftRel_inl_inr

Premises used: Sum.not_liftRel_inl_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
a : α
b : β
⊢ ¬inl b < inr a

Tactic:
not_liftRel_inl_inr

Premises used: Sum.not_liftRel_inl_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
a : α
b : β
⊢ ¬inr b ≤ inl a

Tactic:
not_liftRel_inr_inl

Premises used: Sum.not_liftRel_inr_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
a : α
b : β
⊢ ¬inr b < inl a

Tactic:
not_liftRel_inr_inl

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

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

Premises used: le_of_lt, And.intro, Iff.intro, Sum.LiftRel.mono
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
a b : α ⊕ β
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 c : α
hba : a ≤ c
hab : LT.lt (α := α ⊕ β) (inl c) (inl a)
⊢ False

Tactic:
hba.not_gt (inl_lt_inl_iff.1 hab)

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

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

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

Tactic:
hba.not_gt (inr_lt_inr_iff.1 hab)

Premises used: Sum.inr_lt_inr_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 d : β
hba : b ≤ d
hab : LT.lt (α := α ⊕ β) (inr d) (inr b)
⊢ False

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

Premises used: Sum.inr_lt_inr_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 c : α
hab : a ≤ c
hba : ¬LE.le (α := α ⊕ β) (inl c) (inl a)
⊢ LT.lt (α := α ⊕ β) (inl a) (inl c)

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

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

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

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

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

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

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

Premises used: LE.le.lt_of_not_ge, Sum.LiftRel.inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ Monotone (α := α) (β := α ⊕ β) inl

Tactic:
fun _ _ => LiftRel.inl

Premises used: Sum.LiftRel.inl, Monotone
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ Monotone (α := β) (β := α ⊕ β) inr

Tactic:
fun _ _ => LiftRel.inr

Premises used: Monotone, Sum.LiftRel.inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ StrictMono (α := α) (β := α ⊕ β) inl

Tactic:
fun _ _ => LiftRel.inl

Premises used: StrictMono, Sum.LiftRel.inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
⊢ StrictMono (α := β) (β := α ⊕ β) inr

Tactic:
fun _ _ => LiftRel.inr

Premises used: StrictMono, Sum.LiftRel.inr
-- 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 (α ⊕ β)

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

Premises used: Iff.mpr, Sum.inr_lt_inr_iff, Exists, Sum.inl, NoMinOrder.mk, Sum.inr, LT.lt, Exists.intro, NoMinOrder.exists_lt, _private.0.Sum.LiftRel.refl.match_1, _private.0.Sum.noMinOrder.match_1, Sum.inl_lt_inl_iff
-- 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 (α ⊕ β)

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

Premises used: Iff.mpr, Sum.inr_lt_inr_iff, Exists, NoMaxOrder.mk, Sum.inl, NoMaxOrder.exists_gt, Sum.inr, LT.lt, Exists.intro, _private.0.Sum.LiftRel.refl.match_1, Sum.inl_lt_inl_iff, _private.0.Sum.noMaxOrder.match_1
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h : NoMinOrder (α ⊕ β)
a : α
inl : ∀ (b : α) (h : LT.lt (α := α ⊕ β) (Sum.inl b) (Sum.inl a)), ∃ (b : α), b < a
inr : ∀ (b : β) (h : Sum.inr b < Sum.inl a), ∃ (b : α), b < a
⊢ ∃ (b : α), b < a

Tactic:
obtain ⟨b | b, h⟩ := exists_lt (inl a : α ⊕ β)

Premises used: Sum.inl, NoMinOrder.exists_lt
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : NoMinOrder (α ⊕ β)
a b : α
h : LT.lt (α := α ⊕ β) (inl b) (inl a)
⊢ ∃ (b : α), b < a

Tactic:
⟨b, inl_lt_inl_iff.1 h⟩

Premises used: 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 : NoMinOrder (α ⊕ β)
a b : α
h : LT.lt (α := α ⊕ β) (inl b) (inl a)
⊢ ∃ (b : α), b < a

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

Tactic:
(not_inr_lt_inl h).elim

Premises used: False.elim, Sum.not_inr_lt_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : NoMinOrder (α ⊕ β)
a : α
b : β
h : inr b < inl a
⊢ ∃ (b : α), b < a

Tactic:
exact (not_inr_lt_inl h).elim

Premises used: False.elim, Sum.not_inr_lt_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h : NoMinOrder (α ⊕ β)
a : β
inl : ∀ (b : α) (h : Sum.inl b < Sum.inr a), ∃ (b : β), b < a
inr : ∀ (b : β) (h : LT.lt (α := α ⊕ β) (Sum.inr b) (Sum.inr a)), ∃ (b : β), b < a
⊢ ∃ (b : β), b < a

Tactic:
obtain ⟨b | b, h⟩ := exists_lt (inr a : α ⊕ β)

Premises used: Sum.inr, NoMinOrder.exists_lt
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : NoMinOrder (α ⊕ β)
a : β
b : α
h : inl b < inr a
⊢ ∃ (b : β), b < a

Tactic:
(not_inl_lt_inr h).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 : NoMinOrder (α ⊕ β)
a : β
b : α
h : inl b < inr a
⊢ ∃ (b : β), b < a

Tactic:
exact (not_inl_lt_inr h).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 : NoMinOrder (α ⊕ β)
a b : β
h : LT.lt (α := α ⊕ β) (inr b) (inr a)
⊢ ∃ (b : β), b < a

Tactic:
⟨b, inr_lt_inr_iff.1 h⟩

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

Tactic:
exact ⟨b, inr_lt_inr_iff.1 h⟩
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h : NoMaxOrder (α ⊕ β)
a : α
inl : ∀ (b : α) (h : LT.lt (α := α ⊕ β) (Sum.inl a) (Sum.inl b)), ∃ (b : α), a < b
inr : ∀ (b : β) (h : Sum.inl a < Sum.inr b), ∃ (b : α), a < b
⊢ ∃ (b : α), a < b

Tactic:
obtain ⟨b | b, h⟩ := exists_gt (inl a : α ⊕ β)

Premises used: Sum.inl, NoMaxOrder.exists_gt
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : NoMaxOrder (α ⊕ β)
a b : α
h : LT.lt (α := α ⊕ β) (inl a) (inl b)
⊢ ∃ (b : α), a < b

Tactic:
⟨b, inl_lt_inl_iff.1 h⟩

Premises used: 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 : NoMaxOrder (α ⊕ β)
a b : α
h : LT.lt (α := α ⊕ β) (inl a) (inl b)
⊢ ∃ (b : α), a < b

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

Tactic:
(not_inl_lt_inr h).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 : NoMaxOrder (α ⊕ β)
a : α
b : β
h : inl a < inr b
⊢ ∃ (b : α), a < b

Tactic:
exact (not_inl_lt_inr h).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 : NoMaxOrder (α ⊕ β)
a : β
inl : ∀ (b : α) (h : Sum.inr a < Sum.inl b), ∃ (b : β), a < b
inr : ∀ (b : β) (h : LT.lt (α := α ⊕ β) (Sum.inr a) (Sum.inr b)), ∃ (b : β), a < b
⊢ ∃ (b : β), a < b

Tactic:
obtain ⟨b | b, h⟩ := exists_gt (inr a : α ⊕ β)

Premises used: NoMaxOrder.exists_gt, Sum.inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : NoMaxOrder (α ⊕ β)
a : β
b : α
h : inr a < inl b
⊢ ∃ (b : β), a < b

Tactic:
(not_inr_lt_inl h).elim

Premises used: False.elim, Sum.not_inr_lt_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : NoMaxOrder (α ⊕ β)
a : β
b : α
h : inr a < inl b
⊢ ∃ (b : β), a < b

Tactic:
exact (not_inr_lt_inl h).elim

Premises used: False.elim, Sum.not_inr_lt_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : NoMaxOrder (α ⊕ β)
a b : β
h : LT.lt (α := α ⊕ β) (inr a) (inr b)
⊢ ∃ (b : β), a < b

Tactic:
⟨b, inr_lt_inr_iff.1 h⟩

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

Tactic:
exact ⟨b, inr_lt_inr_iff.1 h⟩
-- 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 β
⊢ DenselyOrdered (α ⊕ β)

Tactic:
⟨fun a b h =>
    match a, b, h with
    | inl _, inl _, LiftRel.inl h =>
      let ⟨c, ha, hb⟩ := exists_between h
      ⟨toLex (inl c), LiftRel.inl ha, LiftRel.inl hb⟩
    | inr _, inr _, LiftRel.inr h =>
      let ⟨c, ha, hb⟩ := exists_between h
      ⟨toLex (inr c), LiftRel.inr ha, LiftRel.inr hb⟩⟩

Premises used: Sum.LiftRel.inl, Exists, Sum.inl, exists_between, Sum.LiftRel.inr, DenselyOrdered.mk, And, Sum.inr, _private.0.Sum.denselyOrdered.match_1, And.intro, LT.lt, Exists.intro, _private.0.Sum.denselyOrdered.match_2, DFunLike.coe, toLex