awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : 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 γ_1
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a : α_1
b_1 : β_1
c : γ_1
α : Type u_10
β : Type u_11
γ : Type u_12
inst_9 : LE α
inst_10 : LE β
inst_11 : LE γ
b : (α ⊕ β) ⊕ γ
val : γ
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inr val) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    inr val ≤ b
have inr : ∀ (val_1 : α),
  LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inr val) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inl val_1)) : α ⊕ β ⊕ γ) ↔
    LE.le (α := (α ⊕ β) ⊕ γ) (inr val) (inl (inl val_1))
Tactic: rcases b with ((_ | _) | _)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : 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 γ_1
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a : α_1
b_1 : β_1
c : γ_1
α : Type u_10
β : Type u_11
γ : Type u_12
inst_9 : LE α
inst_10 : LE β
inst_11 : LE γ
b : (α ⊕ β) ⊕ γ
val : γ
inr :
  ∀ (val_1 : α),
    LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inr val) : α ⊕ β ⊕ γ)
        ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inl val_1)) : α ⊕ β ⊕ γ) ↔
      LE.le (α := (α ⊕ β) ⊕ γ) (Sum.inr val) (inl (inl val_1))
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inr val) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    Sum.inr val ≤ b
have inr₁ : ∀ (val_1 : β),
  LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inr val) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (Sum.inr val_1)) : α ⊕ β ⊕ γ) ↔
    LE.le (α := (α ⊕ β) ⊕ γ) (Sum.inr val) (inl (Sum.inr val_1))
Tactic: rcases b with ((_ | _) | _)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : 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 γ_1
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a : α_1
b_1 : β_1
c : γ_1
α : Type u_10
β : Type u_11
γ : Type u_12
inst_9 : LE α
inst_10 : LE β
inst_11 : LE γ
b : (α ⊕ β) ⊕ γ
val : γ
inr :
  ∀ (val_1 : α),
    LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inr val) : α ⊕ β ⊕ γ)
        ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inl val_1)) : α ⊕ β ⊕ γ) ↔
      LE.le (α := (α ⊕ β) ⊕ γ) (Sum.inr val) (inl (inl val_1))
inr₁ :
  ∀ (val_1 : β),
    LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inr val) : α ⊕ β ⊕ γ)
        ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (Sum.inr val_1)) : α ⊕ β ⊕ γ) ↔
      LE.le (α := (α ⊕ β) ⊕ γ) (Sum.inr val) (inl (Sum.inr val_1))
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inr val) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    Sum.inr val ≤ b
have inr₂ : ∀ (val_1 : γ),
  LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inr val) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inr val_1) : α ⊕ β ⊕ γ) ↔
    LE.le (α := (α ⊕ β) ⊕ γ) (Sum.inr val) (Sum.inr val_1)
Tactic: rcases b with ((_ | _) | _)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
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 (α := Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (inl a) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (inl b) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) ↔
    LE.le (α := (α ⊕ β)ᵒᵈ) (inl a) (inl b)
have inl : LE.le (α := Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) (inl ((toDual : (a : α) → αᵒᵈ) a) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
    (inl ((toDual : (a : α) → αᵒᵈ) b) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) ↔
  LE.le (α := (α ⊕ β)ᵒᵈ) ((toDual : (a : α ⊕ β) → (α ⊕ β)ᵒᵈ) (inl a) : (α ⊕ β)ᵒᵈ)
    ((toDual : (a : α ⊕ β) → (α ⊕ β)ᵒᵈ) (inl b) : (α ⊕ β)ᵒᵈ)
Tactic: change inl (toDual a) ≤ inl (toDual b) ↔ toDual (inl a) ≤ toDual (inl b)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
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 (α := Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (inr a) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (inr b) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) ↔
    LE.le (α := (α ⊕ β)ᵒᵈ) (inr a) (inr b)
have inr : LE.le (α := Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) (inr ((toDual : (a : β) → βᵒᵈ) a) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
    (inr ((toDual : (a : β) → βᵒᵈ) b) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) ↔
  LE.le (α := (α ⊕ β)ᵒᵈ) ((toDual : (a : α ⊕ β) → (α ⊕ β)ᵒᵈ) (inr a) : (α ⊕ β)ᵒᵈ)
    ((toDual : (a : α ⊕ β) → (α ⊕ β)ᵒᵈ) (inr b) : (α ⊕ β)ᵒᵈ)
Tactic: change inr (toDual a) ≤ inr (toDual b) ↔ toDual (inr a) ≤ toDual (inr b)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
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 γ₂
⊢ (e₁.sumLexCongr e₂).trans (f₁.sumLexCongr f₂) = (e₁.trans f₁).sumLexCongr (e₂.trans f₂)
have 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 (γ₁ ⊕ γ₂))
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
⊢ Eq (α := _root_.Lex (α ⊕ β) ≃o _root_.Lex (α ⊕ β)) (sumLexCongr (refl α) (refl β)) (refl (_root_.Lex (α ⊕ β)))
have 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 (α ⊕ β))
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
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 (α ⊕ β))ᵒᵈ
⊢ 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
have inl : ∀ (a : α),
  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 (βᵒᵈ ⊕ αᵒᵈ)) b :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    inl a ≤ b
Tactic: rcases a with (a | a)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
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
⊢ 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
have inr : ∀ (a : β),
  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 (βᵒᵈ ⊕ αᵒᵈ)) b :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    inr a ≤ b
Tactic: rcases a with (a | a)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
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 : α
⊢ 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 (βᵒᵈ ⊕ αᵒᵈ)) b :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    inl a ≤ b
have inl : ∀ (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 (βᵒᵈ ⊕ αᵒᵈ)) (inl b) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    LE.le (α := (_root_.Lex (α ⊕ β))ᵒᵈ) (inl a) (inl b)
Tactic: rcases b with (b | b)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
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)
⊢ 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
have 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
Tactic: rcases b with (b | b)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
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 : β
⊢ 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 (βᵒᵈ ⊕ αᵒᵈ)) b :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    inr a ≤ b
have inr : ∀ (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: rcases b with (b | b)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
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
⊢ 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
have 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)
Tactic: rcases b with (b | b)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
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 (βᵒᵈ ⊕ αᵒᵈ)) (inl b) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    LE.le (α := (_root_.Lex (α ⊕ β))ᵒᵈ) (inl a) (inl b)
have 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 (α ⊕ β)) (inl a)) :
      (_root_.Lex (α ⊕ β))ᵒᵈ)
    ((toDual : (a : _root_.Lex (α ⊕ β)) → (_root_.Lex (α ⊕ β))ᵒᵈ) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl b)) :
      (_root_.Lex (α ⊕ β))ᵒᵈ)
Tactic: change
          toLex (inr <| toDual a) ≤ toLex (inr <| toDual b) ↔
            toDual (toLex <| inl a) ≤ toDual (toLex <| inl b)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
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 (βᵒᵈ ⊕ αᵒᵈ)) (inr b) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    LE.le (α := (_root_.Lex (α ⊕ β))ᵒᵈ) (inr a) (inr b)
have 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 (α ⊕ β)) (inr a)) :
      (_root_.Lex (α ⊕ β))ᵒᵈ)
    ((toDual : (a : _root_.Lex (α ⊕ β)) → (_root_.Lex (α ⊕ β))ᵒᵈ) ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inr b)) :
      (_root_.Lex (α ⊕ β))ᵒᵈ)
Tactic: change
          toLex (inl <| toDual a) ≤ toLex (inl <| toDual b) ↔
            toDual (toLex <| inr a) ≤ toDual (toLex <| inr b)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a b : WithBot α
⊢ LE.le (α := _root_.Lex (PUnit ⊕ α))
      (((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex) :
            (a : WithBot α) → _root_.Lex (PUnit ⊕ α))
          a :
        _root_.Lex (PUnit ⊕ α))
      (((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex) :
            (a : WithBot α) → _root_.Lex (PUnit ⊕ α))
          b :
        _root_.Lex (PUnit ⊕ α)) ↔
    a ≤ b
have simp : Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
    (Sum.elim inr inl
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) a, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y))
    (Sum.elim inr inl
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)) ↔
  a ≤ b
Tactic: simp only [Equiv.optionEquivSumPUnit, Option.elim, Equiv.trans_apply, Equiv.coe_fn_mk,
      Equiv.sumComm_apply, swap, Lex.toLex_le_toLex, le_refl]
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a b : WithBot α
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) a, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    a ≤ b
have bot : Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
    (Sum.elim inr inl
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y))
    (Sum.elim inr inl
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)) ↔
  ⊥ ≤ b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a b : WithBot α
bot :
  Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ b
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) a, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    a ≤ b
have coe : ∀ (a : α),
  Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    (↑a : WithBot α) ≤ b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
b : WithBot α
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ b
have bot : Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
    (Sum.elim inr inl
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y))
    (Sum.elim inr inl
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)) ↔
  LE.le.{u_1} (α := WithBot α) ⊥ ⊥
Tactic: cases b
Cleared hypotheses: b