awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Icc (inlₗ a₁) (inlₗ a₂))
    (map (Embedding.trans Embedding.inl (Equiv.toEmbedding toLex)) (Icc a₁ a₂))
have rw : Eq (α := Finset (_root_.Lex (α ⊕ β))) (Icc (inlₗ a₁) (inlₗ a₂))
  (map (Equiv.toEmbedding toLex) (map Embedding.inl (Icc a₁ a₂)))
Tactic: rw [← Finset.map_map]
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ico (inlₗ a₁) (inlₗ a₂))
    (map (Embedding.trans Embedding.inl (Equiv.toEmbedding toLex)) (Ico a₁ a₂))
have rw : Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ico (inlₗ a₁) (inlₗ a₂))
  (map (Equiv.toEmbedding toLex) (map Embedding.inl (Ico a₁ a₂)))
Tactic: rw [← Finset.map_map]
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioc (inlₗ a₁) (inlₗ a₂))
    (map (Embedding.trans Embedding.inl (Equiv.toEmbedding toLex)) (Ioc a₁ a₂))
have rw : Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioc (inlₗ a₁) (inlₗ a₂))
  (map (Equiv.toEmbedding toLex) (map Embedding.inl (Ioc a₁ a₂)))
Tactic: rw [← Finset.map_map]
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
a₁ a₂ : α
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioo (inlₗ a₁) (inlₗ a₂))
    (map (Embedding.trans Embedding.inl (Equiv.toEmbedding toLex)) (Ioo a₁ a₂))
have rw : Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioo (inlₗ a₁) (inlₗ a₂))
  (map (Equiv.toEmbedding toLex) (map Embedding.inl (Ioo a₁ a₂)))
Tactic: rw [← Finset.map_map]
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Icc (inrₗ b₁) (inrₗ b₂))
    (map (Embedding.trans Embedding.inr (Equiv.toEmbedding toLex)) (Icc b₁ b₂))
have rw : Eq (α := Finset (_root_.Lex (α ⊕ β))) (Icc (inrₗ b₁) (inrₗ b₂))
  (map (Equiv.toEmbedding toLex) (map Embedding.inr (Icc b₁ b₂)))
Tactic: rw [← Finset.map_map]
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ico (inrₗ b₁) (inrₗ b₂))
    (map (Embedding.trans Embedding.inr (Equiv.toEmbedding toLex)) (Ico b₁ b₂))
have rw : Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ico (inrₗ b₁) (inrₗ b₂))
  (map (Equiv.toEmbedding toLex) (map Embedding.inr (Ico b₁ b₂)))
Tactic: rw [← Finset.map_map]
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioc (inrₗ b₁) (inrₗ b₂))
    (map (Embedding.trans Embedding.inr (Equiv.toEmbedding toLex)) (Ioc b₁ b₂))
have rw : Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioc (inrₗ b₁) (inrₗ b₂))
  (map (Equiv.toEmbedding toLex) (map Embedding.inr (Ioc b₁ b₂)))
Tactic: rw [← Finset.map_map]
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
inst_4 : LocallyFiniteOrderTop α
inst_5 : LocallyFiniteOrderBot β
b₁ b₂ : β
⊢ Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioo (inrₗ b₁) (inrₗ b₂))
    (map (Embedding.trans Embedding.inr (Equiv.toEmbedding toLex)) (Ioo b₁ b₂))
have rw : Eq (α := Finset (_root_.Lex (α ⊕ β))) (Ioo (inrₗ b₁) (inrₗ b₂))
  (map (Equiv.toEmbedding toLex) (map Embedding.inr (Ioo b₁ b₂)))
Tactic: rw [← Finset.map_map]
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Antisymm r
inst_1 : Std.Antisymm s
a c : α
hab : r a c
hba : r c a
⊢ Eq (α := α ⊕ β) (inl a) (inl c)
have inl : Eq (α := α ⊕ β) (inl c) (inl c)
Tactic: rw [antisymm hab hba]
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Antisymm r
inst_1 : Std.Antisymm s
b d : β
hab : s b d
hba : s d b
⊢ Eq (α := α ⊕ β) (inr b) (inr d)
have inr : Eq (α := α ⊕ β) (inr d) (inr d)
Tactic: rw [antisymm hab hba]
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Antisymm r
inst_1 : Std.Antisymm s
a₁ a₂ : α
hab : r a₁ a₂
hba : r a₂ a₁
⊢ Eq (α := α ⊕ β) (inl a₁) (inl a₂)
have inl : Eq (α := α ⊕ β) (inl a₂) (inl a₂)
Tactic: rw [antisymm hab hba]
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst : Std.Antisymm r
inst_1 : Std.Antisymm s
b₁ b₂ : β
hab : s b₁ b₂
hba : s b₂ b₁
⊢ Eq (α := α ⊕ β) (inr b₁) (inr b₂)
have inr : Eq (α := α ⊕ β) (inr b₂) (inr b₂)
Tactic: rw [antisymm hab hba]
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
a b : α ⊕ β
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
have refine_1 : ∀ (hab : a < b), ¬b ≤ a
Tactic: refine ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
a b : α ⊕ β
refine_1 : ∀ (hab : a < b), ¬b ≤ a
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
have refine_2 : a ≤ b ∧ ¬b ≤ a → a < b
Tactic: refine ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h : NoMinOrder (α ⊕ β)
a : α
⊢ ∃ (b : α), b < a
have inl : ∀ (b : α) (h : LT.lt (α := α ⊕ β) (inl b) (inl a)), ∃ (b : α), b < a
Tactic: obtain ⟨b | b, h⟩ := exists_lt (inl a : α ⊕ β)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h : NoMinOrder (α ⊕ β)
a : α
inl : ∀ (b : α) (h : LT.lt (α := α ⊕ β) (Sum.inl b) (Sum.inl a)), ∃ (b : α), b < a
⊢ ∃ (b : α), b < a
have inr : ∀ (b : β) (h : inr b < Sum.inl a), ∃ (b : α), b < a
Tactic: obtain ⟨b | b, h⟩ := exists_lt (inl a : α ⊕ β)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h : NoMinOrder (α ⊕ β)
a : β
⊢ ∃ (b : β), b < a
have inl : ∀ (b : α) (h : inl b < inr a), ∃ (b : β), b < a
Tactic: obtain ⟨b | b, h⟩ := exists_lt (inr a : α ⊕ β)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h : NoMinOrder (α ⊕ β)
a : β
inl : ∀ (b : α) (h : Sum.inl b < inr a), ∃ (b : β), b < a
⊢ ∃ (b : β), b < a
have inr : ∀ (b : β) (h : LT.lt (α := α ⊕ β) (inr b) (inr a)), ∃ (b : β), b < a
Tactic: obtain ⟨b | b, h⟩ := exists_lt (inr a : α ⊕ β)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h : NoMaxOrder (α ⊕ β)
a : α
⊢ ∃ (b : α), a < b
have inl : ∀ (b : α) (h : LT.lt (α := α ⊕ β) (inl a) (inl b)), ∃ (b : α), a < b
Tactic: obtain ⟨b | b, h⟩ := exists_gt (inl a : α ⊕ β)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h : NoMaxOrder (α ⊕ β)
a : α
inl : ∀ (b : α) (h : LT.lt (α := α ⊕ β) (Sum.inl a) (Sum.inl b)), ∃ (b : α), a < b
⊢ ∃ (b : α), a < b
have inr : ∀ (b : β) (h : Sum.inl a < inr b), ∃ (b : α), a < b
Tactic: obtain ⟨b | b, h⟩ := exists_gt (inl a : α ⊕ β)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h : NoMaxOrder (α ⊕ β)
a : β
⊢ ∃ (b : β), a < b
have inl : ∀ (b : α) (h : inr a < inl b), ∃ (b : β), a < b
Tactic: obtain ⟨b | b, h⟩ := exists_gt (inr a : α ⊕ β)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h : NoMaxOrder (α ⊕ β)
a : β
inl : ∀ (b : α) (h : inr a < Sum.inl b), ∃ (b : β), a < b
⊢ ∃ (b : β), a < b
have inr : ∀ (b : β) (h : LT.lt (α := α ⊕ β) (inr a) (inr b)), ∃ (b : β), a < b
Tactic: obtain ⟨b | b, h⟩ := exists_gt (inr a : α ⊕ β)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b
have inl : ∀ (c : α) (ha : LT.lt (α := α ⊕ β) (inl a) (inl c)) (hb : LT.lt (α := α ⊕ β) (inl c) (inl b)),
  ∃ (a_1 : α), a < a_1 ∧ a_1 < b
Tactic: obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inl_lt_inl_iff.2 h)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
inl :
  ∀ (c : α) (ha : LT.lt (α := α ⊕ β) (Sum.inl a) (Sum.inl c)) (hb : LT.lt (α := α ⊕ β) (Sum.inl c) (Sum.inl b)),
    ∃ (a_1 : α), a < a_1 ∧ a_1 < b
⊢ ∃ (a_1 : α), a < a_1 ∧ a_1 < b
have inr : ∀ (c : β) (ha : Sum.inl a < inr c) (hb : inr c < Sum.inl b), ∃ (a_1 : α), a < a_1 ∧ a_1 < b
Tactic: obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inl_lt_inl_iff.2 h)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
⊢ ∃ (a_1 : β), a < a_1 ∧ a_1 < b
have inl : ∀ (c : α) (ha : inr a < inl c) (hb : inl c < inr b), ∃ (a_1 : β), a < a_1 ∧ a_1 < b
Tactic: obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inr_lt_inr_iff.2 h)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : LT β
h_1 : DenselyOrdered (α ⊕ β)
a b : β
h : a < b
inl : ∀ (c : α) (ha : inr a < Sum.inl c) (hb : Sum.inl c < inr b), ∃ (a_1 : β), a < a_1 ∧ a_1 < b
⊢ ∃ (a_1 : β), a < a_1 ∧ a_1 < b
have inr : ∀ (c : β) (ha : LT.lt (α := α ⊕ β) (inr a) (inr c)) (hb : LT.lt (α := α ⊕ β) (inr c) (inr b)),
  ∃ (a_1 : β), a < a_1 ∧ a_1 < b
Tactic: obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inr_lt_inr_iff.2 h)
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
a b : _root_.Lex (α ⊕ β)
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
have refine_1 : ∀ (hab : a < b), ¬b ≤ a
Tactic: refine ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
a b : _root_.Lex (α ⊕ β)
refine_1 : ∀ (hab : a < b), ¬b ≤ a
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
have refine_2 : a ≤ b ∧ ¬b ≤ a → a < b
Tactic: refine ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, ?_⟩, ?_⟩
-- 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₁.sumCongr e₂).trans (f₁.sumCongr f₂) = (e₁.trans f₁).sumCongr (e₂.trans f₂)
have h : ∀ (x : α₁ ⊕ α₂),
  Eq (α := γ₁ ⊕ γ₂) (((e₁.sumCongr e₂).trans (f₁.sumCongr f₂) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) x : γ₁ ⊕ γ₂)
    (((e₁.trans f₁).sumCongr (e₂.trans f₂) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) x : γ₁ ⊕ γ₂)
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 (α := α ⊕ β ≃o α ⊕ β) (sumCongr (refl α) (refl β)) (refl (α ⊕ β))
have h : ∀ (x : α ⊕ β),
  Eq (α := α ⊕ β) ((sumCongr (refl α) (refl β) : (a : α ⊕ β) → α ⊕ β) x : α ⊕ β)
    ((refl (α ⊕ β) : (a : α ⊕ β) → α ⊕ β) x : α ⊕ β)
Tactic: ext
-- 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 : α_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 : (α ⊕ β) ⊕ γ
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) a : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    a ≤ b
have inl : ∀ (val : α),
  LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inl val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    inl (inl val) ≤ b
Tactic: rcases a with ((_ | _) | _)
Cleared hypotheses: a
-- 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 : α_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
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) a : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    a ≤ b
have inl₁ : ∀ (val : β),
  LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (inr val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    Sum.inl (inr val) ≤ b
Tactic: rcases a with ((_ | _) | _)
Cleared hypotheses: a
-- 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 : α_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 (inr val)) : α ⊕ β ⊕ γ)
        ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
      Sum.inl (inr val) ≤ b
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) a : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    a ≤ b
have inr : ∀ (val : γ),
  LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inr val) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    inr val ≤ b
Tactic: rcases a with ((_ | _) | _)
Cleared hypotheses: a
-- 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 : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inl val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    inl (inl val) ≤ b
have inl : ∀ (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: 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 : α
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))
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (Sum.inl val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    Sum.inl (Sum.inl val) ≤ b
have 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))
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 : α
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))
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (Sum.inl val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    Sum.inl (Sum.inl val) ≤ b
have 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)
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 : β
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (inl (inr val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    inl (inr val) ≤ b
have inl : ∀ (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: 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 : β
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))
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (inr val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    Sum.inl (inr val) ≤ b
have 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))
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 : β
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))
⊢ LE.le (α := α ⊕ β ⊕ γ) ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) (Sum.inl (inr val)) : α ⊕ β ⊕ γ)
      ((Equiv.sumAssoc α β γ : (a : (α ⊕ β) ⊕ γ) → α ⊕ β ⊕ γ) b : α ⊕ β ⊕ γ) ↔
    Sum.inl (inr val) ≤ b
have 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)
Tactic: rcases b with ((_ | _) | _)
Cleared hypotheses: b