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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ k i < Function.extend Fin.castSucc k (fun x ↦ f.natDegree) j

Tactic:
Function.extend_apply' _ _ _ hj

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ k i < f.natDegree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (s.sup fun i ↦ (f i).degree) ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree

Tactic:
apply Finset.sup_le

Goal state after:
case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ ∀ b ∈ s, (f b).degree ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case neg
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ (f i).degree ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree

Tactic:
rw [degree_eq_natDegree hf]

Goal state after:
case neg
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ ↑(f i).natDegree ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (s.sup fun i ↦ (f i).natDegree) ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).natDegree

Tactic:
apply Finset.sup_le

Goal state after:
case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ ∀ b ∈ s, (f b).natDegree ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ (h.unit⁻¹ • p).Monic

Tactic:
rw [Monic.def, leadingCoeff_smul_of_smul_regular _ (isSMulRegular_of_group _), Units.smul_def]
  simp

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
a✝ : Nontrivial R
⊢ (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0

Tactic:
simp_rw [Ne, Multiset.prod_eq_zero_iff, Multiset.mem_map, leadingCoeff_eq_zero]

Goal state after:
case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
a✝ : Nontrivial R
⊢ ¬∃ a ∈ t, a = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
⊢ leadingCoeffHom t.prod = (Multiset.map (fun f ↦ f.leadingCoeff) t).prod

Tactic:
MonoidHom.map_multiset_prod

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
⊢ (Multiset.map (⇑leadingCoeffHom) t).prod = (Multiset.map (fun f ↦ f.leadingCoeff) t).prod
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_1.refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
this : y ∈ Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ y ∈ adjoin R (s ∪ t)

Tactic:
adjoin_union_eq_adjoin_adjoin

Goal state after:
case refine_1.refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
this : y ∈ Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ y ∈ Subalgebra.restrictScalars R (adjoin (↥(adjoin R s)) t)
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
r : A
hr : r ∈ adjoin R (s ∪ t)
⊢ r ∈ span R (p * q)

Tactic:
adjoin_union_eq_adjoin_adjoin

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
r : A
hr : r ∈ Subalgebra.restrictScalars R (adjoin (↥(adjoin R s)) t)
⊢ r ∈ span R (p * q)
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ Subalgebra.toSubmodule (adjoin R (s ∪ t)) ≤ span R (p * q)

Tactic:
· intro r hr
    change r ∈ adjoin R (s ∪ t) at hr
    rw [adjoin_union_eq_adjoin_adjoin] at hr
    change r ∈ Subalgebra.toSubmodule (adjoin (adjoin R s) t) at hr
    rw [← hq', ← Set.image_id q, Finsupp.mem_span_image_iff_linearCombination (adjoin R s)] at hr
    rcases hr with ⟨l, hlq, rfl⟩
    have := @Finsupp.linearCombination_apply A A (adjoin R s)
    rw [this, Finsupp.sum]
    refine sum_mem ?_
    intro z hz
    change (l z).1 * _ ∈ _
    have : (l z).1 ∈ Subalgebra.toSubmodule (adjoin R s) := (l z).2
    rw [← hp', ← Set.image_id p, Finsupp.mem_span_image_iff_linearCombination R] at this
    rcases this with ⟨l2, hlp, hl⟩
    have := @Finsupp.linearCombination_apply A A R
    rw [this] at hl
    rw [← hl, Finsupp.sum_mul]
    refine sum_mem ?_
    intro t ht
    change _ * _ ∈ _
    rw [smul_mul_assoc]
    refine smul_mem _ _ ?_
    exact subset_span ⟨t, hlp ht, z, hlq hz, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs✝ : S.FG
s : Finset A
hs : Algebra.adjoin R ↑s = S
⊢ (Subalgebra.map f S).FG

Tactic:
exact ⟨s.image f, by rw [Finset.coe_image, Algebra.adjoin_image, hs]⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
hr : Prime r
⊢ Prime (C r)

Tactic:
have := hr.1

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
hr : Prime r
this : r ≠ 0
⊢ Prime (C r)
Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

Goal state before:
pp: case e_a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
⊢ (∃ y, (algebraMap R A) y = MulOpposite.unop x) ↔ ∃ y, (algebraMap R Aᵐᵒᵖ) y = x

Tactic:
MulOpposite.algebraMap_apply

Goal state after:
case e_a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
⊢ (∃ y, (algebraMap R A) y = MulOpposite.unop x) ↔ ∃ y, MulOpposite.op ((algebraMap R A) y) = x
Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ (Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ s)).unop =
    Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ MulOpposite.op ⁻¹' s)

Tactic:
Subsemiring.unop_closure,

Goal state after:
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ Subsemiring.closure (MulOpposite.op ⁻¹' (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ s)) =
    Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ MulOpposite.op ⁻¹' s)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
⊢ fold max 0 (natDegree ∘ fun i ↦ (fun s a ↦ (algebraMap R R[X]) a * s.prod fun n e ↦ f n ^ e) i (F.coeff i))
      F.coeff.support ≤
    m * n

Tactic:
apply Finset.sup_le

Goal state after:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
⊢ ∀ b ∈ F.coeff.support,
    (natDegree ∘ fun i ↦ (fun s a ↦ (algebraMap R R[X]) a * s.prod fun n e ↦ f n ^ e) i (F.coeff i)) b ≤ m * n
Module: Mathlib.Data.Int.ModEq

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

Tactic:
rw [add_comm a, add_comm b] at h₂

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l l' : List α
h : l ~ l'
⊢ ↑l.permutations = ↑l'.permutations

Tactic:
refine coe_eq_coe.mpr ?_
    exact Perm.permutations h

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

Goal state before:
pp: α : Type u_1
⊢ [].permutations = [[]]

Tactic:
permutations,

Goal state after:
α : Type u_1
⊢ [] :: [].permutationsAux [] = [[]]
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) ts.permutations = (map f ts).permutations

Tactic:
permutations,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) (ts :: ts.permutationsAux []) = (map f ts).permutations
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) (ts :: ts.permutationsAux []) = (map f ts).permutations

Tactic:
permutations,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) (ts :: ts.permutationsAux []) = map f ts :: (map f ts).permutationsAux []
Module: Mathlib.Dynamics.PeriodicPts.Defs

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

Tactic:
rw [IsPeriodicPt, hco.comp_iterate] at hfg

Goal state after:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsFixedPt (f^[n] ∘ g^[n]) x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m : l ∈ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is)) is.permutations
⊢ l ~ t :: ts ++ is

Tactic:
permutations,

Goal state after:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m :
  l ∈ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is)) (is :: is.permutationsAux [])
⊢ l ~ t :: ts ++ is
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ minimalPeriod f x = 0

Tactic:
simp only [minimalPeriod, dif_neg hx]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ IsPeriodicPt f (minimalPeriod f x) (f^[n] x)

Tactic:
exact (isPeriodicPt_minimalPeriod f x).apply_iterate n

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

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
⊢ is.length * is.permutations.length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!

Tactic:
permutations,

Goal state after:
α : Type u_1
t : α
ts is : List α
IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
⊢ is.length * (is :: is.permutationsAux []).length + (ts.permutationsAux (t :: is)).length + is.length ! =
    ((t :: ts).length + is.length)!
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
n : ℕ
hn : n < (permutations'Aux x s).length
⊢ (permutations'Aux x s)[n] = s.insertIdx n x

Tactic:
by
  induction s generalizing n with
  | nil =>
    simp only [permutations'Aux, length, Nat.zero_add, lt_one_iff] at hn
    simp [hn]
  | cons y s IH =>
    cases n
    · simp
    · simpa [get] using IH _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
⊢ count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1

Tactic:
by
  induction l generalizing x with
  | nil => simp [takeWhile, count]
  | cons y l IH =>
    rw [permutations'Aux, count_cons_self]
    by_cases hx : x = y
    · subst hx
      simpa [takeWhile, Nat.succ_inj, DecEq_eq] using IH _
    · rw [takeWhile]
      simp only [mem_map, cons.injEq, Ne.symm hx, false_and, and_false, exists_false,
        not_false_iff, count_eq_zero_of_not_mem, Nat.zero_add, hx, decide_false, length_nil]

Goal state after:
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 = (z :: head✝ :: tail✝).prev x ⋯

Tactic:
· rw [prev, dif_neg hy, if_neg hz]

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

Goal state before:
pp: case cons.left
α : 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
⊢ ∀ (x_1 : List α), x_1 ∈ l.permutations' → (permutations'Aux x x_1).Nodup

Tactic:
intro ys hy
      rw [mem_permutations'] at hy
      rw [nodup_permutations'Aux_iff, hy.mem_iff]
      exact fun H => h x H rfl

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 α
⊢ fixedPoints G α = Set.univ

Tactic:
by
  apply Set.eq_univ_of_forall
  simp only [mem_fixedPoints]
  intro x hx
  apply Subsingleton.elim ..

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

Goal state before:
pp: α : Type u_1
⊢ nil.lists = {[]}

Tactic:
nil,

Goal state after:
α : Type u_1
⊢ (↑[]).lists = {[]}
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case mp
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

pp: case mpr
n : ℕ
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
· rintro ⟨p, k, hp', hk', rfl⟩
    refine ⟨k, ?_, hk', ⟨p, Nat.le_pow hk', rfl, hp'⟩⟩
    · calc
        k = Nat.log 2 (2 ^ k) := by simp
        _ ≤ Nat.log 2 (p ^ k) := Nat.log_mono Nat.one_lt_two Nat.AtLeastTwo.prop
                                   (Nat.pow_le_pow_left (Nat.Prime.two_le hp') k)

Goal state after:
case mpr
n : ℕ
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ H.index ≠ 0

Tactic:
index_eq_card

Goal state after:
case intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ Nat.card (G ⧸ H) ≠ 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
← Nat.cast_mul,

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
x : X
inst✝ : IsPretransitive G X
⊢ (stabilizer G x).index = Nat.card X

Tactic:
by
  rw [index_stabilizer, orbit_eq_univ, Set.ncard_univ]

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

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ZMod m
⊢ a.cast = 0 ↔ a = 0

Tactic:
← ZMod.cast_zero (n := m)

Goal state after:
m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ZMod m
⊢ a.cast = cast 0 ↔ a = 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ n ≤ n.divisors.sup id

Tactic:
· exact Finset.le_sup (f := id) <| mem_divisors_self n hn

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

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

Tactic:
exact (geom_sum_pos' h n.succ.succ_ne_zero).ne'

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

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

Tactic:
← Nat.cast_mul,

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

Goal state before:
pp: x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
⊢ (x + 1) % (b + 2) :: (b + 2).digits ((x + 1) / (b + 2)) = [x.succ]

Tactic:
div_eq_of_lt hxb,

Goal state after:
x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
⊢ (x + 1) % (b + 2) :: (b + 2).digits 0 = [x.succ]
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.zero
n : ℕ
a✝ : (digits 0 n).sum ≤ n
⊢ (digits 0 (n + 1)).sum ≤ n + 1

Tactic:
rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]

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

Goal state before:
pp: p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits / p = ofDigits p digits.tail

Tactic:
induction digits with

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:
by rw [hf.pow_dvd_iff_le_multiplicity, not_le]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
⊢ IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0

Tactic:
by
  rcases Decidable.eq_or_ne n 0 with rfl | hn
  · simp
  · exact ⟨fun h ↦ .inl <| h.of_pow hn, fun h ↦ (h.resolve_right hn).pow⟩

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
inst✝ : IsMulTorsionFree G
a : G
ha : IsOfFinOrder a
⊢ a = 1

Tactic:
by
  contrapose! ha
  apply not_isOfFinOrder_of_isMulTorsionFree ha

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun x_1 ↦ x * x_1
⊢ 0 = n ↔ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1

Tactic:
· rw [iff_false_left h.ne]
    rintro ⟨h', -⟩
    exact h1 ⟨n, h, h'⟩

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

Goal state before:
pp: p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ k ≤ n.factorization p

Tactic:
← factorization_le_iff_dvd (Nat.pow_pos pp.pos).ne' hn,

Goal state after:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ (p ^ k).factorization ≤ n.factorization ↔ k ≤ n.factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x y : G
h✝ : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
h : p ∣ orderOf x
⊢ p * orderOf x ∣ orderOf y

pp: case neg
G : Type u_1
inst✝ : Monoid G
x y : G
h✝ : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
h : ¬p ∣ orderOf x
⊢ p * orderOf x ∣ orderOf y

Tactic:
exacts [hdvd p hp h, (hp.coprime_iff_not_dvd.2 h).mul_dvd_of_dvd_of_dvd hpy hxy]

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

Goal state before:
pp: n k : ℕ
hkn : k ≤ n
| n.choose k

Tactic:
rw [← prod_factorization_pow_eq_self (choose_ne_zero hkn)]

Goal state after:
n k : ℕ
hkn : k ≤ n
| (n.choose k).factorization.prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hda
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) ∣ a

pp: case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) ∣ b

pp: case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
· exact prod_pow_dvd_of_le_factorization inf_le_left

Goal state after:
case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) ∣ b

case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Multiplicity

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

Tactic:
simp [add_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p m n : ℕ
inst✝ : ExpChar R p
x : R
⊢ (⇑(frobenius R p))^[m * n] x = (⇑(frobenius R p))^[m]^[n] x

Tactic:
Function.iterate_mul

Goal state after: