mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos.refine_1
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ ∀ b ∈ s, (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)

Tactic:
intro b

Goal state after:
case pos.refine_1
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
⊢ b ∈ s → (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos.refine_2
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ ∀ b ∈ s, (WithBot.some ∘ fun i ↦ (f i).natDegree) b ≤ s.sup' hs fun i ↦ (f i).degree

Tactic:
intro b

Goal state after:
case pos.refine_2
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
⊢ b ∈ s → (WithBot.some ∘ fun i ↦ (f i).natDegree) b ≤ s.sup' hs fun i ↦ (f i).degree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

Tactic:
simp_rw [h, ne_eq, or_true, iff_true, ← Nat.le_zero, ← h, natDegree_map_le]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
⊢ m ∈ (((finSuccEquiv R n) p).coeff i).support → m j ≤ p.support.sup fun m ↦ m j.succ

Tactic:
hm

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ (((finSuccEquiv R n) p).coeff i).support
⊢ m j ≤ p.support.sup fun m ↦ m j.succ
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : ∀ (f_1 g_1 : R[X]), f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → f_1.natDegree = 0 ∨ g_1.natDegree = 0
⊢ ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ (f * g).natDegree)

Tactic:
rw [hf.natDegree_mul hg, add_le_add_iff_right]
    exact fun ha => (h f g hf hg rfl).elim (ha.1.trans_le ha.2).ne' ha.1.ne'

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
h : Even k
⊢ (-1) ^ k + 0 = 1

Tactic:
rw [h.neg_one_pow, add_zero]

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

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
⊢ p.degree < ↑m → (k • p).coeff m = 0

Tactic:
hm

Goal state after:
case refine_1
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : p.degree < ↑m
⊢ (k • p).coeff m = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
⊢ (k • p).degree < ↑m → p.coeff m = 0

Tactic:
hm

Goal state after:
case refine_2
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : (k • p).degree < ↑m
⊢ p.coeff m = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ (k • p).degree = p.degree

pp: case neg
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ k • p ≠ 0

Tactic:
degree_smul_of_smul_regular p h

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ p.degree = p.degree

case neg
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ k • p ≠ 0
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hSA : ⊤.FG
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ⊤.FG

Tactic:
rcases hSA with ⟨t, ht⟩

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
s : Finset S
hs : adjoin R ↑s = ⊤
t : Finset A
ht : adjoin S ↑t = ⊤
⊢ ⊤.FG
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k i j : ℕ
e : (i, j) ∈ antidiagonal k
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)

Tactic:
obtain rfl : i + j = k := mem_antidiagonal.mp e

Goal state after:
case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a + ∑ x ∈ s, n x - (i + j))
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : FiniteType R A
f : A →ₐ[R] B
hf : Surjective ⇑f
⊢ ⊤ = Subalgebra.map f ⊤

Tactic:
simpa only [map_top f, @eq_comm _ ⊤, eq_top_iff, AlgHom.mem_range] using! hf

Goal state after:
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 = ⊤
⊢ ↑(MvPolynomial.aeval Subtype.val).range = Set.univ

Tactic:
← Algebra.adjoin_range_eq_range_aeval,

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 = ⊤
⊢ ↑(adjoin R (Set.range Subtype.val)) = Set.univ
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : A
hx1 : x ∈ toSubmodule S
⊢ x * 1 ∈ toSubmodule S * toSubmodule S

Tactic:
exact Submodule.mul_mem_mul hx1 (show (1 : A) ∈ S from one_mem S)

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

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

Tactic:
MvPolynomial.mem_map_C_iff,

Goal state after:
R : Type u
S : Type u_1
σ : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝ : MvPolynomial σ R
⊢ x✝ ∈ RingHom.ker (map f) ↔ ∀ (m : σ →₀ ℕ), coeff m x✝ ∈ RingHom.ker f
Module: Mathlib.Data.Int.ModEq

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

Tactic:
rw [← add_modulus_modEq_iff, sub_add_cancel]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ≤ J
⊢ map (Quotient.mk J) I = ⊥

Tactic:
by
  rw [map_eq_bot_iff_le_ker, mk_ker]
  exact h

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: case inr
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Infinite { a // a ≠ 0 }
⊢ 0 - 1 = 0

Tactic:
zero_tsub

Goal state after:
case inr
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Infinite { a // a ≠ 0 }
⊢ 0 = 0
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p → p = a

Tactic:
rintro ⟨j, rfl⟩

Goal state after:
a : ℕ
a1 : a ≠ 1
j : ℕ
hp : Prime (a * j)
⊢ a * j = a
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : Ring 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
H : I ≤ comap f J
x : A
⊢ ((quotientMapₐ J f H).comp (Quotient.mkₐ R₁ I)) x = ((Quotient.mkₐ R₁ J).comp f) x

Tactic:
by simp only [quotient_map_mkₐ, Quotient.mkₐ_eq_mk, AlgHom.comp_apply]

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

Goal state before:
pp: α : Type u_1
t : α
ts : List α
⊢ permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd

Tactic:
induction ts with | nil => rfl | cons a ts ih => ?_
  simp only [permutations'Aux, ih, cons_append, permutationsAux2_snd_cons, append_nil, id_eq,
    cons.injEq, true_and]
  simp +singlePass only [← permutationsAux2_append]
  simp [map_permutationsAux2]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
S : Subalgebra R A
x y : A
hx : x ∈ star S.carrier
hy : y ∈ star S.carrier
⊢ x * y ∈ star S.carrier

Tactic:
by
        simp only [Set.mem_star, Subalgebra.mem_carrier] at *
        exact (star_mul x y).symm ▸ mul_mem hy hx

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

Goal state before:
pp: α : Type u_1
t : α
ts ys l l' : List α
⊢ l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

Tactic:
induction ys generalizing l with
  | nil => simp +contextual
  | cons y ys ih => ?_

Goal state after:
case cons
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ l' ∈ (permutationsAux2 t ts [] (y :: ys) fun x ↦ l ++ x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
S : StarSubalgebra R A
⊢ Algebra.adjoin R (s ∪ star s) ≤ S.toSubalgebra ↔ s ⊆ ↑S

Tactic:
Algebra.adjoin_le_iff,

Goal state after:
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
S : StarSubalgebra R A
⊢ s ∪ star s ⊆ ↑S.toSubalgebra ↔ s ⊆ ↑S
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts : List α
r L : List (List α)
⊢ (foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r L).length = (map length L).sum + r.length

Tactic:
by
  simp [foldr_permutationsAux2, length_permutationsAux2, length_flatMap]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ minimalPeriod f x ≤ n

Tactic:
rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]

Goal state after:
α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ Nat.find ⋯ ≤ n
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m : ℕ
⊢ m ∈ List.range (minimalPeriod f x) → ∀ y ∈ List.range (minimalPeriod f x), f^[m] x = f^[y] x → m = y

Tactic:
hm

Goal state after:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
⊢ ∀ y ∈ List.range (minimalPeriod f x), f^[m] x = f^[y] x → m = y
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
hcomm✝ : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : adjoin R s ≤ centralizer R ↑(centralizer R s)
x✝¹ : A
h₁ : x✝¹ ∈ adjoin R s
x✝ : A
h₂ : x✝ ∈ adjoin R s
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
apply this at h₁

Goal state after:
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
hcomm✝ : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : adjoin R s ≤ centralizer R ↑(centralizer R s)
x✝¹ x✝ : A
h₂ : x✝ ∈ adjoin R s
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : x✝¹ ∈ centralizer R ↑(centralizer R s)
⊢ x✝¹ * x✝ = x✝ * x✝¹
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ flatMap (fun x ↦ flatMap (permutations'Aux y✝) (permutations'Aux x✝ x)) l✝.permutations' ~
    flatMap (permutations'Aux x✝) (flatMap (permutations'Aux y✝) l✝.permutations')

Tactic:
flatMap_assoc

Goal state after:
case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ flatMap (fun x ↦ flatMap (permutations'Aux y✝) (permutations'Aux x✝ x)) l✝.permutations' ~
    flatMap (fun x ↦ flatMap (permutations'Aux x✝) (permutations'Aux y✝ x)) l✝.permutations'
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case pos
α : 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

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:
· subst hx
      simpa [takeWhile, Nat.succ_inj, DecEq_eq] using IH _

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 =
    (takeWhile (fun x_1 ↦ decide (x = x_1)) (y :: l)).length + 1
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
⊢ (permutations'Aux x s).length = s.length + 1

Tactic:
induction s with
  | nil => simp
  | cons y s IH => simpa using IH

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l
⊢ l.prev x h ∈ l

Tactic:
rcases l with - | ⟨hd, tl⟩
  · simp at h
  induction tl generalizing hd with
  | nil => simp
  | cons hd' tl hl =>
    by_cases hx : x = hd
    · simp only [hx, prev_cons_cons_eq]
      exact mem_cons_of_mem _ (getLast_mem _)
    · rw [prev, dif_neg hx]
      split_ifs with hm
      · exact mem_cons_self
      · exact mem_cons_of_mem _ (hl _ _)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : { s // s.Nodup }
s : Cycle α
hs : s.Nodup
⊢ ∃ a, (fun l ↦ ⟨↑↑l, ⋯⟩) a = ⟨s, hs⟩

Tactic:
by
    induction s using Quotient.inductionOn' with | _ hs
    exact ⟨⟨_, hs⟩, by simp⟩

Goal state after:
Module: Mathlib.GroupTheory.Index

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

Tactic:
rw [← relIndex_mul_index (show H ≤ ⊤ from le_top), index_top, mul_one]

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

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

Tactic:
by
  subst hab
  cases a <;> rfl

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

Goal state before:
pp: n : ℕ
⊢ (Int.castAddHom (ZMod n)).ker = AddSubgroup.zmultiples ↑n

Tactic:
by
  ext
  rw [Int.mem_zmultiples_iff, AddMonoidHom.mem_ker, Int.coe_castAddHom,
    intCast_zmod_eq_zero_iff_dvd]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

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

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
n : ℕ
h : 0 ∈ n.divisors
⊢ 0 < 0

pp: case succ
n n✝ : ℕ
h : n✝ + 1 ∈ n.divisors
⊢ 0 < n✝ + 1

Tactic:
· rw [mem_divisors, zero_dvd_iff (a := n)] at h
    cases h.2 h.1

Goal state after:
case succ
n n✝ : ℕ
h : n✝ + 1 ∈ n.divisors
⊢ 0 < n✝ + 1
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
mul_val_inv hmn

Goal state after:
m n : ℕ
hmn : m.Coprime n
⊢ 1 = 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n.properDivisors = {1}
m : ℕ
⊢ m < n → m ∣ n → m = 1

Tactic:
hm

Goal state after:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hm : m < n
⊢ m ∣ n → m = 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ofDigits b (hd :: tl ++ l2) = ↑hd + b * ofDigits b tl + b ^ (hd :: tl).length * ofDigits b l2

Tactic:
List.cons_append,

Goal state after:
case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ofDigits b (hd :: (tl ++ l2)) = ↑hd + b * ofDigits b tl + b ^ (hd :: tl).length * ofDigits b l2
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d :: b.digits (ofDigits b L) = d :: L

Tactic:
rw [ih]
      · intro l m
        apply w₁
        exact List.mem_cons_of_mem _ m
      · intro h
        rw [List.getLast_cons h] at w₂
        convert! w₂

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

Goal state before:
pp: case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ padicValNat p n * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
padicValNat,

Goal state after:
case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (ofDigits b) ↑(fixedLengthDigits hb l) ↑(Finset.range (b ^ l))

Tactic:
rw [fixedLengthDigits, Set.coe_toFinset]

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (ofDigits b) {L | L.length = l ∧ ∀ x ∈ L, x < b} ↑(Finset.range (b ^ l))
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (b.digitsAppend l) ↑(Finset.range (b ^ l)) ↑(fixedLengthDigits hb l)

Tactic:
rw [fixedLengthDigits, Set.coe_toFinset]

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (b.digitsAppend l) ↑(Finset.range (b ^ l)) {L | L.length = l ∧ ∀ x ∈ L, x < b}
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ↑(fixedLengthDigits hb l).card * (b * (b - 1) / 2) + ↑b * (l * b ^ (l - 1) * b.choose 2) =
    (l + 1) * b ^ l * b.choose 2

Tactic:
cast_id,

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ (fixedLengthDigits hb l).card * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * b.choose 2) = (l + 1) * b ^ l * b.choose 2
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization + d.factorization = n.factorization - d.factorization + d.factorization

Tactic:
rw [tsub_add_cancel_of_le <| (Nat.factorization_le_iff_dvd hd hn).mpr h, ←
    Nat.factorization_mul (Nat.div_pos (Nat.le_of_dvd hn.bot_lt h) hd.bot_lt).ne' hd,
    Nat.div_mul_cancel h]

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

Goal state before:
pp: case inr.inr.inl
b p : ℕ
pp : Prime p
hb0 : b ≠ 0
hab : 0 ∣ b
⊢ 0 / p ^ (factorization 0) p ∣ b / p ^ b.factorization p

pp: case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
· cases hb0 (zero_dvd_iff.1 hab)

Goal state after:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ 0 - (k ! * (n - k)!).factorization p = 0

Tactic:
zero_tsub

Goal state after:
case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ 0 = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : (fun n ↦ x ^ n) n = (fun n ↦ x ^ n) m
⊢ n = m

Tactic:
rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, modEq_zero_iff] at hnm

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ (n - m) = 1

Tactic:
rw [← mul_left_cancel_iff (a := a ^ m), ← pow_add, add_tsub_cancel_of_le hmn.le, ha, mul_one]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
⊢ m ∈ Ico (p * n + 1) (p * (n + 1)) → emultiplicity p m = 0

Tactic:
hm

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ emultiplicity p m = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1

Tactic:
dvd_neg,

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ ↑i ↔ x ^ (-↑i) = 1
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : NoZeroDivisors R
inst✝¹ : Nontrivial R
inst✝ : Finite R
⊢ Nat.Prime (ringChar R)

Tactic:
apply CharP.char_prime_of_ne_zero R

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : NoZeroDivisors R
inst✝¹ : Nontrivial R
inst✝ : Finite R
⊢ ringChar R ≠ 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
k : ℕ
⊢ (↑k).gcd ↑(orderOf g) = 1 ↔ k.gcd (orderOf g) = 1

Tactic:
Int.gcd_natCast_natCast

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
k : ℕ
⊢ k.gcd (orderOf g) = 1 ↔ k.gcd (orderOf g) = 1