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 α
y : WithBot α
a_1 : α
coe : map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) ⊥ ≤ (↑a_1 : WithBot α)
coe₁ : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) y ≤ (↑a_1 : WithBot α)

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} (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥) ⊥

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 (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ (↑a_1 : WithBot α)) ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
a_1 : α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) ⊥ ≤ (↑a_1 : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
a_1 a_2 : α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) (↑a_2 : WithBot α) ≤ (↑a_1 : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
x y : WithBot α
bot : map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ y ≤ y
coe : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithBot α) y ≤ y
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) x y ≤ 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 : WithBot α
bot : LE.le.{u_1} (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥) ⊥
bot₁ : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ (↑a : WithBot α) ≤ (↑a : WithBot α)
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ y ≤ 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 : WithBot α
a_1 : α
coe : LE.le (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) ⊥) ⊥
coe₁ : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) (↑a : WithBot α) ≤ (↑a : WithBot α)
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) y ≤ 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 : α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ (↑a_1 : WithBot α) ≤ (↑a_1 : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
a_1 : α
⊢ LE.le (α := WithBot α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) ⊥) ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
a_1 a_2 : α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) (↑a_2 : WithBot α) ≤ (↑a_2 : WithBot α)

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

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 : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ z)
bot₁ :
  ∀ (a : α),
    ⊥ ≤ (↑a : WithBot α) → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithBot α) z)
⊢ ⊥ ≤ y → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z)

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 : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ z
coe₁ :
  ∀ (a : α),
    (↑a_1 : WithBot α) ≤ (↑a : WithBot α) →
      (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithBot α) z
⊢ (↑a_1 : WithBot α) ≤ y → (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z

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 : WithBot α
bot :
  LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le.{u_1} (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥)
bot₁ :
  ∀ (a : α),
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥ →
      ⊥ ≤ (↑a : WithBot α) → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ (↑a : WithBot α))
⊢ LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ z)

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 : WithBot α
a_1 : α
bot :
  ⊥ ≤ (↑a_1 : WithBot α) →
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) ⊥)
bot₁ :
  ∀ (a : α),
    ⊥ ≤ (↑a_1 : WithBot α) →
      ⊥ ≤ (↑a : WithBot α) →
        LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) (↑a : WithBot α))
⊢ ⊥ ≤ (↑a_1 : WithBot α) → ⊥ ≤ z → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) z)

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
z : WithBot α
a_1 : α
coe : (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥
coe₁ :
  ∀ (a : α),
    (↑a_1 : WithBot α) ≤ ⊥ →
      (↑a_1 : WithBot α) ≤ (↑a : WithBot α) → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ (↑a : WithBot α)
⊢ (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ z

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 : 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 α) ⊥
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 α)
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
    (↑a_1 : WithBot α) ≤ z → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_2 : WithBot α) z

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

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} (α := WithBot α) ⊥ ⊥ →
    ⊥ ≤ (↑a_1 : WithBot α) → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ (↑a_1 : WithBot α))

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
a_1 : α
⊢ ⊥ ≤ (↑a_1 : WithBot α) →
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥ → LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) ⊥)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
a_1 a_2 : α
⊢ ⊥ ≤ (↑a_1 : WithBot α) →
    ⊥ ≤ (↑a_2 : WithBot α) →
      LE.le (α := WithBot α) ⊥ (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithBot α) (↑a_2 : WithBot α))

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
a_1 : α
⊢ (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ ⊥

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 : WithBot α) ≤ ⊥ →
    (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) ⊥ (↑a_2 : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeInf α
a_1 a_2 : α
⊢ (↑a_1 : WithBot α) ≤ (↑a_2 : WithBot α) →
    (↑a_1 : WithBot α) ≤ ⊥ → (↑a_1 : WithBot α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_2 : WithBot α) ⊥

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : 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 : 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 α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
x y : WithTop α
top : LE.le (α := WithTop α) ⊤ (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ y)
coe : ∀ (a : α), (↑a : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a : WithTop α) y
⊢ x ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) x y

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

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithTop α
a_1 : α
coe : (↑a_1 : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) ⊤
coe₁ : ∀ (a : α), (↑a_1 : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) (↑a : WithTop α)
⊢ (↑a_1 : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : 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 : SemilatticeSup α
⊢ LE.le.{u_1} (α := WithTop α) ⊤ (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 : α
⊢ LE.le (α := WithTop α) ⊤ (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑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 : SemilatticeSup α
a_1 : α
⊢ (↑a_1 : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑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 : SemilatticeSup α
a_1 a_2 : α
⊢ (↑a_1 : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : 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 : SemilatticeSup α
x y : WithTop α
top : y ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ y
coe : ∀ (a : α), y ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a : WithTop α) y
⊢ y ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) x y

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

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y : WithTop α
a_1 : α
coe : LE.le (α := WithTop α) ⊤ (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) ⊤)
coe₁ : ∀ (a : α), (↑a : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) (↑a : WithTop α)
⊢ y ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : 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 : SemilatticeSup α
a_1 : α
⊢ (↑a_1 : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑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 : SemilatticeSup α
a_1 : α
⊢ LE.le (α := WithTop α) ⊤ (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑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 : SemilatticeSup α
a_1 a_2 : α
⊢ (↑a_2 : WithTop α) ≤ WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : 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 : SemilatticeSup α
x y z : WithTop α
top : ⊤ ≤ z → y ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ y ≤ z
coe : ∀ (a : α), (↑a : WithTop α) ≤ z → y ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a : WithTop α) y ≤ z
⊢ x ≤ z → y ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) x y ≤ z

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y z : WithTop α
top : ⊤ ≤ z → ⊤ ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤ ≤ z
top₁ : ∀ (a : α), ⊤ ≤ z → (↑a : WithTop α) ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑a : WithTop α) ≤ z
⊢ ⊤ ≤ z → y ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ y ≤ z

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
y z : WithTop α
a_1 : α
coe : (↑a_1 : WithTop α) ≤ z → ⊤ ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) ⊤ ≤ z
coe₁ :
  ∀ (a : α),
    (↑a_1 : WithTop α) ≤ z →
      (↑a : WithTop α) ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) (↑a : WithTop α) ≤ z
⊢ (↑a_1 : WithTop α) ≤ z → y ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) y ≤ z

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : WithTop α
top :
  LE.le.{u_1} (α := WithTop α) ⊤ ⊤ →
    LE.le.{u_1} (α := WithTop α) ⊤ ⊤ → LE.le.{u_1} (α := WithTop α) (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤) ⊤
top₁ :
  ∀ (a : α),
    ⊤ ≤ (↑a : WithTop α) → ⊤ ≤ (↑a : WithTop α) → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤ ≤ (↑a : WithTop α)
⊢ ⊤ ≤ z → ⊤ ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤ ≤ z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : 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 α)) ⊤
top₁ :
  ∀ (a : α),
    ⊤ ≤ (↑a : WithTop α) →
      (↑a_1 : WithTop α) ≤ (↑a : WithTop α) →
        WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑a_1 : WithTop α) ≤ (↑a : WithTop α)
⊢ ⊤ ≤ z → (↑a_1 : WithTop α) ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑a_1 : WithTop α) ≤ z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : 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 α) ⊤) ⊤
coe₁ :
  ∀ (a : α),
    (↑a_1 : WithTop α) ≤ (↑a : WithTop α) →
      ⊤ ≤ (↑a : WithTop α) → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) ⊤ ≤ (↑a : WithTop α)
⊢ (↑a_1 : WithTop α) ≤ z → ⊤ ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) ⊤ ≤ z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
z : 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 α)) ⊤
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 α)
⊢ (↑a_1 : WithTop α) ≤ z →
    (↑a_2 : WithTop α) ≤ z → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : WithTop α) (↑a_2 : WithTop α) ≤ z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
⊢ LE.le.{u_1} (α := WithTop α) ⊤ ⊤ →
    LE.le.{u_1} (α := WithTop α) ⊤ ⊤ → LE.le.{u_1} (α := WithTop α) (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤) ⊤

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : SemilatticeSup α
a_1 : α
⊢ ⊤ ≤ (↑a_1 : WithTop α) → ⊤ ≤ (↑a_1 : WithTop α) → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ ⊤ ≤ (↑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 : SemilatticeSup α
a_1 : α
⊢ LE.le.{u_1} (α := WithTop α) ⊤ ⊤ →
    (↑a_1 : WithTop α) ≤ ⊤ → LE.le (α := WithTop α) (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑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 : SemilatticeSup α
a_1 a_2 : α
⊢ ⊤ ≤ (↑a_2 : WithTop α) →
    (↑a_1 : WithTop α) ≤ (↑a_2 : WithTop α) →
      WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) ⊤ (↑a_1 : 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 : SemilatticeSup α
a_1 : α
⊢ (↑a_1 : WithTop α) ≤ ⊤ →
    LE.le.{u_1} (α := WithTop α) ⊤ ⊤ →
      LE.le (α := WithTop α) (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑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 : SemilatticeSup α
a_1 a_2 : α
⊢ (↑a_1 : WithTop α) ≤ (↑a_2 : WithTop α) →
    ⊤ ≤ (↑a_2 : WithTop α) → WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : 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 : SemilatticeSup α
a_1 a_2 : α
⊢ (↑a_1 : WithTop α) ≤ ⊤ →
    (↑a_2 : WithTop α) ≤ ⊤ →
      LE.le (α := WithTop α) (WithTop.map₂ (fun (x1 x2 : α) ↦ x1 ⊔ x2) (↑a_1 : 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 : SemilatticeSup α
a_1 a_2 a_3 : α
coe : a_1 ≤ a_3 → a_2 ≤ a_3 → a_1 ≤ a_3 ∧ a_2 ≤ a_3
⊢ (↑a_1 : 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 α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : SemilatticeSup α
a b : α
⊢ (↑(a ⊔ b) : WithBot α) = (↑a : WithBot α) ⊔ (↑b : WithBot α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : SemilatticeInf α
a b : α
⊢ (↑(a ⊓ b) : WithBot α) = (↑a : WithBot α) ⊓ (↑b : WithBot α)

Tactic:
rfl

Premises used: WithBot.some, WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Order.WithBot
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
coe : ∀ (a : α), ((↑a : WithBot α) ⊔ y) ⊓ ((↑a : WithBot α) ⊔ z) ≤ (↑a : WithBot α) ⊔ y ⊓ z
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
cases x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
y z : WithBot α
bot : (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ⊥ ⊓ z
bot₁ : ∀ (a : α), (⊥ ⊔ (↑a : WithBot α)) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ (↑a : WithBot α) ⊓ z
⊢ (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
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
coe₁ :
  ∀ (a : α),
    ((↑a_1 : WithBot α) ⊔ (↑a : WithBot α)) ⊓ ((↑a_1 : WithBot α) ⊔ z) ≤ (↑a_1 : WithBot α) ⊔ (↑a : WithBot α) ⊓ z
⊢ ((↑a_1 : WithBot α) ⊔ y) ⊓ ((↑a_1 : WithBot α) ⊔ z) ≤ (↑a_1 : WithBot α) ⊔ y ⊓ z

Tactic:
cases y
-- Module: Mathlib.Order.WithBot
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 α) ((⊥ ⊔ ⊥) ⊓ (⊥ ⊔ ⊥)) (⊥ ⊔ ⊥ ⊓ ⊥)
bot₁ : ∀ (a : α), (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ (↑a : WithBot α)) ≤ ⊥ ⊔ ⊥ ⊓ (↑a : WithBot α)
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ⊥ ⊓ z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
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 α) ⊓ ⊥
bot₁ : ∀ (a : α), (⊥ ⊔ (↑a_1 : WithBot α)) ⊓ (⊥ ⊔ (↑a : WithBot α)) ≤ ⊥ ⊔ (↑a_1 : WithBot α) ⊓ (↑a : WithBot α)
⊢ (⊥ ⊔ (↑a_1 : WithBot α)) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ (↑a_1 : WithBot α) ⊓ z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
z : WithBot α
a_1 : α
coe : ((↑a_1 : WithBot α) ⊔ ⊥) ⊓ ((↑a_1 : WithBot α) ⊔ ⊥) ≤ (↑a_1 : WithBot α) ⊔ ⊥ ⊓ ⊥
coe₁ :
  ∀ (a : α),
    ((↑a_1 : WithBot α) ⊔ ⊥) ⊓ ((↑a_1 : WithBot α) ⊔ (↑a : WithBot α)) ≤ (↑a_1 : WithBot α) ⊔ ⊥ ⊓ (↑a : WithBot α)
⊢ ((↑a_1 : WithBot α) ⊔ ⊥) ⊓ ((↑a_1 : WithBot α) ⊔ z) ≤ (↑a_1 : WithBot α) ⊔ ⊥ ⊓ z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
z : WithBot α
a_1 a_2 : α
coe : ((↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α)) ⊓ ((↑a_1 : WithBot α) ⊔ ⊥) ≤ (↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α) ⊓ ⊥
coe₁ :
  ∀ (a : α),
    ((↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α)) ⊓ ((↑a_1 : WithBot α) ⊔ (↑a : WithBot α)) ≤
      (↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α) ⊓ (↑a : WithBot α)
⊢ ((↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α)) ⊓ ((↑a_1 : WithBot α) ⊔ z) ≤ (↑a_1 : WithBot α) ⊔ (↑a_2 : WithBot α) ⊓ z

Tactic:
cases z
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
⊢ LE.le.{u_1} (α := WithBot α) ((⊥ ⊔ ⊥) ⊓ (⊥ ⊔ ⊥)) (⊥ ⊔ ⊥ ⊓ ⊥)

Tactic:
simp [← coe_inf, ← coe_sup]

Premises used: WithBot.coe_inf, WithBot.coe_sup
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 : α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ (↑a_1 : WithBot α)) ≤ ⊥ ⊔ ⊥ ⊓ (↑a_1 : WithBot α)

Tactic:
simp [← coe_inf, ← coe_sup]

Premises used: WithBot.coe_inf, WithBot.coe_sup
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 : α
⊢ (⊥ ⊔ (↑a_1 : WithBot α)) ⊓ (⊥ ⊔ ⊥) ≤ ⊥ ⊔ (↑a_1 : WithBot α) ⊓ ⊥

Tactic:
simp [← coe_inf, ← coe_sup]

Premises used: WithBot.coe_inf, WithBot.coe_sup
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : DistribLattice α
a_1 a_2 : α
⊢ (⊥ ⊔ (↑a_1 : WithBot α)) ⊓ (⊥ ⊔ (↑a_2 : WithBot α)) ≤ ⊥ ⊔ (↑a_1 : WithBot α) ⊓ (↑a_2 : WithBot α)

Tactic:
simp [← coe_inf, ← coe_sup]

Premises used: WithBot.coe_inf, WithBot.coe_sup