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

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
⊢ (l.sum fun i a ↦ a • _root_.id i) ∈ span R (p * q)

Tactic:
Finsupp.sum

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
⊢ ∑ a ∈ l.support, l a • _root_.id a ∈ span R (p * q)
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: m k x y : ℕ
hmk : m ∣ k
⊢ x ^ m - y ^ m ∣ x ^ k - y ^ k

Tactic:
obtain ⟨n, rfl⟩ := hmk

Goal state after:
m x y n : ℕ
⊢ x ^ m - y ^ m ∣ x ^ (m * n) - y ^ (m * n)
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ ↑s ⊆ Set.range ⇑f

Tactic:
← AlgHom.coe_range,

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ ↑s ⊆ ↑f.range
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f (Algebra.adjoin R ↑(s.preimage ⇑f ⋯)) = map f S

Tactic:
rw [← Algebra.adjoin_image, Finset.coe_preimage, Set.image_preimage_eq_of_subset, hs]
      rw [← AlgHom.coe_range, ← Algebra.adjoin_le_iff, hs, ← Algebra.map_top]
      exact map_mono le_top

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

Goal state before:
pp: case mpr.refine_2
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ (p * X ^ (n - p.natDegree)).coeff n = p.coeff p.natDegree

Tactic:
← coeff_mul_X_pow p (n - natDegree p),

Goal state after:
case mpr.refine_2
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑n
this : p.natDegree + (n - p.natDegree) = n
⊢ (p * X ^ (n - p.natDegree)).coeff n = (p * X ^ (n - p.natDegree)).coeff (p.natDegree + (n - p.natDegree))
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ Set.range ⇑((FreeAlgebra.lift R) Subtype.val) = Set.univ

Tactic:
← AlgHom.coe_range,

Goal state after:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ ↑((FreeAlgebra.lift R) Subtype.val).range = Set.univ
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
⊢ x ∈ Set.range ⇑(MvPolynomial.aeval Subtype.val)

Tactic:
← AlgHom.coe_range,

Goal state after:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
⊢ x ∈ ↑(MvPolynomial.aeval Subtype.val).range
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ Set.range ⇑(MvPolynomial.aeval Subtype.val) = Set.univ

Tactic:
← AlgHom.coe_range,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑(MvPolynomial.aeval Subtype.val).range = Set.univ
Module: Mathlib.Data.Int.ModEq

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

Tactic:
← add_modulus_mul_modEq_iff,

Goal state after:
n a b c : ℤ
⊢ a - n * b + n * ?m.12 ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

n a b c : ℤ
⊢ ℤ
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]

Tactic:
Nat.modEq_iff_dvd' hle,

Goal state after:
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ p ∣ b - a
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ Even p ↔ p = 2

Tactic:
even_iff_two_dvd,

Goal state after:
p : ℕ
hp : Prime p
⊢ 2 ∣ p ↔ p = 2
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
F : Type w
inst✝¹⁰ : Ring R
inst✝⁹ : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : Ring A
inst✝⁵ : Algebra R₁ A
inst✝⁴ : Algebra R₂ A
inst✝³ : Ring B
inst✝² : Algebra R₁ B
I : Ideal A
J : Ideal B
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : A ≃ₐ[R₁] B
hIJ : J = map (↑f) I
⊢ I = map (↑f.symm) J

Tactic:
by simp only [← AlgEquiv.toAlgHom_toRingHom, hIJ, map_map, ← AlgHom.comp_toRingHom,
        AlgEquiv.symm_comp, AlgHom.id_toRingHom, map_id]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
x : α
hx : ¬x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 ↦ decide (x = x_1)) (y :: l)).length + 1

Tactic:
rw [takeWhile]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
x : α
hx : ¬x = y
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (match decide (x = y) with
        | true => y :: takeWhile (fun x_1 ↦ decide (x = x_1)) l
        | false => []).length +
      1
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ (permutations'Aux x s).get ⟨s.length, ⋯⟩ = t.insertIdx s.length x

Tactic:
← get_permutations'Aux t x s.length (by simp [hl])

Goal state after:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ (permutations'Aux x s).get ⟨s.length, ⋯⟩ = (permutations'Aux x t).get ⟨s.length, ⋯⟩
Module: Mathlib.Data.List.Cycle

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

Tactic:
rw [nodup_iff_injective_get] at hl

Goal state after:
case h.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h✝ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' : (y :: hd :: tl).dropLast[k + 1] = (y :: hd :: tl).getLast ⋯
⊢ k + 1 = (hd :: tl).length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length

Tactic:
rw [← Nat.add_sub_assoc, Nat.sub_add_comm, Nat.add_mod_right, Nat.mod_eq_of_lt]

Goal state after:
case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 < (head :: tail).length

case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ idxOf a (head :: tail)

case neg.e_i.h
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ (head :: tail).length
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.right.inl
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
hx' : (bs.insertIdx m x)[n] = x
ht : n < m
⊢ x ∈ bs

Tactic:
rw [← hx', getElem_insertIdx_of_lt ht]

Goal state after:
case cons.right.inl
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
hx' : (bs.insertIdx m x)[n] = x
ht : n < m
⊢ bs[n] ∈ bs
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
dsimp [ZMod.cast]
    rw [Int.cast_natCast, natCast_zmod_val]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∉ H
⊢ H.index ∣ 2

Tactic:
refine dvd_of_eq (index_eq_two_iff.mpr
        ⟨a, fun b ↦ (xor_iff_or_and_not_and _ _).mpr ⟨ha b, fun h ↦ ha' ?_⟩⟩)

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∉ H
b : G
h : b * a ∈ H ∧ b ∈ H
⊢ a ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
⊢ ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H

Tactic:
suffices ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ((a ^ n₂ : G) : G ⧸ H) = ((a ^ n₁ : G) : G ⧸ H) by
    rcases this with ⟨n₁, n₂, hlt, hle, he⟩
    refine ⟨n₂ - n₁, by lia, by lia, ?_⟩
    rw [eq_comm, QuotientGroup.eq, ← zpow_natCast, ← zpow_natCast, ← zpow_neg, ← zpow_add,
        add_comm] at he
    rw [← zpow_natCast]
    convert! he
    lia

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m = n
⊢ ZMod m ≃+* ZMod n

Tactic:
rcases m with - | m <;> rcases n with - | n

Goal state after:
case zero.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
h : 0 = 0
⊢ ZMod 0 ≃+* ZMod 0

case zero.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : 0 = n + 1
⊢ ZMod 0 ≃+* ZMod (n + 1)

case succ.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
m : ℕ
h : m + 1 = 0
⊢ ZMod (m + 1) ≃+* ZMod 0

case succ.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
⊢ ZMod (m + 1) ≃+* ZMod (n + 1)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n ↦ ↑(a ^ ↑n)
⊢ Injective f

Tactic:
rintro ⟨n₁, h₁, hle₁⟩ ⟨n₂, h₂, hle₂⟩ he

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n ↦ ↑(a ^ ↑n)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he : f ⟨n₁, ⋯⟩ = f ⟨n₂, ⋯⟩
⊢ ⟨n₁, ⋯⟩ = ⟨n₂, ⋯⟩
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ p.1 ≠ 0 ∧ p.2 ≠ 0

Tactic:
obtain ⟨hp₁, hp₂⟩ := Nat.mem_divisorsAntidiagonal.mp hp
  exact mul_ne_zero_iff.mp (hp₁.symm ▸ hp₂)

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
⊢ if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i

Tactic:
by
  have hx0 : x < 0 := (le_add_of_nonneg_right zero_le_one).trans_lt hx
  refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
  · simp only [geom_sum_two, lt_add_iff_pos_left, ite_true, hx, even_two]
  clear hn
  intro n _ ihn
  simp only [Nat.even_add_one, geom_sum_succ]
  split_ifs at ihn ⊢ with hn'
  · rw [lt_add_iff_pos_left]
    exact mul_pos_of_neg_of_neg hx0 ihn
  · grw [← hx.le]
    gcongr
    simpa only [mul_one] using mul_lt_mul_of_neg_left ihn hx0

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

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ ↑m * ↑(↑m)⁻¹.val = 1

Tactic:
obtain rfl | hn := eq_or_ne n 0
  · simp [m.coprime_zero_right.1 hmn]
  have : NeZero n := ⟨hn⟩
  rw [ZMod.natCast_zmod_val, ZMod.coe_mul_inv_eq_one _ hmn]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1 ∨ ∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1

Tactic:
rw [or_iff_not_imp_right]

Goal state after:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
⊢ ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1 → ∑ x ∈ (n + 1 + 1).properDivisors, x = 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ f p * ∏ x ∈ p.properDivisors, f x = f p * f 1

Tactic:
h.prod_properDivisors

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ f p * f 1 = f p * f 1
Module: Mathlib.Algebra.Order.Ring.GeomSum

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

Tactic:
by
      rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert] <;>
        simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z✝ : ℤ
x✝ : z✝.divisors.Nonempty
hx : z✝ = 0
z : ℤ
hz : z ∈ z✝.divisors
⊢ False

Tactic:
by simp [hx] at hz

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

Goal state before:
pp: n✝ : ℕ
a : ZMod (n✝ + 1)
| 2 * a = 0

Tactic:
← a.natCast_zmod_val,

Goal state after:
n✝ : ℕ
a : ZMod (n✝ + 1)
| 2 * ↑a.val = 0
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
⊢ n.choose k ≤ (n + 1 - k) ^ k

Tactic:
rcases le_or_gt k n with h | h
  · obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le h
    rw [Nat.add_comm k m, Nat.add_right_comm, Nat.add_sub_cancel]
    exact choose_add_le_add_one_pow m k
  · simp [choose_eq_zero_of_lt h]

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

Goal state before:
pp: n : ℕ
⊢ n.centralBinom ≤ (2 ^ 2) ^ n

Tactic:
← pow_mul,

Goal state after:
n : ℕ
⊢ n.centralBinom ≤ 2 ^ (2 * n)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case case1
n p✝ p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : q % p = 0
ih : (go n (p * p) ⋯).snd * (p * p) ^ (go n (p * p) ⋯).fst = n ∧ ¬p * p ∣ (go n (p * p) ⋯).snd
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = n ∧ ¬p ∣ (2 * e + 1, q / p).snd

Tactic:
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]

Goal state after:
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
⊢ (b.digits (n / b)).length + 1 = log b n + 1

Tactic:
rw [IH _ this h, log_div_base, tsub_add_cancel_of_le]

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
⊢ 1 ≤ log b n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: M₀ : Type u_6
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
⊢ ¬∃ n, 0 < n ∧ 0 ^ n = 1

Tactic:
simp +contextual [ne_of_gt]

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]
  simp +contextual [ne_of_gt]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h✝ : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ (x ^ n) ^ m = x

Tactic:
← pow_mul,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h✝ : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ x ^ (n * m) = x
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
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ x ^ (n / a.minFac) = 1

Tactic:
← orderOf_dvd_iff_pow_eq_one,

Goal state after:
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
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ orderOf x ∣ n / a.minFac
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
by
  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, modEq_zero_iff] at hnm

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ n = (x + y) ^ (n % p) * ((x + y) ^ p) ^ (n / p)

Tactic:
← pow_mul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ n = (x + y) ^ (n % p) * (x + y) ^ (p * (n / p))
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ n = (x - y) ^ (n % p) * ((x - y) ^ p) ^ (n / p)

Tactic:
← pow_mul,

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ n = (x - y) ^ (n % p) * (x - y) ^ (p * (n / p))
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ False

Tactic:
exact Nat.cast_ne_zero.2 hn.ne' (h <| by simpa using hx)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : ¬IsOfFinOrder x
⊢ zpowers x = zpowers y ↔ x = y ∨ x⁻¹ = y

Tactic:
refine ⟨fun h ↦ ?_, by rintro (rfl | rfl) <;> simp⟩
  have hx_mem : x ∈ zpowers y := by simp [← h]
  have hy_mem : y ∈ zpowers x := by simp [h]
  obtain ⟨k, rfl⟩ := mem_zpowers_iff.mp hy_mem
  obtain ⟨l, hl⟩ := mem_zpowers_iff.mp hx_mem
  rw [← zpow_mul] at hl
  nth_rewrite 2 [← zpow_one x] at hl
  have h1 := (injective_zpow_iff_not_isOfFinOrder.mpr hx) hl
  rcases (Int.mul_eq_one_iff_eq_one_or_neg_one).mp h1 with (h | h) <;> simp [h.1]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ card G = orderOf x * card (G ⧸ zpowers x)

Tactic:
← card_zpowers,

Goal state after:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ card G = card ↥(zpowers x) * card (G ⧸ zpowers x)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (f.sum fun a b ↦ (C b * (X ^ p) ^ a).coeff n) = if p ∣ n then f.coeff (n / p) else 0

Tactic:
← pow_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (f.sum fun a b ↦ (C b * X ^ (p * a)).coeff n) = if p ∣ n then f.coeff (n / p) else 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r (((X - C r) ^ p ^ n) ^ rootMultiplicity (r ^ p ^ n) f * (expand R (p ^ n)) g)

Tactic:
← pow_mul,

Goal state after:
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r ((X - C r) ^ (p ^ n * rootMultiplicity (r ^ p ^ n) f) * (expand R (p ^ n)) g)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
⊢ rootMultiplicity r ((expand R (p ^ 1)) f) = p ^ 1 * rootMultiplicity (r ^ p ^ 1) f

Tactic:
rootMultiplicity_expand_pow

Goal state after:
R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
⊢ p ^ 1 * rootMultiplicity (r ^ p ^ 1) f = p ^ 1 * rootMultiplicity (r ^ p ^ 1) f