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 : 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 α)
⊢ 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₁ : ∀ (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 α)
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 : SemilatticeInf α
z : WithTop α
a_1 : α
⊢ ⊤ ≤ (↑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 α)
have 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 α)
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 : 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 α)
⊢ ⊤ ≤ (↑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 α)
have 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 α)
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 : SemilatticeInf α
z : WithTop α
a_1 : α
⊢ (↑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 α)
have 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 α)
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 : 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 α)
⊢ (↑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 α)
have 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 α)
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 : SemilatticeInf α
z : WithTop α
a_1 a_2 : α
⊢ (↑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 α)
have 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 α)
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 : 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 α)
⊢ (↑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 α)
have 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 α)
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 : SemilatticeInf α
a_1 a_2 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 α)
have coe : a_1 ≤ a_2 → a_1 ≤ a_3 → a_1 ≤ a_2 ∧ a_1 ≤ 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 : WithBot α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) x y ≤ x
have bot : LE.le (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ 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 : WithBot α
bot : LE.le (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ y) ⊥
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) x y ≤ x
have coe : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithBot α) y ≤ (↑a : WithBot α)
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 : WithBot α
⊢ LE.le (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ y) ⊥
have bot : LE.le.{u_1} (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥) ⊥
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 : WithBot α
bot : LE.le.{u_1} (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥) ⊥
⊢ LE.le (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ y) ⊥
have bot₁ : ∀ (a : α), LE.le (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ (↑a : WithBot α)) ⊥
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 : WithBot α
a_1 : α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) y ≤ (↑a_1 : WithBot α)
have coe : map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) ⊥ ≤ (↑a_1 : WithBot α)
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 : WithBot α
a_1 : α
coe : map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) ⊥ ≤ (↑a_1 : WithBot α)
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) y ≤ (↑a_1 : WithBot α)
have coe₁ : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
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 : WithBot α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) x y ≤ y
have bot : map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ y ≤ 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 : WithBot α
bot : map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ y ≤ y
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) x y ≤ y
have coe : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithBot α) y ≤ 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 : WithBot α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ y ≤ y
have bot : LE.le.{u_1} (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥) ⊥
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 : WithBot α
bot : LE.le.{u_1} (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥) ⊥
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ y ≤ y
have bot₁ : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ (↑a : WithBot α) ≤ (↑a : WithBot α)
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 : WithBot α
a_1 : α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) y ≤ y
have coe : LE.le (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) ⊥) ⊥
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 : WithBot α
a_1 : α
coe : LE.le (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) ⊥) ⊥
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) y ≤ y
have coe₁ : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) (↑a : WithBot α) ≤ (↑a : WithBot α)
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 : WithBot α
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z
have bot : ⊥ ≤ y → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z)
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 : WithBot α
bot : ⊥ ≤ y → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z)
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z
have coe : ∀ (a : α), (↑a : WithBot α) ≤ y → (↑a : WithBot α) ≤ z → (↑a : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z
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 : WithBot α
⊢ ⊥ ≤ y → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z)
have bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ z)
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 : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ z)
⊢ ⊥ ≤ y → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z)
have bot₁ : ∀ (a : α), ⊥ ≤ (↑a : WithBot α) → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithBot α) z)
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 : WithBot α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ y → (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z
have coe : (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ z
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 : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ z
⊢ (↑a_1 : WithBot α) ≤ y → (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z
have coe₁ : ∀ (a : α),
  (↑a_1 : WithBot α) ≤ (↑a : WithBot α) →
    (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithBot α) z
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 : WithBot α
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ z)
have bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
  LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥)
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 : SemilatticeInf α
z : WithBot α
bot :
  LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥)
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ z)
have bot₁ : ∀ (a : α),
  LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
    ⊥ ≤ (↑a : WithBot α) → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ (↑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 : SemilatticeInf α
z : WithBot α
a_1 : α
⊢ ⊥ ≤ (↑a_1 : WithBot α) → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) z)
have bot : ⊥ ≤ (↑a_1 : WithBot α) →
  LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : 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 : SemilatticeInf α
z : WithBot α
a_1 : α
bot :
  ⊥ ≤ (↑a_1 : WithBot α) →
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) ⊥)
⊢ ⊥ ≤ (↑a_1 : WithBot α) → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) z)
have bot₁ : ∀ (a : α),
  ⊥ ≤ (↑a_1 : WithBot α) →
    ⊥ ≤ (↑a : WithBot α) →
      LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : 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 : SemilatticeInf α
z : WithBot α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ z
have coe : (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥
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 : SemilatticeInf α
z : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥
⊢ (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ z
have coe₁ : ∀ (a : α),
  (↑a_1 : WithBot α) ≤ ⊥ →
    (↑a_1 : WithBot α) ≤ (↑a : WithBot α) → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ (↑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 : SemilatticeInf α
z : WithBot α
a_1 a_2 : α
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
    (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_2 : WithBot α) z
have coe : (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
  (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_2 : 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 : SemilatticeInf α
z : WithBot α
a_1 a_2 : α
coe :
  (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
    (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_2 : WithBot α) ⊥
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
    (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_2 : WithBot α) z
have coe₁ : ∀ (a : α),
  (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
    (↑a_1 : WithBot α) ≤ (↑a : WithBot α) →
      (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_2 : 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 : SemilatticeInf α
a_1 a_2 a_3 : α
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
    (↑a_1 : WithBot α) ≤ (↑a_3 : WithBot α) →
      (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_2 : WithBot α) (↑a_3 : WithBot α)
have coe : a_1 ≤ a_2 → a_1 ≤ a_3 → a_1 ≤ a_2 ∧ a_1 ≤ 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 : SemilatticeSup α
x y : WithTop α
⊢ x ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) x y
have top : LE.le (α := WithTop α) ⊤ (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ 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 : SemilatticeSup α
x y : WithTop α
top : LE.le (α := WithTop α) ⊤ (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ y)
⊢ x ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) x y
have coe : ∀ (a : α), (↑a : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a : 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 : SemilatticeSup α
y : WithTop α
⊢ LE.le (α := WithTop α) ⊤ (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ y)
have top : LE.le.{u_1} (α := WithTop α) ⊤ (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤)
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 : SemilatticeSup α
y : WithTop α
top : LE.le.{u_1} (α := WithTop α) ⊤ (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤)
⊢ LE.le (α := WithTop α) ⊤ (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ y)
have top₁ : ∀ (a : α), LE.le (α := WithTop α) ⊤ (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑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 : SemilatticeSup α
y : WithTop α
a_1 : α
⊢ (↑a_1 : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) y
have coe : (↑a_1 : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑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 : SemilatticeSup α
y : WithTop α
a_1 : α
coe : (↑a_1 : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) ⊤
⊢ (↑a_1 : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) y
have coe₁ : ∀ (a : α), (↑a_1 : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : 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 : SemilatticeSup α
x y : WithTop α
⊢ y ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) x y
have top : y ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ y
Tactic: cases x
Cleared hypotheses: x