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 : AddMonoid α
n : ℕ
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 α)
⊢ (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₁ : ∀ (n : ℕ),
  (match (motive := WithTop α → ℕ → WithTop α) ⊤, n + 1 + 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α) (β := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) ⊤, n + 1 with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (⊤ : WithTop α)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : AddMonoid α
n : ℕ
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 α)
have coe : (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), HAdd.hAdd (α := ℕ) 0 1 with
  | Option.some a, n => (↑(n • a) : WithTop α)
  | none, 0 => 0
  | none, _n.succ => ⊤) =
  HAdd.hAdd (α := WithTop α)
    (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), 0 with
      | Option.some a, n => (↑(n • a) : WithTop α)
      | none, 0 => 0
      | none, _n.succ => ⊤ :
      WithTop α)
    (↑a : WithTop α)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : AddMonoid α
n : ℕ
a : α
coe :
  (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), HAdd.hAdd (α := ℕ) 0 1 with
    | Option.some a, n => (↑(n • a) : WithTop α)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    HAdd.hAdd (α := WithTop α)
      (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), 0 with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (↑a : WithTop α)
⊢ (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 α)
have coe₁ : ∀ (n : ℕ),
  (match (motive := WithTop α → ℕ → WithTop α) (↑a : WithTop α), n + 1 + 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 + 1 with
        | Option.some a, n => (↑(n • a) : WithTop α)
        | none, 0 => 0
        | none, _n.succ => ⊤ :
        WithTop α)
      (↑a : WithTop α)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
inst : LE α
inst_1 : Add α
inst_2 : ExistsAddOfLE α
a_1 b_1 : WithTop α
a b : α
h : (↑a : WithTop α) ≤ (↑b : WithTop α)
⊢ ∃ (c : WithTop α), (↑b : WithTop α) = (↑a : WithTop α) + c
have obtain : ∀ (c : α) (h : (↑a : WithTop α) ≤ (↑(a + c) : WithTop α)),
  ∃ (c_1 : WithTop α), (↑(a + c) : WithTop α) = (↑a : WithTop α) + c_1
Tactic: obtain ⟨c, rfl⟩ := exists_add_of_le (WithTop.coe_le_coe.1 h)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst : One M
inst_1 : One N
f : OneHom M N
⊢ Eq.{u_2 + 1} (α := WithTop N) (map.{u_1, u_2} (α := M) (⇑f : (a : M) → N) 1) 1
have rw : Eq.{u_2 + 1} (α := WithTop N) ((↑((f : (a : M) → N) 1) : WithTop N) : WithTop N) (1 : WithTop N)
Tactic: rw [WithTop.map_one, map_one, coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst : One M
inst_1 : One N
f : OneHom M N
rw : Eq.{u_2 + 1} (α := WithTop N) ((↑((f : (a : M) → N) 1) : WithTop N) : WithTop N) (1 : WithTop N)
⊢ Eq.{u_2 + 1} (α := WithTop N) (map.{u_1, u_2} (α := M) (⇑f : (a : M) → N) 1) 1
have rw₁ : Eq.{u_2 + 1} (α := WithTop N) (↑1 : WithTop N) 1
Tactic: rw [WithTop.map_one, map_one, coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst : One M
inst_1 : One N
f : OneHom M N
rw : Eq.{u_2 + 1} (α := WithTop N) ((↑((f : (a : M) → N) 1) : WithTop N) : WithTop N) (1 : WithTop N)
rw₁ : Eq.{u_2 + 1} (α := WithTop N) (↑1 : WithTop N) 1
⊢ Eq.{u_2 + 1} (α := WithTop N) (map.{u_1, u_2} (α := M) (⇑f : (a : M) → N) 1) 1
have rw₂ : Eq.{u_2 + 1} (α := WithTop N) 1 1
Tactic: rw [WithTop.map_one, map_one, coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x : WithBot α
⊢ x + ⊥ = ⊥
have bot : HAdd.hAdd (α := WithBot α) ⊥ ⊥ = ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x : WithBot α
bot : HAdd.hAdd (α := WithBot α) ⊥ ⊥ = ⊥
⊢ x + ⊥ = ⊥
have coe : ∀ (a : α), (↑a : WithBot α) + ⊥ = ⊥
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 : WithBot α
⊢ x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥
have bot : ⊥ + y = ⊥ ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥ ∨ 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 : WithBot α
bot : ⊥ + y = ⊥ ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥ ∨ y = ⊥
⊢ x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥
have coe : ∀ (a : α), (↑a : WithBot α) + y = ⊥ ↔ (↑a : WithBot α) = ⊥ ∨ 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 : WithBot α
⊢ ⊥ + y = ⊥ ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥ ∨ y = ⊥
have bot : HAdd.hAdd (α := WithBot α) ⊥ ⊥ = ⊥ ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥ ∨ Eq.{u + 1} (α := WithBot α) ⊥ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithBot α
bot : HAdd.hAdd (α := WithBot α) ⊥ ⊥ = ⊥ ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥ ∨ Eq.{u + 1} (α := WithBot α) ⊥ ⊥
⊢ ⊥ + y = ⊥ ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥ ∨ y = ⊥
have bot₁ : ∀ (a : α), ⊥ + (↑a : WithBot α) = ⊥ ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥ ∨ (↑a : WithBot α) = ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithBot α
a : α
⊢ (↑a : WithBot α) + y = ⊥ ↔ (↑a : WithBot α) = ⊥ ∨ y = ⊥
have coe : (↑a : WithBot α) + ⊥ = ⊥ ↔ (↑a : WithBot α) = ⊥ ∨ Eq.{u + 1} (α := WithBot α) ⊥ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithBot α
a : α
coe : (↑a : WithBot α) + ⊥ = ⊥ ↔ (↑a : WithBot α) = ⊥ ∨ Eq.{u + 1} (α := WithBot α) ⊥ ⊥
⊢ (↑a : WithBot α) + y = ⊥ ↔ (↑a : WithBot α) = ⊥ ∨ y = ⊥
have coe₁ : ∀ (a_1 : α), (↑a : WithBot α) + (↑a_1 : WithBot α) = ⊥ ↔ (↑a : WithBot α) = ⊥ ∨ (↑a_1 : WithBot α) = ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y : WithBot α
⊢ x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥
have bot : ⊥ + y ≠ ⊥ ↔ Ne.{u + 1} (α := WithBot α) ⊥ ⊥ ∧ 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 : WithBot α
bot : ⊥ + y ≠ ⊥ ↔ Ne.{u + 1} (α := WithBot α) ⊥ ⊥ ∧ y ≠ ⊥
⊢ x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥
have coe : ∀ (a : α), (↑a : WithBot α) + y ≠ ⊥ ↔ (↑a : WithBot α) ≠ ⊥ ∧ 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 : WithBot α
⊢ ⊥ + y ≠ ⊥ ↔ Ne.{u + 1} (α := WithBot α) ⊥ ⊥ ∧ y ≠ ⊥
have bot : HAdd.hAdd (α := WithBot α) ⊥ ⊥ ≠ ⊥ ↔ Ne.{u + 1} (α := WithBot α) ⊥ ⊥ ∧ Ne.{u + 1} (α := WithBot α) ⊥ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithBot α
bot : HAdd.hAdd (α := WithBot α) ⊥ ⊥ ≠ ⊥ ↔ Ne.{u + 1} (α := WithBot α) ⊥ ⊥ ∧ Ne.{u + 1} (α := WithBot α) ⊥ ⊥
⊢ ⊥ + y ≠ ⊥ ↔ Ne.{u + 1} (α := WithBot α) ⊥ ⊥ ∧ y ≠ ⊥
have bot₁ : ∀ (a : α), ⊥ + (↑a : WithBot α) ≠ ⊥ ↔ Ne.{u + 1} (α := WithBot α) ⊥ ⊥ ∧ (↑a : WithBot α) ≠ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithBot α
a : α
⊢ (↑a : WithBot α) + y ≠ ⊥ ↔ (↑a : WithBot α) ≠ ⊥ ∧ y ≠ ⊥
have coe : (↑a : WithBot α) + ⊥ ≠ ⊥ ↔ (↑a : WithBot α) ≠ ⊥ ∧ Ne.{u + 1} (α := WithBot α) ⊥ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithBot α
a : α
coe : (↑a : WithBot α) + ⊥ ≠ ⊥ ↔ (↑a : WithBot α) ≠ ⊥ ∧ Ne.{u + 1} (α := WithBot α) ⊥ ⊥
⊢ (↑a : WithBot α) + y ≠ ⊥ ↔ (↑a : WithBot α) ≠ ⊥ ∧ y ≠ ⊥
have coe₁ : ∀ (a_1 : α), (↑a : WithBot α) + (↑a_1 : WithBot α) ≠ ⊥ ↔ (↑a : WithBot α) ≠ ⊥ ∧ (↑a_1 : WithBot α) ≠ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y : WithBot α
inst_1 : LT α
⊢ ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y
have simp_rw : x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥
Tactic: simp_rw [WithBot.bot_lt_iff_ne_bot, add_ne_bot]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
a b c : α
⊢ (↑a : WithBot α) + (↑b : WithBot α) = (↑c : WithBot α) ↔
    ∃ (a' : α), ∃ (b' : α), (↑a' : WithBot α) = (↑a : WithBot α) ∧ (↑b' : WithBot α) = (↑b : WithBot α) ∧ a' + b' = c
have norm_cast : a + b = c ↔ ∃ (a' : α), ∃ (b' : α), a' = a ∧ b' = b ∧ a' + b' = c
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
a : α
ha : IsAddLeftRegular a
b c : α
⊢ Eq.{u + 1} (α := WithBot α) ((fun (x : WithBot α) ↦ (↑a : WithBot α) + x) (Option.some b))
      ((fun (x : WithBot α) ↦ (↑a : WithBot α) + x) (Option.some c)) →
    Option.some b = Option.some c
have some : a + b = a + c → b = c
Tactic: simp [none_eq_bot, some_eq_coe, ← coe_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
a : α
ha : IsAddRightRegular a
b c : α
⊢ Eq.{u + 1} (α := WithBot α) ((fun (x : WithBot α) ↦ x + (↑a : WithBot α)) (Option.some b))
      ((fun (x : WithBot α) ↦ x + (↑a : WithBot α)) (Option.some c)) →
    Option.some b = Option.some c
have some : b + a = c + a → b = c
Tactic: simp [none_eq_bot, some_eq_coe, ← coe_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y z : WithBot α
inst_1 : IsRightCancelAdd α
hz : z ≠ ⊥
⊢ x + z = y + z ↔ x = y
have lift : ∀ (z : α), x + (↑z : WithBot α) = y + (↑z : WithBot α) ↔ 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 : WithBot α
inst_1 : IsRightCancelAdd α
z : α
⊢ x + (↑z : WithBot α) = y + (↑z : WithBot α) ↔ x = y
have bot : ⊥ + (↑z : WithBot α) = y + (↑z : WithBot α) ↔ ⊥ = 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 : WithBot α
inst_1 : IsRightCancelAdd α
z : α
bot : ⊥ + (↑z : WithBot α) = y + (↑z : WithBot α) ↔ ⊥ = y
⊢ x + (↑z : WithBot α) = y + (↑z : WithBot α) ↔ x = y
have coe : ∀ (a : α), (↑a : WithBot α) + (↑z : WithBot α) = y + (↑z : WithBot α) ↔ (↑a : WithBot α) = 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 : WithBot α
inst_1 : IsRightCancelAdd α
z : α
⊢ ⊥ + (↑z : WithBot α) = y + (↑z : WithBot α) ↔ ⊥ = y
have bot : ⊥ + (↑z : WithBot α) = ⊥ + (↑z : WithBot α) ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithBot α
inst_1 : IsRightCancelAdd α
z : α
bot : ⊥ + (↑z : WithBot α) = ⊥ + (↑z : WithBot α) ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥
⊢ ⊥ + (↑z : WithBot α) = y + (↑z : WithBot α) ↔ ⊥ = y
have bot₁ : ∀ (a : α), ⊥ + (↑z : WithBot α) = (↑a : WithBot α) + (↑z : WithBot α) ↔ ⊥ = (↑a : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithBot α
inst_1 : IsRightCancelAdd α
z a : α
⊢ (↑a : WithBot α) + (↑z : WithBot α) = y + (↑z : WithBot α) ↔ (↑a : WithBot α) = y
have coe : (↑a : WithBot α) + (↑z : WithBot α) = ⊥ + (↑z : WithBot α) ↔ (↑a : WithBot α) = ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
y : WithBot α
inst_1 : IsRightCancelAdd α
z a : α
coe : (↑a : WithBot α) + (↑z : WithBot α) = ⊥ + (↑z : WithBot α) ↔ (↑a : WithBot α) = ⊥
⊢ (↑a : WithBot α) + (↑z : WithBot α) = y + (↑z : WithBot α) ↔ (↑a : WithBot α) = y
have coe₁ : ∀ (a_1 : α),
  (↑a : WithBot α) + (↑z : WithBot α) = (↑a_1 : WithBot α) + (↑z : WithBot α) ↔ (↑a : WithBot α) = (↑a_1 : WithBot α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
x y z : WithBot α
inst_1 : IsLeftCancelAdd α
hx : x ≠ ⊥
⊢ x + y = x + z ↔ y = z
have lift : ∀ (x : α), (↑x : WithBot α) + y = (↑x : WithBot α) + 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 : WithBot α
inst_1 : IsLeftCancelAdd α
x : α
⊢ (↑x : WithBot α) + y = (↑x : WithBot α) + z ↔ y = z
have bot : (↑x : WithBot α) + ⊥ = (↑x : WithBot α) + 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 : WithBot α
inst_1 : IsLeftCancelAdd α
x : α
bot : (↑x : WithBot α) + ⊥ = (↑x : WithBot α) + z ↔ ⊥ = z
⊢ (↑x : WithBot α) + y = (↑x : WithBot α) + z ↔ y = z
have coe : ∀ (a : α), (↑x : WithBot α) + (↑a : WithBot α) = (↑x : WithBot α) + z ↔ (↑a : WithBot α) = 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 : WithBot α
inst_1 : IsLeftCancelAdd α
x : α
⊢ (↑x : WithBot α) + ⊥ = (↑x : WithBot α) + z ↔ ⊥ = z
have bot : (↑x : WithBot α) + ⊥ = (↑x : WithBot α) + ⊥ ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
z : WithBot α
inst_1 : IsLeftCancelAdd α
x : α
bot : (↑x : WithBot α) + ⊥ = (↑x : WithBot α) + ⊥ ↔ Eq.{u + 1} (α := WithBot α) ⊥ ⊥
⊢ (↑x : WithBot α) + ⊥ = (↑x : WithBot α) + z ↔ ⊥ = z
have bot₁ : ∀ (a : α), (↑x : WithBot α) + ⊥ = (↑x : WithBot α) + (↑a : WithBot α) ↔ ⊥ = (↑a : WithBot α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
z : WithBot α
inst_1 : IsLeftCancelAdd α
x a : α
⊢ (↑x : WithBot α) + (↑a : WithBot α) = (↑x : WithBot α) + z ↔ (↑a : WithBot α) = z
have coe : (↑x : WithBot α) + (↑a : WithBot α) = (↑x : WithBot α) + ⊥ ↔ (↑a : WithBot α) = ⊥
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
z : WithBot α
inst_1 : IsLeftCancelAdd α
x a : α
coe : (↑x : WithBot α) + (↑a : WithBot α) = (↑x : WithBot α) + ⊥ ↔ (↑a : WithBot α) = ⊥
⊢ (↑x : WithBot α) + (↑a : WithBot α) = (↑x : WithBot α) + z ↔ (↑a : WithBot α) = z
have coe₁ : ∀ (a_1 : α),
  (↑x : WithBot α) + (↑a : WithBot α) = (↑x : WithBot α) + (↑a_1 : WithBot α) ↔ (↑a : WithBot α) = (↑a_1 : WithBot α)
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_1 y_1 z_1 : WithBot α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
x y z : WithBot α
⊢ (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) x y)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) x z)
have bot : (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) y z →
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ y)
    ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ 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 : WithBot α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
x y z : WithBot α
bot :
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ y)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z)
⊢ (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) x y)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) x z)
have coe : ∀ (a : α),
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a : WithBot α) y)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a : WithBot α) 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 : WithBot α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
y z : WithBot α
⊢ (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ y)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z)
have bot : (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ⊥ z →
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
    ((fun (x1 x2 : WithBot α) ↦ 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 : WithBot α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
y z : WithBot α
bot :
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ⊥ z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z)
⊢ (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ y)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z)
have bot₁ : ∀ (a : α),
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) (↑a : WithBot α) z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a : WithBot α))
      ((fun (x1 x2 : WithBot α) ↦ 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 : WithBot α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
y z : WithBot α
a_1 : α
⊢ (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) y)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) z)
have coe : (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ⊥ z →
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) ⊥)
    ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) 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 : WithBot α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
y z : WithBot α
a_1 : α
coe :
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ⊥ z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) ⊥)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) z)
⊢ (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) y z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) y)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) z)
have coe₁ : ∀ (a : α),
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) (↑a : WithBot α) z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) (↑a : WithBot α))
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) (↑a_1 : WithBot α) 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 : WithBot α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
z : WithBot α
⊢ (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ⊥ z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z)
have bot : (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ⊥ ⊥ →
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
    ((fun (x1 x2 : WithBot α) ↦ 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 : WithBot α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
z : WithBot α
bot :
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ⊥ ⊥ →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
⊢ (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ⊥ z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z)
have bot₁ : ∀ (a : α),
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ⊥ (↑a : WithBot α) →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a : WithBot α))
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 : WithBot α
a b : α
inst_1 : LE α
inst_2 : AddLeftMono α
z : WithBot α
a_1 : α
⊢ (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) (↑a_1 : WithBot α) z →
    (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a_1 : WithBot α))
      ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ z)
have bot : (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) (↑a_1 : WithBot α) ⊥ →
  (fun (x1 x2 : WithBot α) ↦ x1 ≤ x2) ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ (↑a_1 : WithBot α))
    ((fun (x1 x2 : WithBot α) ↦ x1 + x2) ⊥ ⊥)
Tactic: cases z
Cleared hypotheses: z