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:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (if hx : x = y then (z :: l).getLast ⋯ else if x = z then y else (z :: l).prev x ⋯) = (z :: l).getLast ⋯

Tactic:
dif_pos hx

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (z :: l).getLast ⋯ = (z :: l).getLast ⋯
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : a = x
⊢ some y = (y :: tail)[idxOf a (x :: y :: tail)]?

Tactic:
grind

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

Goal state before:
pp: case neg.ha
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : ¬a = x
⊢ a ∈ (y :: tail).dropLast

Tactic:
grind

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
w✝ : List α
h✝ : l.dropLast ++ w✝ = l
⊢ [a, l.nextOr a d].length + idxOf a l ≤ l.length

Tactic:
grind

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
h' : (x :: y :: tail).getLast hl = x
⊢ y = d

Tactic:
grind

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
h' : ¬(x :: y :: tail).getLast hl = x
⊢ (y :: tail).getLast ⋯ ∉ (y :: tail).dropLast

Tactic:
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:
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:
grind

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
hl : l ≠ []
ha' : a ∉ l.dropLast
⊢ l.next a ha = l[(idxOf a l + 1) % l.length]

Tactic:
grind [dropLast_append_getLast, next_getLast_eq_head_of_notMem_dropLast, Nat.mod_self]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ []
ha₀ : a ≠ [].head ⋯
⊢ some ([].prev a ha) = [][idxOf a [] - 1]?

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a head✝ : α
ha : a ∈ [head✝]
ha₀ : a ≠ [head✝].head ⋯
⊢ some ([head✝].prev a ha) = [head✝][idxOf a [head✝] - 1]?

Tactic:
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:
grind

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

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

Tactic:
grind

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:
grind

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
tail : List α
ha : a ∈ a :: tail
⊢ (a :: tail).getLast ⋯ = (a :: tail)[tail.length]

Tactic:
grind

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

Goal state before:
pp: case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 < (head :: tail).length

Tactic:
grind

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

Goal state before:
pp: case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ idxOf a (head :: tail)

Tactic:
grind

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

Goal state before:
pp: case neg.e_i.h
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ (head :: tail).length

Tactic:
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:
grind

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

Goal state before:
pp: case nil.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
hab : (IsRotated.setoid α) [] []
⊢ (match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
rfl

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
⊢ Chain r (map f ⟦[]⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦[]⟧

Tactic:
rfl

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 ++ [a]
⊢ r a b

Tactic:
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:
grind

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:
rfl

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

Goal state before:
pp: case h
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
a✝ : ↑(orbitRel.Quotient.orbit ω)
⊢ ((Quotient.mk'' a✝).liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯).liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯ = Quotient.mk'' a✝

Tactic:
rfl

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

Goal state before:
pp: case h
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
a✝ : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
⊢ Quotient.liftOn' ((Quotient.mk'' a✝).liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯) (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯ = Quotient.mk'' a✝

Tactic:
rfl

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

Goal state before:
pp: case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ++ b.primeFactorsList
⊢ Prime p

Tactic:
List.mem_append

Goal state after:
case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
⊢ Prime p
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
⊢ comap f H = comap f.rangeRestrict (H.subgroupOf f.range)

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.1 = a.cast

Tactic:
rfl

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.2 = a.cast

Tactic:
rfl

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ Nat.cast ∘ val = cast

Tactic:
rfl

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

Goal state before:
pp: case zero
a b : ZMod 0
⊢ (a + b).cast = a.cast + b.cast

Tactic:
rfl

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

Goal state before:
pp: case neg
n : ℕ
a b : Fin (n + 1)
h : ¬n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) = cast a + cast b

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ ringEquivCongr ⋯ = RingEquiv.refl (ZMod 0)

Tactic:
rfl

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ ringEquivCongr ⋯ = RingEquiv.refl (ZMod (n✝ + 1))

Tactic:
rfl

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

Goal state before:
pp: a : ℕ
x : ZMod a
⊢ (RingEquiv.refl (ZMod a)) x = x

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯

Tactic:
rfl

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯

Tactic:
rfl

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case zero
x : ZMod 0
⊢ ((ringEquivCongr ⋯) x).val = x.val

Tactic:
rfl

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

Goal state before:
pp: case succ
n✝ : ℕ
x : ZMod (n✝ + 1)
⊢ ((ringEquivCongr ⋯) x).val = x.val

Tactic:
rfl

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

Goal state before:
pp: case zero
a : ℤ
⊢ cast a = a

Tactic:
rfl

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

Goal state before:
pp: case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = ↑↑↑a

Tactic:
rfl

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

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

Tactic:
val_neg_one,

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁴ : Ring R✝
n : ℕ
R : Type u_2
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module (ZMod n) R
inst✝ : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
x : ZMod n
y : R
z : M
⊢ (algebraMap (ZMod n) R) x • y • z = x • y • z

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ #R[X] = max #R ℵ₀

Tactic:
simp [(toFinsuppIso R).toEquiv.cardinal_eq]

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

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + (↑n + 1) * ↑(a.val.gcdB n.succ) = a * ↑(a.val.gcdA n.succ) + (↑n + 1) * ↑(a.val.gcdB n.succ)

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
h : x ∈ n.divisorsAntidiagonal
⊢ x.1 ∈ n.divisors

Tactic:
by
  rw [mem_divisorsAntidiagonal] at h
  simp [Dvd.intro _ h.1, h.2]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
d k : ℕ
hn : d * k ≠ 0
⊢ d * (d * k / d) = d * k ∧ d * k ≠ 0

Tactic:
rw [Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt]

Goal state after:
case mp
d k : ℕ
hn : d * k ≠ 0
⊢ d * k = d * k ∧ d * k ≠ 0
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:
grind

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

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

Tactic:
rfl

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

Goal state before:
pp: case inl.right.«0»
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⇑(castHom ⋯ (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x ↦
    if 0 * 1 = 0 then
      if 0 = 1 then ((RingHom.snd (ZMod 0) (ZMod 1)) x).cast else ((RingHom.fst (ZMod 0) (ZMod 1)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 0 * 1 = 0
x : ZMod 0
⊢ to_fun (inv_fun (x, (fun i ↦ i) ⟨0, ⋯⟩)) = (x, (fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [to_fun, inv_fun, castHom, Prod.ext_iff, eq_iff_true_of_subsingleton]

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

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

Tactic:
rfl

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

Goal state before:
pp: case inr.right.«0»
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⇑(castHom ⋯ (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x ↦
    if 1 * 0 = 0 then
      if 1 = 1 then ((RingHom.snd (ZMod 1) (ZMod 0)) x).cast else ((RingHom.fst (ZMod 1) (ZMod 0)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 1 * 0 = 0
y : ZMod 0
⊢ to_fun (inv_fun ((fun i ↦ i) ⟨0, ⋯⟩, y)) = ((fun i ↦ i) ⟨0, ⋯⟩, y)

Tactic:
simp [to_fun, inv_fun, castHom, Prod.ext_iff, eq_iff_true_of_subsingleton]

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

Goal state before:
pp: case inr.right
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ RightInverse inv_fun to_fun

Tactic:
rintro ⟨x, y⟩
          fin_cases x
          simp [to_fun, inv_fun, castHom, Prod.ext_iff, eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x ∈ n.divisors,
      f ({ toFun := fun d ↦ (d, n / d), inj' := ⋯ } x).1 ({ toFun := fun d ↦ (d, n / d), inj' := ⋯ } x).2 =
    ∏ i ∈ n.divisors, f i (n / i)

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.primeFactors = {p ∈ n.divisors | Prime p}

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ image (fun x ↦ n / x) n.divisors = image (Prod.fst ∘ ⇑{ toFun := fun d ↦ (n / d, d), inj' := ⋯ }) n.divisors

Tactic:
rfl

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

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (a + a * (b - 1)) / (b - 1) = a + a / (b - 1)

Tactic:
Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb),

Goal state after:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / (b - 1) + a = a + a / (b - 1)
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case ofNat.ofNat.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ a✝¹ * a✝ = a✝² ∧ ¬a✝² = 0 ∨ (0 = a✝² ∧ ¬a✝² = 0) ∧ a✝¹ = 0 ∧ a✝ = 0 ↔ ↑a✝¹ * ↑a✝ = ↑a✝² ∧ ¬a✝² = 0

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case ofNat.ofNat.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ (0 = a✝² ∧ ¬a✝² = 0) ∧ a✝¹ = 0 ↔ ↑a✝¹ * -[a✝+1] = ↑a✝² ∧ ¬a✝² = 0

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case ofNat.negSucc.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (0 = a✝² ∧ ¬a✝² = 0) ∧ a✝ = 0 ↔ -[a✝¹+1] * ↑a✝ = ↑a✝² ∧ ¬a✝² = 0

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case negSucc.ofNat.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ ¬↑a✝¹ * ↑a✝ = -[a✝²+1]

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case negSucc.ofNat.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ a✝¹ * (a✝ + 1) = a✝² + 1 ↔ ↑a✝¹ * -[a✝+1] = -[a✝²+1]

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case negSucc.negSucc.ofNat
a✝² a✝¹ a✝ : ℕ
⊢ (a✝¹ + 1) * a✝ = a✝² + 1 ↔ -[a✝¹+1] * ↑a✝ = -[a✝²+1]

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case negSucc.negSucc.negSucc
a✝² a✝¹ a✝ : ℕ
⊢ ¬-[a✝¹+1] * -[a✝+1] = -[a✝²+1]

Tactic:
grind

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

Goal state before:
pp: case «1»
⊢ ↑(-1) = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
⊢ (-↑0).divisorsAntidiag =
    (map (Nat.castEmbedding.prodMap negNatCast) (Nat.divisorsAntidiagonal 0)).disjUnion
      (map (negNatCast.prodMap Nat.castEmbedding) (Nat.divisorsAntidiagonal 0)) ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
n✝ : ℕ
⊢ (-↑(n✝ + 1)).divisorsAntidiag =
    (map (Nat.castEmbedding.prodMap negNatCast) (n✝ + 1).divisorsAntidiagonal).disjUnion
      (map (negNatCast.prodMap Nat.castEmbedding) (n✝ + 1).divisorsAntidiagonal) ⋯

Tactic:
rfl

Goal state after:
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)

pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ 0 < ↑r !

Tactic:
· norm_cast
    rw [← Nat.descFactorial_eq_factorial_mul_choose]
    exact n.pow_sub_le_descFactorial r

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ 0 < ↑r !
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
⊢ 4 = 2 ^ 2

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ 4 = 2 ^ 2

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
⊢ 2 ∣ (n + 1).centralBinom

Tactic:
use (n + 1 + n).choose n
  rw [centralBinom_eq_two_mul_choose, two_mul, ← add_assoc,
      choose_succ_succ' (n + 1 + n) n, choose_symm_add, ← two_mul]

Goal state after:
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:
rfl

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

Goal state before:
pp: case zero
b : ℕ
⊢ ofDigits b (List.replicate 0 0) = 0

Tactic:
rfl

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

Goal state before:
pp: case cons.w₂
b : ℕ
h✝ : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
h : L ≠ []
⊢ L.getLast h ≠ 0

Tactic:
List.getLast_cons h

Goal state after:
case cons.w₂
b : ℕ
h✝ : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
h : L ≠ []
w₂ : L.getLast h ≠ 0
⊢ L.getLast h ≠ 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero.zero
⊢ ofDigits 0 (digits 0 0) = 0

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case succ.succ.ind.zero
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) [] = 0

Tactic:
rfl

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:
grind

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

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

Tactic:
rfl

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:
rfl

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

Goal state before:
pp: case cons
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun x ↦ n * x) tl)
⊢ n * ofDigits b (hd :: tl) = ofDigits b (List.map (fun x ↦ n * x) (hd :: tl))

Tactic:
| cons hd tl ih =>

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

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

Tactic:
grind

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

Goal state before:
pp: case inr
p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
hp₁ : 1 < p
⊢ p ^ k ∣ n ↔ k ≤ padicValNat p n

Tactic:
· exact pow_dvd_iff_le_of_spec hp₁ hn (pow_padicValNat_mul_divMaxPow p n)
      (not_dvd_divMaxPow hp₁ hn)

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:
grind

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

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

Tactic:
grind

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

Goal state before:
pp: b hd : ℕ
tl : List ℕ
IH : (∀ x ∈ tl, x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
⊢ b + 2 ≤ b + 2

Tactic:
rfl

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

Goal state before:
pp: b m n : ℕ
⊢ ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m

Tactic:
by
  rw [ofDigits_append, ofDigits_digits, ofDigits_digits]

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:
rfl

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

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

Tactic:
| cons hd tl ih =>

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

Goal state before:
pp: case inr.inr.nil
p : ℕ
h : p < 1
h_nonempty : [] ≠ []
h_ne_zero : [].getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ [], l < p
⊢ 0 = ofDigits 0 [] - [].sum

Tactic:
rfl

Goal state after: