awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
x y : WithTop α
top :
  LE.le (α := WithTop α)
    (match (motive := WithTop α → WithTop α → WithTop α) ⊤, y with
      | none, none => ⊤
      | Option.some a, none => (↑a : WithTop α)
      | none, Option.some b => (↑b : WithTop α)
      | Option.some a, Option.some b => (↑(a ⊓ b) : WithTop α) :
      WithTop α)
    (⊤ : WithTop α)
coe :
  ∀ (a : α),
    (match (motive := WithTop α → WithTop α → WithTop α) (↑a : WithTop α), y with
      | none, none => ⊤
      | Option.some a, none => (↑a : WithTop α)
      | none, Option.some b => (↑b : WithTop α)
      | Option.some a, Option.some b => (↑(a ⊓ b) : WithTop α)) ≤
      (↑a : WithTop α)
⊢ (match (motive := WithTop α → WithTop α → WithTop α) x, y with
    | none, none => ⊤
    | Option.some a, none => (↑a : WithTop α)
    | none, Option.some b => (↑b : WithTop α)
    | Option.some a, Option.some b => (↑(a ⊓ b) : WithTop α)) ≤
    x

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

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

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

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

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

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

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

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

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

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

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

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

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
x y z : WithTop α
top :
  ⊤ ≤ y →
    ⊤ ≤ z →
      LE.le (α := WithTop α) (⊤ : WithTop α)
        (match (motive := WithTop α → WithTop α → WithTop α) y, z with
          | none, none => ⊤
          | Option.some a, none => (↑a : WithTop α)
          | none, Option.some b => (↑b : WithTop α)
          | Option.some a, Option.some b => (↑(a ⊓ b) : WithTop α) :
          WithTop α)
coe :
  ∀ (a : α),
    (↑a : WithTop α) ≤ y →
      (↑a : WithTop α) ≤ z →
        (↑a : WithTop α) ≤
          match (motive := WithTop α → WithTop α → WithTop α) y, z with
          | none, none => ⊤
          | Option.some a, none => (↑a : WithTop α)
          | none, Option.some b => (↑b : WithTop α)
          | Option.some a, Option.some b => (↑(a ⊓ b) : WithTop α)
⊢ x ≤ y →
    x ≤ z →
      x ≤
        match (motive := WithTop α → WithTop α → WithTop α) y, z with
        | none, none => ⊤
        | Option.some a, none => (↑a : WithTop α)
        | none, Option.some b => (↑b : WithTop α)
        | Option.some a, Option.some b => (↑(a ⊓ b) : WithTop α)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Tactic:
simpa using le_inf

Premises used: le_inf
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
x y : WithBot α
bot : LE.le (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ y) ⊥
coe : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithBot α) y ≤ (↑a : WithBot α)
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) x y ≤ x

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
y : WithBot α
bot : LE.le.{u_1} (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥) ⊥
bot₁ : ∀ (a : α), LE.le (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ (↑a : WithBot α)) ⊥
⊢ LE.le (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ y) ⊥

Tactic:
cases y