mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: case refine_2
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
⊢ (if hlm : l < m then lt l hlm
    else
      ge l ⋯ fun k_1 x ↦
        Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
          (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯)
          k_1 ⋯) =
    Int.strongRec lt ge l

Tactic:
split_ifs with hlm

Goal state after:
case pos
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
hlm : l < m
⊢ lt l hlm = Int.strongRec lt ge l

case neg
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
hlm : ¬l < m
⊢ (ge l ⋯ fun k_1 x ↦
      Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯) k_1
        ⋯) =
    Int.strongRec lt ge l
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: case zero
α : Type u
inst✝ : NonAssocSemiring α
a : α
⊢ 0 • a = ↑0 * a

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: case zero
⊢ IsSquare (sign 0) ↔ 0 ≤ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: case zero
A : Type u_2
F : Type u_4
inst✝² : FunLike F ℕ A
inst✝¹ : AddZeroClass A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
⊢ f 0 = g 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
⊢ a ^ 0 ∣ b ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: case zero
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
⊢ 0 • a = a * ↑0

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ 1 / (-1 * a) = 1 / a * (1 / -1)

Tactic:
one_div_mul_one_div_rev

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ 1 / (-1 * a) = 1 / (-1 * a)
Module: Mathlib.Logic.Nontrivial.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
⊢ ∃ x y, x < y

Tactic:
cases lt_or_gt_of_ne hxy

Goal state after:
case inl
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h✝ : x < y
⊢ ∃ x y, x < y

case inr
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h✝ : y < x
⊢ ∃ x y, x < y
Module: Mathlib.Data.Nat.Cast.Commute

Goal state before:
pp: case zero
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
⊢ Commute (↑0) x

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case zero
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
⊢ ↑0 • b = 0 • b

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
y : M
⊢ (0 • x) • y = 0 • x • y

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ -f x * f y = -(f x * f y)

Tactic:
rw [← neg, ← mul, neg_mul, neg, mul]

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

Goal state before:
pp: case zero
α : Type u_2
inst✝ : Semiring α
a : α
ha : Odd a
⊢ Odd (a ^ 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_2
inst✝¹ : Semiring α
a b : α
inst✝ : IsCancelAdd α
hab : a + b = 0
⊢ a ^ (2 * 0 + 1) + b ^ (2 * 0 + 1) = 0

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a : α
⊢ Odd (a + 2) ↔ Odd a

Tactic:
← one_add_one_eq_two,

Goal state after:
α : Type u_2
inst✝ : Ring α
a : α
⊢ Odd (a + (1 + 1)) ↔ Odd a
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case zero
R : Type u_4
inst✝ : AddMonoidWithOne R
h : 2 = 0
⊢ (Even 0 → ↑0 = 0) ∧ (Odd 0 → ↑0 = 1)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Prod.PProd

Goal state before:
pp: case refl
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
δ : Sort u_4
α : Type u_5
β : Type u_6
x₁ : α
y₁ : β
P : Sort u_7
w : x₁ = x₁ → y₁ = y₁ → P
⊢ P

Tactic:
exact w rfl rfl

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

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a : M₀
inst✝ : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
this : ZeroLEOneClass M₀
⊢ a ^ (n + 1) ≤ a ^ n

Tactic:
← mul_one (a ^ n),

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a : M₀
inst✝ : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
this : ZeroLEOneClass M₀
⊢ a ^ (n + 1) ≤ a ^ n * 1
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 ≤ a
hb : 1 < b
⊢ 1 < a * b

pp: case inr
M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 < a
hb : 1 ≤ b
⊢ 1 < a * b

Tactic:
exacts [one_lt_mul ha hb, one_lt_mul_of_lt_of_le ha hb]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + b + b * c ≤ c
⊢ 1 + a ≤ (1 - b) * (1 + c)

Tactic:
by
  rw [one_sub_mul, mul_one_add, le_sub_iff_add_le, add_assoc, ← add_assoc a]
  gcongr

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a : G₀
⊢ ∀ (a : G₀), 0 < a → 0 < a⁻¹

Tactic:
intro a

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a✝ a : G₀
⊢ 0 < a → 0 < a⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a : G₀
⊢ ∀ (a : G₀), 0 < a → 0 < a⁻¹

Tactic:
intro a

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a✝ a : G₀
⊢ 0 < a → 0 < a⁻¹
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
⊢ ∀ {a b : α},
    { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
intro a

Goal state after:
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
a : α
⊢ ∀ {b : α},
    { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
⊢ ∀ (a a_1 : X), f a ≤ f a_1 ↔ a_1 ≤ a

Tactic:
intro a

Goal state after:
case refine_1
X : Type u_6
Y : Type u_7
F : Type u_8
inst✝² : LinearOrder X
inst✝¹ : Preorder Y
inst✝ : EquivLike F X Y
f : F
hf : StrictAnti ⇑f
a : X
⊢ ∀ (a_1 : X), f a ≤ f a_1 ↔ a_1 ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |a / -↑n| ≤ |a|

Tactic:
Int.ediv_neg,

Goal state after:
this : ∀ (a : ℤ) (n : ℕ), |a / ↑n| ≤ |a|
a b : ℤ
n : ℕ
⊢ |(-(a / ↑n))| ≤ |a|
Module: Mathlib.Algebra.Order.Group.Nat

Goal state before:
pp: case zero
m k : ℕ
⊢ m - 0 ≤ k ↔ m ≤ k + 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
⊢ 1 < a * b ↔ 1 < a ∨ 1 < b

Tactic:
simp only [one_lt_iff_ne_one, Ne, mul_eq_one, not_and_or]

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ IsAddUnit a → a ≠ ⊤

Tactic:
rintro ⟨⟨b, c, hbc, -⟩, rfl⟩ rfl; simp [LinearOrderedAddCommGroupWithTop.top_add'] at hbc

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hac : AddLECancellable (a - c)
h : c ≤ a
⊢ a + b = b + (c + (a - c))

Tactic:
add_tsub_cancel_of_le h,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hac : AddLECancellable (a - c)
h : c ≤ a
⊢ a + b = b + a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe
α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
a✝ : α
yw : y < ↑a✝
⊢ x + ↑a✝ ≤ z + ↑a✝

Tactic:
exact (WithTop.add_lt_add_right coe_ne_top xz).le

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
x✝ y : WithBot α
inst✝ : OrderTop α
x : WithBot α
⊢ x ≤ ⊤

Tactic:
by cases x <;> simp [le_def]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
x : WithBot α
⊢ x ≤ x

Tactic:
by cases x <;> simp [le_def]

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case zero
P : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ findGreatest P 0 = m ↔ m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case zero
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
⊢ findGreatest P 0 ≤ findGreatest Q 0

Tactic:
| zero =>

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
a✝ n✝ : ℕ
x✝ : 0 ≤ a✝
⊢ n✝ ≤ id a✝ ↔ ↑n✝ ≤ a✝

Tactic:
Nat.cast_id,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
a✝ n✝ : ℕ
x✝ : 0 ≤ a✝
⊢ n✝ ≤ id a✝ ↔ n✝ ≤ a✝
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
n a : ℕ
⊢ id n ≤ a ↔ n ≤ ↑a

Tactic:
Nat.cast_id,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
n a : ℕ
⊢ id n ≤ a ↔ n ≤ a
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: case zero
α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
hn : ↑n = ↑n.succ
⊢ ↑(n + 0) = ↑n

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
a : β
⊢ ∀ (y : β),
    ∃ z,
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ y) (extend e f ⊥ z)
Module: Mathlib.Order.WithBot

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

Tactic:
intro a

Goal state after:
case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a : α
⊢ ∀ (a₂ : α), a < a₂ → ∃ a_2, a < a_2 ∧ a_2 < a₂
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ |a - ↑⌊a⌋₊| ≤ 1

Tactic:
refine abs_le.mpr ⟨?_, ?_⟩
  · simpa using (floor_le ha).trans (le_add_of_nonneg_right zero_le_one)
  · simpa [add_comm] using (lt_floor_add_one a).le

Goal state after:
Module: Mathlib.Order.WithBot

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

Tactic:
intro a

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

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
⊢ DirectedOn (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) (Set.univ.pi d)

Tactic:
intro a

Goal state after:
ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
a : (i : ι) → α i
⊢ a ∈ Set.univ.pi d →
    ∀ y ∈ Set.univ.pi d,
      ∃ z ∈ Set.univ.pi d, (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) a z ∧ (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) y z
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Invertible 2
⊢ 2 - 1 = 1

Tactic:
← one_add_one_eq_two,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Invertible 2
⊢ 1 + 1 - 1 = 1
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ -2 + 1 = ⅟b * a + ⅟a * b ↔ -1 + 0 = ⅟b * a + ⅟a * b

Tactic:
← one_add_one_eq_two,

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ -(1 + 1) + 1 = ⅟b * a + ⅟a * b ↔ -1 + 0 = ⅟b * a + ⅟a * b
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case zero
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
hn : 0 + 1 ≠ 0
⊢ x ^ (0 + 1) + y ^ (0 + 1) ≤ (x + y) ^ (0 + 1)

Tactic:
| zero =>

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b : K
h : b ≠ 0
⊢ (b + a) / b = 1 + a / b

Tactic:
by rw [← div_self h, add_div]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b : K
h : b ≠ 0
⊢ (a + b) / b = a / b + 1

Tactic:
by rw [← div_self h, add_div]

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b - c
⊢ a ∣ b ↔ a ∣ c

Tactic:
← sub_add_cancel b c,

Goal state after:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b - c
⊢ a ∣ b - c + c ↔ a ∣ c
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
⊢ StrictMono fun a ↦ a ^ n

Tactic:
intro a

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a : R
⊢ ∀ ⦃b : R⦄, a < b → (fun a ↦ a ^ n) a < (fun a ↦ a ^ n) b
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
⊢ MonotoneOn f₂ s

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
⊢ a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f₂ a ≤ f₂ b
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
⊢ StrictMonoOn f₂ s

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
⊢ a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f₂ a < f₂ b
Module: Mathlib.Algebra.Order.Ring.Abs

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : CommRing α
a b : α
n : ℕ
⊢ a ^ (0 + 1) - b ^ (0 + 1) = (a - b) * geomSum a b 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ WellFoundedGT (Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2) ↔ WellFoundedGT α

Tactic:
isWellFounded_iff

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ (WellFounded fun x1 x2 ↦ x2 < x1) ↔ WellFounded fun x1 x2 ↦ x2 < x1
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
n : ℕ
⊢ a ^ n = -1 ↔ a = -1 ∧ Odd n

Tactic:
by
  simpa using pow_eq_neg_pow_iff (R := R) one_ne_zero

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
⊢ ⇑(prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

Tactic:
by
  simpa only [Equiv.image_eq_preimage_symm] using! prod_assoc_preimage

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a : β
⊢ ∀ (x : β), (∀ (y : β), y < x → f y = g y) → f x = g x

Tactic:
intro a

Goal state after:
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
⊢ (∀ (y : β), y < a → f y = g y) → f a = g a
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a < b
⊢ Ico a b ∪ {a} = Ico a b

Tactic:
union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Ico.2 hab)

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a < b
⊢ Ico a b = Ico a b
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hys : ∀ x ∈ s, ¬y ≤ x
⊢ ∃ b ∈ t, x ≤ b

Tactic:
obtain ⟨z, (hzs | hzt), hxz, hyz⟩ := h x (.inl hx) y (.inr hy)

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hys : ∀ x ∈ s, ¬y ≤ x
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ b ∈ t, x ≤ b

case inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hys : ∀ x ∈ s, ¬y ≤ x
z : α
hzt : z ∈ t
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ b ∈ t, x ≤ b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioo x y)
a : α
ha : a ∈ Ioo x y
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ b, b < ⟨a, ha⟩

Tactic:
exact ⟨⟨b, mem_Ioo.mpr ⟨hb₁, hb₂.trans ha.2⟩⟩, hb₂⟩

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n d : ℕ
inst✝² : Semiring A
inst✝¹ : LinearOrder A
inst✝ : IsStrictOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
⊢ 0 < e

Tactic:
have pos_invOf_d : (0 < ⅟ (d : A)) := pos_invOf_of_invertible_cast d
    have pos_n : (0 < (n : A)) := Nat.cast_pos (n := n) |>.2 (of_decide_eq_true h)
    rw [eq]
    exact mul_pos pos_n pos_invOf_d

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

Goal state before:
pp: case zero
M : Type u_2
inst✝ : Monoid M
a : M
⊢ (replicate 0 a).prod = a ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u
l : List α
⊢ tail^[0] l = drop 0 l

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
l : List α
hl : ∀ (x : α), x ∈ l → p x
⊢ (pmap f l hl).insertIdx 0 (f a ha) = pmap f (l.insertIdx 0 a) ⋯

Tactic:
| zero =>

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

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : ¬a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
· exact ((List.mem_cons.1 h).elim Or.inl (fun h => Or.inr ⟨hab, h⟩))

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

Goal state before:
pp: case zero
G : Type u_7
inst✝ : Group G
f : ℕ → G
⊢ (map (fun k ↦ f k / f (k + 1)) (range 0)).prod = f 0 / f 0

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Injective (map f) ↔ Injective f

Tactic:
refine ⟨fun h x y hxy => ?_, (·.list_map)⟩
  suffices [x] = [y] by simpa using this
  apply h
  simp [hxy]

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

Goal state before:
pp: a b c : ℤ
h : ¬c = 0
⊢ (a + b) /. c = a /. c + b /. c

Tactic:
rw [divInt_add_divInt _ _ h h, divInt_eq_divInt_iff h (Int.mul_ne_zero h h)]

Goal state after:
a b c : ℤ
h : ¬c = 0
⊢ (a + b) * (c * c) = (a * c + b * c) * c
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case zero
a : ℕ
⊢ range' a 0 0 = replicate 0 a

Tactic:
| zero =>

Goal state after: