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

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

Tactic:
cases z

Goal state after:
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: case zero.zero
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
⊢ 0 ≤ 0 → 0 ≤ z → 0 ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) 0 z

Tactic:
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✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
cases z

Goal state after:
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✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
cases z

Goal state after:
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✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝ : SemilatticeInf α
z : WithZero α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ↑a✝¹ ≤ z → ↑a✝¹ ≤ map₂ (fun x1 x2 ↦ x1 ⊓ x2) (↑a✝) z

Tactic:
cases z

Goal state after:
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: case top.top
α : 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

Tactic:
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✝
Module: Mathlib.Order.WithBot

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

Tactic:
cases z

Goal state after:
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✝
Module: Mathlib.Order.WithBot

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

Tactic:
cases z

Goal state after:
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✝
Module: Mathlib.Order.WithBot

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

Tactic:
cases z

Goal state after:
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: case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ⊥ ⊓ z

Tactic:
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✝
Module: Mathlib.Order.WithBot

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

Tactic:
cases z

Goal state after:
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✝
Module: Mathlib.Order.WithBot

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

Tactic:
cases z

Goal state after:
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✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ z) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ z

Tactic:
cases z

Goal state after:
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: case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ⊤ ⊓ z

Tactic:
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✝
Module: Mathlib.Order.WithBot

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

Tactic:
cases z

Goal state after:
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✝
Module: Mathlib.Order.WithBot

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

Tactic:
cases z

Goal state after:
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✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ z) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ z

Tactic:
cases z

Goal state after:
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
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : a < 0
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
rwa [floor_of_nonpos ha.le, lt_ceil, Nat.cast_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ 0 ≤ a - ↑n

Tactic:
exact le_tsub_of_add_le_left ((add_zero _).trans_le h)

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
⊢ DenselyOrdered (WithBot α) ↔ DenselyOrdered α

Tactic:
constructor <;> intro h <;> constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered α
⊢ ∀ (a₁ a₂ : WithBot α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
⊢ DenselyOrdered (WithTop α) ↔ DenselyOrdered α

Tactic:
constructor <;> intro h <;> constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered α
⊢ ∀ (a₁ a₂ : WithTop α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Preorder α
f : α → β
inst✝ : IsDirectedOrder α
hf : Monotone f
hf' : Antitone f
a b : α
⊢ f a = f b

Tactic:
have := hf.forall_le_of_antitone hf' le_rfl

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Preorder α
f : α → β
inst✝ : IsDirectedOrder α
hf : Monotone f
hf' : Antitone f
a b : α
this : ∀ (m n : α), f m ≤ f n
⊢ f a = f b
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = a / b + c * b / (d * b)

Tactic:
mul_div_mul_right c d hb

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = a / b + c / d
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : K
⊢ a / 2 - a = -(a / 2)

Tactic:
by rw [← neg_sub, sub_half]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b c : K
hc : c ≠ 0
⊢ a / c - b = (a - c * b) / c

Tactic:
by
  simpa using div_sub_div a b hc one_ne_zero

Goal state after:
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₁ a ≤ f₁ b

Tactic:
exact h₁ ha hb hab

Goal state after:
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₁ a < f₁ b

Tactic:
exact h₁ ha hb hab

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
hab : a ≤ b
⊢ a = c ∧ b = c

Tactic:
exact
      ⟨eq_of_mem_singleton <| h ▸ left_mem_Icc.2 hab,
        eq_of_mem_singleton <| h ▸ right_mem_Icc.2 hab⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ici a ∩ Iic b ∩ Icc b c = {b}

Tactic:
← Iic_inter_Ici,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ici a ∩ Iic b ∩ (Iic c ∩ Ici b) = {b}
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

pp: case inr.inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 1 ≤ a / 0 ↔ 0 < 0 ∧ 0 ≤ a ∨ 0 < 0 ∧ a ≤ 0

pp: case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

Tactic:
· simp [hb, hb.not_gt, one_le_div_of_neg]

Goal state after:
case inr.inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 1 ≤ a / 0 ↔ 0 < 0 ∧ 0 ≤ a ∨ 0 < 0 ∧ a ≤ 0

case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ ε⁻¹ * ε * ε * a ^ 2 + ε⁻¹ * b ^ 2 = ε * a ^ 2 + ε⁻¹ * b ^ 2

Tactic:
inv_mul_cancel₀ hε.ne',

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 1 * ε * a ^ 2 + ε⁻¹ * b ^ 2 = ε * a ^ 2 + ε⁻¹ * b ^ 2
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n.succ ≠ 0
⊢ (replicate n.succ l).flatten.head? = l.head?

Tactic:
induction l <;> simp [replicate]

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

Goal state before:
pp: α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ a :: (b :: l).dropLast ++ [(a :: b :: l).getLast h] = a :: b :: l

Tactic:
cons_append,

Goal state after:
α : Type u
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ a :: ((b :: l).dropLast ++ [(a :: b :: l).getLast h]) = a :: b :: l
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
a b : α
l : List α
c : α
hc : c ∈ (b :: l).getLast?
⊢ a :: (b :: l).dropLast ++ [c] = a :: b :: l

Tactic:
cons_append,

Goal state after:
α : Type u
a b : α
l : List α
c : α
hc : c ∈ (b :: l).getLast?
⊢ a :: ((b :: l).dropLast ++ [c]) = a :: b :: l
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
⊢ (b :: c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?

Tactic:
cons_append,

Goal state after:
α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
⊢ (b :: (c :: l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
⊢ (b :: (c :: l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?

Tactic:
cons_append,

Goal state after:
α : Type u
b c : α
l₁ : List α
a : α
l₂ : List α
⊢ (b :: c :: (l₁ ++ a :: l₂)).getLast? = (a :: l₂).getLast?
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
by_cases ha : a = 0
  · simp [ha]
  by_cases hn : n = 0
  · rw [hn]
    simp [zpow', ha, zpow_ne_zero ]
  by_cases hm : m = 0
  · rw [hm]
    simp [zpow', ha]
  simpa [zpow', ha, hm, hn] using zpow_mul a m n

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

Goal state before:
pp: M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
⊢ L = L'

Tactic:
by
  refine ext_get h fun i h₁ h₂ => ?_
  have : (L.take (i + 1)).prod = (L'.take (i + 1)).prod := h' _ (Nat.succ_le_of_lt h₁)
  rw [prod_take_succ L i h₁, prod_take_succ L' i h₂, h' i (Nat.le_of_lt h₁)] at this
  convert! mul_left_cancel this

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
⊢ (match f a with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    (f a).toList ++ flatMap (fun a ↦ (f a).toList) l

Tactic:
rcases f a <;> simp [ih]

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ divNat (a * n) (a * d) = divNat n d

Tactic:
ext; push_cast; exact Rat.divInt_mul_left (mod_cast ha)

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ a

Tactic:
rw [h]
    exact ⟨0, by simp⟩

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ x, ¬IsUnit x ∧ b = a * x

Tactic:
rcases hd with ⟨c, rfl⟩

Goal state after:
case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ∃ x, ¬IsUnit x ∧ a * c = a * x
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: case inl
R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b d : R
hab : a < b
this : MulPosStrictMono R
hcd : 0 < d
⊢ a * 0 < b * d

Tactic:
rw [mul_zero]

Goal state after:
case inl
R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b d : R
hab : a < b
this : MulPosStrictMono R
hcd : 0 < d
⊢ 0 < b * d
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (l '' range f) (l (sSup (range f)))

Tactic:
exact gc.isLUB_l_image (isLUB_sSup _)

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:

Tactic:
_ = ⨅ a : range (range <| f ·), ⨆ b : a.1, b.1 := by
      simp_rw [iInf_subtype, iInf_range, iSup_subtype, iSup_range]
    _ = _ := minAx.iInf_iSup_eq _
    _ ≤ _ := iSup_le fun g => by
      refine le_trans ?_ <| le_iSup _ fun a => Classical.choose (g ⟨_, a, rfl⟩).2
      refine le_iInf fun a => le_trans (iInf_le _ ⟨range (f a), a, rfl⟩) ?_
      rw [← Classical.choose_spec (g ⟨_, a, rfl⟩).2]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
h : ¬∃ x, rhs < x ∧ x < lhs
⊢ lhs ≤ rhs

Tactic:
else

Goal state after:
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
h : ¬∃ x, rhs < x ∧ x < lhs
⊢ lhs ≤ rhs
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
b : α
hs : s.Nonempty
hb : b < sSup s
⊢ ∃ a ∈ s, b < a

Tactic:
contrapose! hb
  exact csSup_le hs hb

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
⊢ Ioc a b = Ioc c d ↔ a = c ∧ b = d

Tactic:
refine ⟨fun h ↦ ?_, by grind⟩
  have : b ≤ d ∧ c ≤ a := (Ioc_subset_Ioc_iff (show a < b by grind [Set.nonempty_Ioc])).1 h.subset
  have : d ≤ b ∧ a ≤ c := (Ioc_subset_Ioc_iff (show c < d by grind)).1 h.superset
  grind

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬∃ t, IsChain r s ∧ SuperChain r s t
⊢ IsChain r (SuccChain r s)

Tactic:
else

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ¬∃ t, IsChain r s ∧ SuperChain r s t
⊢ IsChain r (SuccChain r s)
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : ¬∃ t, IsChain r s ∧ SuperChain r s t
⊢ s ⊆ SuccChain r s

Tactic:
else

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
h : ¬∃ t, IsChain r s ∧ SuperChain r s t
⊢ s ⊆ SuccChain r s
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
a : α
ha : a ≠ 0
lt : 0 < a
⊢ Nontrivial { x // 0 ≤ x }

Tactic:
· exact ⟨0, ⟨a, lt.le⟩, Subtype.coe_ne_coe.mp ha.symm⟩

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : ¬BddAbove t
⊢ sSup t = sSup ∅

Tactic:
by simp [ht]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : Inhabited ↑s
h_Sup : ∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s
h_Inf : ∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s
t : Set ↑s
ht : ¬BddBelow t
⊢ sInf t = sInf ∅

Tactic:
by simp [ht]

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f g : ι → M
x✝ : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
hx : ¬x ∈ mulSupport f
⊢ f x = g x

Tactic:
else

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f g : ι → M
x✝ : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
hx : ¬x ∈ mulSupport f
⊢ f x = g x