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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ (p.comp q).natDegree ≤ p.natDegree * q.natDegree

Tactic:
by rw [h0, natDegree_zero]; exact Nat.zero_le _

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.trailingDegree = ↑n ↔ p.natTrailingDegree = n

Tactic:
rw [trailingDegree_eq_natTrailingDegree hp, Nat.cast_inj]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬(p = 0 ∨ p.coeff 0 ≠ 0) ↔ p ≠ 0 ∧ p.coeff 0 = 0

Tactic:
by rw [not_or, not_ne_iff]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
pn : p.natDegree ≤ n
⊢ (q + p).natDegree ≤ n ↔ q.natDegree ≤ n

Tactic:
exact natDegree_add_le_iff_left _ _ pn

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

Goal state before:
pp: case zero
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
⊢ (p ^ 0).coeff (0 * n) = p.coeff n ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
⊢ (C c).nextCoeffUp = 0

Tactic:
rw [nextCoeffUp]

Goal state after:
R : Type u
inst✝ : Semiring R
c : R
⊢ (if (C c).natTrailingDegree = 0 then 0 else (C c).coeff ((C c).natTrailingDegree + 1)) = 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ∞
h : p.trailingDegree < n
h₀ : p = 0
⊢ n ≤ p.trailingDegree

Tactic:
simp [h₀]

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

Goal state before:
pp: N : ℕ
⊢ Function.Injective (revAtFun N)

Tactic:
intro a

Goal state after:
N a : ℕ
⊢ ∀ ⦃a₂ : ℕ⦄, revAtFun N a = revAtFun N a₂ → a = a₂
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.natDegree - 1 + 1 = f.natDegree

Tactic:
tsub_add_cancel_of_le

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.natDegree = f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ 1 ≤ f.natDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
P : MvPolynomial σ R
n : ℕ
⊢ ((uniqueAlgEquiv R σ) P).coeff n = coeff (Finsupp.single default n) P

Tactic:
induction P using induction_on' with

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hf : #f.support = 0
⊢ motive f

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (p * X ^ 0).reverse = p.reverse

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
s' : S₁ → R
f : (MvPolynomial S₁ R)[X]
i : ℕ
⊢ (Polynomial.map (eval s') f).coeff i = (eval s') (f.coeff i)

Tactic:
simp only [Polynomial.coeff_map]

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

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

Tactic:
| zero =>

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 : ι) (s : Multiset ι),
    ((∀ i ∈ s, (f i).Monic) → (Multiset.map f s).prod.Monic) →
      (∀ i ∈ a ::ₘ s, (f i).Monic) → (Multiset.map f (a ::ₘ s)).prod.Monic

Tactic:
intro a

Goal state after:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
a : ι
⊢ ∀ (s : Multiset ι),
    ((∀ i ∈ s, (f i).Monic) → (Multiset.map f s).prod.Monic) →
      (∀ i ∈ a ::ₘ s, (f i).Monic) → (Multiset.map f (a ::ₘ s)).prod.Monic
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
⊢ (φ p).natDegree = fu p.natDegree

Tactic:
refine induction_with_natDegree_le (fun p => (φ p).natDegree = fu p.natDegree)
    p.natDegree (by simp [fu0]) ?_ ?_ _ rfl.le
  · intro n r r0 _
    rw [natDegree_C_mul_X_pow _ _ r0, C_mul_X_pow_eq_monomial, φ_mon_nat _ _ r0]
  · intro f g fg _ fk gk
    rw [natDegree_add_eq_right_of_natDegree_lt fg, map_add]
    by_cases! FG : k ≤ f.natDegree
    · rw [natDegree_add_eq_right_of_natDegree_lt, gk]
      rw [fk, gk]
      exact fc FG fg
    · cases k
      · nomatch FG
      · rwa [φ_k FG, zero_add]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ #f.support = 0 → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin 0), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

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

Tactic:
rw [nextCoeff_multiset_prod]
  · simp only [nextCoeff_X_sub_C]
    exact t.sum_hom (-AddMonoidHom.id R)
  · intros
    apply monic_X_sub_C

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

Goal state before:
pp: case hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬∀ x ∈ Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) t), x = 0

Tactic:
Multiset.mem_map

Goal state after:
case hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬∀ (x : ℕ), (∃ a, (∃ a_1 ∈ t, X - C a_1 = a) ∧ a.natDegree = x) → x = 0
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
| zero =>

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) = x ^ n - y ^ n

Tactic:
by
  rw [← neg_sub (y ^ n), ← h.mul_neg_geom_sum₂, ← neg_mul, neg_sub]

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
m n : ℕ
hmn : m ≤ n
this : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ x ^ n - y ^ n - (x ^ m * y ^ (n - m) - y ^ n) = x ^ n - x ^ m * y ^ (n - m)

Tactic:
sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ n)

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

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

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ⊤.FG
s : Finset A
hs : span R ↑s = ⊤
⊢ ⊤ ≤ toSubmodule (Algebra.adjoin R ↑s)

Tactic:
← hs,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ⊤.FG
s : Finset A
hs : span R ↑s = ⊤
⊢ span R ↑s ≤ toSubmodule (Algebra.adjoin R ↑s)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.restriction.degree = p.degree

Tactic:
simp [degree]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I J : Ideal R[X]
⊢ ∀ r ∈ I.leadingCoeff, ∀ s ∈ J.leadingCoeff, r * s ∈ (I * J).leadingCoeff

Tactic:
intro a

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I J : Ideal R[X]
a : R
⊢ a ∈ I.leadingCoeff → ∀ s ∈ J.leadingCoeff, a * s ∈ (I * J).leadingCoeff
Module: Mathlib.RingTheory.Polynomial.Basic

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

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S))
⊢ m ∈ closure ↑S

Tactic:
adjoin_eq_span

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' ↑S))
⊢ m ∈ closure ↑S
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_1.zero
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
⊢ (↑↥A i) 0 ∈ M'

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_2.zero
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
⊢ (↑↥A f) 0 ∈ M'

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ (0 • x) • y = 0 • x • y

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_3.zero
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✝ : ↥M'
x : M
⊢ 0 ∈ ((↑↥A f).domRestrict N').range

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ 0 ≡ b ^ 0 [ZMOD n]

Tactic:
| zero =>

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

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

Tactic:
mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective

Goal state after:
case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hx : y ∈ ker f
hy : (Quotient.mk I) y = x
⊢ ∃ x ∈ ker f, (Quotient.mk I) x = (Quotient.mk I) y
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

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

Tactic:
mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective

Goal state after:
case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
hx : ∃ x_1 ∈ ker f, (Quotient.mk I) x_1 = x
⊢ x ∈ ker (Quotient.lift I f H)
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 : List α), a ~ m.toList → ∀ (b : List α), b ~ n.toList → a ≠ b

Tactic:
intro a

Goal state after:
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 : List α
⊢ a ~ m.toList → ∀ (b : List α), b ~ n.toList → a ≠ b
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
p : Ideal R
inst✝ : p.IsPrime
hIP : I ≤ p
⊢ (map (Quotient.mk I) p).IsPrime

Tactic:
apply Ideal.map_isPrime_of_surjective
  · exact Quotient.mk_surjective
  · simpa

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

Goal state before:
pp: case cons.H
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ ∀ (a : List α), g' (f (ys_hd :: a)) = f' (g ys_hd :: map g a)

Tactic:
intro a

Goal state after:
case cons.H
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
a : List α
⊢ g' (f (ys_hd :: a)) = f' (g ys_hd :: map g a)
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Injective fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩

Tactic:
intro a

Goal state after:
case refine_3
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
a : ↥(I ^ n) ⧸ I • ⊤
⊢ ∀ ⦃a₂ : ↥(I ^ n) ⧸ I • ⊤⦄,
    (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) a =
        (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) a₂ →
      a = a₂
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[n + minimalPeriod f x] x = f^[n] x

Tactic:
by
  rw [iterate_add_apply]
  congr
  exact isPeriodicPt_minimalPeriod f x

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

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[minimalPeriod f x * n / (minimalPeriod f x).gcd n] x = x

Tactic:
Nat.mul_div_assoc _ (gcd_dvd_right _ _),

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[minimalPeriod f x * (n / (minimalPeriod f x).gcd n)] x = x
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
y x d : α
h : x ≠ y
⊢ (y :: xs).nextOr x d = xs.nextOr x d

Tactic:
by
  rcases xs with - | ⟨z, zs⟩
  · rfl
  · exact if_neg h

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

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ n • a = a ↔ period g a ∣ n

Tactic:
pow_smul_eq_iff_period_dvd

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ period g a ∣ n ↔ period g a ∣ n
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ (n + 1) • a = a ↔ period g a ∣ n + 1

Tactic:
pow_smul_eq_iff_period_dvd

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ period g a ∣ n + 1 ↔ period g a ∣ n + 1
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case zero
α : Type u_1
ts : List α
h : ts.length < 0
⊢ ts.permutations ~ ts.permutations'

Tactic:
| zero =>

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

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℕ
⊢ a ^ n • b = b ↔ period a b ∣ n

Tactic:
pow_smul_eq_iff_period_dvd

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℕ
⊢ period a b ∣ n ↔ period a b ∣ n
Module: Mathlib.Data.List.Cycle

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

Tactic:
prev_eq_getElem_idxOf_pred_of_ne_head ha ha₀

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ (head :: tail)[idxOf a (head :: tail) - 1] =
    (head :: tail)[(idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length]
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (orbit M a).Subsingleton ↔ a ∈ fixedPoints M α

Tactic:
mem_fixedPoints

Goal state after:
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (orbit M a).Subsingleton ↔ ∀ (m : M), m • a = a
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons.zero
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hn : (a :: l).rotate 0 = b :: m
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
| zero =>

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

Goal state before:
pp: case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (a :: c :: s).rotate (d + 1) = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
· rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn
            rw [← hd c _ _ _ hn]
            simp [and_comm]

Goal state after:
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
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
⊢ r b c

Tactic:
simp only [mem_coe_iff, mem_cons] at hb hc

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
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b = a ∨ b ∈ l
hc : c = a ∨ c ∈ l
⊢ r b c
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n k : ℕ
⊢ ∀ {a : ℕ},
    (∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p) → List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)

Tactic:
intro a

Goal state after:
n k a : ℕ
⊢ (∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p) → List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ≤ 0

Tactic:
primeFactorsList_zero

Goal state after:
case inl
p : ℕ
h : p ∈ []
⊢ p ≤ 0
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+~ ((hn + 1) * k).primeFactorsList

Tactic:
simp only [(perm_primeFactorsList_mul (Nat.succ_ne_zero _) h).subperm_left]

Goal state after:
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+~ hn.succ.primeFactorsList ++ k.primeFactorsList
Module: Mathlib.Data.Nat.PrimeFin

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

Tactic:
| zero =>

Goal state after: