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

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ d.support.Nonempty

Tactic:
by
      rw [constantCoeff_eq, coeff, ← Finsupp.notMem_support_iff] at h0
      rw [Finset.nonempty_iff_ne_empty, Ne, Finsupp.support_eq_empty]
      rintro rfl
      contradiction

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N n : ℕ
⊢ reflect N (C 1 * X ^ n) = C 1 * X ^ (revAt N) n

Tactic:
reflect_C_mul_X_pow

Goal state after:
R : Type u_1
inst✝ : Semiring R
N n : ℕ
⊢ C 1 * X ^ (revAt N) n = C 1 * X ^ (revAt N) n
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : f.natDegree ≤ 1
⊢ f.eraseLead = 0

Tactic:
Nat.le_one_iff_eq_zero_or_eq_one,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : f.natDegree = 0 ∨ f.natDegree = 1
⊢ f.eraseLead = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ¬((X - C x) * P).eraseLead = 0
this : #((X - C x) * P).support ≤ 2
⊢ #((X - C x) * P).eraseLead.eraseLead.support = 0

Tactic:
linarith [eraseLead_support_card_lt he₂,
        eraseLead_support_card_lt (mul_ne_zero (X_sub_C_ne_zero x) hp)]

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

Goal state before:
pp: case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun x ↦ Polynomial.X) ((monomial d) r)) =
    eval₂ φ a ((monomial d) r)

Tactic:
← MvPolynomial.uniqueAlgEquiv_apply (R := R) (σ := σ),

Goal state after:
case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ Polynomial.eval₂ φ (a default) ((uniqueAlgEquiv R σ) ((monomial d) r)) = eval₂ φ a ((monomial d) r)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
⊢ C (eval (q.coeff 0) p) = 0

Tactic:
h.1,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
⊢ C 0 = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
hj : ¬j = n
hj_none : j none = n none
hj_some : j.some = n.some
⊢ r = 0

Tactic:
apply False.elim (hj _)

Goal state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
hj : ¬j = n
hj_none : j none = n none
hj_some : j.some = n.some
⊢ j = n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : q = C (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
rw [key, comp_C, C_eq_zero] at h

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : q = C (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ p.natDegree * X.natDegree = p.natDegree

Tactic:
natDegree_X,

Goal state after:
case inr
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ p.natDegree * 1 = p.natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
⊢ p = 1

Tactic:
by
  nontriviality R
  have hdeg : p.degree = 0 := by
    rw [← degree_map_eq_of_leadingCoeff_ne_zero f _, map_eq, degree_one]
    · rw [hp.leadingCoeff, f.map_one]
      exact one_ne_zero
  have hndeg : p.natDegree = 0 :=
    WithBot.coe_eq_coe.mp ((degree_eq_natDegree hp.ne_zero).symm.trans hdeg)
  convert! eq_C_of_degree_eq_zero hdeg
  rw [← hndeg, ← Polynomial.leadingCoeff, hp.leadingCoeff, C.map_one]

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

Goal state before:
pp: case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) (a ::ₘ t)).sum

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons,
      Monic.nextCoeff_mul, ih]
    exacts [fun i hi => ht i (Multiset.mem_cons_of_mem hi), ht a (Multiset.mem_cons_self _ _),
      monic_multiset_prod_of_monic _ _ fun b bs => ht _ (Multiset.mem_cons_of_mem bs)]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun x ↦ x) ∘ f = f
h₁ : ∀ {α : Type ?u.55} {β : Type ?u.57} (f : α → β), (f ∘ fun x ↦ x) = f
h' : (((finSuccEquiv R n) f).support.sup fun x ↦ x) = degreeOf 0 f
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)

Tactic:
rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (nonempty_support_finSuccEquiv h), Finset.max_eq_sup_coe, h₁]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : x ≤ y
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n

Tactic:
← Finset.sum_range_reflect

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : x ≤ y
n : ℕ
⊢ (∑ j ∈ range n, x ^ (n - 1 - j) * y ^ (n - 1 - (n - 1 - j))) * (y - x) = y ^ n - x ^ n
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
induction n with
  | zero => simp
  | succ k hk =>
    simp only [geom_sum_succ', Nat.even_add_one, hk]
    split_ifs with h
    · rw [h.neg_one_pow, add_zero]
    · rw [(Nat.not_even_iff_odd.1 h).neg_one_pow, neg_add_cancel]

Goal state after:
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 - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = -(y ^ n - x ^ n)

Tactic:
← h.mul_neg_geom_sum₂,

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
⊢ f ∈ map C I

Tactic:
← sum_monomial_eq f

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
⊢ (f.sum fun n a ↦ (monomial n) a) ∈ map C I
Module: Mathlib.Algebra.Algebra.Subalgebra.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := ⋯
l' : ι → ↥S' := ⋯
⊢ ↑(∑ i ∈ ι', l' i * s' i) = ↑1

Tactic:
change S'.subtype (∑ i ∈ ι', l' i * s' i) = 1

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun x ↦ ⟨s x, ⋯⟩
l' : ι → ↥S' := fun x ↦ ⟨l x, ⋯⟩
⊢ S'.subtype (∑ i ∈ ι', l' i * s' i) = 1
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
p : Ideal R
x : R
hx : x ∈ p
⊢ x ∈ (map C p).leadingCoeff

Tactic:
exact ((map C p).mem_leadingCoeff x).2 ⟨C x, mem_map_of_mem C hx, leadingCoeff_C x⟩

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

Goal state before:
pp: case refine_1
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K
⊢ finrank F ↥K = 1 → K = ⊥

pp: case refine_2
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K
h : finrank F ↥K = finrank F A
⊢ K = ⊤

Tactic:
· exact fun h' => Subalgebra.eq_bot_of_finrank_one h'

Goal state after:
case refine_2
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K
h : finrank F ↥K = finrank F A
⊢ K = ⊤
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b n : ℤ
⊢ n ∣ b - a ↔ ∃ t, b = a + n * t

Tactic:
exact exists_congr fun t => sub_eq_iff_eq_add'

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

Goal state before:
pp: n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
⊢ a ≡ b [ZMOD n]

Tactic:
by
  rw [add_comm a, add_comm b] at h₂
  exact h₁.add_left_cancel h₂

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

Goal state before:
pp: p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
⊢ a ^ k = p

Tactic:
h.1,

Goal state after:
p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
⊢ p ^ k = p
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Surjective ⇑f
g : A →ₐ[R] C
H : ker f.toRingHom ≤ ker g.toRingHom
x : A
⊢ (f.liftOfSurjective hf g H) (f x) = g x

Tactic:
by
  dsimp [AlgHom.liftOfSurjective]
  erw [AlgEquiv.coe_toAlgHom] -- fixed after #21031
  rw [Ideal.quotientKerAlgEquivOfSurjective_symm_apply]
  rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ J ⊔ I = I ⊔ J

Tactic:
sup_comm

Goal state after:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ I ⊔ J = I ⊔ J
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
a : A
ha : a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))
⊢ a ∈ Algebra.adjoin R (star (↑S ⊔ ↑(star S)))

Tactic:
sup_comm

Goal state after:
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
a : A
ha : a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))
⊢ a ∈ Algebra.adjoin R (star (↑(star S) ⊔ ↑S))
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
⊢ Subalgebra.toSubmodule (adjoin R s).toSubalgebra = span R ↑(Submonoid.closure (s ∪ star s))

Tactic:
rw [adjoin_toSubalgebra, Algebra.adjoin_eq_span]

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

Goal state before:
pp: case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
⊢ (permutationsAux2 t ts (flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
    (permutationsAux2 t ts [] l id).snd ++ flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r

Tactic:
append_assoc,

Goal state after:
case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
⊢ (permutationsAux2 t ts (flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
    (permutationsAux2 t ts [] l id).snd ++ (flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r)
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f^[n] ∘ g^[n]) x

Tactic:
exact IsFixedPt.comp hf hg

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

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
IH : x ∈ [].dropLast → [].nextOr x d = [].nextOr x d'
x_mem : x ∈ [y].dropLast
⊢ [y].nextOr x d = [y].nextOr x d'

pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
· simp at x_mem

Goal state after:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ n • a = a ↔ IsPeriodicPt (fun x ↦ m • x) n a

Tactic:
isPeriodicPt_smul_iff

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ n • a = a ↔ m ^ n • a = a
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case succ
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
⊢ ts.permutations ~ ts.permutations'

Tactic:
| succ n IH =>

Goal state after:
case succ
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
⊢ ts.permutations ~ ts.permutations'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : x = y
⊢ z ∈ xs'

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : ¬x = y
⊢ (z :: zs).nextOr x d ∈ xs'

Tactic:
· exact hxs' _ (mem_cons_of_mem _ mem_cons_self)

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : ¬x = y
⊢ (z :: zs).nextOr x d ∈ xs'
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
x : α
n : ℕ
hn : n < (permutations'Aux x []).length
⊢ (permutations'Aux x [])[n] = [].insertIdx n x

Tactic:
simp only [permutations'Aux, length, Nat.zero_add, lt_one_iff] at hn
    simp [hn]

Goal state after:
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
hl : (s.insertIdx k x).length = (s.insertIdx (k + 1) x).length
⊢ s.insertIdx k x = s.insertIdx (k + 1) x

Tactic:
exact ext_get hl fun n hn hn' => by grind

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ (if hx : x = hd then (hd' :: tl).getLast ⋯ else if x = hd' then hd else (hd' :: tl).prev x ⋯) ∈ hd :: hd' :: tl

Tactic:
dif_neg hx

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ (if x = hd' then hd else (hd' :: tl).prev x ⋯) ∈ hd :: hd' :: tl
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ (l.rotate (Nat.succ 0)).reverse.reverse[(l.rotate (Nat.succ 0)).reverse.length - 1 - (l.length - 1 - k)] =
    (l.rotate 1)[k]

Tactic:
simp [Nat.sub_sub_self (Nat.le_sub_one_of_lt hk)]

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

Goal state before:
pp: α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)
l : List α
⊢ motive (Quotient.mk'' l)

Tactic:
refine List.recOn l ?_ ?_ <;> simp only [mk''_eq_coe, coe_nil]
    assumption'

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

Goal state before:
pp: k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
⊢ (k + 2).minFac * ((k + 2) / (k + 2).minFac).primeFactorsList.prod = k + 2

Tactic:
prod_primeFactorsList h₁,

Goal state after:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
⊢ (k + 2).minFac * ((k + 2) / m) = k + 2
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : G ⧸ H
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ H
⊢ ⟦g₁⁻¹ • x⟧ = ⟦g₂⁻¹ • x⟧

Tactic:
← @Quotient.mk''_eq_mk,

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : G ⧸ H
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ H
⊢ Quotient.mk'' (g₁⁻¹ • x) = Quotient.mk'' (g₂⁻¹ • x)
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case h
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
a✝ : X
⊢ ⟦⋯.choose⁻¹ • x⟧ = Quotient.mk'' a✝

Tactic:
← @Quotient.mk''_eq_mk,

Goal state after:
case h
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
a✝ : X
⊢ Quotient.mk'' (⋯.choose⁻¹ • x) = Quotient.mk'' a✝
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p a b : ℕ
hpa : p ∈ a.primeFactorsList
hb : b ≠ 0
⊢ p ∈ (a * b).primeFactorsList

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Goal state after:
case inl
p b : ℕ
hb : b ≠ 0
hpa : p ∈ primeFactorsList 0
⊢ p ∈ (0 * b).primeFactorsList

case inr
p a b : ℕ
hpa : p ∈ a.primeFactorsList
hb : b ≠ 0
ha : a ≠ 0
⊢ p ∈ (a * b).primeFactorsList
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ ∀ (x : ℕ), ↑x = 0 ↔ n ∣ x

Tactic:
by
    intro k
    rcases n with - | n
    · simp
    · exact Fin.natCast_eq_zero

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index ∣ 2
this : H.index ≤ 1 ∨ H.index = Nat.succ 1
⊢ H.index = 1 ∨ H.index = 2

Tactic:
Nat.le_one_iff_eq_zero_or_eq_one,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index ∣ 2
this : (H.index = 0 ∨ H.index = 1) ∨ H.index = Nat.succ 1
⊢ H.index = 1 ∨ H.index = 2
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b - (n + 1)) = cast a + cast b - ↑(n + 1)

Tactic:
rw [Nat.cast_sub h]

Goal state after:
case pos
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) - ↑(n + 1) = cast a + cast b - ↑(n + 1)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH✝ : H.index ∣ 2
hH : H.index = 1
⊢ ∃ a, ∀ (b : G), b * a ∈ H ∨ b ∈ H

Tactic:
simp [index_eq_one.mp hH]

Goal state after:
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₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ a ^ (n₂ - n₁) ∈ H

Tactic:
rw [← zpow_natCast]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ a ^ ↑(n₂ - n₁) ∈ H
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : ¬x + 1 = 0
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
← Ne

Goal state after:
case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
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
hx : x ≠ -1
hn : n ≠ 0
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
by
  obtain _ | _ | n := n
  · cases hn rfl
  · simp only [zero_add, range_one, sum_singleton, pow_zero, ne_eq, one_ne_zero, not_false_eq_true]
  rw [Ne, eq_neg_iff_add_eq_zero, ← Ne] at hx
  obtain h | h := hx.lt_or_gt
  · have := geom_sum_alternating_of_lt_neg_one h n.one_lt_succ_succ
    split_ifs at this
    · exact this.ne
    · exact (zero_lt_one.trans this).ne'
  · exact (geom_sum_pos' h n.succ.succ_ne_zero).ne'

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ x ∈ image (HDiv.hDiv n) n.divisors, f x = n.divisors.prod f

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

Tactic:
· exact prod_congr (image_div_divisors_eq_divisors n) (by simp)

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ Set.InjOn (HDiv.hDiv n) ↑n.divisors
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
this : NeZero b
⊢ (a.val + (-b).val) % n = a.val - b.val

Tactic:
val_neg_of_ne_zero,

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a.val + (n - b.val)) % n = a.val - b.val
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n : ℕ
hn : n ≠ 0
⊢ padicValNat p n < n

Tactic:
by
  match p with
  | 0 | 1 => simp [Nat.pos_of_ne_zero hn]
  | p + 2 =>
    apply (p + 2 |>.pow_lt_pow_iff_right <| by lia).mp
    apply Nat.lt_of_le_of_lt ?_ <| Nat.lt_pow_self <| by lia
    exact le_of_dvd (Nat.pos_of_ne_zero hn) pow_padicValNat_dvd

Goal state after: