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 y z_1 : WithTop α
a b : α
inst_1 : LT α
inst_2 : AddRightReflectLT α
z : WithTop α
a_1 a_2 : α
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 α) ⊤
⊢ (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₁ : ∀ (a : α),
  (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 α)
        (↑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 : AddRightReflectLT α
a_1 a_2 a_3 : α
⊢ (fun (x1 x2 : WithTop α) ↦ x1 < x2)
      (swap (φ := fun (a a_4 : WithTop α) ↦ WithTop α) (fun (x1 x2 : WithTop α) ↦ x1 + x2) (↑a_1 : WithTop α)
        (↑a_2 : WithTop α))
      (swap (φ := fun (a a_4 : WithTop α) ↦ 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_2 + a_1 < a_3 + a_1 → a_2 < a_3
Tactic: simp [← coe_add, swap]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
hx : x ≠ ⊤
⊢ x + y ≤ x + z → y ≤ z
have lift : ∀ (x : α), (↑x : WithTop α) + y ≤ (↑x : WithTop α) + z → y ≤ z
Tactic: lift x to α using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y z : WithTop α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x : α
⊢ (↑x : WithTop α) + y ≤ (↑x : WithTop α) + z → y ≤ z
have top : (↑x : WithTop α) + ⊤ ≤ (↑x : WithTop α) + z → ⊤ ≤ z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y z : WithTop α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x : α
top : (↑x : WithTop α) + ⊤ ≤ (↑x : WithTop α) + z → ⊤ ≤ z
⊢ (↑x : WithTop α) + y ≤ (↑x : WithTop α) + z → y ≤ z
have coe : ∀ (a : α), (↑x : WithTop α) + (↑a : WithTop α) ≤ (↑x : WithTop α) + z → (↑a : WithTop α) ≤ z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
z : WithTop α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x : α
⊢ (↑x : WithTop α) + ⊤ ≤ (↑x : WithTop α) + z → ⊤ ≤ z
have top : (↑x : WithTop α) + ⊤ ≤ (↑x : WithTop α) + ⊤ → LE.le.{u} (α := WithTop α) ⊤ ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
z : WithTop α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x : α
top : (↑x : WithTop α) + ⊤ ≤ (↑x : WithTop α) + ⊤ → LE.le.{u} (α := WithTop α) ⊤ ⊤
⊢ (↑x : WithTop α) + ⊤ ≤ (↑x : WithTop α) + z → ⊤ ≤ z
have top₁ : ∀ (a : α), (↑x : WithTop α) + ⊤ ≤ (↑x : WithTop α) + (↑a : WithTop α) → ⊤ ≤ (↑a : WithTop α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
z : WithTop α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x a : α
⊢ (↑x : WithTop α) + (↑a : WithTop α) ≤ (↑x : WithTop α) + z → (↑a : WithTop α) ≤ z
have coe : (↑x : WithTop α) + (↑a : WithTop α) ≤ (↑x : WithTop α) + ⊤ → (↑a : WithTop α) ≤ ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
z : WithTop α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x a : α
coe : (↑x : WithTop α) + (↑a : WithTop α) ≤ (↑x : WithTop α) + ⊤ → (↑a : WithTop α) ≤ ⊤
⊢ (↑x : WithTop α) + (↑a : WithTop α) ≤ (↑x : WithTop α) + z → (↑a : WithTop α) ≤ z
have coe₁ : ∀ (a_1 : α),
  (↑x : WithTop α) + (↑a : WithTop α) ≤ (↑x : WithTop α) + (↑a_1 : WithTop α) → (↑a : WithTop α) ≤ (↑a_1 : WithTop α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x a a_1 : α
⊢ (↑x : WithTop α) + (↑a : WithTop α) ≤ (↑x : WithTop α) + (↑a_1 : WithTop α) → (↑a : WithTop α) ≤ (↑a_1 : WithTop α)
have coe : x + a ≤ x + a_1 → a ≤ a_1
Tactic: simp [← coe_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LE α
inst_2 : AddRightReflectLE α
hz : z ≠ ⊤
⊢ x + z ≤ y + z → x ≤ y
have lift : ∀ (z : α), x + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → x ≤ y
Tactic: lift z to α using hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y : WithTop α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z : α
⊢ x + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → x ≤ y
have top : ⊤ + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → ⊤ ≤ y
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y : WithTop α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z : α
top : ⊤ + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → ⊤ ≤ y
⊢ x + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → x ≤ y
have coe : ∀ (a : α), (↑a : WithTop α) + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → (↑a : WithTop α) ≤ y
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z : α
⊢ ⊤ + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → ⊤ ≤ y
have top : ⊤ + (↑z : WithTop α) ≤ ⊤ + (↑z : WithTop α) → LE.le.{u} (α := WithTop α) ⊤ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z : α
top : ⊤ + (↑z : WithTop α) ≤ ⊤ + (↑z : WithTop α) → LE.le.{u} (α := WithTop α) ⊤ ⊤
⊢ ⊤ + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → ⊤ ≤ y
have top₁ : ∀ (a : α), ⊤ + (↑z : WithTop α) ≤ (↑a : WithTop α) + (↑z : WithTop α) → ⊤ ≤ (↑a : WithTop α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z a : α
⊢ (↑a : WithTop α) + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → (↑a : WithTop α) ≤ y
have coe : (↑a : WithTop α) + (↑z : WithTop α) ≤ ⊤ + (↑z : WithTop α) → (↑a : WithTop α) ≤ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z a : α
coe : (↑a : WithTop α) + (↑z : WithTop α) ≤ ⊤ + (↑z : WithTop α) → (↑a : WithTop α) ≤ ⊤
⊢ (↑a : WithTop α) + (↑z : WithTop α) ≤ y + (↑z : WithTop α) → (↑a : WithTop α) ≤ y
have coe₁ : ∀ (a_1 : α),
  (↑a : WithTop α) + (↑z : WithTop α) ≤ (↑a_1 : WithTop α) + (↑z : WithTop α) → (↑a : WithTop α) ≤ (↑a_1 : WithTop α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z a a_1 : α
⊢ (↑a : WithTop α) + (↑z : WithTop α) ≤ (↑a_1 : WithTop α) + (↑z : WithTop α) → (↑a : WithTop α) ≤ (↑a_1 : WithTop α)
have coe : a + z ≤ a_1 + z → a ≤ a_1
Tactic: simp [← coe_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
hx : x ≠ ⊤
⊢ y < z → x + y < x + z
have lift : ∀ (x : α), y < z → (↑x : WithTop α) + y < (↑x : WithTop α) + z
Tactic: lift x to α using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y z : WithTop α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x : α
⊢ y < z → (↑x : WithTop α) + y < (↑x : WithTop α) + z
have top : ⊤ < z → (↑x : WithTop α) + ⊤ < (↑x : WithTop α) + z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y z : WithTop α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x : α
top : ⊤ < z → (↑x : WithTop α) + ⊤ < (↑x : WithTop α) + z
⊢ y < z → (↑x : WithTop α) + y < (↑x : WithTop α) + z
have coe : ∀ (a : α), (↑a : WithTop α) < z → (↑x : WithTop α) + (↑a : WithTop α) < (↑x : WithTop α) + z
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
z : WithTop α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x : α
⊢ ⊤ < z → (↑x : WithTop α) + ⊤ < (↑x : WithTop α) + z
have top : LT.lt.{u} (α := WithTop α) ⊤ ⊤ → (↑x : WithTop α) + ⊤ < (↑x : WithTop α) + ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
z : WithTop α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x : α
top : LT.lt.{u} (α := WithTop α) ⊤ ⊤ → (↑x : WithTop α) + ⊤ < (↑x : WithTop α) + ⊤
⊢ ⊤ < z → (↑x : WithTop α) + ⊤ < (↑x : WithTop α) + z
have top₁ : ∀ (a : α), ⊤ < (↑a : WithTop α) → (↑x : WithTop α) + ⊤ < (↑x : WithTop α) + (↑a : WithTop α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
z : WithTop α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x a : α
⊢ (↑a : WithTop α) < z → (↑x : WithTop α) + (↑a : WithTop α) < (↑x : WithTop α) + z
have coe : (↑a : WithTop α) < ⊤ → (↑x : WithTop α) + (↑a : WithTop α) < (↑x : WithTop α) + ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
z : WithTop α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x a : α
coe : (↑a : WithTop α) < ⊤ → (↑x : WithTop α) + (↑a : WithTop α) < (↑x : WithTop α) + ⊤
⊢ (↑a : WithTop α) < z → (↑x : WithTop α) + (↑a : WithTop α) < (↑x : WithTop α) + z
have coe₁ : ∀ (a_1 : α),
  (↑a : WithTop α) < (↑a_1 : WithTop α) → (↑x : WithTop α) + (↑a : WithTop α) < (↑x : WithTop α) + (↑a_1 : WithTop α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x a a_1 : α
⊢ (↑a : WithTop α) < (↑a_1 : WithTop α) → (↑x : WithTop α) + (↑a : WithTop α) < (↑x : WithTop α) + (↑a_1 : WithTop α)
have coe : a < a_1 → x + a < x + a_1
Tactic: simp [← coe_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y z : WithTop α
inst_1 : LT α
inst_2 : AddRightStrictMono α
hz : z ≠ ⊤
⊢ x < y → x + z < y + z
have lift : ∀ (z : α), x < y → x + (↑z : WithTop α) < y + (↑z : WithTop α)
Tactic: lift z to α using hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y : WithTop α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z : α
⊢ x < y → x + (↑z : WithTop α) < y + (↑z : WithTop α)
have top : ⊤ < y → ⊤ + (↑z : WithTop α) < y + (↑z : WithTop α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y : WithTop α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z : α
top : ⊤ < y → ⊤ + (↑z : WithTop α) < y + (↑z : WithTop α)
⊢ x < y → x + (↑z : WithTop α) < y + (↑z : WithTop α)
have coe : ∀ (a : α), (↑a : WithTop α) < y → (↑a : WithTop α) + (↑z : WithTop α) < y + (↑z : WithTop α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z : α
⊢ ⊤ < y → ⊤ + (↑z : WithTop α) < y + (↑z : WithTop α)
have top : LT.lt.{u} (α := WithTop α) ⊤ ⊤ → ⊤ + (↑z : WithTop α) < ⊤ + (↑z : WithTop α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z : α
top : LT.lt.{u} (α := WithTop α) ⊤ ⊤ → ⊤ + (↑z : WithTop α) < ⊤ + (↑z : WithTop α)
⊢ ⊤ < y → ⊤ + (↑z : WithTop α) < y + (↑z : WithTop α)
have top₁ : ∀ (a : α), ⊤ < (↑a : WithTop α) → ⊤ + (↑z : WithTop α) < (↑a : WithTop α) + (↑z : WithTop α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z a : α
⊢ (↑a : WithTop α) < y → (↑a : WithTop α) + (↑z : WithTop α) < y + (↑z : WithTop α)
have coe : (↑a : WithTop α) < ⊤ → (↑a : WithTop α) + (↑z : WithTop α) < ⊤ + (↑z : WithTop α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithTop α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z a : α
coe : (↑a : WithTop α) < ⊤ → (↑a : WithTop α) + (↑z : WithTop α) < ⊤ + (↑z : WithTop α)
⊢ (↑a : WithTop α) < y → (↑a : WithTop α) + (↑z : WithTop α) < y + (↑z : WithTop α)
have coe₁ : ∀ (a_1 : α),
  (↑a : WithTop α) < (↑a_1 : WithTop α) → (↑a : WithTop α) + (↑z : WithTop α) < (↑a_1 : WithTop α) + (↑z : WithTop α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z a a_1 : α
⊢ (↑a : WithTop α) < (↑a_1 : WithTop α) → (↑a : WithTop α) + (↑z : WithTop α) < (↑a_1 : WithTop α) + (↑z : WithTop α)
have coe : a < a_1 → a + z < a_1 + z
Tactic: simp [← coe_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
w x y z : WithTop α
inst_1 : Preorder α
inst_2 : AddLeftStrictMono α
inst_3 : AddRightStrictMono α
xz : x < z
yw : y < w
⊢ x + y < z + w
have apply : x + w ≤ z + w
Tactic: apply (WithTop.add_lt_add_left xz.ne_top yw).trans_le
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
w x y z : WithTop α
inst_1 : Preorder α
inst_2 : AddLeftStrictMono α
inst_3 : AddRightStrictMono α
xz : x < z
yw : y < w
⊢ x + w ≤ z + w
have top : ∀ (yw : y < ⊤), x + ⊤ ≤ z + ⊤
Tactic: cases w
Cleared hypotheses: w, yw
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
w x y z : WithTop α
inst_1 : Preorder α
inst_2 : AddLeftStrictMono α
inst_3 : AddRightStrictMono α
xz : x < z
yw : y < w
top : ∀ (yw : y < ⊤), x + ⊤ ≤ z + ⊤
⊢ x + w ≤ z + w
have coe : ∀ (a : α) (yw : y < (↑a : WithTop α)), x + (↑a : WithTop α) ≤ z + (↑a : WithTop α)
Tactic: cases w
Cleared hypotheses: w, yw
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
a b : WithTop α
⊢ map (⇑f : (a : α) → β) (a + b) = HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) a) (map (⇑f : (a : α) → β) b)
have top : map (⇑f : (a : α) → β) (⊤ + b) =
  HAdd.hAdd (α := WithTop β) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊤) (map (⇑f : (a : α) → β) b)
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
a b : WithTop α
top :
  map (⇑f : (a : α) → β) (⊤ + b) =
    HAdd.hAdd (α := WithTop β) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊤) (map (⇑f : (a : α) → β) b)
⊢ map (⇑f : (a : α) → β) (a + b) = HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) a) (map (⇑f : (a : α) → β) b)
have coe : ∀ (a : α),
  map (⇑f : (a : α) → β) ((↑a : WithTop α) + b) =
    HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map (⇑f : (a : α) → β) b)
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
b : WithTop α
a : α
⊢ map (⇑f : (a : α) → β) ((↑a : WithTop α) + b) =
    HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map (⇑f : (a : α) → β) b)
have coe : map (⇑f : (a : α) → β) ((↑a : WithTop α) + ⊤) =
  HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊤)
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
b : WithTop α
a : α
coe :
  map (⇑f : (a : α) → β) ((↑a : WithTop α) + ⊤) =
    HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊤)
⊢ map (⇑f : (a : α) → β) ((↑a : WithTop α) + b) =
    HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map (⇑f : (a : α) → β) b)
have coe₁ : ∀ (a_1 : α),
  map (⇑f : (a : α) → β) ((↑a : WithTop α) + (↑a_1 : WithTop α)) =
    HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map (⇑f : (a : α) → β) (↑a_1 : WithTop α))
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
a a_1 : α
⊢ map (⇑f : (a : α) → β) ((↑a : WithTop α) + (↑a_1 : WithTop α)) =
    HAdd.hAdd (α := WithTop β) (map (⇑f : (a : α) → β) (↑a : WithTop α)) (map (⇑f : (a : α) → β) (↑a_1 : WithTop α))
have coe : Eq.{v + 1} (α := WithTop β) (map (⇑f : (a : α) → β) (↑(a + a_1) : WithTop α) : WithTop β)
  ((↑((f : (a : α) → β) (a + a_1)) : WithTop β) : WithTop β)
Tactic: rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : AddMonoid α
a : WithTop α
⊢ Eq (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) a, 0 with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤ :
      WithTop α)
    (0 : WithTop α)
have top : Eq.{u + 1} (α := WithTop α)
  (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤ :
    WithTop α)
  (0 : WithTop α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : AddMonoid α
a : WithTop α
top :
  Eq.{u + 1} (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤ :
      WithTop α)
    (0 : WithTop α)
⊢ Eq (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) a, 0 with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤ :
      WithTop α)
    (0 : WithTop α)
have coe : ∀ (a : α),
  Eq (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), 0 with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤ :
      WithTop α)
    (0 : WithTop α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : AddMonoid α
n : ℕ
a : WithTop α
⊢ (match (motive := WithTop α → ℕ → WithTop α) a, n + 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, n with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      a
have top : (match (motive := WithTop α → ℕ → WithTop α) ⊤, n + 1 with
  | Option.some a, n => (↑(n • a) : WithTop α)
  | none, 0 => 0
  | none, _n.succ => ⊤) =
  HAdd.hAdd (α := WithTop α) (β := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) ⊤, n with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤ :
      WithTop α)
    (⊤ : WithTop α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : AddMonoid α
n : ℕ
a : WithTop α
top :
  (match (motive := WithTop α → ℕ → WithTop α) ⊤, n + 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α) (β := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) ⊤, n with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (⊤ : WithTop α)
⊢ (match (motive := WithTop α → ℕ → WithTop α) a, n + 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) a, n with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      a
have coe : ∀ (a : α),
  (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n + 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (↑a : WithTop α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : AddMonoid α
n : ℕ
⊢ (match (motive := WithTop α → ℕ → WithTop α) ⊤, n + 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α) (β := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) ⊤, n with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (⊤ : WithTop α)
have top : (match (motive := WithTop α → ℕ → WithTop α) ⊤, HAdd.hAdd (α := ℕ) 0 1 with
  | Option.some a, n => (↑(n • a) : WithTop α)
  | none, 0 => 0
  | none, _n.succ => ⊤) =
  HAdd.hAdd (α := WithTop α) (β := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) ⊤, 0 with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤ :
      WithTop α)
    (⊤ : WithTop α)
Tactic: cases n
Cleared hypotheses: n