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

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

Tactic:
intro h f g hf hg he

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
⊢ ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
Module: Mathlib.Algebra.Polynomial.Monic

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

Tactic:
intro h f g hf hg he

Goal state after:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
⊢ f.natDegree = 0 ∨ g.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
by
  rw [hp.irreducible_iff_natDegree', and_iff_right hp1]
  constructor
  · rintro h g hg hdg ⟨f, rfl⟩
    exact h f g (hg.of_mul_monic_left hp) hg (mul_comm f g) hdg
  · rintro h f g - hg rfl hdg
    exact h g hg hdg (dvd_mul_left g f)

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

Goal state before:
pp: R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < #s
⊢ (∏ i ∈ s, (X - C (f i))).coeff (#s - 1) = -∑ i ∈ s, f i

Tactic:
simpa using multiset_prod_X_sub_C_coeff_card_pred (s.1.map f) (by simpa using hs)

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 : ℕ
hm : p.degree < ↑m
⊢ (k • p).coeff m = 0

Tactic:
rw [degree_lt_iff_coeff_zero] at 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 : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
⊢ (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 : ℕ
hm : (k • p).degree < ↑m
⊢ p.coeff m = 0

Tactic:
rw [degree_lt_iff_coeff_zero] at 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 : ∀ (m_1 : ℕ), m ≤ m_1 → (k • p).coeff m_1 = 0
⊢ p.coeff m = 0
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
simp_rw [mul_sum, sum_range_succ_comm, tsub_self, pow_zero, mul_one, add_right_inj, ← mul_assoc,
    (h.symm.pow_right _).eq, mul_assoc, ← pow_succ']

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

Goal state before:
pp: A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
this : ∀ (x : C), x ∈ span B ↑y
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG

Tactic:
mem_span_finset

Goal state after:
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
this : ∀ (x : C), ∃ f, Function.support f ⊆ ↑y ∧ ∑ a ∈ y, f a • a = x
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
⊢ (∑ i ∈ range n, X ^ i).Monic

Tactic:
nontriviality R
  apply monic_X.geom_sum _ hn
  simp only [natDegree_X, zero_lt_one]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FiniteType R A ↔ ∃ s f, Surjective ⇑f

Tactic:
constructor
  · rintro ⟨s, hs⟩
    refine ⟨s, FreeAlgebra.lift _ (↑), ?_⟩
    rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← adjoin_range_eq_range_freeAlgebra_lift,
      Subtype.range_coe_subtype, Finset.setOfPred_mem, hs, coe_top]
  · rintro ⟨s, f, hsur⟩
    exact .of_surjective f hsur

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ (Algebra.adjoin R s).op.toSubsemiring = (Algebra.adjoin R (MulOpposite.unop ⁻¹' s)).toSubsemiring

Tactic:
simp_rw [Algebra.adjoin, op_toSubsemiring, Subsemiring.op_closure, Set.preimage_union]

Goal state after:
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Subsemiring.closure (MulOpposite.unop ⁻¹' Set.range ⇑(algebraMap R A) ∪ MulOpposite.unop ⁻¹' s) =
    Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s)
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
⊢ ((aeval f) F).natDegree ≤ m * n

Tactic:
rw [MvPolynomial.aeval_def, MvPolynomial.eval₂]
  apply (Polynomial.natDegree_sum_le _ _).trans
  apply Finset.sup_le
  intro d hd
  simp_rw [Function.comp_apply, ← Polynomial.C_eq_algebraMap]
  apply (Polynomial.natDegree_C_mul_le _ _).trans
  apply (Polynomial.natDegree_prod_le _ _).trans
  have : ∑ i ∈ d.support, (d i) * n ≤ m * n := by
    rw [← Finset.sum_mul]
    apply mul_le_mul' (.trans _ hF) le_rfl
    rw [MvPolynomial.totalDegree]
    exact Finset.le_sup_of_le hd le_rfl
  apply (Finset.sum_le_sum _).trans this
  rintro i -
  apply Polynomial.natDegree_pow_le.trans
  exact mul_le_mul' le_rfl (hf i)

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_2.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 : Fin k
⊢ f (nj j) ∈ M'

Tactic:
exact subset_span (by simp [hnj])

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

Goal state before:
pp: n a b : ℤ
h : a / n = b / n
⊢ a ≡ b [ZMOD n] ↔ a = b

Tactic:
by grind [ext_ediv_modEq_iff]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsRightCancelAdd R],
    a ≤ b → (↑a = ↑b ↔ a ≡ b [MOD p])
hle : ¬a ≤ b
⊢ b ≡ a [MOD p] ↔ a ≡ b [MOD p]

Tactic:
Nat.ModEq.comm

Goal state after:
case inr
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsRightCancelAdd R],
    a ≤ b → (↑a = ↑b ↔ a ≡ b [MOD p])
hle : ¬a ≤ b
⊢ a ≡ b [MOD p] ↔ a ≡ b [MOD p]
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
F : Type w
inst✝² : Ring R
inst✝¹ : Semiring S
ι : Type u_1
I : ι → Ideal R
inst✝ : ∀ (i : ι), (I i).IsTwoSided
⊢ ∀ a ∈ ⨅ i, I i, (RingHom.pi fun i ↦ Quotient.mk (I i)) a = 0

Tactic:
by simp [← RingHom.mem_ker, ker_Pi_Quotient_mk]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
⊢ ↑n = 0 ↔ 2 ∣ n

Tactic:
obtain hn | hn := Nat.even_or_odd n

Goal state after:
case inl
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Even n
⊢ ↑n = 0 ↔ 2 ∣ n

case inr
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Odd n
⊢ ↑n = 0 ↔ 2 ∣ n
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type w
inst✝³ : Ring R✝
inst✝² : Semiring S
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
hf : Pairwise (IsCoprime on f)
⊢ I ⊓ J = ⨅ i, f i

Tactic:
simp [f, iInf, inf_comm]

Goal state after:
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) I = map (Quotient.mk J) I

Tactic:
bot_sup_eq

Goal state after:
R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
⊢ map (Quotient.mk J) I = map (Quotient.mk J) I
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a b : List α
ha : b ~ m.toList
hb : b ~ n.toList
hab : a = b
⊢ m = n

Tactic:
exact Finset.perm_toList.mp <| Perm.trans ha.symm hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α
ts ys : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t [] r ys fun x ↦ f (x ++ ts)).snd = (permutationsAux2 t ts r ys f).snd

Tactic:
induction ys generalizing f with
  | nil => simp
  | cons ys_hd _ ys_ih => simp [ys_ih fun xs => f (ys_hd :: xs)]

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:
simp only [Set.mem_star, Subalgebra.mem_carrier] at *

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
x y : A
hx : star x ∈ S
hy : star y ∈ S
⊢ star (x * y) ∈ S
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:
simp only [Set.mem_star, Subalgebra.mem_carrier] at *

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
x y : A
hx : star x ∈ S
hy : star y ∈ S
⊢ star (x + y) ∈ S
Module: Mathlib.Data.List.Permutation

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

Tactic:
rw [permutationsAux2_snd_cons,
    show (fun x : List α => l ++ y :: x) = (l ++ [y] ++ ·) by simp, mem_cons, 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' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ (t :: is ++ ts).permutationsAux is' =
    map (fun x ↦ x ++ ts) ((t :: is).permutationsAux is') ++ ts.permutationsAux ((t :: is).reverse ++ is')

Tactic:
| cons t is ih =>

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

Goal state before:
pp: α : Type u_1
is is' ts : List α
⊢ (is ++ ts).permutationsAux is' =
    map (fun x ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')

Tactic:
by
  induction is generalizing is' with | nil => simp | cons t is ih =>
  simp only [foldr_permutationsAux2, ih, map_flatMap, cons_append, permutationsAux_cons, map_append,
    reverse_cons, append_assoc]
  congr 2
  funext _
  rw [map_permutationsAux2]
  simp +singlePass only [← permutationsAux2_comp_append]
  simp only [id, append_assoc]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ x ∈ ⋃ n, ⋃ (_ : n > 0), ptsOfPeriod f n ↔ x ∈ periodicPts f

Tactic:
by simp [mem_periodicPts]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ List.beq = fun a b ↦ decide (a = b)

Tactic:
by
    funext l₁ l₂
    change (l₁ == l₂) = _
    rw [Bool.eq_iff_iff, @beq_iff_eq _ (_), decide_eq_true_iff]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : ¬a = x
⊢ some ((y :: tail).nextOr a d) = (y :: tail)[(idxOf a (y :: tail)).succ]?

Tactic:
nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : ¬a = x
⊢ (y :: tail)[idxOf a (y :: tail) + 1]? = (y :: tail)[(idxOf a (y :: tail)).succ]?

case neg.ha
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : ¬a = x
⊢ a ∈ (y :: tail).dropLast
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.prev x ⋯ = l.next x hx

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
  have lpos : 0 < l.length := k.zero_le.trans_lt hk
  have key : l.length - 1 - k < l.length := by lia
  rw [← getElem_pmap l.next (fun _ h => h) (by simpa using hk)]
  simp_rw [getElem_eq_getElem_reverse (l := l), pmap_next_eq_rotate_one _ h]
  rw [← getElem_pmap l.reverse.prev fun _ h => h]
  · simp_rw [pmap_prev_eq_rotate_length_sub_one _ (nodup_reverse.mpr h), rotate_reverse,
      length_reverse, Nat.mod_eq_of_lt (Nat.sub_lt lpos Nat.succ_pos'),
      Nat.sub_sub_self (Nat.succ_le_of_lt lpos)]
    rw [getElem_eq_getElem_reverse]
    · simp [Nat.sub_sub_self (Nat.le_sub_one_of_lt hk)]
  · simpa

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

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

pp: case refine_2
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)
l : List α
⊢ ∀ (head : α) (tail : List α), motive ↑tail → motive ↑(head :: tail)

Tactic:
assumption'

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inr.mpr
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
refine ⟨k, hkle, hk_pos, n.minFac, Nat.minFac_le ?_, heq, ?_⟩

Goal state after:
case inr.mpr.refine_1
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ 0 < n

case inr.mpr.refine_2
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ Nat.Prime n.minFac
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l m : List α
a : α
⊢ (∀ (hl : m ≠ []), Chain r ↑m ↔ IsChain r (m.getLast hl :: m)) →
    ∀ (hl : m ++ [a] ≠ []), Chain r ↑(m ++ [a]) ↔ IsChain r ((m ++ [a]).getLast hl :: (m ++ [a]))

Tactic:
_H

Goal state after:
α : Type u_1
r : α → α → Prop
l m : List α
a : α
_H : ∀ (hl : m ≠ []), Chain r ↑m ↔ IsChain r (m.getLast hl :: m)
⊢ ∀ (hl : m ++ [a] ≠ []), Chain r ↑(m ++ [a]) ↔ IsChain r ((m ++ [a]).getLast hl :: (m ++ [a]))
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ Disjoint a.primeFactors b.primeFactors ↔ a.Coprime b

Tactic:
by
  simp [disjoint_iff_inter_eq_empty, coprime_iff_gcd_eq_one, ← primeFactors_gcd,
    ha, hb]

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

Goal state before:
pp: case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ replicate (n + 1) a <+~ b.primeFactorsList → a ^ (n + 1) ∣ b

Tactic:
List.subperm_iff

Goal state after:
case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ (∃ l, l ~ b.primeFactorsList ∧ replicate (n + 1) a <+ l) → a ^ (n + 1) ∣ b
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
x y : G'
⊢ f (x⁻¹ * y) = (f x)⁻¹ * f y

Tactic:
f.map_mul,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
x y : G'
⊢ f x⁻¹ * f y = (f x)⁻¹ * f y
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a : ℤ
⊢ (↑a).cast = a

Tactic:
Int.cast_id

Goal state after:
case zero
a : ℤ
⊢ cast a = a
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R : Type u
M' : Type v
inst✝² : Semiring R
inst✝¹ : Infinite M'
inst✝ : Nontrivial R
⊢ #R[M'] = max (lift.{v, u} #R) (lift.{u, v} #M')

Tactic:
by simp [coeffEquiv.cardinal_eq, max_comm]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R : Type u
M' : Type v
inst✝² : Semiring R
inst✝¹ : Nonempty M'
inst✝ : Infinite R
⊢ #R[M'] = max (lift.{v, u} #R) (lift.{u, v} #M')

Tactic:
by simp [coeffEquiv.cardinal_eq, max_comm]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
⊢ if Even 0 then ∑ i ∈ range 0, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range 0, x ^ i

Tactic:
simp only [range_zero, sum_empty, le_refl, ite_true, Even.zero]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
this : Std.Asymm fun x1 x2 ↦ x1.2 < x2.2
⊢ n.divisorsAntidiagonalList.reverse = List.map Prod.swap n.divisorsAntidiagonalList

Tactic:
refine List.Perm.eq_of_pairwise' pairwise_divisorsAntidiagonalList_snd.reverse
    (pairwise_divisorsAntidiagonalList_fst.map _ fun _ _ ↦ id) ?_

Goal state after:
n : ℕ
this : Std.Asymm fun x1 x2 ↦ x1.2 < x2.2
⊢ n.divisorsAntidiagonalList.reverse.Perm (List.map Prod.swap n.divisorsAntidiagonalList)
Module: Mathlib.Algebra.Order.Ring.GeomSum

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

Tactic:
← neg_lt_iff_pos_add',

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hmn✝ : 2 ≤ n
ihn : 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1
⊢ -(x * ∑ i ∈ range n, x ^ i) < 1 ∧ x * ∑ i ∈ range n, x ^ i < 0
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: r n : ℕ
⊢ (2 * n).choose (2 * n / 2) = (2 * n).choose n

Tactic:
Nat.mul_div_cancel_left n zero_lt_two

Goal state after:
r n : ℕ
⊢ (2 * n).choose n = (2 * n).choose n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Nontrivial G
inst✝ : Module (ZMod 1) G
x : G
hx : x ≠ 0
⊢ x = 0

Tactic:
by simpa using char_nsmul_eq_zero 1 x

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

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ ofDigits b l % b = l.head! % b

Tactic:
induction l <;> simp [Nat.ofDigits]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ emultiplicity a b = ↑0 ↔ ¬a ∣ b

Tactic:
emultiplicity_eq_coe

Goal state after:
case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ a ^ 0 ∣ b ∧ ¬a ^ (0 + 1) ∣ b ↔ ¬a ∣ b
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
h : ¬p ∣ n
⊢ n.factorization p = 0

Tactic:
simp [factorization_eq_zero_iff, h]

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

Goal state before:
pp: case refine_2
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : d ∣ n
c : ℕ
h : n = d * c
⊢ d.factorization ≤ n.factorization

Tactic:
· subst h
    rw [factorization_mul hd <| right_ne_zero_of_mul hn]
    apply self_le_add_right

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ψ (x ^ orderOf x) = 1

Tactic:
pow_orderOf_eq_one

Goal state after:
G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ψ 1 = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
x : G
inst✝ : Monoid H
f : G →* H
hf : Injective ⇑f
⊢ 0 < orderOf (f x) ↔ IsOfFinOrder x

Tactic:
orderOf_injective f hf x,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
x : G
inst✝ : Monoid H
f : G →* H
hf : Injective ⇑f
⊢ 0 < orderOf x ↔ IsOfFinOrder x