mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p = C (coeff 0 p)
⊢ (C (coeff 0 p)).totalDegree = 0

Tactic:
totalDegree_C

Goal state after:
case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p = C (coeff 0 p)
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ #f.eraseLead.support = #f.support - 1

Tactic:
by
  by_cases hf : f = 0
  · rw [hf, eraseLead_zero, support_zero, card_empty]
  · rw [← card_support_eraseLead_add_one hf, add_tsub_cancel_right]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
⊢ σ ∈ (((optionEquivLeft R S₁) p).coeff i).support → (i + σ.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
hσ

Goal state after:
case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ (i + σ.sum fun x e ↦ e) ≤ p.totalDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
⊢ σ ∈ (((optionEquivLeft R S₁) p).coeff i).support → (σ.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
hσ

Goal state after:
case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ (σ.sum fun x e ↦ e) ≤ p.totalDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ (p * q).reverse.coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1

Tactic:
reverse_mul

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ (p.reverse * q.reverse).coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1

R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
s' : S₁ → R
f : (MvPolynomial S₁ R)[X]
i : ℕ
⊢ (Polynomial.map (eval s') f).coeff i = (eval s') (f.coeff i)

Tactic:
by
  simp only [Polynomial.coeff_map]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ m 0 = i
⊢ ¬coeff (cons i m.tail) f = 0 ∧ cons i m.tail = m

Tactic:
← h.2,

Goal state after:
case h
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ m 0 = i
⊢ ¬coeff (cons (m 0) m.tail) f = 0 ∧ cons (m 0) m.tail = m
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case cons
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (hd * tl.prod).coeff ((tl.length + 1) * n) = hd.coeff n * (List.map (fun p ↦ p.coeff n) tl).prod

Tactic:
rw [add_mul, one_mul, add_comm, ← IH hl', mul_comm tl.length]

Goal state after:
case cons
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (hd * tl.prod).coeff (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x ≠ 0

Tactic:
rwa [ne_eq]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ degreeLT R (n + 1) = degreeLE R ↑n

Tactic:
by
  ext x
  by_cases x_zero : x = 0
  · simp_rw [x_zero, Submodule.zero_mem]
  · rw [mem_degreeLT, mem_degreeLE, ← natDegree_lt_iff_degree_lt (by rwa [ne_eq]),
      ← natDegree_le_iff_degree_le, Nat.lt_succ_iff]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ i, x ∈ I.leadingCoeffNth i) ↔ ∃ p ∈ I, p.leadingCoeff = x

Tactic:
simp only [mem_leadingCoeffNth]

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ i, ∃ p ∈ I, p.degree ≤ ↑i ∧ p.leadingCoeff = x) ↔ ∃ p ∈ I, p.leadingCoeff = x
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
⊢ I ≤ Submodule.span R[X] ↑s

Tactic:
have : Submodule.span R[X] ↑s = Ideal.span ↑s := rfl

Goal state after:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
⊢ I ≤ Submodule.span R[X] ↑s
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
t : Set A
h : t.Finite
⊢ FiniteType R ↥(adjoin R t)

Tactic:
← Subalgebra.fg_iff_finiteType

Goal state after:
R : Type uR
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
t : Set A
h : t.Finite
⊢ (adjoin R t).FG
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) p).ker ⊔ ((aeval f) q).ker
x : M
hx : x ∈ ((aeval f) p).ker
y : M
hy : y ∈ ((aeval f) q).ker
hxy : x + y = v
h_eval_x : ((aeval f) (p * q)) x = 0
⊢ ((aeval f) (p * q)) y = 0

Tactic:
rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hy, map_zero]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsNoetherianRing (MvPolynomial (Fin 0) R)

Tactic:
apply isNoetherianRing_of_ringEquiv R
  symm; apply MvPolynomial.isEmptyRingEquiv R (Fin 0)

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroupWithOne G
inst✝ : CharZero G
a b : ℤ
n : ℕ
⊢ ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [PMOD ↑n]

Tactic:
by
  simpa using intCast_modEq_intCast (G := G) (z := n)

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a + b ≡ a [ZMOD n] ↔ n ∣ b

Tactic:
by
  simp [modEq_iff_dvd]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
c : Subalgebra R C
⊢ (lift f).range ≤ c ↔ Algebra.adjoin R ↑(NonUnitalAlgHom.range f) ≤ c

Tactic:
lift_range_le,

Goal state after:
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
c : Subalgebra R C
⊢ NonUnitalAlgHom.range f ≤ c.toNonUnitalSubalgebra ↔ Algebra.adjoin R ↑(NonUnitalAlgHom.range f) ≤ c
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
pp : Prime p
i : ℕ
⊢ p.Coprime i ∨ ¬p.Coprime i

Tactic:
apply em

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m : ℕ
hm : IsPeriodicPt f m x
n : ℕ
⊢ IsPeriodicPt f (m * n) x

Tactic:
by
  simp only [IsPeriodicPt, iterate_mul, hm.isFixedPt.iterate n]

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

Goal state before:
pp: case pos
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ IsPeriodicPt f (Nat.find hx) x

Tactic:
exact (Nat.find_spec hx).2

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

Goal state before:
pp: case neg
α : Type u_1
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ IsPeriodicPt f 0 x

Tactic:
· exact isPeriodicPt_zero f x

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

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m :
  l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is :: is.permutationsAux [] ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
⊢ l ~ t :: ts ++ is

Tactic:
rcases m with (m | ⟨l₁, l₂, m, _, rfl⟩)

Goal state after:
case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m : l ∈ ts.permutationsAux (t :: is)
⊢ l ~ t :: ts ++ is

case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left✝ : l₂ ≠ []
⊢ l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is
Module: Mathlib.Dynamics.PeriodicPts.Defs

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

Tactic:
by
  apply Nat.dvd_antisymm
  · apply IsPeriodicPt.minimalPeriod_dvd
    rw [IsPeriodicPt, IsFixedPt, ← iterate_mul, ← Nat.mul_div_assoc _ (gcd_dvd_left _ _),
      mul_comm, Nat.mul_div_assoc _ (gcd_dvd_right _ _), mul_comm, iterate_mul]
    exact (isPeriodicPt_minimalPeriod f x).iterate _
  · apply Coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd h)
    apply Nat.dvd_of_mul_dvd_mul_right h
    rw [Nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc, Nat.div_mul_cancel (gcd_dvd_right _ _),
      mul_comm]
    apply IsPeriodicPt.minimalPeriod_dvd
    rw [IsPeriodicPt, IsFixedPt, iterate_mul]
    exact isPeriodicPt_minimalPeriod _ _

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

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

Tactic:
Nat.mul_comm (_ + 1),

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

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is

Tactic:
rw [permutationsAux_cons, mem_foldr_permutationsAux2]

Goal state after:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f : α → α
x : α
inst✝ : Fintype α
⊢ minimalPeriod f x ≤ card α

Tactic:
rw [← periodicOrbit_length]
  exact List.Nodup.length_le_card nodup_periodicOrbit

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

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

Tactic:
by
  refine ⟨fun h H ↦ ?_, nodup_permutations'Aux_of_notMem _ _⟩
  obtain ⟨⟨k, hk⟩, hk'⟩ := get_of_mem H
  rw [nodup_iff_injective_get] at h
  apply k.succ_ne_self.symm
  have kl : k < (permutations'Aux x s).length := by simpa [Nat.lt_succ_iff] using hk.le
  have k1l : k + 1 < (permutations'Aux x s).length := by simpa using hk
  rw [← @Fin.mk.inj_iff _ _ _ kl k1l]; apply h
  rw [get_permutations'Aux, get_permutations'Aux]
  have hl : length (s.insertIdx k x) = length (s.insertIdx (k + 1) x) := by
    rw [length_insertIdx_of_le_length hk.le, length_insertIdx_of_le_length (Nat.succ_le_of_lt hk)]
  exact ext_get hl fun n hn hn' => by grind

Goal state after:
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 (hg : g.val • x = x)

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ˣ
hg : ↑g • x = x
⊢ g ∈ ⊥
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α) (a :: l) []
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
have := isRotated_nil_iff.1 hab

Goal state after:
case cons.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α) (a :: l) []
this : a :: l = []
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
⊢ ∀ (x : R) (x_1 : ℕ), 0 < x_1 → x ^ x_1 = 0 → ¬Prime x

Tactic:
intro x n _hn hx

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain r ↑(range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ

Tactic:
range_succ,

Goal state after:
r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain r ↑(range n ++ [n]) ↔ r n 0 ∧ ∀ m < n, r m m.succ
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
⊢ ((k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList).prod = k + 2

Tactic:
List.prod_cons,

Goal state after:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
⊢ (k + 2).minFac * ((k + 2) / (k + 2).minFac).primeFactorsList.prod = k + 2
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ a ^ (n + 1) ∣ b

Tactic:
rw [← Nat.prod_primeFactorsList hb, ← hu1.prod_eq, ← prod_replicate]

Goal state after:
case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ (replicate (n + 1) a).prod ∣ u.prod
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 ^ (n + 1) * c ≠ 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList

Tactic:
rw [Ne, pow_succ', mul_assoc, mul_eq_zero, _root_.not_or] at hb

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊥.relIndex H = Nat.card ↥H

Tactic:
by
  rw [relIndex, bot_subgroupOf, index_bot]

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
x : ZMod n
⊢ (castHom ⋯ R) x = 0 → x = 0

Tactic:
obtain ⟨k, rfl⟩ := ZMod.intCast_surjective x

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ (castHom ⋯ R) ↑k = 0 → ↑k = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Injective val

Tactic:
cases n
  · cases NeZero.ne 0 rfl
  intro a b h
  dsimp [ZMod]
  ext
  exact h

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ (a * b).val = a.val * b.val ↔ a.val * b.val < n

Tactic:
constructor <;> intro h
  · rw [← h]; apply ZMod.val_lt
  · apply ZMod.val_mul_of_lt h

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
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.Data.Nat.Choose.Bounds

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

Tactic:
rw [le_div_iff₀']
  · norm_cast
    rw [← Nat.descFactorial_eq_factorial_mul_choose]
    exact n.descFactorial_le_pow r
  exact mod_cast r.factorial_pos

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

Goal state before:
pp: m : ℕ
inst✝¹ : NeZero m
n : ℕ
inst✝ : NeZero n
a : ZMod m
⊢ a.cast.val < m

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne m)

Goal state after:
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
⊢ a.cast.val < m + 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < n
⊢ a.cast.val = a.val

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (NeZero.ne m)

Goal state after:
n m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
h : a.val < n
⊢ a.cast.val = a.val
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inr.inl
b n : ℕ
hn : n ≠ 0
hb : b ≤ 1
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
interval_cases b

Goal state after:
case inr.inl.«0»
b n : ℕ
hn : n ≠ 0
hb : 0 ≤ 1
⊢ (digits 0 n).length ≤ (digits 0 (n + 1)).length

case inr.inl.«1»
b n : ℕ
hn : n ≠ 0
hb : 1 ≤ 1
⊢ (digits 1 n).length ≤ (digits 1 (n + 1)).length
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by_contra nh

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
nh : ¬FiniteMultiplicity a b
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
hm : (if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤) < ↑m
nh : a ^ m ∣ b
⊢ False

Tactic:
split at hm

Goal state after:
case isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
hm : ↑(Nat.find h✝) < ↑m
⊢ False

case isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : ¬FiniteMultiplicity a b
hm : ⊤ < ↑m
⊢ False
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case n
b b' : ℕ
h : b' % b = 1
n : ℕ
| b

pp: case a
b b' : ℕ
h : b' % b = 1
n : ℕ
| n

pp: case b
b b' : ℕ
h : b' % b = 1
n : ℕ
| ofDigits 1 (b'.digits n)

Tactic:
· skip

Goal state after:
case a
b b' : ℕ
h : b' % b = 1
n : ℕ
| n

case b
b b' : ℕ
h : b' % b = 1
n : ℕ
| ofDigits 1 (b'.digits n)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case n
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑b

pp: case a
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n

pp: case b
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ofDigits c (b'.digits n)

Tactic:
· skip

Goal state after:
case a
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ↑n

case b
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ofDigits c (b'.digits n)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
⊢ ¬IsOfFinOrder x

Tactic:
simp_rw [isOfFinOrder_iff_pow_eq_one, not_exists, not_and]
  intro n hn_pos hnx
  rw [← pow_zero x] at hnx
  rw [h hnx] at hn_pos
  exact irrefl 0 hn_pos

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
this : FiniteMultiplicity p b
⊢ emultiplicity p (a + b) = emultiplicity p b

Tactic:
rw [this.emultiplicity_eq_multiplicity] at *

Goal state after:
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ emultiplicity p (a + b) = ↑(multiplicity p b)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k✝ k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a ^ (k + 1))

Tactic:
rw [_root_.pow_succ']; exact hp.finiteMultiplicity_mul ha (ha.pow hp)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x

pp: case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
· exact ⟨0, by rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]⟩

Goal state after:
case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_2
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p * i + r ≠ 0

Tactic:
contrapose hr0

Goal state after:
case refine_2
p r i : ℕ
pp : Prime p
h : p ∣ r
hr0 : p * i + r = 0
⊢ r = 0
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
s : Finset β
f : β → α
⊢ emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
⊢ p ∣ a

Tactic:
simpa [multiplicity_eq_zero] using nh.ne.symm

Goal state after: