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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : Multiset σ
k : ℕ
⊢ degreesLE R σ ((k + 1) • s) = degreesLE R σ s ^ (k + 1)

Tactic:
by simp only [pow_succ, degreesLE_nsmul, degreesLE_add, add_smul, one_smul]

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 : p.natTrailingDegree ≤ i
hj : j < q.natTrailingDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rw [coeff_eq_zero_of_lt_natTrailingDegree hj, mul_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.nextCoeff ≠ 0
⊢ 0 < p.natDegree

Tactic:
by
  grind [nextCoeff]

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p.coeff 1 = 0
⊢ False

Tactic:
← hp,

Goal state after:
case refine_1
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
h : p.coeff p.natDegree = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
simp only [Ne, mul_eq_zero, leadingCoeff_eq_zero, p0, natDegree_comp_eq_of_mul_ne_zero,
        ne_zero_of_natDegree_gt (Nat.pos_of_ne_zero q0), not_false_eq_true, pow_ne_zero, or_self]

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ Polynomial.C (C r) * (Polynomial.X ^ m none * m.some.prod fun a k ↦ Polynomial.C (X a) ^ k) =
    Polynomial.C (C r) * (Polynomial.C (m.some.prod fun n e ↦ X n ^ e) * Polynomial.X ^ m none)

Tactic:
simp only [mul_comm, map_finsuppProd, map_pow]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this✝ : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).leadingCoeff = 1

Tactic:
leadingCoeff_mul' this,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this✝ : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : MonicDegreeEq R n
f : R →+* S
⊢ (Polynomial.map f ↑p).coeff n = 1 ∧ ∀ i > n, (Polynomial.map f ↑p).coeff i = 0

Tactic:
by simp +contextual [coeff_map, p.2]

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

Goal state before:
pp: case succ.refine_1
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
i : Fin (n + 1)
⊢ ∀ ⦃b : Fin (n + 1)⦄,
    i < b →
      Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i < Function.extend Fin.castSucc k (fun x ↦ f.natDegree) b

Tactic:
j

Goal state after:
case succ.refine_1
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
i j : Fin (n + 1)
⊢ i < j →
    Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i < Function.extend Fin.castSucc k (fun x ↦ f.natDegree) j
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ 1 - x ∣ 1 - x ^ n

Tactic:
conv_rhs => rw [← one_pow n]

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ 1 - x ∣ 1 ^ n - x ^ n
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ x - 1 ∣ x ^ n - 1

Tactic:
conv_rhs => rw [← one_pow n]

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ x - 1 ∣ x ^ n - 1 ^ n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
⊢ (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

Tactic:
by
  by_cases hq : q = 0
  · suffices 0 < p.natDegree ↔ p.natDegree ≠ 0 by simp [hq, ← h.natDegree_eq_zero, iffComm]
    exact ⟨fun h => h.ne', fun h => lt_of_le_of_ne (Nat.zero_le _) h.symm⟩
  · simp [h.natDegree_mul', hq]

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

Goal state before:
pp: case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : q * p = r * p
⊢ q - r = 0

Tactic:
← hp.mul_left_eq_zero_iff,

Goal state after:
case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : q * p = r * p
⊢ (q - r) * p = 0
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
⊢ (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)

Tactic:
have :
    ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) =
      ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)) := by
    refine sum_congr rfl fun j j_in => ?_
    rw [← pow_add]
    congr
    rw [mem_range] at j_in
    lia

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 - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.refine_3.hb
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
⊢ ¬∃ a, a.castSucc = Fin.last n

pp: case succ.refine_3.hb
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
⊢ ¬∃ a, a.castSucc = Fin.last n

Tactic:
all_goals exact H

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

Goal state before:
pp: case refine_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ span R (p * q) ≤ Subalgebra.toSubmodule (adjoin R (s ∪ t))

Tactic:
span_le,

Goal state after:
case refine_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ p * q ⊆ ↑(Subalgebra.toSubmodule (adjoin R (s ∪ t)))
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
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)
⊢ span (↥(Algebra.adjoin A ↑s)) (↑(insert 1 y) * ↑(insert 1 y)) ≤ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)

Tactic:
span_le,

Goal state after:
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
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)
⊢ ↑(insert 1 y) * ↑(insert 1 y) ⊆ ↑(span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case H
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
i : ℕ
⊢ ∀ (y : ℕ),
    ∃ z,
      (fun x1 x2 ↦ x1 ≤ x2) ((fun n ↦ I.leadingCoeffNth n) i) ((fun n ↦ I.leadingCoeffNth n) z) ∧
        (fun x1 x2 ↦ x1 ≤ x2) ((fun n ↦ I.leadingCoeffNth n) y) ((fun n ↦ I.leadingCoeffNth n) z)

Tactic:
j

Goal state after:
case H
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
i j : ℕ
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) ((fun n ↦ I.leadingCoeffNth n) i) ((fun n ↦ I.leadingCoeffNth n) z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) ((fun n ↦ I.leadingCoeffNth n) j) ((fun n ↦ I.leadingCoeffNth n) z)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I J : Ideal R[X]
a : R
ha : a ∈ I.leadingCoeff
b : R
hb : b ∈ J.leadingCoeff
p : R[X]
hpI : p ∈ I
hp : p.leadingCoeff = a
⊢ a * b ∈ (I * J).leadingCoeff

Tactic:
rcases (J.mem_leadingCoeff b).1 hb with ⟨q, hqJ, hq⟩

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I J : Ideal R[X]
a : R
ha : a ∈ I.leadingCoeff
b : R
hb : b ∈ J.leadingCoeff
p : R[X]
hpI : p ∈ I
hp : p.leadingCoeff = a
q : R[X]
hqJ : q ∈ J
hq : q.leadingCoeff = b
⊢ a * b ∈ (I * J).leadingCoeff
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
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ f.coeff (m, n).1 ∉ P ∧ g.coeff (m, n).2 ∉ P

Tactic:
exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩

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

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

Tactic:
j

Goal state after:
R✝ : Type u
S : Type v
F : Type w
inst✝³ : Ring R✝
inst✝² : Semiring S
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
i j : Fin 2
⊢ i ≠ j → (IsCoprime on f) i j
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
⊢ 5 ≤ p

Tactic:
by_contra! h
  revert h_two h_three hp
  decide +revert

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
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
⊢ x = p ∧ y = p

Tactic:
by
    obtain hx | hy := hp.dvd_mul.1 pdvdxy <;>
      [skip; rw [And.comm]] <;>
      [skip; rw [mul_comm] at h pdvdxy] <;>
      apply this <;>
      assumption

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

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
x : A ⧸ ker f
⊢ f.kerLift (r • x) = r • f.kerLift x

Tactic:
obtain ⟨a, rfl⟩ := Quotient.mkₐ_surjective R₁ _ x
  exact _root_.map_smul f _ _

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

Goal state before:
pp: R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Surjective ⇑f
g : A →ₐ[R] C
H : ker f.toRingHom ≤ ker g.toRingHom
x : A
⊢ (f.liftOfSurjective hf g H) (f x) = g x

Tactic:
dsimp [AlgHom.liftOfSurjective]

Goal state after:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Surjective ⇑f
g : A →ₐ[R] C
H : ker f.toRingHom ≤ ker g.toRingHom
x : A
⊢ (Quotient.lift (ker ↑f) (↑g) H) (↑(quotientKerAlgEquivOfSurjective hf).symm (f x)) = g x
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : Type u_1
l : Finset α
⊢ l.val.lists.Nodup

Tactic:
have h_nodup : l.val.Nodup := l.nodup
  rw [← Finset.coe_toList l, Multiset.coe_nodup] at h_nodup
  rw [← Finset.coe_toList l]
  exact nodup_permutations l.val.toList (h_nodup)

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✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R ↑(centralizer R s)) = (s ∪ star s).centralizer.centralizer

Tactic:
by
  rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]

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

Goal state before:
pp: α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
⊢ 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:
have :
    (∃ a : List α,
        a ∈ L ∧ ∃ l₁ l₂ : List α, ¬l₂ = nil ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
      ∃ l₁ l₂ : List α, ¬l₂ = nil ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts) :=
    ⟨fun ⟨_, aL, l₁, l₂, l0, e, h⟩ => ⟨l₁, l₂, l0, e ▸ aL, h⟩, fun ⟨l₁, l₂, l0, aL, h⟩ =>
      ⟨_, aL, l₁, l₂, l0, rfl, h⟩⟩
  rw [foldr_permutationsAux2]
  simp only [mem_permutationsAux2', ← this, or_comm, and_left_comm, mem_append, mem_flatMap,
    append_assoc, cons_append]

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

Goal state before:
pp: case h
α : Type u_1
f : α → α
x : α
n : ℕ
left✝ : n > 0
h : IsPeriodicPt f n x
⊢ f^[1] (f^[n - 1] x) = x

Tactic:
← iterate_add_apply,

Goal state after:
case h
α : Type u_1
f : α → α
x : α
n : ℕ
left✝ : n > 0
h : IsPeriodicPt f n x
⊢ f^[1 + (n - 1)] x = x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case e'_2
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)

Tactic:
← iterate_add_apply,

Goal state after:
case e'_2
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n + n] x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case e'_3
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)

Tactic:
← iterate_add_apply,

Goal state after:
case e'_3
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n + n] x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
n : ℕ
hn : n ∈ List.range (minimalPeriod f x)
hmn : f^[m] x = f^[n] x
⊢ m = n

Tactic:
List.mem_range

Goal state after:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : m < minimalPeriod f x
n : ℕ
hn : n < minimalPeriod f x
hmn : f^[m] x = f^[n] x
⊢ m = n
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case inr
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
h' : Finite (Quotient (rightRel H))
⊢ Finite (orbitRel.Quotient (↥H) X)

Tactic:
let f : Quotient (rightRel H) → orbitRel.Quotient H X :=
      fun a ↦ Quotient.liftOn' a (fun g ↦ ⟦g • b⟧) fun g₁ g₂ r ↦ by
        replace r := Setoid.symm' _ r
        rw [rightRel_eq] at r
        simp only [Quotient.eq, orbitRel_apply, mem_orbit_iff]
        exact ⟨⟨g₁ * g₂⁻¹, r⟩, by simp [mul_smul]⟩

Goal state after:
case inr
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
h' : Finite (Quotient (rightRel H))
f : Quotient (rightRel H) → orbitRel.Quotient (↥H) X := fun a ↦ a.liftOn' (fun g ↦ ⟦g • b⟧) ⋯
⊢ Finite (orbitRel.Quotient (↥H) X)
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : G ⧸ H
⊢ ∀ (a b : G), (leftRel H) a b → ⟦a⁻¹ • x⟧ = ⟦b⁻¹ • x⟧

Tactic:
intro g₁ g₂ h

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : G ⧸ H
g₁ g₂ : G
h : (leftRel H) g₁ g₂
⊢ ⟦g₁⁻¹ • x⟧ = ⟦g₂⁻¹ • x⟧
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_2
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → _root_.Prime p

Tactic:
simp_rw [← prime_iff]
    exact h₂

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

Goal state before:
pp: case refine_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.primeFactorsList.prod * b.primeFactorsList.prod = a * b

Tactic:
prod_primeFactorsList ha,

Goal state after:
case refine_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b.primeFactorsList.prod = a * b
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p a b : ℕ
hpa : p ∈ a.primeFactorsList
hb : b ≠ 0
⊢ p ∈ (a * b).primeFactorsList

Tactic:
by
  rcases eq_or_ne a 0 with (rfl | ha)
  · simp at hpa
  apply (mem_primeFactorsList_mul ha hb).2 (Or.inl hpa)

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, a * b ∈ 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), a * b ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ z.cast = z

Tactic:
cast_id

Goal state after:
case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ z = z
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : Fact (1 < n)
⊢ val 1 = 1

Tactic:
by
  rw [val_one_eq_one_mod]
  exact Nat.mod_eq_of_lt Fact.out

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

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

Tactic:
have hx0 : x ≤ 0 := (le_add_of_nonneg_right zero_le_one).trans hx

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
n : ℕ
hx0 : x ≤ 0
⊢ if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ (p ^ k).divisors ↔ a ∈ map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range (k + 1))

Tactic:
rw [mem_divisors_prime_pow pp]

Goal state after:
p : ℕ
pp : Prime p
k a : ℕ
⊢ (∃ j ≤ k, a = p ^ j) ↔ a ∈ map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range (k + 1))
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
hf : f ↑n = 0
x : ℤ
⊢ (fun x ↦ x • ↑n) x ∈ f.ker

Tactic:
simp only [f.map_zsmul, zsmul_zero, f.mem_ker, hf]

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

Goal state before:
pp: case cons.w₁
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
l : ℕ
m : l ∈ L
⊢ l ∈ d :: L

Tactic:
exact List.mem_cons_of_mem _ m

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

Goal state before:
pp: case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
← sum_range_add_sum_Ico _ <| h₁,

Goal state after:
case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) *
      (∑ k ∈ range 1, ofDigits p (List.drop k tl) + ∑ k ∈ Ico 1 tl.length, ofDigits p (List.drop k tl) +
        ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl
p n : ℕ
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
rcases eq_or_ne n 0 with rfl | hn
    · simp
    · convert!
      sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn) <|
        (fun l a ↦ digits_lt_base h a)
      · refine (length_digits p n h hn).symm
      all_goals exact (ofDigits_digits p n).symm

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

Goal state before:
pp: case bit.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit false n) = List.map (fun b ↦ bif b then 1 else 0) (false :: n.bits)

Tactic:
digits_def' one_lt_two

Goal state after:
case bit.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ bit false n % 2 :: digits 2 (bit false n / 2) = List.map (fun b ↦ bif b then 1 else 0) (false :: n.bits)

case bit.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ 0 < bit false n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
| (↑d % ↑k + b' * ofDigits b' L % ↑k) % ↑k

Tactic:
Int.mul_emod

Goal state after:
b b' : ℤ
k : ℕ
h : b % ↑k = b' % ↑k
d : ℕ
L : List ℕ
ih : ofDigits b L % ↑k = ofDigits b' L % ↑k
| (↑d % ↑k + b' % ↑k * (ofDigits b' L % ↑k) % ↑k) % ↑k