mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h :
  ∀ (f_1 g_1 : R[X]),
    f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → ¬(0 < g_1.natDegree ∧ g_1.natDegree + g_1.natDegree ≤ (f * g).natDegree)
⊢ f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
simp_rw [hf.natDegree_mul hg, pos_iff_ne_zero] at h

Goal state after:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h :
  ∀ (f_1 g_1 : R[X]),
    f_1.Monic →
      g_1.Monic → f_1 * g_1 = f * g → ¬(g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree)
⊢ f.natDegree = 0 ∨ g.natDegree = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).coeff 0 = ∏ i ∈ s, (f i).coeff 0

Tactic:
by
  simpa using coeff_zero_multiset_prod (s.1.map f)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

Tactic:
by
  let f : ℕ → ℕ → R := fun m i : ℕ => (x + y) ^ i * y ^ (m - 1 - i)
  change (∑ i ∈ range n, (f n) i) * x + y ^ n = (x + y) ^ n
  induction n with
  | zero => rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
  | succ n ih =>
    have f_last : f (n + 1) n = (x + y) ^ n := by
      dsimp only [f]
      rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
    have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i := fun i hi => by
      dsimp only [f]
      have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
      rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ' y (n - 1 - i), add_tsub_cancel_right,
        ← tsub_add_eq_tsub_tsub, add_comm 1 i]
      have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
      rw [add_comm (i + 1)] at this
      rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
    rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
      (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
      pow_succ' y, mul_assoc, ← mul_add y, ih]

Goal state after:
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
α : Type u_1
s : Finset α
f : α → R
⊢ (∏ a ∈ s, (X - C (f a))).natDegree = #s

Tactic:
by
  rw [Finset.prod, ← (X - C ·).comp_def f, ← Multiset.map_map,
    natDegree_multiset_prod_X_sub_C_eq_card, Multiset.card_map, Finset.card]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
m n : ℕ
hmn : m ≤ n
⊢ (∑ i ∈ Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n

Tactic:
rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul_neg, geom_sum_mul_neg, sub_sub_sub_cancel_left]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy this : span B ↑y = ⊤
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG

Tactic:
simp_rw [eq_top_iff', mem_span_finset] at this

Goal state after:
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
this : ∀ (x : C), ∃ f, Function.support f ⊆ ↑y ∧ ∑ a ∈ y, f a • a = x
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
i : ℕ
⊢ ((∑ i ∈ range 0, X ^ i).comp (X + 1)).coeff i = ↑(Nat.choose 0 (i + 1))

Tactic:
dsimp; simp only [zero_comp, coeff_zero, Nat.cast_zero]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = p.coeff n

Tactic:
rw [h]
    rfl

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
⊢ f ∈ map C I ↔ ∀ (n : ℕ), f.coeff n ∈ I

Tactic:
constructor
  · intro hf
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
    · intro f hf n
      obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
      rw [← hx.right, coeff_C]
      by_cases h : n = 0
      · simpa [h] using hx.left
      · simp [h]
    · simp
    · exact fun f g _ _ hf hg n => by simp [I.add_mem (hf n) (hg n)]
    · intro f g _ hg n
      rw [smul_eq_mul, coeff_mul]
      exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)
  · intro hf
    rw [← sum_monomial_eq f]
    refine (I.map C : Ideal R[X]).sum_mem fun n _ => ?_
    simp only [← C_mul_X_pow_eq_monomial]
    rw [mul_comm]
    exact (I.map C : Ideal R[X]).mul_mem_left _ (mem_map_of_mem _ (hf n))

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ¬P = ⊤

Tactic:
exact h.1

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocSemiring R
s : Set R
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
closure,

Goal state after:
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set R
⊢ (sInf {S | s ⊆ ↑S}).op = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
⊢ FiniteType R (FreeAlgebra S ι)

Tactic:
by
  classical
  cases nonempty_fintype ι
  refine .trans ‹_› ⟨Finset.univ.image (FreeAlgebra.ι _), ?_⟩
  rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  exact FreeAlgebra.adjoin_range_ι ..

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.MulOpposite

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocRing R
s : Set R
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
closure,

Goal state after:
R : Type u_2
inst✝ : NonAssocRing R
s : Set R
⊢ (sInf {S | s ⊆ ↑S}).op = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
⊢ Surjective ⇑(MvPolynomial.aeval fun s ↦ of' R M ↑s)

Tactic:
by
  intro f
  induction f using induction_on with
  | of m =>
    have : m ∈ closure S := hS.symm ▸ mem_top _
    refine AddSubmonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
    · exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
    · exact ⟨1, map_one _⟩
    · rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single,
            one_mul]; rfl⟩
  | add f g ihf ihg =>
    rcases ihf with ⟨P, rfl⟩
    rcases ihg with ⟨Q, rfl⟩
    exact ⟨P + Q, map_add _ _ _⟩
  | smul r f ih =>
    rcases ih with ⟨P, rfl⟩
    exact ⟨r • P, map_smul _ _ _⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
F : Type w
inst✝⁷ : Ring R
inst✝⁶ : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ ∀ (r : R₁) (x : A ⧸ I), ((mk I).comp (algebraMap R₁ A)) r * x = x * ((mk I).comp (algebraMap R₁ A)) r

Tactic:
rintro r ⟨x⟩

Goal state after:
case mk
R : Type u
S : Type v
F : Type w
inst✝⁷ : Ring R
inst✝⁶ : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R₁
inst✝⁴ : CommSemiring R₂
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
I : Ideal A
inst✝ : I.IsTwoSided
r : R₁
x✝ : A ⧸ I
x : A
⊢ ((mk I).comp (algebraMap R₁ A)) r * Quot.mk (⇑(Submodule.quotientRel I)) x =
    Quot.mk (⇑(Submodule.quotientRel I)) x * ((mk I).comp (algebraMap R₁ A)) r
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
a : A
⊢ f.kerLift (r • (Quotient.mkₐ R₁ (ker f)) a) = r • f.kerLift ((Quotient.mkₐ R₁ (ker f)) a)

Tactic:
exact _root_.map_smul f _ _

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

Goal state before:
pp: α : Type u_1
⊢ [].permutations = [[]]

Tactic:
by
  rw [permutations, permutationsAux_nil]

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ (-↑(n + 1)) • a = a ↔ ↑(period g a) ∣ -↑(n + 1)

Tactic:
zpow_neg,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ (g ^ ↑(n + 1))⁻¹ • a = a ↔ ↑(period g a) ∣ -↑(n + 1)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h : x ∉ xs
⊢ (xs ++ [x]).nextOr x d = d

Tactic:
by
  induction xs with
  | nil => simp
  | cons z zs IH =>
    obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)
    rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.next x ⋯ = l.prev x hx

Tactic:
by
  convert! (prev_reverse_eq_next l.reverse (nodup_reverse.mpr h) x (mem_reverse.mpr hx)).symm
  exact (reverse_reverse l).symm

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ stabilizerEquivStabilizer ⋯ = MulEquiv.refl ↥(stabilizer G a)

Tactic:
ext; simp [stabilizerEquivStabilizer_apply]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.reverse.next ⋯ x ⋯ = s.prev hs x hx

Tactic:
by
  simp [← prev_reverse_eq_next]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.reverse.Nodup
x : α
hx : x ∈ s.reverse
⊢ s.reverse.next hs x hx = s.prev ⋯ x ⋯

Tactic:
by
  simp [← prev_reverse_eq_next]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
simp only [ha, hb, iff_true]

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
⊢ a * b ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relIndex ⊤ = H.index

Tactic:
← relIndex_mul_index (show H ≤ ⊤ from le_top),

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relIndex ⊤ = H.relIndex ⊤ * ⊤.index
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a b : ℕ
hab : a = b
⊢ (ringEquivCongr hab).symm = ringEquivCongr ⋯

Tactic:
subst hab
  cases a <;> rfl

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝³ : Group G
inst✝² : Group G'
H K L : Subgroup G
f : G →* G'
inst✝¹ : H.FiniteIndex
inst✝ : K.FiniteIndex
⊢ (H.prod K).FiniteIndex

Tactic:
simp_all [finiteIndex_iff]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n x₁ x₂ : ℕ
x✝ : ℕ × ℕ
x y : ℕ
hx₁ :
  (x, y) ∈
    let y := n / x₁;
    if x₁ * y = n then some (x₁, y) else none
hx₂ :
  (x, y) ∈
    let y := n / x₂;
    if x₂ * y = n then some (x₂, y) else none
⊢ x₁ = x₂

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Polynomial.Cardinal

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
h✝ : Nontrivial R
⊢ #R[X] ≤ max #R ℵ₀

Tactic:
· exact cardinalMk_eq_max.le

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
⊢ n ∈ m.divisors → n ≤ m

Tactic:
rcases m with - | m
  · simp
  · simp only [mem_divisors, Nat.succ_ne_zero m, and_true, Ne, not_false_iff]
    exact Nat.le_of_dvd (Nat.succ_pos m)

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ #n.divisors ≤ #(Ico 1 (n + 1))

Tactic:
apply card_le_card
    simp only [divisors, filter_subset]

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

Goal state before:
pp: n x : ℕ
h : x.Coprime n
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
by
  rw [Nat.Coprime, Nat.gcd_comm, Nat.gcd_rec] at h
  rw [mul_inv_eq_gcd, val_natCast, h, Nat.cast_one]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ p.properDivisors, f x = f 1

Tactic:
simp [h.properDivisors]

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

Goal state before:
pp: case inr.right
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ RightInverse inv_fun to_fun

Tactic:
· rintro ⟨x, y⟩
          fin_cases x
          simp [to_fun, inv_fun, castHom, Prod.ext_iff, eq_iff_true_of_subsingleton]

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

Goal state before:
pp: m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ (if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x.cast).cast else ((RingHom.fst (ZMod m) (ZMod n)) x.cast).cast
    else ↑↑(Nat.chineseRemainder h x.cast.1.val x.cast.2.val)) =
    x

Tactic:
conv_rhs => rw [← ZMod.natCast_zmod_val x]

Goal state after:
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ (if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x.cast).cast else ((RingHom.fst (ZMod m) (ZMod n)) x.cast).cast
    else ↑↑(Nat.chineseRemainder h x.cast.1.val x.cast.2.val)) =
    ↑x.val
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a b : ℤ
⊢ (a, b) ∈ divisorsAntidiag 1 ∨ (a, b) ∈ divisorsAntidiag 2 ∨ (a, b) ∈ divisorsAntidiag 3 ↔
    (a, b) = (1, 1) ∨
      (a, b) = (-1, -1) ∨
        (a, b) = (1, 2) ∨
          (a, b) = (2, 1) ∨
            (a, b) = (-1, -2) ∨
              (a, b) = (-2, -1) ∨ (a, b) = (1, 3) ∨ (a, b) = (3, 1) ∨ (a, b) = (-1, -3) ∨ (a, b) = (-3, -1)

Tactic:
aesop

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a b : ℤ
h₀ : a = 0 ↔ b = 0
⊢ a * b = 0 ∨
      (a, b) ∈ divisorsAntidiag 1 ∨
        (a, b) ∈ divisorsAntidiag 2 ∨ (a, b) ∈ divisorsAntidiag 3 ∨ (a, b) ∈ divisorsAntidiag 4 ↔
    (a, b) = (0, 0) ∨
      (a, b) = (1, 1) ∨
        (a, b) = (-1, -1) ∨
          (a, b) = (1, 2) ∨
            (a, b) = (2, 1) ∨
              (a, b) = (-1, -2) ∨
                (a, b) = (-2, -1) ∨
                  (a, b) = (1, 3) ∨
                    (a, b) = (3, 1) ∨
                      (a, b) = (-1, -3) ∨
                        (a, b) = (-3, -1) ∨
                          (a, b) = (4, 1) ∨
                            (a, b) = (1, 4) ∨
                              (a, b) = (-4, -1) ∨ (a, b) = (-1, -4) ∨ (a, b) = (2, 2) ∨ (a, b) = (-2, -2)

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case neg.succ.zero
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ (n + 1 + 1).choose 0 ≤ 2 ^ (n + 1)

Tactic:
rw [choose_zero_right]

Goal state after:
case neg.succ.zero
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ 1 ≤ 2 ^ (n + 1)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case pos
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : n / b = 0
⊢ n < b ∨ b ≤ 1

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case pos
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
h : b.digits m = []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

Tactic:
simp only [h, List.append_nil] at h_append ⊢

Goal state after:
case pos
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append✝ : b.digits n ++ b.digits m ≠ []
h : b.digits m = []
h_append : b.digits n ≠ []
⊢ (b.digits n).getLast ⋯ ≠ 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ.succ
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1

Tactic:
| succ e =>

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ (-↑n.natAbs) = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
zpow_neg,

Goal state after:
case inr
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : (x ^ ↑n.natAbs)⁻¹ = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e + 1
hlt : n < b ^ (e + 1)
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1

Tactic:
| succ e =>

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: a b m n✝ p n : ℕ
⊢ ∀ (a : ℕ), Prime a → (a ∣ n ∧ ¬n = 0 ↔ ¬a = 1 ∧ ¬n = 0 ∧ a ∣ n)

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: p r i : ℕ
hr : ¬p ∣ r
⊢ (p * i + r).factorization p = 0

Tactic:
apply factorization_eq_zero_of_not_dvd

Goal state after:
p r i : ℕ
hr : ¬p ∣ r
⊢ ¬p ∣ p * i + r
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun x_1 ↦ x * x_1
⊢ ¬(IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1)

Tactic:
rintro ⟨h', -⟩

Goal state after:
case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun x_1 ↦ x * x_1
h' : IsPeriodicPt (fun x_1 ↦ x * x_1) n 1
⊢ False
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ p ^ a.factorization p ∣ p ^ b.factorization p ↔ a.factorization p ≤ b.factorization p

Tactic:
obtain _ | _ | p := p

Goal state after:
case zero
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ 0 ^ a.factorization 0 ∣ 0 ^ b.factorization 0 ↔ a.factorization 0 ≤ b.factorization 0

case succ.zero
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (0 + 1) ^ a.factorization (0 + 1) ∣ (0 + 1) ^ b.factorization (0 + 1) ↔
    a.factorization (0 + 1) ≤ b.factorization (0 + 1)

case succ.succ
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (p + 1 + 1) ^ a.factorization (p + 1 + 1) ∣ (p + 1 + 1) ^ b.factorization (p + 1 + 1) ↔
    a.factorization (p + 1 + 1) ≤ b.factorization (p + 1 + 1)
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ m.factorization p = 0

Tactic:
apply factorization_eq_zero_of_not_dvd

Goal state after:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ ¬p ∣ m
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ((p ^ n).choose k).factorization p = n - k.factorization p

Tactic:
← factorization_choose_prime_pow_add_factorization hp hkn hk0

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ((p ^ n).choose k).factorization p = ((p ^ n).choose k).factorization p + k.factorization p - k.factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ∃ m, x ^ p ^ m = 1
w✝ : ℕ
hm : x ^ p ^ w✝ = 1
⊢ ∃ k, orderOf x = p ^ k

Tactic:
obtain ⟨k, _, hk⟩ := (Nat.dvd_prime_pow hp.elim).mp (orderOf_dvd_of_pow_eq_one hm)
    exact ⟨k, hk⟩

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
hk : x ^ k = 1
⊢ x ^ (m + k) = x ^ m

Tactic:
calc
      x ^ (m + k) = x ^ m * x ^ k := by rw [pow_add]
      _ = x ^ m := by simp [hk]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ ∃ k, p * k < m ∧ m < p * (k + 1)

Tactic:
mem_Ico

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : p * n + 1 ≤ m ∧ m < p * (n + 1)
⊢ ∃ k, p * k < m ∧ m < p * (k + 1)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ orderOf x ∣ i ↔ x ^ (-↑i) = 1

Tactic:
zpow_neg,

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ orderOf x ∣ i ↔ (x ^ ↑i)⁻¹ = 1
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) = ↑(n - multiplicity p k)

Tactic:
by
  push_cast
  rw [← emultiplicity_choose_prime_pow_add_emultiplicity hp hkn hk0,
    (finiteMultiplicity_iff.2 ⟨hp.ne_one, Nat.pos_of_ne_zero hk0⟩).emultiplicity_eq_multiplicity,
    (finiteMultiplicity_iff.2 ⟨hp.ne_one, choose_pos hkn⟩).emultiplicity_eq_multiplicity]
  norm_cast
  rw [Nat.add_sub_cancel_right]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ q.degree ≤ p.degree

Tactic:
exact h.1

Goal state after: