mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ (MvPolynomial.aeval fun s ↦ (of R M) ↑s) (P₁ * P₂) = (of R M) (m₁ * m₂)

Tactic:
map_mul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ * (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) (m₁ * m₂)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) (P₁ * P₂) = (of R M) (m₁ * m₂)

Tactic:
map_mul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ * ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) (m₁ * m₂)
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
a : ℤ
ha₀ : 0 ≤ a
ha : a < ↑p
b : ℤ
hb₀ : 0 ≤ b
hb : b < ↑p
hab : ↑a = ↑b
⊢ a = b

Tactic:
lift a to ℕ using ha₀

Goal state after:
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
b : ℤ
hb₀ : 0 ≤ b
hb : b < ↑p
a : ℕ
ha : ↑a < ↑p
hab : ↑↑a = ↑b
⊢ ↑a = b
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : CharZero R
p : ℕ
hp : Nat.Prime p
⊢ ↑p ≠ 0

Tactic:
simp [hp.ne_zero]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ 2 = 0

Tactic:
← Nat.cast_two,

Goal state after:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ ↑2 = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
⊢ Surjective ⇑(quotientInfToPiQuotient I)

Tactic:
cases nonempty_fintype ι
  intro g
  choose f hf using fun i ↦ mk_surjective (g i)
  have key : ∀ i, ∃ e : R, mk (I i) e = 1 ∧ ∀ j, j ≠ i → mk (I j) e = 0 := by
    intro i
    have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
      intro j hj
      exact hI (by simpa [ne_comm, isCoprime_iff_add] using hj)
    rcases isCoprime_iff_exists.mp (isCoprime_biInf hI') with ⟨u, hu, e, he, hue⟩
    replace he : ∀ j, j ≠ i → e ∈ I j := by simpa using he
    refine ⟨e, ?_, ?_⟩
    · simp [eq_sub_of_add_eq' hue, map_sub, eq_zero_iff_mem.mpr hu]
    · exact fun j hj ↦ eq_zero_iff_mem.mpr (he j hj)
  choose e he using key
  use mk _ (∑ i, f i * e i)
  ext i
  rw [quotientInfToPiQuotient_mk', map_sum, Fintype.sum_eq_single i]
  · simp [(he i).1, hf]
  · intro j hj
    simp [(he j).2 i hj.symm]

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ ¬Odd p ↔ ¬3 ≤ p

Tactic:
not_odd_iff_even,

Goal state after:
p : ℕ
hp : Prime p
⊢ Even p ↔ ¬3 ≤ p
Module: Mathlib.Data.List.Permutation

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

Tactic:
simp only [cons_append] at ye

Goal state after:
case cons.mpr.cons
α : Type u_1
t : α
ts : List α
y : α
ys l : List α
y' : α
l₁ l₂ : List α
l0 : l₂ ≠ []
ye : y :: ys = y' :: (l₁ ++ l₂)
ih :
  ∀ {l_1 : List α},
    l ++ y' :: l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] ys fun x ↦ l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ (t :: y :: ys ++ ts) ∨
    ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁_1 ++ t :: l₂_1 ++ ts
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ IsPeriodicPt f m x

Tactic:
unfold IsPeriodicPt IsFixedPt
    convert! (hm.apply_iterate ((n / r + 1) * r - n)).eq <;>
      rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case mem.mul
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b z : A
hz : z ∈ s
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ * y✝) z ⋯ ⋯

Tactic:
| mul _ _ _ _ h₁ h₂ =>

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
⊢ minimalPeriod (f ∘ g) x ∣ (minimalPeriod f x).lcm (minimalPeriod g x)

Tactic:
rw [← isPeriodicPt_iff_minimalPeriod_dvd]

Goal state after:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
⊢ IsPeriodicPt (f ∘ g) ((minimalPeriod f x).lcm (minimalPeriod g x)) x
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case algebraMap.mul
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b : A
r : R
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p x✝ ((algebraMap R A) r) hx✝ ⋯
h₂ : p y✝ ((algebraMap R A) r) hy✝ ⋯
⊢ p (x✝ * y✝) ((algebraMap R A) r) ⋯ ⋯

Tactic:
| mul _ _ _ _ h₁ h₂ =>

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case mul
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b : A
ha : a ∈ adjoin R s
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p a x✝ ha hx✝
h₂ : p a y✝ ha hy✝
⊢ p a (x✝ * y✝) ha ⋯

Tactic:
| mul _ _ _ _ h₁ h₂ =>

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case mul
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R ↥(adjoin R s)) r)
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)
b x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p ⟨x✝, hx✝⟩
h₂ : p ⟨y✝, hy✝⟩
⊢ p ⟨x✝ * y✝, ⋯⟩

Tactic:
| mul _ _ _ _ h₁ h₂ =>

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

Goal state before:
pp: case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) - 1) % (head :: tail).length

pp: case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ idxOf a (head :: tail)

pp: case neg.e_i.h
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ (head :: tail).length

Tactic:
Nat.mod_eq_of_lt

Goal state after:
case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 = idxOf a (head :: tail) - 1

case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 < (head :: tail).length

case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ idxOf a (head :: tail)

case neg.e_i.h
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ (head :: tail).length
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case mp.zero
h : primeFactorsList 0 = []
⊢ 0 = 0 ∨ 0 = 1

Tactic:
exact Or.inl rfl

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

Goal state before:
pp: case inl
b : ℕ
hab : Coprime 0 b
⊢ (0 * b).primeFactorsList ~ primeFactorsList 0 ++ b.primeFactorsList

Tactic:
simp [(coprime_zero_left _).mp hab]

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

Goal state before:
pp: case inl
b p : ℕ
hab : Coprime 0 b
⊢ p ∈ (0 * b).primeFactorsList ↔ p ∈ primeFactorsList 0 ∪ b.primeFactorsList

Tactic:
simp [(coprime_zero_left _).mp hab]

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

Goal state before:
pp: case zero
a : ℕ
⊢ (↑a).val = a

Tactic:
exact Int.natAbs_natCast a

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

Goal state before:
pp: n a : ℕ
h : a < n
⊢ a % n = a

Tactic:
Nat.mod_eq_of_lt

Goal state after:
n a : ℕ
h : a < n
⊢ a = a

n a : ℕ
h : a < n
⊢ a < n
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
Nat.mod_eq_of_lt

Goal state after:
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑1 = 1

case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ 1 < n✝ + 1 + 1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : (H.subgroupOf L).FiniteIndex
h : H ≤ K
⊢ (K.subgroupOf L).FiniteIndex

Tactic:
exact finiteIndex_of_le <| subgroupOf_mono L h

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

Goal state before:
pp: a : ℤ
b : ℕ
⊢ ↑(a % ↑b) = ↑a

Tactic:
by
  rw [ZMod.intCast_eq_intCast_iff]
  apply Int.mod_modEq

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

Goal state before:
pp: n : ℕ
⊢ val 2 = 2 % n

Tactic:
← Nat.cast_two,

Goal state after:
n : ℕ
⊢ (↑2).val = 2 % n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisors = ∅ ↔ n = 0

Tactic:
contrapose!
  exact nonempty_divisors

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ 0 < ∑ i ∈ range n, x ^ i ↔ Odd n ∨ 0 < x + 1

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · rw [or_iff_not_imp_left, ← not_le, Nat.not_odd_iff_even]
    refine fun hn hx => h.not_ge ?_
    simpa [if_pos hn] using geom_sum_alternating_of_le_neg_one hx n
  · rintro (hn | hx')
    · exact hn.geom_sum_pos
    · exact geom_sum_pos' hx' hn

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ z.divisors = ∅ ↔ z = 0

Tactic:
contrapose!
  exact nonempty_divisors

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

Goal state before:
pp: n✝ : ℕ
a : ZMod (n✝ + 1)
| 2 * ↑a.val = 0

Tactic:
← Nat.cast_two,

Goal state after:
n✝ : ℕ
a : ZMod (n✝ + 1)
| ↑2 * ↑a.val = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
h : m < n
⊢ a.cast.val < m + 1

pp: case neg
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
h : n ≤ m
⊢ a.cast.val < m + 1

Tactic:
· obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne n)
    rw [← natCast_val, val_cast_of_lt]
    · apply a.val_lt
    apply lt_of_le_of_lt (Nat.le_of_lt_succ (ZMod.val_lt a)) h

Goal state after:
case neg
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
h : n ≤ m
⊢ a.cast.val < m + 1
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: case h
n : ℕ
⊢ (n + 1 + n).choose n + (n + 1 + n).choose (n + 1) = 2 * (n + 1 + n).choose n

Tactic:
choose_symm_add,

Goal state after:
case h
n : ℕ
⊢ (n + 1 + n).choose n + (n + 1 + n).choose n = 2 * (n + 1 + n).choose n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons.w₁
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
l : ℕ
m : l ∈ L
⊢ l < b

Tactic:
apply w₁

Goal state after:
case cons.w₁
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
l : ℕ
m : l ∈ L
⊢ l ∈ d :: L
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
L : List ℕ
⊢ ofDigits b L =
    (List.map
        (fun x ↦
          match x with
          | (a, i) => a * b ^ i)
        L.zipIdx).sum

Tactic:
List.zipIdx_eq_zip_range',

Goal state after:
b : ℕ
L : List ℕ
⊢ ofDigits b L =
    (List.map
        (fun x ↦
          match x with
          | (a, i) => a * b ^ i)
        (L.zip (List.range' 0 L.length))).sum
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b m : ℕ
hb : 1 < b
⊢ m ≠ 0 → b ^ (b.digits m).length ≤ b * m

Tactic:
by
  rcases b with (_ | _ | b) <;> simp_all [base_pow_length_digits_le']

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

Goal state before:
pp: case inl.cons
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
⊢ (p - 1) * ∑ x ∈ range (tl.length + 1), ofDigits p (List.drop x.succ (hd :: tl)) =
    ofDigits p (hd :: tl) - (hd + tl.sum)

Tactic:
simp only [ofDigits]

Goal state after:
case inl.cons
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
⊢ (p - 1) * ∑ x ∈ range (tl.length + 1), ofDigits p (List.drop x.succ (hd :: tl)) =
    ↑hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b m : ℕ
⊢ ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2

Tactic:
by
  induction m using Nat.strongRecOn with | ind n IH => ?_
  intro d hd
  rcases n with - | n
  · rw [digits_zero] at hd
    cases hd
  -- base b+2 expansion of 0 has no digits
  rw [digits_add_two_add_one] at hd
  cases hd
  · exact n.succ.mod_lt (by linarith)
  · apply IH ((n + 1) / (b + 2))
    · apply Nat.div_lt_self <;> lia
    · assumption

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

Goal state before:
pp: case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ (hd + p * ofDigits p tl) % p ^ (i + 1) = hd + p * (ofDigits p tl % p ^ i)

Tactic:
add_mod,

Goal state after:
case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ (hd % p ^ (i + 1) + p * ofDigits p tl % p ^ (i + 1)) % p ^ (i + 1) = hd + p * (ofDigits p tl % p ^ i)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ (hd + p * (ofDigits p tl % p ^ i)) % (p * p ^ i) = hd + p * (ofDigits p tl % p ^ i)

Tactic:
mod_eq_of_lt

Goal state after:
case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd + p * (ofDigits p tl % p ^ i) = hd + p * (ofDigits p tl % p ^ i)

case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd + p * (ofDigits p tl % p ^ i) < p * p ^ i
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case a
b b' : ℕ
h : b' % b = 1
n : ℕ
| n

pp: case b
b b' : ℕ
h : b' % b = 1
n : ℕ
| ofDigits 1 (b'.digits n)

Tactic:
· rw [← ofDigits_digits b' n]

Goal state after:
case b
b b' : ℕ
h : b' % b = 1
n : ℕ
| ofDigits 1 (b'.digits n)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case a
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n

pp: case b
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ofDigits c (b'.digits n)

Tactic:
· rw [← ofDigits_digits b' n]

Goal state after:
case b
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ofDigits c (b'.digits n)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: 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)
⊢ n < b * b ^ (e + 1)

Tactic:
← pow_add_one'

Goal state after:
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)
⊢ n < b ^ (e + 1 + 1)
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
hprod : d = f.prod fun x1 x2 ↦ x1 ^ x2
⊢ d.factorization ≤ n.factorization

Tactic:
rwa [hprod, factorization_prod_pow_eq_self_of_le_factorization hle]

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

Goal state before:
pp: n p : ℕ
⊢ p ^ n.factorization p ∣ n

Tactic:
by
  if hp : p.Prime then ?_ else simp [hp]
  rw [← primeFactorsList_count_eq]
  apply dvd_of_primeFactorsList_subperm (pow_ne_zero _ hp.ne_zero)
  rw [hp.primeFactorsList_pow, List.subperm_ext_iff]
  intro q hq
  simp [List.eq_of_mem_replicate hq]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
h : ¬a = 1
b : ℕ
ha : n = orderOf x * b * a.minFac
hb : a = b * a.minFac
⊢ a.minFac ∣ n

Tactic:
exact Dvd.intro_left (orderOf x * b) ha.symm

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

Goal state before:
pp: n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
pp : Prime p
⊢ n.factorization p ≤ b

Tactic:
exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)

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

Goal state before:
pp: d n : ℕ
h : d ∣ n
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
rcases eq_or_ne d 0 with (rfl | hd); · simp [zero_dvd_iff.mp h]
  rcases eq_or_ne n 0 with (rfl | hn); · simp [tsub_eq_zero_of_le]
  apply add_left_injective d.factorization
  simp only
  rw [tsub_add_cancel_of_le <| (Nat.factorization_le_iff_dvd hd hn).mpr h, ←
    Nat.factorization_mul (Nat.div_pos (Nat.le_of_dvd hn.bot_lt h) hd.bot_lt).ne' hd,
    Nat.div_mul_cancel h]

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

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

Tactic:
rintro (n_eq_zero | not_dvd)

Goal state after:
case mpr.inl
n p : ℕ
hp : Prime p
n_eq_zero : n = 0
⊢ n / p ^ n.factorization p = n

case mpr.inr
n p : ℕ
hp : Prime p
not_dvd : ¬p ∣ n
⊢ n / p ^ n.factorization p = n