mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

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

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

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

Tactic:
<;>

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

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

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

case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝ ≤
    match ↑a✝¹, ↑a✝ with
    | none, none => 0
    | some a, none => ↑a
    | none, some b => ↑b
    | some a, some b => ↑(a ⊔ b)
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

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

Tactic:
<;>

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

case coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
y z : WithZero α
a✝ : α
⊢ ↑a✝ ≤ z →
    y ≤ z →
      (match ↑a✝, y with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        z
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ⊥ ≤ ⊥

pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ↑a✝ ≤ ↑a✝

pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝ ⊥ ≤ ⊥

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝ ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ↑a✝ ≤ ↑a✝

case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝ ⊥ ≤ ⊥

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝ ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y z : WithBot α
⊢ ⊥ ≤ y → ⊥ ≤ z → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y z : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y → ↑a✝ ≤ z → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y z : WithBot α
⊢ ⊥ ≤ y → ⊥ ≤ z → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
y z : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y → ↑a✝ ≤ z → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

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

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

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

Tactic:
<;>

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

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

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

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

Goal state before:
pp: case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
z : WithBot α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ z → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ z

pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
z : WithBot α
a✝ : α
⊢ ⊥ ≤ ↑a✝ → ⊥ ≤ z → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) z

pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
z : WithBot α
a✝ : α
⊢ ↑a✝ ≤ ⊥ → ↑a✝ ≤ z → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ z

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
z : WithBot α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ z → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) z

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
z : WithBot α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ z → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ z

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
z : WithBot α
a✝ : α
⊢ ⊥ ≤ ↑a✝ → ⊥ ≤ z → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) z

case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
z : WithBot α
a✝ : α
⊢ ↑a✝ ≤ ⊥ → ↑a✝ ≤ z → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ z

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
z : WithBot α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ z → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) z
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ⊥ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ⊥

pp: case bot.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ↑a✝ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ↑a✝

pp: case bot.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ⊥ ≤ ↑a✝ → ⊥ ≤ ⊥ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝ ⊥

pp: case bot.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ⊥ ≤ ↑a✝¹ → ⊥ ≤ ↑a✝ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝

pp: case coe.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ↑a✝ ≤ ⊥ → ↑a✝ ≤ ⊥ → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ⊥

pp: case coe.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ⊥ → ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ↑a✝

pp: case coe.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ ⊥ → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝ ⊥

pp: case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝¹ → ↑a✝² ≤ ↑a✝ → ↑a✝² ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝

Tactic:
<;>

Goal state after:
case bot.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ⊥ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ⊥

case bot.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ↑a✝ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ↑a✝

case bot.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ⊥ ≤ ↑a✝ → ⊥ ≤ ⊥ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝ ⊥

case bot.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ⊥ ≤ ↑a✝¹ → ⊥ ≤ ↑a✝ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝

case coe.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ↑a✝ ≤ ⊥ → ↑a✝ ≤ ⊥ → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ⊥

case coe.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ⊥ → ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ↑a✝

case coe.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ ⊥ → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝ ⊥

case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝¹ → ↑a✝² ≤ ↑a✝ → ↑a✝² ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 y ≤ 0

pp: case coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y : WithZero α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) y ≤ ↑a✝

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 y ≤ 0

case coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y : WithZero α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithTop α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ y

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithTop α
a✝ : α
⊢ ↑a✝ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) (↑a✝) y

Tactic:
<;>

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithTop α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ y

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithTop α
a✝ : α
⊢ ↑a✝ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) (↑a✝) y
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤

pp: case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝

pp: case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝ ⊤

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ↑a✝

Tactic:
<;>

Goal state after:
case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝

case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝ ⊤

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ↑a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0 ≤ 0

pp: case zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝ ≤ 0

pp: case coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0 ≤ ↑a✝

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝ ≤ ↑a✝¹

Tactic:
<;>

Goal state after:
case zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0 ≤ 0

case zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝ ≤ 0

case coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0 ≤ ↑a✝

case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithTop α
⊢ y ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ y

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithTop α
a✝ : α
⊢ y ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) (↑a✝) y

Tactic:
<;>

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithTop α
⊢ y ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ y

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y : WithTop α
a✝ : α
⊢ y ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) (↑a✝) y
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 y ≤ y

pp: case coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y : WithZero α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) y ≤ y

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y : WithZero α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 y ≤ y

case coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y : WithZero α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) y ≤ y
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤

pp: case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝

pp: case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝ ⊤

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ↑a✝

Tactic:
<;>

Goal state after:
case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝

case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊤ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝ ⊤

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝ ≤ WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ↑a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0 ≤ 0

pp: case zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝ ≤ ↑a✝

pp: case coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0 ≤ 0

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝ ≤ ↑a✝

Tactic:
<;>

Goal state after:
case zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0 ≤ 0

case zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝ ≤ ↑a✝

case coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0 ≤ 0

case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝ ≤ ↑a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y z : WithZero α
⊢ 0 ≤ y → 0 ≤ z → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

pp: case coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y z : WithZero α
a✝ : α
⊢ ↑a✝ ≤ y → ↑a✝ ≤ z → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y z : WithZero α
⊢ 0 ≤ y → 0 ≤ z → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

case coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
y z : WithZero α
a✝ : α
⊢ ↑a✝ ≤ y → ↑a✝ ≤ z → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
⊢ 0 ≤ 0 → 0 ≤ z → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 z

pp: case zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
a✝ : α
⊢ 0 ≤ ↑a✝ → 0 ≤ z → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) z

pp: case coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
a✝ : α
⊢ ↑a✝ ≤ 0 → ↑a✝ ≤ z → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 z

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ z → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) z

Tactic:
<;>

Goal state after:
case zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
⊢ 0 ≤ 0 → 0 ≤ z → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 z

case zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
a✝ : α
⊢ 0 ≤ ↑a✝ → 0 ≤ z → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) z

case coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
a✝ : α
⊢ ↑a✝ ≤ 0 → ↑a✝ ≤ z → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 z

case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ z → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) z
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y z : WithTop α
⊢ ⊤ ≤ z → y ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ y ≤ z

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y z : WithTop α
a✝ : α
⊢ ↑a✝ ≤ z → y ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) (↑a✝) y ≤ z

Tactic:
<;>

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y z : WithTop α
⊢ ⊤ ≤ z → y ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ y ≤ z

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
y z : WithTop α
a✝ : α
⊢ ↑a✝ ≤ z → y ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) (↑a✝) y ≤ z
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
⊢ 0 ≤ 0 → 0 ≤ 0 → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0

pp: case zero.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ 0 ≤ 0 → 0 ≤ ↑a✝ → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝

pp: case zero.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ 0 ≤ ↑a✝ → 0 ≤ 0 → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0

pp: case zero.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ 0 ≤ ↑a✝¹ → 0 ≤ ↑a✝ → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝

pp: case coe.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ ↑a✝ ≤ 0 → ↑a✝ ≤ 0 → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0

pp: case coe.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ 0 → ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝

pp: case coe.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ 0 → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0

pp: case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝¹ → ↑a✝² ≤ ↑a✝ → ↑a✝² ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝

Tactic:
<;>

Goal state after:
case zero.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
⊢ 0 ≤ 0 → 0 ≤ 0 → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0

case zero.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ 0 ≤ 0 → 0 ≤ ↑a✝ → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝

case zero.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ 0 ≤ ↑a✝ → 0 ≤ 0 → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0

case zero.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ 0 ≤ ↑a✝¹ → 0 ≤ ↑a✝ → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝

case coe.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ ↑a✝ ≤ 0 → ↑a✝ ≤ 0 → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0

case coe.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ 0 → ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝

case coe.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ 0 → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0

case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝¹ → ↑a✝² ≤ ↑a✝ → ↑a✝² ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝