awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x_1 y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
x y z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) x y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) x z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
have coe : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a : WithTop α) y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
y z : WithTop α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
have top : (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
    ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
y z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
have top₁ : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a : WithTop α) z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
y z : WithTop α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
have coe : (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
    ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
y z : WithTop α
a_1 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) y)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
have coe₁ : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a : WithTop α) z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
z : WithTop α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
have top : (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
    ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
have top₁ : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α)) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ (↑a : WithTop α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
z : WithTop α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) z
have top : (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
    ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
z : WithTop α
a_1 : α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) ⊤
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) z
have top₁ : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α)) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) (↑a : WithTop α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
z : WithTop α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
have coe : (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
    ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
z : WithTop α
a_1 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
have coe₁ : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a : WithTop α)) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ (↑a : WithTop α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
z : WithTop α
a_1 a_2 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) z
have coe : (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α))
    ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
z : WithTop α
a_1 a_2 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) ⊤
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) z
have coe₁ : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a : WithTop α)) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) (↑a : WithTop α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddLeftReflectLT α
a_1 a_2 a_3 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2) ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α))
      ((fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) (↑a_3 : WithTop α)) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) (↑a_3 : WithTop α)
have coe : a_1 + a_2 < a_1 + a_3 → a_2 < a_3
Tactic: simp [← coe_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x_1 y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
x y z : WithTop α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) x y)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) x z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
have top : (fun (x1 x2 : WithTop α) ↦ x1 < x2)
    (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
    (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x_1 y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
x y z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) x y)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) x z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
have coe : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a : WithTop α) y)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
y z : WithTop α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
have top : (fun (x1 x2 : WithTop α) ↦ x1 < x2)
    (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
    (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
y z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ y)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
have top₁ : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α))
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a : WithTop α) z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
y z : WithTop α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) y)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
have coe : (fun (x1 x2 : WithTop α) ↦ x1 < x2)
    (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
    (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y_1 z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
y z : WithTop α
a_1 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) y)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) y z
have coe₁ : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
        (↑a : WithTop α))
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a : WithTop α) z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithTop α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
have top : (fun (x1 x2 : WithTop α) ↦ x1 < x2)
    (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
    (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithTop α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
have top₁ : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤)
      (swap (φ := fun (a a_1 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α)) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ (↑a : WithTop α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithTop α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) z
have top : (fun (x1 x2 : WithTop α) ↦ x1 < x2)
    (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
    (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithTop α
a_1 : α
top :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) ⊤
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) z
have top₁ : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a_1 : WithTop α))
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) ⊤ (↑a : WithTop α)) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_1 : WithTop α) (↑a : WithTop α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithTop α
a_1 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
have coe : (fun (x1 x2 : WithTop α) ↦ x1 < x2)
    (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
    (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithTop α
a_1 : α
coe :
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ ⊤
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ z
have coe₁ : ∀ (a : α),
  (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤)
      (swap (φ := fun (a a_2 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
        (↑a : WithTop α)) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) ⊤ (↑a : WithTop α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
w x y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithTop α
a_1 a_2 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
        (↑a_2 : WithTop α))
      (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) z) →
    (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) z
have coe : (fun (x1 x2 : WithTop α) ↦ x1 < x2)
    (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
      (↑a_2 : WithTop α))
    (swap (φ := fun (a a_3 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α) ⊤) →
  (fun (x1 x2 : WithTop α) ↦ x1 < x2) (↑a_2 : WithTop α) ⊤
Tactic: cases z
Cleared hypotheses: z