awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u
inst : Add α
z : WithBot α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x : α
⊢ (↑x : WithBot α) + ⊥ ≤ (↑x : WithBot α) + z → ⊥ ≤ z
have bot : (↑x : WithBot α) + ⊥ ≤ (↑x : WithBot α) + ⊥ → LE.le.{u} (α := 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 : LE α
inst_2 : AddLeftReflectLE α
x : α
bot : (↑x : WithBot α) + ⊥ ≤ (↑x : WithBot α) + ⊥ → LE.le.{u} (α := 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 : LE α
inst_2 : AddLeftReflectLE α
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 : LE α
inst_2 : AddLeftReflectLE α
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
inst : Add α
inst_1 : LE α
inst_2 : AddLeftReflectLE α
x a a_1 : α
⊢ (↑x : WithBot α) + (↑a : WithBot α) ≤ (↑x : WithBot α) + (↑a_1 : WithBot α) → (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
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 : WithBot α
inst_1 : LE α
inst_2 : AddRightReflectLE α
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 : LE α
inst_2 : AddRightReflectLE α
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 : LE α
inst_2 : AddRightReflectLE α
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 : LE α
inst_2 : AddRightReflectLE α
z : α
⊢ ⊥ + (↑z : WithBot α) ≤ y + (↑z : WithBot α) → ⊥ ≤ y
have bot : ⊥ + (↑z : WithBot α) ≤ ⊥ + (↑z : WithBot α) → LE.le.{u} (α := 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 : LE α
inst_2 : AddRightReflectLE α
z : α
bot : ⊥ + (↑z : WithBot α) ≤ ⊥ + (↑z : WithBot α) → LE.le.{u} (α := 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 : LE α
inst_2 : AddRightReflectLE α
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 : LE α
inst_2 : AddRightReflectLE α
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 α
inst_1 : LE α
inst_2 : AddRightReflectLE α
z a a_1 : α
⊢ (↑a : WithBot α) + (↑z : WithBot α) ≤ (↑a_1 : WithBot α) + (↑z : WithBot α) → (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
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 : WithBot α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
hx : x ≠ ⊥
⊢ y < z → x + y < x + z
have lift : ∀ (x : α), y < z → (↑x : WithBot α) + y < (↑x : WithBot α) + 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 : LT α
inst_2 : AddLeftStrictMono α
x : α
⊢ y < z → (↑x : WithBot α) + y < (↑x : WithBot α) + z
have bot : ⊥ < z → (↑x : WithBot α) + ⊥ < (↑x : 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 α
y z : WithBot α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x : α
bot : ⊥ < z → (↑x : WithBot α) + ⊥ < (↑x : WithBot α) + z
⊢ y < z → (↑x : WithBot α) + y < (↑x : WithBot α) + z
have coe : ∀ (a : α), (↑a : WithBot α) < z → (↑x : WithBot α) + (↑a : WithBot α) < (↑x : 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 : LT α
inst_2 : AddLeftStrictMono α
x : α
⊢ ⊥ < z → (↑x : WithBot α) + ⊥ < (↑x : WithBot α) + z
have bot : LT.lt.{u} (α := WithBot α) ⊥ ⊥ → (↑x : WithBot α) + ⊥ < (↑x : 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 : LT α
inst_2 : AddLeftStrictMono α
x : α
bot : LT.lt.{u} (α := WithBot α) ⊥ ⊥ → (↑x : WithBot α) + ⊥ < (↑x : WithBot α) + ⊥
⊢ ⊥ < z → (↑x : WithBot α) + ⊥ < (↑x : WithBot α) + z
have bot₁ : ∀ (a : α), ⊥ < (↑a : WithBot α) → (↑x : 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 : LT α
inst_2 : AddLeftStrictMono α
x a : α
⊢ (↑a : WithBot α) < z → (↑x : WithBot α) + (↑a : WithBot α) < (↑x : WithBot α) + z
have coe : (↑a : WithBot α) < ⊥ → (↑x : WithBot α) + (↑a : WithBot α) < (↑x : 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 : LT α
inst_2 : AddLeftStrictMono α
x a : α
coe : (↑a : WithBot α) < ⊥ → (↑x : WithBot α) + (↑a : WithBot α) < (↑x : WithBot α) + ⊥
⊢ (↑a : WithBot α) < z → (↑x : WithBot α) + (↑a : WithBot α) < (↑x : WithBot α) + z
have coe₁ : ∀ (a_1 : α),
  (↑a : WithBot α) < (↑a_1 : WithBot α) → (↑x : WithBot α) + (↑a : WithBot α) < (↑x : 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
inst : Add α
inst_1 : LT α
inst_2 : AddLeftStrictMono α
x a a_1 : α
⊢ (↑a : WithBot α) < (↑a_1 : WithBot α) → (↑x : WithBot α) + (↑a : WithBot α) < (↑x : WithBot α) + (↑a_1 : WithBot α)
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 : WithBot α
inst_1 : LT α
inst_2 : AddRightStrictMono α
hz : z ≠ ⊥
⊢ x < y → x + z < y + z
have lift : ∀ (z : α), x < y → x + (↑z : WithBot α) < y + (↑z : WithBot α)
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 : LT α
inst_2 : AddRightStrictMono α
z : α
⊢ x < y → x + (↑z : WithBot α) < y + (↑z : WithBot α)
have bot : ⊥ < y → ⊥ + (↑z : WithBot α) < y + (↑z : 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 α
inst_1 : LT α
inst_2 : AddRightStrictMono α
z : α
bot : ⊥ < y → ⊥ + (↑z : WithBot α) < y + (↑z : WithBot α)
⊢ x < y → x + (↑z : WithBot α) < y + (↑z : WithBot α)
have coe : ∀ (a : α), (↑a : WithBot α) < y → (↑a : WithBot α) + (↑z : WithBot α) < y + (↑z : WithBot α)
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 : LT α
inst_2 : AddRightStrictMono α
z : α
⊢ ⊥ < y → ⊥ + (↑z : WithBot α) < y + (↑z : WithBot α)
have bot : LT.lt.{u} (α := WithBot α) ⊥ ⊥ → ⊥ + (↑z : WithBot α) < ⊥ + (↑z : 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 : LT α
inst_2 : AddRightStrictMono α
z : α
bot : LT.lt.{u} (α := WithBot α) ⊥ ⊥ → ⊥ + (↑z : WithBot α) < ⊥ + (↑z : WithBot α)
⊢ ⊥ < y → ⊥ + (↑z : WithBot α) < y + (↑z : WithBot α)
have bot₁ : ∀ (a : α), ⊥ < (↑a : WithBot α) → ⊥ + (↑z : WithBot α) < (↑a : WithBot α) + (↑z : 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 : LT α
inst_2 : AddRightStrictMono α
z a : α
⊢ (↑a : WithBot α) < y → (↑a : WithBot α) + (↑z : WithBot α) < y + (↑z : WithBot α)
have coe : (↑a : WithBot α) < ⊥ → (↑a : WithBot α) + (↑z : WithBot α) < ⊥ + (↑z : 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 : LT α
inst_2 : AddRightStrictMono α
z a : α
coe : (↑a : WithBot α) < ⊥ → (↑a : WithBot α) + (↑z : WithBot α) < ⊥ + (↑z : WithBot α)
⊢ (↑a : WithBot α) < y → (↑a : WithBot α) + (↑z : WithBot α) < y + (↑z : WithBot α)
have coe₁ : ∀ (a_1 : α),
  (↑a : WithBot α) < (↑a_1 : WithBot α) → (↑a : WithBot α) + (↑z : WithBot α) < (↑a_1 : WithBot α) + (↑z : WithBot α)
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 : WithBot α) < (↑a_1 : WithBot α) → (↑a : WithBot α) + (↑z : WithBot α) < (↑a_1 : WithBot α) + (↑z : WithBot α)
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_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
⊢ a + c ≤ b + c ↔ a ≤ b
have bot : ⊥ + c ≤ b + c ↔ ⊥ ≤ b
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
bot : ⊥ + c ≤ b + c ↔ ⊥ ≤ b
⊢ a + c ≤ b + c ↔ a ≤ b
have coe : ∀ (a : WithTop α), (↑a : WithBot (WithTop α)) + c ≤ b + c ↔ (↑a : WithBot (WithTop α)) ≤ b
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
⊢ ⊥ + c ≤ b + c ↔ ⊥ ≤ b
have bot : ⊥ + c ≤ ⊥ + c ↔ LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
bot : ⊥ + c ≤ ⊥ + c ↔ LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
⊢ ⊥ + c ≤ b + c ↔ ⊥ ≤ b
have bot₁ : ∀ (a : WithTop α), ⊥ + c ≤ (↑a : WithBot (WithTop α)) + c ↔ ⊥ ≤ (↑a : WithBot (WithTop α))
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a : WithTop α
⊢ (↑a : WithBot (WithTop α)) + c ≤ b + c ↔ (↑a : WithBot (WithTop α)) ≤ b
have coe : (↑a : WithBot (WithTop α)) + c ≤ ⊥ + c ↔ (↑a : WithBot (WithTop α)) ≤ ⊥
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a : WithTop α
coe : (↑a : WithBot (WithTop α)) + c ≤ ⊥ + c ↔ (↑a : WithBot (WithTop α)) ≤ ⊥
⊢ (↑a : WithBot (WithTop α)) + c ≤ b + c ↔ (↑a : WithBot (WithTop α)) ≤ b
have coe₁ : ∀ (a_1 : WithTop α),
  (↑a : WithBot (WithTop α)) + c ≤ (↑a_1 : WithBot (WithTop α)) + c ↔
    (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
⊢ ⊥ + c ≤ ⊥ + c ↔ LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
have bot : ∀ (hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥) (hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤),
  HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ≤ HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ↔
    LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
Tactic: induction c
Cleared hypotheses: c, hc, hc'
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
bot :
  ∀ (hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥) (hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤),
    HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ≤ HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ↔
      LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
⊢ ⊥ + c ≤ ⊥ + c ↔ LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
have bot₁ : ∀ (a : WithTop α) (hc : (↑a : WithBot (WithTop α)) ≠ ⊥) (hc' : (↑a : WithBot (WithTop α)) ≠ ⊤),
  ⊥ + (↑a : WithBot (WithTop α)) ≤ ⊥ + (↑a : WithBot (WithTop α)) ↔ LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
Tactic: induction c
Cleared hypotheses: c, hc, hc'
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a : WithTop α
⊢ ⊥ + c ≤ (↑a : WithBot (WithTop α)) + c ↔ ⊥ ≤ (↑a : WithBot (WithTop α))
have bot : ∀ (hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥) (hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤),
  HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ≤ (↑a : WithBot (WithTop α)) + ⊥ ↔ ⊥ ≤ (↑a : WithBot (WithTop α))
Tactic: induction c
Cleared hypotheses: c, hc, hc'
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a : WithTop α
bot :
  ∀ (hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥) (hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤),
    HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ≤ (↑a : WithBot (WithTop α)) + ⊥ ↔ ⊥ ≤ (↑a : WithBot (WithTop α))
⊢ ⊥ + c ≤ (↑a : WithBot (WithTop α)) + c ↔ ⊥ ≤ (↑a : WithBot (WithTop α))
have bot₁ : ∀ (a_1 : WithTop α) (hc : (↑a_1 : WithBot (WithTop α)) ≠ ⊥) (hc' : (↑a_1 : WithBot (WithTop α)) ≠ ⊤),
  ⊥ + (↑a_1 : WithBot (WithTop α)) ≤ (↑a : WithBot (WithTop α)) + (↑a_1 : WithBot (WithTop α)) ↔
    ⊥ ≤ (↑a : WithBot (WithTop α))
Tactic: induction c
Cleared hypotheses: c, hc, hc'
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a : WithTop α
⊢ (↑a : WithBot (WithTop α)) + c ≤ ⊥ + c ↔ (↑a : WithBot (WithTop α)) ≤ ⊥
have coe : ∀ (hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥) (hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤),
  (↑a : WithBot (WithTop α)) + ⊥ ≤ HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ↔ (↑a : WithBot (WithTop α)) ≤ ⊥
Tactic: induction c
Cleared hypotheses: c, hc, hc'
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a : WithTop α
coe :
  ∀ (hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥) (hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤),
    (↑a : WithBot (WithTop α)) + ⊥ ≤ HAdd.hAdd (α := WithBot (WithTop α)) ⊥ ⊥ ↔ (↑a : WithBot (WithTop α)) ≤ ⊥
⊢ (↑a : WithBot (WithTop α)) + c ≤ ⊥ + c ↔ (↑a : WithBot (WithTop α)) ≤ ⊥
have coe₁ : ∀ (a_1 : WithTop α) (hc : (↑a_1 : WithBot (WithTop α)) ≠ ⊥) (hc' : (↑a_1 : WithBot (WithTop α)) ≠ ⊤),
  (↑a : WithBot (WithTop α)) + (↑a_1 : WithBot (WithTop α)) ≤ ⊥ + (↑a_1 : WithBot (WithTop α)) ↔
    (↑a : WithBot (WithTop α)) ≤ ⊥
Tactic: induction c
Cleared hypotheses: c, hc, hc'
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a a_1 : WithTop α
⊢ (↑a : WithBot (WithTop α)) + c ≤ (↑a_1 : WithBot (WithTop α)) + c ↔
    (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))
have coe : ∀ (hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥) (hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤),
  (↑a : WithBot (WithTop α)) + ⊥ ≤ (↑a_1 : WithBot (WithTop α)) + ⊥ ↔
    (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))
Tactic: induction c
Cleared hypotheses: c, hc, hc'
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
a a_1 : WithTop α
coe :
  ∀ (hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥) (hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤),
    (↑a : WithBot (WithTop α)) + ⊥ ≤ (↑a_1 : WithBot (WithTop α)) + ⊥ ↔
      (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))
⊢ (↑a : WithBot (WithTop α)) + c ≤ (↑a_1 : WithBot (WithTop α)) + c ↔
    (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))
have coe₁ : ∀ (a_2 : WithTop α) (hc : (↑a_2 : WithBot (WithTop α)) ≠ ⊥) (hc' : (↑a_2 : WithBot (WithTop α)) ≠ ⊤),
  (↑a : WithBot (WithTop α)) + (↑a_2 : WithBot (WithTop α)) ≤
      (↑a_1 : WithBot (WithTop α)) + (↑a_2 : WithBot (WithTop α)) ↔
    (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))
Tactic: induction c
Cleared hypotheses: c, hc, hc'
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a : WithTop α
hc : (↑a : WithBot (WithTop α)) ≠ ⊥
hc' : (↑a : WithBot (WithTop α)) ≠ ⊤
⊢ ⊥ + (↑a : WithBot (WithTop α)) ≤ ⊥ + (↑a : WithBot (WithTop α)) ↔ LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
have bot : ∀ (hc' : ¬a = ⊤),
  ⊥ + (↑a : WithBot (WithTop α)) ≤ ⊥ + (↑a : WithBot (WithTop α)) ↔ LE.le.{u_1} (α := WithBot (WithTop α)) ⊥ ⊥
Tactic: norm_cast at *
Cleared hypotheses: hc'
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (hypothesis)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a a_1 : WithTop α
hc : (↑a_1 : WithBot (WithTop α)) ≠ ⊥
hc' : (↑a_1 : WithBot (WithTop α)) ≠ ⊤
⊢ ⊥ + (↑a_1 : WithBot (WithTop α)) ≤ (↑a : WithBot (WithTop α)) + (↑a_1 : WithBot (WithTop α)) ↔
    ⊥ ≤ (↑a : WithBot (WithTop α))
have hc'₁ : ¬a_1 = ⊤
Tactic: norm_cast at *
Cleared hypotheses: hc'
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (hypothesis)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a a_1 : WithTop α
hc : (↑a_1 : WithBot (WithTop α)) ≠ ⊥
hc' : (↑a_1 : WithBot (WithTop α)) ≠ ⊤
⊢ (↑a : WithBot (WithTop α)) + (↑a_1 : WithBot (WithTop α)) ≤ ⊥ + (↑a_1 : WithBot (WithTop α)) ↔
    (↑a : WithBot (WithTop α)) ≤ ⊥
have hc'₁ : ¬a_1 = ⊤
Tactic: norm_cast at *
Cleared hypotheses: hc'
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a a_1 : WithTop α
hc : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊥
hc' : Ne.{u_1 + 1} (α := WithBot (WithTop α)) ⊥ ⊤
⊢ (↑a : WithBot (WithTop α)) + ⊥ ≤ (↑a_1 : WithBot (WithTop α)) + ⊥ ↔
    (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))
have coe : (↑a : WithBot (WithTop α)) + ⊥ ≤ (↑a_1 : WithBot (WithTop α)) + ⊥ ↔ a ≤ a_1
Tactic: norm_cast at *
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Unbundled.WithTop (goal)
Goal:
α : Type u_1
inst : Add α
inst_1 : LE α
inst_2 : AddRightMono α
inst_3 : AddRightReflectLE α
a a_1 a_2 : WithTop α
hc : (↑a_2 : WithBot (WithTop α)) ≠ ⊥
hc' : (↑a_2 : WithBot (WithTop α)) ≠ ⊤
⊢ (↑a : WithBot (WithTop α)) + (↑a_2 : WithBot (WithTop α)) ≤
      (↑a_1 : WithBot (WithTop α)) + (↑a_2 : WithBot (WithTop α)) ↔
    (↑a : WithBot (WithTop α)) ≤ (↑a_1 : WithBot (WithTop α))
have coe : ∀ (hc' : ¬a_2 = ⊤), a + a_2 ≤ a_1 + a_2 ↔ a ≤ a_1
Tactic: norm_cast at *
Cleared hypotheses: hc'
-- 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 : WithBot α
⊢ map (⇑f : (a : α) → β) (a + b) = HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) a) (map (⇑f : (a : α) → β) b)
have bot : map (⇑f : (a : α) → β) (⊥ + b) =
  HAdd.hAdd (α := WithBot β) (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 : WithBot α
bot :
  map (⇑f : (a : α) → β) (⊥ + b) =
    HAdd.hAdd (α := WithBot β) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊥) (map (⇑f : (a : α) → β) b)
⊢ map (⇑f : (a : α) → β) (a + b) = HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) a) (map (⇑f : (a : α) → β) b)
have coe : ∀ (a : α),
  map (⇑f : (a : α) → β) ((↑a : WithBot α) + b) =
    HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (map (⇑f : (a : α) → β) b)
Tactic: induction a
Cleared hypotheses: a