mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S → ∃ ι x f, Surjective ⇑f

pp: case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ ι x f, Surjective ⇑f) → FiniteType R S

Tactic:
· rw [iff_quotient_mvPolynomial]
    rintro ⟨s, f, hsur⟩
    use { x : S // x ∈ s }, inferInstance, f

Goal state after:
case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ ι x f, Surjective ⇑f) → FiniteType R S
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : f.FiniteType
hg : Surjective ⇑g
⊢ (g.comp f).FiniteType

Tactic:
by
  algebraize_only [f, g.comp f]
  exact ‹Algebra.FiniteType _ _›.of_surjective
    { g with
      toFun := g
      commutes' := fun a => rfl }
    hg

Goal state after:
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
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
⊢ p.leadingCoeff ∈ M

Tactic:
exact hm2 k ((I.mem_leadingCoeffNth _ _).2
              ⟨_, hp, hn ▸ Polynomial.degree_le_natDegree, rfl⟩)

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

Goal state before:
pp: R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ ↑(b - a + a) = ↑a

Tactic:
Nat.sub_add_cancel hle,

Goal state after:
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ ↑b = ↑a
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
x : R
⊢ (Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J ⊔ I

Tactic:
← mem_comap,

Goal state after:
R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
x : R
⊢ x ∈ comap (Quotient.mk I) (map (Quotient.mk I) J) ↔ x ∈ J ⊔ I
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x : R
⊢ 2 • x = 0

Tactic:
rw [two_zsmul, add_self_eq_zero]

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

Goal state before:
pp: case mpr
m n : ℕ
h : ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬m.Coprime n

Tactic:
obtain ⟨p, hp⟩ := h

Goal state after:
case mpr
m n p : ℕ
hp : Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬m.Coprime n
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
⊢ p ∣ m / p ^ k * (n / p ^ l)

Tactic:
simpa [Nat.div_mul_div_comm hpm hpn] using hpd3

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✝
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
S : Type v
inst✝² : Ring S
I : Ideal R
J : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R →+* S
hIJ : I ≤ comap f J
x✝ : R
ha : x✝ ∈ I
⊢ ((Quotient.mk J).comp f) x✝ = 0

Tactic:
simpa [Function.comp_apply, RingHom.coe_comp, Quotient.eq_zero_iff_mem] using hIJ ha

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
p : Ideal R
inst✝ : p.IsPrime
hIP : I ≤ p
⊢ (map (Quotient.mk I) p).IsPrime

Tactic:
apply Ideal.map_isPrime_of_surjective

Goal state after:
case hf
R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
p : Ideal R
inst✝ : p.IsPrime
hIP : I ≤ p
⊢ Surjective ⇑(Quotient.mk I)

case hk
R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
p : Ideal R
inst✝ : p.IsPrime
hIP : I ≤ p
⊢ ker (Quotient.mk I) ≤ p
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
s : Set A
a✝ : A
hx : a✝ ∈ (Algebra.adjoin R (s ∪ star s)).carrier
⊢ star a✝ ∈ (Algebra.adjoin R (s ∪ star s)).carrier

Tactic:
by
      rwa [Subalgebra.mem_carrier, ← Subalgebra.mem_star_iff, Subalgebra.star_adjoin_comm,
        Set.union_star, star_star, Set.union_comm]

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
⊢ GaloisConnection (adjoin R) SetLike.coe

Tactic:
intro s 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
S : StarSubalgebra R A
⊢ adjoin R s ≤ S ↔ s ⊆ ↑S
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.mpr
α : 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₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts) →
    l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts

Tactic:
· rintro ⟨_ | ⟨y', l₁⟩, l₂, l0, ye, rfl⟩
    · simp [ye]
    · simp only [cons_append] at ye
      rcases ye with ⟨rfl, rfl⟩
      exact Or.inr ⟨l₁, l₂, l0, by simp⟩

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

Goal state before:
pp: case pos.refine_1.inl
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n = minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
rwa [hM', hM, iterate_minimalPeriod]

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

Goal state before:
pp: case pos.refine_1.inr
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n < minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
· exact H _ hM'

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)

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:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
⊢ m ^ period m a • a = a

Tactic:
by
  rw [period_eq_minimalPeriod, ← smul_iterate_apply, iterate_minimalPeriod]

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

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

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

Goal state after:
case inr
α : Type u_1
f : α → α
inst✝ : Finite α
h : Injective f
x : α
m n : ℕ
heq : f^[m] x = f^[n] x
hne : m ≠ n
hlt : n < m
⊢ x ∈ periodicPts f
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l ≠ []
⊢ l.prev (l.head hl) ⋯ = l.getLast hl

Tactic:
cases l with
  | nil => contradiction
  | cons head tail => apply prev_getLast_cons

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

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ (a :: l).rotate 1 = l ++ [a]

Tactic:
by rw [rotate_cons_succ, rotate_zero]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
x : orbitRel.Quotient G α
⊢ ∀ (x_1 y : ↑x.orbit), ∃ g, g • x_1 = y

Tactic:
induction x using Quotient.inductionOn'

Goal state after:
case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ : α
⊢ ∀ (x y : ↑(orbitRel.Quotient.orbit (Quotient.mk'' a✝))), ∃ g, g • x = y
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
⊢ g ∈ (MulAction.toPermHom G (G ⧸ H)).ker

Tactic:
apply Equiv.Perm.ext

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
⊢ ∀ (x : G ⧸ H), ((MulAction.toPermHom G (G ⧸ H)) g) x = 1 x
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a : G
⊢ a * a ∈ H

Tactic:
rw [mul_mem_iff_of_index_two h]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊓ K).index ≤ H.index * K.index

Tactic:
simp_rw [← relIndex_top_right, relIndex_inf_le]

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

Goal state before:
pp: a : ℤ
⊢ ↑a.natAbs = ↑(a.natAbs.gcd 0)

Tactic:
by rw [Nat.gcd_zero_right]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ.inr.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 = 0
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

pp: case succ.succ.inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : 0 < x + 1
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
· simp only [eq_neg_of_add_eq_zero_left hx, h, neg_one_geom_sum, if_false, zero_lt_one]

Goal state after:
case succ.succ.inr.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : 0 < x + 1
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ 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) ∧ p ^ k ≠ 0 ↔ ∃ j ≤ k, x = p ^ j
Module: Mathlib.Data.Nat.Choose.Central

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

Tactic:
rw [two_mul n, add_assoc,
                                                               Nat.add_sub_cancel_left]

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:
Nat.mod_eq_of_lt (-a).val_lt

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : NonAssocSemiring R
f g : ZMod n →+* R
k : ℤ
⊢ f ↑k = g ↑k

Tactic:
let φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))

Goal state after:
n : ℕ
R : Type u_1
inst✝ : NonAssocSemiring R
f g : ZMod n →+* R
k : ℤ
φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
⊢ f ↑k = g ↑k
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inl
n k l : ℕ
hn : n ≠ 0
h : 0 ^ k * l = n
hl : ¬0 ∣ l
⊢ maxPowDvdDiv 0 n = (k, l)

pp: case inr.inl
n k l : ℕ
hn : n ≠ 0
h : 1 ^ k * l = n
hl : ¬1 ∣ l
⊢ maxPowDvdDiv 1 n = (k, l)

pp: case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
· cases k.eq_zero_or_pos <;> simp_all

Goal state after:
case inr.inl
n k l : ℕ
hn : n ≠ 0
h : 1 ^ k * l = n
hl : ¬1 ∣ l
⊢ maxPowDvdDiv 1 n = (k, l)

case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ p.maxPowDvdDiv n = (k, l)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
Nat.mul_left_cancel_iff

Goal state after:
case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : l = n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)

case inr.inr.p
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ 0 < p ^ (p.maxPowDvdDiv n).fst
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
b k : ℕ
hb : 1 < b
n : ℕ
h : ¬n = 0
⊢ log b n + 1 ≤ k ↔ log b n < k

Tactic:
exact add_one_le_iff

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

Goal state before:
pp: case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ n + 1

Tactic:
← ofDigits_digits p.succ (n + 1)

Goal state after:
case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ ofDigits p.succ (p.succ.digits (n + 1))
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
| n ≡ ofDigits 1 (b'.digits n) [MOD b]

Tactic:
congr
    · skip
    · rw [← ofDigits_digits b' n]

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

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

Tactic:
congr
    · skip
    · rw [← ofDigits_digits b' n]

Goal state after:
case b
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
| ofDigits c (b'.digits n)
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:
by rw [_root_.pow_succ']; exact hp.finiteMultiplicity_mul ha (ha.pow hp)

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

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization ↔ ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
refine ⟨fun h ↦ ⟨_, h, prod_factorization_pow_eq_self hd |>.symm⟩, fun ⟨f, hle, hprod⟩ ↦ ?_⟩

Goal state after:
n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
hprod : d = f.prod fun x1 x2 ↦ x1 ^ x2
⊢ d.factorization ≤ n.factorization
Module: Mathlib.Algebra.CharP.Lemmas

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

Tactic:
by
    rw [h.add_pow, ← Nat.Ico_zero_eq_range, Ico_add_one_right_eq_Icc]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1

Tactic:
orderOf_eq_zero h,

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ 0 = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
⊢ Submonoid.closure (s ∪ s⁻¹) ≤ Submonoid.closure s

Tactic:
refine Submonoid.closure_le.mpr <| Set.union_subset Submonoid.subset_closure
    fun x (hx : x⁻¹ ∈ s) ↦ ?_

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
x : G
hx : x⁻¹ ∈ s
⊢ x ∈ ↑(Submonoid.closure s)
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
rw [← add_right_inj (a.gcd b).factorization, ←
    factorization_mul (mt gcd_eq_zero_iff.1 fun h => ha h.1) (lcm_ne_zero ha hb), gcd_mul_lcm,
    factorization_gcd ha hb, factorization_mul ha hb]

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorization + b.factorization = a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case h
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ n.factorization.support ⊆ {p ∈ Finset.range m | Prime p}

Tactic:
exact fun p hp => Finset.mem_filter.mpr ⟨Finset.mem_range.2 <| pr.trans_le' <|
      le_of_mem_primeFactors hp, prime_of_mem_primeFactors hp⟩

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

Goal state before:
pp: case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ d, g' = g + d
⊢ (single g 1 * x %ᵒᶠ g).coeff g' = 0

Tactic:
rw [coeff_modOf_of_not_exists_add _ _ _ h, coeff_single_mul_of_forall_add_ne]
    simpa [eq_comm] using h

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

Goal state before:
pp: case succ
p n : ℕ
hn : #({e ∈ Finset.range n | p ∣ e + 1}) = n / p
⊢ #({e ∈ Finset.range (n + 1) | p ∣ e + 1}) = (n + 1) / p

Tactic:
simp [Nat.succ_div, add_ite, add_zero, Finset.range_add_one, filter_insert, apply_ite card,
      card_insert_of_notMem, hn]

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

Goal state before:
pp: case neg
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : ¬m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
use 0
      simp_all

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

Goal state before:
pp: case refine_3
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)
⊢ ∀ (n : ℕ) (a : R),
    (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n) → (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))

Tactic:
· intro n a _
    by_cases a0 : a = 0
    · exact Or.inl (by rw [a0, C_0, zero_mul, natDegree_zero])
    · refine Or.inr ?_
      rw [C_mul_X_pow_eq_monomial]
      exact h_monomial a0 n.succ_ne_zero

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

Goal state before:
pp: 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)
⊢ M f

Tactic:
by
  suffices f.natDegree = 0 ∨ M f from Or.recOn this (fun h => (f0 h).elim) id
  refine Polynomial.induction_on f ?_ ?_ ?_
  · exact fun a => Or.inl (natDegree_C _)
  · rintro p q (hp | hp) (hq | hq)
    · refine Or.inl ?_
      rw [eq_C_of_natDegree_eq_zero hp, eq_C_of_natDegree_eq_zero hq, ← C_add, natDegree_C]
    · refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hp]
      exact h_C_add hq
    · refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hq, add_comm]
      exact h_C_add hp
    · exact Or.inr (h_add hp hq)
  · intro n a _
    by_cases a0 : a = 0
    · exact Or.inl (by rw [a0, C_0, zero_mul, natDegree_zero])
    · refine Or.inr ?_
      rw [C_mul_X_pow_eq_monomial]
      exact h_monomial a0 n.succ_ne_zero

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
⊢ rootMultiplicity x (X - C y) = if x = y then 1 else 0

Tactic:
split_ifs with hxy

Goal state after:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
hxy : x = y
⊢ rootMultiplicity x (X - C y) = 1

case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq R
x y : R
hxy : ¬x = y
⊢ rootMultiplicity x (X - C y) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : p %ₘ q = 0
⊢ 0 < q.natDegree

Tactic:
Nat.pos_iff_ne_zero

Goal state after:
case pos
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : p %ₘ q = 0
⊢ q.natDegree ≠ 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f = 0
⊢ f /ₘ g = 0

Tactic:
rw [hf, zero_divByMonic]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
rw [degree_eq_natDegree hf, degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hfg,
    ← Nat.cast_add, Nat.cast_inj] at this

Goal state after:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.natDegree + (f /ₘ g).natDegree = f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit ((expand R p) f)
hf2 : (expand R p) f = C (if p ∣ 0 then f.coeff (0 / p) else 0)
⊢ IsUnit f

Tactic:
if_pos (dvd_zero _),

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit ((expand R p) f)
hf2 : (expand R p) f = C (f.coeff (0 / p))
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ p - q * (p /ₘ q) = q * (r - p /ₘ q)

Tactic:
mul_sub,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ p - q * (p /ₘ q) = q * r - q * (p /ₘ q)