mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
hA : FiniteType R A
s : Finset A
hS : adjoin R ↑s = ⊤
b : A
⊢ b ∈ adjoin S ↑s

Tactic:
have le : adjoin R (s : Set A) ≤ Subalgebra.restrictScalars R (adjoin S s) := by
    apply (Algebra.adjoin_le _ : adjoin R (s : Set A) ≤ Subalgebra.restrictScalars R (adjoin S ↑s))
    simp only [Subalgebra.coe_restrictScalars]
    exact Algebra.subset_adjoin

Goal state after:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
hA : FiniteType R A
s : Finset A
hS : adjoin R ↑s = ⊤
b : A
le : adjoin R ↑s ≤ Subalgebra.restrictScalars R (adjoin S ↑s)
⊢ b ∈ adjoin S ↑s
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S → ∃ n f, Surjective ⇑f

Tactic:
rw [iff_quotient_mvPolynomial']
    rintro ⟨ι, hfintype, f, hsur⟩
    have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
    exact ⟨Fintype.card ι, AlgHom.comp f equiv.symm.toAlgHom, by simpa using hsur⟩

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

Goal state before:
pp: case intro
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ϕ (∑ v ∈ p.support, (monomial v) (coeff v p)) = eval₂ (ϕ.comp C) (fun s ↦ ϕ (X s)) p

Tactic:
rw [MvPolynomial.eval₂_eq', map_sum ϕ]

Goal state after:
case intro
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ∑ x ∈ p.support, ϕ ((monomial x) (coeff x p)) = ∑ d ∈ p.support, (ϕ.comp C) (coeff d p) * ∏ i, ϕ (X i) ^ d i
Module: Mathlib.Data.Int.ModEq

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

Tactic:
simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]

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

Goal state before:
pp: R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]

Tactic:
by
  wlog hle : a ≤ b
  · rw [eq_comm, this R p (le_of_not_ge hle), Nat.ModEq.comm]
  rw [Nat.modEq_iff_dvd' hle, ← cast_eq_zero_iff R p (b - a),
    ← add_right_cancel_iff (G := R) (a := a) (b := b - a), zero_add, ← Nat.cast_add,
    Nat.sub_add_cancel hle, eq_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
a b c : R
⊢ a + b = c ↔ a = c + b

Tactic:
by
  rw [← sub_eq_iff_eq_add, sub_eq_add]

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

Goal state before:
pp: p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
⊢ a ^ k = p

Tactic:
rw [h.1, h.2, pow_one]

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

Goal state before:
pp: p a k : ℕ
hp : Prime p
⊢ a ^ k = p ↔ a = p ∧ k = 1

Tactic:
by
  refine ⟨fun h => ?_, fun h => by rw [h.1, h.2, pow_one]⟩
  rw [← h] at hp
  rw [← h, hp.eq_one_of_pow, eq_self_iff_true, _root_.and_true, pow_one]

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S : Type v
inst✝² : Ring S
J : Ideal R
I : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
r : R
ha : f r ∈ I
⊢ (Quotient.mk J) r = 0

Tactic:
exact Quotient.eq_zero_iff_mem.mpr (h ha)

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a : List α
ha : a ~ m.toList
⊢ ∀ (b : List α), b ~ n.toList → a ≠ b

Tactic:
b

Goal state after:
case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a : List α
ha : a ~ m.toList
b : List α
⊢ b ~ n.toList → a ≠ b
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
t : α
ts : List α
⊢ map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)

Tactic:
induction ts with
  | nil => rfl
  | cons a ts ih => simp only [permutations'Aux, map_cons, map_map, ← ih, Function.comp_def]

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

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

Tactic:
b

Goal state after:
case refine_3
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
a b : ↥(I ^ n) ⧸ I • ⊤
⊢ (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) a =
      (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) b →
    a = b
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → l.length = n) → (map length L).sum = n * L.length
H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n
⊢ (map length (l :: L)).sum = n * (l :: L).length

Tactic:
have sum_map : (map length L).sum = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)

Goal state after:
case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → l.length = n) → (map length L).sum = n * L.length
H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n
sum_map : (map length L).sum = n * L.length
⊢ (map length (l :: L)).sum = n * (l :: L).length
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:
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: α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[n + minimalPeriod f x] x = f^[n] x

Tactic:
iterate_add_apply

Goal state after:
α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[n] (f^[minimalPeriod f x] x) = f^[n] x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m - n + n] x = f^[n] x
hmn' : n < m
⊢ False

Tactic:
iterate_add_apply

Goal state after:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m - n] (f^[n] x) = f^[n] x
hmn' : n < m
⊢ False
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ (if x = hd' then hd else (hd' :: tl).prev x ⋯) ∈ hd :: hd' :: tl

Tactic:
split_ifs with hm

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
hm : x = hd'
⊢ hd ∈ hd :: hd' :: tl

case neg
α : Type u_1
inst✝ : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
hm : ¬x = hd'
⊢ (hd' :: tl).prev x ⋯ ∈ hd :: hd' :: tl
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case mp
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
rintro ⟨p, k, hp', hk', rfl⟩

Goal state after:
case mp
p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
⊢ ∃ k_1, k_1 ≤ Nat.log 2 (p ^ k) ∧ 0 < k_1 ∧ ∃ p_1, p_1 ≤ p ^ k ∧ p ^ k = p_1 ^ k_1 ∧ Nat.Prime p_1
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case mpr
k : ℕ
hk' : 0 < k
p : ℕ
hp' : Nat.Prime p
hk : k ≤ Nat.log 2 (p ^ k)
hp : p ≤ p ^ k
⊢ ∃ p_1 k_1, Nat.Prime p_1 ∧ 0 < k_1 ∧ p_1 ^ k_1 = p ^ k

Tactic:
exact ⟨p, k, hp', hk', rfl⟩

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : Chain r ↑(a :: l)
⊢ ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b

Tactic:
b

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : Chain r ↑(a :: l)
b : α
⊢ b ∈ ↑(a :: l) → ∀ b_1 ∈ ↑(a :: l), r b b_1
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: n : ℕ
⊢ n.primeFactors.Nonempty ↔ 1 < n

Tactic:
contrapose!
  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: case inl
a : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ primeFactorsList 0
⊢ a ∣ 0

pp: case inr
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
hb : b > 0
⊢ a ∣ b

Tactic:
· exact dvd_zero _

Goal state after:
case inr
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
hb : b > 0
⊢ a ∣ b
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬H.relIndex L = 0
⊢ H.relIndex (K ⊓ L) * K.relIndex L ≤ H.relIndex L * K.relIndex L

Tactic:
grw [relIndex_le_of_le_right inf_le_right h]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n ↦ ↑(a ^ ↑n)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he : f ⟨n₁, ⋯⟩ = f ⟨n₂, ⋯⟩
hc' : ¬(n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁))
⊢ ⟨n₁, ⋯⟩ = ⟨n₂, ⋯⟩

Tactic:
dsimp only [f] at he

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n ↦ ↑(a ^ ↑n)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₁) = ↑(a ^ n₂)
hc' : ¬(n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁))
⊢ ⟨n₁, ⋯⟩ = ⟨n₂, ⋯⟩
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ↑(if k = 0 then n✝ else ↑k - 1) = ↑↑k - 1

Tactic:
if_neg

Goal state after:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ↑(↑k - 1) = ↑↑k - 1

case neg.succ.hnc
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ¬k = 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
a : G
⊢ ∀ ⦃a₂ : G⦄, ((MulDistribMulAction.toMonoidEnd H G) h) a = ((MulDistribMulAction.toMonoidEnd H G) h) a₂ → a = a₂

Tactic:
b

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
a b : G
⊢ ((MulDistribMulAction.toMonoidEnd H G) h) a = ((MulDistribMulAction.toMonoidEnd H G) h) b → a = b
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
a : G
⊢ ∀ ⦃a₂ : G⦄, ((DistribMulAction.toAddMonoidEnd H G) h) a = ((DistribMulAction.toAddMonoidEnd H G) h) a₂ → a = a₂

Tactic:
b

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
a b : G
⊢ ((DistribMulAction.toAddMonoidEnd H G) h) a = ((DistribMulAction.toAddMonoidEnd H G) h) b → a = b
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ ∀ ⦃a₂ : ZMod (n✝ + 1)⦄, a.val = a₂.val → a = a₂

Tactic:
b

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
⊢ a.val = b.val → a = b
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
apply Finset.subset_iff.2

Goal state after:
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
⊢ ∀ ⦃x : ℕ⦄, x ∈ m.divisors → x ∈ n.properDivisors
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = n - a.val

Tactic:
apply Nat.mod_eq_of_lt

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ n - a.val < n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: n b : ℕ
hb : 2 ≤ b
hn : 0 < n
⊢ b.digits n = n % b :: b.digits (n / b)

Tactic:
rw [Nat.eq_add_of_sub_eq hb rfl, Nat.eq_add_of_sub_eq hn rfl, Nat.digits_add_two_add_one]

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n ≃+* R
⊢ f = g

Tactic:
RingEquiv.coe_ringHom_inj_iff

Goal state after:
n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n ≃+* R
⊢ ↑f = ↑g
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : NonAssocRing R
f : R →+* ZMod 0
k : ZMod 0
⊢ f k.cast = k

Tactic:
dsimp +instances [ZMod, ZMod.cast] at f k ⊢
    simp

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

Goal state before:
pp: b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits n ++ (List.replicate k 0 ++ b.digits m) = b.digits (n + b ^ ((b.digits n).length + k) * m)

Tactic:
← digits_base_pow_mul hb hm

Goal state after:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits n ++ b.digits (b ^ k * m) = b.digits (n + b ^ ((b.digits n).length + k) * m)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l

Tactic:
by
  rw [← List.dropLast_append_getLast hl]
  simp only [List.length_append, List.length, zero_add, List.length_dropLast, ofDigits_append,
    List.length_dropLast, ofDigits_singleton, add_comm (l.length - 1), pow_add, pow_one]
  apply Nat.mul_le_mul_left
  refine le_trans ?_ (Nat.le_add_left _ _)
  have : 0 < l.getLast hl := by rwa [pos_iff_ne_zero]
  convert! Nat.mul_le_mul_left ((b + 2) ^ (l.length - 1)) this using 1
  rw [Nat.mul_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : (x ^ ↑n.natAbs)⁻¹ = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
inv_eq_one,

Goal state after:
case inr
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ ↑n.natAbs = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ y ^ n = 1

Tactic:
← isConj_one_right,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ IsConj 1 (y ^ n)
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 (-b) = emultiplicity p b

Tactic:
emultiplicity_neg

Goal state after:
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b = emultiplicity p b
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 (-b) < emultiplicity p a

Tactic:
emultiplicity_neg

Goal state after:
α : 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.Factorization.Defs

Goal state before:
pp: case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
x : α
T : Finset α
hxS : x ∈ S
⊢ T ⊆ S →
    x ∉ T →
      (T.prod g).factorization = ∑ x ∈ T, (g x).factorization →
        ((insert x T).prod g).factorization = ∑ x ∈ insert x T, (g x).factorization

Tactic:
hTS

Goal state after:
case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
⊢ x ∉ T →
    (T.prod g).factorization = ∑ x ∈ T, (g x).factorization →
      ((insert x T).prod g).factorization = ∑ x ∈ insert x T, (g x).factorization
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p (b + a) = min (multiplicity p a) (multiplicity p b)

Tactic:
ha.multiplicity_add_of_gt hab,

Goal state after:
case inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p a = min (multiplicity p a) (multiplicity p b)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ (x ^ n) ^ 1 = x

Tactic:
rw [h, pow_one, pow_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ orderOf x = p ^ (n + 1)

Tactic:
apply minimalPeriod_eq_prime_pow <;> rwa [isPeriodicPt_mul_iff_pow_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ orderOf x ∣ i ↔ (x ^ ↑i)⁻¹ = 1

Tactic:
inv_eq_one,

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ orderOf x ∣ i ↔ x ^ ↑i = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
a : G
ha₀ : a ≤ 0
ha : IsOfFinOrder a
⊢ ¬a = 1

Tactic:
rintro rfl; exact one_pos.not_ge ha₀

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

Goal state before:
pp: case refine_2.inl.inl
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : p.natDegree = 0
hq : q.natDegree = 0
⊢ (C (p.coeff 0 + q.coeff 0)).natDegree = 0

Tactic:
natDegree_C

Goal state after:
case refine_2.inl.inl
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : p.natDegree = 0
hq : q.natDegree = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos.h₀
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
hb2 : b ≠ n / p
⊢ (if p * b = n then f.coeff b else 0) = 0

Tactic:
if_neg

Goal state after:
case pos.h₀
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
hb2 : b ≠ n / p
⊢ 0 = 0

case pos.h₀.hnc
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
hb2 : b ≠ n / p
⊢ ¬p * b = n
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ f.support
⊢ (if p * k = n then f.coeff k else 0) = 0

Tactic:
if_neg

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ f.support
⊢ 0 = 0

case neg.hnc
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ f.support
⊢ ¬p * k = n
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ (C (eval 1 f)).natDegree = 0

Tactic:
natDegree_C

Goal state after:
case inl
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
this : q.natDegree = q.natDegree * p.natDegree + (1 * p.natDegree + r.natDegree)
⊢ False

Tactic:
exact
      ne_of_lt
        (lt_add_of_le_of_pos (le_mul_of_one_le_right (Nat.zero_le _) hnp)
          (add_pos_of_pos_of_nonneg (by rwa [one_mul]) (Nat.zero_le _)))
        this

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this✝ : DecidableEq R := Classical.decEq R
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
this : ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) %ₘ q).degree < q.degree
⊢ (p %ₘ q).degree < q.degree

Tactic:
grind [divModByMonicAux, modByMonic]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ derivative (C a * X ^ 2) = C (a * 2) * X

Tactic:
derivative_C_mul_X_pow,

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
⊢ C (a * ↑2) * X ^ (2 - 1) = C (a * 2) * X
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).natDegree < p.natDegree

Tactic:
· rw [natDegree_lt_natDegree_iff hp']
    exact degree_derivative_lt fun h => hp (h.symm ▸ natDegree_zero)

Goal state after:
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: case mpr
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ (∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t) → t ∈ ⨅ i, l i

Tactic:
· rintro ⟨⟨I, f⟩, ⟨hI₁, hI₂⟩, hsub⟩
      grw [← hsub]
      exact (biInter_mem hI₁).mpr fun i hi => mem_iInf_of_mem i <| (hl i).mem_of_mem <| hI₂ _ hi

Goal state after: