mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.PeriodicPts.Defs

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

Tactic:
IsPeriodicPt,

Goal state after:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f ∘ g)^[n] x
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:
IsPeriodicPt,

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

Goal state before:
pp: α : Type u_1
⊢ ∀ {ts is l : List α}, l ∈ ts.permutationsAux is → l ~ ts ++ is

Tactic:
show ∀ (ts is l : List α), l ∈ permutationsAux ts is → l ~ ts ++ is

Goal state after:
α : Type u_1
⊢ ∀ (ts is l : List α), l ∈ ts.permutationsAux is → l ~ ts ++ is
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[n + minimalPeriod f x] x = f^[n] x

Tactic:
rw [iterate_add_apply]

Goal state after:
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[n] (f^[minimalPeriod f x] x) = f^[n] x
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)

pp: α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicPts f

Tactic:
· exact (isPeriodicPt_minimalPeriod f x).apply_iterate n

Goal state after:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicPts f
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ IsPeriodicPt f^[n] (minimalPeriod f x / (minimalPeriod f x).gcd n) x

Tactic:
IsPeriodicPt,

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

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ IsPeriodicPt f (n * minimalPeriod f^[n] x) x

Tactic:
IsPeriodicPt,

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ IsFixedPt f^[n * minimalPeriod f^[n] x] x
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
⊢ adjoin R s ≤ centralizer R ↑(centralizer R s)

Tactic:
rw [← toSubalgebra_le_iff, centralizer_toSubalgebra, adjoin_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
⊢ Algebra.adjoin R (s ∪ star s) ≤ Subalgebra.centralizer R (↑(centralizer R s) ∪ star ↑(centralizer R s))
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
n : ℕ
⊢ IsPeriodicPt (fun x ↦ m • x) n a ↔ (fun x ↦ m • x)^[n] a = a

Tactic:
IsPeriodicPt,

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
n : ℕ
⊢ IsFixedPt (fun x ↦ m • x)^[n] a ↔ (fun x ↦ m • x)^[n] a = a
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
a b : α
l : List α
⊢ flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)

Tactic:
induction l with
  | nil => exact Perm.swap [a, b] [b, a] []
  | cons c l ih => ?_
  simp only [permutations'Aux, flatMap_cons, map_cons, map_map, cons_append]
  apply Perm.swap'
  have :
    ∀ a b,
      (map (cons c) (permutations'Aux a l)).flatMap (permutations'Aux b) ~
        map (cons b ∘ cons c) (permutations'Aux a l) ++
          map (cons c) ((permutations'Aux a l).flatMap (permutations'Aux b)) := by
    intro a' b'
    simp only [flatMap_map, permutations'Aux]
    change (permutations'Aux _ l).flatMap (fun a => ([b' :: c :: a] ++
      map (cons c) (permutations'Aux _ a))) ~ _
    refine (flatMap_append_perm _ (fun x => [b' :: c :: x]) _).symm.trans ?_
    rw [← map_eq_flatMap, ← map_flatMap]
    exact Perm.refl _
  refine (((this _ _).append_left _).trans ?_).trans ((this _ _).append_left _).symm
  rw [← append_assoc, ← append_assoc]
  exact perm_append_comm.append (ih.map _)

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x d : α
h : [].nextOr x d ≠ d
⊢ x ∈ []

Tactic:
simp at h

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

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d y : α
IH : [].nextOr x d ≠ d → x ∈ []
h : [y].nextOr x d ≠ d
⊢ x ∈ [y]

Tactic:
simp at h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x✝ : α
h : x✝ ∈ []
⊢ α

Tactic:
simp 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 : StarSubalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤

Tactic:
ext x

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 : StarSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s

Tactic:
rw [← Nat.card_prod]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card ((α ⧸ s) × ↥s)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : x ∈ []
⊢ [].prev x h ∈ []

Tactic:
simp at h

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
i : ℕ
hi : i < [a, l.nextOr a d].length
hi₁ : ¬i = 1
⊢ l[i + idxOf a l]? = some [a, l.nextOr a d][i]

Tactic:
grind [getElem?_idxOf, mem_of_mem_dropLast]

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:
rw [← sub_eq_zero]
  refine h _ ?_
  rw [smul_sub, h', sub_self]

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 α
H K : Subgroup G
⊢ orbitRel (↥(H.subgroupOf K)) α = orbitRel (↥(Subgroup.map K.subtype (H.subgroupOf K))) α

Tactic:
ext x

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
x b✝ : α
⊢ (orbitRel (↥(H.subgroupOf K)) α) x b✝ ↔ (orbitRel (↥(Subgroup.map K.subtype (H.subgroupOf K))) α) x b✝
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
⊢ (stabilizerEquivStabilizer hg).symm = stabilizerEquivStabilizer ⋯

Tactic:
ext x

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(stabilizer G b)
⊢ ↑((stabilizerEquivStabilizer hg).symm x) = ↑((stabilizerEquivStabilizer ⋯) x)
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:
exact dvd_mul_right _ _

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
a : α
l : List α
h✝ : Chain r ↑l → ↑l = Cycle.nil
h : Chain r ↑(a :: l)
ha : a ∈ a :: l
⊢ ↑(a :: l) = Cycle.nil

Tactic:
exact (irrefl_of r a <| chain_iff_pairwise.1 h a ha a ha).elim

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

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G ⧸ H
⊢ (fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯) ((fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯) g) = g

Tactic:
cases g using Quotient.inductionOn' with | _ g
     =>  _ 

Goal state after:
case h
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ (fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯)
      ((fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯) (Quotient.mk'' g)) =
    Quotient.mk'' g
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card ↑(ConjClasses.mk g).carrier = Fintype.card G / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card ↑(ConjClasses.mk g).carrier =
    Fintype.card (ConjAct G) / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
⊢ g'⁻¹ * g⁻¹ * g'⁻¹⁻¹ ∈ H

Tactic:
exact H.normalCore.inv_mem hg g'⁻¹

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

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
⊢ ↑g = ↑1

Tactic:
← mul_one g

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
⊢ ↑(g * 1) = ↑1
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: k p : ℕ
hk : k ≠ 0
hp : Prime p
⊢ (p ^ k).primeFactors = {p}

Tactic:
simp [primeFactors_pow p hk, hp]

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 ^ n ∣ a ^ n * c

Tactic:
exact dvd_mul_right _ _

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'
hf : Surjective ⇑f
⊢ (map f H).index ∣ H.index

Tactic:
index_map,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Surjective ⇑f
⊢ (H ⊔ f.ker).index * f.range.index ∣ H.index
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'
hf : f.ker ≤ H
⊢ H.index ∣ (map f H).index

Tactic:
index_map,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : f.ker ≤ H
⊢ H.index ∣ (H ⊔ f.ker).index * f.range.index
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.relIndex K ∣ 2 ↔ ∃ a ∈ K, ∀ b ∈ K, b * a ∈ H ∨ b ∈ H

Tactic:
by
  simp [Subgroup.relIndex, Subgroup.index_dvd_two_iff, mem_subgroupOf]

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

Goal state before:
pp: n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ (finCongr h).toFun (a * b) = (finCongr h).toFun a * (finCongr h).toFun b

Tactic:
dsimp [ZMod]
          ext
          rw [Fin.val_cast, Fin.val_mul, Fin.val_mul, Fin.val_cast, Fin.val_cast, ← h]

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

Goal state before:
pp: p n : ℕ
h : 0 ≤ Int.negSucc n
⊢ ↑(Int.negSucc n).toNat = ↑(Int.negSucc n)

Tactic:
simp at h

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

Goal state before:
pp: a b : ZMod 0
h : a.val + b.val < 0
⊢ False

Tactic:
simp at h

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ map { toFun := fun d ↦ (n / d, d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal

Tactic:
apply Finset.map_injective (Equiv.prodComm _ _).toEmbedding

Goal state after:
n : ℕ
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding (map { toFun := fun d ↦ (n / d, d), inj' := ⋯ } n.divisors) =
    map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
simp at h

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
by
  by_cases hn : n = 0; · simp [hn]
  rw [← prod_image]
  · exact prod_congr (image_div_divisors_eq_divisors n) (by simp)
  · intro x hx y hy h
    rw [mem_coe, mem_divisors] at hx hy
    exact (div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
z : ℤ
⊢ xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0

Tactic:
by
  rcases z, xy with ⟨_ | _, ⟨_ | _, _ | _⟩⟩
  -- splitting this case saves about 1770 heartbeats i.e. 12.5% faster
  case ofNat.negSucc.negSucc =>
    simp [divisorsAntidiag]
    grind [Nat.cast_inj]
  all_goals
    simp [divisorsAntidiag]
    grind

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1).choose k ≤ 2 ^ n

Tactic:
by_cases lt : n + 1 < k

Goal state after:
case pos
n k : ℕ
lt : n + 1 < k
⊢ (n + 1).choose k ≤ 2 ^ n

case neg
n k : ℕ
lt : ¬n + 1 < k
⊢ (n + 1).choose k ≤ 2 ^ n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
h : a.val < 0
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: m n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
⊢ (a ^ m).val ≤ a.val ^ m

Tactic:
induction m with
  | zero => simp [ZMod.val_one]
  | succ m ih =>
    rw [pow_succ, pow_succ]
    apply le_trans (ZMod.val_mul_le _ _)
    apply Nat.mul_le_mul_right _ ih

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

Goal state before:
pp: case zero
p : ℕ
h : ¬p ∣ 0
⊢ p.maxPowDvdDiv 0 = (0, 0)

Tactic:
simp at h

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

Goal state before:
pp: p n : ℕ
⊢ padicValNat p n ≤ n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
p : ℕ
⊢ padicValNat p 0 ≤ 0

case inr
p n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ≤ n
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inr
p : ℕ
hp : p ≠ 0
n k : ℕ
hp1 : 1 < p
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inr.inl
p : ℕ
hp : p ≠ 0
k : ℕ
hp1 : 1 < p
⊢ (p ^ k * 0).divMaxPow p = divMaxPow 0 p

case inr.inr
p : ℕ
hp : p ≠ 0
n k : ℕ
hp1 : 1 < p
hn : n ≠ 0
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : 1 < p
⊢ p.maxPowDvdDiv p = (1, 1)

Tactic:
simpa using maxPowDvdDiv_base_pow hp 1

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

Goal state before:
pp: case inr.refine_2
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

Tactic:
by_cases h : digits b m = []

Goal state after:
case pos
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
h : b.digits m = []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

case neg
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
h : ¬b.digits m = []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case ind.succ.tail
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ d < b + 2

Tactic:
apply IH ((n + 1) / (b + 2))

Goal state after:
case ind.succ.tail.a
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ (n + 1) / (b + 2) < n + 1

case ind.succ.tail.a
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ d ∈ (b + 2).digits ((n + 1) / (b + 2))
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl
p n : ℕ
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl.inl
p : ℕ
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range (log p 0).succ, 0 / p ^ i.succ = 0 - (p.digits 0).sum

case inl.inr
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
n : ℕ
x : G
⊢ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ↔ x ^ n = 1

Tactic:
IsPeriodicPt,

Goal state after:
G : Type u_1
inst✝ : Monoid G
n : ℕ
x : G
⊢ IsFixedPt (fun x_1 ↦ x * x_1)^[n] 1 ↔ x ^ n = 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: case inr
p n : ℕ
hp : p ≠ 1
⊢ (emultiplicity p n).toNat = padicValNat p n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inr.inl
p : ℕ
hp : p ≠ 1
⊢ (emultiplicity p 0).toNat = padicValNat p 0

case inr.inr
p n : ℕ
hp : p ≠ 1
hn : n ≠ 0
⊢ (emultiplicity p n).toNat = padicValNat p n
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (a * b).factorization p = (a.factorization + b.factorization) p

Tactic:
simp only [add_apply, ← primeFactorsList_count_eq,
    perm_iff_count.mp (perm_primeFactorsList_mul ha hb) p, count_append]

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

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

Tactic:
simp [hp]

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

Goal state before:
pp: n p : ℕ
hp : ¬Prime p
⊢ p ^ n.factorization p ∣ n

Tactic:
simp [hp]

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p.factorization p = 1

Tactic:
simp [hp]

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

Goal state before:
pp: n p : ℕ
hp : ¬Prime p
⊢ p ^ n.factorization p = 1

Tactic:
simp [hp]

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

Goal state before:
pp: n p : ℕ
hp : ¬Prime p
⊢ n / p ^ n.factorization p = n

Tactic:
simp [hp]

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

Goal state before:
pp: n p : ℕ
pp : Prime p
⊢ 0 < p ^ n.factorization p

Tactic:
simp [Nat.pow_pos pp.pos]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
⊢ orderOf (y ^ m) = orderOf y

Tactic:
by
  by_cases hg : IsOfFinOrder y
  · rw [hg.orderOf_pow y m, h.gcd_eq_one, Nat.div_one]
  · rw [m.coprime_zero_left.1 (orderOf_eq_zero hg ▸ h), pow_one]

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

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

Tactic:
simp [hp]

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

Goal state before:
pp: p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ n + 1 ∣ (n + 1) * n.choose k

Tactic:
exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

pp: case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1

Tactic:
· rw [Int.natCast_dvd_natCast, orderOf_dvd_iff_pow_eq_one, zpow_natCast]

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
⊢ e.factorization ≤ a.factorization ⊓ b.factorization

Tactic:
have hea' := (factorization_le_iff_dvd he_pos ha_pos).mpr hea

Goal state after:
case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : e.factorization ≤ a.factorization
⊢ e.factorization ≤ a.factorization ⊓ b.factorization
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
n k : ℕ
⊢ n + 1 ∣ (n + 1) * n.choose k

Tactic:
exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h : zpowers x = zpowers (x ^ k)
hx_mem : x ∈ zpowers (x ^ k)
hy_mem : x ^ k ∈ zpowers x
l : ℤ
hl : (x ^ k) ^ l = x
⊢ x = x ^ k ∨ x⁻¹ = x ^ k

Tactic:
← zpow_mul

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h : zpowers x = zpowers (x ^ k)
hx_mem : x ∈ zpowers (x ^ k)
hy_mem : x ^ k ∈ zpowers x
l : ℤ
hl : x ^ (k * l) = x
⊢ x = x ^ k ∨ x⁻¹ = x ^ k
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ Icc 1 (n.factorization p) = {i ∈ Ico 1 n | p ^ i ∣ n}

Tactic:
ext x

Goal state after:
case inr
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : ℕ
⊢ x ∈ Icc 1 (n.factorization p) ↔ x ∈ {i ∈ Ico 1 n | p ^ i ∣ n}
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
⊢ {i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Icc 1 b | p ^ i ∣ n}

Tactic:
ext x

Goal state after:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
⊢ x ∈ {i ∈ Ico 1 n | p ^ i ∣ n} ↔ x ∈ {i ∈ Icc 1 b | p ^ i ∣ n}
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case mpr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ of' k G g * (x /ᵒᶠ g)

Tactic:
exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
x : G
inst✝ : DecidableEq G
this : Fintype ↥(zpowers x) := (zpowers x).instFintypeSubtypeMemOfDecidablePred
⊢ Finset.image (fun i ↦ x ^ i) (Finset.range (orderOf x)) = (↑(zpowers x)).toFinset

Tactic:
ext x

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
x✝ : G
inst✝ : DecidableEq G
this : Fintype ↥(zpowers x✝) := (zpowers x✝).instFintypeSubtypeMemOfDecidablePred
x : G
⊢ x ∈ Finset.image (fun i ↦ x✝ ^ i) (Finset.range (orderOf x✝)) ↔ x ∈ (↑(zpowers x✝)).toFinset
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mp
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑n = 0
⊢ p ∣ n

Tactic:
rw [← Nat.mod_add_div n p, Nat.cast_add, Nat.cast_mul, H, zero_mul, add_zero] at h

Goal state after:
case mp
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
n : ℕ
H : ↑p = 0
h : ↑(n % p) = 0
⊢ p ∣ n