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 α
x y : WithTop α
top : y ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ y
⊢ y ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) x y
have coe : ∀ (a : α), y ≤ 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 α
⊢ y ≤ 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) ⊤ ⊤)
⊢ y ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ y
have top₁ : ∀ (a : α), (↑a : 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 : α
⊢ y ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) y
have coe : LE.le (α := 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 : LE.le (α := WithTop α) ⊤ (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) ⊤)
⊢ y ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) y
have coe₁ : ∀ (a : α), (↑a : 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 z : WithTop α
⊢ x ≤ z → y ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) x y ≤ z
have top : ⊤ ≤ z → y ≤ z → WithTop.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 : SemilatticeSup α
x y z : WithTop α
top : ⊤ ≤ z → y ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ y ≤ z
⊢ x ≤ z → y ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) x y ≤ z
have coe : ∀ (a : α), (↑a : WithTop α) ≤ z → y ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a : WithTop α) 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 : SemilatticeSup α
y z : WithTop α
⊢ ⊤ ≤ z → y ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ y ≤ z
have top : ⊤ ≤ z → ⊤ ≤ z → WithTop.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 : SemilatticeSup α
y z : WithTop α
top : ⊤ ≤ z → ⊤ ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤ ≤ z
⊢ ⊤ ≤ z → y ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ y ≤ z
have top₁ : ∀ (a : α), ⊤ ≤ z → (↑a : WithTop α) ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑a : WithTop α) ≤ 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 : SemilatticeSup α
y z : WithTop α
a_1 : α
⊢ (↑a_1 : WithTop α) ≤ z → y ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) y ≤ z
have coe : (↑a_1 : WithTop α) ≤ z → ⊤ ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) ⊤ ≤ 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 : SemilatticeSup α
y z : WithTop α
a_1 : α
coe : (↑a_1 : WithTop α) ≤ z → ⊤ ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) ⊤ ≤ z
⊢ (↑a_1 : WithTop α) ≤ z → y ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) y ≤ z
have coe₁ : ∀ (a : α),
  (↑a_1 : WithTop α) ≤ z →
    (↑a : WithTop α) ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) (↑a : WithTop α) ≤ 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 : SemilatticeSup α
z : WithTop α
⊢ ⊤ ≤ z → ⊤ ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤ ≤ z
have top : LE.le.{u_1} (α := WithTop α) ⊤ ⊤ →
  LE.le.{u_1} (α := WithTop α) ⊤ ⊤ → LE.le.{u_1} (α := WithTop α) (WithTop.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 : SemilatticeSup α
z : WithTop α
top :
  LE.le.{u_1} (α := WithTop α) ⊤ ⊤ →
    LE.le.{u_1} (α := WithTop α) ⊤ ⊤ → LE.le.{u_1} (α := WithTop α) (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤) ⊤
⊢ ⊤ ≤ z → ⊤ ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤ ≤ z
have top₁ : ∀ (a : α), ⊤ ≤ (↑a : WithTop α) → ⊤ ≤ (↑a : WithTop α) → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤ ≤ (↑a : 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 : SemilatticeSup α
z : WithTop α
a_1 : α
⊢ ⊤ ≤ z → (↑a_1 : WithTop α) ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑a_1 : WithTop α) ≤ z
have top : LE.le.{u_1} (α := WithTop α) ⊤ ⊤ →
  (↑a_1 : WithTop α) ≤ ⊤ → LE.le (α := WithTop α) (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑a_1 : 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 : SemilatticeSup α
z : WithTop α
a_1 : α
top :
  LE.le.{u_1} (α := WithTop α) ⊤ ⊤ →
    (↑a_1 : WithTop α) ≤ ⊤ → LE.le (α := WithTop α) (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑a_1 : WithTop α)) ⊤
⊢ ⊤ ≤ z → (↑a_1 : WithTop α) ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑a_1 : WithTop α) ≤ z
have top₁ : ∀ (a : α),
  ⊤ ≤ (↑a : WithTop α) →
    (↑a_1 : WithTop α) ≤ (↑a : WithTop α) →
      WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑a_1 : WithTop α) ≤ (↑a : 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 : SemilatticeSup α
z : WithTop α
a_1 : α
⊢ (↑a_1 : WithTop α) ≤ z → ⊤ ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) ⊤ ≤ z
have coe : (↑a_1 : WithTop α) ≤ ⊤ →
  LE.le.{u_1} (α := WithTop α) ⊤ ⊤ →
    LE.le (α := WithTop α) (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : 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 : SemilatticeSup α
z : WithTop α
a_1 : α
coe :
  (↑a_1 : WithTop α) ≤ ⊤ →
    LE.le.{u_1} (α := WithTop α) ⊤ ⊤ →
      LE.le (α := WithTop α) (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) ⊤) ⊤
⊢ (↑a_1 : WithTop α) ≤ z → ⊤ ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) ⊤ ≤ z
have coe₁ : ∀ (a : α),
  (↑a_1 : WithTop α) ≤ (↑a : WithTop α) →
    ⊤ ≤ (↑a : WithTop α) → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) ⊤ ≤ (↑a : 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 : SemilatticeSup α
z : WithTop α
a_1 a_2 : α
⊢ (↑a_1 : WithTop α) ≤ z →
    (↑a_2 : WithTop α) ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α) ≤ z
have coe : (↑a_1 : WithTop α) ≤ ⊤ →
  (↑a_2 : WithTop α) ≤ ⊤ →
    LE.le (α := WithTop α) (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) (↑a_2 : 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 : SemilatticeSup α
z : WithTop α
a_1 a_2 : α
coe :
  (↑a_1 : WithTop α) ≤ ⊤ →
    (↑a_2 : WithTop α) ≤ ⊤ →
      LE.le (α := WithTop α) (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α)) ⊤
⊢ (↑a_1 : WithTop α) ≤ z →
    (↑a_2 : WithTop α) ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α) ≤ z
have coe₁ : ∀ (a : α),
  (↑a_1 : WithTop α) ≤ (↑a : WithTop α) →
    (↑a_2 : WithTop α) ≤ (↑a : WithTop α) →
      WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α) ≤ (↑a : 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 : SemilatticeSup α
a_1 a_2 a_3 : α
⊢ (↑a_1 : WithTop α) ≤ (↑a_3 : WithTop α) →
    (↑a_2 : WithTop α) ≤ (↑a_3 : WithTop α) →
      WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α) ≤ (↑a_3 : WithTop α)
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 : DistribLattice α
x y z : WithBot α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
have bot : (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ 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 : DistribLattice α
x y z : WithBot α
bot : (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
have coe : ∀ (a : α), ((↑a : WithBot α) ⊔ y) ⊓ ((↑a : WithBot α) ⊔ z) ≤ (↑a : WithBot α) ⊔ 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 : DistribLattice α
y z : WithBot α
⊢ (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z
have bot : (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ⊥ ⊓ 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 : DistribLattice α
y z : WithBot α
bot : (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ⊥ ⊓ z
⊢ (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z
have bot₁ : ∀ (a : α), (⊥ ⊔ (↑a : WithBot α)) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ (↑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 : DistribLattice α
y z : WithBot α
a_1 : α
⊢ ((↑a_1 : WithBot α) ⊔ y) ⊓ ((↑a_1 : WithBot α) ⊔ z) ≤ (↑a_1 : WithBot α) ⊔ y ⊓ z
have coe : ((↑a_1 : WithBot α) ⊔ ⊥) ⊓ ((↑a_1 : WithBot α) ⊔ z) ≤ (↑a_1 : 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 : DistribLattice α
y z : WithBot α
a_1 : α
coe : ((↑a_1 : WithBot α) ⊔ ⊥) ⊓ ((↑a_1 : WithBot α) ⊔ z) ≤ (↑a_1 : WithBot α) ⊔ ⊥ ⊓ z
⊢ ((↑a_1 : WithBot α) ⊔ y) ⊓ ((↑a_1 : WithBot α) ⊔ z) ≤ (↑a_1 : WithBot α) ⊔ y ⊓ z
have coe₁ : ∀ (a : α),
  ((↑a_1 : WithBot α) ⊔ (↑a : WithBot α)) ⊓ ((↑a_1 : WithBot α) ⊔ z) ≤ (↑a_1 : WithBot α) ⊔ (↑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 : DistribLattice α
z : WithBot α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ⊥ ⊓ z
have bot : LE.le.{u_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 : DistribLattice α
z : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ((⊥ ⊔ ⊥) ⊓ (⊥ ⊔ ⊥)) (⊥ ⊔ ⊥ ⊓ ⊥)
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ⊥ ⊓ z
have bot₁ : ∀ (a : α), (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ (↑a : 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 : DistribLattice α
z : WithBot α
a_1 : α
⊢ (⊥ ⊔ (↑a_1 : WithBot α)) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ (↑a_1 : WithBot α) ⊓ z
have bot : (⊥ ⊔ (↑a_1 : WithBot α)) ⊓ (⊥ ⊔ ⊥) ≤ ⊥ ⊔ (↑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 : DistribLattice α
z : WithBot α
a_1 : α
bot : (⊥ ⊔ (↑a_1 : WithBot α)) ⊓ (⊥ ⊔ ⊥) ≤ ⊥ ⊔ (↑a_1 : WithBot α) ⊓ ⊥
⊢ (⊥ ⊔ (↑a_1 : WithBot α)) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ (↑a_1 : WithBot α) ⊓ z
have bot₁ : ∀ (a : α), (⊥ ⊔ (↑a_1 : WithBot α)) ⊓ (⊥ ⊔ (↑a : WithBot α)) ≤ ⊥ ⊔ (↑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 : DistribLattice α
z : WithBot α
a_1 : α
⊢ ((↑a_1 : WithBot α) ⊔ ⊥) ⊓ ((↑a_1 : WithBot α) ⊔ z) ≤ (↑a_1 : WithBot α) ⊔ ⊥ ⊓ z
have coe : ((↑a_1 : WithBot α) ⊔ ⊥) ⊓ ((↑a_1 : WithBot α) ⊔ ⊥) ≤ (↑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 : DistribLattice α
z : WithBot α
a_1 : α
coe : ((↑a_1 : WithBot α) ⊔ ⊥) ⊓ ((↑a_1 : WithBot α) ⊔ ⊥) ≤ (↑a_1 : WithBot α) ⊔ ⊥ ⊓ ⊥
⊢ ((↑a_1 : WithBot α) ⊔ ⊥) ⊓ ((↑a_1 : WithBot α) ⊔ z) ≤ (↑a_1 : WithBot α) ⊔ ⊥ ⊓ z
have coe₁ : ∀ (a : α),
  ((↑a_1 : WithBot α) ⊔ ⊥) ⊓ ((↑a_1 : WithBot α) ⊔ (↑a : WithBot α)) ≤ (↑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 : DistribLattice α
z : WithBot α
a_1 a_2 : α
⊢ ((↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α)) ⊓ ((↑a_1 : WithBot α) ⊔ z) ≤ (↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α) ⊓ z
have coe : ((↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α)) ⊓ ((↑a_1 : WithBot α) ⊔ ⊥) ≤ (↑a_1 : WithBot α) ⊔ (↑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 : DistribLattice α
z : WithBot α
a_1 a_2 : α
coe : ((↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α)) ⊓ ((↑a_1 : WithBot α) ⊔ ⊥) ≤ (↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α) ⊓ ⊥
⊢ ((↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α)) ⊓ ((↑a_1 : WithBot α) ⊔ z) ≤ (↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α) ⊓ z
have coe₁ : ∀ (a : α),
  ((↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α)) ⊓ ((↑a_1 : WithBot α) ⊔ (↑a : WithBot α)) ≤
    (↑a_1 : WithBot α) ⊔ (↑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 : DistribLattice α
a_1 a_2 a_3 : α
⊢ ((↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α)) ⊓ ((↑a_1 : WithBot α) ⊔ (↑a_3 : WithBot α)) ≤
    (↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α) ⊓ (↑a_3 : WithBot α)
have coe : (a_1 ⊔ a_2) ⊓ (a_1 ⊔ a_3) ≤ a_1 ⊔ a_2 ⊓ a_3
Tactic: simp [← coe_inf, ← coe_sup]
-- 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 : DistribLattice α
x y z : WithTop α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
have top : (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ 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 : DistribLattice α
x y z : WithTop α
top : (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
have coe : ∀ (a : α), ((↑a : WithTop α) ⊔ y) ⊓ ((↑a : WithTop α) ⊔ z) ≤ (↑a : WithTop α) ⊔ 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 : DistribLattice α
y z : WithTop α
⊢ (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z
have top : (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ⊤ ⊓ 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 : DistribLattice α
y z : WithTop α
top : (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ⊤ ⊓ z
⊢ (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z
have top₁ : ∀ (a : α), (⊤ ⊔ (↑a : WithTop α)) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ (↑a : WithTop α) ⊓ 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 : DistribLattice α
y z : WithTop α
a_1 : α
⊢ ((↑a_1 : WithTop α) ⊔ y) ⊓ ((↑a_1 : WithTop α) ⊔ z) ≤ (↑a_1 : WithTop α) ⊔ y ⊓ z
have coe : ((↑a_1 : WithTop α) ⊔ ⊤) ⊓ ((↑a_1 : WithTop α) ⊔ z) ≤ (↑a_1 : WithTop α) ⊔ ⊤ ⊓ 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 : DistribLattice α
y z : WithTop α
a_1 : α
coe : ((↑a_1 : WithTop α) ⊔ ⊤) ⊓ ((↑a_1 : WithTop α) ⊔ z) ≤ (↑a_1 : WithTop α) ⊔ ⊤ ⊓ z
⊢ ((↑a_1 : WithTop α) ⊔ y) ⊓ ((↑a_1 : WithTop α) ⊔ z) ≤ (↑a_1 : WithTop α) ⊔ y ⊓ z
have coe₁ : ∀ (a : α),
  ((↑a_1 : WithTop α) ⊔ (↑a : WithTop α)) ⊓ ((↑a_1 : WithTop α) ⊔ z) ≤ (↑a_1 : WithTop α) ⊔ (↑a : WithTop α) ⊓ 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 : DistribLattice α
z : WithTop α
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ⊤ ⊓ z
have top : LE.le.{u_1} (α := 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 : DistribLattice α
z : WithTop α
top : LE.le.{u_1} (α := WithTop α) ((⊤ ⊔ ⊤) ⊓ (⊤ ⊔ ⊤)) (⊤ ⊔ ⊤ ⊓ ⊤)
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ⊤ ⊓ z
have top₁ : ∀ (a : α), (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ (↑a : WithTop α)) ≤ ⊤ ⊔ ⊤ ⊓ (↑a : 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 : DistribLattice α
z : WithTop α
a_1 : α
⊢ (⊤ ⊔ (↑a_1 : WithTop α)) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ (↑a_1 : WithTop α) ⊓ z
have top : (⊤ ⊔ (↑a_1 : WithTop α)) ⊓ (⊤ ⊔ ⊤) ≤ ⊤ ⊔ (↑a_1 : 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 : DistribLattice α
z : WithTop α
a_1 : α
top : (⊤ ⊔ (↑a_1 : WithTop α)) ⊓ (⊤ ⊔ ⊤) ≤ ⊤ ⊔ (↑a_1 : WithTop α) ⊓ ⊤
⊢ (⊤ ⊔ (↑a_1 : WithTop α)) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ (↑a_1 : WithTop α) ⊓ z
have top₁ : ∀ (a : α), (⊤ ⊔ (↑a_1 : WithTop α)) ⊓ (⊤ ⊔ (↑a : WithTop α)) ≤ ⊤ ⊔ (↑a_1 : WithTop α) ⊓ (↑a : 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 : DistribLattice α
z : WithTop α
a_1 : α
⊢ ((↑a_1 : WithTop α) ⊔ ⊤) ⊓ ((↑a_1 : WithTop α) ⊔ z) ≤ (↑a_1 : WithTop α) ⊔ ⊤ ⊓ z
have coe : ((↑a_1 : WithTop α) ⊔ ⊤) ⊓ ((↑a_1 : WithTop α) ⊔ ⊤) ≤ (↑a_1 : 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 : DistribLattice α
z : WithTop α
a_1 : α
coe : ((↑a_1 : WithTop α) ⊔ ⊤) ⊓ ((↑a_1 : WithTop α) ⊔ ⊤) ≤ (↑a_1 : WithTop α) ⊔ ⊤ ⊓ ⊤
⊢ ((↑a_1 : WithTop α) ⊔ ⊤) ⊓ ((↑a_1 : WithTop α) ⊔ z) ≤ (↑a_1 : WithTop α) ⊔ ⊤ ⊓ z
have coe₁ : ∀ (a : α),
  ((↑a_1 : WithTop α) ⊔ ⊤) ⊓ ((↑a_1 : WithTop α) ⊔ (↑a : WithTop α)) ≤ (↑a_1 : WithTop α) ⊔ ⊤ ⊓ (↑a : 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 : DistribLattice α
z : WithTop α
a_1 a_2 : α
⊢ ((↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α)) ⊓ ((↑a_1 : WithTop α) ⊔ z) ≤ (↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α) ⊓ z
have coe : ((↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α)) ⊓ ((↑a_1 : WithTop α) ⊔ ⊤) ≤ (↑a_1 : WithTop α) ⊔ (↑a_2 : 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 : DistribLattice α
z : WithTop α
a_1 a_2 : α
coe : ((↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α)) ⊓ ((↑a_1 : WithTop α) ⊔ ⊤) ≤ (↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α) ⊓ ⊤
⊢ ((↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α)) ⊓ ((↑a_1 : WithTop α) ⊔ z) ≤ (↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α) ⊓ z
have coe₁ : ∀ (a : α),
  ((↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α)) ⊓ ((↑a_1 : WithTop α) ⊔ (↑a : WithTop α)) ≤
    (↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α) ⊓ (↑a : 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 : DistribLattice α
a_1 a_2 a_3 : α
⊢ ((↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α)) ⊓ ((↑a_1 : WithTop α) ⊔ (↑a_3 : WithTop α)) ≤
    (↑a_1 : WithTop α) ⊔ (↑a_2 : WithTop α) ⊓ (↑a_3 : WithTop α)
have coe : (a_1 ⊔ a_2) ⊓ (a_1 ⊔ a_3) ≤ a_1 ⊔ a_2 ⊓ a_3
Tactic: simp [← WithTop.coe_inf, ← WithTop.coe_sup]
-- 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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : WithBot α
⊢ x ≤ y ∨ y ≤ x
have bot : ⊥ ≤ 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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : WithBot α
bot : ⊥ ≤ y ∨ y ≤ ⊥
⊢ x ≤ y ∨ y ≤ x
have coe : ∀ (a : α), (↑a : WithBot α) ≤ y ∨ 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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithBot α
⊢ ⊥ ≤ y ∨ y ≤ ⊥
have bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ ∨ LE.le.{u_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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ ∨ LE.le.{u_1} (α := WithBot α) ⊥ ⊥
⊢ ⊥ ≤ y ∨ y ≤ ⊥
have bot₁ : ∀ (a : α), ⊥ ≤ (↑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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithBot α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ y ∨ y ≤ (↑a_1 : WithBot α)
have coe : (↑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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
y : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) ≤ ⊥ ∨ ⊥ ≤ (↑a_1 : WithBot α)
⊢ (↑a_1 : WithBot α) ≤ y ∨ y ≤ (↑a_1 : WithBot α)
have coe₁ : ∀ (a : α), (↑a_1 : WithBot α) ≤ (↑a : 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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
a_1 a_2 : α
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) ∨ (↑a_2 : WithBot α) ≤ (↑a_1 : WithBot α)
have coe : a_1 ≤ a_2 ∨ a_2 ≤ a_1
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 : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : WithTop α
⊢ x ≤ y ∨ y ≤ x
have top : ⊤ ≤ y ∨ y ≤ ⊤
Tactic: cases x
Cleared hypotheses: x