mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
h : a = b
⊢ ⅟a = ⅟b

Tactic:
apply invOf_eq_right_inv

Goal state after:
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
h : a = b
⊢ a * ⅟b = 1
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝ : MulOneClass α
r : α
hr : Invertible r
s si : α
hs : s = r
hsi : si = ⅟r
⊢ si * s = 1

Tactic:
rw [hs, hsi, invOf_mul_self]

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 b hab
    obtain ⟨c, hc⟩ := exists_between (WithTop.coe_lt_coe.mpr hab)
    induction c with
    | top => simp at hc
    | coe c => exact ⟨c, by simpa using hc⟩

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

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

Tactic:
rwa [add_comm, add_div', add_comm]

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |(-1) ^ n| = 1

Tactic:
by rw [← pow_abs, abs_neg, abs_one, one_pow]

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case inr.inr
β : 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 : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
this : c < a
⊢ f a = g a

Tactic:
rw [IH c this] at hc

Goal state after:
case inr.inr
β : 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 : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : g c = g a
this : c < a
⊢ f a = g a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ 0
hs : IsBot b
hb : 0 ≤ b
⊢ IsBot 0

Tactic:
exact hs.mono hb

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
this : 1 / a < b⁻¹ ↔ b⁻¹ * a < 1
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
rwa [one_div, mul_comm b⁻¹, ← division_def, div_lt_iff_of_neg hb, one_mul] at this

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
ha : a < 0
hb : b < 0
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
by
  have := div_lt_iff_of_neg ha (b := 1) (a := b⁻¹)
  rwa [one_div, mul_comm b⁻¹, ← division_def, div_lt_iff_of_neg hb, one_mul] at this

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

Goal state before:
pp: α : Type u_1
Rₐ : α → α → Prop
a : α
l : List α
⊢ Forall₂ Rₐ (a :: l) (a :: l) ↔ ∀ (x : α), x ∈ a :: l → Rₐ x x

Tactic:
by simp [@forall₂_same l]

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

Goal state before:
pp: case mpr.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ (a✝¹ :: l₂✝)

Tactic:
intro l₁ hl1; exact SublistForall₂.cons_right (ih hl1)

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

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
y z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z * l.prod)

Tactic:
exact Commute.mul_right h.1 (IH h.2)

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 *
      (match b == a with
        | true => l
        | false => b :: l.erase a).prod =
    (b :: l).prod

Tactic:
beq_false_of_ne ne.symm,

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
⊢ a *
      (match false with
        | true => l
        | false => b :: l.erase a).prod =
    (b :: l).prod
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case cons
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (foldl comp f (lh :: lt))

Tactic:
apply l_ih fun _ h => hl _ (List.mem_cons_of_mem _ h)
    apply Function.Injective.comp hf
    apply hl _ mem_cons_self

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

Goal state before:
pp: case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
u : αˣ
hnd : ¬a * ↑u ∣ a
⊢ False

Tactic:
simp at hnd

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

Goal state before:
pp: case neg
n : ℤ
hn : ¬n = 0
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
· have : (n : ℚ) ≠ 0 := by rwa [← intCast_inj]  at hn
    simp only [Int.ediv_self hn, Int.cast_one, div_self this]

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

Goal state before:
pp: case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 → n ∣ m

Tactic:
Rat.den_eq_one_iff,

Goal state after:
case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ ↑(↑m / ↑n).num = ↑m / ↑n → n ∣ m
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → ℕ → α
a : α
an cn : ℤ
ad b b' cd : ℕ
⊢ f = HPow.hPow → IsRat a an ad → IsNat b b' → an.pow b' = cn → ad.pow b' = cd → IsRat (f a b) cn cd

Tactic:
rintro rfl ⟨_, rfl⟩ ⟨rfl⟩ (rfl : an ^ b = _) (rfl : ad ^ b = _)

Goal state after:
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
f : α → ℕ → α
a : α
an cn ad b b' cd : ℕ
⊢ f = HPow.hPow → IsNNRat a an ad → IsNat b b' → an.pow b' = cn → ad.pow b' = cd → IsNNRat (f a b) cn cd

Tactic:
rintro rfl ⟨_, rfl⟩ ⟨rfl⟩ (rfl : an ^ b = _) (rfl : ad ^ b = _)

Goal state after:
α : Type u_1
inst✝ : Semiring α
an ad b : ℕ
inv✝ : Invertible ↑ad
⊢ IsNNRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
⊢ n1 * (n2 * (e1 / e2)) = t1

Tactic:
mul_div_left_comm,

Goal state after:
α : Type u_1
inst✝ : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
⊢ n1 * (e1 * (n2 / e2)) = t1
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: case inr
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ (a - b + b) * c = a * c

Tactic:
tsub_add_cancel_of_le hba

Goal state after:
case inr
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hba : b ≤ a
⊢ a * c = a * c
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
inst✝ : CompleteLattice β
s : Set (Set β)
⊢ sSup (⋃₀ s) = ⨆ t ∈ s, sSup t

Tactic:
by
  simp only [sUnion_eq_biUnion, sSup_eq_iSup, iSup_iUnion]

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
x : ↑(Iic a)
⊢ x = ⊤ ↔ ↑x = a

Tactic:
by
  simp [Subtype.ext_iff]

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

Goal state before:
pp: case ht
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ y ∈ range fun i ↦ f i, ∃ x ∈ ⋃ i, Iic (f i), y ≤ x

Tactic:
rintro x ⟨i, rfl⟩
    exact ⟨f i, mem_iUnion_of_mem i le_rfl, le_rfl⟩

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

Goal state before:
pp: case left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ a₂ ≤ a₁

Tactic:
refine le_of_not_gt fun h' => ?_

Goal state after:
case left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
⊢ False
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ b₁ ≤ b₂

Tactic:
refine le_of_not_gt fun h' => ?_

Goal state after:
case right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ x = y

Tactic:
suffices x.2 = y.2 by exact Prod.ext (hf _ hx.2 <| h.trans <| by rw [this]) this
    refine ht.elim hx.2 hy.2 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.1, ?_⟩)
    rw [h]
    exact mem_image_of_mem _ hy.1

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
hs : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
⊢ y ≤ x

Tactic:
by
  cases hs.total hx hy with
  | inr h' => exact h'
  | inl h' => simpa [lt_iff_le_not_ge, h'] using h

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : 0 ≤ a
b : α
hb : 0 ≤ b
c : α
hc : 0 ≤ c
⊢ ⟨a, ha⟩ - ⟨b, hb⟩ ≤ ⟨c, hc⟩ ↔ ⟨a, ha⟩ ≤ ⟨c, hc⟩ + ⟨b, hb⟩

Tactic:
simp only [sub_le_iff_le_add, Subtype.mk_le_mk, mk_sub_mk, mk_add_mk, toNonneg_le]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ ↑p.num / ↑p.den < ↑q.num / ↑q.den

Tactic:
div_lt_div_iff₀,

Goal state after:
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ ↑p.num * ↑q.den < ↑q.num * ↑p.den

case hb
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ 0 < ↑p.den

case hd
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ 0 < ↑q.den
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹.mul db ≤ num✝.mul da) = true
h : ↑(num✝¹.mul db) ≤ ↑(num✝.mul da)
ha : 0 ≤ ⅟↑da
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
have hb : 0 ≤ ⅟(db : α) := invOf_nonneg.mpr <| Nat.cast_nonneg db

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹.mul db ≤ num✝.mul da) = true
h : ↑(num✝¹.mul db) ≤ ↑(num✝.mul da)
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true
h : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))
ha : 0 ≤ ⅟↑da
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
have hb : 0 ≤ ⅟(db : α) := invOf_nonneg.mpr <| Nat.cast_nonneg db

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true
h : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial k = n.descFactorialBinary k

Tactic:
descFactorialBinary

Goal state after:
n k : ℕ
⊢ n.descFactorial k = if n < k then 0 else (n - k + 1).ascFactorialBinary k
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ (if 2 * fract x < 1 then ⌊x⌋ + y else ⌈x + ↑y⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y

Tactic:
Int.ceil_add_intCast,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ (if 2 * fract x < 1 then ⌊x⌋ + y else ⌈x⌉ + y) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℕ
⊢ round (↑y + x) = ↑y + round x

Tactic:
rw [add_comm, round_add_natCast, add_comm]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 0 < fract x + fract x
⊢ 0 < fract x

Tactic:
simpa only [← two_mul, mul_pos_iff_of_pos_left, zero_lt_two] using hx

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a + b⌋ ≤ a + b

Tactic:
exact floor_le _

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ ⌈a⌉ ≤ ⌊a⌋ + 1

Tactic:
by
  rw [ceil_le, Int.cast_add, Int.cast_one]
  exact (lt_floor_add_one a).le

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
z : ℤ
⊢ ⌈-a⌉ ≤ z ↔ -⌊a⌋ ≤ z

Tactic:
neg_le,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
a : R
inst✝ : IsOrderedRing R
z : ℤ
⊢ ⌈-a⌉ ≤ z ↔ -z ≤ ⌊a⌋
Module: Mathlib.Tactic.Positivity.Basic

Goal state before:
pp: a : ℤ
ha : 0 < a
⊢ 0 < a / a

Tactic:
by
  rw [Int.ediv_self ha.ne']; exact zero_lt_one

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

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
let s : Set ℤ := { n : ℤ | a ^ n ≤ g }
  obtain ⟨k, hk : g⁻¹ ≤ a ^ k⟩ := MulArchimedean.arch g⁻¹ ha
  have h_ne : s.Nonempty := ⟨-k, by simpa [s] using inv_le_inv' hk⟩
  obtain ⟨k, hk⟩ := MulArchimedean.arch g ha
  have h_bdd : ∀ n ∈ s, n ≤ (k : ℤ) := by
    intro n hn
    apply (zpow_le_zpow_iff_right ha).mp
    rw [← zpow_natCast] at hk
    exact le_trans hn hk
  obtain ⟨m, hm, hm'⟩ := Int.exists_greatest_of_bdd ⟨k, h_bdd⟩ h_ne
  have hm'' : g < a ^ (m + 1) := by
    contrapose! hm'
    exact ⟨m + 1, hm', lt_add_one _⟩
  refine ⟨m, ⟨hm, hm''⟩, fun n hn => (hm' n hn.1).antisymm <| Int.le_of_lt_add_one ?_⟩
  rw [← zpow_lt_zpow_iff_right ha]
  exact lt_of_le_of_lt hm hn.2

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

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den

Tactic:
have : q⁻¹.num < (⌊q⁻¹⌋ + 1) * q⁻¹.den := Rat.num_lt_succ_floor_mul_den q⁻¹

Goal state after:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : q⁻¹.num < (⌊q⁻¹⌋ + 1) * ↑q⁻¹.den
⊢ q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : ↑q₁ < ↑q₂
this : 0 < ↑q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Tactic:
norm_cast at hq₁₂ this

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mp
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
m : Multiset α
hm : a ::ₘ as = m
h : Rel r m bs
⊢ ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

Tactic:
induction h generalizing as with
    | zero => simp at hm
    | @cons a' b as' bs ha'b h ih =>
      rcases cons_eq_cons.1 hm with (⟨rfl, rfl⟩ | ⟨_h, cs, eq₁, eq₂⟩)
      · exact ⟨b, bs, ha'b, h, rfl⟩
      · rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
        exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩

Goal state after:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} → ∃ a, s = {a} ∧ f a = b

pp: case mpr
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ (∃ a, s = {a} ∧ f a = b) → map f s = {b}

Tactic:
· intro h
    obtain ⟨a, ha⟩ : ∃ a, s = {a} := by rw [← card_eq_one, ← card_map, h, card_singleton]
    refine ⟨a, ha, ?_⟩
    rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]

Goal state after:
case mpr
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ (∃ a, s = {a} ∧ f a = b) → map f s = {b}
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∈ (l₁ ++ l₂).dedup
⊢ (l₁ ++ l₂).dedup = List.insert a (l₁ ++ l₂).dedup

Tactic:
insert_of_mem h

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∈ (l₁ ++ l₂).dedup
⊢ (l₁ ++ l₂).dedup = (l₁ ++ l₂).dedup
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ dropSlice n m xs ~ ys ∩ dropSlice n m xs

Tactic:
by
  simp only [dropSlice_eq]
  have : n ≤ n + m := Nat.le_add_right _ _
  have h₂ := h.nodup_iff.2 h'
  apply Perm.trans _ (Perm.inter_append _).symm
  · exact Perm.append (Perm.take_inter _ h h') (Perm.drop_inter _ h h')
  · exact disjoint_take_drop h₂ this

Goal state after:
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.toFinset ⊆ t.toFinset ↔ s ⊆ t

Tactic:
by
  simp only [Finset.subset_iff, Multiset.subset_iff, Multiset.mem_toFinset]

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ countP p (map f (a ::ₘ t)) = (filter (fun a ↦ p (f a)) (a ::ₘ t)).card

Tactic:
rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
      Nat.add_comm]

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ min (count x N) (count x Q) + count x (P - M) = count x N

Tactic:
Multiset.count_sub

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ min (count x N) (count x Q) + (count x P - count x M) = count x N
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] = (take x.length y).concat y[x.length]

pp: α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x.length < y.length

Tactic:
List.concat_eq_append

Goal state after:
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] = take x.length y ++ [y[x.length]]

α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x.length < y.length
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
s : List α
this : s = [] ↔ s <+: []
⊢ s ∈ [].inits ↔ s <+: []

Tactic:
simpa only [inits, mem_singleton]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₁
⊢ s₁ ∩ insert a s₂ = s₁ ∩ s₂

Tactic:
by rw [inter_comm, insert_inter_of_notMem h, inter_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s.erase a ⊆ (insert a s).erase a

Tactic:
grw [← subset_insert]

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ map f s₁ ⊆ map f s₂

Tactic:
simp [subset_def, Multiset.map_subset_map h]

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
hx : f.symm x ∈ s
⊢ x ∈ t

Tactic:
simpa using h hx

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ map f (s.erase a) = (map f s).erase (f a)

Tactic:
map_eq_image

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ image (⇑f) (s.erase a) = (image (⇑f) s).erase (f a)
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑(b.castPred ⋯)

Tactic:
· exact H

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

Goal state before:
pp: n : ℕ
i : Fin n
h : ↑i + 1 < n
⊢ ↑(i + 1) = ↑i + 1

Tactic:
by
  simpa [add_def] using Nat.mod_eq_of_lt (by lia)

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
⊢ a.castLT ha - b.castLT ⋯ = (a - b).castLT ⋯

Tactic:
rw [Fin.ext_iff]

Goal state after:
n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
⊢ ↑(a.castLT ha - b.castLT ⋯) = ↑((a - b).castLT ⋯)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ (last n).predAbove i = if hi : i = last (n + 1) then last n else i.castPred hi

Tactic:
by
  split_ifs with hi
  · rw [hi, predAbove_right_last]
  · rw [predAbove_last_of_ne_last hi]

Goal state after: