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

Goal state before:
pp: case pos
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝¹ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst✝ : Decidable (↑s.support ⊆ range f)
h : ↑s.support ⊆ range f
⊢ (killCompl hf) ((monomial s) c) = (monomial (Finsupp.comapDomain f s ⋯)) c

Tactic:
exact killCompl_monomial_eq_monomial_comapDomain_of_subset hf c h

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

Goal state before:
pp: case refine_1
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
x✝ : ∃ n, ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q
n : σ →₀ ℕ
hn1 : ¬coeff n p + coeff n q = 0
hn2 : r = coeff n p + coeff n q
⊢ (∃ n, ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ n, ¬coeff n q = 0 ∧ r = coeff n q

pp: case refine_2
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
⊢ ((∃ n, ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ n, ¬coeff n q = 0 ∧ r = coeff n q) →
    ∃ n, ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q

Tactic:
· obtain (h | h) := hor n hn1
    · exact Or.inl ⟨n, by simp [h, hn2, hl n h]⟩
    · exact Or.inr ⟨n, by simp [h, hn2, hr n h]⟩

Goal state after:
case refine_2
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
⊢ ((∃ n, ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ n, ¬coeff n q = 0 ∧ r = coeff n q) →
    ∃ n, ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
⊢ (if a = 0 then ⊥ else toMultiset s) ≤ toMultiset s

Tactic:
split_ifs

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
h✝ : a = 0
⊢ ⊥ ≤ toMultiset s

case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
h✝ : ¬a = 0
⊢ toMultiset s ≤ toMultiset s
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_1.mem_mul_mem
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial s) (m * n) ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
← add_zero s,

Goal state after:
case refine_1.mem_mul_mem
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial (s + 0)) (m * n) ∈ coeffsIn σ M * coeffsIn σ N
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
i : σ
hi : i ∈ u.support
⊢ (if i ∈ s then X i else 0) ^ u i = X i ^ u i

Tactic:
simp [hs ((mem_vars_iff_mem_support _).mpr ⟨u, hu, hi⟩)]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : i < p.natTrailingDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rw [coeff_eq_zero_of_lt_natTrailingDegree hi, zero_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ (embDomain (revAt N) f.coeff) i = (embDomain (revAt N) f.coeff) ((revAt N) ((revAt N) i))

Tactic:
rw [revAt_invol]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p : R[X]
⊢ (if p.natDegree = 0 then 0 else (map f p).coeff (p.natDegree - 1)) =
    f (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))

Tactic:
split_ifs

Goal state after:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p : R[X]
h✝ : p.natDegree = 0
⊢ 0 = f 0

case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p : R[X]
h✝ : ¬p.natDegree = 0
⊢ (map f p).coeff (p.natDegree - 1) = f (p.coeff (p.natDegree - 1))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₂
⊢ (sumAlgEquiv R S₁ S₂) (X (Sum.inr c)) = C (X c)

Tactic:
ext; simp [sumAlgEquiv, C, X, monomial, coeff]

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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₂
⊢ (sumAlgEquiv R S₁ S₂).symm (C (X c)) = X (Sum.inr c)

Tactic:
ext; simp [sumAlgEquiv, C, X, monomial, coeff]

Goal state after:
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
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

Tactic:
by
  -- if `P = 0` this is trivial
  by_cases hp : P = 0
  · simp [hp]
  -- can assume eraseLead P ≠ 0, otherwise it's a monomial and both sides are zero.
  by_cases he : P.eraseLead = 0
  · rw [he, mul_zero]
    by_cases he₂ : ((X - C x) * P).eraseLead = 0
    · simp [he₂]
    suffices #((X - C x) * P).support ≤ 2 by
      rw [← card_support_eq_zero]
      linarith [eraseLead_support_card_lt he₂,
        eraseLead_support_card_lt (mul_ne_zero (X_sub_C_ne_zero x) hp)]
    have h₂ : #(X - C x).support = 2 := by
      simpa [← sub_eq_add_neg] using!
        card_support_binomial one_ne_zero one_ne_zero (neg_ne_zero.mpr hx)
    have hmul := card_support_mul_le (p := X - C x) (q := P)
    rw [h₂] at hmul
    linarith [card_support_le_one_of_eraseLead_eq_zero he]
  have h₁ : ((X - C x) * P).natDegree = P.natDegree + 1 := by
    rw [natDegree_mul (X_sub_C_ne_zero x) hp, natDegree_X_sub_C, add_comm]
  -- 2 ≤ P.natDegree
  obtain ⟨dP, hdP⟩ := Nat.exists_eq_add_of_le' (two_le_natDegree_of_nextCoeff_eraseLead he h)
  -- the subleading term of (X - C η) * P is nonzero
  have h₂ : ((X - C x) * P).nextCoeff ≠ 0 := by
    simp only [nextCoeff, hdP, Nat.succ_ne_zero, ite_false, Nat.add_one_sub_one] at h
    rw [nextCoeff, h₁, add_tsub_cancel_right, hdP, coeff_X_sub_C_mul]
    simp [h, hx, ← hdP, hp]
  -- Prove equality by showing coefficients are equal
  ext n
  rcases n.lt_or_ge P.natDegree with hn | hn
  · --n < P.natDegree
    have hd₁ : n < ((X - C x) * P).eraseLead.natDegree := by
      linarith [natDegree_eraseLead_add_one h₂]
    rw [← self_sub_monomial_natDegree_leadingCoeff, coeff_sub, coeff_monomial, if_neg hd₁.ne']
    rw [← self_sub_monomial_natDegree_leadingCoeff, coeff_sub, coeff_monomial, if_neg (by lia)]
    rw [← self_sub_monomial_natDegree_leadingCoeff, mul_sub, coeff_sub,
      sub_zero, sub_zero, eq_sub_iff_add_eq, add_eq_left]
    rcases hn₂ : n
    · simpa [coeff_monomial, hp] using! fun _ ↦ by lia
    · rw [coeff_X_sub_C_mul, coeff_monomial, coeff_monomial, if_neg (by lia),
        if_neg (by lia), mul_zero, sub_zero]
  · --n ≥ P.natDegree, so all the coefficients are zero.
    trans 0 <;> rw [coeff_eq_zero_of_natDegree_lt]
    · grw [eraseLead_natDegree_le, eraseLead_natDegree_le]
      simpa [h₁, hdP] using! hn
    · grw [natDegree_mul (X_sub_C_ne_zero x) he, natDegree_eraseLead_le_of_nextCoeff_eq_zero h]
      simpa [add_comm, hdP] using! hn

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ ((optionEquivLeft R σ) f).support.Nonempty

Tactic:
Polynomial.support_nonempty,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ (optionEquivLeft R σ) f ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
h : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).leadingCoeff = 1

Tactic:
leadingCoeff_mul,

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
h : p ≠ 0
⊢ p.leadingCoeff * (C p.leadingCoeff⁻¹).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p.reverse * q.reverse).leadingCoeff = p.trailingCoeff * q.trailingCoeff

Tactic:
leadingCoeff_mul,

Goal state after:
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ p.reverse.leadingCoeff * q.reverse.leadingCoeff = p.trailingCoeff * q.trailingCoeff
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
a✝ : Nontrivial R
⊢ f p.leadingCoeff ≠ 0

Tactic:
· rw [hp.leadingCoeff, f.map_one]
      exact one_ne_zero

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
⊢ (↑p).coeff i = if i = n then 1 else 0

Tactic:
split_ifs

Goal state after:
case pos
R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
h✝ : i = n
⊢ (↑p).coeff i = 1

case neg
R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
h✝ : ¬i = n
⊢ (↑p).coeff i = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
⊢ (if h : Function.HasFiniteMulSupport f then ∏ i ∈ Set.Finite.toFinset h, f i else 1).Monic

Tactic:
split_ifs

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
h✝ : Function.HasFiniteMulSupport f
⊢ (∏ i ∈ Set.Finite.toFinset h✝, f i).Monic

case neg
R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
h✝ : ¬Function.HasFiniteMulSupport f
⊢ Monic 1
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
⊢ ((finSuccEquiv R n) f).support.Nonempty

Tactic:
Polynomial.support_nonempty,

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ (finSuccEquiv R n) f ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ (g * C f.leadingCoeff).leadingCoeff = 1

Tactic:
leadingCoeff_mul,

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ g.leadingCoeff * (C f.leadingCoeff).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ (f * C g.leadingCoeff).leadingCoeff = 1

Tactic:
leadingCoeff_mul,

Goal state after:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ f.leadingCoeff * (C g.leadingCoeff).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case neg
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ ∑ b ∈ s, (v b • map (algebraMap R A) (f b)).coeff (f i).natDegree ≠ 0

Tactic:
conv in (fun _ ↦ _) =>
      ext
      rw [coeff_smul, smul_eq_mul, coeff_map, mul_comm, ← Algebra.smul_def]

Goal state after:
case neg
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ ∑ x ∈ s, (f x).coeff (f i).natDegree • v x ≠ 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
x : R
⊢ eval x p = ∑ i, (degreeLTEquiv R n) ⟨p, hp⟩ i * x ^ ↑i

Tactic:
simp_rw [eval_eq_sum]
  exact (sum_fin _ (by simp_rw [zero_mul, forall_const]) (mem_degreeLT.mp hp)).symm

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
i : ℕ
⊢ (if i = 0 then 1 else 0) = ↑(if i = 0 then 1 else 0)

Tactic:
split_ifs

Goal state after:
case pos
R : Type u
inst✝ : Ring R
i : ℕ
h✝ : i = 0
⊢ 1 = ↑1

case neg
R : Type u
inst✝ : Ring R
i : ℕ
h✝ : ¬i = 0
⊢ 0 = ↑0
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ IsNoetherianRing S

Tactic:
apply
    isNoetherianRing_of_surjective (MvPolynomial s R) S
      (MvPolynomial.aeval (↑) : MvPolynomial s R →ₐ[R] S).toRingHom

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ Surjective ⇑(MvPolynomial.aeval Subtype.val).toRingHom
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsNoetherianRing (MvPolynomial (Fin 0) R)

Tactic:
by
  apply isNoetherianRing_of_ringEquiv R
  symm; apply MvPolynomial.isEmptyRingEquiv R (Fin 0)

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

Goal state before:
pp: case inr
j : ℕ
left✝ : Prime j
a1 : 1 ≠ 1
hp : Prime (1 * j)
⊢ 1 * j = 1

Tactic:
exact (a1 rfl).elim

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

Goal state before:
pp: x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
⊢ p = a * y

Tactic:
rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h

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) (comap (Quotient.mk I) (map (Quotient.mk I) J)) = map (Quotient.mk J) I

Tactic:
Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (ts is : List α), map (map f) (ts.permutationsAux is) = (map f ts).permutationsAux (map f is)

Tactic:
refine permutationsAux.rec (by simp) ?_

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (t : α) (ts is : List α),
    map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is)) →
      map (map f) (is.permutationsAux []) = (map f is).permutationsAux (map f []) →
        map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
⊢ ∀ (ts is l : List α), l ∈ ts.permutationsAux is → l ~ ts ++ is

Tactic:
refine permutationsAux.rec (by simp) ?_

Goal state after:
α : Type u_1
⊢ ∀ (t : α) (ts is : List α),
    (∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is) →
      (∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []) →
        ∀ (l : List α), l ∈ (t :: ts).permutationsAux is → l ~ t :: ts ++ is
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
⊢ ∀ (ts is : List α), (ts.permutationsAux is).length + is.length ! = (ts.length + is.length)!

Tactic:
refine permutationsAux.rec (by simp) ?_

Goal state after:
α : Type u_1
⊢ ∀ (t : α) (ts is : List α),
    (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)! →
      (is.permutationsAux []).length + [].length ! = (is.length + [].length)! →
        ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
⊢ ∀ (ts is l : List α), l ~ is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux is

Tactic:
refine permutationsAux.rec (by simp) ?_

Goal state after:
α : Type u_1
⊢ ∀ (t : α) (ts is : List α),
    (∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)) →
      (∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []) →
        ∀ (l : List α), l ~ is ++ t :: ts → (∃ is' x, l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l.dropLast
y : α
hy : x ≠ y
⊢ l.nextOr x ((y :: l).get ⟨0, ⋯⟩) = l.nextOr x (l.get ⟨0, ⋯⟩)

Tactic:
nextOr_eq_nextOr_of_mem_dropLast

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l.dropLast
y : α
hy : x ≠ y
⊢ l.nextOr x ?d' = l.nextOr x (l.get ⟨0, ⋯⟩)

case d'
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l.dropLast
y : α
hy : x ≠ y
⊢ α

case x_mem
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l.dropLast
y : α
hy : x ≠ y
⊢ x ∈ l.dropLast
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : 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
⊢ (hd' :: tl).getLast ⋯ ∈ hd :: hd' :: tl

Tactic:
exact mem_cons_of_mem _ (getLast_mem _)

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

Goal state before:
pp: case cons.right
α : 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
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
⊢ False

Tactic:
have hx : (as.insertIdx n x)[m]'(by
          rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]) = x := by
        simp [hn', ← hm']

Goal state after:
case cons.right
α : 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
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
⊢ False
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.reverse.rotate (l.reverse.length - 1))[l.length - 1 - k] = (l.rotate 1)[k]

Tactic:
rotate_reverse,

Goal state after:
α : 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 (l.length - (l.reverse.length - 1) % l.length)).reverse[l.length - 1 - k] = (l.rotate 1)[k]
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
⊢ (if x✝ = a then b else if x✝ = b then a else x✝) ∈ S ↔ x✝ ∈ S

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
h✝ : x✝ = a
⊢ b ∈ S ↔ x✝ ∈ S

case pos
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
h✝¹ : ¬x✝ = a
h✝ : x✝ = b
⊢ a ∈ S ↔ x✝ ∈ S

case neg
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
h✝¹ : ¬x✝ = a
h✝ : ¬x✝ = b
⊢ x✝ ∈ S ↔ x✝ ∈ S
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
obtain ⟨n, hn⟩ := hab

Goal state after:
case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
n : ℕ
hn : (a :: l).rotate n = b :: m
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])
Module: Mathlib.Algebra.IsPrimePow

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

Tactic:
· grind [Nat.minFac_prime_iff]

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
⊢ a * l₁.prod = a * ((b :: l₂).erase a).prod

Tactic:
rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]

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
⊢ False

Tactic:
have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h

Goal state after:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0 * m
⊢ False
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: a b n : ℕ
ha : Prime a
hb : b ≠ 0
⊢ replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b

Tactic:
induction n generalizing b with
  | zero => simp
  | succ n ih =>
    constructor
    · rw [List.subperm_iff]
      rintro ⟨u, hu1, hu2⟩
      rw [← Nat.prod_primeFactorsList hb, ← hu1.prod_eq, ← prod_replicate]
      exact hu2.prod_dvd_prod
    · rintro ⟨c, rfl⟩
      rw [Ne, pow_succ', mul_assoc, mul_eq_zero, _root_.not_or] at hb
      rw [pow_succ', mul_assoc, replicate_succ,
        (Nat.perm_primeFactorsList_mul hb.1 hb.2).subperm_left, primeFactorsList_prime ha,
        singleton_append, subperm_cons, ih hb.2]
      exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.GroupTheory.Index

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

Tactic:
Subgroup.index_eq_two_iff_exists_notMem_and

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), b * a ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, b * a ∈ H ∨ b ∈ H