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

Goal state before:
pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ ((((optionEquivLeft R S₁) p).coeff i).support.sup fun s ↦ s.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
Finset.sup_le_iff

Goal state after:
case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ ∀ b ∈ (((optionEquivLeft R S₁) p).coeff i).support, (b.sum fun x e ↦ e) ≤ p.totalDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.trailingCoeff = f.leadingCoeff

Tactic:
by
  rw [trailingCoeff, natTrailingDegree_reverse, coeff_zero_reverse]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
hn : (p ^ n).natDegree = n * p.natDegree
⊢ (p ^ n * p).natDegree = (n + 1) * p.natDegree

Tactic:
(hp.pow n).natDegree_mul hp,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
hn : (p ^ n).natDegree = n * p.natDegree
⊢ (p ^ n).natDegree + p.natDegree = (n + 1) * p.natDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ WithBot.unbotD 0 ↑(degreeOf 0 f) = degreeOf 0 f

Tactic:
WithBot.unbotD_coe

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ degreeOf 0 f = degreeOf 0 f
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ ((((finSuccEquiv R n) p).coeff i).support.sup fun m ↦ m j) ≤ p.support.sup fun m ↦ m j.succ

Tactic:
Finset.sup_le_iff

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ ∀ b ∈ (((finSuccEquiv R n) p).coeff i).support, b j ≤ p.support.sup fun m ↦ m j.succ
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
h✝ : (∑ x_1, if i = k x_1 then x x_1 else 0) ≠ 0
j : Fin n
left✝ : j ∈ univ
h : (if i = k j then x j else 0) ≠ 0
⊢ ∃ a, k a = i

Tactic:
exact ⟨j, (ite_ne_right_iff.mp h).1.symm⟩

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
⊢ t.prod.Monic

Tactic:
by simpa using monic_multiset_prod_of_monic _ _ h

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ p.degree < (X ^ n).degree

Tactic:
simp [mem_degreeLT.1 hp]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < ⊥
hp_zero : p = 0
x : R[X]
hx : x ∈ s
⊢ False

Tactic:
exact not_lt_bot (h x hx)

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

Goal state before:
pp: case inl
x y n : ℕ
h : y ≤ x
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
have : y ^ n ≤ x ^ n := Nat.pow_le_pow_left h _
    exact mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n

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

Goal state before:
pp: m x y n : ℕ
⊢ x ^ m - y ^ m ∣ x ^ (m * n) - y ^ (m * n)

Tactic:
simpa [pow_mul] using (x ^ m).sub_dvd_pow_sub_pow (y ^ m) n

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

Goal state before:
pp: case inr.inr
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)
yi : C
hyi : yi ∈ ↑y
yj : C
hyj : yj ∈ ↑y
⊢ yi * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

Tactic:
rw [← hf (yi * yj)]

Goal state after:
case inr.inr
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)
yi : C
hyi : yi ∈ ↑y
yj : C
hyj : yj ∈ ↑y
⊢ ∑ a ∈ y, f (yi * yj) a • 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.coeff (WithBot.unbotD 0 ↑n) = p.coeff n

Tactic:
WithBot.unbotD_coe

Goal state after:
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.coeff n = p.coeff n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ∀ {x y : R[X]}, x * y ∈ map C P → x ∈ map C P ∨ y ∈ map C P

Tactic:
· intro f g
      simp only [mem_map_C_iff]
      contrapose!
      rintro ⟨hf, hg⟩
      classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        rw [coeff_mul, ← Finset.insert_erase ((Finset.mem_antidiagonal (a := (m, n))).mpr rfl),
          Finset.sum_insert (Finset.notMem_erase _ _), (P.add_mem_iff_left _).not]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          lia
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ adjoin R (of' R M '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤

Tactic:
suffices of' R M '' ⋃ f ∈ S, (f.coeff.support : Set M) = ⋃ f ∈ S, of' R M '' f.coeff.support by
    rw [this]
    exact support_gen_of_gen hS

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ of' R M '' ⋃ f ∈ S, ↑f.coeff.support = ⋃ f ∈ S, of' R M '' ↑f.coeff.support
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁)) 1 *
      single (Multiplicative.toAdd (Multiplicative.ofAdd m₂)) 1 =
    single (Multiplicative.toAdd (Multiplicative.ofAdd (m₁ + m₂))) 1

Tactic:
single_mul_single,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁) + Multiplicative.toAdd (Multiplicative.ofAdd m₂)) (1 * 1) =
    single (Multiplicative.toAdd (Multiplicative.ofAdd (m₁ + m₂))) 1
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁)) 1 *
      single (Multiplicative.toAdd (Multiplicative.ofAdd m₂)) 1 =
    single (Multiplicative.toAdd (Multiplicative.ofAdd (m₁ + m₂))) 1

Tactic:
single_mul_single,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁) + Multiplicative.toAdd (Multiplicative.ofAdd m₂)) (1 * 1) =
    single (Multiplicative.toAdd (Multiplicative.ofAdd (m₁ + m₂))) 1
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single m₁ 1 * single m₂ 1 = single (m₁ * m₂) 1

Tactic:
single_mul_single,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single (m₁ * m₂) (1 * 1) = single (m₁ * m₂) 1
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single m₁ 1 * single m₂ 1 = single (m₁ * m₂) 1

Tactic:
single_mul_single,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ single (m₁ * m₂) (1 * 1) = single (m₁ * m₂) 1
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]

Tactic:
obtain hc | rfl | hc := lt_trichotomy c 0

Goal state after:
case inl
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ c * a ≡ c * b [ZMOD c * n]

case inr.inl
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 * a ≡ 0 * b [ZMOD 0 * n]

case inr.inr
n a b c : ℤ
h : a ≡ b [ZMOD n]
hc : 0 < c
⊢ c * a ≡ c * b [ZMOD c * n]
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case inr.inl.inr.inr
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : 1 = -1
⊢ 1 = -1

pp: case inr.inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : -1 = 1
⊢ -1 = 1

Tactic:
· exact ((Ring.neg_one_ne_one_of_char_ne_two hR).symm h).elim

Goal state after:
case inr.inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : -1 = 1
⊢ -1 = 1
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case inl_add_inr
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : f (Unitization.inl r + ↑a) = 0
⊢ Unitization.inl r + ↑a = 0

Tactic:
simp_rw [map_add, hf, ← Unitization.algebraMap_eq_inl, AlgHomClass.commutes] at hx

Goal state after:
case inl_add_inr
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r + ↑a = 0
⊢ Unitization.inl r + ↑a = 0
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ n.Coprime m

Tactic:
by
  rw [← not_not (a := n.Coprime m), Prime.not_coprime_iff_dvd]
  push Not
  exact fun p hp hn hm ↦
    ((le_of_dvd (by lia) hm).trans_lt <| h.trans_le <| minFac_le_of_dvd hp.two_le hn).false

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

Goal state before:
pp: case h
α : Type u_1
l a✝ : List α
⊢ l ∈ lists ⟦a✝⟧ ↔ ⟦a✝⟧ = ⟦l⟧

Tactic:
simpa using perm_comm

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
h : IsPeriodicPt f n x
m : ℕ
| f^[m % n + n * (m / n)] x

Tactic:
iterate_add_apply,

Goal state after:
α : Type u_1
f : α → α
x : α
n : ℕ
h : IsPeriodicPt f n x
m : ℕ
| f^[m % n] (f^[n * (m / n)] x)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.e_a.e_b
α : 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' x✝ : List α
⊢ (permutationsAux2 t (is ++ ts) [] x✝ id).snd = map (fun x ↦ x ++ ts) (permutationsAux2 t is [] x✝ id).snd

Tactic:
rw [map_permutationsAux2]

Goal state after:
case cons.e_a.e_b
α : 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' x✝ : List α
⊢ (permutationsAux2 t (is ++ ts) [] x✝ id).snd = (permutationsAux2 t is [] x✝ fun x ↦ x ++ ts).snd
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case pos
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ IsPeriodicPt f (Nat.find hx) x

pp: case neg
α : Type u_1
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ IsPeriodicPt f 0 x

Tactic:
· exact (Nat.find_spec hx).2

Goal state after:
case neg
α : Type u_1
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ IsPeriodicPt f 0 x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → α
x : α
g : β → β
y : β
⊢ minimalPeriod f x = minimalPeriod g y ↔ ∀ (n : ℕ), IsPeriodicPt f n x ↔ IsPeriodicPt g n y

Tactic:
simp_rw [isPeriodicPt_iff_minimalPeriod_dvd, dvd_right_iff_eq]

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

Goal state before:
pp: case inl.nil
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ (∃ is' x, l₁ ++ [t] ++ ts = is' ++ t :: ts) ∨
    l₁ ++ [t] ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ [t] ++ ts = l₁_1 ++ t :: l₂ ++ ts

pp: case inl.cons
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ (∃ is' x, l₁ ++ t :: a :: l₂' ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: a :: l₂' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁_1 ++ t :: l₂ ++ ts

Tactic:
· exact Or.inl ⟨l₁, by simpa using p⟩

Goal state after:
case inl.cons
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ (∃ is' x, l₁ ++ t :: a :: l₂' ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: a :: l₂' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁_1 ++ t :: l₂ ++ ts
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (if x = y then z else (z :: l).nextOr x ((y :: z :: l).get ⟨0, ⋯⟩)) = z

Tactic:
if_pos hx

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ z = z
Module: Mathlib.Data.List.Permutation

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

Tactic:
by rwa [length_reverse]

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

Goal state before:
pp: case cons.right.inl
α : 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
hx' : (bs.insertIdx m x)[n] = x
ht : n < m
⊢ False

Tactic:
suffices x ∈ bs by exact h x (hb.subset this) rfl
        rw [← hx', getElem_insertIdx_of_lt ht]
        exact getElem_mem _

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
⊢ MulAction.stabilizer Rˣ x = ⊥

Tactic:
eq_bot_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
⊢ MulAction.stabilizer Rˣ x ≤ ⊥
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.next hs x hx ∈ s

Tactic:
by
  induction s using Quot.inductionOn
  apply next_mem; assumption

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:
← hb.prod_eq

Goal state after:
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 = (b :: l₂).prod
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
J K : Subgroup G'
hJK : J.relIndex K ≠ 0
⊢ (comap f J).relIndex (comap f K) ≠ 0

Tactic:
by
  rw [relIndex_comap]
  exact fun h ↦ hJK <| relIndex_eq_zero_of_le_right (map_comap_le _ _) h

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = 0
hn : n = 0
⊢ False

Tactic:
exact (Fintype.card_eq_zero_iff.mp h).elim' 0

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a b c : ℕ
hab : a = b
hbc : b = c
⊢ (ringEquivCongr hab).trans (ringEquivCongr hbc) = ringEquivCongr ⋯

Tactic:
subst hab hbc
  cases a <;> rfl

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

Goal state before:
pp: case h₁
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i ≤ x

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0

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

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

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
hn : 1 < n
⊢ ∀ (n : ℕ),
    2 ≤ n →
      0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1 →
        0 < ∑ i ∈ range (n + 1), x ^ i ∧ ∑ i ∈ range (n + 1), x ^ i < 1

Tactic:
· rw [geom_sum_two]
    exact ⟨hx', (add_lt_iff_neg_right _).2 hx⟩

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
hn : 1 < n
⊢ ∀ (n : ℕ),
    2 ≤ n →
      0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1 →
        0 < ∑ i ∈ range (n + 1), x ^ i ∧ ∑ i ∈ range (n + 1), x ^ i < 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ map { toFun := fun d ↦ (n / d, d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal

Tactic:
apply Finset.map_injective (Equiv.prodComm _ _).toEmbedding
  ext
  rw [map_swap_divisorsAntidiagonal, ← map_div_right_divisors, Finset.map_map]
  simp

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

Goal state before:
pp: case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ ∑ i ∈ Ico 1 0, a / b ^ i ≤ a / (b - 1)

pp: case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a / (b - 1)

Tactic:
· rw [Ico_eq_empty_of_le (by lia), sum_empty]
    exact Nat.zero_le _

Goal state after:
case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a / (b - 1)
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ n.centralBinom < 2 ^ (2 * n)

Tactic:
apply choose_lt_two_pow

Goal state after:
n : ℕ
h : n ≠ 0
⊢ 0 < 2 * n
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
⊢ 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * ((2 * n + 1) * (2 * n).choose n)

Tactic:
mul_comm (2 * n + 1)

Goal state after:
n : ℕ
⊢ 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * ((2 * n).choose n * (2 * n + 1))