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

Goal state before:
pp: case refine_2
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
j : Fin n
⊢ x j ≠ 0

pp: case refine_2
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
j : Fin n
⊢ ∀ b ∈ univ, b ≠ j → (if k j = k b then x b else 0) = 0

Tactic:
· exact hx j

Goal state after:
case refine_2
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
j : Fin n
⊢ ∀ b ∈ univ, b ≠ j → (if k j = k b then x b else 0) = 0
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
this : t.prod ≠ 0
⊢ ↑(Multiset.map natDegree t).sum = (Multiset.map degree t).sum

Tactic:
Nat.cast_multiset_sum,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
this : t.prod ≠ 0
⊢ (Multiset.map Nat.cast (Multiset.map natDegree t)).sum = (Multiset.map degree t).sum
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

Tactic:
let f : ℕ → ℕ → R := fun m i : ℕ => (x + y) ^ i * y ^ (m - 1 - i)

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
hp : (map f p).Monic
⊢ (map f p).leadingCoeff = f 1

Tactic:
hp.leadingCoeff,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
hp : (map f p).Monic
⊢ 1 = f 1
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
⊢ ∏ i ∈ s, (f i).leadingCoeff ≠ 0

Tactic:
prod_ne_zero_iff

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
⊢ ∀ a ∈ s, (f a).leadingCoeff ≠ 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
hx✝ : g ∈ Submodule.span R[X] (⇑C '' ↑I)
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ ∑ x ∈ antidiagonal n, f.coeff x.1 * g.coeff x.2 ∈ I

Tactic:
exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
H : ∀ (i : ι), ∃ n, s i ^ n • x ∈ S'
this : x ∈ toSubmodule (ofId (↥S') S).range
⊢ x ∈ S'

Tactic:
obtain ⟨x, rfl⟩ := this

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : ↥S'
H : ∀ (i : ι), ∃ n, s i ^ n • (ofId (↥S') S).toRingHom x ∈ S'
⊢ (ofId (↥S') S).toRingHom x ∈ S'
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf : f✝ ∈ Ideal.map C I
f g : MvPolynomial σ R
hx✝ : g ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I)
hg : ∀ (m : σ →₀ ℕ), coeff m g ∈ I
n : σ →₀ ℕ
⊢ ∑ x ∈ antidiagonal n, coeff x.1 f * coeff x.2 g ∈ I

Tactic:
exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)

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

Goal state before:
pp: n a b : ℤ
m : ℕ
h : a ≡ b [ZMOD n]
⊢ a ^ m ≡ b ^ m [ZMOD n]

Tactic:
induction m with

Goal state after:
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 : (algebraMap R A) r + ↑a = 0
⊢ Unitization.inl r + ↑a = 0

Tactic:
rw [add_eq_zero_iff_eq_neg] 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
⊢ Unitization.inl r = -↑a
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : 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)
⊢ map g' (permutationsAux2 t ts r (ys_hd :: tail✝) f).snd =
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g (ys_hd :: tail✝)) f').snd

Tactic:
simp only [map, permutationsAux2_snd_cons, cons_append, cons.injEq]

Goal state after:
case cons
α : 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)
⊢ g' (f (t :: ys_hd :: (tail✝ ++ ts))) = f' (g t :: g ys_hd :: (map g tail✝ ++ map g ts)) ∧
    map g' (permutationsAux2 t ts r tail✝ fun x ↦ f (ys_hd :: x)).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) fun x ↦ f' (g ys_hd :: x)).snd
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
x✝¹ x✝ : StarSubalgebra R A
⊢ x✝¹.toNonUnitalStarSubalgebra = x✝.toNonUnitalStarSubalgebra → x✝¹ = x✝

Tactic:
simp [SetLike.ext_iff]

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
S : Subalgebra R A
x y : A
hx : x ∈ star S.carrier
hy : y ∈ star S.carrier
⊢ x + y ∈ star S.carrier

Tactic:
by
        simp only [Set.mem_star, Subalgebra.mem_carrier] at *
        exact (star_add x y).symm ▸ add_mem hx hy

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 (f^[n - 1] x) = x

Tactic:
nth_rw 1 [← iterate_one f]

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

Goal state before:
pp: case pos.refine_1.inl
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n = minimalPeriod f x - succ 0
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x] x)

Tactic:
iterate_minimalPeriod

Goal state after:
case pos.refine_1.inl
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n = minimalPeriod f x - succ 0
⊢ r (f^[minimalPeriod f x - succ 0] x) x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
⊢ (fun x ↦ m • x)^[minimalPeriod (fun x ↦ m • x) a] a = a

Tactic:
iterate_minimalPeriod

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
⊢ a = a
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ s.length < (permutations'Aux x t).length

Tactic:
by simp [hl]

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

Goal state before:
pp: α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ (permutations'Aux x s).get ⟨k, kl⟩ = (permutations'Aux x s).get ⟨k + 1, k1l⟩

Tactic:
rw [get_permutations'Aux, get_permutations'Aux]

Goal state after:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ s.insertIdx k x = s.insertIdx (k + 1) x
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ ∀ (i : ℕ) (h₁ : i < (pmap l.next l ⋯).length) (h₂ : i < (l.rotate 1).length), (pmap l.next l ⋯)[i] = (l.rotate 1)[i]

Tactic:
intros
    rw [getElem_pmap, getElem_rotate, next_getElem _ h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ (∀ (x : α), (swap a b) x ∈ S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)

Tactic:
swap_apply_def

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ (∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ (∀ g ∈ H, g • s ⊆ s) → H ≤ stabilizer G s

Tactic:
intro hyp g hg
    rw [mem_stabilizer_iff]
    apply subset_antisymm (hyp g hg)
    intro x hx
    use g⁻¹ • x
    constructor
    · apply hyp g⁻¹ (inv_mem hg)
      simp only [Set.smul_mem_smul_set_iff, hx]
    · simp only [smul_inv_smul]

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
g : Rˣ
hg : ↑g • x = x
⊢ (↑g - 1) • x = 0

Tactic:
sub_smul,

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
g : Rˣ
hg : ↑g • x = x
⊢ ↑g • x - 1 • x = 0
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Chain r Cycle.nil

Tactic:
trivial

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

Goal state before:
pp: case nil
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ Cycle.nil
⊢ Chain r₂ Cycle.nil

Tactic:
trivial

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

Goal state before:
pp: k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ (k + 2).primeFactorsList.prod = k + 2

Tactic:
have h₁ : (k + 2) / m ≠ 0 := fun h => by
        have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
        rw [zero_mul] at this; exact (show k + 2 ≠ 0 by simp) this
      rw [primeFactorsList, List.prod_cons, prod_primeFactorsList h₁,
        Nat.mul_div_cancel' (minFac_dvd _)]

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

Goal state before:
pp: p : ℕ
hp : Prime p
this✝ : p = p - 2 + 2
this : p.minFac = p
⊢ p.minFac :: (p / p.minFac).primeFactorsList = [p]

Tactic:
simp only [this, primeFactorsList, Nat.div_self (Nat.Prime.pos hp)]

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

Goal state before:
pp: n : ℕ
⊢ n.primeFactors = ∅ ↔ n ≤ 1

Tactic:
rw [primeFactors_eq_empty, Nat.le_one_iff_eq_zero_or_eq_one]

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

Goal state before:
pp: n k : ℕ
h : n ∣ k
h' : k ≠ 0
⊢ n.primeFactorsList <+ k.primeFactorsList

Tactic:
by
  obtain ⟨a, rfl⟩ := h
  exact primeFactorsList_sublist_right (right_ne_zero_of_mul h')

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
⊢ ∀ (x y : G'), x⁻¹ * y ∈ comap f H ↔ (f x)⁻¹ * f y ∈ H

Tactic:
exact fun x y => iff_of_eq (congr_arg (· ∈ H) (by rw [f.map_mul, f.map_inv]))

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Surjective (Quotient.map' ⇑f ⋯)

Tactic:
refine Quotient.ind' fun x => ?_
    obtain ⟨y, hy⟩ := hf x
    exact ⟨y, (Quotient.map'_mk'' f _ y).trans (congr_arg Quotient.mk'' hy)⟩

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.val = a

Tactic:
cases n
  · cases NeZero.ne 0 rfl
  · apply Fin.cast_val_eq_self

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

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

Tactic:
rw [← ringEquivCongr_trans hab hbc]

Goal state after:
a b c : ℕ
hab : a = b
hbc : b = c
x : ZMod a
⊢ (ringEquivCongr hbc) ((ringEquivCongr hab) x) = ((ringEquivCongr hab).trans (ringEquivCongr hbc)) x
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝ : NeZero (m * n)
this : NeZero m
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun

Tactic:
have : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩

Goal state after:
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
k p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ (p ^ k).divisors, f x = ∏ x ∈ range (k + 1), f (p ^ x)

Tactic:
by
  simp [h, divisors_prime_pow]

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

Goal state before:
pp: m n : ℕ
a : ZMod n
ilt : Fact (1 < n)
h : a.val ^ m < n
⊢ (a ^ m).val = a.val ^ m

Tactic:
induction m with

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

Goal state before:
pp: m n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
⊢ (a ^ m).val ≤ a.val ^ m

Tactic:
induction m with

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

Goal state before:
pp: n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ f ↑n = 0 ↔ (Int.castAddHom (ZMod n)).ker ≤ f.ker

Tactic:
ker_intCastAddHom

Goal state after:
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ f ↑n = 0 ↔ AddSubgroup.zmultiples ↑n ≤ f.ker
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b m : ℕ
hm : m ≠ 0
⊢ (b.digits m).getLast ⋯ ≠ 0

Tactic:
rcases b with (_ | _ | b)

Goal state after:
case zero
m : ℕ
hm : m ≠ 0
⊢ (digits 0 m).getLast ⋯ ≠ 0

case succ.zero
m : ℕ
hm : m ≠ 0
⊢ ((0 + 1).digits m).getLast ⋯ ≠ 0

case succ.succ
m : ℕ
hm : m ≠ 0
b : ℕ
⊢ ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b m : ℕ
hb : 1 < b
⊢ m ≠ 0 → b ^ (b.digits m).length ≤ b * m

Tactic:
rcases b with (_ | _ | b)

Goal state after:
case zero
m : ℕ
hb : 1 < 0
⊢ m ≠ 0 → 0 ^ (digits 0 m).length ≤ 0 * m

case succ.zero
m : ℕ
hb : 1 < 0 + 1
⊢ m ≠ 0 → (0 + 1) ^ ((0 + 1).digits m).length ≤ (0 + 1) * m

case succ.succ
m b : ℕ
hb : 1 < b + 1 + 1
⊢ m ≠ 0 → (b + 1 + 1) ^ ((b + 1 + 1).digits m).length ≤ (b + 1 + 1) * m
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b m d : ℕ
hb : 1 < b
hd : d ∈ b.digits m
⊢ d < b

Tactic:
rcases b with (_ | _ | b)

Goal state after:
case zero
m d : ℕ
hb : 1 < 0
hd : d ∈ digits 0 m
⊢ d < 0

case succ.zero
m d : ℕ
hb : 1 < 0 + 1
hd : d ∈ (0 + 1).digits m
⊢ d < 0 + 1

case succ.succ
m d b : ℕ
hb : 1 < b + 1 + 1
hd : d ∈ (b + 1 + 1).digits m
⊢ d < b + 1 + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
l : List ℕ
hb : 1 < b
hl : ∀ x ∈ l, x < b
⊢ ofDigits b l < b ^ l.length

Tactic:
rcases b with (_ | _ | b)

Goal state after:
case zero
l : List ℕ
hb : 1 < 0
hl : ∀ x ∈ l, x < 0
⊢ ofDigits 0 l < 0 ^ l.length

case succ.zero
l : List ℕ
hb : 1 < 0 + 1
hl : ∀ x ∈ l, x < 0 + 1
⊢ ofDigits (0 + 1) l < (0 + 1) ^ l.length

case succ.succ
l : List ℕ
b : ℕ
hb : 1 < b + 1 + 1
hl : ∀ x ∈ l, x < b + 1 + 1
⊢ ofDigits (b + 1 + 1) l < (b + 1 + 1) ^ l.length
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b m : ℕ
hb : 1 < b
⊢ m < b ^ (b.digits m).length

Tactic:
rcases b with (_ | _ | b)

Goal state after:
case zero
m : ℕ
hb : 1 < 0
⊢ m < 0 ^ (digits 0 m).length

case succ.zero
m : ℕ
hb : 1 < 0 + 1
⊢ m < (0 + 1) ^ ((0 + 1).digits m).length

case succ.succ
m b : ℕ
hb : 1 < b + 1 + 1
⊢ m < (b + 1 + 1) ^ ((b + 1 + 1).digits m).length
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits (b * m) = 0 :: b.digits m

Tactic:
rw [digits_def' hb (by positivity)]

Goal state after:
b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b * m % b :: b.digits (b * m / b) = 0 :: b.digits m
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
nh : ↑n = ⊤
⊢ False

Tactic:
trivial

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

Goal state before:
pp: b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
hx : n / b = 0
⊢ (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length

Tactic:
then

Goal state after:
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
hx : n / b = 0
⊢ (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case inr
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList = padicValNat p n

Tactic:
apply _root_.le_antisymm

Goal state after:
case inr.a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ count p n.primeFactorsList ≤ padicValNat p n

case a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ padicValNat p n ≤ count p n.primeFactorsList
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a - b) = emultiplicity p b

Tactic:
rw [sub_eq_add_neg, emultiplicity_add_of_gt]

Goal state after:
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (-b) = emultiplicity p b

α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (-b) < emultiplicity p a
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l i : ℕ
x✝² : i ∈ ↑(Finset.range b)
j : ℕ
x✝¹ : j ∈ ↑(Finset.range b)
x✝ : (consFixedLengthDigits hb l i ∩ consFixedLengthDigits hb l j).Nonempty
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l i ∩ consFixedLengthDigits hb l j
⊢ i = j

Tactic:
Finset.mem_inter

Goal state after:
b : ℕ
hb : 1 < b
l i : ℕ
x✝² : i ∈ ↑(Finset.range b)
j : ℕ
x✝¹ : j ∈ ↑(Finset.range b)
x✝ : (consFixedLengthDigits hb l i ∩ consFixedLengthDigits hb l j).Nonempty
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l i ∧ L ∈ consFixedLengthDigits hb l j
⊢ i = j
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
pp : Prime p
⊢ 0 < p ^ n.factorization p

Tactic:
then

Goal state after:
n p : ℕ
pp : Prime p
⊢ 0 < p ^ n.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ 0 < n / p ^ n.factorization p

Tactic:
then

Goal state after:
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ 0 < n / p ^ n.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b p : ℕ
ha : a = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
then

Goal state after:
a b p : ℕ
ha : a = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b p : ℕ
ha : ¬a = 0
hb : b = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
then

Goal state after:
a b p : ℕ
ha : ¬a = 0
hb : b = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p b : ℕ
hb : n ≤ p ^ b
hn : n = 0
⊢ n.factorization p ≤ b

Tactic:
then

Goal state after:
n p b : ℕ
hb : n ≤ p ^ b
hn : n = 0
⊢ n.factorization p ≤ b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
pp : Prime p
⊢ n.factorization p ≤ b

Tactic:
then

Goal state after:
n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
pp : Prime p
⊢ n.factorization p ≤ b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
hn : n = 0
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization

Tactic:
then

Goal state after:
n p : ℕ
hn : n = 0
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n / p ^ n.factorization p).factorization q = (Finsupp.erase p n.factorization) q

Tactic:
· rw [Finsupp.erase_ne hqp, factorization_div (ordProj_dvd n p)]
    simp [pp.factorization, hqp.symm]

Goal state after: