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

Goal state before:
pp: case refine_2.mem.inl
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✝ x : ↥N
hx : x = n
⊢ f n ∈ M'

Tactic:
hn

Goal state after:
case refine_2.mem.inl
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✝ x : ↥N
hx : x = n
⊢ 0 ∈ M'
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: case inr
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Odd n
⊢ ↑n = 0 ↔ 2 ∣ n

Tactic:
· simp_rw [hn.not_two_dvd_nat, iff_false]
      rwa [natCast_eq_one_of_odd_of_two_eq_zero hn h₂]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R 2
inst✝ : NoZeroDivisors R
x y : R
h : (fun x ↦ x ^ 2) x = (fun x ↦ x ^ 2) y
⊢ x = y

Tactic:
rwa [← CharTwo.add_eq_zero, ← add_sq, pow_eq_zero_iff two_ne_zero, CharTwo.add_eq_zero] at h

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 ≤ S ↔ s ⊆ ↑S

Tactic:
rw [← toSubalgebra_le_iff, adjoin_toSubalgebra, Algebra.adjoin_le_iff, coe_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
⊢ s ∪ star s ⊆ ↑S ↔ s ⊆ ↑S
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
⊢ (t :: ts).permutationsAux is =
    foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is)) is.permutations

Tactic:
by
  rw [permutationsAux, permutationsAux.rec]; rfl

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x

Tactic:
rw [add_comm] at hn
  exact hn.left_of_add hm

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ minimalPeriod f x = 1 ↔ IsFixedPt f x

Tactic:
by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [← iterate_one f]
    refine Function.IsPeriodicPt.isFixedPt ?_
    rw [← h]
    exact isPeriodicPt_minimalPeriod f x
  · exact
      ((h.isPeriodicPt 1).minimalPeriod_le Nat.one_pos).antisymm
        (Nat.succ_le_of_lt ((h.isPeriodicPt 1).minimalPeriod_pos Nat.one_pos))

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
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x

Tactic:
apply Coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd h)

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x * (n / (minimalPeriod f x).gcd n)
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
n : ℕ
⊢ n ∈ List.range (minimalPeriod f x) → f^[m] x = f^[n] x → m = n

Tactic:
hn

Goal state after:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
n : ℕ
hn : n ∈ List.range (minimalPeriod f x)
⊢ f^[m] x = f^[n] x → m = n
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f : α → α
inst✝ : Finite α
h : periodicPts f = univ
⊢ Surjective f

Tactic:
← range_eq_univ,

Goal state after:
α : Type u_1
f : α → α
inst✝ : Finite α
h : periodicPts f = univ
⊢ range f = univ
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (l₁ == l₂) = true ↔ decide (l₁ = l₂) = true

Tactic:
@beq_iff_eq _ (_),

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₁ = l₂ ↔ decide (l₁ = l₂) = true
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
head✝ : α
tail✝ : List α
h : x ∈ y :: z :: head✝ :: tail✝
⊢ (y :: z :: head✝ :: tail✝).prev x h = y

Tactic:
rw [prev, dif_neg hy, if_pos hz]

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

Goal state before:
pp: α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
⊢ m < (as.insertIdx n x).length

Tactic:
length_insertIdx_of_le_length hn,

Goal state after:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
⊢ m < as.length + 1
Module: Mathlib.Data.List.Cycle

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

Tactic:
hn

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < (pmap l.prev l ⋯).length
⊢ ∀ (h₂ : n < (l.rotate (l.length - 1)).length), (pmap l.prev l ⋯)[n] = (l.rotate (l.length - 1))[n]
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : R
hn✝ : IsPrimePow n
k : ℕ
hk : k ≠ 0
p : R
k' : ℕ
hp : Prime p
hk' : 0 < k'
hn : p ^ k' = n
⊢ (p ^ k') ^ k = n ^ k

Tactic:
hn

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : R
hn✝ : IsPrimePow n
k : ℕ
hk : k ≠ 0
p : R
k' : ℕ
hp : Prime p
hk' : 0 < k'
hn : p ^ k' = n
⊢ n ^ k = n ^ k
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
simp only [isPrimePow_def, Nat.prime_iff]

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

Goal state before:
pp: case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (c :: (s ++ [a])).rotate d = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
← hd c _ _ _ hn

Goal state after:
case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (c :: (s ++ [a])).rotate d = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (c :: (s ++ [a]) ++ [c])
Module: Mathlib.Data.List.Prime

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
⊢ a ∣ (a :: l₁).prod

Tactic:
rw [prod_cons]; exact dvd_mul_right _ _

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

Goal state before:
pp: case cons
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : Chain r₁ ↑(a✝¹ :: l✝)
⊢ Chain r₂ ↑(a✝¹ :: l✝)

Tactic:
· rw [chain_coe_cons] at p ⊢
    exact p.imp H

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

Goal state before:
pp: case mp
n : ℕ
⊢ n ≠ 0 ∧ n ≠ 1 → n.primeFactors.Nonempty

Tactic:
rintro hn

Goal state after:
case mp
n : ℕ
hn : n ≠ 0 ∧ n ≠ 1
⊢ n.primeFactors.Nonempty
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate n a <+~ (a ^ n * c).primeFactorsList

Tactic:
ih hb.2

Goal state after:
case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ a ^ n ∣ a ^ n * c
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑a.cast = a

Tactic:
dsimp [ZMod.cast]

Goal state after:
case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑↑a.val = a
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
hn : n = 0
⊢ False

Tactic:
hn

Goal state after:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = 0
hn : n = 0
⊢ False
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
rw [← ZMod.intCast_eq_intCast_iff', Int.cast_natCast, ZMod.natCast_val, ZMod.cast_id]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
h : x ∈ n.divisorsAntidiagonal
⊢ x.2 ∈ n.divisors

Tactic:
by
  rw [mem_divisorsAntidiagonal] at h
  simp [Dvd.intro_left _ h.1, h.2]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
rcases Decidable.eq_or_ne n 0 with (rfl | hn)

Goal state after:
case inl
⊢ ∑ i ∈ divisors 0, i = ∑ i ∈ properDivisors 0, i + 0

case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f (n / i) i

Tactic:
by
  rw [← map_swap_divisorsAntidiagonal, Finset.prod_map]
  exact prod_divisorsAntidiagonal fun i j => f j i

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ ↑n.divisors
y : ℕ
hy : y ∈ ↑n.divisors
h : n / x = n / y
⊢ x = y

Tactic:
rw [mem_coe, mem_divisors] at hx hy

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∣ n ∧ n ≠ 0
y : ℕ
hy : y ∣ n ∧ n ≠ 0
h : n / x = n / y
⊢ x = y
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b x : ℕ
hx : x ≠ 0
hxb : x < b
⊢ b.digits x = [x]

Tactic:
rcases exists_eq_succ_of_ne_zero hx with ⟨x, rfl⟩
  rcases Nat.exists_eq_add_of_le' ((Nat.le_add_left 1 x).trans_lt hxb) with ⟨b, rfl⟩
  rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : NonAssocRing R
n✝ : ℕ
f : R →+* ZMod (n✝ + 1)
k : ZMod (n✝ + 1)
⊢ f k.cast = k

Tactic:
dsimp [ZMod.cast]

Goal state after:
case succ
R : Type u_1
inst✝ : NonAssocRing R
n✝ : ℕ
f : R →+* ZMod (n✝ + 1)
k : ZMod (n✝ + 1)
⊢ f ↑k.val = k
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
simp only [add_comm p.1.val, mul_add_div (NeZero.pos _),
        (Nat.div_eq_zero_iff).2 <| .inr p.1.val_lt, add_zero]

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

Goal state before:
pp: b : ℕ
l : List ℕ
this :
  List.zipWith (fun a i ↦ a * b ^ (i + 1)) l (List.range l.length) =
    List.zipWith (fun a i ↦ b * (a * b ^ i)) l (List.range l.length)
⊢ (List.zipWith (fun a i ↦ a * b ^ (i + 1)) l (List.range l.length)).sum =
    b * (List.zipWith (fun a i ↦ a * b ^ i) l (List.range l.length)).sum

Tactic:
by simp [this]

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

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

Tactic:
IH _ this h,

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

Goal state before:
pp: b n : ℕ
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
rcases Decidable.eq_or_ne n 0 with (rfl | hn)

Goal state after:
case inl
b : ℕ
⊢ (b.digits 0).length ≤ (b.digits (0 + 1)).length

case inr
b n : ℕ
hn : n ≠ 0
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n ≤ emultiplicity a b
⊢ n ≤ multiplicity a b

Tactic:
rw [emultiplicity_eq_multiplicity hfin] at h
  assumption_mod_cast

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n < emultiplicity a b
⊢ n < multiplicity a b

Tactic:
rw [emultiplicity_eq_multiplicity hfin] at h
  assumption_mod_cast

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ y ^ n = 1

Tactic:
by rw [← isConj_one_right, ← eq']; exact h.pow n

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]

Tactic:
modEq_zero_iff_dvd,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ n = 1 ↔ orderOf x ∣ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
⊢ (n / q ^ n.factorization q).factorization q = (Finsupp.erase q n.factorization) q

Tactic:
simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ordCompl pp hn]
    simp

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

Goal state before:
pp: n : ℕ
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
by_cases hn : n = 0
  · subst hn
    simp
  · simpa [prod_primeFactorsList hn] using (n.primeFactorsList : Multiset ℕ).toFinset_prod_dvd_prod

Goal state after:
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 ^ p ^ n = 0

Tactic:
← add_pow_expChar_pow_of_commute _ _ (Commute.one_right _),

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

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
g : G
ha : g ≠ 1
⊢ orderOf g ≤ 1

Tactic:
rw [ne_eq, ← isOfFinOrder_iff_eq_one, ← orderOf_eq_zero_iff] at ha
    simp [ha]

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

Goal state before:
pp: case refine_1
h2 : _root_.Prime 2
⊢ 0 ≠ 0 → emultiplicity 2 0! < ↑0

Tactic:
exact fun h => False.elim <| h rfl

Goal state after:
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 : ℕ
⊢ 0 < n → x ^ n ≠ 1

Tactic:
hn

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
⊢ x ^ n ≠ 1
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ¬p.divX = 0

Tactic:
divX_eq_zero_iff

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ¬p = C (p.coeff 0)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ ((expand R p) f).coeff n = if p ∣ n then f.coeff (n / p) else 0

Tactic:
simp only [expand_eq_sum]
  simp_rw [coeff_sum, ← pow_mul, C_mul_X_pow_eq_monomial, coeff_monomial, sum]
  split_ifs with h
  · rw [Finset.sum_eq_single (n / p), Nat.mul_div_cancel' h, if_pos rfl]
    · intro b _ hb2
      rw [if_neg]
      intro hb3
      apply hb2
      rw [← hb3, Nat.mul_div_cancel_left b hp]
    · intro hn
      rw [notMem_support_iff.1 hn]
      split_ifs <;> rfl
  · rw [Finset.sum_eq_zero]
    intro k _
    rw [if_neg]
    exact fun hkn => h ⟨k, hkn.symm⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
by
  by_cases hq : q.Monic
  · rcases subsingleton_or_nontrivial R with hR | hR
    · simp only [eq_iff_true_of_subsingleton]
    · exact
      (div_modByMonic_unique (c • (p /ₘ q)) (c • (p %ₘ q)) hq
          ⟨by rw [mul_smul_comm, ← smul_add, modByMonic_add_div],
            (degree_smul_le _ _).trans_lt (degree_modByMonic_lt _ hq)⟩).2
  · simp_rw [modByMonic_eq_of_not_monic _ hq]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∑ a ∈ range (n + 1), C ((map f p).coeff a * ↑a) * X ^ (a - 1) =
    map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

Tactic:
· simp only [Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C, map_mul, coeff_map,
      map_natCast, Polynomial.map_natCast, Polynomial.map_pow, map_X]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ map f p = map f (p %ₘ q) + map f (q * (p /ₘ q))

Tactic:
← Polynomial.map_add,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ map f p = map f (p %ₘ q + q * (p /ₘ q))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i =
    p.coeff (n + 1) + a * ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i

Tactic:
Icc_eq_cons_Ioc (Nat.succ_le_iff.mpr hn),

Goal state after:
case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ ∑ i ∈ cons n.succ (Ioc n.succ p.natDegree) ⋯, a ^ (i - (n + 1)) * p.coeff i =
    p.coeff (n + 1) + a * ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
n : ℕ
⊢ n ∈ p.support → ((fun n a ↦ C (a * ↑n) * X ^ (n - 1)) n (p.coeff n)).degree ≤ ↑(p.natDegree - 1)

Tactic:
hn

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
n : ℕ
hn : n ∈ p.support
⊢ ((fun n a ↦ C (a * ↑n) * X ^ (n - 1)) n (p.coeff n)).degree ≤ ↑(p.natDegree - 1)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : derivative p = 0
hp' : p ≠ 0
⊢ p.degree ≤ 0

Tactic:
by_contra! f_nat_degree_pos

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : derivative p = 0
hp' : p ≠ 0
f_nat_degree_pos : 0 < p.degree
⊢ False
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)

Tactic:
have : Pairwise fun i j => ∃ (s : {s // s ∈ l i}) (t : {t // t ∈ l j}), Disjoint s.1 t.1 := by
    simpa only [Pairwise, Function.onFun, Filter.disjoint_iff, exists_prop, Subtype.exists] using hd

Goal state after:
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
this : Pairwise fun i j ↦ ∃ s t, Disjoint ↑s ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
b : α
⊢ ￢∂ b = ⊤

Tactic:
exact hnot_boundary _

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

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : Subsingleton M₀ˣ
s : Finset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∀ (a : M₀), Multiset.countP (Associated a) (Multiset.map (fun p ↦ p) s.val) ≤ 1

Tactic:
simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter,
            ← s.val.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup]

Goal state after: