[GOAL]
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
⊢ CovariantClass (WithZero α) (WithZero α) (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
[PROOFSTEP]
refine ⟨fun a b c hbc => ?_⟩
[GOAL]
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : WithZero α
hbc : b ≤ c
⊢ a * b ≤ a * c
[PROOFSTEP]
induction a using WithZero.recZeroCoe
[GOAL]
case h₁
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
b c : WithZero α
hbc : b ≤ c
⊢ 0 * b ≤ 0 * c
[PROOFSTEP]
exact zero_le _
[GOAL]
case h₂
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
b c : WithZero α
hbc : b ≤ c
a✝ : α
⊢ ↑a✝ * b ≤ ↑a✝ * c
[PROOFSTEP]
induction b using WithZero.recZeroCoe
[GOAL]
case h₂.h₁
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ * 0 ≤ ↑a✝ * c
[PROOFSTEP]
exact zero_le _
[GOAL]
case h₂.h₂
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
c : WithZero α
a✝¹ a✝ : α
hbc : ↑a✝ ≤ c
⊢ ↑a✝¹ * ↑a✝ ≤ ↑a✝¹ * c
[PROOFSTEP]
rcases WithBot.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
[GOAL]
case h₂.h₂.intro.intro
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑a✝¹ * ↑a✝ ≤ ↑a✝¹ * ↑c
[PROOFSTEP]
refine
  le_trans ?_
    (le_of_eq <| coe_mul)
      -- rw [← coe_mul, ← coe_mul, coe_le_coe]
        -- Porting note: rewriting `coe_mul` here doesn't work because of some difference between
        -- `coe` and `WithBot.some`, even though they're definitionally equal as shown by the `refine'`
[GOAL]
case h₂.h₂.intro.intro
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑a✝¹ * ↑a✝ ≤ ↑(a✝¹ * c)
[PROOFSTEP]
rw [← coe_mul, coe_le_coe]
[GOAL]
case h₂.h₂.intro.intro
α : Type u
inst✝² : Mul α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ a✝¹ * a✝ ≤ a✝¹ * c
[PROOFSTEP]
exact mul_le_mul_left' hbc' _
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ ↑a ≤ max ↑b ↑c ↔ a ≤ max b c
[PROOFSTEP]
simp only [WithZero.coe_le_coe, le_max_iff]
[GOAL]
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min ↑a ↑b ≤ ↑c ↔ min a b ≤ c
[PROOFSTEP]
simp only [WithZero.coe_le_coe, min_le_iff]
[GOAL]
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
⊢ CovariantClass (WithZero α) (WithZero α) (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
[PROOFSTEP]
refine ⟨fun a b c hbc => ?_⟩
[GOAL]
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a b c : WithZero α
hbc : b ≤ c
⊢ a + b ≤ a + c
[PROOFSTEP]
induction a using WithZero.recZeroCoe
[GOAL]
case h₁
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
⊢ 0 + b ≤ 0 + c
[PROOFSTEP]
rwa [zero_add, zero_add]
[GOAL]
case h₂
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
b c : WithZero α
hbc : b ≤ c
a✝ : α
⊢ ↑a✝ + b ≤ ↑a✝ + c
[PROOFSTEP]
induction b using WithZero.recZeroCoe
[GOAL]
case h₂.h₁
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ + 0 ≤ ↑a✝ + c
[PROOFSTEP]
rw [add_zero]
[GOAL]
case h₂.h₁
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ ≤ ↑a✝ + c
[PROOFSTEP]
induction c using WithZero.recZeroCoe
[GOAL]
case h₂.h₁.h₁
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a✝ : α
hbc : 0 ≤ 0
⊢ ↑a✝ ≤ ↑a✝ + 0
[PROOFSTEP]
rw [add_zero]
[GOAL]
case h₂.h₁.h₂
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ : α
hbc : 0 ≤ ↑a✝
⊢ ↑a✝¹ ≤ ↑a✝¹ + ↑a✝
[PROOFSTEP]
rw [← coe_add, coe_le_coe]
[GOAL]
case h₂.h₁.h₂
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ : α
hbc : 0 ≤ ↑a✝
⊢ a✝¹ ≤ a✝¹ + a✝
[PROOFSTEP]
exact le_add_of_nonneg_right (h _)
[GOAL]
case h₂.h₂
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
c : WithZero α
a✝¹ a✝ : α
hbc : ↑a✝ ≤ c
⊢ ↑a✝¹ + ↑a✝ ≤ ↑a✝¹ + c
[PROOFSTEP]
rcases WithBot.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
[GOAL]
case h₂.h₂.intro.intro
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑a✝¹ + ↑a✝ ≤ ↑a✝¹ + ↑c
[PROOFSTEP]
refine le_trans ?_ (le_of_eq <| coe_add _ _)
[GOAL]
case h₂.h₂.intro.intro
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ ↑a✝¹ + ↑a✝ ≤ ↑(a✝¹ + c)
[PROOFSTEP]
rw [← coe_add, coe_le_coe]
[GOAL]
case h₂.h₂.intro.intro
α : Type u
inst✝² : AddZeroClass α
inst✝¹ : Preorder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
h : ∀ (a : α), 0 ≤ a
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ a✝¹ + a✝ ≤ a✝¹ + c
[PROOFSTEP]
exact add_le_add_left hbc' _
[GOAL]
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
a b : WithZero α
⊢ a ≤ b → ∃ c, b = a + c
[PROOFSTEP]
induction a using WithZero.cases_on
[GOAL]
case a
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
b : WithZero α
⊢ 0 ≤ b → ∃ c, b = 0 + c
[PROOFSTEP]
exact fun _ => ⟨b, (zero_add b).symm⟩
[GOAL]
case a
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
b : WithZero α
a✝ : α
⊢ ↑a✝ ≤ b → ∃ c, b = ↑a✝ + c
[PROOFSTEP]
induction b using WithZero.cases_on
[GOAL]
case a.a
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
a✝ : α
⊢ ↑a✝ ≤ 0 → ∃ c, 0 = ↑a✝ + c
[PROOFSTEP]
exact fun h => (WithBot.not_coe_le_bot _ h).elim
[GOAL]
case a.a
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ∃ c, ↑a✝ = ↑a✝¹ + c
[PROOFSTEP]
intro h
[GOAL]
case a.a
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
a✝¹ a✝ : α
h : ↑a✝¹ ≤ ↑a✝
⊢ ∃ c, ↑a✝ = ↑a✝¹ + c
[PROOFSTEP]
obtain ⟨c, rfl⟩ := exists_add_of_le (WithZero.coe_le_coe.1 h)
[GOAL]
case a.a.intro
α : Type u
inst✝² : Add α
inst✝¹ : Preorder α
inst✝ : ExistsAddOfLE α
a✝ c : α
h : ↑a✝ ≤ ↑(a✝ + c)
⊢ ∃ c_1, ↑(a✝ + c) = ↑a✝ + c_1
[PROOFSTEP]
exact ⟨c, rfl⟩
[GOAL]
α : Type u
inst✝ : CanonicallyOrderedAddMonoid α
src✝² : OrderBot (WithZero α) := orderBot
src✝¹ : OrderedAddCommMonoid (WithZero α) := WithZero.orderedAddCommMonoid (_ : ∀ (a : α), 0 ≤ a)
src✝ : ExistsAddOfLE (WithZero α) := existsAddOfLE
a b : WithZero α
⊢ a ≤ a + b
[PROOFSTEP]
induction a using WithZero.cases_on
[GOAL]
case a
α : Type u
inst✝ : CanonicallyOrderedAddMonoid α
src✝² : OrderBot (WithZero α) := orderBot
src✝¹ : OrderedAddCommMonoid (WithZero α) := WithZero.orderedAddCommMonoid (_ : ∀ (a : α), 0 ≤ a)
src✝ : ExistsAddOfLE (WithZero α) := existsAddOfLE
b : WithZero α
⊢ 0 ≤ 0 + b
[PROOFSTEP]
exact bot_le
[GOAL]
case a
α : Type u
inst✝ : CanonicallyOrderedAddMonoid α
src✝² : OrderBot (WithZero α) := orderBot
src✝¹ : OrderedAddCommMonoid (WithZero α) := WithZero.orderedAddCommMonoid (_ : ∀ (a : α), 0 ≤ a)
src✝ : ExistsAddOfLE (WithZero α) := existsAddOfLE
b : WithZero α
a✝ : α
⊢ ↑a✝ ≤ ↑a✝ + b
[PROOFSTEP]
induction b using WithZero.cases_on
[GOAL]
case a.a
α : Type u
inst✝ : CanonicallyOrderedAddMonoid α
src✝² : OrderBot (WithZero α) := orderBot
src✝¹ : OrderedAddCommMonoid (WithZero α) := WithZero.orderedAddCommMonoid (_ : ∀ (a : α), 0 ≤ a)
src✝ : ExistsAddOfLE (WithZero α) := existsAddOfLE
a✝ : α
⊢ ↑a✝ ≤ ↑a✝ + 0
[PROOFSTEP]
exact le_rfl
[GOAL]
case a.a
α : Type u
inst✝ : CanonicallyOrderedAddMonoid α
src✝² : OrderBot (WithZero α) := orderBot
src✝¹ : OrderedAddCommMonoid (WithZero α) := WithZero.orderedAddCommMonoid (_ : ∀ (a : α), 0 ≤ a)
src✝ : ExistsAddOfLE (WithZero α) := existsAddOfLE
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝¹ + ↑a✝
[PROOFSTEP]
exact WithZero.coe_le_coe.2 le_self_add
