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

Goal state before:
pp: case refine_3.add
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝⁴ : AddCommMonoid M
x✝³ : Module R M
x✝² : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝¹ : ↥M'
x✝ x y : M
hx✝ : x ∈ span (↥A) (Set.range mj)
hy✝ : y ∈ span (↥A) (Set.range mj)
hx : x ∈ ((↑↥A f).domRestrict N').range
hy : y ∈ ((↑↥A f).domRestrict N').range
⊢ x + y ∈ ((↑↥A f).domRestrict N').range

Tactic:
exact add_mem hx hy

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

Goal state before:
pp: a b : ℕ
⊢ ↑a * a.gcdA b ≡ ↑(a.gcd b) [ZMOD ↑b]

Tactic:
rw [← add_zero ((a : ℤ) * _), Nat.gcd_eq_gcd_ab]
  exact (dvd_mul_right _ _).zero_modEq_int.add_left _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
l : Multiset R
⊢ l.sum * l.sum = (Multiset.map (fun x ↦ x * x) l).sum

Tactic:
by simp_rw [← pow_two, multiset_sum_sq]

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

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

Tactic:
· exact ⟨y :: l₁, l₂, l0, by simp⟩

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
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
hb : b ∈ adjoin R s
⊢ p a b ha hb

Tactic:
by
  induction hb using adjoin_induction with
  | mem z hz => induction ha using adjoin_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | algebraMap _ => exact algebraMap_left _ _ hz
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | star _ _ h => exact star_left _ _ _ _ h
  | algebraMap r =>
    induction ha using adjoin_induction with
    | mem _ h => exact algebraMap_right _ _ h
    | algebraMap _ => exact algebraMap_both _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | star _ _ h => exact star_left _ _ _ _ h
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
  | star _ _ h => exact star_right _ _ _ _ h

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

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℕ
⊢ a ^ (n % minimalPeriod (fun x ↦ a • x) b) • b = a ^ n • b

Tactic:
rw [← period_eq_minimalPeriod, pow_mod_period_smul]

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 α
inst✝ : Subsingleton α
x : α
⊢ ∀ (m : G), m • x = x

Tactic:
hx

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Subsingleton α
x : α
hx : G
⊢ hx • x = x
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l[(k + 1) % l.length] = (l.rotate n).next l[k] ⋯

Tactic:
getElem_eq_getElem_rotate _ n k

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l[(k + 1) % l.length] = (l.rotate n).next (l.rotate n)[(l.length - n % l.length + k) % l.length] ⋯
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : IsPretransitive G α
a b : orbitRel.Quotient G α
⊢ a = b

Tactic:
refine Quot.inductionOn a (fun x ↦ ?_)
    exact Quot.inductionOn b (fun y ↦ Quot.sound <| exists_smul_eq G y x)

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

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
⊢ x ∈ s → x ∈ g • s

Tactic:
hx

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ x ∈ g • s
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α) (a :: l) []
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
have := isRotated_nil_iff.1 hab
        contradiction

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
x : R
n : ℕ
_hn : 0 < n
⊢ x ^ n = 0 → ¬Prime x

Tactic:
hx

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime x
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
⊢ RightInverse (fun q ↦ q.liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯) fun q ↦ Quotient.liftOn' q (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯

Tactic:
simp only [Function.RightInverse, LeftInverse]

Goal state after:
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
⊢ ∀ (x : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))),
    Quotient.liftOn' (x.liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯) (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯ = x
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
⊢ a.primeFactorsList.Disjoint b.primeFactorsList

Tactic:
intro q hqa hqb

Goal state after:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ False
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ((H ⊓ K).subgroupOf K).index = (H.subgroupOf K).index

Tactic:
inf_subgroupOf_right

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H.subgroupOf K).index = (H.subgroupOf K).index
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: p m n : ℕ
h : n ≤ m
⊢ ↑p ^ m = 0

Tactic:
obtain ⟨q, rfl⟩ := Nat.exists_eq_add_of_le h

Goal state after:
p n q : ℕ
h : n ≤ n + q
⊢ ↑p ^ (n + q) = 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case inl
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⟩

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 = n
⊢ ZMod m ≃+* ZMod n

Tactic:
by
  rcases m with - | m <;> rcases n with - | n
  · exact RingEquiv.refl _
  · exfalso
    exact n.succ_ne_zero h.symm
  · exfalso
    exact m.succ_ne_zero h
  · exact
      { finCongr h with
        map_mul' := fun a b => by
          dsimp [ZMod]
          ext
          rw [Fin.val_cast, Fin.val_mul, Fin.val_mul, Fin.val_cast, Fin.val_cast, ← h]
        map_add' := fun a b => by
          dsimp [ZMod]
          ext
          rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h] }

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

Goal state before:
pp: a : ℕ
x : ZMod a
⊢ (ringEquivCongr ⋯) x = x

Tactic:
rw [ringEquivCongr_refl]
  rfl

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

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x * y).cast = (↑(x.cast * y.cast)).cast

Tactic:
Int.cast_mul,

Goal state after:
n : ℕ
x y : ZMod n
⊢ (x * y).cast = (↑x.cast * ↑y.cast).cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1

Tactic:
rw [Fin.coe_neg_one]

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

Goal state before:
pp: case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ ↑↑z.val + ↑(↑p * k) = z

Tactic:
Int.cast_mul,

Goal state after:
case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ ↑↑z.val + ↑↑p * ↑k = z
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
x : ℕ
⊢ x ∈ m.divisors → x ∈ n.properDivisors

Tactic:
hx

Goal state after:
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
x : ℕ
hx : x ∈ m.divisors
⊢ x ∈ n.properDivisors
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
⊢ Nontrivial (ZMod 0)

Tactic:
by
  delta ZMod; infer_instance

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : Even n
ihn : ∑ i ∈ range n, x ^ i < 0
⊢ 1 < x * ∑ i ∈ range n, x ^ i + 1

pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0

Tactic:
· rw [lt_add_iff_pos_left]
    exact mul_pos_of_neg_of_neg hx0 ihn

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ⇑(Equiv.prodComm ℕ ℕ).toEmbedding '' ↑n.divisorsAntidiagonal = ↑n.divisorsAntidiagonal

Tactic:
Equiv.coe_toEmbedding,

Goal state after:
n : ℕ
⊢ ⇑(Equiv.prodComm ℕ ℕ) '' ↑n.divisorsAntidiagonal = ↑n.divisorsAntidiagonal
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
H : IsUnit ↑m
H' : (↑H.unit).val.Coprime n
⊢ m.Coprime n

Tactic:
IsUnit.unit_spec,

Goal state after:
m n : ℕ
H : IsUnit ↑m
H' : (↑m).val.Coprime n
⊢ m.Coprime n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
⊢ x ∈ ↑n.divisors → ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑n.divisors → n / x = n / x₂ → x = x₂

Tactic:
hx

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ ↑n.divisors
⊢ ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑n.divisors → n / x = n / x₂ → x = x₂
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag = z.divisorsAntidiag

Tactic:
ext; simp [mem_divisorsAntidiag, mul_comm]

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

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (n + (a.val - b.val)) % n = a.val - b.val

Tactic:
Nat.add_mod_left

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a.val - b.val) % n = a.val - b.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Nontrivial G
inst✝ : Module (ZMod 1) G
x : G
hx : x ≠ 0
⊢ False

Tactic:
exact hx <| by simpa using char_nsmul_eq_zero 1 x

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

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

Tactic:
← pow_mul',

Goal state after:
α : Type u_1
inst✝ : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
⊢ a ^ (n * (↑n)⁻¹.val) = a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
M : Type u_1
inst✝ : AddCommMonoid M
n : ℕ
m1 m2 : Module (ZMod (n + 1)) M
m : M
r : ℕ
⊢ ↑r • m = ↑r • m

Tactic:
rw [(letI := m1; Nat.cast_smul_eq_nsmul _ r m), Nat.cast_smul_eq_nsmul _ r m]

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

Goal state before:
pp: case succ
n b : ℕ
⊢ ofDigits (b + 1) ((b + 1).digits n) = n

Tactic:
· rcases b with - | b
    · induction n with
      | zero => rfl
      | succ n ih =>
        rw [Nat.zero_add] at ih ⊢
        simp only [ih, add_comm 1, ofDigits_one_cons, Nat.cast_id, digits_one_succ]
    · induction n using Nat.strongRecOn with | ind n h => ?_
      cases n
      · rw [digits_zero]
        rfl
      · simp only [digits_add_two_add_one]
        dsimp [ofDigits]
        rw [h _ (Nat.div_lt_self' _ b)]
        rw [Nat.mod_add_div]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hf : FiniteMultiplicity a b
⊢ multiplicity a b < k ↔ ¬a ^ k ∣ b

Tactic:
rw [hf.pow_dvd_iff_le_multiplicity, not_le]

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

Goal state before:
pp: n b e : ℕ
h_b_pos : 0 < b
⊢ n < b ^ e.succ → n / b < b ^ e

Tactic:
by
  simp only [Nat.pow_succ]
  exact (@Nat.div_lt_iff_lt_mul b n (b ^ e) h_b_pos).mpr

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

Goal state before:
pp: case ind
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
i : ℕ
⊢ ((b + 2).digits n.succ)[i]?.getD 0 = n.succ / (b + 2) ^ i % (b + 2)

Tactic:
rcases i with _ | i

Goal state after:
case ind.zero
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ ((b + 2).digits n.succ)[0]?.getD 0 = n.succ / (b + 2) ^ 0 % (b + 2)

case ind.succ
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
i : ℕ
⊢ ((b + 2).digits n.succ)[i + 1]?.getD 0 = n.succ / (b + 2) ^ (i + 1) % (b + 2)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
⊢ emultiplicity a b ≤ emultiplicity c d

Tactic:
unfold emultiplicity

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
⊢ (if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤) ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
⊢ x ∈ d :: L → x < b

Tactic:
hx

Goal state after:
case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hx : x ∈ d :: L
⊢ x < b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
rw [add_comm, ha.multiplicity_add_of_gt hab, min_eq_left]

Goal state after:
case inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p a ≤ multiplicity p b
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: p : ℕ
hp : Prime p
q : ℕ
⊢ p.factorization q = (single p 1) q

Tactic:
rw [← primeFactorsList_count_eq, primeFactorsList_prime hp, single_apply, count_singleton',
    if_congr eq_comm]

Goal state after:
case h_t
p : ℕ
hp : Prime p
q : ℕ
⊢ 1 = ?m.41

case h_e
p : ℕ
hp : Prime p
q : ℕ
⊢ 0 = ?m.42

p : ℕ
hp : Prime p
q : ℕ
⊢ ℕ

p : ℕ
hp : Prime p
q : ℕ
⊢ ℕ
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h✝ : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ (x ^ n) ^ m = x

Tactic:
by rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]

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

Goal state before:
pp: case refine_1
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p ∣ p * i + r

Tactic:
← Nat.dvd_add_iff_right (dvd_mul_right p i)

Goal state after:
case refine_1
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p ∣ r
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: α : Type u_1
p : ℕ
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (∑ x ∈ S, (g x).factorization) p = ∑ x ∈ S, (g x).factorization p

Tactic:
finsetSum_apply

Goal state after:
α : Type u_1
p : ℕ
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ ∑ i ∈ S, (g i).factorization p = ∑ x ∈ S, (g x).factorization p
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case insert
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
a : β
s : Finset β
has : a ∉ s
ih : emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)
⊢ emultiplicity p (∏ x ∈ insert a s, f x) = ∑ x ∈ insert a s, emultiplicity p (f x)

Tactic:
| insert a s has ih =>

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

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ (p - 1) * n !.factorization p = n - (p.digits n).sum

Tactic:
by
  simp only [factorization_factorial hp <| lt_succ_of_lt <| Nat.lt_add_one (log p n),
    ← Finset.sum_Ico_add' _ 0 _ 1, Ico_zero_eq_range,
    ← sub_one_mul_sum_log_div_pow_eq_sub_sum_digits]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(Finset.image (fun x ↦ a ^ x) (Finset.range (orderOf a)))).Finite

Tactic:
exact Finset.finite_toSet _

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ 1 ^ i = 1

Tactic:
one_zpow

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ 1 = 1
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n + 1 = 0

Tactic:
nth_rw 2 [← one_pow (p ^ n)]

Goal state after:
R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n + 1 ^ p ^ n = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
⊢ x ^ n ≠ 1

Tactic:
hx

Goal state after:
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ False
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
r : R
x✝ : (expand R 1) (C r * X ^ n) = C r * X ^ n
⊢ (expand R 1) (C r * X ^ (n + 1)) = C r * X ^ (n + 1)

Tactic:
rw [map_mul, expand_C, map_pow, expand_X, pow_one]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
⊢ x ∈ ↑(antidiagonal n) →
    ∀ ⦃x₂ : ℕ × ℕ⦄, x₂ ∈ ↑(antidiagonal n) → (fun x ↦ (x.1 * p, x.2 * p)) x = (fun x ↦ (x.1 * p, x.2 * p)) x₂ → x = x₂

Tactic:
hx

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
hx : x ∈ ↑(antidiagonal n)
⊢ ∀ ⦃x₂ : ℕ × ℕ⦄, x₂ ∈ ↑(antidiagonal n) → (fun x ↦ (x.1 * p, x.2 * p)) x = (fun x ↦ (x.1 * p, x.2 * p)) x₂ → x = x₂
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective ⇑S.val
| S.val ((aeval x) p) = S.val 0

Tactic:
map_zero

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective ⇑S.val
| S.val ((aeval x) p) = 0
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree < q.natDegree

Tactic:
by_cases h0 :
    C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree < q.natDegree

case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree < q.natDegree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] p = ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x

Tactic:
by
  conv_lhs => rw [(derivative^[k] p).as_sum_support_C_mul_X_pow]
  refine sum_congr rfl fun i _ ↦ ?_
  rw [coeff_iterate_derivative, Nat.descFactorial_eq_factorial_mul_choose]

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ p.natDegree - 1 + 1 ∈ p.support

Tactic:
tsub_add_cancel_of_le (by lia),

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ p.natDegree ∈ p.support