Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
⊢ 0 ≤ 0 →
    0 ≤ 0 →
      (match 0, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

pp: case zero.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ 0 ≤ ↑a✝ →
    0 ≤ ↑a✝ →
      (match 0, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

pp: case zero.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ 0 ≤ 0 →
    ↑a✝ ≤ 0 →
      (match 0, ↑a✝ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

pp: case zero.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ 0 ≤ ↑a✝ →
    ↑a✝¹ ≤ ↑a✝ →
      (match 0, ↑a✝¹ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

pp: case coe.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ 0 →
    0 ≤ 0 →
      (match ↑a✝, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

pp: case coe.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ →
    0 ≤ ↑a✝ →
      (match ↑a✝¹, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

pp: case coe.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ 0 →
    ↑a✝ ≤ 0 →
      (match ↑a✝¹, ↑a✝ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

pp: case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝ →
    ↑a✝¹ ≤ ↑a✝ →
      (match ↑a✝², ↑a✝¹ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

Tactic:
<;>

Goal state after:
case zero.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
⊢ 0 ≤ 0 →
    0 ≤ 0 →
      (match 0, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

case zero.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ 0 ≤ ↑a✝ →
    0 ≤ ↑a✝ →
      (match 0, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

case zero.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ 0 ≤ 0 →
    ↑a✝ ≤ 0 →
      (match 0, ↑a✝ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

case zero.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ 0 ≤ ↑a✝ →
    ↑a✝¹ ≤ ↑a✝ →
      (match 0, ↑a✝¹ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

case coe.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ 0 →
    0 ≤ 0 →
      (match ↑a✝, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

case coe.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ →
    0 ≤ ↑a✝ →
      (match ↑a✝¹, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

case coe.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ 0 →
    ↑a✝ ≤ 0 →
      (match ↑a✝¹, ↑a✝ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝ →
    ↑a✝¹ ≤ ↑a✝ →
      (match ↑a✝², ↑a✝¹ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝