mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
x y z : WithBot α
⊢ x ≤ z →
    y ≤ z →
      (match x, y with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        z

Tactic:
cases x <;> cases y <;> cases z

Goal state after:
case bot.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
⊢ ⊥ ≤ ⊥ →
    ⊥ ≤ ⊥ →
      (match ⊥, ⊥ with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        ⊥

case bot.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊥ ≤ ↑a✝ →
    ⊥ ≤ ↑a✝ →
      (match ⊥, ⊥ with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        ↑a✝

case bot.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊥ ≤ ⊥ →
    ↑a✝ ≤ ⊥ →
      (match ⊥, ↑a✝ with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        ⊥

case bot.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ⊥ ≤ ↑a✝ →
    ↑a✝¹ ≤ ↑a✝ →
      (match ⊥, ↑a✝¹ with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        ↑a✝

case coe.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ ⊥ →
    ⊥ ≤ ⊥ →
      (match ↑a✝, ⊥ with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        ⊥

case coe.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ →
    ⊥ ≤ ↑a✝ →
      (match ↑a✝¹, ⊥ with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        ↑a✝

case coe.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ⊥ →
    ↑a✝ ≤ ⊥ →
      (match ↑a✝¹, ↑a✝ with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        ⊥

case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝ →
    ↑a✝¹ ≤ ↑a✝ →
      (match ↑a✝², ↑a✝¹ with
        | none, none => ⊥
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊔ b)) ≤
        ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
x y z : WithTop α
⊢ x ≤ y →
    x ≤ z →
      x ≤
        match y, z with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)

Tactic:
cases x <;> cases y <;> cases z

Goal state after:
case top.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
⊢ ⊤ ≤ ⊤ →
    ⊤ ≤ ⊤ →
      ⊤ ≤
        match ⊤, ⊤ with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)

case top.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ⊤ ≤ ⊤ →
    ⊤ ≤ ↑a✝ →
      ⊤ ≤
        match ⊤, ↑a✝ with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)

case top.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ⊤ ≤ ↑a✝ →
    ⊤ ≤ ⊤ →
      ⊤ ≤
        match ↑a✝, ⊤ with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)

case top.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ⊤ ≤ ↑a✝¹ →
    ⊤ ≤ ↑a✝ →
      ⊤ ≤
        match ↑a✝¹, ↑a✝ with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)

case coe.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ↑a✝ ≤ ⊤ →
    ↑a✝ ≤ ⊤ →
      ↑a✝ ≤
        match ⊤, ⊤ with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)

case coe.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ⊤ →
    ↑a✝¹ ≤ ↑a✝ →
      ↑a✝¹ ≤
        match ⊤, ↑a✝ with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)

case coe.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ →
    ↑a✝¹ ≤ ⊤ →
      ↑a✝¹ ≤
        match ↑a✝, ⊤ with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)

case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝¹ →
    ↑a✝² ≤ ↑a✝ →
      ↑a✝² ≤
        match ↑a✝¹, ↑a✝ with
        | none, none => ⊤
        | Option.some a, none => ↑a
        | none, Option.some b => ↑b
        | Option.some a, Option.some b => ↑(a ⊓ b)
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
x y z : WithZero α
⊢ x ≤ z →
    y ≤ z →
      (match x, y with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        z

Tactic:
cases x <;> cases y <;> cases z

Goal state after:
case zero.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
⊢ 0 ≤ 0 →
    0 ≤ 0 →
      (match 0, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

case zero.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ 0 ≤ ↑a✝ →
    0 ≤ ↑a✝ →
      (match 0, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

case zero.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ 0 ≤ 0 →
    ↑a✝ ≤ 0 →
      (match 0, ↑a✝ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

case zero.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ 0 ≤ ↑a✝ →
    ↑a✝¹ ≤ ↑a✝ →
      (match 0, ↑a✝¹ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

case coe.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ 0 →
    0 ≤ 0 →
      (match ↑a✝, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

case coe.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ →
    0 ≤ ↑a✝ →
      (match ↑a✝¹, 0 with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝

case coe.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ 0 →
    ↑a✝ ≤ 0 →
      (match ↑a✝¹, ↑a✝ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        0

case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝ →
    ↑a✝¹ ≤ ↑a✝ →
      (match ↑a✝², ↑a✝¹ with
        | none, none => 0
        | some a, none => ↑a
        | none, some b => ↑b
        | some a, some b => ↑(a ⊔ b)) ≤
        ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : 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

Tactic:
cases x <;> cases y <;> cases z

Goal state after:
case bot.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ⊥ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ⊥

case bot.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ⊥ ≤ ⊥ → ⊥ ≤ ↑a✝ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ↑a✝

case bot.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ⊥ ≤ ↑a✝ → ⊥ ≤ ⊥ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝ ⊥

case bot.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ⊥ ≤ ↑a✝¹ → ⊥ ≤ ↑a✝ → ⊥ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝

case coe.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝ : α
⊢ ↑a✝ ≤ ⊥ → ↑a✝ ≤ ⊥ → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ⊥

case coe.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ⊥ → ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⊥ ↑a✝

case coe.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ ⊥ → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝ ⊥

case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝¹ → ↑a✝² ≤ ↑a✝ → ↑a✝² ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
x y z : WithZero α
⊢ x ≤ y → x ≤ z → x ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) y z

Tactic:
cases x <;> cases y <;> cases z

Goal state after:
case zero.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
⊢ 0 ≤ 0 → 0 ≤ 0 → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0

case zero.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ 0 ≤ 0 → 0 ≤ ↑a✝ → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝

case zero.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ 0 ≤ ↑a✝ → 0 ≤ 0 → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0

case zero.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ 0 ≤ ↑a✝¹ → 0 ≤ ↑a✝ → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝

case coe.zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝ : α
⊢ ↑a✝ ≤ 0 → ↑a✝ ≤ 0 → ↑a✝ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 0

case coe.zero.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ 0 → ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 ↑a✝

case coe.coe.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ 0 → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) 0

case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝¹ → ↑a✝² ≤ ↑a✝ → ↑a✝² ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) ↑a✝¹ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : 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

Tactic:
cases x <;> cases y <;> cases z

Goal state after:
case top.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
⊢ ⊤ ≤ ⊤ → ⊤ ≤ ⊤ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤ ≤ ⊤

case top.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊤ ≤ ↑a✝ → ⊤ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤ ≤ ↑a✝

case top.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊤ ≤ ⊤ → ↑a✝ ≤ ⊤ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝ ≤ ⊤

case top.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ⊤ ≤ ↑a✝ → ↑a✝¹ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝¹ ≤ ↑a✝

case coe.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ ⊤ → ⊤ ≤ ⊤ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝ ⊤ ≤ ⊤

case coe.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ⊤ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ⊤ ≤ ↑a✝

case coe.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ⊤ → ↑a✝ ≤ ⊤ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ↑a✝ ≤ ⊤

case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝ → ↑a✝¹ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝² ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : 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

Tactic:
cases x <;> cases y <;> cases z

Goal state after:
case bot.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ ⊥) ≤ ⊥ ⊔ ⊥ ⊓ ⊥

case bot.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ ↑a✝) ≤ ⊥ ⊔ ⊥ ⊓ ↑a✝

case bot.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊥ ⊔ ↑a✝) ⊓ (⊥ ⊔ ⊥) ≤ ⊥ ⊔ ↑a✝ ⊓ ⊥

case bot.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (⊥ ⊔ ↑a✝¹) ⊓ (⊥ ⊔ ↑a✝) ≤ ⊥ ⊔ ↑a✝¹ ⊓ ↑a✝

case coe.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (↑a✝ ⊔ ⊥) ⊓ (↑a✝ ⊔ ⊥) ≤ ↑a✝ ⊔ ⊥ ⊓ ⊥

case coe.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ⊥) ⊓ (↑a✝¹ ⊔ ↑a✝) ≤ ↑a✝¹ ⊔ ⊥ ⊓ ↑a✝

case coe.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ ⊥) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ ⊥

case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝² a✝¹ a✝ : α
⊢ (↑a✝² ⊔ ↑a✝¹) ⊓ (↑a✝² ⊔ ↑a✝) ≤ ↑a✝² ⊔ ↑a✝¹ ⊓ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : 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

Tactic:
cases x <;> cases y <;> cases z

Goal state after:
case top.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ ⊤) ≤ ⊤ ⊔ ⊤ ⊓ ⊤

case top.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ ↑a✝) ≤ ⊤ ⊔ ⊤ ⊓ ↑a✝

case top.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊤ ⊔ ↑a✝) ⊓ (⊤ ⊔ ⊤) ≤ ⊤ ⊔ ↑a✝ ⊓ ⊤

case top.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (⊤ ⊔ ↑a✝¹) ⊓ (⊤ ⊔ ↑a✝) ≤ ⊤ ⊔ ↑a✝¹ ⊓ ↑a✝

case coe.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (↑a✝ ⊔ ⊤) ⊓ (↑a✝ ⊔ ⊤) ≤ ↑a✝ ⊔ ⊤ ⊓ ⊤

case coe.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ⊤) ⊓ (↑a✝¹ ⊔ ↑a✝) ≤ ↑a✝¹ ⊔ ⊤ ⊓ ↑a✝

case coe.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ ⊤) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ ⊤

case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝² a✝¹ a✝ : α
⊢ (↑a✝² ⊔ ↑a✝¹) ⊓ (↑a✝² ⊔ ↑a✝) ≤ ↑a✝² ⊔ ↑a✝¹ ⊓ ↑a✝
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ a + (↑b + ↑d) ↔ b ≤ b + (⌊a⌋₊ + d)

Tactic:
add_left_comm _ (b : R)

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ ↑b + (a + ↑d) ↔ b ≤ b + (⌊a⌋₊ + d)
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
h : f ≤ g
m n : α
⊢ f m ≤ g n

Tactic:
by
  obtain ⟨k, hkm, hkn⟩ := exists_ge_ge m n
  calc
    f m ≤ f k := hf hkm
    _ ≤ g k := h _
    _ ≤ g n := hg hkn

Goal state after:
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible (a * b)
inst✝ : Invertible b
⊢ b * ⅟(a * b) * a = 1

Tactic:
rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one,
      one_mul]

Goal state after:
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟a + ⅟b = ⅟a * (a + b) * ⅟b

Tactic:
rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a| * |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a| * |geomSum a b n| ≤ (↑n + 1) * (max |a| |b| ^ n * max |a| |b|)
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
a b c : α
inst✝ : Preorder α
h₁ : SymmGen (fun x1 x2 ↦ x1 ≤ x2) a b
h₂ : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) b c
⊢ SymmGen (fun x1 x2 ↦ x1 ≤ x2) a c

Tactic:
by
  obtain (h | h) := h₁
  · exact (h.trans h₂.le).symmGen
  · exact (h₂.ge.trans h).symmGen_symm

Goal state after:
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddBelow s → BddAbove t → BddAbove (image2 f s t)

Tactic:
by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  exact ⟨f a b, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha hb⟩

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
⊢ WellFounded r

Tactic:
grind [wellFounded_iff_has_min]

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : α → Type u_4
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
⊢ ⇑(piEquivPiSubtypeProd p β).symm ⁻¹' univ.pi s = (univ.pi fun i ↦ s ↑i) ×ˢ univ.pi fun i ↦ s ↑i

Tactic:
by
  ext ⟨f, g⟩
  simp only [mem_preimage, mem_univ_pi, prodMk_mem_set_prod_eq, Subtype.forall, ← forall_and]
  refine forall_congr' fun i => ?_
  by_cases hi : p i <;> simp [hi]

Goal state after:
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
hc : IsCofinalFor s t
a : α
hat : a ∈ t
⊢ ∃ b ∈ t, a ≤ b

Tactic:
· exact ⟨a, hat, le_rfl⟩

Goal state after:
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : DirectedOn (fun x y ↦ y ≤ x) s
hMin : Minimal (fun x ↦ x ∈ s) a
hb : b ∈ s
⊢ a ≤ b

Tactic:
obtain ⟨z, hz, hza, hzb⟩ := h a hMin.1 b hb

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : DirectedOn (fun x y ↦ y ≤ x) s
hMin : Minimal (fun x ↦ x ∈ s) a
hb : b ∈ s
z : α
hz : z ∈ s
hza : z ≤ a
hzb : z ≤ b
⊢ a ≤ b
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t

Tactic:
prl,

Goal state after:
α : Type u_1
inst✝ : AddCommMonoid α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ tl + r = t
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t

Tactic:
prl,

Goal state after:
α : Type u_1
inst✝ : AddCommGroup α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ tl + r = t
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : a < b
⊢ 1 / b < 1 / a

Tactic:
rwa [lt_div_iff₀' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)]

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun b ↦ 0 * b) '' s) (0 * b)

Tactic:
· simp_rw [zero_mul]
    rw [hs.nonempty.image_const]
    exact isGLB_singleton

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List β
⊢ l = [] → Forall₂ R [] l

Tactic:
by rintro rfl; exact Forall₂.nil

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
⊢ l = [] → Forall₂ R l []

Tactic:
by rintro rfl; exact Forall₂.nil

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons.inr
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
⊢ a * b * (l.erase a).prod = b * l.prod

Tactic:
comm a ha b mem_cons_self,

Goal state after:
case cons.inr
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
⊢ b * a * (l.erase a).prod = b * l.prod