-- Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
protected lemma addLeftMono [AddZeroClass α] [AddLeftMono α]
    (h : ∀ a : α, 0 ≤ a) : AddLeftMono (WithZero α)

Proof state:
case h₂.h₂.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ a✝¹ + a✝ ≤ a✝¹ + c

Tactic:
exact add_le_add_left hbc' _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a b c : WithZero α
hbc : b ≤ c
⊢ a + b ≤ a + c

Tactic:
induction a

Result:
case h₁
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
⊢ 0 + b ≤ 0 + c

case h₂
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
a✝ : α
⊢ ↑a✝ + b ≤ ↑a✝ + c

Proof state:
case h₂.h₁.h₂
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ : α
hbc : 0 ≤ ↑a✝
⊢ ↑a✝¹ ≤ ↑a✝¹ + ↑a✝

Tactic:
rw [← coe_add, coe_le_coe]

Result:
case h₂.h₁.h₂
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ : α
hbc : 0 ≤ ↑a✝
⊢ a✝¹ ≤ a✝¹ + a✝

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
⊢ AddLeftMono (WithZero α)

Tactic:
refine ⟨fun a b c hbc => ?_⟩

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a b c : WithZero α
hbc : b ≤ c
⊢ a + b ≤ a + c

Proof state:
case h₂.h₁
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ ≤ ↑a✝ + c

Tactic:
induction c

Result:
case h₂.h₁.h₁
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝ : α
hbc : 0 ≤ 0
⊢ ↑a✝ ≤ ↑a✝ + 0

case h₂.h₁.h₂
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ : α
hbc : 0 ≤ ↑a✝
⊢ ↑a✝¹ ≤ ↑a✝¹ + ↑a✝

Proof state:
case h₂
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
a✝ : α
⊢ ↑a✝ + b ≤ ↑a✝ + c

Tactic:
induction b

Result:
case h₂.h₁
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ + 0 ≤ ↑a✝ + c

case h₂.h₂
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝¹ a✝ : α
hbc : ↑a✝ ≤ c
⊢ ↑a✝¹ + ↑a✝ ≤ ↑a✝¹ + c

Proof state:
case h₂.h₁.h₂
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ : α
hbc : 0 ≤ ↑a✝
⊢ a✝¹ ≤ a✝¹ + a✝

Tactic:
exact le_add_of_nonneg_right (h _)

Result:
no goals

Proof state:
case h₂.h₂.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑a✝¹ + ↑a✝ ≤ ↑a✝¹ + ↑c

Tactic:
rw [← coe_add, ← coe_add _ c, coe_le_coe]

Result:
case h₂.h₂.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ a✝¹ + a✝ ≤ a✝¹ + c

Proof state:
case h₂.h₁.h₁
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝ : α
hbc : 0 ≤ 0
⊢ ↑a✝ ≤ ↑a✝ + 0

Tactic:
rw [add_zero]

Result:
no goals

Proof state:
case h₁
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
⊢ 0 + b ≤ 0 + c

Tactic:
rwa [zero_add, zero_add]

Result:
no goals

Proof state:
case h₂.h₂
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝¹ a✝ : α
hbc : ↑a✝ ≤ c
⊢ ↑a✝¹ + ↑a✝ ≤ ↑a✝¹ + c

Tactic:
rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩

Result:
case h₂.h₂.intro.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑a✝¹ + ↑a✝ ≤ ↑a✝¹ + ↑c

Proof state:
case h₂.h₁
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ + 0 ≤ ↑a✝ + c

Tactic:
rw [add_zero]

Result:
case h₂.h₁
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddZeroClass α
inst✝ : AddLeftMono α
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ ≤ ↑a✝ + c