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

Goal state before:
pp: case pos
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf✝ : f✝ ∈ Ideal.map C I
f : MvPolynomial σ R
hf : f ∈ ⇑C '' ↑I
n : σ →₀ ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : n = 0
⊢ (if 0 = n then x else 0) ∈ I

pp: case neg
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf✝ : f✝ ∈ Ideal.map C I
f : MvPolynomial σ R
hf : f ∈ ⇑C '' ↑I
n : σ →₀ ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : ¬n = 0
⊢ (if 0 = n then x else 0) ∈ I

Tactic:
· simpa [h] using hx.left

Goal state after:
case neg
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf✝ : f✝ ∈ Ideal.map C I
f : MvPolynomial σ R
hf : f ∈ ⇑C '' ↑I
n : σ →₀ ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : ¬n = 0
⊢ (if 0 = n then x else 0) ∈ I
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
⊢ a ≡ b [ZMOD n]

Tactic:
add_comm a,

Goal state after:
n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : c + a ≡ b + d [ZMOD n]
⊢ a ≡ b [ZMOD n]
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case prime.prime
R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
hp : Nat.Prime p
hchar✝¹ : CharP R p
hprime✝ : Nat.Prime p
hchar✝ : CharP S p
⊢ ExpChar (R × S) p

Tactic:
have := Prod.charP R S p

Goal state after:
case prime.prime
R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
hp : Nat.Prime p
hchar✝¹ : CharP R p
hprime✝ : Nat.Prime p
hchar✝ : CharP S p
this : CharP (R × S) p
⊢ ExpChar (R × S) p
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)
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
he : e ∈ ⨅ j ∈ {i}ᶜ, I j
hue : u + e = 1
⊢ ∃ e, (Quotient.mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) e = 0

Tactic:
replace he : ∀ j, j ≠ i → e ∈ I j := by simpa using he

Goal state after:
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
⊢ ∃ e, (Quotient.mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) e = 0
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:
rw [add_assoc, add_self_eq_zero, add_zero]

Goal state after:
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)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
this : p ^ k * p ∣ m ∨ p ^ l * p ∣ n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n

Tactic:
by rwa [_root_.pow_succ, _root_.pow_succ]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
h : I ≤ J
⊢ comap (Quotient.mk I) (map (Quotient.mk I) J) = J

Tactic:
by
  simpa

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

Goal state before:
pp: case a
α : 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:
apply IsPeriodicPt.minimalPeriod_dvd

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

Goal state before:
pp: case a
α : 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:
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 _

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

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

Tactic:
apply IsPeriodicPt.minimalPeriod_dvd

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ IsPeriodicPt f (n * minimalPeriod f^[n] x) x
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.succ.nil
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hl : [].Nodup
h✝ : [y].getLast ⋯ ∈ []
h : [y].getLast ⋯ ∈ [y]
hy : [y].getLast ⋯ ≠ y
H : [y].getLast ⋯ ∈ [y].dropLast
hk : k + 1 < [y].dropLast.length
hk' : [y].dropLast[k + 1] = [y].getLast ⋯
⊢ k + 1 = [].length

Tactic:
simp at hk

Goal state after:
Module: Mathlib.Data.Finite.Sigma

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
this : Fintype α := Fintype.ofFinite α
⊢ Finite ((a : α) × β a)

Tactic:
let := fun a => Fintype.ofFinite (β a)

Goal state after:
α : Type u_1
β : α → Type u_2
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
this✝ : Fintype α := Fintype.ofFinite α
this : (a : α) → Fintype (β a) := fun a ↦ Fintype.ofFinite (β a)
⊢ Finite ((a : α) × β a)
Module: Mathlib.GroupTheory.GroupAction.Quotient

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

Tactic:
by
  apply le_antisymm
  · intro g hg
    apply Equiv.Perm.ext
    refine fun q ↦ QuotientGroup.induction_on q ?_
    refine fun g' => (MulAction.Quotient.smul_mk H g g').trans (QuotientGroup.eq.mpr ?_)
    rw [smul_eq_mul, mul_inv_rev, ← inv_inv g', inv_inv]
    exact H.normalCore.inv_mem hg g'⁻¹
  · refine (Subgroup.normal_le_normalCore.mpr fun g hg => ?_)
    rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]
    exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))

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

Goal state before:
pp: case zero
n : ℕ
hk : 0 ≠ 0
⊢ (n ^ 0).primeFactors = n.primeFactors

Tactic:
simp at hk

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₁) = ↑(a ^ n₂)
⊢ a ^ (n₂ - n₁) ∈ H

Tactic:
QuotientGroup.eq,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : (a ^ n₁)⁻¹ * a ^ n₂ ∈ H
⊢ a ^ (n₂ - n₁) ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Tactic:
suffices ∃ n₁ n₂, n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧
      ((a ^ n₂ : G) : G ⧸ H) = ((a ^ n₁ : G) : G ⧸ H) by
    rcases this with ⟨n₁, n₂, hne, hle₁, hle₂, he⟩
    rcases hne.lt_or_gt with hlt | hlt
    · exact ⟨n₁, n₂, hlt, hle₂, he⟩
    · exact ⟨n₂, n₁, hlt, hle₁, he.symm⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
⊢ ∃ n₁ n₂, n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)
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]

Goal state after:
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ Fin.cast h (a * b) = Fin.cast h a * Fin.cast h b
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]

Goal state after:
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
a b : ZMod (m + 1)
⊢ Fin.cast h (a + b) = Fin.cast h a + Fin.cast h b
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = z.val + p * k) → ↑n = z

Tactic:
rintro ⟨k, rfl⟩
    rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul,
      add_zero]

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

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

Tactic:
dsimp [ZMod]

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
h : a.val = b.val
⊢ a = b
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ k_1 ≤ k, x = p ^ k_1) ∧ p ^ k ≠ 0 ↔ ∃ j ≤ k, x = p ^ j

Tactic:
and_iff_left (ne_of_gt (pow_pos pp.pos k))

Goal state after:
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ k_1 ≤ k, x = p ^ k_1) ↔ ∃ j ≤ k, x = p ^ j
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
inv_coe_unit,

Goal state after:
n : ℕ
u : (ZMod n)ˣ
⊢ ↑u * ↑u⁻¹ = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
⊢ a⁻¹ * b = 1 ↔ a = b

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H ▸ a.inv_mul_of_unit ha⟩

Goal state after:
n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
H : a⁻¹ * b = 1
⊢ a = b
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n.properDivisors = {1}
⊢ 1 ∈ n.properDivisors

Tactic:
simp [h]

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

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = ∑ i ∈ insert 0 (Ico (0 + 1) n.succ), a / b ^ i

Tactic:
sum_insert

Goal state after:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / b ^ 0 + ∑ x ∈ Ico (0 + 1) n.succ, a / b ^ x

b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ 0 ∉ Ico (0 + 1) n.succ
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x✝¹ : 1 < n + 2
x✝ : ZMod (n + 2)
⊢ x✝.val = 1 ↔ x✝ = 1

Tactic:
by simp only [val, ZMod, Fin.ext_iff, Fin.val_one]

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

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

Tactic:
rintro ⟨m, he⟩
    rcases m with - | m
    · rw [mul_zero, mul_eq_zero] at he
      rcases he with (⟨⟨⟩⟩ | he)
      exact Or.inl (a.val_eq_zero.1 he)
    cases m
    · right
      rwa [show 0 + 1 = 1 from rfl, mul_one] at he
    refine (a.val_lt.not_ge <| Nat.le_of_mul_le_mul_left ?_ zero_lt_two).elim
    rw [he, mul_comm]
    apply Nat.mul_le_mul_left
    simp

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

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

Tactic:
choose_mul_succ_eq

Goal state after:
n : ℕ
⊢ (2 * n + 2).choose n * (2 * n + 2 - n) = (2 * n + 1 + 1).choose n * (2 * n + 1 + 1 - n)
Module: Mathlib.Data.Nat.Choose.Central

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

Tactic:
choose_mul_succ_eq

Goal state after:
n : ℕ
⊢ 2 * ((2 * n + 1).choose n * (2 * n + 1 - n)) = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n))
Module: Mathlib.Data.Nat.Choose.Central

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

Tactic:
rw [choose_mul_succ_eq]

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

Goal state before:
pp: b : ℕ
h : 1 < b
x y : ℕ
hxb : x < b
hxy : x ≠ 0 ∨ y ≠ 0
⊢ b.digits (x + b * y) = x :: b.digits y

Tactic:
rcases Nat.exists_eq_add_of_le' h with ⟨b, rfl : _ = _ + 2⟩
  cases y
  · simp [hxb, hxy.resolve_right (absurd rfl)]
  dsimp [digits]
  rw [digitsAux_def]
  · congr
    · simp [Nat.add_mod, mod_eq_of_lt hxb]
    · simp [add_mul_div_left, div_eq_of_lt hxb]
  · apply Nat.succ_pos

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

Goal state before:
pp: case pos
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : n / b = 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1

Tactic:
simp [h]

Goal state after:
case pos
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : n / b = 0
⊢ n < b ∨ b ≤ 1
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp.left
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ↑n ≤ emultiplicity a b

Tactic:
simp [h]

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

Goal state before:
pp: a : ℕ
ha : a ∈ {x | x ≠ 0}
b : ℕ
hb : b ∈ {x | x ≠ 0}
h : a.factorization = b.factorization
p : ℕ
⊢ a.factorization p = b.factorization p

Tactic:
simp [h]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ ¬FiniteMultiplicity p a ∨ ¬FiniteMultiplicity p b

Tactic:
simpa only [FiniteMultiplicity.mul_iff hp, not_and_or] using hfin

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
rw [h0, lcm_zero_left]
    apply dvd_zero

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

Goal state before:
pp: case h
p k : ℕ
hp : Prime p
⊢ ∀ (p_1 : ℕ), (p ^ k / p ^ (p ^ k).factorization p).factorization p_1 = (factorization 1) p_1

Tactic:
· simp [Prime.factorization_pow hp]

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

Goal state before:
pp: case pos
p n k : ℕ
h : (n.choose k).factorization p = 0
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
simp [h]

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

Goal state before:
pp: p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ p * (k / p) + k % p + (p * ((n - k) / p) + (n - k) % p) < succ 2 * p

Tactic:
rwa [div_add_mod, div_add_mod, add_tsub_cancel_of_le hkn]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x y : G
h : orderOf x = orderOf y
n : ℕ
⊢ (finCongr h) ⟨n % orderOf x, ⋯⟩ = ⟨n % orderOf y, ⋯⟩

Tactic:
simp [h]

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

Goal state before:
pp: n p : ℕ
pp : Prime p
hn : n ≠ 0
x✝ : ℕ
⊢ x✝ ∈ {i | i ≠ 0 ∧ p ^ i ∣ n} ↔ x✝ ∈ Set.Icc 1 (n.factorization p)

Tactic:
simp [one_le_iff_ne_zero, pp.pow_dvd_iff_le_factorization hn]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : ¬IsOfFinOrder x
h : zpowers x = zpowers y
hx_mem : x ∈ zpowers y
⊢ y ∈ zpowers x

Tactic:
simp [h]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
x y : G
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ (finCongr h) ⟨n % orderOf x, ⋯⟩ = ⟨n % orderOf y, ⋯⟩

Tactic:
simp [h]

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.divX * X + C (p.coeff 0)).coeff 0 = p.coeff 0

Tactic:
simp [coeff_C, coeff_mul_X]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (p.divX * X + C (p.coeff 0)).coeff (n✝ + 1) = p.coeff (n✝ + 1)

Tactic:
simp [coeff_C, coeff_mul_X]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case succ
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
a : M
ha : a ∈ S
n : ℕ
ih : a ^ (n + 1) ∈ S
⊢ a ^ (n + 1 + 1) ∈ S

Tactic:
← hS2,

Goal state after:
case succ
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
a : M
ha : a ∈ S
n : ℕ
ih : a ^ (n + 1) ∈ S
⊢ a ^ (n + 1 + 1) ∈ S * S
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
⊢ p.divX.degree < p.degree

Tactic:
calc
    degree (divX p) < (divX p * X + C (p.coeff 0)).degree :=
      if h : degree p ≤ 0 then by
        have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
        rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]
        exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))
      else by
        have hXp0 : divX p ≠ 0 := by
          simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
        have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
        have : degree (C (p.coeff 0)) < degree (divX p * X) :=
          calc
            degree (C (p.coeff 0)) ≤ 0 := degree_C_le
            _ < 1 := by decide
            _ = degree (X : R[X]) := degree_X.symm
            _ ≤ degree (divX p * X) := by
              rw [← zero_add (degree X), degree_mul' this]
              exact add_le_add
                (by rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
                    exact fun h0 => h (h0.symm ▸ degree_C_le))
                    le_rfl
        rw [degree_add_eq_left_of_degree_lt this]; exact degree_lt_degree_mul_X hXp0
    _ = degree p := congr_arg _ (divX_mul_X_add _)

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

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

Tactic:
eq_C_of_natDegree_eq_zero hq,

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

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

Tactic:
eq_C_of_natDegree_eq_zero hq,

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 0
hg : g.degree = 1
⊢ IsUnit f

pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 1
hg : g.degree = 0
⊢ IsUnit f

Tactic:
swap

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 1
hg : g.degree = 0
⊢ IsUnit f

case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 0
hg : g.degree = 1
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ ⦃x : ℕ × ℕ⦄, (∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = x) → x.1 + x.2 = n * p

Tactic:
rintro _ ⟨x, rfl, rfl⟩

Goal state after:
case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
x : ℕ × ℕ
⊢ (x.1 * p, x.2 * p).1 + (x.1 * p, x.2 * p).2 = (x.1 + x.2) * p
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
h : Function.Injective ⇑(algebraMap A B)
⊢ (aeval ((algebraMap A B) x)) p = 0 ↔ (aeval x) p = 0

Tactic:
rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
        ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ i ∈ range n.succ, (n + 1).choose (i + 1) • ((⇑derivative)^[n + 1 - (i + 1)] p * (⇑derivative)^[i + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)

Tactic:
by
        simp_rw [Nat.choose_succ_succ, Nat.succ_sub_succ, add_smul, sum_add_distrib]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ i ∈ range n.succ, (n + 1).choose (i + 1) • ((⇑derivative)^[n + 1 - (i + 1)] p * (⇑derivative)^[i + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ k ∈ range n.succ, n.succ.choose (k + 1) • ((⇑derivative)^[n.succ - (k + 1)] p * (⇑derivative)^[k + 1] q) +
      1 • ((⇑derivative)^[n.succ - 0] p * (⇑derivative)^[0] q)

Tactic:
tsub_zero

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ i ∈ range n.succ, (n + 1).choose (i + 1) • ((⇑derivative)^[n + 1 - (i + 1)] p * (⇑derivative)^[i + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ k ∈ range n.succ, n.succ.choose (k + 1) • ((⇑derivative)^[n.succ - (k + 1)] p * (⇑derivative)^[k + 1] q) +
      1 • ((⇑derivative)^[n.succ] p * (⇑derivative)^[0] q)