mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case algebraMap.algebraMap
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
r r✝ : R
⊢ p ((algebraMap R A) r✝) ((algebraMap R A) r) ⋯ ⋯

Tactic:
exact algebraMap_both _ _

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (ts is : List α), (ts.permutationsAux is).length + is.length ! = (ts.length + is.length)!

Tactic:
by
  refine permutationsAux.rec (by simp) ?_
  intro t ts is IH1 IH2
  have IH2 : length (permutationsAux is nil) + 1 = is.length ! := by simpa using IH2
  simp only [List.length_cons, factorial, Nat.mul_comm, add_eq] at IH1
  rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]

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

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

pp: case neg
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

Tactic:
· have hx' := minimalPeriod_pos_of_mem_periodicPts hx
    have hM := Nat.sub_add_cancel (succ_le_iff.2 hx')
    rw [periodicOrbit, ← Cycle.map_coe, Cycle.chain_map, ← hM, Cycle.chain_range_succ]
    refine ⟨?_, fun H => ⟨?_, fun m hm => H _ (hm.trans (Nat.lt_succ_self _))⟩⟩
    · rintro ⟨hr, H⟩ n hn
      rcases eq_or_lt_of_le (Nat.lt_succ_iff.1 hn) with hM' | hM'
      · rwa [hM', hM, iterate_minimalPeriod]
      · exact H _ hM'
    · rw [iterate_zero_apply]
      nth_rw 3 [← @iterate_minimalPeriod α f x]
      nth_rw 2 [← hM]
      exact H _ (Nat.lt_succ_self _)

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
hx : ¬x ∈ s
⊢ (permutations'Aux x s).Nodup

Tactic:
by
  induction s with
  | nil => simp
  | cons y s IH =>
    simp only [not_or, mem_cons] at hx
    simp only [permutations'Aux, nodup_cons, mem_map, cons.injEq, exists_eq_right_right, not_and]
    refine ⟨fun _ => Ne.symm hx.left, ?_⟩
    rw [nodup_map_iff]
    · exact IH hx.right
    · simp

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : a = head
⊢ (head :: tail).prev a ha =
    (head :: tail)[(idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length]

Tactic:
subst ha₀
    simp
    grind

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝² : Monoid M
inst✝¹ : AddGroup G
inst✝ : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
⊢ a = b

Tactic:
← sub_eq_zero

Goal state after:
M : Type u_1
G : Type u_2
inst✝² : Monoid M
inst✝¹ : AddGroup G
inst✝ : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
⊢ a - b = 0
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
⊢ ∀ (g : Ω), Finite ↑g.orbit

Tactic:
intro g

Goal state after:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
g : Ω
⊢ Finite ↑g.orbit
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
⊢ MulAction.stabilizer Rˣ x ≤ ⊥

Tactic:
intro g

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
⊢ g ∈ MulAction.stabilizer Rˣ x → g ∈ ⊥
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k

Tactic:
rw [isPrimePow_nat_iff_bounded_log]

Goal state after:
n : ℕ
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
y₁ y₂ : G ⧸ stabilizer G x
g₁ g₂ : G
H : g₁ • x = g₂ • x
⊢ (leftRel (stabilizer G x)) g₁ g₂

Tactic:
by
      rw [leftRel_apply]
      change (g₁⁻¹ * g₂) • x = x
      rw [mul_smul, ← H, inv_smul_smul]

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

Goal state before:
pp: n p : ℕ
h : p ∈ n.primeFactorsList
⊢ p ∣ n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Goal state after:
case inl
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ∣ 0

case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ∣ n
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n p : ℕ
h : p ∈ n.primeFactorsList
⊢ p ≤ n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

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

case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ≤ n
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_1
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : l.prod = 0
⊢ False

Tactic:
rw [prod_eq_zero_iff] at h₁

Goal state after:
case refine_1
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : 0 ∈ l
⊢ False
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore ≤ (MulAction.toPermHom G (G ⧸ H)).ker

Tactic:
intro g

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ g ∈ H.normalCore → g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
Module: Mathlib.Data.Nat.Factors

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

Tactic:
by
  intro q hqa hqb
  apply not_prime_one
  rw [← eq_one_of_dvd_coprimes hab (dvd_of_mem_primeFactorsList hqa)
    (dvd_of_mem_primeFactorsList hqb)]
  exact prime_of_mem_primeFactorsList hqa

Goal state after:
Module: Mathlib.GroupTheory.Index

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

Tactic:
K.range_subtype

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
K : Subgroup G'
⊢ H.relIndex (map f K) = H.relIndex (map f K)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (∃ a ∉ H, a ∈ K ∧ ∀ a_1 ∈ K, a_1 * a ∈ H ∨ a_1 ∈ H) ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H

Tactic:
refine exists_congr fun g ↦ ?_

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
⊢ (g ∉ H ∧ g ∈ K ∧ ∀ a ∈ K, a * g ∈ H ∨ a ∈ H) ↔ g ∈ K ∧ g ∉ H ∧ ∀ b ∈ K, b * g ∈ H ∨ b ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (∃ a ∉ H, a ∈ K ∧ ∀ a_1 ∈ K, a * a_1 ∈ H ∨ a_1 ∈ H) ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H

Tactic:
refine exists_congr fun g ↦ ?_

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
⊢ (g ∉ H ∧ g ∈ K ∧ ∀ a ∈ K, g * a ∈ H ∨ a ∈ H) ↔ g ∈ K ∧ g ∉ H ∧ ∀ b ∈ K, g * b ∈ H ∨ b ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a : ℕ
⊢ (↑a).val = a % 0

Tactic:
Nat.mod_zero

Goal state after:
case zero
a : ℕ
⊢ (↑a).val = a
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H K L : Subgroup G
f : G →* G'
inst✝ : H.FiniteIndex
⊢ H.normalCore.FiniteIndex

Tactic:
normalCore_eq_ker

Goal state after:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H K L : Subgroup G
f : G →* G'
inst✝ : H.FiniteIndex
⊢ (MulAction.toPermHom G (G ⧸ H)).ker.FiniteIndex
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
h : a.val + b.val < n
this : NeZero n
⊢ (a + b).val = a.val + b.val

Tactic:
rw [ZMod.val_add, Nat.mod_eq_of_lt h]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ (a + b).val = a.val + b.val - n

Tactic:
val_add_val_of_le h

Goal state after:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ (a + b).val = (a + b).val + n - n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val % 0

Tactic:
Nat.mod_zero

Goal state after:
case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
u : (ZMod n)ˣ
⊢ (↑u)⁻¹ = ↑u⁻¹

Tactic:
have := congr_arg ((↑) : ℕ → ZMod n) (val_coe_unit_coprime u)

Goal state after:
n : ℕ
u : (ZMod n)ˣ
this : ↑((↑u).val.gcd n) = ↑1
⊢ (↑u)⁻¹ = ↑u⁻¹
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
s : Finset ℕ
hsub : s ⊆ properDivisors 0
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0

Tactic:
rw [properDivisors_zero, subset_empty] at hsub

Goal state after:
case zero
s : Finset ℕ
hsub : s = ∅
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ Prime (n✝ + 1 + 1)

Tactic:
· rw [← properDivisors_eq_singleton_one_iff_prime]
      refine ⟨fun h => ?_, fun h => h.symm ▸ sum_singleton _ _⟩
      rw [@eq_comm (Finset ℕ) _ _]
      apply
        eq_properDivisors_of_subset_of_sum_eq_sum
          (singleton_subset_iff.2
            (one_mem_properDivisors_iff_one_lt.2 (succ_lt_succ (Nat.succ_pos _))))
          ((sum_singleton _ _).trans h.symm)

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

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

Tactic:
rw [mul_zero, mul_eq_zero] at he
      rcases he with (⟨⟨⟩⟩ | he)
      exact Or.inl (a.val_eq_zero.1 he)

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : NonAssocRing R
f : R →+* ZMod 0
k : ZMod 0
⊢ f k.cast = k

Tactic:
dsimp +instances [ZMod, ZMod.cast] at f k ⊢

Goal state after:
case zero
R : Type u_1
inst✝ : NonAssocRing R
f : R →+* ℤ
k : ℤ
⊢ f ↑k = k
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
replace hn : (Nat.card α).Coprime n := hn

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

Goal state before:
pp: b n : ℕ
⊢ b.digits n = [] ↔ n = 0

Tactic:
by
  constructor
  · intro h
    have : ofDigits b (digits b n) = ofDigits b [] := by rw [h]
    convert! this
    rw [ofDigits_digits]
  · rintro rfl
    simp

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

Goal state before:
pp: case zero
m d : ℕ
hb : 1 < 0
hd : d ∈ digits 0 m
⊢ d < 0

Tactic:
simp_all [@digits_lt_base' _ m d]

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

Goal state before:
pp: case succ.zero
m d : ℕ
hb : 1 < 0 + 1
hd : d ∈ (0 + 1).digits m
⊢ d < 0 + 1

Tactic:
simp_all [@digits_lt_base' _ m d]

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

Goal state before:
pp: case succ.succ
m d b : ℕ
hb : 1 < b + 1 + 1
hd : d ∈ (b + 1 + 1).digits m
⊢ d < b + 1 + 1

Tactic:
simp_all [@digits_lt_base' _ m d]

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

Goal state before:
pp: case bit.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit false n) = List.map (fun b ↦ bif b then 1 else 0) (false :: n.bits)

Tactic:
rw [digits_def' one_lt_two]
      · simpa [Nat.bit]
      · simpa [Nat.bit, pos_iff_ne_zero]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
emultiplicity_eq_multiplicity hfin

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b ≤ n
⊢ ↑(multiplicity a b) ≤ ↑n
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:
emultiplicity_eq_multiplicity hfin

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n ≤ ↑(multiplicity a b)
⊢ n ≤ multiplicity a b
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
emultiplicity_eq_multiplicity hfin

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b < n
⊢ ↑(multiplicity a b) < ↑n
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:
emultiplicity_eq_multiplicity hfin

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n < ↑(multiplicity a b)
⊢ n < multiplicity a b
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b n : ℕ
⊢ ∀ (l1 l2 : List Char), l1.length = l2.length → l1.length = l2.length

Tactic:
l1

Goal state after:
case zero
b n : ℕ
l1 : List Char
⊢ ∀ (l2 : List Char), l1.length = l2.length → l1.length = l2.length
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
n : ℕ
⊢ ∀ (l1 l2 : List Char),
    l1.length = l2.length →
      (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
        (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length

Tactic:
l1

Goal state after:
case succ
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
n : ℕ
l1 : List Char
⊢ ∀ (l2 : List Char),
    l1.length = l2.length →
      (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
        (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h_2 : ¬FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ⊤

Tactic:
simp_all only [not_exists, Decidable.not_not, le_top]

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

Goal state before:
pp: n p : ℕ
⊢ p ∉ n.primeFactors ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0

Tactic:
mem_primeFactors,

Goal state after:
n p : ℕ
⊢ ¬(Prime p ∧ p ∣ n ∧ n ≠ 0) ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_1
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ (d :: L).length = l + 1

Tactic:
simpa using ((mem_fixedLengthDigits_iff hb).mp hL).1

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]

Goal state after:
case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun x_1 ↦ x * x_1
⊢ ¬(IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ n = 1 ↔ orderOf x ∣ n

Tactic:
orderOf_dvd_iff_pow_eq_one

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ n = 1 ↔ x ^ n = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
a b x✝ y : G
n m : ℕ
M : Type ?u.16
inst✝ : Monoid M
x : M
hx : IsOfFinOrder x
⊢ x ^ (orderOf x - 1 + 1) = 1

Tactic:
tsub_add_cancel_of_le (by exact hx.orderOf_pos),

Goal state after:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
a b x✝ y : G
n m : ℕ
M : Type ?u.16
inst✝ : Monoid M
x : M
hx : IsOfFinOrder x
⊢ x ^ orderOf x = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p k : ℕ
hp : Prime p
⊢ p ^ k / p ^ (p ^ k).factorization p = 1

Tactic:
apply Nat.eq_of_factorization_eq

Goal state after:
case ha
p k : ℕ
hp : Prime p
⊢ p ^ k / p ^ (p ^ k).factorization p ≠ 0

case hb
p k : ℕ
hp : Prime p
⊢ 1 ≠ 0

case h
p k : ℕ
hp : Prime p
⊢ ∀ (p_1 : ℕ), (p ^ k / p ^ (p ^ k).factorization p).factorization p_1 = (factorization 1) p_1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
⊢ a = b

Tactic:
by_contra hab

Goal state after:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ False
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case zero
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : 0 ≠ 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : 0 ^ i ∣ n
⊢ i < b

Tactic:
rw [zero_pow, zero_dvd_iff] at h

Goal state after:
case zero
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : 0 ≠ 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : n = 0
⊢ i < b

case zero
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : 0 ≠ 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : 0 ^ i ∣ n
⊢ i ≠ 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : x ^ (m + k) = x ^ m
hk : x ^ k = 1
⊢ m + k ≡ m [MOD orderOf x]

Tactic:
simpa using Nat.ModEq.add_left m (pow_eq_one_iff_modEq.1 hk)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ orderOf x ∣ i ↔ x ^ i = 1

Tactic:
orderOf_dvd_iff_pow_eq_one

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ x ^ i = 1 ↔ x ^ i = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
k : ℤ
h : x ^ k ∈ zpowers x
⊢ orderOf (x ^ k) ∣ orderOf x

Tactic:
orderOf_dvd_iff_pow_eq_one

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
k : ℤ
h : x ^ k ∈ zpowers x
⊢ (x ^ k) ^ orderOf x = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
n : ℤ
⊢ x ^ n = 1 ↔ ↑(orderOf x) ∣ n

Tactic:
orderOf_dvd_iff_zpow_eq_one

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
n : ℤ
⊢ x ^ n = 1 ↔ x ^ n = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
x : G
h : ¬IsOfFinOrder x
n m : ℤ
hnm : n ≡ m [ZMOD ↑(orderOf x)]
⊢ n = m

Tactic:
orderOf_eq_zero_iff.2 h,

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
x : G
h : ¬IsOfFinOrder x
n m : ℤ
hnm : n ≡ m [ZMOD ↑0]
⊢ n = m
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1

Tactic:
rw [emultiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]

Goal state after:
case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (2 * n)! < ↑(2 * n) + 1
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
hx : x ^ n = 1
⊢ False

Tactic:
replace hx : |x| ^ n = 1 := by simpa only [abs_one, abs_pow] using congr_arg abs 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.Inductions

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

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

Tactic:
· refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hq, add_comm]
      exact h_C_add hp

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ rootMultiplicity a (p * (X - C a) ^ n) ≤ rootMultiplicity a p + n

pp: case refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ rootMultiplicity a p + n ≤ rootMultiplicity a (p * (X - C a) ^ n)

Tactic:
· rw [rootMultiplicity_le_iff h2, add_assoc, add_comm n, ← add_assoc, pow_add,
      dvd_cancel_right_mem_nonZeroDivisors (monic_X_sub_C a |>.pow n |>.mem_nonZeroDivisors)]
    exact pow_rootMultiplicity_not_dvd h a

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ rootMultiplicity a p + n ≤ rootMultiplicity a (p * (X - C a) ^ n)