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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ (φ g).natDegree = fu g.natDegree

pp: case pos
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ (φ f).natDegree < (φ g).natDegree

Tactic:
gk

Goal state after:
case pos
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ fu g.natDegree = fu g.natDegree

case pos
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ (φ f).natDegree < (φ g).natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ fu f.natDegree < (φ g).natDegree

Tactic:
gk

Goal state after:
case pos
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ fu f.natDegree < fu g.natDegree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ (a * t.prod).leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod

Tactic:
Polynomial.leadingCoeff_mul'

Goal state after:
case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod

case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
⊢ ((finSuccEquiv R n) f).natDegree = degreeOf 0 f

Tactic:
rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]

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
⊢ (Multiset.map ((fun x ↦ X - C x) ∘ f) s.val).prod.natDegree = #s

Tactic:
← Multiset.map_map,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
α : Type u_1
s : Finset α
f : α → R
⊢ (Multiset.map (fun x ↦ X - C x) (Multiset.map f s.val)).prod.natDegree = #s
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x ≠ 0

Tactic:
by rwa [ne_eq]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ C r ≠ 0

Tactic:
intro h; apply (this (C_eq_zero.mp h))

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FiniteType R A ↔ ∃ ι x f, Surjective ⇑f

Tactic:
by
  constructor
  · rw [iff_quotient_freeAlgebra]
    rintro ⟨s, f, hsur⟩
    use { x : A // x ∈ s }, inferInstance, f
  · rintro ⟨ι, hfintype, f, hsur⟩
    let : Fintype ι := hfintype
    exact .of_surjective f hsur

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : c + a ≡ b + d [ZMOD n]
⊢ a ≡ b [ZMOD n]

Tactic:
add_comm b

Goal state after:
n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : c + a ≡ d + b [ZMOD n]
⊢ a ≡ b [ZMOD n]
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑(m.gcd c) ∣ b - a

Tactic:
refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_

Goal state after:
case refine_1
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m / ↑d ∣ c / ↑d * (b - a)

case refine_2
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ (m / ↑(m.gcd c)).gcd (c / ↑d) = 1
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑z.natAbs < b ∧ ↑z.natAbs ≡ a [ZMOD b]

Tactic:
by
    constructor <;> rw [natAbs_of_nonneg hz1] <;> assumption

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

Goal state before:
pp: case inr
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h✝ : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
h : p = 0
⊢ CharZero R

Tactic:
| inr h =>

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
⊢ Nat.card αˣ = Nat.card α - 1

Tactic:
rw [Nat.card_congr unitsEquivNeZero, eq_comm, ← Nat.card_congr (Equiv.sumCompl (· = (0 : α)))]
  rcases finite_or_infinite {a : α // a ≠ 0}
  · rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]
  · rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]

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

Goal state before:
pp: case cons.mpr
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts) →
    l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts

Tactic:
rintro ⟨_ | ⟨y', l₁⟩, l₂, l0, ye, rfl⟩
    · simp [ye]
    · simp only [cons_append] at ye
      rcases ye with ⟨rfl, rfl⟩
      exact Or.inr ⟨l₁, l₂, l0, by simp⟩

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

Goal state before:
pp: case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
⊢ (permutationsAux2 t ts (flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
    flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r

Tactic:
flatMap_cons,

Goal state after:
case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
⊢ (permutationsAux2 t ts (flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
    (permutationsAux2 t ts [] l id).snd ++ flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt (f ∘ g) n x

Tactic:
by
  rw [IsPeriodicPt, hco.comp_iterate]
  exact IsFixedPt.comp hf hg

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

Goal state before:
pp: α : Type u_1
f : α → α
n : ℕ
hn : 0 < n
x : α
hx : x ∈ ptsOfPeriod f n
⊢ f (f^[n.pred] x) = x

Tactic:
rw [← comp_apply (f := f), comp_iterate_pred_of_pos f hn, hx.eq]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s

Tactic:
by
  rw [← Nat.card_prod]; exact Nat.card_congr Subgroup.groupEquivQuotientProdSubgroup

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

Goal state before:
pp: α : Type u_1
s : List α
x : α
⊢ (permutations'Aux x s).Nodup ↔ ¬x ∈ s

Tactic:
refine ⟨fun h H ↦ ?_, nodup_permutations'Aux_of_notMem _ _⟩
  obtain ⟨⟨k, hk⟩, hk'⟩ := get_of_mem H
  rw [nodup_iff_injective_get] at h
  apply k.succ_ne_self.symm
  have kl : k < (permutations'Aux x s).length := by simpa [Nat.lt_succ_iff] using hk.le
  have k1l : k + 1 < (permutations'Aux x s).length := by simpa using hk
  rw [← @Fin.mk.inj_iff _ _ _ kl k1l]; apply h
  rw [get_permutations'Aux, get_permutations'Aux]
  have hl : length (s.insertIdx k x) = length (s.insertIdx (k + 1) x) := by
    rw [length_insertIdx_of_le_length hk.le, length_insertIdx_of_le_length (Nat.succ_le_of_lt hk)]
  exact ext_get hl fun n hn hn' => by grind

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
this : (n + 1 + tl.length) % (tl.length + 1) = n
⊢ (hd :: tl)[(n + 1 + ((hd :: tl).length - 1)) % (hd :: tl).length] = (hd :: tl)[n]

Tactic:
simp only [length_cons, Nat.succ_sub_succ_eq_sub, Nat.sub_zero, this]

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

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Nodup
⊢ s.Nontrivial ↔ ¬s.Subsingleton

Tactic:
length_subsingleton_iff

Goal state after:
α : Type u_1
s : Cycle α
h : s.Nodup
⊢ s.Nontrivial ↔ ¬s.length ≤ 1
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
⊢ (k + 2).primeFactorsList.prod = k + 2

Tactic:
primeFactorsList,

Goal state after:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
⊢ ((k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList).prod = k + 2
Module: Mathlib.Data.Nat.Prime.Infinite

Goal state before:
pp: ⊢ ¬BddAbove {p | Prime p}

Tactic:
rw [not_bddAbove_iff]
  intro n
  obtain ⟨p, hi, hp⟩ := exists_infinite_primes n.succ
  exact ⟨p, hp, hi⟩

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index = 2 ↔ ∃ a ∉ H, ∀ (b : G), b * a ∈ H ∨ b ∈ H

Tactic:
simp only [index_eq_two_iff, xor_iff_or_and_not_and]
  exact exists_congr fun a ↦ ⟨fun h ↦ ⟨fun ha ↦ ((h a)).2 ⟨mul_mem ha ha, ha⟩, fun b ↦ (h b).1⟩,
    fun h b ↦ ⟨h.2 b, fun h' ↦ h.1 (by simpa using mul_mem (inv_mem h'.2) h'.1)⟩⟩

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

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 1
⊢ ↑(1 % (0 + 1)) = 1

Tactic:
subsingleton [CharP.CharOne.subsingleton]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑(↑a * ↑b) = ↑↑(a * b)

Tactic:
Fin.val_mul,

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑(↑a * ↑b) = ↑(↑a * ↑b % (n✝ + 1))
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
⊢ Bijective ⇑(castHom ⋯ R)

Tactic:
by
  have : NeZero n :=
    ⟨by
      intro hn
      rw [hn] at h
      exact (Fintype.card_eq_zero_iff.mp h).elim' 0⟩
  rw [Fintype.bijective_iff_injective_and_card, ZMod.card, h, eq_self_iff_true, and_true]
  apply ZMod.castHom_injective

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
hlt : n₂ < n₁
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Tactic:
exact ⟨n₂, n₁, hlt, hle₁, he.symm⟩

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

Goal state before:
pp: case zero.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : 0 = n + 1
⊢ False

Tactic:
exact n.succ_ne_zero h.symm

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

Goal state before:
pp: n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ ↑(a * b) = ↑(Fin.cast h a * Fin.cast h b)

Tactic:
Fin.val_mul,

Goal state after:
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ ↑a * ↑b % (m + 1) = ↑(Fin.cast h a * Fin.cast h b)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ ↑a * ↑b % (m + 1) = ↑(Fin.cast h a * Fin.cast h b)

Tactic:
Fin.val_mul,

Goal state after:
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ ↑a * ↑b % (m + 1) = ↑(Fin.cast h a) * ↑(Fin.cast h b) % (n + 1)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (toAddSubgroup H).FiniteIndex ↔ H.FiniteIndex

Tactic:
simp [finiteIndex_iff, AddSubgroup.finiteIndex_iff]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_3
inst✝ : AddGroup G
H : AddSubgroup G
⊢ (AddSubgroup.toSubgroup H).FiniteIndex ↔ H.FiniteIndex

Tactic:
simp [finiteIndex_iff, AddSubgroup.finiteIndex_iff]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ map { toFun := fun d ↦ (n / d, d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal

Tactic:
by
  apply Finset.map_injective (Equiv.prodComm _ _).toEmbedding
  ext
  rw [map_swap_divisorsAntidiagonal, ← map_div_right_divisors, Finset.map_map]
  simp

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

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = ∑ i ∈ Ico 0 n.succ, a / b ^ i

Tactic:
← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _),

Goal state after:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = ∑ i ∈ insert 0 (Ico (0 + 1) n.succ), a / b ^ i
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case pos
n k : ℕ
lt : n + 1 < k
⊢ (n + 1).choose k ≤ 2 ^ n

pp: case neg
n k : ℕ
lt : ¬n + 1 < k
⊢ (n + 1).choose k ≤ 2 ^ n

Tactic:
· simp [choose_eq_zero_of_lt lt]

Goal state after:
case neg
n k : ℕ
lt : ¬n + 1 < k
⊢ (n + 1).choose k ≤ 2 ^ n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
⊢ a.cast.cast = a

Tactic:
have : NeZero n := ⟨((Nat.zero_lt_of_ne_zero hm.out).trans_le h).ne'⟩

Goal state after:
m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
this : NeZero n
⊢ a.cast.cast = a
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.e_tail.e_a
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) / (b + 2) = n✝ + 1

Tactic:
· simp [add_mul_div_left, div_eq_of_lt hxb]

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

Goal state before:
pp: case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ x.natAbs ≤ (↑n * m + x).natAbs

Tactic:
apply hl.trans

Goal state after:
case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 ≤ (↑n * m + x).natAbs
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n ≃+* R
⊢ f = g

Tactic:
rw [RingEquiv.coe_ringHom_inj_iff]

Goal state after:
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n ≃+* R
⊢ ↑f = ↑g
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₂ : k ≤ n
a : ℕ
ha : n = k + a
H₁ : m ∣ a
⊢ ∃ y, n = k + m * y

Tactic:
obtain ⟨b, rfl⟩ := H₁

Goal state after:
case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₂ : k ≤ n
b : ℕ
ha : n = k + m * b
⊢ ∃ y, n = k + m * y
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
n : ℕ
⊢ (fun p ↦ p.1.val + N * p.2) ((fun n ↦ (↑n, n / N)) n) = n

Tactic:
simpa only [val_natCast] using mod_add_div n N

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

Goal state before:
pp: case pos
b k : ℕ
hb : 1 < b
n : ℕ
h : n = 0
⊢ (b.digits n).length ≤ k ↔ n < b ^ k

pp: case neg
b k : ℕ
hb : 1 < b
n : ℕ
h : ¬n = 0
⊢ (b.digits n).length ≤ k ↔ n < b ^ k

Tactic:
· have : 0 < b ^ k := by positivity
    simpa [h]

Goal state after:
case neg
b k : ℕ
hb : 1 < b
n : ℕ
h : ¬n = 0
⊢ (b.digits n).length ≤ k ↔ n < b ^ k
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n : ℕ
⊢ digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits

Tactic:
induction n using Nat.binaryRecFromOne with

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (b.digitsAppend l) ↑(Finset.range (b ^ l)) ↑(fixedLengthDigits hb l)

Tactic:
rw [fixedLengthDigits, Set.coe_toFinset]
  convert! bijOn_digitsAppend hb l
  ext; simp

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
⊢ b.factorization ≤ (a * b).factorization

Tactic:
by
  rw [mul_comm]
  apply factorization_le_factorization_mul_left ha

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

Goal state before:
pp: case pos
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : n = 0
⊢ n = 0 ∨ ¬p ∣ n

Tactic:
simp [n_zero]

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

Goal state before:
pp: case hf
n k : ℕ
hkn : k ≤ n
⊢ ∀ x ∈ Finset.range (n + 1),
    x ∉ (n.choose k).factorization.support → (fun x1 x2 ↦ x1 ^ x2) x ((n.choose k).factorization x) = 1

Tactic:
· intro p _ h2
    simp [Classical.not_not.1 (mt Finsupp.mem_support_iff.2 h2)]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ m = x ^ n ↔ n ≡ m [MOD orderOf x]

Tactic:
Nat.ModEq.comm,

Goal state after:
case inr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ m = x ^ n ↔ m ≡ n [MOD orderOf x]
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ (a.gcd b).factorization = a.factorization ⊓ b.factorization

Tactic:
by
  suffices (a.factorization ⊓ b.factorization).prod (· ^ ·) = gcd a b by
    rw [← this, factorization_prod_pow_eq_self_of_le_factorization inf_le_left]
  apply gcd_greatest
  · exact prod_pow_dvd_of_le_factorization inf_le_left
  · exact prod_pow_dvd_of_le_factorization inf_le_right
  · intro e hea heb
    rcases eq_or_ne e 0 with (rfl | he_pos)
    · exact absurd (zero_dvd_iff.mp hea) ha_pos
    apply dvd_prod_pow_of_factorization_le he_pos
    have hea' := (factorization_le_iff_dvd he_pos ha_pos).mpr hea
    have heb' := (factorization_le_iff_dvd he_pos hb_pos).mpr heb
    simp [hea', heb']

Goal state after:
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ x ^ p + y ^ p + ↑p * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p) - y ^ p

Tactic:
add_right_comm,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ x ^ p + ↑p * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p) + y ^ p - y ^ p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
x : G
⊢ (Injective fun n ↦ x ^ n) → ¬IsOfFinOrder x

Tactic:
simp_rw [isOfFinOrder_iff_pow_eq_one]
    rintro h ⟨n, hn, hx⟩
    exact Nat.cast_ne_zero.2 hn.ne' (h <| by simpa using hx)

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k) = ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}))

Tactic:
have h₁ :
      emultiplicity p (choose (n + k) k) + emultiplicity p (k ! * n !) =
        #{i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i} + emultiplicity p (k ! * n !) := by
    rw [← hp.emultiplicity_mul, ← mul_assoc]
    have := (add_tsub_cancel_right n k) ▸ choose_mul_factorial_mul_factorial (le_add_left k n)
    rw [this, hp.emultiplicity_factorial hnb, hp.emultiplicity_mul,
      hp.emultiplicity_factorial ((log_mono_right (le_add_left k n)).trans_lt hnb),
      hp.emultiplicity_factorial ((log_mono_right (le_add_left n k)).trans_lt
      (add_comm n k ▸ hnb)), multiplicity_choose_aux hp (le_add_left k n)]
    simp [add_comm]
  refine WithTop.add_right_cancel ?_ h₁
  apply finiteMultiplicity_iff_emultiplicity_ne_top.1
  exact Nat.finiteMultiplicity_iff.2 ⟨hp.ne_one, mul_pos (factorial_pos k) (factorial_pos n)⟩

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

Goal state before:
pp: n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
i : ℕ
⊢ p ^ i ∣ n → 1 ≤ i → (i < n ↔ i < b)

Tactic:
refine fun h1 h2 ↦ ⟨fun h ↦ ?_, fun h ↦ lt_of_pow_dvd_right hn (Prime.one_lt pp) h1⟩

Goal state after:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
i : ℕ
h1 : p ^ i ∣ n
h2 : 1 ≤ i
h : i < n
⊢ i < b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case zero
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
pp : Prime 0
hb : n < 0 ^ b
h1 : 0 ^ i ∣ n
⊢ i < b

Tactic:
zero_pow (by lia),

Goal state after:
case zero
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
pp : Prime 0
hb : n < 0 ^ b
h1 : 0 ∣ n
⊢ i < b