mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Subalgebra.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥B
inst✝ : Free ↥B ↥(Algebra.adjoin ↥B ↑A)
⊢ finrank R ↥(A ⊔ B) = finrank R ↥B * finrank ↥B ↥(Algebra.adjoin ↥B ↑A)

Tactic:
sup_comm,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥B
inst✝ : Free ↥B ↥(Algebra.adjoin ↥B ↑A)
⊢ finrank R ↥(B ⊔ A) = finrank R ↥B * finrank ↥B ↥(Algebra.adjoin ↥B ↑A)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
σ : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝ : MvPolynomial σ R
⊢ (map f) x✝ = 0 ↔ ∀ (m : σ →₀ ℕ), coeff m x✝ ∈ RingHom.ker f

Tactic:
MvPolynomial.ext_iff

Goal state after:
R : Type u
S : Type u_1
σ : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝ : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m ((map f) x✝) = coeff m 0) ↔ ∀ (m : σ →₀ ℕ), coeff m x✝ ∈ RingHom.ker f
Module: Mathlib.Data.Int.ModEq

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

Tactic:
rw [add_comm, modEq_add_modulus_mul_iff]

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

Goal state before:
pp: case refine_2.inl_add_inr
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
r : R
a : A
⊢ (lift f).toRingHom (inl r + ↑a) ∈ S

Tactic:
| _ r a =>

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : SetLike S R
hSR : NonUnitalSubringClass S R
s : S
⊢ (unitization s).range = subalgebraOfSubring (Subring.closure ↑s)

Tactic:
have := AddSubgroupClass.zsmulMemClass (S := S)
  rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_int]

Goal state after:
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: case hp
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ ∃ a, Even a

Tactic:
use 0

Goal state after:
case h
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ Even 0
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case refine_2.inl_add_inr
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
r : R
a : A
⊢ (↑(starLift f)).toRingHom (inl r + ↑a) ∈ S

Tactic:
| _ r a =>

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

Goal state before:
pp: R : Type u_1
S : 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
inst✝¹ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
⊢ (unitization s).range = StarAlgebra.adjoin R ↑s

Tactic:
rw [unitization, Unitization.starLift_range]

Goal state after:
R : Type u_1
S : 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
inst✝¹ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
⊢ StarAlgebra.adjoin R ↑(NonUnitalStarAlgHom.range (NonUnitalStarSubalgebraClass.subtype s)) = StarAlgebra.adjoin R ↑s
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: case hp
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
⊢ ∃ a, Even a

Tactic:
use 0

Goal state after:
case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
⊢ Even 0
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
h2 : p ≠ 2
n : ℕ
hn : p = 2 * n + 1
⊢ p - 1 = n + n

Tactic:
hn,

Goal state after:
p : ℕ
hp : Prime p
h2 : p ≠ 2
n : ℕ
hn : p = 2 * n + 1
⊢ 2 * n + 1 - 1 = n + n
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
⊢ (permutations'Aux x s).get ⟨s.length, ⋯⟩ = (permutations'Aux x t).get ⟨s.length, ⋯⟩

Tactic:
simp only [get_eq_getElem, h, hl]

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

Goal state before:
pp: α : 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
⊢ n < (bs.insertIdx m x).length

Tactic:
length_insertIdx_of_le_length hm,

Goal state after:
α : 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
⊢ n < bs.length + 1
Module: Mathlib.Data.List.Permutation

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

Tactic:
exact take_sublist 2 _

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Nonempty α
⊢ IsPretransitive G α ↔ Nonempty (Unique (orbitRel.Quotient G α))

Tactic:
rw [unique_iff_subsingleton_and_nonempty, pretransitive_iff_subsingleton_quotient, iff_self_and]
  exact fun _ ↦ (nonempty_quotient_iff _).mpr inferInstance

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

Goal state before:
pp: case mp.cons.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
obtain ⟨x, hx1, hx2⟩ := L_ih hd

Goal state after:
case mp.cons.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
x : M
hx1 : x ∈ L_tl
hx2 : p ∣ x
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n p : ℕ
⊢ p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n ∧ n ≠ 0

Tactic:
cases n <;> simp [mem_primeFactorsList, *]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : K.Normal
⊢ K.relIndex (K ⊔ H) = K.relIndex H

Tactic:
sup_comm,

Goal state after:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : K.Normal
⊢ K.relIndex (H ⊔ K) = K.relIndex H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relIndex ⊤ = H.relIndex ⊤ * ⊤.index

Tactic:
index_top,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relIndex ⊤ = H.relIndex ⊤ * 1
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'
⊢ ⊥.relIndex f.range = Nat.card ↥f.range

Tactic:
relIndex_bot_left

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ Nat.card ↥f.range = Nat.card ↥f.range
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
K : Subgroup G
f : G →* G'
⊢ ⊥.relIndex (map f K) = Nat.card ↥(map f K)

Tactic:
relIndex_bot_left

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
K : Subgroup G
f : G →* G'
⊢ Nat.card ↥(map f K) = Nat.card ↥(map f K)
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
⊢ (H ⊔ f.ker).index * ⊤.index ∣ H.index

Tactic:
index_top,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Surjective ⇑f
⊢ (H ⊔ f.ker).index * 1 ∣ H.index
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
h : IsUnit ↑n
⊢ n = 1

Tactic:
by
  rw [← Nat.mod_zero n, ← val_natCast, val_unit'.mp h]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.1 = a.cast

Tactic:
simp [ZMod.cast]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.2 = a.cast

Tactic:
simp [ZMod.cast]

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

Goal state before:
pp: case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑↑a.val = a

Tactic:
Int.cast_natCast,

Goal state after:
case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑a.val = a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
hlt : ↑(↑a).val < ↑n
⊢ ↑↑(↑a).val = ↑a

Tactic:
Int.cast_natCast,

Goal state after:
n : ℕ
a : ℤ
inst✝ : NeZero n
hle : 0 ≤ ↑(↑a).val
hlt : ↑(↑a).val < ↑n
⊢ ↑(↑a).val = ↑a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ ↑↑z.val + ↑↑p * ↑k = z

Tactic:
Int.cast_natCast,

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

Goal state before:
pp: case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ ↑z.val + ↑↑p * ↑k = z

Tactic:
Int.cast_natCast,

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

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

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

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

Goal state before:
pp: case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a * b).val = a.val * b.val % (n✝ + 1)

Tactic:
· apply Fin.val_mul

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
⊢ m.divisors ⊆ n.properDivisors

Tactic:
by
  apply Finset.subset_iff.2
  intro x hx
  exact
    Nat.mem_properDivisors.2
      ⟨(Nat.mem_divisors.1 hx).1.trans h,
        lt_of_le_of_lt (divisor_le hx)
          (lt_of_le_of_ne (divisor_le (Nat.mem_divisors.2 ⟨h, hzero⟩)) hdiff)⟩

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
by_cases hn : n = 0; · simp [hn]
  rw [← prod_image]
  · exact prod_congr (image_div_divisors_eq_divisors n) (by simp)
  · intro x hx y hy h
    rw [mem_coe, mem_divisors] at hx hy
    exact (div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: q : ℕ
hq : 1 < q
k✝ : ℕ
k : ℕ × ℕ
hk : k ∈ map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) (antidiagonal k✝)
⊢ k ∈ (q ^ k✝).divisorsAntidiagonal

Tactic:
obtain ⟨i, hi, rfl⟩ := Finset.mem_map.mp hk

Goal state after:
q : ℕ
hq : 1 < q
k : ℕ
i : ℕ × ℕ
hi : i ∈ antidiagonal k
hk :
  ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) i ∈
    map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) (antidiagonal k)
⊢ ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) i ∈ (q ^ k).divisorsAntidiagonal
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑(n + 1 - r) ^ r / ↑r ! ≤ ↑(n.choose r)

Tactic:
rw [div_le_iff₀']
  · norm_cast
    rw [← Nat.descFactorial_eq_factorial_mul_choose]
    exact n.pow_sub_le_descFactorial r
  exact mod_cast r.factorial_pos

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

Goal state before:
pp: case neg
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : ¬m = 0
⊢ (m % b :: b.digits (m / b)).getLast ⋯ = (b.digits (m / b)).getLast q

Tactic:
rw [List.getLast_cons]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
⊢ WithTop.untopD 1 (emultiplicity a b) = 1

Tactic:
emultiplicity_eq_top.mpr h

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
⊢ WithTop.untopD 1 ⊤ = 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ ∀ (n : ℕ), a ^ n.succ ∣ b

Tactic:
simpa [FiniteMultiplicity] using h

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
⊢ (if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤) ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Tactic:
split

Goal state after:
case mpr.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h✝ : FiniteMultiplicity a b
⊢ ↑(Nat.find h✝) ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

case mpr.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h✝ : ¬FiniteMultiplicity a b
⊢ ⊤ ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
⊢ ↑(Nat.find ⋯) ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Tactic:
split

Goal state after:
case isTrue
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h✝ : FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ↑(Nat.find h✝)

case isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h✝ : ¬FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ⊤
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ (b.digitsAppend l n).length = l

Tactic:
digitsAppend,

Goal state after:
n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ (b.digits n ++ replicate (l - (b.digits n).length) 0).length = l
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digitsAppend l n
⊢ i < b

Tactic:
digitsAppend,

Goal state after:
n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digits n ++ replicate (l - (b.digits n).length) 0
⊢ i < b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l x✝¹ : ℕ
x✝ : x✝¹ ∈ {n | n < b ^ l}
⊢ ofDigits b (b.digitsAppend l x✝¹) = x✝¹

Tactic:
digitsAppend,

Goal state after:
b : ℕ
hb : 1 < b
l x✝¹ : ℕ
x✝ : x✝¹ ∈ {n | n < b ^ l}
⊢ ofDigits b (b.digits x✝¹ ++ replicate (l - (b.digits x✝¹).length) 0) = x✝¹
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ ofDigits b (b.digitsAppend l (ofDigits b L)) = ofDigits b L

Tactic:
digitsAppend,

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ ofDigits b (b.digits (ofDigits b L) ++ replicate (l - (b.digits (ofDigits b L)).length) 0) = ofDigits b L
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ f (x ^ n) = 1

Tactic:
hn,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ f 1 = 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : min (emultiplicity p a) (emultiplicity p b) = ⊤
⊢ ⊤ ≤ emultiplicity p (a + b)

Tactic:
simp only [top_le_iff, min_eq_top, emultiplicity_eq_top] at hm ⊢
    contrapose hm
    simp only [not_and_or, not_not] at hm ⊢
    exact hm.or_of_add

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ (b.digits (ofDigits b L)).sum = (b.digitsAppend l (ofDigits b L)).sum

Tactic:
digitsAppend,

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ (b.digits (ofDigits b L)).sum = (b.digits (ofDigits b L) ++ replicate (l - (b.digits (ofDigits b L)).length) 0).sum
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
⊢ b.factorization ≤ (a * b).factorization

Tactic:
rw [mul_comm]
  apply factorization_le_factorization_mul_left ha

Goal state after:
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : ¬Prime p
⊢ (n.choose k).factorization p = 0

Tactic:
exact factorization_eq_zero_of_not_prime (choose n k) hp

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : e.factorization ≤ a.factorization
heb' : e.factorization ≤ b.factorization
⊢ e.factorization ≤ a.factorization ⊓ b.factorization

Tactic:
simp [hea', heb']

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

Goal state before:
pp: case succ
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + ↑n
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (n + 1)! + ↑(n + 1)

Tactic:
simp only [hp, emultiplicity_factorial_mul_succ, ih, factorial_succ, emultiplicity_mul,
      cast_add, cast_one, ← add_assoc]
    congr 1
    rw [add_comm, add_assoc]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ ↑(multiplicity p (p ^ n)!) = ↑(∑ i ∈ range n, p ^ i)

Tactic:
← (Nat.finiteMultiplicity_iff.2
      ⟨hp.ne_one, (p ^ n).factorial_pos⟩).emultiplicity_eq_multiplicity

Goal state after:
n p : ℕ
hp : Prime p
⊢ emultiplicity p (p ^ n)! = ↑(∑ i ∈ range n, p ^ i)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
m n : ℤ
⊢ x ^ (m - n) = 1 ↔ m ≡ n [ZMOD ↑(orderOf x)]

Tactic:
zpow_eq_one_iff_modEq,

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
m n : ℤ
⊢ m - n ≡ 0 [ZMOD ↑(orderOf x)] ↔ m ≡ n [ZMOD ↑(orderOf x)]
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ), (p.divX * X + C (p.coeff 0)).coeff n = p.coeff n

Tactic:
rintro ⟨_ | _⟩ <;> simp [coeff_C, coeff_mul_X]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
key : g • a ≤ g • g ^ (Nat.card G - 1) • a
⊢ g • a = a

Tactic:
rw [smul_smul, ← _root_.pow_succ',
    Nat.sub_one_add_one_eq_of_pos Nat.card_pos, pow_card_eq_one', one_smul] at key

Goal state after:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
key : g • a ≤ a
⊢ g • a = a
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : ¬m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
use 0

Goal state after:
case h
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : ¬m = 0
⊢ a = 0 ^ n ∧ b = 0 ^ m
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
key : g • g ^ (Nat.card G - 1) • a ≤ g • a
⊢ g • a = a

Tactic:
rw [smul_smul, ← _root_.pow_succ',
    Nat.sub_one_add_one_eq_of_pos Nat.card_pos, pow_card_eq_one', one_smul] at key

Goal state after:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
key : a ≤ g • a
⊢ g • a = a
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ derivative ((expand R p) f) = (expand R p) (derivative f) * (↑p * X ^ (p - 1))

Tactic:
rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_natCast, derivative_X, mul_one]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ f.natDegree < n * p

Tactic:
calc
    f.natDegree < f.natDegree + 1 := Nat.lt_succ_self _
    _ ≤ n * 1 := by simpa only [mul_one] using hn
    _ ≤ n * p := by gcongr; exact hp.bot_lt

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
x : ℕ × ℕ
⊢ (x.1 * p, x.2 * p).1 + (x.1 * p, x.2 * p).2 = (x.1 + x.2) * p

Tactic:
simp_rw [add_mul]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p ≠ 0
⊢ (derivative p).degree < p.degree

Tactic:
exact degree_derivative_lt fun h => hp (h.symm ▸ natDegree_zero)

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ p %ₘ q = p - q * (p /ₘ q)

Tactic:
by
      rw [modByMonic_eq_of_not_monic _ hq, divByMonic_eq_of_not_monic _ hq, mul_zero, sub_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ (p.sum fun n a ↦ eval x (C (a * ↑n)) * x ^ (n - 1)) = p.sum fun n a ↦ a * ↑n * x ^ (n - 1)

Tactic:
eval_C

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
h : Function.Injective ⇑(algebraMap A B)
⊢ (algebraMap A B) ((aeval x) p) = (algebraMap A B) 0 ↔ (aeval x) p = 0

Tactic:
h.eq_iff

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
h : Function.Injective ⇑(algebraMap A B)
⊢ (aeval x) p = 0 ↔ (aeval x) p = 0