mathlib-initiative/mathlib-tactics huggingface dataset:
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 ∈ star (Algebra.adjoin R (↑S ⊔ ↑(star S)))

Tactic:
star_adjoin_comm,

Goal state after:
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 (↑S ⊔ ↑(star 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 : StarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S

Tactic:
by rw [h]; exact mem_top

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

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

Tactic:
refine ⟨fun h ↦ eq_univ_iff_forall.mpr h.mem_periodicPts, fun h ↦ ?_⟩
  rw [Finite.injective_iff_surjective, ← range_eq_univ, ← univ_subset_iff, ← h]
  apply periodicPts_subset_range

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

Goal state before:
pp: case h.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h✝ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' : (y :: hd :: tl).dropLast[k + 1] = (y :: hd :: tl).getLast ⋯
⊢ k + 1 = tl.length + 1

Tactic:
Nat.succ_inj

Goal state after:
case h.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h✝ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' : (y :: hd :: tl).dropLast[k + 1] = (y :: hd :: tl).getLast ⋯
⊢ k = tl.length
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ (s.insertIdx k x).length = (s.insertIdx (k + 1) x).length

Tactic:
rw [length_insertIdx_of_le_length hk.le, length_insertIdx_of_le_length (Nat.succ_le_of_lt hk)]

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

Goal state before:
pp: α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ ¬s.permutations.Nodup

Tactic:
List.Perm.nodup_iff (List.Perm.permutations ht),

Goal state after:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ ¬([x, x] ++ l).permutations.Nodup
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case h
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ Duplicate (x :: x :: l) ([x, x] ++ l).permutations

Tactic:
rw [List.duplicate_iff_sublist, ← permutations_take_two]

Goal state after:
case h
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ take 2 (x :: x :: l).permutations <+ ([x, x] ++ l).permutations
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g • s = s

Tactic:
rw [← mem_stabilizer_iff]

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G s
Module: Mathlib.Algebra.IsPrimePow

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

Tactic:
_hn

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
x : R
n : ℕ
_hn : 0 < n
⊢ x ^ n = 0 → ¬Prime x
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
⊢ n.primeFactorsList = [] ↔ n = 0 ∨ n = 1

Tactic:
constructor <;> intro h
  · rcases n with (_ | _ | n)
    · exact Or.inl rfl
    · exact Or.inr rfl
    · rw [primeFactorsList] at h
      injection h
  · rcases h with (rfl | rfl)
    · exact primeFactorsList_zero
    · exact primeFactorsList_one

Goal state after:
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
⊢ a :: replicate n a <+~ a :: (a ^ n * c).primeFactorsList

Tactic:
subperm_cons,

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
⊢ replicate n a <+~ (a ^ n * c).primeFactorsList
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
H K : Subgroup G
⊢ (map f H).relIndex (map f K) = (H ⊔ f.ker).relIndex (K ⊔ f.ker)

Tactic:
by
  rw [← comap_map_eq, ← comap_map_eq, relIndex_comap, (gc_map_comap f).l_u_l_eq_l]

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

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

Tactic:
by
  rw [← ZMod.coe_intCast, Int.cast_mul, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝³ : Group G
inst✝² : Group M
inst✝¹ : Finite G
inst✝ : Finite M
f : G →* M
h : Nat.card ↥f.ker ≤ Nat.card G / Nat.card M
⊢ (↑⊤).ncard ≤ (↑f.range).ncard

Tactic:
Subgroup.coe_top,

Goal state after:
G : Type u_1
M : Type u_2
inst✝³ : Group G
inst✝² : Group M
inst✝¹ : Finite G
inst✝ : Finite M
f : G →* M
h : Nat.card ↥f.ker ≤ Nat.card G / Nat.card M
⊢ Set.univ.ncard ≤ (↑f.range).ncard
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R✝ : Type u_1
inst✝⁴ : Ring R✝
n : ℕ
R : Type u_2
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module (ZMod n) R
inst✝ : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
x : ZMod n
y : R
z : M
⊢ (x • y) • z = x • y • z

Tactic:
rw [Algebra.smul_def, mul_smul]

Goal state after:
R✝ : Type u_1
inst✝⁴ : Ring R✝
n : ℕ
R : Type u_2
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module (ZMod n) R
inst✝ : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
x : ZMod n
y : R
z : M
⊢ (algebraMap (ZMod n) R) x • y • z = x • y • z
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n ∧ n ≠ 0
⊢ x.1 ∈ n.divisors

Tactic:
simp [Dvd.intro _ h.1, h.2]

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

Goal state before:
pp: m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ m.Coprime n

Tactic:
rw [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm, ← H']

Goal state after:
m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ n.gcd m = (m % n).gcd n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod n
h : IsUnit a
⊢ a⁻¹ * a = 1

Tactic:
rw [mul_comm, mul_inv_of_unit a h]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
n : ℕ
h : ∑ x ∈ (n + 1).properDivisors, x ∣ n + 1
⊢ ∑ x ∈ (n + 1).properDivisors, x = 1 ∨ ∑ x ∈ (n + 1).properDivisors, x = n + 1

Tactic:
rcases n with - | n
    · simp at h
    · rw [or_iff_not_imp_right]
      intro ne_n
      have hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ :=
        lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h) ne_n
      symm
      rw [← mem_singleton, eq_properDivisors_of_subset_of_sum_eq_sum (singleton_subset_iff.2
        (mem_properDivisors.2 ⟨h, hlt⟩)) (sum_singleton _ _), mem_properDivisors]
      exact ⟨one_dvd _, Nat.succ_lt_succ (Nat.succ_pos _)⟩

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∈ (p ^ k).properDivisors ↔ ∃ j, ∃ (_ : j < k), x = p ^ j

Tactic:
rw [mem_properDivisors, Nat.dvd_prime_pow pp]

Goal state after:
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k ↔ ∃ j, ∃ (_ : j < k), x = p ^ j
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:
rw [← map_swap_divisorsAntidiagonal, Finset.prod_map]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x ∈ n.divisorsAntidiagonal, f ((Equiv.prodComm ℕ ℕ).toEmbedding x).1 ((Equiv.prodComm ℕ ℕ).toEmbedding x).2 =
    ∏ i ∈ n.divisors, f (n / i) i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a : ℤ
⊢ ↑|a| = ↑a

Tactic:
cases le_total a 0

Goal state after:
case inl
a : ℤ
h✝ : a ≤ 0
⊢ ↑|a| = ↑a

case inr
a : ℤ
h✝ : 0 ≤ a
⊢ ↑|a| = ↑a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ n % n = 0

Tactic:
Nat.mod_self

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ 0 = 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
h : 2 ≤ b
n : ℕ
w : 0 < n
⊢ b.digitsAux h n = n % b :: b.digitsAux h (n / b)

Tactic:
by
  cases n
  · cases w
  · rw [digitsAux]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun x y ↦ ↑x + b * y) 0 L
⊢ ↑d + b * ofDigits b L = ↑d + b * List.foldr (fun x y ↦ ↑x + b * y) 0 L

Tactic:
rw [ih]

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.val = k

Tactic:
rw [map_natCast, natCast_zmod_val]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑d + ↑b * ↑(ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L

Tactic:
rw [ih]

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

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

Tactic:
rw [ih]

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

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

Goal state before:
pp: p i n : ℕ
h : 2 ≤ p
⊢ n % p ^ i = ofDigits p (List.take i (p.digits n))

Tactic:
convert!
    ofDigits_mod_pow_eq_ofDigits_take i (zero_lt_of_lt h) (p.digits n)
      (fun l hl ↦ digits_lt_base h hl)

Goal state after:
p i n : ℕ
h : 2 ≤ p
⊢ n = ofDigits p (p.digits n)
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: p : ℕ
hp : p ≠ 1
n : ℕ
hn : n ≠ 0
⊢ ↑(padicValNat p n) = emultiplicity p n

Tactic:
by
  rw [eq_comm, emultiplicity_eq_coe, pow_dvd_iff_le_padicValNat hp hn,
    pow_dvd_iff_le_padicValNat hp hn]
  simp

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l x✝¹ : ℕ
x✝ : x✝¹ ∈ {n | n < b ^ l}
⊢ ofDigits b (b.digitsAppend l x✝¹) = x✝¹

Tactic:
by rw [digitsAppend, ofDigits_append_replicate_zero,
    ofDigits_digits]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ (n % orderOf x) = x ^ (n % orderOf x + orderOf x * (n / orderOf x))

Tactic:
by
        simp [pow_add, pow_mul, pow_orderOf_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ψ 1 = 1

Tactic:
apply map_one

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

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ x ∈ fixedLengthDigits hb l, ∑ x ∈ Finset.range b, x + ∑ x ∈ fixedLengthDigits hb l, ∑ x_1 ∈ Finset.range b, x.sum =
    (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
Finset.sum_const,

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ (fixedLengthDigits hb l).card • ∑ x ∈ Finset.range b, x +
      ∑ x ∈ fixedLengthDigits hb l, (Finset.range b).card • x.sum =
    (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Tactic:
by
  have hdiva : p ^ multiplicity p a ∣ a := pow_multiplicity_dvd ..
  have hdivb : p ^ multiplicity p b ∣ b := pow_multiplicity_dvd ..
  have hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b := by
    rw [pow_add]; gcongr
  have hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b :=
    fun h =>
    not_or_intro (hfin.mul_left.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
      (hfin.mul_right.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
      (_root_.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul hp hdiva hdivb h)
  rw [hfin.multiplicity_eq_iff]
  exact ⟨hdiv, hsucc⟩

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ ∀ (i : ℕ), a.factorization i ≤ b.factorization i

Tactic:
congr! 1 with p

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ p ^ a.factorization p ∣ p ^ b.factorization p ↔ a.factorization p ≤ b.factorization p
Module: Mathlib.Data.Nat.Choose.Factorization

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

Tactic:
factorization_factorial hp ((log_mono_right (le_add_left k n)).trans_lt
      hnb),

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h2 : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ∑ i ∈ Ico 1 b, (n + k) / p ^ i =
    #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) + (∑ i ∈ Ico 1 b, k / p ^ i + n !.factorization p)
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ((p ^ n).choose k).factorization p = n - k.factorization p

Tactic:
nth_rewrite 2 [← factorization_choose_prime_pow_add_factorization hp hkn hk0]

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ((p ^ n).choose k).factorization p = ((p ^ n).choose k).factorization p + k.factorization p - k.factorization p
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) =
    x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k)

Tactic:
simp_rw [Icc_eq_cons_Ico zero_le, Ico_eq_cons_Ioo (pow_pos hp.pos _)]
    simp [-cons_eq_insert, add_assoc]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
wlog hmn : m ≤ n generalizing m n
  · rw [eq_comm, Nat.ModEq.comm, this (le_of_not_ge hmn)]
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  constructor
  · intro h
    have hk : x ^ k = 1 := by
      apply (mul_right_cancel_iff (a := x ^ m)).1
      calc
        x ^ k * x ^ m = x ^ (k + m) := (pow_add _ _ _).symm
        _ = x ^ (m + k) := by simp [Nat.add_comm]
        _ = x ^ m := h
        _ = 1 * x ^ m := by simp
    exact by simpa using Nat.ModEq.add_left m (pow_eq_one_iff_modEq.1 hk)
  · intro h
    have hk : x ^ k = 1 := by
      apply pow_eq_one_iff_modEq.2
      exact Nat.ModEq.add_left_cancel' m (by simpa using h)
    calc
      x ^ (m + k) = x ^ m * x ^ k := by rw [pow_add]
      _ = x ^ m := by simp [hk]

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

Goal state before:
pp: case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
r : R
hr : (x + y) ^ p = x ^ p + y ^ p + ↑p * x * y * r
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
simp [hr]

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

Goal state before:
pp: case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
r : R
hr : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * x * y * r
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
simp [hr]

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.gcd b).factorization + (a.lcm b).factorization = (a.gcd b).factorization + a.factorization ⊔ b.factorization

Tactic:
←
    factorization_mul (mt gcd_eq_zero_iff.1 fun h => ha h.1) (lcm_ne_zero ha hb),

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.gcd b * a.lcm b).factorization = (a.gcd b).factorization + a.factorization ⊔ b.factorization
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ 0 ^ p = 0

Tactic:
zero_pow (expChar_ne_zero R p)

Goal state after:
R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ 0 = 0
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
obtain rfl | ha := eq_or_ne g 1
  · simp
  · 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: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})

Tactic:
simp +contextual [disjoint_right, *, dvd_iff_mod_eq_zero,
          Nat.mod_lt _ (pow_pos hp.pos _)]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f✝ : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
f : R
s : S
⊢ (_root_.iterateFrobenius S p n) (f • s) =
    (_root_.iterateFrobenius R p n) f • (↑↑(_root_.iterateFrobenius S p n)).toFun s

Tactic:
simp_rw [iterateFrobenius_def, Algebra.smul_def, mul_pow, ← map_pow]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f✝ : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
f : R
s : S
⊢ (algebraMap R S) (f ^ p ^ n) * s ^ p ^ n = (algebraMap R S) (f ^ p ^ n) * (↑↑(_root_.iterateFrobenius S p n)).toFun s
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (C a).divX.coeff n = coeff 0 n

Tactic:
simp [coeff_divX]

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

Goal state before:
pp: case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
⊢ c ≠ 0 → (divX_hom ((monomial n) c)).natDegree = n - 1

Tactic:
c0

Goal state after:
case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ (divX_hom ((monomial n) c)).natDegree = n - 1
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
⊢ (C a * X ^ n).divX = if n = 0 then 0 else C a * X ^ (n - 1)

Tactic:
by
  simp only [divX_C_mul, divX_X_pow, mul_ite, mul_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f✝ f g : R[X]
ihf : (expand R 1) f = f
ihg : (expand R 1) g = g
⊢ (expand R 1) (f + g) = f + g

Tactic:
rw [map_add, ihf, ihg]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ((expand R p) f).degree = ↑(f.natDegree * p)

Tactic:
refine le_antisymm ((degree_le_iff_coeff_zero _ _).2 fun n hn => ?_) ?_

Goal state after:
case neg.refine_1
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
⊢ ((expand R p) f).coeff n = 0

case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ↑(f.natDegree * p) ≤ ((expand R p) f).degree
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
w✝ : R
⊢ (aeval ((algebraMap R S) w✝)) p ≠ 0

Tactic:
aeval_algebraMap_apply_eq_algebraMap_eval

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
⊢ (algebraMap R S) (eval w✝ p) ≠ 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
⊢ (derivative p).natDegree < p.natDegree

Tactic:
rcases eq_or_ne (derivative p) 0 with hp' | hp'

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p = 0
⊢ (derivative p).natDegree < p.natDegree

case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p ≠ 0
⊢ (derivative p).natDegree < p.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
⊢ q ∣ p %ₘ q ↔ q ∣ p

Tactic:
by
  simpa using dvd_iff_dvd_of_dvd_sub <| dvd_modByMonic_sub p q

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

Goal state before:
pp: case succ
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k)) f) = f ^ p ^ k
⊢ map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1))) f) = f ^ p ^ (k + 1)

Tactic:
| succ k n_ih =>

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
this : (p %ₘ (X - C a)).degree < 1
⊢ (p %ₘ (X - C a)).degree ≤ 0

Tactic:
revert this

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
⊢ (p %ₘ (X - C a)).degree < 1 → (p %ₘ (X - C a)).degree ≤ 0
Module: Mathlib.Order.Filter.Ker

Goal state before:
pp: α : Type u_2
β : Type u_3
m : α → β
f : Filter β
⊢ (comap m f).ker = m ⁻¹' f.ker

Tactic:
ext a
  simp only [mem_ker, mem_comap, forall_exists_index, and_imp, @forall_comm (Set α), mem_preimage]
  exact forall₂_congr fun s _ ↦ ⟨fun h ↦ h _ Subset.rfl, fun ha t ht ↦ ht ha⟩

Goal state after: