Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl
α : 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✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a✝ : α
b✝ : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a b : α₁
⊢ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inl a)) ≤
      (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inl b)) ↔
    toLex (inl a) ≤ toLex (inl b)

pp: case inl.inr
α : 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✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a✝ : α
b✝ : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a : α₁
b : β₁
⊢ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inl a)) ≤
      (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inr b)) ↔
    toLex (inl a) ≤ toLex (inr b)

pp: case inr.inl
α : 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✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a✝ : α
b✝ : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a : β₁
b : α₁
⊢ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inr a)) ≤
      (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inl b)) ↔
    toLex (inr a) ≤ toLex (inl b)

pp: case inr.inr
α : 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✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a✝ : α
b✝ : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a b : β₁
⊢ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inr a)) ≤
      (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inr b)) ↔
    toLex (inr a) ≤ toLex (inr b)

Tactic:
<;>

Goal state after:
case inl.inl
α : 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✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a✝ : α
b✝ : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a b : α₁
⊢ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inl a)) ≤
      (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inl b)) ↔
    toLex (inl a) ≤ toLex (inl b)

case inl.inr
α : 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✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a✝ : α
b✝ : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a : α₁
b : β₁
⊢ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inl a)) ≤
      (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inr b)) ↔
    toLex (inl a) ≤ toLex (inr b)

case inr.inl
α : 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✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a✝ : α
b✝ : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a : β₁
b : α₁
⊢ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inr a)) ≤
      (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inl b)) ↔
    toLex (inr a) ≤ toLex (inl b)

case inr.inr
α : 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✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a✝ : α
b✝ : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
a b : β₁
⊢ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inr a)) ≤
      (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex (inr b)) ↔
    toLex (inr a) ≤ toLex (inr b)