awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
b : β
⊢ Eq (α := Sum.{u_1, u_2} αᵒᵈ βᵒᵈ)
    ((sumDualDistrib α β : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) ((toDual : (a : α ⊕ β) → (α ⊕ β)ᵒᵈ) (inr b)) :
      Sum.{u_1, u_2} αᵒᵈ βᵒᵈ)
    (inr ((toDual : (a : β) → βᵒᵈ) b) : Sum.{u_1, u_2} αᵒᵈ βᵒᵈ)

Tactic:
rfl

Premises used: OrderDual, rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
a : α
⊢ Eq (α := (α ⊕ β)ᵒᵈ)
    ((symm (sumDualDistrib α β) : (a : αᵒᵈ ⊕ βᵒᵈ) → (α ⊕ β)ᵒᵈ) (inl ((toDual : (a : α) → αᵒᵈ) a)) : (α ⊕ β)ᵒᵈ)
    ((toDual : (a : α ⊕ β) → (α ⊕ β)ᵒᵈ) (inl a) : (α ⊕ β)ᵒᵈ)

Tactic:
rfl

Premises used: OrderDual, rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
b : β
⊢ Eq (α := (α ⊕ β)ᵒᵈ)
    ((symm (sumDualDistrib α β) : (a : αᵒᵈ ⊕ βᵒᵈ) → (α ⊕ β)ᵒᵈ) (inr ((toDual : (a : β) → βᵒᵈ) b)) : (α ⊕ β)ᵒᵈ)
    ((toDual : (a : α ⊕ β) → (α ⊕ β)ᵒᵈ) (inr b) : (α ⊕ β)ᵒᵈ)

Tactic:
rfl

Premises used: OrderDual, rfl
-- 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_1 : α
b_1 : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a b : α₁
⊢ LE.le (α := _root_.Lex (α₂ ⊕ β₂))
      ((Equiv.trans ofLex (((↑ea : α₁ ≃ α₂).sumCongr (↑eb : β₁ ≃ β₂)).trans toLex) :
            (a : _root_.Lex (α₁ ⊕ β₁)) → _root_.Lex (α₂ ⊕ β₂))
          ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inl a)) :
        _root_.Lex (α₂ ⊕ β₂))
      ((Equiv.trans ofLex (((↑ea : α₁ ≃ α₂).sumCongr (↑eb : β₁ ≃ β₂)).trans toLex) :
            (a : _root_.Lex (α₁ ⊕ β₁)) → _root_.Lex (α₂ ⊕ β₂))
          ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inl b)) :
        _root_.Lex (α₂ ⊕ β₂)) ↔
    LE.le (α := _root_.Lex (α₁ ⊕ β₁)) ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inl a) : _root_.Lex (α₁ ⊕ β₁))
      ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inl b) : _root_.Lex (α₁ ⊕ β₁))

Tactic:
simp
-- 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_1 : α
b_1 : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a : α₁
b : β₁
⊢ LE.le (α := _root_.Lex (α₂ ⊕ β₂))
      ((Equiv.trans ofLex (((↑ea : α₁ ≃ α₂).sumCongr (↑eb : β₁ ≃ β₂)).trans toLex) :
            (a : _root_.Lex (α₁ ⊕ β₁)) → _root_.Lex (α₂ ⊕ β₂))
          ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inl a)) :
        _root_.Lex (α₂ ⊕ β₂))
      ((Equiv.trans ofLex (((↑ea : α₁ ≃ α₂).sumCongr (↑eb : β₁ ≃ β₂)).trans toLex) :
            (a : _root_.Lex (α₁ ⊕ β₁)) → _root_.Lex (α₂ ⊕ β₂))
          ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inr b)) :
        _root_.Lex (α₂ ⊕ β₂)) ↔
    LE.le (α := _root_.Lex (α₁ ⊕ β₁)) ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inl a) : _root_.Lex (α₁ ⊕ β₁))
      ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inr b) : _root_.Lex (α₁ ⊕ β₁))

Tactic:
simp
-- 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_1 : α
b_1 : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a : β₁
b : α₁
⊢ LE.le (α := _root_.Lex (α₂ ⊕ β₂))
      ((Equiv.trans ofLex (((↑ea : α₁ ≃ α₂).sumCongr (↑eb : β₁ ≃ β₂)).trans toLex) :
            (a : _root_.Lex (α₁ ⊕ β₁)) → _root_.Lex (α₂ ⊕ β₂))
          ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inr a)) :
        _root_.Lex (α₂ ⊕ β₂))
      ((Equiv.trans ofLex (((↑ea : α₁ ≃ α₂).sumCongr (↑eb : β₁ ≃ β₂)).trans toLex) :
            (a : _root_.Lex (α₁ ⊕ β₁)) → _root_.Lex (α₂ ⊕ β₂))
          ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inl b)) :
        _root_.Lex (α₂ ⊕ β₂)) ↔
    LE.le (α := _root_.Lex (α₁ ⊕ β₁)) ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inr a) : _root_.Lex (α₁ ⊕ β₁))
      ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inl b) : _root_.Lex (α₁ ⊕ β₁))

Tactic:
simp
-- 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_1 : α
b_1 : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a b : β₁
⊢ LE.le (α := _root_.Lex (α₂ ⊕ β₂))
      ((Equiv.trans ofLex (((↑ea : α₁ ≃ α₂).sumCongr (↑eb : β₁ ≃ β₂)).trans toLex) :
            (a : _root_.Lex (α₁ ⊕ β₁)) → _root_.Lex (α₂ ⊕ β₂))
          ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inr a)) :
        _root_.Lex (α₂ ⊕ β₂))
      ((Equiv.trans ofLex (((↑ea : α₁ ≃ α₂).sumCongr (↑eb : β₁ ≃ β₂)).trans toLex) :
            (a : _root_.Lex (α₁ ⊕ β₁)) → _root_.Lex (α₂ ⊕ β₂))
          ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inr b)) :
        _root_.Lex (α₂ ⊕ β₂)) ↔
    LE.le (α := _root_.Lex (α₁ ⊕ β₁)) ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inr a) : _root_.Lex (α₁ ⊕ β₁))
      ((toLex : (a : α₁ ⊕ β₁) → _root_.Lex (α₁ ⊕ β₁)) (inr b) : _root_.Lex (α₁ ⊕ β₁))

Tactic:
simp
-- 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 : _root_.Lex (α₁ ⊕ α₂)),
    Eq (α := _root_.Lex (γ₁ ⊕ γ₂))
      (((e₁.sumLexCongr e₂).trans (f₁.sumLexCongr f₂) : (a : _root_.Lex (α₁ ⊕ α₂)) → _root_.Lex (γ₁ ⊕ γ₂)) x :
        _root_.Lex (γ₁ ⊕ γ₂))
      (((e₁.trans f₁).sumLexCongr (e₂.trans f₂) : (a : _root_.Lex (α₁ ⊕ α₂)) → _root_.Lex (γ₁ ⊕ γ₂)) x :
        _root_.Lex (γ₁ ⊕ γ₂))
⊢ (e₁.sumLexCongr e₂).trans (f₁.sumLexCongr f₂) = (e₁.trans f₁).sumLexCongr (e₂.trans f₂)

Tactic:
ext
-- 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 γ₂
x : _root_.Lex (α₁ ⊕ α₂)
⊢ Eq (α := _root_.Lex (γ₁ ⊕ γ₂))
    (((e₁.sumLexCongr e₂).trans (f₁.sumLexCongr f₂) : (a : _root_.Lex (α₁ ⊕ α₂)) → _root_.Lex (γ₁ ⊕ γ₂)) x :
      _root_.Lex (γ₁ ⊕ γ₂))
    (((e₁.trans f₁).sumLexCongr (e₂.trans f₂) : (a : _root_.Lex (α₁ ⊕ α₂)) → _root_.Lex (γ₁ ⊕ γ₂)) x :
      _root_.Lex (γ₁ ⊕ γ₂))

Tactic:
simp
-- Module: Mathlib.Data.Sum.Order
Goal:
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
inst : LE α₁
inst_1 : LE α₂
inst_2 : LE β₁
inst_3 : LE β₂
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
⊢ (ea.sumLexCongr eb).symm = ea.symm.sumLexCongr eb.symm

Tactic:
rfl

Premises used: Sum.map, Equiv.trans, Lex, RelIso.symm, OrderIso.symm, OrderIso.sumLexCongr, Equiv.symm, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
h :
  ∀ (x : _root_.Lex (α ⊕ β)),
    Eq (α := _root_.Lex (α ⊕ β))
      ((sumLexCongr (refl α) (refl β) : (a : _root_.Lex (α ⊕ β)) → _root_.Lex (α ⊕ β)) x : _root_.Lex (α ⊕ β))
      ((refl (_root_.Lex (α ⊕ β)) : (a : _root_.Lex (α ⊕ β)) → _root_.Lex (α ⊕ β)) x : _root_.Lex (α ⊕ β))
⊢ Eq (α := _root_.Lex (α ⊕ β) ≃o _root_.Lex (α ⊕ β)) (sumLexCongr (refl α) (refl β)) (refl (_root_.Lex (α ⊕ β)))

Tactic:
ext
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
x : _root_.Lex (α ⊕ β)
⊢ Eq (α := _root_.Lex (α ⊕ β))
    ((sumLexCongr (refl α) (refl β) : (a : _root_.Lex (α ⊕ β)) → _root_.Lex (α ⊕ β)) x : _root_.Lex (α ⊕ β))
    ((refl (_root_.Lex (α ⊕ β)) : (a : _root_.Lex (α ⊕ β)) → _root_.Lex (α ⊕ β)) x : _root_.Lex (α ⊕ β))

Tactic:
simp
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : LE β
inst_2 : LE γ
a : α
⊢ Eq (α := _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))
    ((sumLexAssoc α β γ : (a : _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ)) → _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))
        ((toLex : (a : _root_.Lex (α ⊕ β) ⊕ γ) → _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ))
          (inl ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl a)))) :
      _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))
    ((toLex : (a : α ⊕ _root_.Lex (β ⊕ γ)) → _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ))) (inl a) :
      _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))

Tactic:
rfl

Premises used: Lex, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : LE β
inst_2 : LE γ
b : β
⊢ Eq (α := _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))
    ((sumLexAssoc α β γ : (a : _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ)) → _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))
        ((toLex : (a : _root_.Lex (α ⊕ β) ⊕ γ) → _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ))
          (inl ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inr b)))) :
      _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))
    ((toLex : (a : α ⊕ _root_.Lex (β ⊕ γ)) → _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))
        (inr ((toLex : (a : β ⊕ γ) → _root_.Lex (β ⊕ γ)) (inl b))) :
      _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))

Tactic:
rfl

Premises used: Lex, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : LE β
inst_2 : LE γ
c : γ
⊢ Eq (α := _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))
    ((sumLexAssoc α β γ : (a : _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ)) → _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))
        ((toLex : (a : _root_.Lex (α ⊕ β) ⊕ γ) → _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ)) (inr c)) :
      _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))
    ((toLex : (a : α ⊕ _root_.Lex (β ⊕ γ)) → _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))
        (inr ((toLex : (a : β ⊕ γ) → _root_.Lex (β ⊕ γ)) (inr c))) :
      _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ)))

Tactic:
rfl

Premises used: Lex, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : LE β
inst_2 : LE γ
a : α
⊢ Eq (α := _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ))
    ((symm (sumLexAssoc α β γ) : (a : _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ))) → _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ))
        (inl a) :
      _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ))
    (inl (inl a) : (α ⊕ β) ⊕ γ)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : LE β
inst_2 : LE γ
b : β
⊢ Eq (α := _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ))
    ((symm (sumLexAssoc α β γ) : (a : _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ))) → _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ))
        (inr (inl b)) :
      _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ))
    (inl (inr b) : (α ⊕ β) ⊕ γ)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : LE β
inst_2 : LE γ
c : γ
⊢ Eq (α := _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ))
    ((symm (sumLexAssoc α β γ) : (a : _root_.Lex (α ⊕ _root_.Lex (β ⊕ γ))) → _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ))
        (inr (inr c)) :
      _root_.Lex (_root_.Lex (α ⊕ β) ⊕ γ))
    (inr c : _root_.Lex (α ⊕ β) ⊕ γ)

Tactic:
rfl

Premises used: Lex, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α_1 : Type u_1
β_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 α_1
inst_1 : LE β_1
inst_2 : LE γ
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a_1 : α_1
b_1 : β_1
c : γ
α : Type u_10
β : Type u_11
inst_9 : LE α
inst_10 : LE β
a b : (_root_.Lex (α ⊕ β))ᵒᵈ
inl :
  ∀ (a : α),
    LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
        ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inl a) :
          _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
        ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) b :
          _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
      Sum.inl a ≤ b
inr :
  ∀ (a : β),
    LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
        ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inr a) :
          _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
        ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) b :
          _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
      Sum.inr a ≤ b
⊢ LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) a :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) b :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    a ≤ b

Tactic:
rcases a with (a | a)
-- Module: Mathlib.Data.Sum.Order
Goal:
α_1 : Type u_1
β_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 α_1
inst_1 : LE β_1
inst_2 : LE γ
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a_1 : α_1
b_1 : β_1
c : γ
α : Type u_10
β : Type u_11
inst_9 : LE α
inst_10 : LE β
b : (_root_.Lex (α ⊕ β))ᵒᵈ
a : α
inl :
  ∀ (b : α),
    LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
        ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inl a) :
          _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
        ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inl b) :
          _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
      LE.le (α := (_root_.Lex (α ⊕ β))ᵒᵈ) (Sum.inl a) (Sum.inl b)
inl₁ :
  ∀ (b : β),
    LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
        ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inl a) :
          _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
        ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inr b) :
          _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
      Sum.inl a ≤ inr b
⊢ LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inl a) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) b :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    Sum.inl a ≤ b

Tactic:
rcases b with (b | b)
-- Module: Mathlib.Data.Sum.Order
Goal:
α_1 : Type u_1
β_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 α_1
inst_1 : LE β_1
inst_2 : LE γ
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a_1 : α_1
b_1 : β_1
c : γ
α : Type u_10
β : Type u_11
inst_9 : LE α
inst_10 : LE β
b : (_root_.Lex (α ⊕ β))ᵒᵈ
a : β
inr :
  ∀ (b : α),
    LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
        ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inr a) :
          _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
        ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inl b) :
          _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
      Sum.inr a ≤ inl b
inr₁ :
  ∀ (b : β),
    LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
        ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inr a) :
          _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
        ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inr b) :
          _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
      LE.le (α := (_root_.Lex (α ⊕ β))ᵒᵈ) (Sum.inr a) (Sum.inr b)
⊢ LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inr a) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) b :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    Sum.inr a ≤ b

Tactic:
rcases b with (b | b)
-- Module: Mathlib.Data.Sum.Order
Goal:
α_1 : Type u_1
β_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 α_1
inst_1 : LE β_1
inst_2 : LE γ
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a_1 : α_1
b_1 : β_1
c : γ
α : Type u_10
β : Type u_11
inst_9 : LE α
inst_10 : LE β
a b : α
inl :
  LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((toLex : (a : βᵒᵈ ⊕ αᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inr ((toDual : (a : α) → αᵒᵈ) a)) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((toLex : (a : βᵒᵈ ⊕ αᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inr ((toDual : (a : α) → αᵒᵈ) b)) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    LE.le (α := (_root_.Lex (α ⊕ β))ᵒᵈ)
      ((toDual : (a : _root_.Lex (α ⊕ β)) → (_root_.Lex (α ⊕ β))ᵒᵈ)
          ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (Sum.inl a)) :
        (_root_.Lex (α ⊕ β))ᵒᵈ)
      ((toDual : (a : _root_.Lex (α ⊕ β)) → (_root_.Lex (α ⊕ β))ᵒᵈ)
          ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (Sum.inl b)) :
        (_root_.Lex (α ⊕ β))ᵒᵈ)
⊢ LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inl a) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inl b) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    LE.le (α := (_root_.Lex (α ⊕ β))ᵒᵈ) (Sum.inl a) (Sum.inl b)

Tactic:
change
          toLex (inr <| toDual a) ≤ toLex (inr <| toDual b) ↔
            toDual (toLex <| inl a) ≤ toDual (toLex <| inl b)

Premises used: OrderDual.toDual, Sum.inl, Sum.inr, DFunLike.coe, toLex
-- Module: Mathlib.Data.Sum.Order
Goal:
α_1 : Type u_1
β_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 α_1
inst_1 : LE β_1
inst_2 : LE γ
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a_1 : α_1
b_1 : β_1
c : γ
α : Type u_10
β : Type u_11
inst_9 : LE α
inst_10 : LE β
a b : α
⊢ LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((toLex : (a : βᵒᵈ ⊕ αᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inr ((toDual : (a : α) → αᵒᵈ) a)) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((toLex : (a : βᵒᵈ ⊕ αᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inr ((toDual : (a : α) → αᵒᵈ) b)) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    LE.le (α := (_root_.Lex (α ⊕ β))ᵒᵈ)
      ((toDual : (a : _root_.Lex (α ⊕ β)) → (_root_.Lex (α ⊕ β))ᵒᵈ)
          ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl a)) :
        (_root_.Lex (α ⊕ β))ᵒᵈ)
      ((toDual : (a : _root_.Lex (α ⊕ β)) → (_root_.Lex (α ⊕ β))ᵒᵈ)
          ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl b)) :
        (_root_.Lex (α ⊕ β))ᵒᵈ)

Tactic:
simp [toDual_le_toDual]

Premises used: OrderDual.toDual_le_toDual
-- Module: Mathlib.Data.Sum.Order
Goal:
α_1 : Type u_1
β_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 α_1
inst_1 : LE β_1
inst_2 : LE γ
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a_1 : α_1
b_1 : β_1
c : γ
α : Type u_10
β : Type u_11
inst_9 : LE α
inst_10 : LE β
a : α
b : β
⊢ LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inl a) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inr b) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    inl a ≤ inr b

Tactic:
iff_of_false (@Lex.not_inr_le_inl (OrderDual β) (OrderDual α) _ _ _ _)
          Lex.not_inr_le_inl

Premises used: iff_of_false, Sum.Lex.not_inr_le_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α_1 : Type u_1
β_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 α_1
inst_1 : LE β_1
inst_2 : LE γ
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a_1 : α_1
b_1 : β_1
c : γ
α : Type u_10
β : Type u_11
inst_9 : LE α
inst_10 : LE β
a : α
b : β
⊢ LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inl a) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inr b) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    inl a ≤ inr b

Tactic:
exact iff_of_false (@Lex.not_inr_le_inl (OrderDual β) (OrderDual α) _ _ _ _)
          Lex.not_inr_le_inl

Premises used: iff_of_false, Sum.Lex.not_inr_le_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α_1 : Type u_1
β_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 α_1
inst_1 : LE β_1
inst_2 : LE γ
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a_1 : α_1
b_1 : β_1
c : γ
α : Type u_10
β : Type u_11
inst_9 : LE α
inst_10 : LE β
a : β
b : α
⊢ LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inr a) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inl b) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    inr a ≤ inl b

Tactic:
iff_of_true (@Lex.inl_le_inr (OrderDual β) (OrderDual α) _ _ _ _)
          (Lex.inl_le_inr _ _)

Premises used: iff_of_true, Sum.Lex.inl_le_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α_1 : Type u_1
β_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 α_1
inst_1 : LE β_1
inst_2 : LE γ
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a_1 : α_1
b_1 : β_1
c : γ
α : Type u_10
β : Type u_11
inst_9 : LE α
inst_10 : LE β
a : β
b : α
⊢ LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inr a) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inl b) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    inr a ≤ inl b

Tactic:
exact iff_of_true (@Lex.inl_le_inr (OrderDual β) (OrderDual α) _ _ _ _)
          (Lex.inl_le_inr _ _)

Premises used: iff_of_true, Sum.Lex.inl_le_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α_1 : Type u_1
β_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 α_1
inst_1 : LE β_1
inst_2 : LE γ
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a_1 : α_1
b_1 : β_1
c : γ
α : Type u_10
β : Type u_11
inst_9 : LE α
inst_10 : LE β
a b : β
inr :
  LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((toLex : (a : βᵒᵈ ⊕ αᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inl ((toDual : (a : β) → βᵒᵈ) a)) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((toLex : (a : βᵒᵈ ⊕ αᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inl ((toDual : (a : β) → βᵒᵈ) b)) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    LE.le (α := (_root_.Lex (α ⊕ β))ᵒᵈ)
      ((toDual : (a : _root_.Lex (α ⊕ β)) → (_root_.Lex (α ⊕ β))ᵒᵈ)
          ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (Sum.inr a)) :
        (_root_.Lex (α ⊕ β))ᵒᵈ)
      ((toDual : (a : _root_.Lex (α ⊕ β)) → (_root_.Lex (α ⊕ β))ᵒᵈ)
          ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (Sum.inr b)) :
        (_root_.Lex (α ⊕ β))ᵒᵈ)
⊢ LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inr a) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((Equiv.sumComm α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (Sum.inr b) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    LE.le (α := (_root_.Lex (α ⊕ β))ᵒᵈ) (Sum.inr a) (Sum.inr b)

Tactic:
change
          toLex (inl <| toDual a) ≤ toLex (inl <| toDual b) ↔
            toDual (toLex <| inr a) ≤ toDual (toLex <| inr b)

Premises used: OrderDual.toDual, Sum.inl, Sum.inr, DFunLike.coe, toLex