mathlib-initiative/mathlib-tactics huggingface dataset:
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
hl : (s.insertIdx k x).length = (s.insertIdx (k + 1) x).length
n : ℕ
hn : n < (s.insertIdx k x).length
hn' : n < (s.insertIdx (k + 1) x).length
⊢ (s.insertIdx k x).get ⟨n, hn⟩ = (s.insertIdx (k + 1) x).get ⟨n, hn'⟩

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l ≠ []
h : l.getLast hl ∉ l.dropLast
⊢ l.get ⟨0, ⋯⟩ = l.head hl

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
a : α
ha : a ∈ l
⊢ 0 < l.length

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
this : idxOf a l = (idxOf a l.tail).succ
⊢ [l.prev a ha, a].length + (idxOf a l - 1) ≤ l.length

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
h1 : l.length - 1 + 1 = l.length
⊢ l.length - 1 < l.length

Tactic:
by grind

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

Goal state before:
pp: case hl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (pmap l.next l ⋯).length = (l.rotate 1).length

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:
· simp

Goal state after:
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]
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.right.inl
α : 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
hx' : (bs.insertIdx m x)[n] = x
ht : n < m
⊢ (bs.insertIdx m x)[n] ∈ bs

Tactic:
getElem_insertIdx_of_lt ht

Goal state after:
case cons.right.inl
α : 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
hx' : (bs.insertIdx m x)[n] = x
ht : n < m
⊢ bs[n] ∈ bs
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case hl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (pmap l.prev l ⋯).length = (l.rotate (l.length - 1)).length

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

Tactic:
· simp

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ ∀ (i : ℕ) (h₁ : i < (pmap l.prev l ⋯).length) (h₂ : i < (l.rotate (l.length - 1)).length),
    (pmap l.prev l ⋯)[i] = (l.rotate (l.length - 1))[i]
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.right.inr.inr
α : 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
hx' : (bs.insertIdx m x)[n] = x
ht : m < n
⊢ (as.insertIdx n x)[m] ∈ as

Tactic:
getElem_insertIdx_of_lt ht

Goal state after:
case cons.right.inr.inr
α : 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
hx' : (bs.insertIdx m x)[n] = x
ht : m < n
⊢ as[m] ∈ as
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
hl : [].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[] ∧ y ∈ ↑[]) ↔ 2 ≤ [].length

pp: case cons.nil
α : Type u_1
hd : α
hl : [hd].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[hd] ∧ y ∈ ↑[hd]) ↔ 2 ≤ [hd].length

pp: case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ (hd :: hd' :: tl).length

Tactic:
· simp

Goal state after:
case cons.nil
α : Type u_1
hd : α
hl : [hd].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[hd] ∧ y ∈ ↑[hd]) ↔ 2 ≤ [hd].length

case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ (hd :: hd' :: tl).length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.nil
α : Type u_1
hd : α
hl : [hd].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[hd] ∧ y ∈ ↑[hd]) ↔ 2 ≤ [hd].length

pp: case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ (hd :: hd' :: tl).length

Tactic:
· simp

Goal state after:
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ (hd :: hd' :: tl).length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.nil
α : Type u_1
h : Subsingleton (Quot.mk ⇑(IsRotated.setoid α) [])
⊢ Nodup (Quot.mk ⇑(IsRotated.setoid α) [])

pp: case h.cons
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))

Tactic:
· simp

Goal state after:
case h.cons
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
Module: Mathlib.Data.Nat.Prime.Pow

Goal state before:
pp: case inl
k : ℕ
hk : k ≠ 0
⊢ (1 ^ k).minFac = minFac 1

pp: case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
⊢ (n ^ k).minFac = n.minFac

Tactic:
· simp

Goal state after:
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
⊢ (n ^ k).minFac = n.minFac
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inl
⊢ (∃ k, k ≤ Nat.log 2 1 ∧ 0 < k ∧ ∃ p, p ≤ 1 ∧ 1 = p ^ k ∧ Nat.Prime p) ↔
    ∃ k, k ≤ Nat.log 2 1 ∧ 0 < k ∧ 1 = Nat.minFac 1 ^ k

pp: case inr
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k

Tactic:
· simp

Goal state after:
case inr
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l ++ [a]
⊢ r a b

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
c : α
hc : c ∈ [a]
⊢ r b c

Tactic:
by grind

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

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
x✝³ x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ x✝²⁻¹ * (x✝³⁻¹ * (x✝³ * x✝¹)) ∈ H

Tactic:
inv_mul_cancel_left

Goal state after:
G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
x✝³ x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ x✝²⁻¹ * x✝¹ ∈ H
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G✝ : Type u
X : Type v
inst✝² : Group G✝
inst✝¹ : MulAction G✝ X
x : X
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (x y : G ⧸ H), ∃ g, g • x = y

Tactic:
by
    { rintro ⟨x⟩ ⟨y⟩
      refine ⟨y * x⁻¹, QuotientGroup.eq.mpr ?_⟩
      simp only [smul_eq_mul, H.one_mem, inv_mul_cancel, inv_mul_cancel_right]}

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

Goal state before:
pp: case inl
k : ℕ
⊢ (0 ^ (k + 1)).primeFactors = primeFactors 0

pp: case inr
n k : ℕ
hn : n ≠ 0
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors

Tactic:
· simp

Goal state after:
case inr
n k : ℕ
hn : n ≠ 0
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors
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 : f.ker ≤ H
⊢ H.index ∣ (map f H).index

Tactic:
rw [index_map, sup_of_le_left hf]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : f.ker ≤ H
⊢ H.index ∣ H.index * f.range.index
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'
J K : Subgroup G'
hJK : J.relIndex K ≠ 0
⊢ (comap f J).relIndex (comap f K) ≠ 0

Tactic:
rw [relIndex_comap]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
J K : Subgroup G'
hJK : J.relIndex K ≠ 0
⊢ J.relIndex (map f (comap f K)) ≠ 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : H.relIndex L ≠ 0
hK : K.relIndex L ≠ 0
⊢ (H ⊓ K).relIndex L ≠ 0

Tactic:
by
  replace hH : H.relIndex (K ⊓ L) ≠ 0 := mt (relIndex_eq_zero_of_le_right inf_le_right) hH
  rw [← inf_relIndex_right] at hH hK ⊢
  rw [inf_assoc]
  exact relIndex_ne_zero_trans hH hK

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

Goal state before:
pp: case zero
k : ℕ
⊢ ↑k = 0 ↔ 0 ∣ k

pp: case succ
k n : ℕ
⊢ ↑k = 0 ↔ n + 1 ∣ k

Tactic:
· simp

Goal state after:
case succ
k n : ℕ
⊢ ↑k = 0 ↔ n + 1 ∣ k
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : H.index ≠ 0
hK : K.index ≠ 0
⊢ (H ⊓ K).index ≠ 0

Tactic:
rw [← relIndex_top_right] at hH hK ⊢

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : H.relIndex ⊤ ≠ 0
hK : K.relIndex ⊤ ≠ 0
⊢ (H ⊓ K).relIndex ⊤ ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) n✝ + 1 with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0

Tactic:
· simp

Goal state after:
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:
simp_rw [index, ← Nat.card_pi]

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
⊢ Nat.card ((ι → G) ⧸ pi Set.univ H) = Nat.card ((a : ι) → G ⧸ H a)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
⊢ ↑(-1) = 0

pp: case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1

Tactic:
· simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
⊢ (-1).cast = ↑0 - 1

pp: case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (-1).cast = ↑(n + 1) - 1

Tactic:
· dsimp [ZMod, ZMod.cast]; simp

Goal state after:
case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (-1).cast = ↑(n + 1) - 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (-1).cast = ↑n - 1

Tactic:
by
  rcases n with - | n
  · dsimp [ZMod, ZMod.cast]; simp
  · rw [← natCast_val, val_neg_one, Nat.cast_succ, add_sub_cancel_right]

Goal state after:
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:
Nat.cast_add,

Goal state after:
case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℕ
⊢ ↑z.val + ↑(p * k) = z
Module: Mathlib.Algebra.Polynomial.Cardinal

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
h✝ : Subsingleton R
⊢ #R[X] ≤ max #R ℵ₀

pp: case inr
R : Type u
inst✝ : Semiring R
h✝ : Nontrivial R
⊢ #R[X] ≤ max #R ℵ₀

Tactic:
· exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
h✝ : Nontrivial R
⊢ #R[X] ≤ max #R ℵ₀
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
⊢ List.Pairwise (fun x1 x2 ↦ x1.2 > x2.2) (divisorsAntidiagonalList 0)

pp: case inr
n : ℕ
hn : n ≠ 0
⊢ List.Pairwise (fun x1 x2 ↦ x1.2 > x2.2) n.divisorsAntidiagonalList

Tactic:
· simp

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ List.Pairwise (fun x1 x2 ↦ x1.2 > x2.2) n.divisorsAntidiagonalList
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
n : ℕ
⊢ n ∈ divisors 0 → n ≤ 0

pp: case succ
n m : ℕ
⊢ n ∈ (m + 1).divisors → n ≤ m + 1

Tactic:
· simp

Goal state after:
case succ
n m : ℕ
⊢ n ∈ (m + 1).divisors → n ≤ m + 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal = n.divisorsAntidiagonal

Tactic:
rw [← coe_inj, coe_map, Equiv.coe_toEmbedding, Equiv.coe_prodComm,
    Set.image_swap_eq_preimage_swap]
  ext
  exact swap_mem_divisorsAntidiagonal

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
⊢ ∑ i ∈ divisors 0, i = ∑ i ∈ properDivisors 0, i + 0

pp: case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
· simp

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
this : (m % n).gcd n = m.gcd n
⊢ (m % n).Coprime n ↔ m.Coprime n

Tactic:
by grind

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

Goal state before:
pp: p d : ℕ
hp : Nat.Prime p
hd : 0 < d
⊢ ¬IsUnit ↑p

Tactic:
simp [isUnit_prime_iff_not_dvd hp]
  lia

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
h : ∑ x ∈ properDivisors 0, x ∣ 0
⊢ ∑ x ∈ properDivisors 0, x = 1 ∨ ∑ x ∈ properDivisors 0, x = 0

pp: case succ
n : ℕ
h : ∑ x ∈ (n + 1).properDivisors, x ∣ n + 1
⊢ ∑ x ∈ (n + 1).properDivisors, x = 1 ∨ ∑ x ∈ (n + 1).properDivisors, x = n + 1

Tactic:
· simp

Goal state after:
case succ
n : ℕ
h : ∑ x ∈ (n + 1).properDivisors, x ∣ n + 1
⊢ ∑ x ∈ (n + 1).properDivisors, x = 1 ∨ ∑ x ∈ (n + 1).properDivisors, x = n + 1
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)
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun

Tactic:
have : NeZero m := ⟨left_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
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
intro k hk

Goal state after:
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
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: x z : ℤ
y : ℕ
⊢ ↑y = x ∨ -↑y = x ↔ y = x.natAbs

Tactic:
by grind

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

Goal state before:
pp: case zero
a : ZMod 0
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = 0

pp: case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
· simp

Goal state after:
case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n✝ + 1
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case neg.succ
k n : ℕ
lt : ¬n + 1 + 1 < k
⊢ (n + 1 + 1).choose k ≤ 2 ^ (n + 1)

Tactic:
| succ n =>

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

Goal state before:
pp: case zero.succ
n : ℕ
⊢ ofDigits 0 (digits 0 (n + 1)) = n + 1

Tactic:
· simp

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

Goal state before:
pp: p m : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ p * m ≠ 0
hp₀ : 0 < p
⊢ 0 < m

Tactic:
by grind

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

Goal state before:
pp: case succ
p n : ℕ
h : ¬p ∣ n + 1
⊢ p.maxPowDvdDiv (n + 1) = (0, n + 1)

Tactic:
| succ n =>

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

Goal state before:
pp: case inl
p : ℕ
⊢ padicValNat p 0 ≤ 0

pp: case inr
p n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ≤ n

Tactic:
· simp

Goal state after:
case inr
p n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ≤ n
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
⊢ p = 0 ∨ 1 < p

Tactic:
by grind

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

Goal state before:
pp: p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
⊢ p = 0 ∨ p = 1 ∨ 1 < p

Tactic:
by grind

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

Goal state before:
pp: p : ℕ
hp : p ≠ 0
n k : ℕ
⊢ p = 1 ∨ 1 < p

Tactic:
by grind

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

Goal state before:
pp: case inl
n k : ℕ
hp : 1 ≠ 0
⊢ (1 ^ k * n).divMaxPow 1 = n.divMaxPow 1

pp: case inr
p : ℕ
hp : p ≠ 0
n k : ℕ
hp1 : 1 < p
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p

Tactic:
· simp

Goal state after:
case inr
p : ℕ
hp : p ≠ 0
n k : ℕ
hp1 : 1 < p
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case zero.succ
n✝ : ℕ
hm : n✝ + 1 ≠ 0
⊢ (digits 0 (n✝ + 1)).getLast ⋯ ≠ 0

Tactic:
· simp

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

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

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

Tactic:
· simp

Goal state after:
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: case inl
m n : ℕ
hb : 0 < succ 0
⊢ (succ 0).digits n ++ (succ 0).digits m = (succ 0).digits (n + succ 0 ^ ((succ 0).digits n).length * m)

pp: case inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
⊢ b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)

Tactic:
· simp

Goal state after:
case inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
⊢ b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl
b : ℕ
⊢ (b.digits 0).length ≤ (b.digits (0 + 1)).length

pp: case inr
b n : ℕ
hn : n ≠ 0
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
· simp

Goal state after:
case inr
b n : ℕ
hn : n ≠ 0
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
p n : ℕ
a✝ : (p.digits n).sum ≤ n
⊢ (p.digits (n + 1)).sum ≤ n + 1

Tactic:
| succ n =>

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

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

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

Tactic:
· simp

Goal state after:
case inl.inr
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
Module: Mathlib.Data.Nat.Digits.Lemmas

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

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

Tactic:
· simp

Goal state after:
case inr.inr
p n : ℕ
h : p < 1
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
Module: Mathlib.Data.Nat.Digits.Lemmas

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

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

Tactic:
· simpa [Nat.bit]

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b < ↑n
⊢ multiplicity a b < n

Tactic:
by
  exact_mod_cast multiplicity_le_emultiplicity.trans_lt h

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

Goal state before:
pp: case pos.zero
b : ℕ
h : b ≠ 1
hb : 1 < b
⊢ (b.digits 0).head! = 0 % b

pp: case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (n + 1) % b

Tactic:
· simp

Goal state after:
case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (n + 1) % b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Monoid α
a b : α
hk : ↑0 ≤ emultiplicity a b
⊢ a ^ 0 ∣ b

pp: case succ
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
hk : ↑(n✝ + 1) ≤ emultiplicity a b
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
· simp

Goal state after:
case succ
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
hk : ↑(n✝ + 1) ≤ emultiplicity a b
⊢ a ^ (n✝ + 1) ∣ b
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case pos
b f n e : ℕ
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
h✝ : n / b = 0
⊢ [(n % b).digitChar].length ≤ e + 1 + 1

pp: case neg
b f n e : ℕ
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
h✝ : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1

Tactic:
· simp

Goal state after:
case neg
b f n e : ℕ
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
h✝ : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: a b : ℕ
t : List ℕ
⊢ ofDigits (-1) (a :: b :: t) = (List.map (fun n ↦ ↑n) (a :: b :: t)).alternatingSum

Tactic:
by
    simp only [ofDigits, List.alternatingSum, List.map_cons, ofDigits_neg_one t]
    ring

Goal state after: