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 → ∃ s f, Surjective ⇑f

Tactic:
rintro ⟨s, hs⟩
    use s, MvPolynomial.aeval (↑)
    intro x
    rw [← Set.mem_range, ← AlgHom.coe_range, ← adjoin_eq_range, SetLike.mem_coe, hs]
    apply mem_top

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

Goal state before:
pp: case refine_3
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝² : A
hx✝ : x✝² ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
x✝¹ : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
x✝ : y ∈ Algebra.adjoin R (↑S ∪ ↑T)
hx : x ∈ toSubmodule S * toSubmodule T
hy : y ∈ toSubmodule S * toSubmodule T
⊢ x * y ∈ toSubmodule S * toSubmodule T

Tactic:
have := Submodule.mul_mem_mul hx hy

Goal state after:
case refine_3
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝² : A
hx✝ : x✝² ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
x✝¹ : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
x✝ : y ∈ Algebra.adjoin R (↑S ∪ ↑T)
hx : x ∈ toSubmodule S * toSubmodule T
hy : y ∈ toSubmodule S * toSubmodule T
this : x * y ∈ toSubmodule S * toSubmodule T * (toSubmodule S * toSubmodule T)
⊢ x * y ∈ toSubmodule S * toSubmodule T
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
⊢ x ∈ comap (Quotient.mk I) (map (Quotient.mk I) J) ↔ x ∈ J ⊔ I

Tactic:
comap_map_of_surjective (Quotient.mk I) Quotient.mk_surjective,

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

Goal state before:
pp: case h
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
e : ι → R
he : ∀ (i : ι), (Quotient.mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) (e i) = 0
i : ι
⊢ (Quotient.mk (I i)) (f i * e i) = g i

pp: case h
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
e : ι → R
he : ∀ (i : ι), (Quotient.mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) (e i) = 0
i : ι
⊢ ∀ (x : ι), x ≠ i → (Quotient.mk (I i)) (f x * e x) = 0

Tactic:
· simp [(he i).1, hf]

Goal state after:
case h
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
e : ι → R
he : ∀ (i : ι), (Quotient.mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) (e i) = 0
i : ι
⊢ ∀ (x : ι), x ≠ i → (Quotient.mk (I i)) (f x * e x) = 0
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ (↑(List.map (fun n ↦ f^[n] x) (List.range (minimalPeriod f x)))).Nodup

Tactic:
Cycle.nodup_coe_iff,

Goal state after:
α : Type u_1
f : α → α
x : α
⊢ (List.map (fun n ↦ f^[n] x) (List.range (minimalPeriod f x))).Nodup
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h : xs.nextOr x d ≠ d
⊢ x ∈ xs

Tactic:
induction xs with
  | nil => simp at h
  | cons y ys IH => ?_

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x d y : α
ys : List α
IH : ys.nextOr x d ≠ d → x ∈ ys
h : (y :: ys).nextOr x d ≠ d
⊢ x ∈ y :: ys
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ stabilizer G (g • a) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)

Tactic:
ext h

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : G
⊢ h ∈ stabilizer G (g • a) ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)
Module: Mathlib.Data.Nat.Prime.Pow

Goal state before:
pp: case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ (n ^ k).minFac = n.minFac

Tactic:
apply (minFac_le_of_dvd (minFac_prime hn).two_le ((minFac_dvd n).pow hk)).antisymm

Goal state after:
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ n.minFac ≤ (n ^ k).minFac
Module: Mathlib.Data.List.Cycle

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

Tactic:
Nat.add_comm,

Goal state after:
case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (a :: c :: s).rotate (1 + d) = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])
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)

Tactic:
QuotientGroup.out_eq',

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

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
inst✝³ : MulAction G X
b : X
inst✝² : Fintype G
inst✝¹ : Fintype ↑(orbit G b)
inst✝ : Fintype ↥(stabilizer G b)
⊢ Fintype.card (↑(orbit G b) × ↥(stabilizer G b)) = Fintype.card G

Tactic:
Fintype.card_congr (orbitProdStabilizerEquivGroup G b)

Goal state after:
G : Type u
X : Type v
inst✝⁴ : Group G
inst✝³ : MulAction G X
b : X
inst✝² : Fintype G
inst✝¹ : Fintype ↑(orbit G b)
inst✝ : Fintype ↥(stabilizer G b)
⊢ Fintype.card G = Fintype.card G
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index = 2 ↔ ∃ a, ∀ (b : G), Xor (b * a ∈ H) (b ∈ H)

Tactic:
simp only [index, Nat.card_eq_two_iff' ((1 : G) : G ⧸ H), ExistsUnique, inv_mem_iff,
    QuotientGroup.exists_mk, QuotientGroup.forall_mk, Ne, QuotientGroup.eq, mul_one,
    xor_iff_iff_not]
  refine exists_congr fun a =>
    ⟨fun ha b => ⟨fun hba hb => ?_, fun hb => ?_⟩, fun ha => ⟨?_, fun b hb => ?_⟩⟩
  · exact ha.1 ((mul_mem_cancel_left hb).1 hba)
  · exact inv_inv b ▸ ha.2 _ (mt (inv_mem_iff (x := b)).1 hb)
  · rw [← inv_mem_iff (x := a), ← ha, inv_mul_cancel]
    exact one_mem _
  · rwa [ha, inv_mem_iff (x := b)]

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'
K : Subgroup G
f : G →* G'
⊢ f.ker.relIndex K = Nat.card ↥(map f K)

Tactic:
by
  rw [← MonoidHom.comap_bot, relIndex_comap, relIndex_bot_left]

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'
f : G →* G'
hf : Surjective ⇑f
⊢ Nat.card (G ⧸ f.ker) ∣ Nat.card G

Tactic:
exact Dvd.intro_left (Nat.card f.ker) f.ker.card_mul_index

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod n
⊢ a.cast.1 = a.cast

Tactic:
by
  cases n
  · rfl
  · simp [ZMod.cast]

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod n
⊢ a.cast.2 = a.cast

Tactic:
by
  cases n
  · rfl
  · simp [ZMod.cast]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑↑a + ↑↑b = ↑↑(a + b)

Tactic:
rw [← Nat.cast_add, Fin.val_add, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _),
    @CharP.cast_eq_zero_iff R _ m]

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ m ∣ ↑a + ↑b - (↑a + ↑b) % (n✝ + 1)
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1

Tactic:
refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < ∑ i ∈ range 2, x ^ i ∧ ∑ i ∈ range 2, x ^ i < 1

case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ ∀ (n : ℕ),
    2 ≤ n →
      0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1 →
        0 < ∑ i ∈ range (n + 1), x ^ i ∧ ∑ i ∈ range (n + 1), x ^ i < 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
a : ℕ × ℕ
⊢ a ∈ n.divisorsAntidiagonalList ↔ a.1 * a.2 = n ∧ n ≠ 0

Tactic:
by
  rw [← List.mem_toFinset, toFinset_divisorsAntidiagonalList, mem_divisorsAntidiagonal]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i

Tactic:
refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ if Even 2 then ∑ i ∈ range 2, x ^ i < 0 else 1 < ∑ i ∈ range 2, x ^ i

case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ ∀ (n : ℕ),
    2 ≤ n →
      (if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i) →
        if Even (n + 1) then ∑ i ∈ range (n + 1), x ^ i < 0 else 1 < ∑ i ∈ range (n + 1), x ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors, x → s = (n✝ + 1).properDivisors

Tactic:
rw [← sum_sdiff hsub]

Goal state after:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x → s = (n✝ + 1).properDivisors
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
simp [divisorsAntidiag]
    grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
simp [divisorsAntidiag]
    grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
simp [divisorsAntidiag]
    grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
simp [divisorsAntidiag]
    grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
simp [divisorsAntidiag]
    grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
simp [divisorsAntidiag]
    grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
simp [divisorsAntidiag]
    grind

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

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

pp: case inr
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a.val ^ m < n

Tactic:
· by_cases hm : m = 0
        · cases hm; simp [ilt.out]
        · simp only [val_zero, ne_eq, hm, not_false_eq_true, zero_pow, Nat.zero_lt_of_lt h]

Goal state after:
case inr
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a.val ^ m < n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits n ++ b.digits (b ^ k * m) = b.digits (n + b ^ ((b.digits n).length + k) * m)

Tactic:
simp only [digits_append_digits (zero_lt_of_lt hb), digits_inj_iff, add_right_inj]

Goal state after:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b ^ (b.digits n).length * (b ^ k * m) = b ^ ((b.digits n).length + k) * m
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
hk : ↑(n✝ + 1) ≤ if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
split at hk

Goal state after:
case succ.isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : FiniteMultiplicity a b
hk : ↑(n✝ + 1) ≤ ↑(Nat.find h✝)
⊢ a ^ (n✝ + 1) ∣ b

case succ.isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : ¬FiniteMultiplicity a b
hk : ↑(n✝ + 1) ≤ ⊤
⊢ a ^ (n✝ + 1) ∣ b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
inst✝ : IsMulTorsionFree G
a : G
ha : a ≠ 1
⊢ ¬IsOfFinOrder a

Tactic:
apply not_isOfFinOrder_of_isMulTorsionFree ha

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
⊢ False

Tactic:
have da : p ∣ a := by simpa [multiplicity_eq_zero] using nh.ne.symm

Goal state after:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
⊢ False
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n k p : ℕ
hp : Prime p
⊢ p ^ k * n / p ^ (p ^ k * n).factorization p = n / p ^ n.factorization p

Tactic:
by
  rw [ordCompl_mul, ordCompl_self_pow hp, one_mul]

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

Goal state before:
pp: case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ n ≤ ((p ^ n).choose k).factorization p + k.factorization p

Tactic:
· nth_rewrite 1 [← factorization_pow_self (n := n) hp]
    exact factorization_le_factorization_choose_add hkn hk0

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p m n : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p (m + n)) x = (iterateFrobenius R p m) ((iterateFrobenius R p n) x)

Tactic:
simp_rw [iterateFrobenius_def, add_comm m n, pow_add, pow_mul]

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

Goal state before:
pp: case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
⊢ p ^ padicValNat p n = 1

Tactic:
obtain ⟨hp1, hp2⟩ := Finset.mem_sdiff.mp hp

Goal state after:
case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
hp1 : p ∈ {p ∈ Finset.range m | Prime p}
hp2 : p ∉ n.factorization.support
⊢ p ^ padicValNat p n = 1
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
m : WithBot ℕ
p : R[X]
h_deg_le : p.degree ≤ m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0
hh : m ≠ ⊥
⊢ p.degree = m

Tactic:
obtain ⟨m, rfl⟩ := WithBot.ne_bot_iff_exists.mp hh

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p : R[X]
m : ℕ
h_deg_le : p.degree ≤ ↑m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 ↑m) ≠ 0
hh : ↑m ≠ ⊥
⊢ p.degree = ↑m
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.degree = ↑(p.natDegree - q.natDegree) + q.degree

Tactic:
degree_eq_natDegree h.2,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ ↑p.natDegree = ↑(p.natDegree - q.natDegree) + q.degree
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
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ ↑0 < ↑↑q.natDegree

Tactic:
simpa [degree_eq_natDegree hq.ne_zero] using! h0q

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ f q.leadingCoeff ≠ 0

Tactic:
rw [Monic.def.1 hq, f.map_one]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ 1 ≠ 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ Monic 1

Tactic:
by convert! monic_one (R := R)

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

Goal state before:
pp: case insert
α : Type u
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
a✝ : i ∉ s
hs : ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)
⊢ 𝓟 (f i) ⊓ 𝓟 (⋂ i ∈ s, f i) = 𝓟 (f i ∩ ⋂ x ∈ s, f x)

Tactic:
inf_principal

Goal state after:
case insert
α : Type u
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
a✝ : i ∉ s
hs : ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)
⊢ 𝓟 (f i ∩ ⋂ i ∈ s, f i) = 𝓟 (f i ∩ ⋂ x ∈ s, f x)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u

Tactic:
eq_C_of_natDegree_eq_zero h₁,

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * C (u.coeff 0)).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : u.coeff 0 = 1
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u

Tactic:
eq_C_of_natDegree_eq_zero h₁,

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : u.coeff 0 = 1
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * C (u.coeff 0)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s : Finset ι
f : ι → R[X]
⊢ derivative (∏ b ∈ s, f b) = ∑ a ∈ s, (∏ b ∈ s.erase a, f b) * derivative (f a)

Tactic:
simpa using! derivative_prod

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case inl
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ a
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

pp: case inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Tactic:
· have hap := hs a (Multiset.mem_cons.2 (Or.inl rfl))
      exact ⟨a, Multiset.mem_cons_self a _, hp.associated_of_dvd hap h⟩

Goal state after:
case inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_1.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ IsUnit k

Tactic:
exact .of_mul_eq_one_right _ hk

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inr.inl
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c✝ * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hc : x = c✝ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

pp: case cons.inr.inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c✝ * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hc : y = c✝ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
· rw [hc]; rw [hc, mul_assoc] at hprod
        refine Submonoid.mul_mem _ (subset_closure ?_)
          (hind _ _ ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod))
        · right; exact ha₂
        rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
        exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))

Goal state after:
case cons.inr.inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c✝ * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hc : y = c✝ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ ↑(if h : p = 0 then ∅ else Classical.choose ⋯).card ≤ p.degree

Tactic:
rw [dif_neg hp0]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ ↑(Classical.choose ⋯).card ≤ p.degree