mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_1.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b₁✝ b₂✝ : β
hba : b₁✝ ≤ b₂✝
hab : inr b₂✝ < inr b₁✝
⊢ False

pp: case refine_1.sep
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b : α
a : β
hab : inr a < inl b
⊢ False

Tactic:
·

Goal state after:
case refine_1.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b₁✝ b₂✝ : β
hba : b₁✝ ≤ b₂✝
hab : inr b₂✝ < inr b₁✝
⊢ False
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_1.sep
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b : α
a : β
hab : inr a < inl b
⊢ False

Tactic:
·

Goal state after:
case refine_1.sep
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b : α
a : β
hab : inr a < inl b
⊢ False
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ₗ β
⊢ a ≤ b ∧ ¬b ≤ a → a < b

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ₗ β
⊢ a ≤ b ∧ ¬b ≤ a → a < b
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_2.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁✝ a₂✝ : α
hab : a₁✝ ≤ a₂✝
hba : ¬inl a₂✝ ≤ inl a₁✝
⊢ inl a₁✝ < inl a₂✝

pp: case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b₁✝ b₂✝ : β
hab : b₁✝ ≤ b₂✝
hba : ¬inr b₂✝ ≤ inr b₁✝
⊢ inr b₁✝ < inr b₂✝

pp: case refine_2.sep
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
hba : ¬inr b ≤ inl a
⊢ inl a < inr b

Tactic:
·

Goal state after:
case refine_2.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁✝ a₂✝ : α
hab : a₁✝ ≤ a₂✝
hba : ¬inl a₂✝ ≤ inl a₁✝
⊢ inl a₁✝ < inl a₂✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b₁✝ b₂✝ : β
hab : b₁✝ ≤ b₂✝
hba : ¬inr b₂✝ ≤ inr b₁✝
⊢ inr b₁✝ < inr b₂✝

pp: case refine_2.sep
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
hba : ¬inr b ≤ inl a
⊢ inl a < inr b

Tactic:
·

Goal state after:
case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b₁✝ b₂✝ : β
hab : b₁✝ ≤ b₂✝
hba : ¬inr b₂✝ ≤ inr b₁✝
⊢ inr b₁✝ < inr b₂✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_2.sep
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
hba : ¬inr b ≤ inl a
⊢ inl a < inr b

Tactic:
·

Goal state after:
case refine_2.sep
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
hba : ¬inr b ≤ inl a
⊢ inl a < inr b
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
a : α
⊢ inl ⊥ ≤ inl a

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
b : β
⊢ inl ⊥ ≤ inr b

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
a : α
⊢ inl ⊥ ≤ inl a
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
b : β
⊢ inl ⊥ ≤ inr b

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
b : β
⊢ inl ⊥ ≤ inr b
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
a : α
⊢ inl a ≤ inr ⊤

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
b : β
⊢ inr b ≤ inr ⊤

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
a : α
⊢ inl a ≤ inr ⊤
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hmin : IsMin (sSup s)
⊢ sSup s ∈ s

pp: case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s

Tactic:
·

Goal state after:
case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hmin : IsMin (sSup s)
⊢ sSup s ∈ s
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s

Tactic:
·

Goal state after:
case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
hlim : ¬IsSuccPrelimit (sSup ∅)
⊢ sSup ∅ ∈ ∅

pp: case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
hs : s.Nonempty
⊢ sSup s ∈ s

Tactic:
·

Goal state after:
case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
hlim : ¬IsSuccPrelimit (sSup ∅)
⊢ sSup ∅ ∈ ∅
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
hs : s.Nonempty
⊢ sSup s ∈ s

Tactic:
·

Goal state after:
case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
hs : s.Nonempty
⊢ sSup s ∈ s
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
b : β
⊢ inr b ≤ inr ⊤

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
b : β
⊢ inr b ≤ inr ⊤
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
h : IsSuccPrelimit ⊥
⊢ sSup (Iio ⊥) = ⊥

pp: case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
hx : ⊥ < x
⊢ sSup (Iio x) = x

Tactic:
·

Goal state after:
case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
h : IsSuccPrelimit ⊥
⊢ sSup (Iio ⊥) = ⊥
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
hx : ⊥ < x
⊢ sSup (Iio x) = x

Tactic:
·

Goal state after:
case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
hx : ⊥ < x
⊢ sSup (Iio x) = x
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
⊢ ⨆ a, succ ↑a ≤ x

pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
y : α
hy : y < x
⊢ y < ⨆ a, succ ↑a

Tactic:
·

Goal state after:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
⊢ ⨆ a, succ ↑a ≤ x
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
y : α
hy : y < x
⊢ y < ⨆ a, succ ↑a

Tactic:
·

Goal state after:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
y : α
hy : y < x
⊢ y < ⨆ a, succ ↑a
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: α : Type u
⊢ lift.{u, u} #α + lift.{u, u} #PUnit = #α + 1

Tactic:
mk_eq_one PUnit,

Goal state after:
α : Type u
⊢ lift.{u, u} #α + lift.{u, u} 1 = #α + 1
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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : α
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl b) ↔ inl a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : α
b : β
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr b) ↔ inl a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : β
b : α
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl b) ↔ inr a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr b) ↔ inr a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : α
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl b) ↔ inl a ≤ inl b
Module: Mathlib.Data.Sum.Order

Goal state before:
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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : α
b : β
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr b) ↔ inl a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : β
b : α
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl b) ↔ inr a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr b) ↔ inr a ≤ inr b

Tactic:
·

Goal state after:
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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : α
b : β
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr b) ↔ inl a ≤ inr b
Module: Mathlib.Data.Sum.Order

Goal state before:
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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : β
b : α
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl b) ↔ inr a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr b) ↔ inr a ≤ inr b

Tactic:
·

Goal state after:
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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : β
b : α
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl b) ↔ inr a ≤ inl b
Module: Mathlib.Data.Sum.Order

Goal state before:
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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr b) ↔ inr a ≤ inr b

Tactic:
·

Goal state after:
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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr b) ↔ inr a ≤ inr b
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
⊢ ∃ a, f a = x

pp: case inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∉ Set.range ⇑f
hs : s y x
⊢ ∃ a, f a = x

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
⊢ ∃ a, f a = x
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
y : β
hy : y ∈ Set.range ⇑f
IH : ∀ (y_1 : β), s y_1 y → ∃ a, f a = y_1
hs : ¬s y y
⊢ ∃ a, f a = y

pp: case inl.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h✝ : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
h : s x y
⊢ ∃ a, f a = x

Tactic:
·

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
y : β
hy : y ∈ Set.range ⇑f
IH : ∀ (y_1 : β), s y_1 y → ∃ a, f a = y_1
hs : ¬s y y
⊢ ∃ a, f a = y
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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : α
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) (inl b) ↔ inl a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : α
b : β
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) (inr b) ↔ inl a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : β
b : α
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inl b) ↔ inr a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inr b) ↔ inr a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : α
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) (inl b) ↔ inl a ≤ inl b
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h✝ : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
h : s x y
⊢ ∃ a, f a = x

Tactic:
·

Goal state after:
case inl.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h✝ : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
h : s x y
⊢ ∃ a, f a = x
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∉ Set.range ⇑f
hs : s y x
⊢ ∃ a, f a = x

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∉ Set.range ⇑f
hs : s y x
⊢ ∃ a, f a = x
Module: Mathlib.Data.Sum.Order

Goal state before:
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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : α
b : β
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) (inr b) ↔ inl a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : β
b : α
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inl b) ↔ inr a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inr b) ↔ inr a ≤ inr b

Tactic:
·

Goal state after:
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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : α
b : β
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) (inr b) ↔ inl a ≤ inr b
Module: Mathlib.Data.Sum.Order

Goal state before:
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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : β
b : α
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inl b) ↔ inr a ≤ 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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inr b) ↔ inr a ≤ inr b

Tactic:
·

Goal state after:
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 : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : β
b : α
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inl b) ↔ inr a ≤ inl b