awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a : α
⊢ LE.le (α := WithZero α) (0 : WithZero α)
    (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
      | none, none => 0
      | some a, none => (↑a : WithZero α)
      | none, some b => (↑b : WithZero α)
      | some a, some b => (↑(a ⊔ b) : WithZero α) :
      WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a a_1 : α
⊢ (↑a_1 : WithZero α) ≤
    match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), (↑a_1 : WithZero α) with
    | none, none => 0
    | some a, none => (↑a : WithZero α)
    | none, some b => (↑b : WithZero α)
    | some a, some b => (↑(a ⊔ b) : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
x y z : WithZero α
zero :
  0 ≤ z →
    y ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) 0, y with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
coe :
  ∀ (a : α),
    (↑a : WithZero α) ≤ z →
      y ≤ z →
        (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
          z
⊢ x ≤ z →
    y ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) x, y with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y z : WithZero α
zero :
  0 ≤ z →
    0 ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
zero₁ :
  ∀ (a : α),
    0 ≤ z →
      (↑a : WithZero α) ≤ z →
        (match (motive := WithZero α → WithZero α → WithZero α) 0, (↑a : WithZero α) with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
          z
⊢ 0 ≤ z →
    y ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) 0, y with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
y z : WithZero α
a : α
coe :
  (↑a : WithZero α) ≤ z →
    0 ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithZero α) ≤ z →
      (↑a_1 : WithZero α) ≤ z →
        (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), (↑a_1 : WithZero α) with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
          z
⊢ (↑a : WithZero α) ≤ z →
    y ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), y with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
z : WithZero α
zero :
  LE.le.{u_1} (α := WithZero α) 0 0 →
    LE.le.{u_1} (α := WithZero α) 0 0 →
      LE.le.{u_1} (α := WithZero α)
        (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α) :
          WithZero α)
        (0 : WithZero α)
zero₁ :
  ∀ (a : α),
    0 ≤ (↑a : WithZero α) →
      0 ≤ (↑a : WithZero α) →
        (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
          (↑a : WithZero α)
⊢ 0 ≤ z →
    0 ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
z : WithZero α
a : α
zero :
  LE.le.{u_1} (α := WithZero α) 0 0 →
    (↑a : WithZero α) ≤ 0 →
      LE.le (α := WithZero α)
        (match (motive := WithZero α → WithZero α → WithZero α) 0, (↑a : WithZero α) with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α) :
          WithZero α)
        (0 : WithZero α)
zero₁ :
  ∀ (a_1 : α),
    0 ≤ (↑a_1 : WithZero α) →
      (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
        (match (motive := WithZero α → WithZero α → WithZero α) 0, (↑a : WithZero α) with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
          (↑a_1 : WithZero α)
⊢ 0 ≤ z →
    (↑a : WithZero α) ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) 0, (↑a : WithZero α) with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
z : WithZero α
a : α
coe :
  (↑a : WithZero α) ≤ 0 →
    LE.le.{u_1} (α := WithZero α) 0 0 →
      LE.le (α := WithZero α)
        (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α) :
          WithZero α)
        (0 : WithZero α)
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
      0 ≤ (↑a_1 : WithZero α) →
        (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
          (↑a_1 : WithZero α)
⊢ (↑a : WithZero α) ≤ z →
    0 ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
z : WithZero α
a a_1 : α
coe :
  (↑a : WithZero α) ≤ 0 →
    (↑a_1 : WithZero α) ≤ 0 →
      LE.le (α := WithZero α)
        (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), (↑a_1 : WithZero α) with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α) :
          WithZero α)
        (0 : WithZero α)
coe₁ :
  ∀ (a_2 : α),
    (↑a : WithZero α) ≤ (↑a_2 : WithZero α) →
      (↑a_1 : WithZero α) ≤ (↑a_2 : WithZero α) →
        (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), (↑a_1 : WithZero α) with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
          (↑a_2 : WithZero α)
⊢ (↑a : WithZero α) ≤ z →
    (↑a_1 : WithZero α) ≤ z →
      (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), (↑a_1 : WithZero α) with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
⊢ LE.le.{u_1} (α := WithZero α) 0 0 →
    LE.le.{u_1} (α := WithZero α) 0 0 →
      LE.le.{u_1} (α := WithZero α)
        (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α) :
          WithZero α)
        (0 : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a : α
⊢ 0 ≤ (↑a : WithZero α) →
    0 ≤ (↑a : WithZero α) →
      (match (motive := WithZero α → WithZero α → WithZero α) 0, 0 with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        (↑a : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a : α
⊢ LE.le.{u_1} (α := WithZero α) 0 0 →
    (↑a : WithZero α) ≤ 0 →
      LE.le (α := WithZero α)
        (match (motive := WithZero α → WithZero α → WithZero α) 0, (↑a : WithZero α) with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α) :
          WithZero α)
        (0 : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a a_1 : α
⊢ 0 ≤ (↑a_1 : WithZero α) →
    (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
      (match (motive := WithZero α → WithZero α → WithZero α) 0, (↑a : WithZero α) with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        (↑a_1 : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a : α
⊢ (↑a : WithZero α) ≤ 0 →
    LE.le.{u_1} (α := WithZero α) 0 0 →
      LE.le (α := WithZero α)
        (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α) :
          WithZero α)
        (0 : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a a_1 : α
⊢ (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
    0 ≤ (↑a_1 : WithZero α) →
      (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), 0 with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        (↑a_1 : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a a_1 : α
⊢ (↑a : WithZero α) ≤ 0 →
    (↑a_1 : WithZero α) ≤ 0 →
      LE.le (α := WithZero α)
        (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), (↑a_1 : WithZero α) with
          | none, none => 0
          | some a, none => (↑a : WithZero α)
          | none, some b => (↑b : WithZero α)
          | some a, some b => (↑(a ⊔ b) : WithZero α) :
          WithZero α)
        (0 : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a a_1 a_2 : α
coe : a ≤ a_2 → a_1 ≤ a_2 → a ≤ a_2 ∧ a_1 ≤ a_2
⊢ (↑a : WithZero α) ≤ (↑a_2 : WithZero α) →
    (↑a_1 : WithZero α) ≤ (↑a_2 : WithZero α) →
      (match (motive := WithZero α → WithZero α → WithZero α) (↑a : WithZero α), (↑a_1 : WithZero α) with
        | none, none => 0
        | some a, none => (↑a : WithZero α)
        | none, some b => (↑b : WithZero α)
        | some a, some b => (↑(a ⊔ b) : WithZero α)) ≤
        (↑a_2 : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
a a_1 a_2 : α
⊢ a ≤ a_2 → a_1 ≤ a_2 → a ≤ a_2 ∧ a_1 ≤ a_2

Tactic:
simpa using sup_le

Premises used: sup_le
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : SemilatticeSup α
a b : α
⊢ (↑(a ⊔ b) : WithZero α) = (↑a : WithZero α) ⊔ (↑b : WithZero α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
x y : WithZero α
zero : LE.le (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 y) 0
coe : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) y ≤ (↑a : WithZero α)
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) x y ≤ x

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
y : WithZero α
zero : LE.le.{u_1} (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0) 0
zero₁ : ∀ (a : α), LE.le (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 (↑a : WithZero α)) 0
⊢ LE.le (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 y) 0

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
y : WithZero α
a : α
coe : map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) 0 ≤ (↑a : WithZero α)
coe₁ : ∀ (a_1 : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) (↑a_1 : WithZero α) ≤ (↑a : WithZero α)
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) y ≤ (↑a : WithZero α)

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
⊢ LE.le.{u_1} (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a : α
⊢ LE.le (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 (↑a : WithZero α)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a : α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) 0 ≤ (↑a : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a a_1 : α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) (↑a_1 : WithZero α) ≤ (↑a : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
x y : WithZero α
zero : map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 y ≤ y
coe : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) y ≤ y
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) x y ≤ y

Tactic:
cases x
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
y : WithZero α
zero : LE.le.{u_1} (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0) 0
zero₁ : ∀ (a : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 (↑a : WithZero α) ≤ (↑a : WithZero α)
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 y ≤ y

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
y : WithZero α
a : α
coe : LE.le (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) 0) 0
coe₁ : ∀ (a_1 : α), map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) (↑a_1 : WithZero α) ≤ (↑a_1 : WithZero α)
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) y ≤ y

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a : α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 (↑a : WithZero α) ≤ (↑a : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a : α
⊢ LE.le (α := WithZero α) (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a a_1 : α
⊢ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) (↑a_1 : WithZero α) ≤ (↑a_1 : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
x y z : WithZero α
zero : 0 ≤ y → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z)
coe :
  ∀ (a : α), (↑a : WithZero α) ≤ y → (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ 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.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
y z : WithZero α
zero : LE.le.{u_1} (α := WithZero α) 0 0 → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 z)
zero₁ :
  ∀ (a : α),
    0 ≤ (↑a : WithZero α) → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) z)
⊢ 0 ≤ y → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z)

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
y z : WithZero α
a : α
coe : (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 z
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
      (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithZero α) z
⊢ (↑a : WithZero α) ≤ y → (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) y z

Tactic:
cases y
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
z : WithZero α
zero :
  LE.le.{u_1} (α := WithZero α) 0 0 →
    LE.le.{u_1} (α := WithZero α) 0 0 → LE.le.{u_1} (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0)
zero₁ :
  ∀ (a : α),
    LE.le.{u_1} (α := WithZero α) 0 0 →
      0 ≤ (↑a : WithZero α) → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 (↑a : WithZero α))
⊢ LE.le.{u_1} (α := WithZero α) 0 0 → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 z)

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
z : WithZero α
a : α
zero :
  0 ≤ (↑a : WithZero α) →
    LE.le.{u_1} (α := WithZero α) 0 0 → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) 0)
zero₁ :
  ∀ (a_1 : α),
    0 ≤ (↑a : WithZero α) →
      0 ≤ (↑a_1 : WithZero α) →
        LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) (↑a_1 : WithZero α))
⊢ 0 ≤ (↑a : WithZero α) → 0 ≤ z → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) z)

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
z : WithZero α
a : α
coe : (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0
coe₁ :
  ∀ (a_1 : α),
    (↑a : WithZero α) ≤ 0 →
      (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
        (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 (↑a_1 : WithZero α)
⊢ (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
z : WithZero α
a a_1 : α
coe :
  (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
    (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithZero α) 0
coe₁ :
  ∀ (a_2 : α),
    (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
      (↑a : WithZero α) ≤ (↑a_2 : WithZero α) →
        (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithZero α) (↑a_2 : WithZero α)
⊢ (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
    (↑a : WithZero α) ≤ z → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithZero α) z

Tactic:
cases z
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
⊢ LE.le.{u_1} (α := WithZero α) 0 0 →
    LE.le.{u_1} (α := WithZero α) 0 0 → LE.le.{u_1} (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a : α
⊢ LE.le.{u_1} (α := WithZero α) 0 0 →
    0 ≤ (↑a : WithZero α) → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 (↑a : WithZero α))

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a : α
⊢ 0 ≤ (↑a : WithZero α) →
    LE.le.{u_1} (α := WithZero α) 0 0 → LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a a_1 : α
⊢ 0 ≤ (↑a : WithZero α) →
    0 ≤ (↑a_1 : WithZero α) →
      LE.le (α := WithZero α) 0 (map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a : WithZero α) (↑a_1 : WithZero α))

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a : α
⊢ (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a a_1 : α
⊢ (↑a : WithZero α) ≤ 0 →
    (↑a : WithZero α) ≤ (↑a_1 : WithZero α) → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) 0 (↑a_1 : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a a_1 : α
⊢ (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
    (↑a : WithZero α) ≤ 0 → (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithZero α) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a a_1 a_2 : α
coe : a ≤ a_1 → a ≤ a_2 → a ≤ a_1 ∧ a ≤ a_2
⊢ (↑a : WithZero α) ≤ (↑a_1 : WithZero α) →
    (↑a : WithZero α) ≤ (↑a_2 : WithZero α) →
      (↑a : WithZero α) ≤ map₂ (fun (x1 x2 : α) ↦ x1 ⊓ x2) (↑a_1 : WithZero α) (↑a_2 : WithZero α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
a a_1 a_2 : α
⊢ a ≤ a_1 → a ≤ a_2 → a ≤ a_1 ∧ a ≤ a_2

Tactic:
simpa using le_inf

Premises used: le_inf
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
inst : SemilatticeInf α
a b : α
⊢ (↑(a ⊓ b) : WithZero α) = (↑a : WithZero α) ⊓ (↑b : WithZero α)

Tactic:
rfl

Premises used: WithZero.map₂, WithZero.coe, rfl, Option.map₂
-- Module: Mathlib.Algebra.Order.GroupWithZero.Canonical
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : DecidableLE α
x : WithZero α
⊢ 0 ≤ x

Tactic:
simp