mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * X i ^ k) = degreeOf i p + k
s : σ →₀ ℕ
hs : coeff s p ≠ 0
⊢ p * X i ^ k ≠ 0

Tactic:
refine ne_zero_iff.mpr ⟨s + Finsupp.single i k, ?_⟩

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * X i ^ k) = degreeOf i p + k
s : σ →₀ ℕ
hs : coeff s p ≠ 0
⊢ coeff (s + Finsupp.single i k) (p * X i ^ k) ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
e : ℕ
r : R
he : e ≠ 0
hr : r ≠ 0
⊢ ((monomial (Finsupp.single i e)) r).vars = {i}

Tactic:
rw [vars_monomial hr, Finsupp.support_single _ he]

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: case neg
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : ¬a = 0
⊢ (cons (t 0) t.tail) (a.pred c_a).succ = t (a.pred c_a).succ

Tactic:
cons_succ,

Goal state after:
case neg
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : ¬a = 0
⊢ t.tail (a.pred c_a) = t (a.pred c_a).succ
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
⊢ degreeOf i (p * X j ^ 0) = degreeOf i p

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i j : σ
h : i ≠ j
⊢ degreeOf i (p * 1) = degreeOf i p
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a b : MvPolynomial σ R
x✝¹ x✝ : σ →₀ ℕ
⊢ ((x✝¹ + x✝).sum fun x e ↦ e) ≤ (x✝¹.sum fun x e ↦ e) + x✝.sum fun x e ↦ e

Tactic:
simp [Finsupp.sum_add_index']

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.eraseLead.support = f.support.erase f.natDegree

Tactic:
by
  simp only [eraseLead, support_erase]

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
x : S₁
⊢ (optionEquivLeft R S₁) (X (Option.some x)) = Polynomial.C (X x)

Tactic:
by
  simp [optionEquivLeft_apply, aeval_X]

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
⊢ (optionEquivLeft R S₁) (X none) = Polynomial.X

Tactic:
by
  simp [optionEquivLeft_apply, aeval_X]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
⊢ (comp 0 (-X)).degree = degree 0

Tactic:
rw [zero_comp]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : p.degree < q.degree
⊢ (p + q).Monic

Tactic:
by
  rwa [Monic, leadingCoeff_add_of_degree_lt hpq]

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ (p ^ 0).nextCoeff = 0 • p.nextCoeff

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ nextCoeff 1 = 0 • p.nextCoeff
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
⊢ y ^ 0 = (x + y) ^ 0

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
⊢ 1 = (x + y) ^ 0
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (x + y) ^ n * y ^ 0 = (x + y) ^ n

Tactic:
pow_zero,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (x + y) ^ n * 1 = (x + y) ^ n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (¬∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (2 / 2)) ↔
    ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Tactic:
push Not

Goal state after:
case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (∃ f g, f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)) ↔
    ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : b = 0
⊢ r ^ 0 ^ a - r ∣ r ^ 0 ^ 0 - r

Tactic:
pow_zero,

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : b = 0
⊢ r ^ 0 ^ a - r ∣ r ^ 1 - r
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ (Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) s)).sum = s.card

pp: case h
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) s, f.Monic

Tactic:
Multiset.map_map

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ (Multiset.map (natDegree ∘ fun x ↦ X - C x) s).sum = s.card

case h
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) s, f.Monic
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ x ^ n * y ^ 0 + ∑ i ∈ range n, x ^ i * y ^ (n - i) = x ^ n + ∑ i ∈ range n, y * (x ^ i * y ^ (n - 1 - i))

Tactic:
pow_zero,

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ x ^ n * 1 + ∑ i ∈ range n, x ^ i * y ^ (n - i) = x ^ n + ∑ i ∈ range n, y * (x ^ i * y ^ (n - 1 - i))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬∃ S, S.Finite ∧ Submodule.span R S = ⊤

Tactic:
push Not

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ∀ (S : Set R[X]), S.Finite → Submodule.span R S ≠ ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case empty
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ ∅, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (if k = 0 then 1 else 0) ∈ I ^ 0

Tactic:
pow_zero,

Goal state after:
case empty
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ ∅, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (if k = 0 then 1 else 0) ∈ 1
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ (Ideal.span {C r}).IsPrime

pp: R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ C r ≠ 0

pp: R : Type u
inst✝ : CommRing R
r : R
hr : Prime r
this : r ≠ 0
⊢ r ≠ 0

Tactic:
· rw [← Set.image_singleton, ← Ideal.map_span]
      infer_instance

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ C r ≠ 0

R : Type u
inst✝ : CommRing R
r : R
hr : Prime r
this : r ≠ 0
⊢ r ≠ 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
hr : Prime r
⊢ Prime (C r)

Tactic:
by
    have := hr.1
    rw [← Ideal.span_singleton_prime] at hr ⊢
    · rw [← Set.image_singleton, ← Ideal.map_span]
      infer_instance
    · intro h; apply (this (C_eq_zero.mp h))
    · assumption

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

Goal state before:
pp: case h.inl
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : k ≤ N
⊢ p ∈ Ideal.span ↑s

Tactic:
subst k

Goal state after:
case h.inl
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
p : R[X]
hp : p ∈ I
ih : ∀ m < p.natDegree, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
h : p.natDegree ≤ N
⊢ p ∈ Ideal.span ↑s
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_1.mem.inl
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✝ x : ↥N
hx : x = n
⊢ i n ∈ M'

Tactic:
← hb,

Goal state after:
case refine_1.mem.inl
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✝ x : ↥N
hx : x = n
⊢ ((Module.piEquiv (Fin k) R M) mj) b ∈ M'
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 * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
h_eval₂_pqq' : ((aeval f) (p * (q * q'))) v = 0
⊢ ∃ y ∈ ((aeval f) p).ker, ∃ z ∈ ((aeval f) q).ker, y + z = v

Tactic:
rw [aeval_mul] at h_eval₂_qpp' h_eval₂_pqq'

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 * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) q * (aeval f) (p * p')) v = 0
h_eval₂_pqq' : ((aeval f) p * (aeval f) (q * q')) v = 0
⊢ ∃ y ∈ ((aeval f) p).ker, ∃ z ∈ ((aeval f) q).ker, y + z = v
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hy : y ∈ ker f ∧ (Quotient.mk I) y = x
⊢ (Quotient.lift I f H) x = 0

Tactic:
← hy.right,

Goal state after:
case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hy : y ∈ ker f ∧ (Quotient.mk I) y = x
⊢ (Quotient.lift I f H) ((Quotient.mk I) y) = 0
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ ¬∃ p, Prime p ∧ p ∣ n ∧ p ∣ m

Tactic:
push Not

Goal state after:
n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ ∀ (p : ℕ), Prime p → p ∣ n → ¬p ∣ m
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S : Type v
inst✝² : Ring S
J : Ideal R
I : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
hf : Surjective ⇑f
x✝ : S ⧸ I
x : S
hx : (Quotient.mk I) x = x✝
y : R
hy : f y = x
⊢ (quotientMap I f H) ((Quotient.mk J) y) = x✝

Tactic:
simp [hx, hy]

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

Goal state before:
pp: 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
ι : Sort u_5
inst✝ : Nonempty ι
f : A →⋆ₐ[R] B
hf : Function.Injective ⇑f
s : ι → StarSubalgebra R A
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Goal state after:
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
ι : Sort u_5
inst✝ : Nonempty ι
f : A →⋆ₐ[R] B
hf : Function.Injective ⇑f
s : ι → StarSubalgebra R A
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₁ = l₂ ↔ decide (l₁ = l₂) = true

Tactic:
decide_eq_true_iff

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₁ = l₂ ↔ l₁ = l₂
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : l.Nodup
h✝ : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
⊢ False

Tactic:
obtain ⟨_ | k, hk, hk'⟩ := getElem_of_mem H

Goal state after:
case h.zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : l.Nodup
h✝ : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
hk : 0 < (y :: l).dropLast.length
hk' : (y :: l).dropLast[0] = (y :: l).getLast ⋯
⊢ False

case h.succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : l.Nodup
h✝ : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
k : ℕ
hk : k + 1 < (y :: l).dropLast.length
hk' : (y :: l).dropLast[k + 1] = (y :: l).getLast ⋯
⊢ False
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ k = k.succ

Tactic:
rw [← @Fin.mk.inj_iff _ _ _ kl k1l]

Goal state after:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ ⟨k, kl⟩ = ⟨k + 1, k1l⟩
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.left
α : 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
ys : List α
hy : ys ~ l
⊢ (permutations'Aux x ys).Nodup

Tactic:
nodup_permutations'Aux_iff,

Goal state after:
case cons.left
α : 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
ys : List α
hy : ys ~ l
⊢ ¬x ∈ ys
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 + 1 + ((hd :: tl).length - 1)) % (hd :: tl).length] = (hd :: tl)[n]

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

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

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

Tactic:
rw [add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt hn]

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

Goal state before:
pp: α : Type u_1
x y : α
s : List α
⊢ take 2 (x :: y :: s).permutations = [x :: y :: s, y :: x :: s]

Tactic:
by
  induction s <;> simp [permutations]

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p ≤ p ^ k

Tactic:
{

Goal state after:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p ≤ p ^ k
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G✝ : Type u
X : Type v
inst✝² : Group G✝
inst✝¹ : MulAction G✝ X
x : X
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (x y : G ⧸ H), ∃ g, g • x = y

Tactic:
{

Goal state after:
G✝ : Type u
X : Type v
inst✝² : Group G✝
inst✝¹ : MulAction G✝ X
x : X
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (x y : G ⧸ H), ∃ g, g • x = y
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ H.relIndex (K ⊓ L) * K.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.relIndex L = (H ⊓ K).relIndex L
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
⊢ cast 1 = 1

pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ n + 1
⊢ cast 1 = 1

Tactic:
· exact Int.cast_one

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ n + 1
⊢ cast 1 = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0 + 1
⊢ ↑(1 % (0 + 1)) = 1

Tactic:
rw [Nat.dvd_one] at h

Goal state after:
case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m = 1
⊢ ↑(1 % (0 + 1)) = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0 + 1
⊢ ↑(1 % (0 + 1)) = 1

pp: case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑(1 % (n✝ + 1 + 1)) = 1

Tactic:
· rw [Nat.dvd_one] at h
    subst m
    subsingleton [CharP.CharOne.subsingleton]

Goal state after:
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑(1 % (n✝ + 1 + 1)) = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ℤ
inst✝ : NeZero n
⊢ ↑(↑a).val = a % ↑n

Tactic:
have hle : (0 : ℤ) ≤ ↑(a : ZMod n).val := Int.natCast_nonneg _
  have hlt : ↑(a : ZMod n).val < (n : ℤ) := Int.ofNat_lt.mpr (ZMod.val_lt a)
  refine (Int.emod_eq_of_lt hle hlt).symm.trans ?_
  rw [← ZMod.intCast_eq_intCast_iff', Int.cast_natCast, ZMod.natCast_val, ZMod.cast_id]

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

Goal state before:
pp: n : ℕ
inst✝ : Fact (1 < n)
⊢ val 1 = 1

Tactic:
rw [val_one_eq_one_mod]

Goal state after:
n : ℕ
inst✝ : Fact (1 < n)
⊢ 1 % n = 1
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
n m : ℕ
inst✝ : CharP R m
h : m ∣ n
a : ZMod n
r : R
⊢ a.cast * r = r * a.cast

Tactic:
rcases ZMod.intCast_surjective a with ⟨k, rfl⟩
      change ZMod.castHom h R k * r = r * ZMod.castHom h R k
      rw [map_intCast, Int.cast_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∣ m → n ≤ m

Tactic:
exact le_of_dvd hm.bot_lt

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

Goal state before:
pp: case zero
a : ℤ
⊢ a * a⁻¹ = ↑((val a).gcd 0)

Tactic:
calc
      _ = a * Int.sign a := rfl
      _ = a.natAbs := by rw [Int.mul_sign_self]
      _ = a.natAbs.gcd 0 := by rw [Nat.gcd_zero_right]

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

Goal state before:
pp: a b n : ℕ
⊢ ∑ k ∈ range n, a / b ^ (k + 1) * b + a / b ^ 0 * b - (∑ x ∈ range n, a / b ^ x + a / b ^ n) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)

Tactic:
pow_zero,

Goal state after:
a b n : ℕ
⊢ ∑ k ∈ range n, a / b ^ (k + 1) * b + a / 1 * b - (∑ x ∈ range n, a / b ^ x + a / b ^ n) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
Module: Mathlib.Algebra.Order.Ring.GeomSum

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

Tactic:
pow_zero,

Goal state after:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / 1 + ∑ i ∈ Ico 1 n.succ, a / b ^ i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
h : n ≤ m
⊢ a.cast.val < m + 1

Tactic:
apply lt_of_lt_of_le (ZMod.val_lt _) (le_trans h (Nat.le_succ m))

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

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
⊢ (a - b).val = a.val - b.val

Tactic:
have : NeZero b := ⟨hb⟩
    rw [sub_eq_add_neg, val_add, val_neg_of_ne_zero, ← Nat.add_sub_assoc (le_of_lt (val_lt _)),
      add_comm, Nat.add_sub_assoc h, Nat.add_mod_left]
    apply Nat.mod_eq_of_lt (tsub_lt_of_lt (val_lt _))

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

Goal state before:
pp: case zero
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
hxy : x ≠ 0 ∨ 0 ≠ 0
⊢ (b + 2).digits (x + (b + 2) * 0) = x :: (b + 2).digits 0

Tactic:
simp [hxb, hxy.resolve_right (absurd rfl)]

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

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

Tactic:
pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn

Goal state after:
case h₂
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ (p.maxPowDvdDiv n).fst ≤ padicValNat p n
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ (∀ (n : ℕ), a ^ n ∣ b) → ¬FiniteMultiplicity a b

Tactic:
simp [FiniteMultiplicity]; tauto

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n

Tactic:
rw [and_imp]
    apply emultiplicity_eq_of_dvd_of_not_dvd

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) = n

Tactic:
factorization_eq_primeFactorsList_multiset n

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ ((Multiset.toFinsupp ↑n.primeFactorsList).prod fun x1 x2 ↦ x1 ^ x2) = n
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ ¬(¬Prime n.minFac ∨ ¬n.minFac ∣ n ∨ n = 0)

Tactic:
push Not

Goal state after:
n : ℕ
hn : 1 < n
⊢ Prime n.minFac ∧ n.minFac ∣ n ∧ n ≠ 0