mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
a b : α
⊢ flatMap (permutations'Aux b) (permutations'Aux a []) ~ flatMap (permutations'Aux a) (permutations'Aux b [])

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x d d' : α
x_mem : x ∈ [].dropLast
⊢ [].nextOr x d = [].nextOr x d'

Tactic:
| nil =>

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

Goal state before:
pp: case cons
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ flatMap (permutations'Aux b) (permutations'Aux a (c :: l)) ~
    flatMap (permutations'Aux a) (permutations'Aux b (c :: l))

Tactic:
simp only [permutations'Aux, flatMap_cons, map_cons, map_map, cons_append]

Goal state after:
case cons
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ (b :: a :: c :: l) ::
      (a :: b :: c :: l) ::
        (map (cons a ∘ cons c) (permutations'Aux b l) ++
          flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l))) ~
    (a :: b :: c :: l) ::
      (b :: a :: c :: l) ::
        (map (cons b ∘ cons c) (permutations'Aux a l) ++
          flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l)))
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ (if x = y then z else (z :: zs).nextOr x d) = if x = y then z else (z :: zs).nextOr x d'

Tactic:
IH

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ (if x = y then z else (z :: zs).nextOr x d') = if x = y then z else (z :: zs).nextOr x d'

case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ x ∈ (z :: zs).dropLast
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ (n + 1) • a = a ↔ ↑(period g a) ∣ -↑(n + 1)

Tactic:
Int.dvd_neg,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ (n + 1) • a = a ↔ ↑(period g a) ∣ ↑(n + 1)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
s t : List α
⊢ [].permutations' ~ [].permutations'

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x d : α
h : [].nextOr x d ≠ d
⊢ x ∈ []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x d : α
h : x ∉ []
⊢ ([] ++ [x]).nextOr x d = d

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
hxs' : ∀ x ∈ [], x ∈ xs'
⊢ [].nextOr x d ∈ xs'

Tactic:
| nil =>

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

Goal state before:
pp: case succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ flatMap (fun y ↦ (permutationsAux2 t [] [] y id).snd) ts.permutations' ++ map (fun x ↦ x ++ [t]) ts.permutations' ~
    ([t] ++ ts).permutations'

Tactic:
rw [map_eq_flatMap, singleton_append, permutations']

Goal state after:
case succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ flatMap (fun y ↦ (permutationsAux2 t [] [] y id).snd) ts.permutations' ++
      flatMap (fun x ↦ [x ++ [t]]) ts.permutations' ~
    flatMap (permutations'Aux t) ts.permutations'
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
x : α
n : ℕ
hn : n < (permutations'Aux x []).length
⊢ (permutations'Aux x [])[n] = [].insertIdx n x

Tactic:
| nil =>

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

Goal state before:
pp: case refine_3
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✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : StarRing B
inst✝³ : StarModule R A
s : Set A
inst✝² : FunLike F (↥(adjoin R s)) B
inst✝¹ : AlgHomClass F R (↥(adjoin R s)) B
inst✝ : StarHomClass F (↥(adjoin R s)) B
f g : F
h : ∀ (x : ↥(adjoin R s)), ↑x ∈ s → f x = g x
a x y : ↥(adjoin R s)
hx : f x = g x
hy : f y = g y
⊢ f (x + y) = g (x + y)

Tactic:
simp only [map_add, map_add, hx, hy]

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
⊢ count [x] (permutations'Aux x []) = (takeWhile (fun x_1 ↦ decide (x = x_1)) []).length + 1

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
x : α
⊢ (permutations'Aux x []).length = [].length + 1

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
x : α
hx : ¬x ∈ []
⊢ (permutations'Aux x []).Nodup

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
hl : [] ≠ []
⊢ [].prev ([].head hl) ⋯ = [].getLast hl

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
s : List α
⊢ [].permutations'.Nodup

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x hd : α
h : x ∈ [hd]
⊢ [hd].prev x h ∈ [hd]

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
a : α
ha : a ∈ []
⊢ [].prev a ha = [][(idxOf a [] + ([].length - 1)) % [].length]

Tactic:
| nil =>

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (hd :: tl)[(n + ((hd :: tl).length - 1) + 1) % (hd :: tl).length] = (hd :: tl)[n]

Tactic:
· have : (n + length tl + 1) % (length tl + 1) = n := by
      rw [length_cons] at hn
      rw [add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
    simp [this]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ (l.rotate (Nat.succ 0)).reverse[l.length - 1 - k] = (l.rotate 1)[k]

Tactic:
rw [getElem_eq_getElem_reverse]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ (l.rotate (Nat.succ 0)).reverse.reverse[(l.rotate (Nat.succ 0)).reverse.length - 1 - (l.length - 1 - k)] =
    (l.rotate 1)[k]
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.prev x hx = l'.prev x ⋯

Tactic:
rw [← next_reverse_eq_prev _ hn, ← next_reverse_eq_prev _ (h.nodup_iff.mp hn)]
  exact isRotated_next_eq h.reverse (nodup_reverse.mpr hn) _

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

Goal state before:
pp: α : Type u_1
l : List α
hl : l.Nodup
⊢ (↑l).Nontrivial ↔ 2 ≤ l.length

Tactic:
by
  rw [Nontrivial]
  rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
  · simp
  · simp
  · simp only [mem_cons, mem_coe_iff, List.length, Ne, Nat.succ_le_succ_iff,
      Nat.zero_le, iff_true]
    refine ⟨hd, hd', ?_, by simp⟩
    simp only [not_or, mem_cons, nodup_cons] at hl
    exact hl.left.left

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

Goal state before:
pp: case mp.nil
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
h : p ∣ [].prod
⊢ ∃ a, a ∈ [] ∧ p ∣ a

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
s : Cycle α
⊢ (∀ a ∈ nil, ∀ b ∈ nil, r a b) → Chain r nil

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
⊢ Chain r nil → ∀ a ∈ nil, ∀ b ∈ nil, r a b

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
h : Chain r Cycle.nil
⊢ Cycle.nil = Cycle.nil

Tactic:
| nil =>

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
p : ℕ
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
by
  rcases a.eq_zero_or_pos with (rfl | ha)
  · simp [(coprime_zero_left _).mp hab]
  rcases b.eq_zero_or_pos with (rfl | hb)
  · simp [(coprime_zero_right _).mp hab]
  rw [mem_primeFactorsList_mul ha.ne' hb.ne', List.mem_union_iff]

Goal state after:
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 ⊓ (K ⊓ L)).relIndex L ≤ H.relIndex L * K.relIndex L

Tactic:
← relIndex_mul_relIndex _ _ L inf_le_right inf_le_right,

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬H.relIndex L = 0
⊢ (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L ≤ H.relIndex L * K.relIndex L
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑(↑a + ↑b - (↑a + ↑b) % (n✝ + 1)) = 0

Tactic:
@CharP.cast_eq_zero_iff R _ m

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ m ∣ ↑a + ↑b - (↑a + ↑b) % (n✝ + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑(↑a * ↑b - ↑a * ↑b % (n✝ + 1)) = 0

Tactic:
@CharP.cast_eq_zero_iff R _ m

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ m ∣ ↑a * ↑b - ↑a * ↑b % (n✝ + 1)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
⊢ (pi Set.univ H).index = ∏ i, (H i).index

Tactic:
by
  simp_rw [index, ← Nat.card_pi]
  refine Nat.card_congr
    ((Quotient.congrRight (fun x y ↦ ?_)).trans (Setoid.piQuotientEquiv _).symm)
  rw [QuotientGroup.leftRel_pi]

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

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

Tactic:
rw [geom_sum_succ, add_lt_iff_neg_right, ← neg_lt_iff_pos_add', neg_mul_eq_neg_mul]

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hmn✝ : 2 ≤ n
ihn : 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1
⊢ -x * ∑ i ∈ range n, x ^ i < 1 ∧ x * ∑ i ∈ range n, x ^ i < 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ a * a⁻¹ = ↑(a.val.gcd n)

Tactic:
by
  rcases n with - | n
  · dsimp [ZMod] at a ⊢
    calc
      _ = a * Int.sign a := rfl
      _ = a.natAbs := by rw [Int.mul_sign_self]
      _ = a.natAbs.gcd 0 := by rw [Nat.gcd_zero_right]
  · calc
      a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by
        rw [natCast_self, zero_mul, add_zero]
      _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) := by
        push_cast
        rw [natCast_zmod_val]
        rfl
      _ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ n.Perfect ↔ ∑ i ∈ n.divisors, i = 2 * n

Tactic:
perfect_iff_sum_properDivisors h,

Goal state after:
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.divisors, i = 2 * n
Module: Mathlib.Algebra.Order.Ring.GeomSum

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

Tactic:
Ico_eq_empty_of_le (by lia),

Goal state after:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ ∑ i ∈ ∅, a / b ^ i ≤ a / (b - 1)
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
⊢ (n + k).choose k ≤ (n + 1) ^ k

Tactic:
rw [choose_eq_asc_factorial_div_factorial]

Goal state after:
n k : ℕ
⊢ (n + 1).ascFactorial k / k ! ≤ (n + 1) ^ k
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
rw [sub_eq_add_neg, val_add, val_neg_of_ne_zero, ← Nat.add_sub_assoc (le_of_lt (val_lt _)),
      add_comm, Nat.add_sub_assoc h, Nat.add_mod_left]

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a.val - b.val) % n = a.val - b.val
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Semiring α
b : α
⊢ ofDigits b [] = List.foldr (fun x y ↦ ↑x + b * y) 0 []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
b : ℕ
l2 : List ℕ
⊢ ofDigits b ([] ++ l2) = ofDigits b [] + b ^ [].length * ofDigits b l2

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Semiring α
b : ℕ
⊢ ↑(ofDigits b []) = ofDigits ↑b []

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
⊢ a ^ 1 = a

Tactic:
pow_one

Goal state after:
α : Type u_1
inst✝ : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
⊢ a = a
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case nil
b : ℕ
h : 1 < b
w₁ : ∀ l ∈ [], l < b
w₂ : ∀ (h : [] ≠ []), [].getLast h ≠ 0
⊢ b.digits (ofDigits b []) = []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
⊢ ofDigits 1 [] = [].sum

Tactic:
| nil =>

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

Goal state before:
pp: case nil
n b : ℕ
⊢ n * ofDigits b [] = ofDigits b (List.map (fun x ↦ n * x) [])

Tactic:
| nil =>

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

Goal state before:
pp: case nil
b : ℕ
hb : 1 < b
L2 : List ℕ
len : [].length = L2.length
w1 : ∀ l ∈ [], l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b [] = ofDigits b L2
⊢ [] = L2

Tactic:
| nil =>

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

Goal state before:
pp: case nil
b : ℕ
⊢ List.foldr (fun x y ↦ ↑x + b * y) 0 [] =
    (List.zipWith
        (Function.curry fun x ↦
          match x with
          | (a, i) => a * b ^ i)
        [] (List.range [].length)).sum

Tactic:
| nil =>

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

Goal state before:
pp: case nil
b : ℕ
l2 : List ℕ
h : [].length = l2.length
⊢ ofDigits b [] + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) [] l2)

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
b hd₁ : ℕ
tl₁ : List ℕ
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)
h : (hd₁ :: tl₁).length = [].length
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b [] = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁) [])

Tactic:
| nil =>

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

Goal state before:
pp: case inl.nil
p : ℕ
h : 1 < p
h_nonempty : [] ≠ []
h_ne_zero : [].getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ [], l < p
⊢ (p - 1) * ∑ i ∈ range [].length, ofDigits p [] / p ^ i.succ = ofDigits p [] - [].sum

Tactic:
| nil =>

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

Goal state before:
pp: case nil
b : ℕ
hl : ∀ x ∈ [], x < b + 2
⊢ ofDigits (b + 2) [] < (b + 2) ^ [].length

Tactic:
| nil =>

Goal state after:
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) <;> simp_all [ofDigits_lt_base_pow_length']

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

Goal state before:
pp: case nil
p q : ℕ
h : p ≤ q
⊢ ofDigits p [] ≤ ofDigits q []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
p : ℕ
hpos : 0 < p
w₁ : ∀ l ∈ [], l < p
⊢ ofDigits p [] / p = ofDigits p [].tail

Tactic:
| nil =>

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

Goal state before:
pp: case succ.nil
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
w₁ : ∀ l ∈ [], l < p
⊢ ofDigits p [] % p ^ (i + 1) = ofDigits p (List.take (i + 1) [])

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
⊢ k ∣ ofDigits a [] - ofDigits b []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
b b' k : ℕ
h : b ≡ b' [MOD k]
⊢ ofDigits b [] ≡ ofDigits b' [] [MOD k]

Tactic:
| nil =>

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

Goal state before:
pp: case nil
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
⊢ ofDigits b [] ≡ ofDigits b' [] [ZMOD ↑k]

Tactic:
| nil =>

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

Goal state before:
pp: case succ.succ.zero
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
h_e_pos : 0 < 0 + 1
hlt : n < b ^ 1
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0 + 1

Tactic:
pow_one

Goal state after:
case succ.succ.zero
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
h_e_pos : 0 < 0 + 1
hlt : n < b
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0 + 1
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
Nat.add_sub_cancel'

Goal state after:
n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ l = l

n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ (b.digits n).length ≤ l
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
hp : Prime p
hn : n ≠ 0
h : p ∣ n
⊢ 0 < n.factorization p

Tactic:
← primeFactorsList_count_eq,

Goal state after:
n p : ℕ
hp : Prime p
hn : n ≠ 0
h : p ∣ n
⊢ 0 < count p n.primeFactorsList
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 : α
⊢ ∀ (s : Finset α),
    x ∈ S →
      s ⊆ S →
        x ∉ s →
          (s.prod g).factorization = ∑ x ∈ s, (g x).factorization →
            ((insert x s).prod g).factorization = ∑ x ∈ insert x s, (g x).factorization

Tactic:
T

Goal state after:
case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
x : α
T : Finset α
⊢ 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
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
hTS : T ⊆ S
hxT : 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:
IH

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
hxT : x ∉ T
IH : (T.prod g).factorization = ∑ x ∈ T, (g x).factorization
⊢ ((insert x T).prod g).factorization = ∑ x ∈ insert x T, (g x).factorization
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: p : ℕ
hp : Prime p
q : ℕ
⊢ p.factorization q = (single p 1) q

Tactic:
← primeFactorsList_count_eq,

Goal state after:
p : ℕ
hp : Prime p
q : ℕ
⊢ count q p.primeFactorsList = (single p 1) q
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : m = 0
⊢ False

Tactic:
by simp [hx, hm0] at hb

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime 0
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
coprime_zero_right

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
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 ^ 1 = x

Tactic:
pow_one

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ x = x
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h✝ : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ x ^ 1 = x

Tactic:
pow_one

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h✝ : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ x = x
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ (n + 1).factorization p + ∑ i ∈ Ico 1 b, n / p ^ i = #({i ∈ Ico 1 b | p ^ i ∣ n + 1}) + ∑ i ∈ Ico 1 b, n / p ^ i

Tactic:
add_left_inj

Goal state after:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ (n + 1).factorization p = #({i ∈ Ico 1 b | p ^ i ∣ n + 1})
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
⊢ orderOf (y ^ 1) = orderOf y

Tactic:
pow_one

Goal state after:
case neg
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
⊢ orderOf y = orderOf y
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case h
n k : ℕ
hkn : k ≤ n
⊢ (n.choose k).factorization.support ⊆ Finset.range (n + 1)

Tactic:
intro p hp
    rw [Finset.mem_range]
    contrapose! hp
    rw [Finsupp.mem_support_iff, Classical.not_not, factorization_choose_eq_zero_of_lt hp]

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

Goal state before:
pp: case succ
p : ℕ
hp : Prime p
n : ℕ
h : emultiplicity p (p ^ n)! = ↑(∑ i ∈ range n, p ^ i)
⊢ emultiplicity p (p ^ (n + 1))! = ↑(∑ i ∈ range (n + 1), p ^ i)

Tactic:
rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.natCast_add]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
x : R
⊢ x ^ p ^ 1 = x ^ p

Tactic:
pow_one

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
x : R
⊢ x ^ p = x ^ p