awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α₁ ⊕ α₂
⊢ Eq (α := γ₁ ⊕ γ₂) (((e₁.sumCongr e₂).trans (f₁.sumCongr f₂) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) x : γ₁ ⊕ γ₂)
    (((e₁.trans f₁).sumCongr (e₂.trans f₂) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) x : γ₁ ⊕ γ₂)

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.sumCongr eb).symm = ea.symm.sumCongr eb.symm

Tactic:
rfl

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

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

Tactic:
simp
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_10
β : Type u_11
inst : LE α
inst_1 : LE β
⊢ Eq (α := β ⊕ α ≃o α ⊕ β) (symm (sumComm α β)) (sumComm β α)

Tactic:
rfl

Premises used: Sum.swap, OrderIso.sumComm, Equiv.sumComm, RelIso.symm, OrderIso.symm, Equiv.symm, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
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 : α_1
b_1 : β_1
c : γ_1
α : Type u_10
β : Type u_11
γ : Type u_12
inst_9 : LE α
inst_10 : LE β
inst_11 : LE γ
a b : (α ⊕ β) ⊕ γ
inl :
  ∀ (val : α),
    LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (Sum.inl val)) : α ⊕ β ⊕ γ)
        ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
      Sum.inl (Sum.inl val) ≤ b
inl₁ :
  ∀ (val : β),
    LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (Sum.inr val)) : α ⊕ β ⊕ γ)
        ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
      Sum.inl (Sum.inr val) ≤ b
inr :
  ∀ (val : γ),
    LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inr val) : α ⊕ β ⊕ γ)
        ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
      Sum.inr val ≤ b
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) a : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    a ≤ b

Tactic:
rcases a with ((_ | _) | _)
-- Module: Mathlib.Data.Sum.Order
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 : α
inl :
  ∀ (val_1 : α),
    LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (Sum.inl val)) : α ⊕ β ⊕ γ)
        ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (Sum.inl val_1)) : α ⊕ β ⊕ γ) ↔
      LE.le (α := (α ⊕ β) ⊕ γ) (Sum.inl (Sum.inl val)) (Sum.inl (Sum.inl val_1))
inl₁ :
  ∀ (val_1 : β),
    LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (Sum.inl val)) : α ⊕ β ⊕ γ)
        ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (inr val_1)) : α ⊕ β ⊕ γ) ↔
      LE.le (α := (α ⊕ β) ⊕ γ) (Sum.inl (Sum.inl val)) (Sum.inl (inr val_1))
inl₂ :
  ∀ (val_1 : γ),
    LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (Sum.inl val)) : α ⊕ β ⊕ γ)
        ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inr val_1) : α ⊕ β ⊕ γ) ↔
      LE.le (α := (α ⊕ β) ⊕ γ) (Sum.inl (Sum.inl val)) (inr val_1)
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (Sum.inl val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    Sum.inl (Sum.inl val) ≤ b

Tactic:
rcases b with ((_ | _) | _)
-- Module: Mathlib.Data.Sum.Order
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 : β
inl :
  ∀ (val_1 : α),
    LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (inr val)) : α ⊕ β ⊕ γ)
        ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (Sum.inl val_1)) : α ⊕ β ⊕ γ) ↔
      LE.le (α := (α ⊕ β) ⊕ γ) (Sum.inl (inr val)) (Sum.inl (Sum.inl val_1))
inl₁ :
  ∀ (val_1 : β),
    LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (inr val)) : α ⊕ β ⊕ γ)
        ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (inr val_1)) : α ⊕ β ⊕ γ) ↔
      LE.le (α := (α ⊕ β) ⊕ γ) (Sum.inl (inr val)) (Sum.inl (inr val_1))
inl₂ :
  ∀ (val_1 : γ),
    LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (inr val)) : α ⊕ β ⊕ γ)
        ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inr val_1) : α ⊕ β ⊕ γ) ↔
      LE.le (α := (α ⊕ β) ⊕ γ) (Sum.inl (inr val)) (inr val_1)
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (inr val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    Sum.inl (inr val) ≤ b

Tactic:
rcases b with ((_ | _) | _)
-- Module: Mathlib.Data.Sum.Order
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))
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)
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inr val) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    Sum.inr val ≤ b

Tactic:
rcases b with ((_ | _) | _)
-- Module: Mathlib.Data.Sum.Order
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
c : γ_1
α : Type u_10
β : Type u_11
γ : Type u_12
inst_9 : LE α
inst_10 : LE β
inst_11 : LE γ
val val_1 : α
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inl val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inl val_1)) : α ⊕ β ⊕ γ) ↔
    LE.le (α := (α ⊕ β) ⊕ γ) (inl (inl val)) (inl (inl val_1))

Tactic:
simp [Equiv.sumAssoc]

Premises used: Equiv.sumAssoc
-- Module: Mathlib.Data.Sum.Order
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
c : γ_1
α : Type u_10
β : Type u_11
γ : Type u_12
inst_9 : LE α
inst_10 : LE β
inst_11 : LE γ
val : α
val_1 : β
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inl val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inr val_1)) : α ⊕ β ⊕ γ) ↔
    LE.le (α := (α ⊕ β) ⊕ γ) (inl (inl val)) (inl (inr val_1))

Tactic:
simp [Equiv.sumAssoc]

Premises used: Equiv.sumAssoc
-- Module: Mathlib.Data.Sum.Order
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
c : γ_1
α : Type u_10
β : Type u_11
γ : Type u_12
inst_9 : LE α
inst_10 : LE β
inst_11 : LE γ
val : α
val_1 : γ
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inl val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inr val_1) : α ⊕ β ⊕ γ) ↔
    LE.le (α := (α ⊕ β) ⊕ γ) (inl (inl val)) (inr val_1)

Tactic:
simp [Equiv.sumAssoc]

Premises used: Equiv.sumAssoc
-- Module: Mathlib.Data.Sum.Order
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
c : γ_1
α : Type u_10
β : Type u_11
γ : Type u_12
inst_9 : LE α
inst_10 : LE β
inst_11 : LE γ
val : β
val_1 : α
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inr val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inl val_1)) : α ⊕ β ⊕ γ) ↔
    LE.le (α := (α ⊕ β) ⊕ γ) (inl (inr val)) (inl (inl val_1))

Tactic:
simp [Equiv.sumAssoc]

Premises used: Equiv.sumAssoc
-- Module: Mathlib.Data.Sum.Order
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
c : γ_1
α : Type u_10
β : Type u_11
γ : Type u_12
inst_9 : LE α
inst_10 : LE β
inst_11 : LE γ
val val_1 : β
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inr val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inr val_1)) : α ⊕ β ⊕ γ) ↔
    LE.le (α := (α ⊕ β) ⊕ γ) (inl (inr val)) (inl (inr val_1))

Tactic:
simp [Equiv.sumAssoc]

Premises used: Equiv.sumAssoc
-- Module: Mathlib.Data.Sum.Order
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
c : γ_1
α : Type u_10
β : Type u_11
γ : Type u_12
inst_9 : LE α
inst_10 : LE β
inst_11 : LE γ
val : β
val_1 : γ
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inr val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inr val_1) : α ⊕ β ⊕ γ) ↔
    LE.le (α := (α ⊕ β) ⊕ γ) (inl (inr val)) (inr val_1)

Tactic:
simp [Equiv.sumAssoc]

Premises used: Equiv.sumAssoc
-- Module: Mathlib.Data.Sum.Order
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
c : γ_1
α : Type u_10
β : Type u_11
γ : Type u_12
inst_9 : LE α
inst_10 : LE β
inst_11 : LE γ
val : γ
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:
simp [Equiv.sumAssoc]

Premises used: Equiv.sumAssoc
-- Module: Mathlib.Data.Sum.Order
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
c : γ_1
α : Type u_10
β : Type u_11
γ : Type u_12
inst_9 : LE α
inst_10 : LE β
inst_11 : LE γ
val : γ
val_1 : β
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inr val) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inr val_1)) : α ⊕ β ⊕ γ) ↔
    LE.le (α := (α ⊕ β) ⊕ γ) (inr val) (inl (inr val_1))

Tactic:
simp [Equiv.sumAssoc]

Premises used: Equiv.sumAssoc
-- Module: Mathlib.Data.Sum.Order
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
c : γ_1
α : Type u_10
β : Type u_11
γ : Type u_12
inst_9 : LE α
inst_10 : LE β
inst_11 : LE γ
val val_1 : γ
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inr val) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inr val_1) : α ⊕ β ⊕ γ) ↔
    LE.le (α := (α ⊕ β) ⊕ γ) (inr val) (inr val_1)

Tactic:
simp [Equiv.sumAssoc]

Premises used: Equiv.sumAssoc
-- 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 (α := α ⊕ β ⊕ γ) ((sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inl a)) : α ⊕ β ⊕ γ) (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 (α := α ⊕ β ⊕ γ) ((sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inr b)) : α ⊕ β ⊕ γ)
    (inr (inl 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 (α := α ⊕ β ⊕ γ) ((sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inr c) : α ⊕ β ⊕ γ) (inr (inr c) : α ⊕ β ⊕ γ)

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 γ
a : α
⊢ Eq (α := (α ⊕ β) ⊕ γ) ((symm (sumAssoc α β γ) : (a : α ⊕ β ⊕ γ) → (α ⊕ β) ⊕ γ) (inl a) : (α ⊕ β) ⊕ γ)
    (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 (α := (α ⊕ β) ⊕ γ) ((symm (sumAssoc α β γ) : (a : α ⊕ β ⊕ γ) → (α ⊕ β) ⊕ γ) (inr (inl b)) : (α ⊕ β) ⊕ γ)
    (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 (α := (α ⊕ β) ⊕ γ) ((symm (sumAssoc α β γ) : (a : α ⊕ β ⊕ γ) → (α ⊕ β) ⊕ γ) (inr (inr c)) : (α ⊕ β) ⊕ γ)
    (inr c : (α ⊕ β) ⊕ γ)

Tactic:
rfl

Premises used: 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 : α
inl :
  LE.le (α := Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) (Sum.inl ((toDual : (a : α) → αᵒᵈ) a) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      (Sum.inl ((toDual : (a : α) → αᵒᵈ) b) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) ↔
    LE.le (α := (α ⊕ β)ᵒᵈ) ((toDual : (a : α ⊕ β) → (α ⊕ β)ᵒᵈ) (Sum.inl a) : (α ⊕ β)ᵒᵈ)
      ((toDual : (a : α ⊕ β) → (α ⊕ β)ᵒᵈ) (Sum.inl b) : (α ⊕ β)ᵒᵈ)
⊢ LE.le (α := Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (Sum.inl a) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (Sum.inl b) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) ↔
    LE.le (α := (α ⊕ β)ᵒᵈ) (Sum.inl a) (Sum.inl b)

Tactic:
change inl (toDual a) ≤ inl (toDual b) ↔ toDual (inl a) ≤ toDual (inl b)

Premises used: OrderDual.toDual, Sum.inl, DFunLike.coe
-- 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 (α := 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:
simp [toDual_le_toDual, inl_le_inl_iff]

Premises used: OrderDual.toDual_le_toDual, Sum.inl_le_inl_iff
-- 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 (α := Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (inl a) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (inr b) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) ↔
    inl a ≤ inr b

Tactic:
iff_of_false (@not_inl_le_inr (OrderDual β) (OrderDual α) _ _ _ _) not_inr_le_inl

Premises used: iff_of_false, Sum.not_inr_le_inl, Sum.not_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 (α := Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (inl a) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (inr b) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) ↔
    inl a ≤ inr b

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

Premises used: iff_of_false, Sum.not_inr_le_inl, Sum.not_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 (α := Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (inr a) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (inl b) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) ↔
    inr a ≤ inl b

Tactic:
iff_of_false (@not_inr_le_inl (OrderDual α) (OrderDual β) _ _ _ _) not_inl_le_inr

Premises used: iff_of_false, Sum.not_inr_le_inl, Sum.not_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 (α := Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (inr a) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (inl b) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) ↔
    inr a ≤ inl b

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

Premises used: iff_of_false, Sum.not_inr_le_inl, Sum.not_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 (α := Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) (Sum.inr ((toDual : (a : β) → βᵒᵈ) a) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      (Sum.inr ((toDual : (a : β) → βᵒᵈ) b) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) ↔
    LE.le (α := (α ⊕ β)ᵒᵈ) ((toDual : (a : α ⊕ β) → (α ⊕ β)ᵒᵈ) (Sum.inr a) : (α ⊕ β)ᵒᵈ)
      ((toDual : (a : α ⊕ β) → (α ⊕ β)ᵒᵈ) (Sum.inr b) : (α ⊕ β)ᵒᵈ)
⊢ LE.le (α := Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (Sum.inr a) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ)
      ((Equiv.refl (α ⊕ β)ᵒᵈ : (a : (α ⊕ β)ᵒᵈ) → αᵒᵈ ⊕ βᵒᵈ) (Sum.inr b) : Sum.{u_10, u_11} αᵒᵈ βᵒᵈ) ↔
    LE.le (α := (α ⊕ β)ᵒᵈ) (Sum.inr a) (Sum.inr b)

Tactic:
change inr (toDual a) ≤ inr (toDual b) ↔ toDual (inr a) ≤ toDual (inr b)

Premises used: OrderDual.toDual, Sum.inr, DFunLike.coe
-- 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 (α := 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:
simp [toDual_le_toDual, inr_le_inr_iff]

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

Tactic:
rfl

Premises used: OrderDual, rfl