mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case refine_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ (Quotient.mk (I i)) e = 1

Tactic:
simp [eq_sub_of_add_eq' hue, map_sub, eq_zero_iff_mem.mpr hu]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
⊢ (unitization s).range = subalgebraOfSubring (Subring.closure ↑s)

Tactic:
have := AddSubgroupClass.zsmulMemClass (S := S)

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
this : SMulMemClass S ℤ R
⊢ (unitization s).range = subalgebraOfSubring (Subring.closure ↑s)
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
a b : R
⊢ a + b + b = a

Tactic:
by
  rw [add_assoc, add_self_eq_zero, add_zero]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
x : ι → R
y : R
hy : ∀ (i : ι), (Quotient.mk (I i)) y = (Quotient.mk (I i)) (x i)
⊢ ∃ r, ∀ (i : ι), r - x i ∈ I i

Tactic:
exact ⟨y, fun i ↦ (Submodule.Quotient.eq (I i)).mp <| hy i⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type w
inst✝³ : Ring R✝
inst✝² : Semiring S
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
⊢ Pairwise (IsCoprime on f)

Tactic:
intro i

Goal state after:
R✝ : Type u
S : Type v
F : Type w
inst✝³ : Ring R✝
inst✝² : Semiring S
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
i : Fin 2
⊢ ∀ ⦃j : Fin 2⦄, i ≠ j → (IsCoprime on f) i j
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
C : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : Semiring B
inst✝⁶ : StarRing B
inst✝⁵ : Algebra R B
inst✝⁴ : StarModule R B
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ (∀ (r : R), (algebraMap R A) r ∈ s) ∧ ∀ {x : A}, x ∈ s → star x ∈ s
⊢ 1 ∈ s

Tactic:
simpa using h.2.2.1 1

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

Goal state before:
pp: case cons
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ l' ∈ (l ++ (t :: y :: ys ++ ts)) :: (permutationsAux2 t ts [] ys fun x ↦ l ++ y :: x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

Tactic:
show (fun x : List α => l ++ y :: x) = (l ++ [y] ++ ·) by simp,

Goal state after:
case cons
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ l' ∈ (l ++ (t :: y :: ys ++ ts)) :: (permutationsAux2 t ts [] ys fun x ↦ l ++ [y] ++ x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ (t :: is ++ ts).permutationsAux is' =
    map (fun x ↦ x ++ ts) ((t :: is).permutationsAux is') ++ ts.permutationsAux ((t :: is).reverse ++ is')

Tactic:
simp only [foldr_permutationsAux2, ih, map_flatMap, cons_append, permutationsAux_cons, map_append,
    reverse_cons, append_assoc]

Goal state after:
case cons
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ flatMap (fun y ↦ (permutationsAux2 t (is ++ ts) [] y id).snd) is'.permutations ++
      (map (fun x ↦ x ++ ts) (is.permutationsAux (t :: is')) ++ ts.permutationsAux (is.reverse ++ t :: is')) =
    flatMap (fun a ↦ map (fun x ↦ x ++ ts) (permutationsAux2 t is [] a id).snd) is'.permutations ++
      (map (fun x ↦ x ++ ts) (is.permutationsAux (t :: is')) ++ ts.permutationsAux (is.reverse ++ t :: ([] ++ is')))
Module: Mathlib.Dynamics.PeriodicPts.Defs

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

Tactic:
rcases hx with ⟨r, hr, hr'⟩

Goal state after:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ IsPeriodicPt f m x
Module: Mathlib.Dynamics.PeriodicPts.Defs

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

Tactic:
by simp only [minimalPeriod, dif_neg hx]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
h : x ∉ periodicPts f
⊢ ¬0 < minimalPeriod f x

Tactic:
by simp only [minimalPeriod, dif_neg h, lt_irrefl 0, not_false_iff]

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

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

Tactic:
simp at x_mem

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
⊢ IsMulCommutative ↥(adjoin R s)

Tactic:
have := adjoin_le_centralizer_centralizer R s

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
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : adjoin R s ≤ centralizer R ↑(centralizer R s)
⊢ IsMulCommutative ↥(adjoin R s)
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f : α → α
x : α
inst✝ : Fintype α
⊢ (periodicOrbit f x).length ≤ card α

Tactic:
exact List.Nodup.length_le_card nodup_periodicOrbit

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

Goal state before:
pp: case inl
α : Type u_1
f : α → α
inst✝ : Finite α
h : Injective f
x : α
m n : ℕ
heq : f^[m] x = f^[n] x
hne : m ≠ n
hlt : m < n
⊢ x ∈ periodicPts f

Tactic:
exact mk_mem_periodicPts (by lia) (iterate_cancel h heq.symm)

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

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

Tactic:
by_cases ha₀ : a = head
  · subst ha₀
    simp
    grind
  rw [prev_eq_getElem_idxOf_pred_of_ne_head ha ha₀]
  congr
  rw [← Nat.add_sub_assoc, Nat.sub_add_comm, Nat.add_mod_right, Nat.mod_eq_of_lt]
  all_goals grind

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
i✝ : ℕ
h₁✝ : i✝ < (pmap l.next l ⋯).length
h₂✝ : i✝ < (l.rotate 1).length
⊢ l.next l[i✝] ⋯ = l[(i✝ + 1) % l.length]

Tactic:
next_getElem _ h

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
i✝ : ℕ
h₁✝ : i✝ < (pmap l.next l ⋯).length
h₂✝ : i✝ < (l.rotate 1).length
⊢ l[(i✝ + 1) % l.length] = l[(i✝ + 1) % l.length]
Module: Mathlib.Data.List.Cycle

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

Tactic:
rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn
            rw [← hd c _ _ _ hn]
            simp [and_comm]

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

Goal state before:
pp: ⊢ primeFactorsList 0 = []

Tactic:
rw [primeFactorsList]

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

Goal state before:
pp: ⊢ primeFactorsList 1 = []

Tactic:
rw [primeFactorsList]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ stabilizer G ↑1 = H

Tactic:
by
  ext
  simp [QuotientGroup.eq]

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

Goal state before:
pp: n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)

Tactic:
rw [primeFactorsList]

Goal state after:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
⊢ (n + 2).primeFactorsList = (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList

Tactic:
rw [primeFactorsList]

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

Goal state before:
pp: case succ
n : ℕ
a b : Fin (n + 1)
⊢ ↑(if n + 1 ≤ ↑a + ↑b then ↑a + ↑b - (n + 1) else ↑a + ↑b) =
    if ↑n + 1 ≤ ↑↑a + ↑↑b then cast a + cast b - (↑n + 1) else cast a + cast b

Tactic:
norm_cast

Goal state after:
case succ
n : ℕ
a b : Fin (n + 1)
⊢ ↑(if n + 1 ≤ ↑a + ↑b then ↑a + ↑b - (n + 1) else ↑a + ↑b) =
    if n + 1 ≤ ↑a + ↑b then cast a + cast b - ↑(n + 1) else cast a + cast b
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R : Type u
M' : Type v
inst✝² : Semiring R
inst✝¹ : Infinite M'
inst✝ : Nontrivial R
⊢ #R[M'] = max (lift.{v, u} #R) (lift.{u, v} #M')

Tactic:
simp [coeffEquiv.cardinal_eq, max_comm]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R : Type u
M' : Type v
inst✝² : Semiring R
inst✝¹ : Nonempty M'
inst✝ : Infinite R
⊢ #R[M'] = max (lift.{v, u} #R) (lift.{u, v} #M')

Tactic:
simp [coeffEquiv.cardinal_eq, max_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
rcases z, xy with ⟨_ | _, ⟨_ | _, _ | _⟩⟩

Goal state after:
case ofNat.ofNat.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, ofNat a✝) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (ofNat a✝¹, ofNat a✝).1 * (ofNat a✝¹, ofNat a✝).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

case ofNat.ofNat.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, -[a✝+1]) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (ofNat a✝¹, -[a✝+1]).1 * (ofNat a✝¹, -[a✝+1]).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

case ofNat.negSucc.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], ofNat a✝) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (-[a✝¹+1], ofNat a✝).1 * (-[a✝¹+1], ofNat a✝).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

case ofNat.negSucc.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], -[a✝+1]) ∈ (ofNat a✝²).divisorsAntidiag ↔
    (-[a✝¹+1], -[a✝+1]).1 * (-[a✝¹+1], -[a✝+1]).2 = ofNat a✝² ∧ ofNat a✝² ≠ 0

case negSucc.ofNat.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, ofNat a✝) ∈ -[a✝²+1].divisorsAntidiag ↔
    (ofNat a✝¹, ofNat a✝).1 * (ofNat a✝¹, ofNat a✝).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

case negSucc.ofNat.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (ofNat a✝¹, -[a✝+1]) ∈ -[a✝²+1].divisorsAntidiag ↔
    (ofNat a✝¹, -[a✝+1]).1 * (ofNat a✝¹, -[a✝+1]).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

case negSucc.negSucc.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], ofNat a✝) ∈ -[a✝²+1].divisorsAntidiag ↔
    (-[a✝¹+1], ofNat a✝).1 * (-[a✝¹+1], ofNat a✝).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0

case negSucc.negSucc.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (-[a✝¹+1], -[a✝+1]) ∈ -[a✝²+1].divisorsAntidiag ↔
    (-[a✝¹+1], -[a✝+1]).1 * (-[a✝¹+1], -[a✝+1]).2 = -[a✝²+1] ∧ -[a✝²+1] ≠ 0
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑r ! * ↑(n.choose r) ≤ ↑n ^ r

Tactic:
norm_cast

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ r ! * n.choose r ≤ n ^ r
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ ↑k ! * ↑(n.choose k) < ↑n ^ k

Tactic:
norm_cast

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ k ! * n.choose k < n ^ k
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case inl
n k : ℕ
h : k ≤ n
⊢ n.choose k ≤ (n + 1 - k) ^ k

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le h

Goal state after:
case inl
k m : ℕ
h : k ≤ k + m
⊢ (k + m).choose k ≤ (k + m + 1 - k) ^ k
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑(n + 1 - r) ^ r ≤ ↑r ! * ↑(n.choose r)

Tactic:
norm_cast

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ r ! * n.choose r
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
⊢ (2 * n + 2).choose (n + 1) * (n + 1) = (2 * n + 1).choose n * (2 * n + 2)

Tactic:
rw [choose_succ_right_eq, choose_mul_succ_eq]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val = (-a).val % n

Tactic:
rw [Nat.mod_eq_of_lt (-a).val_lt]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val + a.val ≡ n - a.val + a.val [MOD n]

Tactic:
by
          rw [Nat.ModEq, ← val_add, neg_add_cancel, tsub_add_cancel_of_le a.val_le, Nat.mod_self,
            val_zero]

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

Goal state before:
pp: case pos
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : m = 0
⊢ val 0 ^ m < n

pp: case neg
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : ¬m = 0
⊢ val 0 ^ m < n

Tactic:
· cases hm; simp [ilt.out]

Goal state after:
case neg
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : ¬m = 0
⊢ val 0 ^ m < n
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case hn
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ k * n ≠ 0

Tactic:
exact Nat.mul_ne_zero (Nat.ne_of_gt <| Nat.pow_pos <| Nat.zero_lt_of_lt hp) hn

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case h₂
a b : ℕ
h_congr_thm✝ :
  ∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c), (∀ (h : c), x_1 ⋯ = u h) → (∀ (h : ¬c), y ⋯ = v h) → dite b x_1 y = dite c u v
h✝ : ∃ n, ¬a ^ (n + 1) ∣ b
x✝ : ℕ
⊢ ↑a ^ (x✝ + 1) ∣ ↑b ↔ a ^ (x✝ + 1) ∣ b

Tactic:
norm_cast

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case h₁
a b x✝ : ℕ
⊢ ↑a ^ (x✝ + 1) ∣ ↑b ↔ a ^ (x✝ + 1) ∣ b

Tactic:
norm_cast

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ a ^ zero ∣ b

Tactic:
by
        rw [_root_.pow_zero]
        exact one_dvd _

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ ↑(multiplicity a b) < ↑m

Tactic:
norm_cast

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ↑n < ↑(n + 1)

Tactic:
norm_cast

Goal state after:
case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ n < n + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b f : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1

Tactic:
by
  induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length])
  | succ f ih =>
    grind

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

Goal state before:
pp: n : ℕ
⊢ ofDigits (-1) [n] = (List.map (fun n ↦ ↑n) [n]).alternatingSum

Tactic:
simp [ofDigits, List.alternatingSum]

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

Goal state before:
pp: b f n e : ℕ
h_e_pos : 0 < e
hlt : n < b ^ e
⊢ (b.toDigitsCore f n []).length ≤ e

Tactic:
induction f generalizing n e hlt h_e_pos with

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
H : Submonoid G
x : ↥H
⊢ (∃ n, 0 < n ∧ ↑x ^ n = 1) ↔ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
norm_cast

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.InvOn (b.digitsAppend l) (ofDigits b) {L | L.length = l ∧ ∀ x ∈ L, x < b} {n | n < b ^ l}

Tactic:
refine ⟨fun L hL ↦ ?_, fun _ _ ↦ by rw [digitsAppend, ofDigits_append_replicate_zero,
    ofDigits_digits]⟩
  refine (injOn_ofDigits hb l) ⟨?_, ?_⟩ hL
    (by rw [digitsAppend, ofDigits_append_replicate_zero, ofDigits_digits])
  · rw [length_digitsAppend hb _ (mapsTo_ofDigits hb _ hL)]
  · exact fun x hx ↦ lt_of_mem_digitsAppend hb l x hx

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : 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:
norm_cast

Goal state after:
case pos
α : 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
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
simp [factorization_mul ha hb, pow_add]

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

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

Tactic:
exact Nat.add_right_cancel h₁

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

Goal state before:
pp: case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ ∀ ⦃x : ℕ⦄, 1 ≤ x → x < log p n + 1 → k % p ^ x + (n - k) % p ^ x < p ^ x

Tactic:
intro i

Goal state after:
case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
⊢ 1 ≤ i → i < log p n + 1 → k % p ^ i + (n - k) % p ^ i < p ^ i
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) = x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) * ↑p)

Tactic:
norm_cast

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) = x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p * p)
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)

Tactic:
by
  rw [← sub_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]

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
⊢ ↑(multiplicity p ((p ^ n).choose k)) =
    ↑(multiplicity p ((p ^ n).choose k)) + ↑(multiplicity p k) - ↑(multiplicity p k)

Tactic:
norm_cast

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ multiplicity p ((p ^ n).choose k) = multiplicity p ((p ^ n).choose k) + multiplicity p k - multiplicity p k
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
s : Submonoid G
hs : (↑s).Finite
x : G
hx : x ∈ s
⊢ orderOf x ≤ Nat.card ↥s

Tactic:
← Nat.card_submonoidPowers

Goal state after:
G : Type u_6
inst✝ : Group G
s : Submonoid G
hs : (↑s).Finite
x : G
hx : x ∈ s
⊢ Nat.card ↥(powers x) ≤ Nat.card ↥s
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
g' : G
⊢ (of' k G g * x %ᵒᶠ g).coeff g' = (coeff 0) g'

Tactic:
simp only [of'_apply, coeff_zero, Finsupp.coe_zero, Pi.zero_apply]

Goal state after:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
g' : G
⊢ (single g 1 * x %ᵒᶠ g).coeff g' = 0
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : p.coeff 0 = 0
⊢ M (p.divX * X + C (p.coeff 0))

Tactic:
hcp0,

Goal state after:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : p.coeff 0 = 0
⊢ M (p.divX * X + C 0)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
⊢ c ∣ p ^ n

Tactic:
rw [← CharP.cast_eq_zero_iff R c, ← hn, Nat.cast_card_eq_zero]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree