awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : WithBot α
a_1 : α
⊢ (↑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
have 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 α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
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 α)
⊢ (↑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
have 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 α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : WithBot α
a_1 a_2 : α
⊢ (↑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
have 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 α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
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 α)
⊢ (↑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
have 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 α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
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 : 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 α)
have coe : a_1 ≤ a_3 → a_2 ≤ a_3 → a_1 ≤ a_3 ∧ a_2 ≤ a_3
Tactic: simp
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
x y : 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
have 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 α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
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 α)
⊢ (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
have 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 α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
y : 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 α)
have 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 α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
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 α)
⊢ 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 α)
have 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 α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
y : WithTop α
a_1 : α
⊢ (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 α)
have 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 α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
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 α)
⊢ (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 α)
have 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 α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
x y : 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 α)) ≤
    y
have 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
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
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
⊢ (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
have 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
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
y : 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
have 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 α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
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 α)
⊢ (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
have 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 α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
y : WithTop α
a_1 : α
⊢ (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
have 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 α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
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 α)
⊢ (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
have 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 α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
x y z : 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 α)
have 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 α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
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 α)
⊢ 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 α)
have 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 α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
y z : 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 α)
have 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 α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
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 α)
⊢ ⊤ ≤ 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 α)
have 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 α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
y z : WithTop α
a_1 : α
⊢ (↑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 α)
have 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 α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
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 α)
⊢ (↑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 α)
have 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 α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
z : 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 α)
have 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 α)
Tactic: cases z
Cleared hypotheses: z