mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ
q n p : ℕ
dvd : (p + 1).gcd q ∣ n
le : (p + 1).pred * q.pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * q = n

Tactic:
obtain _ | q := q

Goal state after:
case succ.zero
n p : ℕ
dvd : (p + 1).gcd 0 ∣ n
le : (p + 1).pred * pred 0 ≤ n
⊢ ∃ a b, a * (p + 1) + b * 0 = n

case succ.succ
n p q : ℕ
dvd : (p + 1).gcd (q + 1) ∣ n
le : (p + 1).pred * (q + 1).pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hm : a ^ m = 1
hn : a ^ n = 1
⊢ a ^ m.gcd n = 1

Tactic:
obtain _ | m := m
    · simpa
    obtain ⟨y, rfl⟩ := IsUnit.of_pow_eq_one hm m.succ_ne_zero
    rw [← Units.val_pow_eq_pow_val, ← Units.val_one (α := M), ← zpow_natCast, ← Units.ext_iff] at *
    rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Group α
a : WithZero α
ha : a ≠ 0
⊢ a * a⁻¹ = 1

Tactic:
lift a to α using ha

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Group α
a : α
⊢ ↑a * (↑a)⁻¹ = 1
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 : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < c + b

Tactic:
rw [add_comm]
  exact hb.tsub_lt_iff_left hba

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
a : R
⊢ a < ↑⌊a⌋₊ + 1

Tactic:
simpa using lt_succ_floor a

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
a b : R
hb : 0 ≤ b
⊢ Nat.cast ⁻¹' Icc a b = Icc ⌈a⌉₊ ⌊b⌋₊

Tactic:
ext
  simp [ceil_le, hb, le_floor_iff]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
hab : a < b
c : WithBot α
hc : ↑a < c ∧ c < ↑b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
induction c with
    | bot => simp at hc
    | coe c => exact ⟨c, by simpa using hc⟩

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a b : α
hab : r a b
⊢ DirectedOn r {b, a}

Tactic:
rw [Set.pair_comm]
  apply directedOn_pair hab

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ (a + b) ^ 2 = a ^ 2 + b ^ 2 + (a * b + b * a)

Tactic:
by
        simp_rw [pow_succ', pow_zero, mul_one, add_mul, mul_add, add_comm (b * a), add_add_add_comm]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
a : α
⊢ |a ^ n|ₘ = |a|ₘ ^ |n|

Tactic:
obtain n0 | n0 := le_total 0 n
  · obtain ⟨n, rfl⟩ := Int.eq_ofNat_of_zero_le n0
    simp only [mabs_pow, zpow_natCast, Nat.abs_cast]
  · obtain ⟨m, h⟩ := Int.eq_ofNat_of_zero_le (neg_nonneg.2 n0)
    rw [← mabs_inv, ← zpow_neg, ← abs_neg, h, zpow_natCast, Nat.abs_cast, zpow_natCast]
    exact mabs_pow m _

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
⊢ image2 f (insert a s) t = (fun b ↦ f a b) '' t ∪ image2 f s t

Tactic:
rw [insert_eq, image2_union_left, image2_singleton_left]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ Relation.Fibration (fun x1 x2 ↦ x1 < x2) (fun x1 x2 ↦ x1 < x2) (toAntisymmetrization fun x1 x2 ↦ x1 ≤ x2)

Tactic:
rintro a ⟨b⟩ h

Goal state after:
case mk
α : Type u_1
inst✝ : Preorder α
a : α
b✝ : Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2
b : α
h : Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 ↦ x1 ≤ x2)) b < toAntisymmetrization (fun x1 x2 ↦ x1 ≤ x2) a
⊢ ∃ a',
    (fun x1 x2 ↦ x1 < x2) a' a ∧
      toAntisymmetrization (fun x1 x2 ↦ x1 ≤ x2) a' = Quot.mk (⇑(AntisymmRel.setoid α fun x1 x2 ↦ x1 ≤ x2)) b
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

pp: case refine_3
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
a b : α
⊢ ¬r a b → ¬r b a → a = b

Tactic:
· grind [wellFounded_iff_has_min]

Goal state after:
case refine_3
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)
a b : α
⊢ ¬r a b → ¬r b a → a = b
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α : Type v
x : F (G α)
⊢ Comp.map id (mk x) = mk x

Tactic:
by simp only [Comp.map, id_map, id_map']; rfl

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 1 / a ^ n < 1 / a ^ m

Tactic:
by
  refine (one_div_lt_one_div ?_ ?_).2 (pow_lt_pow_right₀ a1 mn) <;>
    exact pow_pos (zero_lt_one.trans a1) _

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

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ ∃ c, 0 < c ∧ b * c < a

Tactic:
refine ⟨a / max (b + 1) 1, this, ?_⟩

Goal state after:
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ b * (a / max (b + 1) 1) < a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b c : α
hc₀ : 0 < c
hc : b * c < a
⊢ b < a / c

Tactic:
lt_div_iff₀ hc₀

Goal state after:
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b c : α
hc₀ : 0 < c
hc : b * c < a
⊢ b * c < a
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 < 1 / b ↔ b < 1 / a

Tactic:
by
  simpa using lt_inv_of_neg ha hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
h₁ : l₁.length = l₂.length
⊢ (a, b) ∈ (a :: l₁).zip (b :: l₂)

Tactic:
by simp [zip]

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

Goal state before:
pp: α : Type u
f : α → α
hf : Involutive f
x : α
l : List α
⊢ (∃ y, y ∈ l ∧ f y = x) → f x ∈ l

Tactic:
rintro ⟨y, h, rfl⟩; rwa [hf y]

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

Goal state before:
pp: case mpr
α : Type u
hα : Subsingleton α
⊢ Injective length

Tactic:
l1

Goal state after:
case mpr
α : Type u
hα : Subsingleton α
l1 : List α
⊢ ∀ ⦃a₂ : List α⦄, l1.length = a₂.length → l1 = a₂
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hl✝ : l ≠ []
x : M
xs : List M
hl : x :: xs ≠ []
⊢ (map (⇑f) (x :: xs)).prod = f (x :: xs).prod

Tactic:
by induction xs generalizing x <;> simp_all

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
he : e ≠ 0
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ ((n, e) ::ᵣ L).eval * ((-n, e) ::ᵣ l).eval = l'.eval

Tactic:
rw [mul_eq_eval₂ n (-n) e h]

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
he : e ≠ 0
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ ((n + -n, e) ::ᵣ l').eval = l'.eval
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
⊢ [a].alternatingProd = a

Tactic:
alternatingProd_singleton

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
⊢ a = a
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l : List α
⊢ foldlM f b l =
    foldl
      (fun mb a ↦ do
        let b ← mb
        f b a)
      (pure b) l

Tactic:
by
  suffices h :
    ∀ mb : m β, (mb >>= fun b => List.foldlM f b l) = foldl (fun mb a => mb >>= fun b => f b a) mb l
    by simp [← h (pure b)]
  induction l with
  | nil => simp
  | cons _ _ l_ih => intro; simp only [List.foldlM, foldl, ← l_ih, functor_norm]

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

Goal state before:
pp: a : ℤ
b : ℕ
⊢ (a /. ↑b)⁻¹ = ↑b /. a

Tactic:
inv_divInt

Goal state after:
a : ℤ
b : ℕ
⊢ ↑b /. a = ↑b /. a
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
x✝ : a ∣ b * ↑u
c : α
eq : b * ↑u = a * c
⊢ b = a * (c * ↑u⁻¹)

Tactic:
rw [← mul_assoc, ← eq, Units.mul_inv_cancel_right]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑n₁ / ↑↑d₁ = ↑n₂ / ↑↑d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
norm_cast at h

Goal state after:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ / ↑d₁ = ↑n₂ / ↑d₂
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n : ℕ
⊢ IsSquare ↑n ∧ IsSquare 1 ↔ IsSquare n

Tactic:
IsSquare.one,

Goal state after:
n : ℕ
⊢ IsSquare ↑n ∧ True ↔ IsSquare n
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: z : ℤ
⊢ IsSquare z ∧ IsSquare 1 ↔ IsSquare z

Tactic:
IsSquare.one,

Goal state after:
z : ℤ
⊢ IsSquare z ∧ True ↔ IsSquare z
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a✝¹ b✝¹ c : ℕ
a✝ b✝ : Q(ℕ)
depth : ℕ
a b₀ c₀ b : Q(ℕ)
p : Q(Prop)
hp : «$p» =Q («$a».pow «$b₀» = «$c₀»)
b' : ℕ := Expr.natLit! b
d : ℕ := depth >>> 1
hi : Q(ℕ)
⊢ «$p» =Q («$a».pow «$b₀» = «$c₀»)

Tactic:
by exact hp

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
x y : α
⊢ x ⊔ y = ⨆ b, bif b then x else y

Tactic:
rw [iSup_bool_eq, Bool.cond_true, Bool.cond_false]

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ u 0 ⊔ ⨆ i, u (i + 1) = ⨆ x ∈ {0} ∪ range Nat.succ, u x

Tactic:
rw [iSup_union, iSup_singleton, iSup_range]

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

Goal state before:
pp: α : Type u_1
inst✝ : SupSet α
p q : Prop
f₁ : p → α
f₂ : q → α
pq : p ↔ q
f : ∀ (x : q), f₁ ⋯ = f₂ x
⊢ iSup f₁ = iSup f₂

Tactic:
obtain rfl := propext pq

Goal state after:
α : Type u_1
inst✝ : SupSet α
p : Prop
f₁ f₂ : p → α
pq : p ↔ p
f : ∀ (x : p), f₁ ⋯ = f₂ x
⊢ iSup f₁ = iSup f₂
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set (WithTop α)
h : ¬BddAbove (some ⁻¹' s)
⊢ sSup s = ⊤

Tactic:
by_cases hmem : ⊤ ∈ s

Goal state after:
case pos
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set (WithTop α)
h : ¬BddAbove (some ⁻¹' s)
hmem : ⊤ ∈ s
⊢ sSup s = ⊤

case neg
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set (WithTop α)
h : ¬BddAbove (some ⁻¹' s)
hmem : ⊤ ∉ s
⊢ sSup s = ⊤
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ y ∈ ∅, x ≤ y
ht : ∀ y ∈ ∅, ∃ x ∈ s, y ≤ x
x : α
xs : x ∈ s
⊢ False

Tactic:
simpa using hs x xs

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
⊢ IsLUB ∅ (sSup ∅)

pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
· simp [sSup]

Goal state after:
case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s.Nonempty
⊢ IsLUB s (sSup s)
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₁
h' : b₂ < b₁
⊢ False

Tactic:
have ab := xa.trans (h ⟨xa, xb⟩).2

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₁
ab : a₁ < b₂
⊢ False
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s

Tactic:
intro x hx y hy hxy

Goal state after:
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ Icc x y ⊆ s
Module: Mathlib.Order.Antichain

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
h : r x y
⊢ False

Tactic:
| inl h =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝ : LE α
s✝ t✝ : Flag α
a : α
s t : Flag α
h : s.carrier = t.carrier
⊢ s = t

Tactic:
cases s
    cases t
    congr

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ ≤ b

Tactic:
← oneLePart_div_leOnePart b

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ ≤ b⁺ᵐ / b⁻ᵐ
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!

Tactic:
rw [ascFactorial_succ, ← Nat.add_assoc, factorial_succ, Nat.mul_comm (n + 1 + k),
      ← Nat.mul_assoc, factorial_mul_ascFactorial n k, Nat.mul_comm, Nat.add_right_comm]

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

Goal state before:
pp: ⊢ descFactorial = descFactorialBinary

Tactic:
by
  ext n k
  rw [descFactorialBinary]
  split_ifs with h
  · rw [descFactorial_of_lt h]
  · rw [← ascFactorial_eq_ascFactorialBinary, ← add_descFactorial_eq_ascFactorial']
    grind

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
⊢ |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Goal state after:
case inl
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m : ℕ
⊢ |↑m / ↑0 - ↑(round (↑m / ↑0))| = ↑(min (m % 0) (0 - m % 0)) / ↑0

case inr
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
⊢ |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n
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 : R
m : ℤ
⊢ fract (a + ↑m) = fract a

Tactic:
by
  rw [fract]
  simp

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 : R
m : ℕ
⊢ fract (a + ↑m) = fract a

Tactic:
by
  rw [fract]
  simp

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 : R
m : ℤ
⊢ fract (a - ↑m) = fract a

Tactic:
by
  rw [fract]
  simp

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 : R
n : ℕ
⊢ fract (a - ↑n) = fract a

Tactic:
by
  rw [fract]
  simp

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
⊢ (∃ z, a - b = ↑z) → fract a = fract b

Tactic:
rintro ⟨z, hz⟩

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
z : ℤ
hz : a - b = ↑z
⊢ fract a = fract b
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case mp
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
⊢ (∃ z, -x = ↑z) → ∃ z, x = ↑z

Tactic:
rintro ⟨z, hz⟩

Goal state after:
case mp
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : -x = ↑z
⊢ ∃ z, x = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
⊢ (∃ z, x = ↑z) → ∃ z, -x = ↑z

Tactic:
rintro ⟨z, hz⟩

Goal state after:
case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : x = ↑z
⊢ ∃ z, -x = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
⊢ fract (↑m / ↑n) = ↑(m % n) / ↑n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Goal state after:
case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℕ
⊢ fract (↑m / ↑0) = ↑(m % 0) / ↑0

case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
⊢ fract (↑m / ↑n) = ↑(m % n) / ↑n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Goal state after:
case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
⊢ fract (↑m / ↑0) = ↑(m % ↑0) / ↑0

case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : n > 0
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case h
K : Type u_4
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / ε < ↑n + 1

Tactic:
apply hn.trans
    simp [zero_lt_one]

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

Goal state before:
pp: case inr
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
this : ∀ (x y : G), x < y → x ∈ Ico l (l + a) → R (f x) (f y)
hx : x ∉ Ico l (l + a)
⊢ R (f x) (f y)

pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
⊢ R (f x) (f y)

Tactic:
· rcases existsUnique_sub_zsmul_mem_Ico ha x l with ⟨m, hm, -⟩
    suffices R (f (x - m • a)) (f (y - m • a)) by simpa using hR (m • b) this
    exact this _ _ (by simpa) hm

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
⊢ R (f x) (f y)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
hf : Nat.find this = 0
H : 1 < b * c
⊢ False

Tactic:
exact (H.trans <| (mul_lt_of_lt_one_right hb₀ hc₁).trans_le hb₁).false

Goal state after:
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₃) / (p₂ /ₛ p₃) = p₁ /ₛ p₂

Tactic:
rw [← sdiv_smul_eq_sdiv_div, sdiv_smul]

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

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
k : ℤ
⊢ R (f l + k • b) (f (l + a) + k • b)

Tactic:
refine hR (k • b) (hf _ ?_ _ ?_ ?_) <;> simpa

Goal state after:
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: case h.left
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x ~ l₁

Tactic:
mapₓ

Goal state after:
case h.left
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
sublist : w <+ map f l₂
x : List α
perm : map f x ~ map f l₁
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x ~ l₁
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝¹ x✝ : List α
⊢ ⟦x✝¹⟧ ≤ ⟦x✝⟧ ↔ ∀ (a : α), count a ⟦x✝¹⟧ ≤ count a ⟦x✝⟧

Tactic:
simp [subperm_iff_count]

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
this : ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'
⊢ s ≤ a ::ₘ t → s ≤ t

Tactic:
exact fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))

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

Goal state before:
pp: case mpr
α : Type u_1
s : Multiset α
⊢ Rel (fun x1 x2 ↦ x1 = x2) s s

Tactic:
exact rel_eq_refl

Goal state after: