mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

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

pp: 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

Tactic:
· exact Quotient.mk_surjective

Goal state after:
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.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts [] ys f).snd ++ r = (permutationsAux2 t ts r ys f).snd

Tactic:
by
  induction ys generalizing f <;> simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ (permutationsAux2 t ts [] ys f).snd.length = ys.length

Tactic:
by
  induction ys generalizing f <;> simp [*]

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

Goal state before:
pp: α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ flatMap (fun x ↦ [b' :: c :: x]) (permutations'Aux a' l) ++
      flatMap (fun a ↦ map (cons c) (permutations'Aux b' a)) (permutations'Aux a' l) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))

Tactic:
rw [← map_eq_flatMap, ← map_flatMap]

Goal state after:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ map (fun x ↦ b' :: c :: x) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l)) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
ts : List α
n : ℕ
h : ts.length < n
⊢ ts.permutations ~ ts.permutations'

Tactic:
induction n generalizing ts with

Goal state after:
case succ
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
⊢ ts.permutations ~ ts.permutations'
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : (ts ++ [t]).length < n + 1
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'

Tactic:
rw [← concat_eq_append, length_concat, Nat.succ_lt_succ_iff] at h

Goal state after:
case succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'
Module: Mathlib.Data.List.Prime

Goal state before:
pp: case mp.cons.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
x : M
hx1 : x ∈ L_tl
hx2 : p ∣ x
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
exact ⟨x, mem_cons_of_mem L_hd hx1, hx2⟩

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

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
y₁ y₂ : G ⧸ stabilizer G x
g₁ g₂ : G
H : g₁ • x = g₂ • x
⊢ (leftRel (stabilizer G x)) g₁ g₂

Tactic:
rw [leftRel_apply]
      change (g₁⁻¹ * g₂) • x = x
      rw [mul_smul, ← H, inv_smul_smul]

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

Goal state before:
pp: n p : ℕ
h : p ∈ n.primeFactorsList
⊢ p ≤ n

Tactic:
by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · rw [primeFactorsList_zero] at h
    cases h
  · exact le_of_dvd hn (dvd_of_mem_primeFactorsList h)

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

Goal state before:
pp: case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
case refine_1
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : l.prod = 0
⊢ False
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList

Tactic:
rw [mem_primeFactorsList (mul_ne_zero ha hb), mem_primeFactorsList ha, mem_primeFactorsList hb,
    ← and_or_left]

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
⊢ Bijective ⇑(castHom ⋯ R)

Tactic:
have : NeZero n :=
    ⟨by
      intro hn
      rw [hn] at h
      exact (Fintype.card_eq_zero_iff.mp h).elim' 0⟩

Goal state after:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Bijective ⇑(castHom ⋯ R)
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
rintro rfl

Goal state after:
case mp
p n : ℕ
inst✝ : NeZero p
⊢ ∃ k, n = (↑n).val + p * k
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
rintro rfl

Goal state after:
case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ ∃ k, n = ↑(↑n).val + ↑p * k
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case e_p
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := ↑f
⊢ f' g * f' y⁻¹ = f' x ↔ f' g = f' x * f' y

Tactic:
rw [← f'.coe_toHomUnits y⁻¹, map_inv, Units.mul_inv_eq_iff_eq_mul, f'.coe_toHomUnits]

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

Goal state before:
pp: n : ℕ
a b : ZMod n
h : a.val + b.val < n
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
a b : ZMod 0
h : a.val + b.val < 0
⊢ False
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + ↑n.succ * ↑(a.val.gcdB n.succ) = ↑(↑a.val * a.val.gcdA n.succ + ↑n.succ * a.val.gcdB n.succ)

Tactic:
push_cast

Goal state after:
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + (↑n + 1) * ↑(a.val.gcdB n.succ) = ↑a.val * ↑(a.val.gcdA n.succ) + (↑n + 1) * ↑(a.val.gcdB n.succ)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ Prime (n✝ + 1 + 1)

Tactic:
← properDivisors_eq_singleton_one_iff_prime

Goal state after:
case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ (n✝ + 1 + 1).properDivisors = {1}
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: 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}

Tactic:
rw [Nat.mem_divisorsAntidiagonal]

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

Goal state before:
pp: case mpr
n : ℕ
⊢ n = 1 → Subsingleton (ZMod n)

Tactic:
rintro rfl

Goal state after:
case mpr
⊢ Subsingleton (ZMod 1)
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 ^ (n + 1) = 4 * 4 ^ n

Tactic:
rw [pow_succ']

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

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ (n - 0) % n = 0

Tactic:
tsub_zero,

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ n % n = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Module (ZMod n) G
inst✝ : Nontrivial G
⊢ n ≠ 1

Tactic:
rintro rfl

Goal state after:
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Nontrivial G
inst✝ : Module (ZMod 1) G
⊢ False
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(d + b * ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L

Tactic:
push_cast

Goal state after:
case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑d + ↑b * ↑(ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b n : ℕ
⊢ ofDigits b (b.digits n) = n

Tactic:
by
  rcases b with - | b
  · rcases n with - | n
    · rfl
    · simp
  · rcases b with - | b
    · induction n with
      | zero => rfl
      | succ n ih =>
        rw [Nat.zero_add] at ih ⊢
        simp only [ih, add_comm 1, ofDigits_one_cons, Nat.cast_id, digits_one_succ]
    · induction n using Nat.strongRecOn with | ind n h => ?_
      cases n
      · rw [digits_zero]
        rfl
      · simp only [digits_add_two_add_one]
        dsimp [ofDigits]
        rw [h _ (Nat.div_lt_self' _ b)]
        rw [Nat.mod_add_div]

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

Goal state before:
pp: case mpr
b n : ℕ
⊢ n = 0 → b.digits n = []

Tactic:
rintro rfl

Goal state after:
case mpr
b : ℕ
⊢ b.digits 0 = []
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: n p : ℕ
hnp : 1 < p ∧ n ≠ 0
⊢ (go n p hnp).snd * p ^ (go n p hnp).fst = n ∧ ¬p ∣ (go n p hnp).snd

Tactic:
fun_induction go with
  | case1 p hp hmod e q heq hqp ih =>
    rw [heq] at ih
    rcases ih with ⟨rfl, hdvd⟩
    have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
    simp_all [← Nat.dvd_iff_mod_eq_zero, Nat.pow_add', ← Nat.mul_assoc, Nat.div_mul_cancel,
      Nat.two_mul, Nat.mul_pow]
  | case2 p hp hmod e q heq hqp ih =>
    rw [heq] at ih
    rcases ih with ⟨rfl, hdvd⟩
    simp_all [Nat.dvd_iff_mod_eq_zero, Nat.two_mul, Nat.mul_pow, Nat.pow_add]
  | case3 =>
    simp_all [Nat.dvd_iff_mod_eq_zero]

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

Goal state before:
pp: n b e : ℕ
h_b_pos : 0 < b
⊢ n < b ^ e.succ → n / b < b ^ e

Tactic:
simp only [Nat.pow_succ]
  exact (@Nat.div_lt_iff_lt_mul b n (b ^ e) h_b_pos).mpr

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

Goal state before:
pp: ⊢ factorization 0 = 0

Tactic:
by ext; simp [factorization]

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

Goal state before:
pp: ⊢ factorization 1 = 0

Tactic:
by ext; simp [factorization]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun x_1 ↦ x * x_1
⊢ 0 = n ↔ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1

Tactic:
rw [iff_false_left h.ne]
    rintro ⟨h', -⟩
    exact h1 ⟨n, h, h'⟩

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

Goal state before:
pp: case mp
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
⊢ f = n.factorization → (f.prod fun x1 x2 ↦ x1 ^ x2) = n

Tactic:
rintro rfl

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
hf : ∀ p ∈ n.factorization.support, Prime p
⊢ (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) = n
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case mpr
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) = n → f = n.factorization

Tactic:
rintro rfl

Goal state after:
case mpr
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
hn : (f.prod fun x1 x2 ↦ x1 ^ x2) ≠ 0
⊢ f = (f.prod fun x1 x2 ↦ x1 ^ x2).factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
⊢ orderOf x = n

Tactic:
by
  -- Let `a` be `n/(orderOf x)`, and show `a = 1`
  obtain ⟨a, ha⟩ := exists_eq_mul_right_of_dvd (orderOf_dvd_of_pow_eq_one hx)
  suffices a = 1 by simp [this, ha]
  -- Assume `a` is not one...
  by_contra h
  have a_min_fac_dvd_p_sub_one : a.minFac ∣ n := by
    obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd
    rw [hb, ← mul_assoc] at ha
    exact Dvd.intro_left (orderOf x * b) ha.symm
  -- Use the minimum prime factor of `a` as `p`.
  refine hd a.minFac (Nat.minFac_prime h) a_min_fac_dvd_p_sub_one ?_
  rw [← orderOf_dvd_iff_pow_eq_one, Nat.dvd_div_iff_mul_dvd a_min_fac_dvd_p_sub_one, ha, mul_comm,
    Nat.mul_dvd_mul_iff_left (IsOfFinOrder.orderOf_pos _)]
  · exact Nat.minFac_dvd a
  · rw [isOfFinOrder_iff_pow_eq_one]
    exact Exists.intro n (id ⟨hn, hx⟩)

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
⊢ #({i ∈ Ico 1 b | p ^ i ∣ n + 1}) + ∑ i ∈ Ico 1 b, n / p ^ i =
    ∑ i ∈ Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0)

Tactic:
simp [Nat.add_comm, sum_add_distrib, sum_boole]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ≠ 1 ∧ b.natAbs ≠ 0 ↔ a.natAbs ≠ 1 ∧ b ≠ 0

Tactic:
Int.natAbs_ne_zero

Goal state after:
a b : ℤ
⊢ a.natAbs ≠ 1 ∧ b ≠ 0 ↔ a.natAbs ≠ 1 ∧ b ≠ 0
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k : ℕ
p_large : n < p ^ 2
⊢ (n.choose k).factorization p ≤ 1

Tactic:
apply factorization_choose_le_log.trans
  rcases eq_or_ne n 0 with (rfl | hn0); · simp
  exact Nat.lt_succ_iff.1 (log_lt_of_lt_pow hn0 p_large)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
p : ℕ
hp : p ≠ 2
inst✝ : CharP R p
x : R
⊢ x = -1 → ¬x = 1

Tactic:
rintro rfl

Goal state after:
R : Type u_6
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
p : ℕ
hp : p ≠ 2
inst✝ : CharP R p
⊢ ¬-1 = 1
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ emultiplicity p (p * n)! = emultiplicity p n ! + ↑n

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    simp only [hp, emultiplicity_factorial_mul_succ, ih, factorial_succ, emultiplicity_mul,
      cast_add, cast_one, ← add_assoc]
    congr 1
    rw [add_comm, add_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Finite R
⊢ p ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Finite R
inst✝ : CharP R 0
⊢ False
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) = ↑(n - multiplicity p k)

Tactic:
push_cast

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) = ↑n - ↑(multiplicity p k)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mp
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b → ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b

Tactic:
rintro rfl

Goal state after:
case mp
a : ℕ
ha hb : a ≠ 0
⊢ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p a
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case refine_1
p n k : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose k
⊢ k ≠ 0

Tactic:
rintro rfl

Goal state after:
case refine_1
p n : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose 0
⊢ False
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case refine_2
p n k : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose k
⊢ k ≠ p ^ n

Tactic:
rintro rfl

Goal state after:
case refine_2
p n : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose (p ^ n)
⊢ False
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
k : ℕ
k_pos : k ≠ 0
ha : a ^ k = 1
⊢ card ↥(zpowers a) ≤ k

Tactic:
rw [Fintype.card_zpowers]
  apply orderOf_le_of_pow_eq_one k_pos.bot_lt ha

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

Goal state before:
pp: h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 n ! + ↑n < ↑(n + n)

Tactic:
push_cast

Goal state after:
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 n ! + ↑n < ↑n + ↑n
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ ↑(2 * n) < ↑(2 * n) + 1

Tactic:
exact mod_cast lt_succ_self _

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ ↑((Nat.card G).gcd n) = g ^ (↑(Nat.card G) * (Nat.card G).gcdA n + ↑n * (Nat.card G).gcdB n)
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g

Tactic:
rwa [zpow_add, zpow_mul, zpow_mul', zpow_natCast, zpow_natCast, zpow_natCast, h.gcd_eq_one,
      pow_one, pow_card_eq_one', one_zpow, one_mul, eq_comm] at key

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Semiring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
a : G
ha₀ : 0 ≤ a
ha✝ : IsOfFinOrder a
n : ℕ
hn : 0 < n
ha : a ^ n = 1
⊢ a = 1

Tactic:
exact (pow_eq_one_iff_of_nonneg ha₀ hn.ne').1 ha

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
a : G
ha₀ : a ≤ 0
ha : IsOfFinOrder a
⊢ ¬a = 1

Tactic:
rintro rfl

Goal state after:
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
ha₀ : 1 ≤ 0
ha : IsOfFinOrder 1
⊢ False
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ rootMultiplicity a (p * (X - C a) ^ n) ≤ rootMultiplicity a p + n

Tactic:
rw [rootMultiplicity_le_iff h2, add_assoc, add_comm n, ← add_assoc, pow_add,
      dvd_cancel_right_mem_nonZeroDivisors (monic_X_sub_C a |>.pow n |>.mem_nonZeroDivisors)]

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
h2 : p * (X - C a) ^ n ≠ 0
⊢ ¬(X - C a) ^ (rootMultiplicity a p + 1) ∣ p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = p * C q.leadingCoeff

Tactic:
obtain ⟨r, rfl⟩ := hdvd
  obtain rfl | hr := eq_or_ne r 0
  · simp
  have : r.natDegree = 0 := by simpa [hp.natDegree_mul' hr] using hdeg
  rw [eq_C_of_natDegree_eq_zero this]
  simp [leadingCoeff_monic_mul hp]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative (X ^ (n + 1)) = C (↑n + 1) * X ^ n

Tactic:
simp [derivative_X_pow]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : ¬q.degree ≤ p.degree
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
unfold divByMonic divModByMonicAux
        simp [dif_pos hq, h, degree_zero, bot_le]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ((map f p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = map f (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1))

Tactic:
rw [sum_over_range' _ _ (n + 1) ((le_max_left _ _).trans_lt (lt_add_one _))]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ((map f p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f
hf : Irreducible ((expand R (p * p ^ n)) f)
⊢ Irreducible ((expand R p) ((expand R (p ^ n)) f))

Tactic:
rwa [expand_expand]

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ p ≠ 0

Tactic:
rintro rfl

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
hp : natDegree 0 ≠ 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case zero
R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ X ^ n = ↑(n.descFactorial 0) * X ^ (n - 0)

Tactic:
tsub_zero,

Goal state after:
case zero
R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ X ^ n = ↑(n.descFactorial 0) * X ^ n
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
⊢ I.pi s ∈ pi f

Tactic:
rw [pi_def, biInter_eq_iInter]

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
⊢ ⋂ x, eval ↑x ⁻¹' s ↑x ∈ pi f
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
lb : Filter β
ld : Filter δ
⊢ comap (Prod.map f g) (lb ×ˢ ld) = comap f lb ×ˢ comap g ld

Tactic:
by
  simp [prod_eq_inf, comap_comap, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
f₁ f₂ : Filter α
⊢ (f₁ ⊓ f₂) ×ˢ g = (f₁ ⊓ f₂) ×ˢ (g ⊓ g)

Tactic:
inf_idem

Goal state after:
α : Type u_1
β : Type u_2
g : Filter β
f₁ f₂ : Filter α
⊢ (f₁ ⊓ f₂) ×ˢ g = (f₁ ⊓ f₂) ×ˢ g
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊓ g₂) = (f ⊓ f) ×ˢ (g₁ ⊓ g₂)

Tactic:
inf_idem

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊓ g₂) = f ×ˢ (g₁ ⊓ g₂)
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: p : ℕ → Prop
⊢ (∃ᶠ (n : ℕ) in cofinite, p n) ↔ {n | p n}.Infinite

Tactic:
frequently_cofinite_iff_infinite

Goal state after:
p : ℕ → Prop
⊢ {x | p x}.Infinite ↔ {n | p n}.Infinite
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case pos
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∃ y ∈ s, ∃ x, f y < x
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
rcases all_top with ⟨y, hys, x, hx⟩

Goal state after:
case pos
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case mpr
α : Type u_2
f : Filter α
⊢ f.kerᶜ ∈ f → f.ker = ∅

Tactic:
· intro h
    rw [eq_empty_iff_forall_notMem]
    intro x hx
    exact hx f.kerᶜ h hx

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
x : R
w : p ≠ 0
⊢ x ∈ p.roots ↔ (aeval x) p = 0

Tactic:
by
  rw [aeval_def, ← mem_roots_map_of_injective (FaithfulSMul.algebraMap_injective _ _) w,
    Algebra.algebraMap_self, map_id]

Goal state after: