mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]

Tactic:
simp [modEq_iff_dvd]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a + b ≡ a [ZMOD n] ↔ n ∣ b

Tactic:
simp [modEq_iff_dvd]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b : ℤ
⊢ a ≡ b [ZMOD 0] ↔ a = b

Tactic:
by rw [ModEq, emod_zero, emod_zero]

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

Goal state before:
pp: case inr.inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : -1 = 1
⊢ -1 = 1

Tactic:
· exact ((Ring.neg_one_ne_one_of_char_ne_two hR) h).elim

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

Goal state before:
pp: p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
⊢ 5 ≤ p

Tactic:
by_contra! h

Goal state after:
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
h : p < 5
⊢ False
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
⊢ x = p ∧ y = p

Tactic:
have pdvdxy : p ∣ x * y := by rw [h]; simp [sq]

Goal state after:
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
⊢ x = p ∧ y = p
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case algebraMap.mem
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b : A
r : R
x✝ : A
h : x✝ ∈ s
⊢ p x✝ ((algebraMap R A) r) ⋯ ⋯

Tactic:
exact algebraMap_right _ _ h

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

Goal state before:
pp: case algebraMap
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b : A
ha : a ∈ adjoin R s
r : R
⊢ p a ((algebraMap R A) r) ha ⋯

Tactic:
induction ha using adjoin_induction with
    | mem _ h => exact algebraMap_right _ _ h
    | algebraMap _ => exact algebraMap_both _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | star _ _ h => exact star_left _ _ _ _ h

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

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

Tactic:
apply prev_getLast_cons

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l.next l[k] hx = (l.rotate n).next l[k] ⋯

Tactic:
next_getElem _ hn

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l[(k + 1) % l.length] = (l.rotate n).next l[k] ⋯
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : R
x✝ : ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
p : R
k : ℕ
hp : Prime p
hk : 0 < k
hn : p ^ k = n
⊢ p ^ (k - 1 + 1) = n

Tactic:
by rwa [Nat.sub_add_cancel hk]

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]

Goal state after:
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
⊢ g₁⁻¹ * g₂ ∈ stabilizer G x
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
⊢ n = p ^ n.primeFactorsList.length

Tactic:
set k := n.primeFactorsList.length

Goal state after:
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := n.primeFactorsList.length
⊢ n = p ^ k
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod

Tactic:
← List.prod_append,

Goal state after:
case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = ((a + 1 + 1).primeFactorsList ++ b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
Module: Mathlib.GroupTheory.Index

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

Tactic:
← inf_relIndex_right (H ⊓ K) L,

Goal state after:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ K ⊓ L).relIndex L
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊥.index = Nat.card ↥H

Tactic:
index_bot

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nat.card ↥H = Nat.card ↥H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊤.index = 1

Tactic:
index_top

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ 1 = 1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
K : Subgroup ↥H
⊢ K.index * H.subtype.range.index = K.index * H.index

Tactic:
H.range_subtype

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
K : Subgroup ↥H
⊢ K.index * H.index = K.index * H.index
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).relIndex ⊤ ≠ 0
⊢ (⨅ i, f i).relIndex ⊤ ≠ 0

Tactic:
exact relIndex_iInf_ne_zero hf

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.IsFiniteRelIndex K ↔ (H.subgroupOf K).FiniteIndex

Tactic:
rw [isFiniteRelIndex_iff_relIndex_ne_zero, finiteIndex_iff, relIndex]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
a : ℕ × ℕ
⊢ a.swap ∈ n.divisorsAntidiagonalList ↔ a ∈ n.divisorsAntidiagonalList

Tactic:
simp [mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ n ≤ n.divisors.sup id

Tactic:
exact Finset.le_sup (f := id) <| mem_divisors_self n hn

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

Goal state before:
pp: m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ ↑(Nat.chineseRemainder h x.cast.1.val x.cast.2.val) ≡ x.val [MOD m] ∧
    ↑(Nat.chineseRemainder h x.cast.1.val x.cast.2.val) ≡ x.val [MOD n]

Tactic:
Prod.fst_zmod_cast,

Goal state after:
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ ↑(Nat.chineseRemainder h x.cast.val x.cast.2.val) ≡ x.val [MOD m] ∧
    ↑(Nat.chineseRemainder h x.cast.val x.cast.2.val) ≡ x.val [MOD n]
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ Set.InjOn (HDiv.hDiv n) ↑n.divisors

Tactic:
· intro x hx y hy h
    rw [mem_coe, mem_divisors] at hx hy
    exact (div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
z : ℤ
⊢ xy.swap ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Tactic:
simp [mul_comm]

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

Goal state before:
pp: case neg.zero
k : ℕ
lt : ¬0 + 1 < k
⊢ (0 + 1).choose k ≤ 2 ^ 0

Tactic:
cases k <;> simp_all

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

Goal state before:
pp: m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
this : NeZero n
⊢ a.cast.cast = a

Tactic:
rw [cast_eq_val, val_cast_eq_val_of_lt (a.val_lt.trans_le h), natCast_zmod_val]

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

Goal state before:
pp: case zero
M : Type u_1
inst✝ : AddCommMonoid M
⊢ Subsingleton (Module (ZMod 0) M)

Tactic:
exact inferInstanceAs (Subsingleton (Module ℤ M))

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

Goal state before:
pp: case succ
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits % p ^ (i + 1) = ofDigits p (List.take (i + 1) digits)

Tactic:
| succ i ih =>

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: M₀ : Type u_6
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
⊢ orderOf 0 = 0

Tactic:
rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one]

Goal state after:
M₀ : Type u_6
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
⊢ ¬∃ n, 0 < n ∧ 0 ^ n = 1
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ ∀ (a : α) (s : Finset α),
    a ∈ S →
      s ⊆ S →
        a ∉ s →
          (s.prod g).factorization = ∑ x ∈ s, (g x).factorization →
            ((insert a s).prod g).factorization = ∑ x ∈ insert a s, (g x).factorization

Tactic:
intro x T hxS hTS hxT IH

Goal state after:
case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : x ∉ T
IH : (T.prod g).factorization = ∑ x ∈ T, (g x).factorization
⊢ ((insert x T).prod g).factorization = ∑ x ∈ insert x T, (g x).factorization
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: p a b : ℕ
hab : a.Coprime b
⊢ (a * b).factorization p = a.factorization p + b.factorization p

Tactic:
simp only [← primeFactorsList_count_eq,
    perm_iff_count.mp (perm_primeFactorsList_mul_of_coprime hab), count_append]

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

Goal state before:
pp: a b p : ℕ
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
by
  if ha : a = 0 then simp [ha] else
  if hb : b = 0 then simp [hb] else
  simp only [ordProj_mul p ha hb]
  rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]

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

Goal state before:
pp: p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ p ^ k ∣ p ^ n.factorization p

Tactic:
pow_dvd_pow_iff_le_right pp.one_lt,

Goal state after:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ k ≤ n.factorization p
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case zero
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : 0 ≠ 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : n = 0
⊢ i < b

pp: case zero
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : 0 ≠ 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : 0 ^ i ∣ n
⊢ i ≠ 0

Tactic:
exacts [(hn.ne' h).elim, one_le_iff_ne_zero.1 hi]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
· have := (infinite_powers.2 ha).to_subtype
    rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ (p - 1) * multiplicity p n ! = n - (p.digits n).sum

Tactic:
simp only [multiplicity_eq_of_emultiplicity_eq_some <|
      emultiplicity_factorial hp <| lt_succ_of_lt <| Nat.lt_add_one (log p n),
    ← Finset.sum_Ico_add' _ 0 _ 1, Ico_zero_eq_range, ←
    sub_one_mul_sum_log_div_pow_eq_sub_sum_digits]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
· have := (infinite_powers.2 ha).to_subtype
    rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
x y : R
n : ℕ
h : Commute x y
inst✝ : CharZero R
⊢ (x + y) ^ 1 ^ n = x ^ 1 ^ n + y ^ 1 ^ n

pp: case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
· simp only [one_pow, pow_one]

Goal state after:
case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ (finEquivZPowers hx).symm ⟨x ^ n, ⋯⟩ = ⟨n % orderOf x, ⋯⟩

Tactic:
rw [finEquivZPowers, Equiv.symm_trans_apply]; exact finEquivPowers_symm_apply _ n

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n + 1 ^ p ^ n = 0

Tactic:
rw [← add_pow_expChar_pow_of_commute _ _ (Commute.one_right _), neg_add_cancel,
    zero_pow (pow_ne_zero _ <| expChar_ne_zero R p)]

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)
⊢ emultiplicity p (k ! * n !) ≠ ⊤

Tactic:
apply finiteMultiplicity_iff_emultiplicity_ne_top.1

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)
⊢ FiniteMultiplicity p (k ! * n !)
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : bit b 0 ≠ 0
⊢ emultiplicity 2 (bit b 0)! < ↑(bit b 0)

Tactic:
simp only [ne_eq, bit_eq_zero_iff, true_and, Bool.not_eq_false] at h

Goal state after:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ emultiplicity 2 (bit b 0)! < ↑(bit b 0)
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2

Tactic:
· decide

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
⊢ ↑n ≠ ⊤

Tactic:
exact Ne.symm nofun

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

Goal state before:
pp: case mpr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ x %ᵒᶠ g = 0 → of' k G g ∣ x

Tactic:
· intro h
    rw [← divOf_add_modOf x g, h, add_zero]
    exact dvd_mul_right _ _

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff = (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff

Tactic:
simp [mul_comm]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ (contract p f).coeff n = f.coeff (n * p)

Tactic:
simp only [contract, coeff_monomial, sum_ite_eq', finsetSum_coeff, mem_range, not_lt,
    ite_eq_left_iff]

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ f.natDegree + 1 ≤ n → 0 = f.coeff (n * p)
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]; exact one_ne_zero

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ eval₂ g x (s • p) = g s * eval₂ g x p

Tactic:
rw [eval₂_eq_sum, eval₂_eq_sum, sum_over_range' _ _ _ A, sum_over_range' _ _ _ B]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∑ a ∈ range p.natDegree.succ, g ((s • p).coeff a) * x ^ a = g s * ∑ a ∈ range p.natDegree.succ, g (p.coeff a) * x ^ a

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∀ (n : ℕ), g 0 * x ^ n = 0

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∀ (n : ℕ), g 0 * x ^ n = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
| p

Tactic:
← modByMonic_add_div p 1

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
| p %ₘ 1 + 1 * (p /ₘ 1)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < (X - C a).degree

Tactic:
rw [degree_X_sub_C]

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < 1
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ 0 < (X - C a).degree

Tactic:
rw [degree_X_sub_C]

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ 0 < 1
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : g.IsCountablyGenerated
⊢ (f ⊓ g).IsCountablyGenerated

Tactic:
rcases f.exists_antitone_basis with ⟨s, hs⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
⊢ (f ⊓ g).IsCountablyGenerated
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : g.IsCountablyGenerated
⊢ (f ⊔ g).IsCountablyGenerated

Tactic:
rcases f.exists_antitone_basis with ⟨s, hs⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
⊢ (f ⊔ g).IsCountablyGenerated
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case mpr
α : Type u_1
f : Filter α
⊢ (∃ x, f.HasAntitoneBasis x) → f.IsCountablyGenerated

Tactic:
· rintro ⟨x, h⟩
    rw [h.1.eq_iInf]
    exact isCountablyGenerated_seq x

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
⊢ p.degree = 1

Tactic:
by
      have h₁ : degree (X - C x) = 1 := degree_X_sub_C x
      have h₂ : degree (X - C x) = 0 := degree_eq_zero_of_isUnit h
      rw [h₁] at h₂; exact absurd h₂ (by decide)

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s

Tactic:
rintro ⟨t₁, ⟨s₁, hs₁, hts₁⟩, t₂, ⟨s₂, hs₂, hts₂⟩, rfl⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
t₁ : Set (α × β)
s₁ : Set α
hs₁ : s₁ ∈ f
hts₁ : Prod.fst ⁻¹' s₁ ⊆ t₁
t₂ : Set (α × β)
s₂ : Set β
hs₂ : s₂ ∈ g
hts₂ : Prod.snd ⁻¹' s₂ ⊆ t₂
⊢ ∃ t₁_1 ∈ f, ∃ t₂_1 ∈ g, t₁_1 ×ˢ t₂_1 ⊆ t₁ ∩ t₂
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
⊢ map (Pi.map f) (pi l) = pi fun i ↦ map (f i) (l i)

Tactic:
refine le_antisymm (tendsto_piMap_pi fun _ ↦ tendsto_map) ?_

Goal state after:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
⊢ (pi fun i ↦ map (f i) (l i)) ≤ map (Pi.map f) (pi l)