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

Goal state before:
pp: case refine_2.mem.inl
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝ x : ↥N
hx : x = n
⊢ f x ∈ M'

Tactic:
rw [hx, hn]; exact zero_mem _

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

Goal state before:
pp: case mpr
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
⊢ ∀ m ∈ f.support, (monomial m) (coeff m f) ∈ Ideal.map C I

Tactic:
intro m _

Goal state after:
case mpr
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
m : σ →₀ ℕ
a✝ : m ∈ f.support
⊢ (monomial m) (coeff m f) ∈ Ideal.map C I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
σ : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ RingHom.ker (map f) = Ideal.map C (RingHom.ker f)

Tactic:
ext
  rw [MvPolynomial.mem_map_C_iff, RingHom.mem_ker, MvPolynomial.ext_iff]
  simp_rw [coeff_map, coeff_zero, RingHom.mem_ker]

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

Goal state before:
pp: a b : ℕ
⊢ Prime (a * b) ↔ Prime a ∧ b = 1 ∨ Prime b ∧ a = 1

Tactic:
simp only [irreducible_mul_iff, ← irreducible_iff_nat_prime, Nat.isUnit_iff]

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

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ A ∙ (mk I) 1 = A ∙ (Submodule.mkQ I) 1

Tactic:
Submodule.mkQ_apply,

Goal state after:
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ A ∙ (mk I) 1 = A ∙ Submodule.Quotient.mk 1
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✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S T : StarSubalgebra R A
h : S.toSubalgebra = T.toSubalgebra
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toSubalgebra, ← mem_toSubalgebra, h]

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

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
i : ℤ
g : G
a : α
⊢ g ^ (↑(period g a) + i) • a = g ^ i • a

Tactic:
rw [← zpow_mod_period_smul, Int.add_emod_left, zpow_mod_period_smul]

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

Goal state before:
pp: α : Type u_1
s : List α
hs : s.Nodup
⊢ s.permutations.Nodup

Tactic:
rw [(permutations_perm_permutations' s).nodup_iff]

Goal state after:
α : Type u_1
s : List α
hs : s.Nodup
⊢ s.permutations'.Nodup
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case h
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ Duplicate (x :: x :: l) ([x, x] ++ l).permutations

Tactic:
List.duplicate_iff_sublist,

Goal state after:
case h
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ [x :: x :: l, x :: x :: l] <+ ([x, x] ++ l).permutations
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s

Tactic:
by
  constructor
  · intro hyp g hg
    apply Eq.subset
    rw [← mem_stabilizer_iff]
    exact hyp hg
  · intro hyp g hg
    rw [mem_stabilizer_iff]
    apply subset_antisymm (hyp g hg)
    intro x hx
    use g⁻¹ • x
    constructor
    · apply hyp g⁻¹ (inv_mem hg)
      simp only [Set.smul_mem_smul_set_iff, hx]
    · simp only [smul_inv_smul]

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

Goal state before:
pp: case cons.inr.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hb : b ∈ l
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r b c

pp: case cons.inr.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b ∈ l
hc : c ∈ l
⊢ r b c

Tactic:
· exact hs.2.2 b hb

Goal state after:
case cons.inr.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b ∈ l
hc : c ∈ l
⊢ r b c
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ (Quotient.out q)⁻¹ * (g ^ minimalPeriod (fun x ↦ g • x) q * Quotient.out q) ∈ H

Tactic:
← QuotientGroup.eq,

Goal state after:
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ ↑(Quotient.out q) = ↑(g ^ minimalPeriod (fun x ↦ g • x) q * Quotient.out q)
Module: Mathlib.GroupTheory.GroupAction.Quotient

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

Tactic:
← QuotientGroup.eq,

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

Goal state before:
pp: case inr.zero
b : ℕ
hb : b > 0
ha : 0 ≠ 0
h : primeFactorsList 0 <+~ b.primeFactorsList
⊢ 0 ∣ b

Tactic:
exact (ha rfl).elim

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
⊢ comap f H = comap f.rangeRestrict (H.subgroupOf f.range)

Tactic:
by rfl

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

Goal state before:
pp: a b : ℕ
hab : a = b
⊢ (ringEquivCongr hab).symm = ringEquivCongr ⋯

Tactic:
subst hab

Goal state after:
a : ℕ
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = a % ↑(n✝ + 1)

Tactic:
rw [← val_intCast, val]

Goal state after:
case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = ↑↑↑a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x + y).cast = (x.cast + y.cast) % ↑n

Tactic:
← ZMod.coe_intCast,

Goal state after:
n : ℕ
x y : ZMod n
⊢ (x + y).cast = (↑(x.cast + y.cast)).cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x * y).cast = x.cast * y.cast % ↑n

Tactic:
← ZMod.coe_intCast,

Goal state after:
n : ℕ
x y : ZMod n
⊢ (x * y).cast = (↑(x.cast * y.cast)).cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x y : ZMod n
⊢ (x - y).cast = (x.cast - y.cast) % ↑n

Tactic:
← ZMod.coe_intCast,

Goal state after:
n : ℕ
x y : ZMod n
⊢ (x - y).cast = (↑(x.cast - y.cast)).cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x : ZMod n
⊢ (-x).cast = -x.cast % ↑n

Tactic:
← ZMod.coe_intCast,

Goal state after:
n : ℕ
x : ZMod n
⊢ (-x).cast = (↑(-x.cast)).cast
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ #(Ico 1 (n + 1)) = n

Tactic:
by rw [card_Ico, add_tsub_cancel_right]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
n : ℕ
h : n = 0 ∧ n ≠ 0
⊢ 0 < 0

Tactic:
cases h.2 h.1

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisors.sup id = n

Tactic:
refine le_antisymm (Finset.sup_le fun _ ↦ divisor_le) ?_
  rcases Decidable.eq_or_ne n 0 with rfl | hn
  · apply zero_le
  · exact Finset.le_sup (f := id) <| mem_divisors_self n hn

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

Goal state before:
pp: case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i

Tactic:
· exact geom_sum_pos hx' (by simp)

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

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : 0 + 1 ≠ 0
⊢ ∑ i ∈ range (0 + 1), x ^ i ≠ 0

pp: case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
· simp only [zero_add, range_one, sum_singleton, pow_zero, ne_eq, one_ne_zero, not_false_eq_true]

Goal state after:
case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
⊢ n.divisorsAntidiagonal = {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}

Tactic:
ext ⟨n1, n2⟩

Goal state after:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ (n1, n2) ∈ n.divisorsAntidiagonal ↔ (n1, n2) ∈ {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
x y z✝ z : ℤ
s : Finset ℕ := z.natAbs.divisors
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp +contextual [s, disjoint_left, Eq.comm, forall_comm (β := _ = _)]

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

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

Tactic:
exact Or.inl (a.val_eq_zero.1 he)

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
b : α
L : List ℕ
⊢ ofDigits b L = List.foldr (fun x y ↦ ↑x + b * y) 0 L

Tactic:
induction L with
  | nil => rfl
  | cons d L ih => dsimp [ofDigits]; rw [ih]

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

Goal state before:
pp: b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q

Tactic:
by_cases hm : m = 0
  · simp [hm]
  simp only [digits_eq_cons_digits_div h hm]
  rw [List.getLast_cons]

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

Goal state before:
pp: p k n a b : ℕ
hp : 1 < p
hn : n ≠ 0
hab : p ^ a * b = n
hb : ¬p ∣ b
⊢ p ^ k ∣ n ↔ k ≤ a

Tactic:
subst hab

Goal state after:
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
⊢ p ^ k ∣ p ^ a * b ↔ k ≤ a
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
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
this : n / b < n
⊢ log b (n / b) + 1 + 1 = log b n + 1

Tactic:
log_div_base,

Goal state after:
case neg
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
this : n / b < n
⊢ log b n - 1 + 1 + 1 = log b n + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b hd : ℕ
tl : List ℕ
IH : (∀ x ∈ tl, x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
⊢ b + 2 ≤ b + 2

Tactic:
by rfl

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

Goal state before:
pp: case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = ofDigits b (b.digits (n + 1)) % b

Tactic:
rw [Nat.ofDigits_mod_eq_head! _ _]

Goal state after:
case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (b.digits (n + 1)).head! % b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ (b.digits n ++ replicate (l - (b.digits n).length) 0).length = l

Tactic:
length_append,

Goal state after:
n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ (b.digits n).length + (replicate (l - (b.digits n).length) 0).length = l
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case inl
p : ℕ
⊢ count p (primeFactorsList 0) = (factorization 0) p

pp: case inr
n p : ℕ
hn0 : n > 0
⊢ count p n.primeFactorsList = n.factorization p

Tactic:
· simp [factorization, count]

Goal state after:
case inr
n p : ℕ
hn0 : n > 0
⊢ count p n.primeFactorsList = n.factorization p
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ ¬p ^ (multiplicity p b + 1) ∣ a + b

Tactic:
rw [dvd_add_right]
    · apply this.not_pow_dvd_of_multiplicity_lt
      simp
    apply pow_dvd_of_le_emultiplicity
    exact Order.add_one_le_of_lt h

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

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ (n + 1)!.factorization p = (n + 1).factorization p + n !.factorization p

Tactic:
factorial_succ,

Goal state after:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ((n + 1) * n !).factorization p = (n + 1).factorization p + n !.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ n = 0 ∨ ¬p ∣ n

Tactic:
right
      rw [← h]
      exact not_dvd_ordCompl hp n_zero

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

Goal state before:
pp: case succ
p n✝ n : ℕ
hn : n < p → n !.factorization p = 0
h : n + 1 < p
⊢ (n + 1)!.factorization p = 0

Tactic:
factorial_succ,

Goal state after:
case succ
p n✝ n : ℕ
hn : n < p → n !.factorization p = 0
h : n + 1 < p
⊢ ((n + 1) * n !).factorization p = 0
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ emultiplicity p (n + 1)! = emultiplicity p n ! + emultiplicity p (n + 1)

Tactic:
factorial_succ,

Goal state after:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ emultiplicity p ((n + 1) * n !) = emultiplicity p n ! + emultiplicity p (n + 1)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
⊢ (Injective fun n ↦ x ^ n) ↔ ¬IsOfFinOrder x

Tactic:
refine ⟨fun h => not_isOfFinOrder_of_injective_pow h, fun h n m hnm => ?_⟩
  rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, Nat.modEq_zero_iff] at hnm

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ ∑ m ∈ n.divisors, #{x | orderOf x = m} = #{x | x ^ n = 1}

Tactic:
by
  refine (Finset.card_biUnion ?_).symm.trans ?_
  · simp +contextual [Set.PairwiseDisjoint, Set.Pairwise, disjoint_iff, Finset.ext_iff]
  · congr; ext; simp [hn, orderOf_dvd_iff_pow_eq_one]

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

Goal state before:
pp: n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
h1 : p ^ x ∣ n
⊢ x < n ↔ x ≤ b

Tactic:
exact iff_of_true (lt_of_pow_dvd_right hn pp.two_le h1) <|
    (Nat.pow_le_pow_iff_right pp.one_lt).1 <| (le_of_dvd hn.bot_lt h1).trans hb

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

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
ha : a = c ^ n
⊢ b = c ^ m

Tactic:
apply Nat.pow_left_injective hn0

Goal state after:
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := ⋯
c : ℕ := ⋯
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
ha : a = c ^ n
⊢ (fun a ↦ a ^ n) b = (fun a ↦ a ^ n) (c ^ m)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
p : ℕ
foo : ∀ p ∈ factors.support, Prime p
⊢ a.factorization p = (n • factors) p

Tactic:
suffices n ∣ a.factorization p by
    simp [factors, Nat.mul_div_cancel' this]

Goal state after:
case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
p : ℕ
foo : ∀ p ∈ factors.support, Prime p
⊢ n ∣ a.factorization p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
⊢ False

Tactic:
have hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0 := by
      simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_mul, Ne,
          hr0, not_false_eq_true]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
p0 : p.natDegree = 0
⊢ (derivative p).natDegree ≤ p.natDegree - 1

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
p0 : ¬p.natDegree = 0
⊢ (derivative p).natDegree ≤ p.natDegree - 1

Tactic:
· simp [p0, derivative_of_natDegree_zero]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
p0 : ¬p.natDegree = 0
⊢ (derivative p).natDegree ≤ p.natDegree - 1
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ Irreducible (C a * X + C b)

Tactic:
apply irreducible_of_degree_eq_one_of_isRelPrime_coeff
  · compute_degree!
  · simpa using hab.symm

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
rootMultiplicity_eq_multiplicity (p * q),

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (if p * q = 0 then 0 else multiplicity (X - C x) (p * q)) = rootMultiplicity x p + rootMultiplicity x q
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p) a) = a ^ p
hb : map (frobenius R p) ((expand R p) b) = b ^ p
⊢ map (frobenius R p) ((expand R p) a + (expand R p) b) = (a + b) ^ p

Tactic:
Polynomial.map_add,

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p) a) = a ^ p
hb : map (frobenius R p) ((expand R p) b) = b ^ p
⊢ map (frobenius R p) ((expand R p) a) + map (frobenius R p) ((expand R p) b) = (a + b) ^ p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ ⊥ < p.degree

Tactic:
bot_lt_iff_ne_bot,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ p.degree ≠ ⊥
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ ¬IsAlgebraic R x ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 0

Tactic:
IsAlgebraic,

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ (¬∃ p, p ≠ 0 ∧ (aeval x) p = 0) ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
⊢ q.coeff n = (p %ₘ (X - C a) + (X - C a) * (p /ₘ (X - C a))).coeff (n + 1) + a * q.coeff (n + 1)

Tactic:
have : degree (p %ₘ (X - C a)) < ↑(n + 1) := degree_X_sub_C a ▸ p.degree_modByMonic_lt this
    |>.trans_le <| WithBot.coe_le_coe.mpr le_add_self

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this✝ : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
this : (p %ₘ (X - C a)).degree < ↑(n + 1)
⊢ q.coeff n = (p %ₘ (X - C a) + (X - C a) * (p /ₘ (X - C a))).coeff (n + 1) + a * q.coeff (n + 1)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
p : R[X]
this : X - C b ∣ p - C (eval b p)
⊢ a - b ∣ eval a p - eval b p

Tactic:
by
    simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C]
      using (_root_.map_dvd (evalRingHom a)) this

Goal state after:
Module: Mathlib.Order.Filter.Ker

Goal state before:
pp: ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ (⨆ i, f i).ker = ⋃ i, (f i).ker

Tactic:
refine subset_antisymm (fun x hx ↦ ?_) ker_mono.le_map_iSup
  simp only [mem_iUnion, mem_ker] at hx ⊢
  contrapose! hx
  choose s hsf hxs using hx
  refine ⟨⋃ i, s i, ?_, by simpa⟩
  exact mem_iSup.2 fun i ↦ mem_of_superset (hsf i) (subset_iUnion s i)

Goal state after:
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ Disjoint cofinite l ↔ ∃ s ∈ l, s.Finite

Tactic:
by
  simp [l.basis_sets.disjoint_iff_right]

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ⊔ ∂ a = a

Tactic:
rw [boundary, sup_inf_left, hnot_sup_self, inf_top_eq, sup_eq_right]

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ≤ a
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
s t : Set α
ht : t.Finite
⊢ cofinite ⊓ 𝓟 (s ∩ tᶜ) = cofinite ⊓ 𝓟 s

Tactic:
← inf_principal,

Goal state after:
α : Type u_2
s t : Set α
ht : t.Finite
⊢ cofinite ⊓ (𝓟 s ⊓ 𝓟 tᶜ) = cofinite ⊓ 𝓟 s
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
c : R
m : ℕ
⊢ derivative ((X - C c) ^ m) = C ↑m * (X - C c) ^ (m - 1)

Tactic:
rw [derivative_pow, derivative_X_sub_C, mul_one]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
y : α
hy : y ∈ Classical.choose ⋯
hx : normalize y ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯)
⊢ Prime (normalize y)

Tactic:
rw [(normalize_associated _).prime_iff]

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
y : α
hy : y ∈ Classical.choose ⋯
hx : normalize y ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯)
⊢ Prime y
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X.roots = {0}

Tactic:
rw [← roots_X_sub_C, C_0, sub_zero]

Goal state after: