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 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
a₂ : α
b₁ : β
⊢ Icc (inr b₁) (inl a₂) = ∅

Tactic:
rfl

Premises used: Finset.Icc, Finset.sumLift₂, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
a₂ : α
b₁ : β
⊢ Ico (inr b₁) (inl a₂) = ∅

Tactic:
rfl

Premises used: Finset.Ico, Finset.sumLift₂, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
a₂ : α
b₁ : β
⊢ Ioc (inr b₁) (inl a₂) = ∅

Tactic:
rfl

Premises used: Finset.sumLift₂, rfl, Finset.Ioc
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
a₂ : α
b₁ : β
⊢ Ioo (inr b₁) (inl a₂) = ∅

Tactic:
rfl

Premises used: Finset.Ioo, Finset.sumLift₂, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Eq (α := Finset (α ⊕ β)) (Icc (inr b₁) (inr b₂)) (map Embedding.inr (Icc b₁ b₂))

Tactic:
rfl

Premises used: Finset.map, Finset.Icc, Finset.sumLift₂, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Eq (α := Finset (α ⊕ β)) (Ico (inr b₁) (inr b₂)) (map Embedding.inr (Ico b₁ b₂))

Tactic:
rfl

Premises used: Finset.map, Finset.Ico, Finset.sumLift₂, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Eq (α := Finset (α ⊕ β)) (Ioc (inr b₁) (inr b₂)) (map Embedding.inr (Ioc b₁ b₂))

Tactic:
rfl

Premises used: Finset.map, Finset.sumLift₂, rfl, Finset.Ioc
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Eq (α := Finset (α ⊕ β)) (Ioo (inr b₁) (inr b₂)) (map Embedding.inr (Ioo b₁ b₂))

Tactic:
rfl

Premises used: Finset.map, Finset.Ioo, Finset.sumLift₂, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderBot α
inst_3 : LocallyFiniteOrderBot β
⊢ ∀ (a x : α ⊕ β),
    Membership.mem (γ := Finset (α ⊕ β))
        (Sum.elim (fun (x : α) ↦ map Embedding.inl (Iic x)) (fun (x : β) ↦ map Embedding.inr (Iic x)) a) x ↔
      x ≤ a

Tactic:
simp
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderBot α
inst_3 : LocallyFiniteOrderBot β
⊢ ∀ (a x : α ⊕ β),
    Membership.mem (γ := Finset (α ⊕ β))
        (Sum.elim (fun (x : α) ↦ map Embedding.inl (Iio x)) (fun (x : β) ↦ map Embedding.inr (Iio x)) a) x ↔
      x < a

Tactic:
simp
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderBot α
inst_3 : LocallyFiniteOrderBot β
a : α
⊢ Eq (α := Finset (α ⊕ β)) (Iic (inl a)) (map Embedding.inl (Iic a))

Tactic:
rfl

Premises used: Finset.map, Finset.Iic, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderBot α
inst_3 : LocallyFiniteOrderBot β
b : β
⊢ Eq (α := Finset (α ⊕ β)) (Iic (inr b)) (map Embedding.inr (Iic b))

Tactic:
rfl

Premises used: Finset.map, Finset.Iic, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderBot α
inst_3 : LocallyFiniteOrderBot β
a : α
⊢ Eq (α := Finset (α ⊕ β)) (Iio (inl a)) (map Embedding.inl (Iio a))

Tactic:
rfl

Premises used: Finset.Iio, Finset.map, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrderBot α
inst_3 : LocallyFiniteOrderBot β
b : β
⊢ Eq (α := Finset (α ⊕ β)) (Iio (inr b)) (map Embedding.inr (Iio b))

Tactic:
rfl

Premises used: Finset.Iio, 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 : LocallyFiniteOrderTop β
⊢ ∀ (a x : α ⊕ β),
    Membership.mem (γ := Finset (α ⊕ β))
        (Sum.elim (fun (x : α) ↦ map Embedding.inl (Ici x)) (fun (x : β) ↦ map Embedding.inr (Ici x)) 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 : LocallyFiniteOrderTop β
⊢ ∀ (a x : α ⊕ β),
    Membership.mem (γ := Finset (α ⊕ β))
        (Sum.elim (fun (x : α) ↦ map Embedding.inl (Ioi x)) (fun (x : β) ↦ map Embedding.inr (Ioi x)) 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 : LocallyFiniteOrderTop β
a : α
⊢ Eq (α := Finset (α ⊕ β)) (Ici (inl a)) (map Embedding.inl (Ici a))

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 : LocallyFiniteOrderTop β
b : β
⊢ Eq (α := Finset (α ⊕ β)) (Ici (inr b)) (map Embedding.inr (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 : LocallyFiniteOrderTop β
a : α
⊢ Eq (α := Finset (α ⊕ β)) (Ioi (inl a)) (map Embedding.inl (Ioi a))

Tactic:
rfl

Premises used: Finset.Ioi, 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 : LocallyFiniteOrderTop β
b : β
⊢ Eq (α := Finset (α ⊕ β)) (Ioi (inr b)) (map Embedding.inr (Ioi b))

Tactic:
rfl

Premises used: Finset.Ioi, Finset.map, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
⊢ ∀ (a b x : _root_.Lex (α ⊕ β)),
    Membership.mem (γ := Finset (_root_.Lex (α ⊕ β)))
        (map (Equiv.toEmbedding toLex)
          (sumLexLift Icc Icc (fun (a : α) (x : β) ↦ Ici a) (fun (x : α) ↦ Iic)
            ((ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) a) ((ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) b)))
        x ↔
      a ≤ x ∧ x ≤ b

Tactic:
simp
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
⊢ ∀ (a b x : _root_.Lex (α ⊕ β)),
    Membership.mem (γ := Finset (_root_.Lex (α ⊕ β)))
        (map (Equiv.toEmbedding toLex)
          (sumLexLift Ico Ico (fun (a : α) (x : β) ↦ Ici a) (fun (x : α) ↦ Iio)
            ((ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) a) ((ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) b)))
        x ↔
      a ≤ x ∧ x < b

Tactic:
simp
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
⊢ ∀ (a b x : _root_.Lex (α ⊕ β)),
    Membership.mem (γ := Finset (_root_.Lex (α ⊕ β)))
        (map (Equiv.toEmbedding toLex)
          (sumLexLift Ioc Ioc (fun (a : α) (x : β) ↦ Ioi a) (fun (x : α) ↦ Iic)
            ((ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) a) ((ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) b)))
        x ↔
      a < x ∧ x ≤ b

Tactic:
simp
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
⊢ ∀ (a b x : _root_.Lex (α ⊕ β)),
    Membership.mem (γ := Finset (_root_.Lex (α ⊕ β)))
        (map (Equiv.toEmbedding toLex)
          (sumLexLift Ioo Ioo (fun (a : α) (x : β) ↦ Ioi a) (fun (x : α) ↦ Iio)
            ((ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) a) ((ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) b)))
        x ↔
      a < x ∧ x < b

Tactic:
simp
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a₁ a₂ : α
rw :
  Eq (α := Finset (_root_.Lex (α ⊕ β))) (Icc (inlₗ a₁) (inlₗ a₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inl (Icc a₁ a₂)))
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Icc (inlₗ a₁) (inlₗ a₂))
    (map (Embedding.trans Embedding.inl (Equiv.toEmbedding toLex)) (Icc a₁ a₂))

Tactic:
rw [← Finset.map_map]

Premises used: Finset.map_map
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Icc (inlₗ a₁) (inlₗ a₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inl (Icc a₁ a₂)))

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a₁ a₂ : α
rw :
  Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ico (inlₗ a₁) (inlₗ a₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inl (Ico a₁ a₂)))
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ico (inlₗ a₁) (inlₗ a₂))
    (map (Embedding.trans Embedding.inl (Equiv.toEmbedding toLex)) (Ico a₁ a₂))

Tactic:
rw [← Finset.map_map]

Premises used: Finset.map_map
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ico (inlₗ a₁) (inlₗ a₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inl (Ico a₁ a₂)))

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a₁ a₂ : α
rw :
  Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioc (inlₗ a₁) (inlₗ a₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inl (Ioc a₁ a₂)))
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioc (inlₗ a₁) (inlₗ a₂))
    (map (Embedding.trans Embedding.inl (Equiv.toEmbedding toLex)) (Ioc a₁ a₂))

Tactic:
rw [← Finset.map_map]

Premises used: Finset.map_map
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioc (inlₗ a₁) (inlₗ a₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inl (Ioc a₁ a₂)))

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a₁ a₂ : α
rw :
  Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioo (inlₗ a₁) (inlₗ a₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inl (Ioo a₁ a₂)))
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioo (inlₗ a₁) (inlₗ a₂))
    (map (Embedding.trans Embedding.inl (Equiv.toEmbedding toLex)) (Ioo a₁ a₂))

Tactic:
rw [← Finset.map_map]

Premises used: Finset.map_map
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioo (inlₗ a₁) (inlₗ a₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inl (Ioo a₁ a₂)))

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a : α
b : β
⊢ Icc (inlₗ a) (inrₗ b) = map (Equiv.toEmbedding toLex) ((Ici a).disjSum (Iic b))

Tactic:
rfl

Premises used: Lex, Finset.map, Finset.Icc, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a : α
b : β
⊢ Ico (inlₗ a) (inrₗ b) = map (Equiv.toEmbedding toLex) ((Ici a).disjSum (Iio b))

Tactic:
rfl

Premises used: Lex, Finset.map, Finset.Ico, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a : α
b : β
⊢ Ioc (inlₗ a) (inrₗ b) = map (Equiv.toEmbedding toLex) ((Ioi a).disjSum (Iic b))

Tactic:
rfl

Premises used: Lex, Finset.map, rfl, Finset.Ioc
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a : α
b : β
⊢ Ioo (inlₗ a) (inrₗ b) = map (Equiv.toEmbedding toLex) ((Ioi a).disjSum (Iio b))

Tactic:
rfl

Premises used: Lex, Finset.map, Finset.Ioo, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a : α
b : β
⊢ Icc (inrₗ b) (inlₗ a) = ∅

Tactic:
rfl

Premises used: Multiset.map, List.map, Finset.map, Multiset.zero, Finset.empty, Finset.Icc, Multiset.ofList, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a : α
b : β
⊢ Ico (inrₗ b) (inlₗ a) = ∅

Tactic:
rfl

Premises used: Multiset.map, List.map, Finset.map, Finset.Ico, Multiset.zero, Finset.empty, Multiset.ofList, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a : α
b : β
⊢ Ioc (inrₗ b) (inlₗ a) = ∅

Tactic:
rfl

Premises used: Multiset.map, List.map, Finset.map, Multiset.zero, Finset.empty, Multiset.ofList, rfl, Finset.Ioc
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a : α
b : β
⊢ Ioo (inrₗ b) (inlₗ a) = ∅

Tactic:
rfl

Premises used: Multiset.map, List.map, Finset.map, Multiset.zero, Finset.empty, Multiset.ofList, Finset.Ioo, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
b₁ b₂ : β
rw :
  Eq (α := Finset (_root_.Lex (α ⊕ β))) (Icc (inrₗ b₁) (inrₗ b₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inr (Icc b₁ b₂)))
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Icc (inrₗ b₁) (inrₗ b₂))
    (map (Embedding.trans Embedding.inr (Equiv.toEmbedding toLex)) (Icc b₁ b₂))

Tactic:
rw [← Finset.map_map]

Premises used: Finset.map_map
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Icc (inrₗ b₁) (inrₗ b₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inr (Icc b₁ b₂)))

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
b₁ b₂ : β
rw :
  Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ico (inrₗ b₁) (inrₗ b₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inr (Ico b₁ b₂)))
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ico (inrₗ b₁) (inrₗ b₂))
    (map (Embedding.trans Embedding.inr (Equiv.toEmbedding toLex)) (Ico b₁ b₂))

Tactic:
rw [← Finset.map_map]

Premises used: Finset.map_map
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ico (inrₗ b₁) (inrₗ b₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inr (Ico b₁ b₂)))

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
b₁ b₂ : β
rw :
  Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioc (inrₗ b₁) (inrₗ b₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inr (Ioc b₁ b₂)))
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioc (inrₗ b₁) (inrₗ b₂))
    (map (Embedding.trans Embedding.inr (Equiv.toEmbedding toLex)) (Ioc b₁ b₂))

Tactic:
rw [← Finset.map_map]

Premises used: Finset.map_map
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioc (inrₗ b₁) (inrₗ b₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inr (Ioc b₁ b₂)))

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
b₁ b₂ : β
rw :
  Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioo (inrₗ b₁) (inrₗ b₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inr (Ioo b₁ b₂)))
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioo (inrₗ b₁) (inrₗ b₂))
    (map (Embedding.trans Embedding.inr (Equiv.toEmbedding toLex)) (Ioo b₁ b₂))

Tactic:
rw [← Finset.map_map]

Premises used: Finset.map_map
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioo (inrₗ b₁) (inrₗ b₂))
    (map (Equiv.toEmbedding toLex) (map Embedding.inr (Ioo b₁ b₂)))

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : LocallyFiniteOrderBot α
inst_4 : LocallyFiniteOrderBot β
⊢ ∀ (a x : _root_.Lex (α ⊕ β)),
    Membership.mem (γ := Finset (_root_.Lex (α ⊕ β)))
        (comp (β := α ⊕ β)
          (Sum.elim (fun (x : α) ↦ map (Embedding.trans Embedding.inl (Equiv.toEmbedding toLex)) (Iic x)) fun (x : β) ↦
            map (Equiv.toEmbedding toLex) (disjSum univ (Iic x)))
          (⇑ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) a)
        x ↔
      x ≤ a

Tactic:
simp
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : LocallyFiniteOrderBot α
inst_4 : LocallyFiniteOrderBot β
⊢ ∀ (a x : _root_.Lex (α ⊕ β)),
    Membership.mem (γ := Finset (_root_.Lex (α ⊕ β)))
        (comp (β := α ⊕ β)
          (Sum.elim (fun (x : α) ↦ map (Embedding.trans Embedding.inl (Equiv.toEmbedding toLex)) (Iio x)) fun (x : β) ↦
            map (Equiv.toEmbedding toLex) (disjSum univ (Iio x)))
          (⇑ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) a)
        x ↔
      x < a

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: Finset.Iio, Finset.map, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : OrderBot α
inst_4 : OrderBot β
inst_5 : OrderTop α
inst_6 : LocallyFiniteOrder α
inst_7 : LocallyFiniteOrder β
⊢ Eq (α := LocallyFiniteOrderBot (_root_.Lex (α ⊕ β))) LocallyFiniteOrder.toLocallyFiniteOrderBot
    instLocallyFiniteOrderBot

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Preorder α
inst_2 : Preorder β
inst_3 : OrderBot α
inst_4 : OrderBot β
inst_5 : OrderTop α
inst_6 : LocallyFiniteOrder α
inst_7 : LocallyFiniteOrder β
⊢ Eq (α := LocallyFiniteOrderBot (_root_.Lex (α ⊕ β))) LocallyFiniteOrder.toLocallyFiniteOrderBot
    instLocallyFiniteOrderBot

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.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 x : _root_.Lex (α ⊕ β)),
    Membership.mem (γ := Finset (_root_.Lex (α ⊕ β)))
        (comp (β := α ⊕ β)
          (Sum.elim (fun (x : α) ↦ map (Equiv.toEmbedding toLex) ((Ici x).disjSum univ)) fun (x : β) ↦
            map (Embedding.trans Embedding.inr (Equiv.toEmbedding toLex)) (Ici x))
          (⇑ofLex : (a : _root_.Lex (α ⊕ β)) → α ⊕ β) a)
        x ↔
      a ≤ x

Tactic:
simp