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

Goal state before:
pp: case h.inr
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
⊢ p ∈ Ideal.span ↑s

Tactic:
have hp0 : p ≠ 0 := by
            rintro rfl
            cases hn
            exact Nat.not_lt_zero _ h
          have : (0 : R) ≠ 1 := by
            intro h
            apply hp0
            ext i
            refine (mul_one _).symm.trans ?_
            rw [← h, mul_zero]
            rfl
          have : Nontrivial R := ⟨⟨0, 1, this⟩⟩
          have : p.leadingCoeff ∈ I.leadingCoeffNth N := by
            rw [HN]
            exact hm2 k ((I.mem_leadingCoeffNth _ _).2
              ⟨_, hp, hn ▸ Polynomial.degree_le_natDegree, rfl⟩)
          rw [I.mem_leadingCoeffNth] at this
          rcases this with ⟨q, hq, hdq, hlqp⟩
          have hq0 : q ≠ 0 := by
            intro H
            rw [← Polynomial.leadingCoeff_eq_zero] at H
            rw [hlqp, Polynomial.leadingCoeff_eq_zero] at H
            exact hp0 H
          have h1 : p.degree = (q * Polynomial.X ^ (k - q.natDegree)).degree := by
            rw [Polynomial.degree_mul', Polynomial.degree_X_pow]
            · rw [Polynomial.degree_eq_natDegree hp0, Polynomial.degree_eq_natDegree hq0]
              rw [← Nat.cast_add, add_tsub_cancel_of_le, hn]
              · refine le_trans (Polynomial.natDegree_le_of_degree_le hdq) (le_of_lt h)
            rw [Polynomial.leadingCoeff_X_pow, mul_one]
            exact mt Polynomial.leadingCoeff_eq_zero.1 hq0
          have h2 : p.leadingCoeff = (q * Polynomial.X ^ (k - q.natDegree)).leadingCoeff := by
            rw [← hlqp, Polynomial.leadingCoeff_mul_X_pow]
          have := Polynomial.degree_sub_lt_left h1 hp0 h2
          rw [Polynomial.degree_eq_natDegree hp0] at this
          rw [← sub_add_cancel p (q * Polynomial.X ^ (k - q.natDegree))]
          convert! (Ideal.span ↑s).add_mem _ ((Ideal.span (s : Set R[X])).mul_mem_right _ _)
          · by_cases hpq : p - q * Polynomial.X ^ (k - q.natDegree) = 0
            · rw [hpq]
              exact Ideal.zero_mem _
            refine ih _ ?_ (I.sub_mem hp (I.mul_mem_right _ hq)) rfl
            rwa [Polynomial.degree_eq_natDegree hpq, Nat.cast_lt, hn] at this
          exact hs2 ⟨Polynomial.mem_degreeLE.2 hdq, hq⟩

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

Goal state before:
pp: case h
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (q * q')) v ∈ ((aeval f) q).range ∧ ((aeval f) (p * p')) v + ((aeval f) (q * q')) v = v

Tactic:
use LinearMap.mem_range.2 ⟨aeval f q' v, by simp only [Module.End.mul_apply, aeval_mul]⟩

Goal state after:
case right
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (p * p')) v + ((aeval f) (q * q')) v = v
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: m a b c : ℤ
hc : c ≠ 0
⊢ c * a ≡ c * b [ZMOD c * m] → a ≡ b [ZMOD m]

Tactic:
by
  simp only [modEq_iff_dvd, ← Int.mul_sub]
  exact Int.dvd_of_mul_dvd_mul_left hc

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
a : R
⊢ a ∈ ker f → f a = 0

Tactic:
by simp only [mem_ker, imp_self]

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

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
⊢ x ∈ map (Quotient.mk I) (ker f) → x ∈ ker (Quotient.lift I f H)

Tactic:
· intro hx
    rw [mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective] at hx
    obtain ⟨y, hy⟩ := hx
    rw [mem_ker, ← hy.right, Ideal.Quotient.lift_mk]
    exact hy.left

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : Field R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
⊢ Function.Injective ⇑f

Tactic:
refine AlgHomClass.unitization_injective' s (fun r hr hr' ↦ ?_) f hf
  rw [Algebra.algebraMap_eq_smul_one] at hr'
  exact h1 <| inv_smul_smul₀ hr (1 : A) ▸ SMulMemClass.smul_mem r⁻¹ hr'

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

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

Tactic:
add_self_eq_zero

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
x : R
⊢ 0 = 0
Module: Mathlib.Algebra.CharP.Two

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

Tactic:
add_self_eq_zero

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x : R
⊢ 0 = 0
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: a p k : ℕ
pp : Prime p
h₁ : ¬a ∣ p ^ k
h₂ : a ∣ p ^ (k + 1)
⊢ a = p ^ (k + 1)

Tactic:
obtain ⟨l, ⟨h, rfl⟩⟩ := (dvd_prime_pow pp).1 h₂
  congr
  exact le_antisymm h (not_le.1 ((not_congr (pow_dvd_pow_iff_le_right (Prime.one_lt pp))).1 h₁))

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

Goal state before:
pp: R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Surjective ⇑f
g : A →ₐ[R] C
H : ker f.toRingHom ≤ ker g.toRingHom
x : A
⊢ (Quotient.lift (ker ↑f) (↑g) H) ((quotientKerAlgEquivOfSurjective hf).symm (f x)) = g x

Tactic:
rw [Ideal.quotientKerAlgEquivOfSurjective_symm_apply]

Goal state after:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Surjective ⇑f
g : A →ₐ[R] C
H : ker f.toRingHom ≤ ker g.toRingHom
x : A
⊢ (Quotient.lift (ker ↑f) (↑g) H) ((Quotient.mk (ker f)) x) = g x
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
S : Subalgebra R A
a : A
ha : a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))
⊢ a ∈ Algebra.adjoin R (star (↑(star S) ⊔ ↑S))

Tactic:
simpa using ha

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

Goal state before:
pp: 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
S : StarSubalgebra R A
⊢ (adjoin R s).toSubalgebra ≤ S.toSubalgebra ↔ s ⊆ ↑S

Tactic:
adjoin_toSubalgebra,

Goal state after:
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
S : StarSubalgebra R A
⊢ Algebra.adjoin R (s ∪ star s) ≤ S.toSubalgebra ↔ s ⊆ ↑S
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: 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
⊢ Subalgebra.toSubmodule (adjoin R s).toSubalgebra = span R ↑(Submonoid.closure (s ∪ star s))

Tactic:
adjoin_toSubalgebra,

Goal state after:
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
⊢ Subalgebra.toSubmodule (Algebra.adjoin R (s ∪ star s)) = span R ↑(Submonoid.closure (s ∪ star s))
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ IsPeriodicPt f (minimalPeriod f x) x

Tactic:
by
  classical
  delta minimalPeriod
  split_ifs with hx
  · exact (Nat.find_spec hx).2
  · exact isPeriodicPt_zero f x

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

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n]^[minimalPeriod f^[n] x] x = x

Tactic:
exact isPeriodicPt_minimalPeriod _ _

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

Goal state before:
pp: α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ flatMap (permutations'Aux b') (map (cons c) (permutations'Aux a' l)) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))

Tactic:
simp only [flatMap_map, permutations'Aux]

Goal state after:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ flatMap (fun a ↦ (b' :: c :: a) :: map (cons c) (permutations'Aux b' a)) (permutations'Aux a' l) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n % minimalPeriod f x] x) (f^[n % minimalPeriod f (f x)] (f x))

Tactic:
← iterate_succ_apply,

Goal state after:
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
n : ℕ
⊢ r (f^[n % minimalPeriod f x] x) (f^[(n % minimalPeriod f (f x)).succ] x)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x d z : α
zs : List α
IH : x ∉ zs → (zs ++ [x]).nextOr x d = d
h : x ∉ z :: zs
hz : ¬x = z
hzs : x ∉ zs
⊢ (z :: zs ++ [x]).nextOr x d = d

Tactic:
rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]

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

Goal state before:
pp: case inr
α : Type u_1
f : α → α
inst✝ : Finite α
h : Injective f
x : α
m n : ℕ
heq : f^[m] x = f^[n] x
hne : m ≠ n
hlt : n < m
⊢ x ∈ periodicPts f

Tactic:
exact mk_mem_periodicPts (by lia) (iterate_cancel h heq)

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < (pmap l.prev l ⋯).length
hn' : n < (l.rotate (l.length - 1)).length
⊢ (pmap l.prev l ⋯)[n] = (l.rotate (l.length - 1))[n]

Tactic:
rw [getElem_rotate, getElem_pmap, prev_getElem _ h]

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

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ (l ++ [a]).rotate 0 = l ++ [a]

Tactic:
rotate_zero

Goal state after:
α : Type u_1
l : List α
a : α
⊢ l ++ [a] = l ++ [a]
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : R
x✝ : ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
p : R
k : ℕ
hp : Prime p
hk : 0 < k
hn : p ^ k = n
⊢ p ^ (k - 1 + 1) = n

Tactic:
rwa [Nat.sub_add_cancel hk]

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

Goal state before:
pp: G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ g ^ minimalPeriod (fun x ↦ g • x) q • q = q

Tactic:
pow_smul_eq_iff_minimalPeriod_dvd

Goal state after:
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ minimalPeriod (fun x ↦ g • x) q ∣ minimalPeriod (fun x ↦ g • x) q
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ≤ 0

Tactic:
rw [primeFactorsList_zero] at h

Goal state after:
case inl
p : ℕ
h : p ∈ []
⊢ p ≤ 0
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).primeFactors = a.primeFactors ∪ b.primeFactors

Tactic:
ext; simp only [Finset.mem_union, mem_primeFactors_iff_mem_primeFactorsList,
    mem_primeFactorsList_mul ha hb]

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ Prime q

Tactic:
exact prime_of_mem_primeFactorsList hqa

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

Goal state before:
pp: n : ℕ
a : ℤ
inst✝ : NeZero n
⊢ ↑(↑a).val = a % ↑n

Tactic:
have hle : (0 : ℤ) ≤ ↑(a : ZMod n).val := Int.natCast_nonneg _

Goal state after:
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
⊢ ↑(↑a).val = a % ↑n
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
K : Subgroup G'
⊢ (H.prod K).index = H.index * K.index

Tactic:
by
  simp_rw [index, ← Nat.card_prod]
  exact Nat.card_congr (QuotientGroup.prodEquiv H K)

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

Goal state before:
pp: n : ℕ
inst✝ : Fact (1 < n)
⊢ 1 % n = 1

Tactic:
exact Nat.mod_eq_of_lt Fact.out

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

Goal state before:
pp: case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

pp: case succ.succ.inr.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 = 0
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

pp: case succ.succ.inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : 0 < x + 1
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
· have := geom_sum_alternating_of_lt_neg_one hx k.one_lt_succ_succ
    simp only [h, if_false] at this
    exact zero_lt_one.trans this

Goal state after:
case succ.succ.inr.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 = 0
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

case succ.succ.inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : 0 < x + 1
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n p : ℕ
hp : Nat.Prime p
⊢ IsUnit ↑p ↔ ¬p ∣ n

Tactic:
isUnit_iff_coprime,

Goal state after:
n p : ℕ
hp : Nat.Prime p
⊢ p.Coprime n ↔ ¬p ∣ n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: p d a : ℕ
hp : Nat.Prime p
hd : 0 < d
⊢ IsUnit ↑a ↔ ¬p ∣ a

Tactic:
isUnit_iff_coprime,

Goal state after:
p d a : ℕ
hp : Nat.Prime p
hd : 0 < d
⊢ a.Coprime (p ^ d) ↔ ¬p ∣ a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mp.succ.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = (n✝ + 1) * (0 + 1)
⊢ 2 * a.val = n✝ + 1

Tactic:
rwa [show 0 + 1 = 1 from rfl, mul_one] at he

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

Goal state before:
pp: n : ℕ
n_big : 4 ≤ n
⊢ 4 ^ n < n * n.centralBinom

Tactic:
induction n using Nat.strong_induction_on with | _ n IH
   =>  _ 

Goal state after:
case h
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
⊢ 4 ^ n < n * n.centralBinom
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
h : a.val < n + 1
⊢ a.cast.val = a.val

Tactic:
exact Fin.val_cast_of_lt h

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

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

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 [Nat.add_mod, mod_eq_of_lt hxb]

Goal state after:
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
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
n : ℕ
hn : (Nat.card α).gcd n = 1
a : α
⊢ (a ^ (↑n)⁻¹.val) ^ n = a

Tactic:
replace hn : (Nat.card α).Coprime n := hn
  rw [← pow_mul', ← pow_mod_natCard, ← ZMod.val_natCast, Nat.cast_mul, ZMod.mul_val_inv hn.symm,
    ZMod.val_one_eq_one_mod, pow_mod_natCard, pow_one]

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ (b.digits n).length = log b n + 1

Tactic:
induction n using Nat.strong_induction_on with | _ n IH
   =>  _ 

Goal state after:
case h
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
⊢ (b.digits n).length = log b n + 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ fixedLengthDigits hb 1 = Finset.image (fun x ↦ [x]) (Finset.range b)

Tactic:
by
  ext
  rw [mem_fixedLengthDigits_iff, List.length_eq_one_iff]
  grind

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
⊢ (a * b).factorization = a.factorization + b.factorization

Tactic:
by
  ext q
  rw [Finsupp.add_apply, factorization_mul_apply_of_coprime hab]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ ∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = l * b ^ (l - 1) * b.choose 2

Tactic:
rw [← List.sum_fixedLengthDigits_sum hb]

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
⊢ ∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = ∑ L ∈ List.fixedLengthDigits hb l, L.sum
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
⊢ (Injective fun n ↦ x ^ n) ↔ ¬IsOfFinOrder x

Tactic:
refine ⟨fun h => not_isOfFinOrder_of_injective_pow h, fun h n m hnm => ?_⟩
  rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, modEq_zero_iff] at hnm

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

Goal state before:
pp: m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
⊢ emultiplicity m n = ↑(#(Ico 1 (multiplicity m n + 1)))

Tactic:
simp [fin.emultiplicity_eq_multiplicity]

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p) =
    x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p))

Tactic:
rw [← mul_pow_sub_one (by lia), ← mul_pow_sub_one (n := p ^ n - k) (by lia)]

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ x * x ^ (k - 1) * (y * y ^ (p ^ n - k - 1)) * ↑((p ^ n).choose k / p) =
    x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p))
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)

Tactic:
rw [← add_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]

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

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
⊢ False

Tactic:
have : CharZero R := charP_to_charZero R

Goal state after:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
this : CharZero R
⊢ False
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_2
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n.primeFactors ⊆ k.primeFactors
⊢ n ∣ k ^ n

Tactic:
· grw [dvd_prod_primeFactors_pow_self hn, prod_dvd_prod_of_subset _ _ _ h, prod_primeFactors_dvd]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
⊢ M p

Tactic:
have wf : degree (divX p) < degree p := degree_divX_lt hp

Goal state after:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
wf : p.divX.degree < p.degree
⊢ M p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
⊢ CharP R (p ^ n)

Tactic:
obtain ⟨c, hc⟩ := CharP.exists R

Goal state after:
R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
⊢ CharP R (p ^ n)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
⊢ ∀ (a : R), (C a).natDegree = 0 ∨ M (C a)

pp: case refine_2
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
⊢ ∀ (p q : R[X]), p.natDegree = 0 ∨ M p → q.natDegree = 0 ∨ M q → (p + q).natDegree = 0 ∨ M (p + q)

pp: case refine_3
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
⊢ ∀ (n : ℕ) (a : R),
    (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n) → (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))

Tactic:
· exact fun a => Or.inl (natDegree_C _)

Goal state after:
case refine_2
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
⊢ ∀ (p q : R[X]), p.natDegree = 0 ∨ M p → q.natDegree = 0 ∨ M q → (p + q).natDegree = 0 ∨ M (p + q)

case refine_3
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
⊢ ∀ (n : ℕ) (a : R),
    (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n) → (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : FaithfulSMul R S
p : R[X]
hp : Irreducible p
hdeg : p.natDegree ≠ 1
x : S
hx : x ∈ (algebraMap R S).range
⊢ (aeval x) p ≠ 0

Tactic:
obtain ⟨_, rfl⟩ := hx

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : FaithfulSMul R S
p : R[X]
hp : Irreducible p
hdeg : p.natDegree ≠ 1
w✝ : R
⊢ (aeval ((algebraMap R S) w✝)) p ≠ 0