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

Goal state before:
pp: case refine_2.inl
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : n < p.natDegree
⊢ p.coeff n = if n = p.natDegree then 1 else 0

Tactic:
if_neg hn.ne,

Goal state after:
case refine_2.inl
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : n < p.natDegree
⊢ p.coeff n = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.coeff (f.natDegree - 1) = f.coeff (f.natDegree - 1)

pp: case hnc
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ ¬f.natDegree = 0

Tactic:
eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.coeff (f.natDegree - 1) = f.coeff (f.natDegree - 1)

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1

case hnc
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ ¬f.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
k : ℕ
⊢ (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree

Tactic:
induction k with

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
⊢ (C a * p).nextCoeff = a * p.nextCoeff

Tactic:
by
  by_cases h₀ : a = 0 <;> simp [h₀, nextCoeff, natDegree_C_mul]

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

Goal state before:
pp: case neg.inr
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P).eraseLead.eraseLead.coeff n = ((X - C x) * P.eraseLead).coeff n

Tactic:
· --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.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ p.comp q ≠ 0

Tactic:
simp_rw [Ne, comp_eq_zero_iff, hp, false_or, not_and_or, ← degree_le_zero_iff]

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ ¬eval (q.coeff 0) p = 0 ∨ ¬q.degree ≤ 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : R[X]
fg : f.leadingCoeff * g.leadingCoeff ≠ 0
⊢ reflect (f * g).natDegree (f * g) = reflect f.natDegree f * reflect g.natDegree g

Tactic:
natDegree_mul' fg,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f g : R[X]
fg : f.leadingCoeff * g.leadingCoeff ≠ 0
⊢ reflect (f.natDegree + g.natDegree) (f * g) = reflect f.natDegree f * reflect g.natDegree g
Module: Mathlib.Algebra.Polynomial.Monic

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

Tactic:
contrapose! h

Goal state after:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ (Multiset.map (fun i ↦ (X - C i).nextCoeff) t).sum = -t.sum

pp: case h
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ ∀ i ∈ t, (X - C i).Monic

Tactic:
· simp only [nextCoeff_X_sub_C]
    exact t.sum_hom (-AddMonoidHom.id R)

Goal state after:
case h
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ ∀ i ∈ t, (X - C i).Monic
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg.h₀
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j✝ : Fin (n + 1)
i : Fin n
hij : i.castSucc < j✝
hj : ¬∃ j₀, j₀.castSucc = j✝
j : Fin n
a✝ : j ∈ univ
hji : j ≠ i
⊢ (C (x j) * X ^ k j).coeff (k i) = 0

Tactic:
rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
k : ℕ
x : R
hx : x ≠ 0
⊢ #(C x * X ^ k).support = 1

Tactic:
rw [support_C_mul_X_pow k hx, card_singleton]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Tactic:
rcases exists_degree_le_of_mem_span_of_finite s_fin s_emp with ⟨p', _, hp'max⟩

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
p' : R[X]
left✝ : p' ∈ s
hp'max : ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
h : Odd n
⊢ x + y ∣ x ^ n + y ^ n

Tactic:
have h₁ := geom_sum₂_mul x (-y) n

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))

Tactic:
induction n generalizing i with

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: case convert_3
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 = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
hyy :
  span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) * span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) ≤
    span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
⊢ Subalgebra.toSubmodule (Algebra.adjoin A ↑x) ≤ restrictScalars A (span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y))

Tactic:
Algebra.adjoin_eq_span,

Goal state after:
case convert_3
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 = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
hyy :
  span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) * span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) ≤
    span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
⊢ span A ↑(Submonoid.closure ↑x) ≤ restrictScalars A (span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.inr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = ↑n
⊢ ∃ p_1 ∈ I, p_1.degree ≤ ↑n ∧ p_1.leadingCoeff = p.coeff n

Tactic:
refine ⟨p, hpI, le_of_eq hpdeg, ?_⟩
      rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbotD_coe]

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

Goal state before:
pp: case convert_3
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
x✝ : ℕ
⊢ Prime (C r) ↔ Prime r

Tactic:
induction Fintype.card σ with

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : AddMonoid M
h : FiniteType R R[M]
⊢ ∃ G, adjoin R (of' R M '' ↑G) = ⊤

Tactic:
obtain ⟨S, hS⟩ := h
  let : DecidableEq M := Classical.decEq M
  use Finset.biUnion S fun f => f.coeff.support
  have : S.biUnion (fun f => f.coeff.support) = ⋃ f ∈ S, (f.coeff.support : Set M) := by
    simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]
  rw [this]
  exact support_gen_of_gen' hS

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommRing R
inst✝ : Monoid M
h : FiniteType R R[M]
⊢ ∃ G, adjoin R (⇑(of R M) '' ↑G) = ⊤

Tactic:
obtain ⟨S, hS⟩ := h
  let : DecidableEq M := Classical.decEq M
  use Finset.biUnion S fun f => f.coeff.support
  have : S.biUnion (fun f => f.coeff.support) = ⋃ f ∈ S, (f.coeff.support : Set M) := by
    simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]
  rw [this]
  exact support_gen_of_gen' hS

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

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
this : ∀ m ∈ p.support, (monomial m) (coeff m p) ∈ I
⊢ ∑ v ∈ p.support, (monomial v) (coeff v p) ∈ I

Tactic:
exact Submodule.sum_mem I this

Goal state after:
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
h : comap f I ≤ J
r : R
ha : (quotientMap I f H) ((Quotient.mk J) r) = 0
⊢ (Quotient.mk J) r = 0

Tactic:
rw [quotientMap_mk, Quotient.eq_zero_iff_mem] at ha

Goal state after:
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
h : comap f I ≤ J
r : R
ha : f r ∈ I
⊢ (Quotient.mk J) r = 0
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case mp
α : 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 : ∀ a ∈ n.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
hc : m = n
⊢ False

Tactic:
contrapose! h

Goal state after:
case mp
α : 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
hc : m = n
h : True
⊢ ∃ a ∈ n.toList.permutations, ∃ b ∈ n.toList.permutations, a = b
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case mp
α : 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
hc : m = n
h : True
⊢ ∃ a ∈ n.toList.permutations, ∃ b ∈ n.toList.permutations, a = b

Tactic:
use n.toList

Goal state after:
case h
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
hc : m = n
h : True
⊢ n.toList ∈ n.toList.permutations ∧ ∃ b ∈ n.toList.permutations, n.toList = b
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
S : StarSubalgebra R A
⊢ adjoin R s ≤ S ↔ s ⊆ ↑S

Tactic:
← toSubalgebra_le_iff,

Goal state after:
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
S : StarSubalgebra R A
⊢ (adjoin R s).toSubalgebra ≤ S.toSubalgebra ↔ 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
⊢ GaloisConnection (adjoin R) SetLike.coe

Tactic:
by
  intro s S
  rw [← toSubalgebra_le_iff, adjoin_toSubalgebra, Algebra.adjoin_le_iff, coe_toSubalgebra]
  exact
    ⟨fun h => Set.subset_union_left.trans h, fun h =>
      Set.union_subset h fun x hx => star_star x ▸ star_mem (show star x ∈ S from h hx)⟩

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
b : ↥(I ^ n) ⧸ I • ⊤
x : R
hx : x ∈ I ^ n
⊢ (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) (Submodule.Quotient.mk ⟨x, hx⟩) =
      (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) b →
    Submodule.Quotient.mk ⟨x, hx⟩ = b

Tactic:
obtain ⟨⟨y, hy⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ b

Goal state after:
case refine_3
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x : R
hx : x ∈ I ^ n
y : R
hy : y ∈ I ^ n
⊢ (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) (Submodule.Quotient.mk ⟨x, hx⟩) =
      (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) (Submodule.Quotient.mk ⟨y, hy⟩) →
    Submodule.Quotient.mk ⟨x, hx⟩ = Submodule.Quotient.mk ⟨y, hy⟩
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts ys l l' : List α
⊢ l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

Tactic:
induction ys generalizing l with
  | nil => simp +contextual
  | cons y ys ih => ?_
  rw [permutationsAux2_snd_cons,
    show (fun x : List α => l ++ y :: x) = (l ++ [y] ++ ·) by simp, mem_cons, ih]
  constructor
  · rintro (rfl | ⟨l₁, l₂, l0, rfl, rfl⟩)
    · exact ⟨[], y :: ys, by simp⟩
    · exact ⟨y :: l₁, l₂, l0, by simp⟩
  · rintro ⟨_ | ⟨y', l₁⟩, l₂, l0, ye, rfl⟩
    · simp [ye]
    · simp only [cons_append] at ye
      rcases ye with ⟨rfl, rfl⟩
      exact Or.inr ⟨l₁, l₂, l0, by simp⟩

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

Goal state before:
pp: α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ a, a ∈ L ∧ ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ foldr (fun y r ↦ (permutationsAux2 t ts r y id).snd) r L ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts

Tactic:
foldr_permutationsAux2

Goal state after:
α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ a, a ∈ L ∧ ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m : l ∈ ts.permutationsAux (t :: is)
⊢ l ~ t :: ts ++ is

pp: case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left✝ : l₂ ≠ []
⊢ l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is

Tactic:
· exact (IH1 _ m).trans perm_middle

Goal state after:
case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left✝ : l₂ ≠ []
⊢ l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
a b : α
⊢ flatMap (permutations'Aux b) (permutations'Aux a []) ~ flatMap (permutations'Aux a) (permutations'Aux b [])

Tactic:
exact Perm.swap [a, b] [b, a] []

Goal state after:
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
⊢ adjoin R s ≤ centralizer R ↑(centralizer R s)

Tactic:
← toSubalgebra_le_iff,

Goal state after:
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
⊢ (adjoin R s).toSubalgebra ≤ (centralizer R ↑(centralizer R s)).toSubalgebra
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

Tactic:
rw [← Nat.mod_add_div n (period m a), pow_add, mul_smul,
    pow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
| m ^ (n % period m a) • a
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
hd : d ∈ xs
⊢ xs.nextOr x d ∈ xs

Tactic:
revert hd
  suffices ∀ xs' : List α, (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → nextOr xs x d ∈ xs' by
    exact this xs fun _ => id
  intro xs' hxs' hd
  induction xs with
  | nil => exact hd
  | cons y ys ih => ?_
  rcases ys with - | ⟨z, zs⟩
  · exact hd
  rw [nextOr]
  split_ifs with h
  · exact hxs' _ (mem_cons_of_mem _ mem_cons_self)
  · exact ih fun _ h => hxs' _ (mem_cons_of_mem _ h)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l ≠ []
⊢ l.prev (l.head hl) ⋯ = l.getLast hl

Tactic:
cases l with

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
⊢ l.prev a ha = l[(idxOf a l + (l.length - 1)) % l.length]

Tactic:
cases l with

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

Goal state before:
pp: case h
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ [x :: x :: l, x :: x :: l] <+ ([x, x] ++ l).permutations

Tactic:
← permutations_take_two

Goal state after:
case h
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ take 2 (x :: x :: l).permutations <+ ([x, x] ++ l).permutations
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ stabilizer G (g • a) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)

Tactic:
by
  ext h
  rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
⊢ (stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) = stabilizerEquivStabilizer hk

Tactic:
by
  ext; simp [stabilizerEquivStabilizer_apply, H]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a : α
⊢ Chain r ↑[a] ↔ r a a

Tactic:
chain_coe_cons,

Goal state after:
α : Type u_1
r : α → α → Prop
a : α
⊢ IsChain r (a :: ([] ++ [a])) ↔ r a a
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : 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 ↑(a :: m) ↔ IsChain r ((m ++ [a]).getLast hl✝ :: (m ++ [a]))

Tactic:
chain_coe_cons,

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] ≠ []
⊢ IsChain r (a :: (m ++ [a])) ↔ IsChain r ((m ++ [a]).getLast hl✝ :: (m ++ [a]))
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain r ↑(n :: range n) ↔ r n 0 ∧ ∀ m < n, r m m.succ

Tactic:
chain_coe_cons,

Goal state after:
r : ℕ → ℕ → Prop
n : ℕ
⊢ IsChain r (n :: (range n ++ [n])) ↔ r n 0 ∧ ∀ m < n, r m m.succ
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : Chain r ↑(a :: l)
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
⊢ r b c

Tactic:
rw [Cycle.chain_coe_cons, List.isChain_iff_pairwise] at hs

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : List.Pairwise r (a :: (l ++ [a]))
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
⊢ r b c
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : H.Normal
inst✝² : SMul G X
inst✝¹ : MulAction (G ⧸ H) X
inst✝ : IsScalarTower G (G ⧸ H) X
g : G
x : X
⊢ ↑g • x = g • x

Tactic:
← smul_one_smul (G ⧸ H) g x,

Goal state after:
G : Type u
X : Type v
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : H.Normal
inst✝² : SMul G X
inst✝¹ : MulAction (G ⧸ H) X
inst✝ : IsScalarTower G (G ⧸ H) X
g : G
x : X
⊢ ↑g • x = (g • 1) • x
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p = (p ^ n).primeFactorsList

Tactic:
rw [← List.replicate_perm]

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p ~ (p ^ n).primeFactorsList
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: case inr
n k : ℕ
hn : n ≠ 0
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors

Tactic:
induction k with

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
← cons_self_properDivisors hn,

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ cons n n.properDivisors ⋯, i = ∑ i ∈ n.properDivisors, i + n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
⊢ (n✝ + 1).properDivisors \ s = ∅

Tactic:
contrapose! h

Goal state after:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ ∑ x ∈ s, x ≠ ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x