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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁)) 1 *
      single (Multiplicative.toAdd (Multiplicative.ofAdd m₂)) 1 =
    (of R M) (Multiplicative.ofAdd (m₁ + m₂))

Tactic:
of_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁)) 1 *
      single (Multiplicative.toAdd (Multiplicative.ofAdd m₂)) 1 =
    single (Multiplicative.toAdd (Multiplicative.ofAdd (m₁ + m₂))) 1
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ (of R M) (Multiplicative.ofAdd m₁) * (of R M) (Multiplicative.ofAdd m₂) = (of R M) (Multiplicative.ofAdd (m₁ + m₂))

Tactic:
of_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁)) 1 * (of R M) (Multiplicative.ofAdd m₂) =
    (of R M) (Multiplicative.ofAdd (m₁ + m₂))
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁)) 1 * (of R M) (Multiplicative.ofAdd m₂) =
    (of R M) (Multiplicative.ofAdd (m₁ + m₂))

Tactic:
of_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁)) 1 *
      single (Multiplicative.toAdd (Multiplicative.ofAdd m₂)) 1 =
    (of R M) (Multiplicative.ofAdd (m₁ + m₂))
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁)) 1 *
      single (Multiplicative.toAdd (Multiplicative.ofAdd m₂)) 1 =
    (of R M) (Multiplicative.ofAdd (m₁ + m₂))

Tactic:
of_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁)) 1 *
      single (Multiplicative.toAdd (Multiplicative.ofAdd m₂)) 1 =
    single (Multiplicative.toAdd (Multiplicative.ofAdd (m₁ + m₂))) 1
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ (of R M) m₁ * (of R M) m₂ = (of R M) (m₁ * m₂)

Tactic:
of_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single m₁ 1 * (of R M) m₂ = (of R M) (m₁ * m₂)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single m₁ 1 * (of R M) m₂ = (of R M) (m₁ * m₂)

Tactic:
of_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single m₁ 1 * single m₂ 1 = (of R M) (m₁ * m₂)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single m₁ 1 * single m₂ 1 = (of R M) (m₁ * m₂)

Tactic:
of_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single m₁ 1 * single m₂ 1 = single (m₁ * m₂) 1
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ (of R M) m₁ * (of R M) m₂ = (of R M) (m₁ * m₂)

Tactic:
of_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single m₁ 1 * (of R M) m₂ = (of R M) (m₁ * m₂)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single m₁ 1 * (of R M) m₂ = (of R M) (m₁ * m₂)

Tactic:
of_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single m₁ 1 * single m₂ 1 = (of R M) (m₁ * m₂)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single m₁ 1 * single m₂ 1 = (of R M) (m₁ * m₂)

Tactic:
of_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single m₁ 1 * single m₂ 1 = single (m₁ * m₂) 1
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) p).ker ⊔ ((aeval f) q).ker
x : M
hx : x ∈ ((aeval f) p).ker
y : M
hy : y ∈ ((aeval f) q).ker
hxy : x + y = v
h_eval_x : ((aeval f) (p * q)) x = 0
⊢ ((aeval f) p) (((aeval f) q) y) = 0

Tactic:
LinearMap.mem_ker.1 hy,

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) p).ker ⊔ ((aeval f) q).ker
x : M
hx : x ∈ ((aeval f) p).ker
y : M
hy : y ∈ ((aeval f) q).ker
hxy : x + y = v
h_eval_x : ((aeval f) (p * q)) x = 0
⊢ ((aeval f) p) 0 = 0
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_1.mem.inr
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x : ↥N
j j' : Fin k
x✝ : j' ∈ Finset.univ
c' : ↥A := ⟨c j j', ⋯⟩
⊢ c j j' • mj j' ∈ M'

Tactic:
show c j j' • mj j' = c' • mj j' from rfl

Goal state after:
case refine_1.mem.inr
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x : ↥N
j j' : Fin k
x✝ : j' ∈ Finset.univ
c' : ↥A := ⟨c j j', ⋯⟩
⊢ c' • mj j' ∈ M'
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
⊢ ∀ i ∈ d.support, ((fun n e ↦ f n ^ e) i (d i)).natDegree ≤ d i * n

Tactic:
rintro i -

Goal state after:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
i : σ
⊢ ((fun n e ↦ f n ^ e) i (d i)).natDegree ≤ d i * n
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

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

Tactic:
← RingHom.comap_ker,

Goal state after:
R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
⊢ map (Quotient.mk J) (comap (Quotient.mk I) (ker (Quotient.mk (map (Quotient.mk I) J)))) = map (Quotient.mk J) I
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 =
    flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r

Tactic:
induction L with
  | nil => rfl
  | cons l L ih => simp_rw [foldr_cons, ih, flatMap_cons, append_assoc, permutationsAux2_append]

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

Goal state before:
pp: α : Type u_1
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → l.length = n
⊢ (foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r L).length = n * L.length + r.length

Tactic:
rw [length_foldr_permutationsAux2, (_ : (map length L).sum = n * length L)]
  induction L with
  | nil => simp
  | cons l L ih =>
    have sum_map : (map length L).sum = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)
    have length_l : length l = n := H _ mem_cons_self
    simp [sum_map, length_l, Nat.add_comm, mul_succ]

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

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
| g ^ (j % ↑(period g a)) • g ^ (↑(period g a) * (j / ↑(period g a))) • a

Tactic:
zpow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
| g ^ (j % ↑(period g a)) • a
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case refine_5
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✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : StarRing B
inst✝³ : StarModule R A
s : Set A
inst✝² : FunLike F (↥(adjoin R s)) B
inst✝¹ : AlgHomClass F R (↥(adjoin R s)) B
inst✝ : StarHomClass F (↥(adjoin R s)) B
f g : F
h : ∀ (x : ↥(adjoin R s)), ↑x ∈ s → f x = g x
a x : ↥(adjoin R s)
hx : f x = g x
⊢ f (star x) = g (star x)

Tactic:
simp only [map_star, hx]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (hd :: tl)[(n + ((hd :: tl).length - 1) + 1) % (hd :: tl).length] = (hd :: tl)[n]

Tactic:
have : (n + length tl + 1) % (length tl + 1) = n := by
      rw [length_cons] at hn
      rw [add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
    simp [this]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : x = y
⊢ (↑(x :: y :: l)).Nontrivial ↔ (↑(x :: l)).Nontrivial

Tactic:
simp [h, Nontrivial]

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

Goal state before:
pp: case inr
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
⊢ Finite (orbitRel.Quotient (↥H) X)

Tactic:
have h' : Finite (Quotient (rightRel H)) :=
      Finite.of_equiv _ (quotientRightRelEquivQuotientLeftRel _).symm

Goal state after:
case inr
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
h' : Finite (Quotient (rightRel H))
⊢ Finite (orbitRel.Quotient (↥H) X)
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p.primeFactors = {p}

Tactic:
by
  simp [Nat.primeFactors, primeFactorsList_prime hp]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.relIndex K = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H

Tactic:
by
  rw [Subgroup.relIndex, Subgroup.index_eq_two_iff_exists_notMem_and]
  simp only [mem_subgroupOf, coe_mul, Subtype.forall, Subtype.exists, exists_and_left, exists_prop]
  refine exists_congr fun g ↦ ?_
  simp only [and_left_comm]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hlt : 0 < n
hle : n ≤ (H.subgroupOf K).index
he : ⟨a, ha⟩ ^ n ∈ H.subgroupOf K
⊢ a ^ n ∈ H ⊓ K

Tactic:
simpa [pow_mem ha, mem_subgroupOf] using he

Goal state after:
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: case succ
R✝ : Type u_1
inst✝² : Ring R✝
R : Type u_2
inst✝¹ : Ring R
x : R
n : ℕ
inst✝ : Module (ZMod (n + 1)) R
r : ZMod (n + 1)
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x

Tactic:
obtain ⟨r, rfl⟩ := ZMod.natCast_zmod_surjective r
      simp [Nat.cast_smul_eq_nsmul, Nat.cast_comm]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0

Tactic:
· 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: n : ℤ
⊢ n ≡ 1 [ZMOD ↑2] ↔ Odd n

Tactic:
Int.odd_iff,

Goal state after:
n : ℤ
⊢ n ≡ 1 [ZMOD ↑2] ↔ n % 2 = 1
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
h : Odd n
⊢ 0 < ∑ i ∈ range n, x ^ i

Tactic:
rcases n with (_ | _ | k)

Goal state after:
case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
h : Odd 0
⊢ 0 < ∑ i ∈ range 0, x ^ i

case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
h : Odd (0 + 1)
⊢ 0 < ∑ i ∈ range (0 + 1), x ^ i

case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
k : ℕ
h : Odd (k + 1 + 1)
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Even n → ¬x + 1 ≤ 0

Tactic:
refine fun hn hx => h.not_ge ?_

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn✝ : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
hn : Even n
hx : x + 1 ≤ 0
⊢ ∑ i ∈ range n, x ^ i ≤ 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ ∑ i ∈ Ico 1 0, a / b ^ i ≤ a / (b - 1)

Tactic:
rw [Ico_eq_empty_of_le (by lia), sum_empty]
    exact Nat.zero_le _

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

Goal state before:
pp: case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₁ : ↑n = ↑k
H₂ : k ≤ n
⊢ ∃ y, n = k + m * y

Tactic:
obtain ⟨a, ha⟩ := le_iff_exists_add.mp H₂
    simp only [ha, Nat.cast_add, add_eq_left, ZMod.natCast_eq_zero_iff] at H₁
    obtain ⟨b, rfl⟩ := H₁
    exact ⟨b, ha⟩

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

Goal state before:
pp: case succ.zero.succ
n : ℕ
ih : ofDigits (0 + 1) ((0 + 1).digits n) = n
⊢ ofDigits (0 + 1) ((0 + 1).digits (n + 1)) = n + 1

Tactic:
rw [Nat.zero_add] at ih ⊢

Goal state after:
case succ.zero.succ
n : ℕ
ih : ofDigits 1 (digits 1 n) = n
⊢ ofDigits 1 (digits 1 (n + 1)) = n + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ l ∈ tl, l < p) → ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p (hd :: tl) / p = ofDigits p (hd :: tl).tail

Tactic:
refine Eq.trans (add_mul_div_left hd _ hpos) ?_

Goal state after:
case cons
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ l ∈ tl, l < p) → ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd / p + ofDigits p tl = ofDigits p (hd :: tl).tail
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n ≤ emultiplicity a b
⊢ n ≤ multiplicity a b

Tactic:
rw [emultiplicity_eq_multiplicity hfin] at h

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n ≤ ↑(multiplicity a b)
⊢ n ≤ multiplicity a b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n < emultiplicity a b
⊢ n < multiplicity a b

Tactic:
rw [emultiplicity_eq_multiplicity hfin] at h

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n < ↑(multiplicity a b)
⊢ n < multiplicity a b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
⊢ emultiplicity ↑a ↑b = emultiplicity a b

Tactic:
unfold emultiplicity FiniteMultiplicity
  congr! <;> norm_cast

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ ¬a ^ m ∣ b

Tactic:
by
  apply not_pow_dvd_of_emultiplicity_lt
  rw [hf.emultiplicity_eq_multiplicity]
  norm_cast

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case convert_2
G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ orderOf x = (fun x_1 ↦ x * x_1)^[minimalPeriod (fun x_1 ↦ x * x_1) 1] 1

Tactic:
orderOf,

Goal state after:
case convert_2
G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ minimalPeriod (fun x_1 ↦ x * x_1) 1 = (fun x_1 ↦ x * x_1)^[minimalPeriod (fun x_1 ↦ x * x_1) 1] 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : ¬IsOfFinOrder x
⊢ orderOf x = 0

Tactic:
orderOf,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
h : ¬IsOfFinOrder x
⊢ minimalPeriod (fun x_1 ↦ x * x_1) 1 = 0