awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : PartialOrder α
x y : WithBot α
inst_1 : NoBotOrder α
h : ∀ (a : α), (↑a : WithBot α) ≤ x ↔ (↑a : WithBot α) ≤ y
⊢ x = y

Tactic:
le_antisymm (forall_coe_le_iff_le.mp fun a ↦ (h a).1) (forall_coe_le_iff_le.mp fun a ↦ (h a).2)

Premises used: Iff.mpr, le_antisymm, Iff.mp, WithBot.forall_coe_le_iff_le
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : PartialOrder α
x y : WithBot α
inst_1 : NoBotOrder α
h : ∀ (a : α), x ≤ (↑a : WithBot α) ↔ y ≤ (↑a : WithBot α)
⊢ x = y

Tactic:
le_antisymm (forall_le_coe_iff_le.mp fun a ↦ (h a).2) (forall_le_coe_iff_le.mp fun a ↦ (h a).1)

Premises used: Iff.mpr, le_antisymm, Iff.mp, WithBot.forall_le_coe_iff_le
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
x y : WithBot α
bot :
  LE.le (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)
coe :
  ∀ (a : α),
    (↑a : WithBot α) ≤
      match (motive := WithBot α → WithBot α → WithBot α) (↑a : WithBot α), y with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
⊢ x ≤
    match (motive := WithBot α → WithBot α → WithBot α) x, y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithBot α
bot :
  LE.le.{u_1} (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)
bot₁ :
  ∀ (a : α),
    LE.le (α := WithBot α) (⊥ : WithBot α)
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a : WithBot α) with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
        WithBot α)
⊢ LE.le (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithBot α
a_1 : α
coe :
  (↑a_1 : WithBot α) ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
coe₁ :
  ∀ (a : α),
    (↑a_1 : WithBot α) ≤
      match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), (↑a : WithBot α) with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
⊢ (↑a_1 : WithBot α) ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
⊢ LE.le.{u_1} (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 : α
⊢ LE.le (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a_1 : WithBot α) with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 a_2 : α
⊢ (↑a_1 : WithBot α) ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), (↑a_2 : WithBot α) with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
x y : WithBot α
bot :
  y ≤
    match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
coe :
  ∀ (a : α),
    y ≤
      match (motive := WithBot α → WithBot α → WithBot α) (↑a : WithBot α), y with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
⊢ y ≤
    match (motive := WithBot α → WithBot α → WithBot α) x, y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithBot α
bot :
  LE.le.{u_1} (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)
bot₁ :
  ∀ (a : α),
    (↑a : WithBot α) ≤
      match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a : WithBot α) with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
⊢ y ≤
    match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithBot α
a_1 : α
coe :
  LE.le (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)
coe₁ :
  ∀ (a : α),
    (↑a : WithBot α) ≤
      match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), (↑a : WithBot α) with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)
⊢ y ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), y with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤
    match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a_1 : WithBot α) with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 : α
⊢ LE.le (α := WithBot α) (⊥ : WithBot α)
    (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
      | none, none => ⊥
      | Option.some a, none => (↑a : WithBot α)
      | none, Option.some b => (↑b : WithBot α)
      | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
      WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 a_2 : α
⊢ (↑a_2 : WithBot α) ≤
    match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), (↑a_2 : WithBot α) with
    | none, none => ⊥
    | Option.some a, none => (↑a : WithBot α)
    | none, Option.some b => (↑b : WithBot α)
    | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
x y z : WithBot α
bot :
  ⊥ ≤ z →
    y ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
coe :
  ∀ (a : α),
    (↑a : WithBot α) ≤ z →
      y ≤ z →
        (match (motive := WithBot α → WithBot α → WithBot α) (↑a : WithBot α), y with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
          z
⊢ x ≤ z →
    y ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) x, y with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y z : WithBot α
bot :
  ⊥ ≤ z →
    ⊥ ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
bot₁ :
  ∀ (a : α),
    ⊥ ≤ z →
      (↑a : WithBot α) ≤ z →
        (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a : WithBot α) with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
          z
⊢ ⊥ ≤ z →
    y ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, y with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y z : WithBot α
a_1 : α
coe :
  (↑a_1 : WithBot α) ≤ z →
    ⊥ ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z
coe₁ :
  ∀ (a : α),
    (↑a_1 : WithBot α) ≤ z →
      (↑a : WithBot α) ≤ z →
        (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), (↑a : WithBot α) with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
          z
⊢ (↑a_1 : WithBot α) ≤ z →
    y ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), y with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : WithBot α
bot :
  LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
      LE.le.{u_1} (α := WithBot α)
        (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
          WithBot α)
        (⊥ : WithBot α)
bot₁ :
  ∀ (a : α),
    ⊥ ≤ (↑a : WithBot α) →
      ⊥ ≤ (↑a : WithBot α) →
        (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
          (↑a : WithBot α)
⊢ ⊥ ≤ z →
    ⊥ ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : WithBot α
a_1 : α
bot :
  LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
    (↑a_1 : WithBot α) ≤ ⊥ →
      LE.le (α := WithBot α)
        (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a_1 : WithBot α) with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
          WithBot α)
        (⊥ : WithBot α)
bot₁ :
  ∀ (a : α),
    ⊥ ≤ (↑a : WithBot α) →
      (↑a_1 : WithBot α) ≤ (↑a : WithBot α) →
        (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a_1 : WithBot α) with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
          (↑a : WithBot α)
⊢ ⊥ ≤ z →
    (↑a_1 : WithBot α) ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a_1 : WithBot α) with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : WithBot α
a_1 : α
coe :
  (↑a_1 : WithBot α) ≤ ⊥ →
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
      LE.le (α := WithBot α)
        (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
          WithBot α)
        (⊥ : WithBot α)
coe₁ :
  ∀ (a : α),
    (↑a_1 : WithBot α) ≤ (↑a : WithBot α) →
      ⊥ ≤ (↑a : WithBot α) →
        (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
          (↑a : WithBot α)
⊢ (↑a_1 : WithBot α) ≤ z →
    ⊥ ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : WithBot α
a_1 a_2 : α
coe :
  (↑a_1 : WithBot α) ≤ ⊥ →
    (↑a_2 : WithBot α) ≤ ⊥ →
      LE.le (α := WithBot α)
        (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), (↑a_2 : WithBot α) with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
          WithBot α)
        (⊥ : WithBot α)
coe₁ :
  ∀ (a : α),
    (↑a_1 : WithBot α) ≤ (↑a : WithBot α) →
      (↑a_2 : WithBot α) ≤ (↑a : WithBot α) →
        (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), (↑a_2 : WithBot α) with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
          (↑a : WithBot α)
⊢ (↑a_1 : WithBot α) ≤ z →
    (↑a_2 : WithBot α) ≤ z →
      (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), (↑a_2 : WithBot α) with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
      LE.le.{u_1} (α := WithBot α)
        (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
          WithBot α)
        (⊥ : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 : α
⊢ ⊥ ≤ (↑a_1 : WithBot α) →
    ⊥ ≤ (↑a_1 : WithBot α) →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, ⊥ with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        (↑a_1 : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 : α
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
    (↑a_1 : WithBot α) ≤ ⊥ →
      LE.le (α := WithBot α)
        (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a_1 : WithBot α) with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
          WithBot α)
        (⊥ : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 a_2 : α
⊢ ⊥ ≤ (↑a_2 : WithBot α) →
    (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
      (match (motive := WithBot α → WithBot α → WithBot α) ⊥, (↑a_1 : WithBot α) with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        (↑a_2 : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ ⊥ →
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
      LE.le (α := WithBot α)
        (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
          WithBot α)
        (⊥ : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 a_2 : α
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
    ⊥ ≤ (↑a_2 : WithBot α) →
      (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), ⊥ with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        (↑a_2 : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 a_2 : α
⊢ (↑a_1 : WithBot α) ≤ ⊥ →
    (↑a_2 : WithBot α) ≤ ⊥ →
      LE.le (α := WithBot α)
        (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), (↑a_2 : WithBot α) with
          | none, none => ⊥
          | Option.some a, none => (↑a : WithBot α)
          | none, Option.some b => (↑b : WithBot α)
          | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α) :
          WithBot α)
        (⊥ : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 a_2 a_3 : α
coe : a_1 ≤ a_3 → a_2 ≤ a_3 → a_1 ≤ a_3 ∧ a_2 ≤ a_3
⊢ (↑a_1 : WithBot α) ≤ (↑a_3 : WithBot α) →
    (↑a_2 : WithBot α) ≤ (↑a_3 : WithBot α) →
      (match (motive := WithBot α → WithBot α → WithBot α) (↑a_1 : WithBot α), (↑a_2 : WithBot α) with
        | none, none => ⊥
        | Option.some a, none => (↑a : WithBot α)
        | none, Option.some b => (↑b : WithBot α)
        | Option.some a, Option.some b => (↑(a ⊔ b) : WithBot α)) ≤
        (↑a_3 : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 a_2 a_3 : α
⊢ a_1 ≤ a_3 → a_2 ≤ a_3 → a_1 ≤ a_3 ∧ a_2 ≤ a_3

Tactic:
simpa using sup_le

Premises used: sup_le