mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ TransGen OneStep = IsDershowitzMannaLT

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
⊢ WellFounded IsDershowitzMannaLT

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: a✝ : ℚ≥0
h : a✝ < 0
⊢ ⌊↑a✝⌋₊ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: a : ℚ≥0
n : ℕ
h : 0 ≤ a
⊢ n ≤ ⌊↑a⌋₊ ↔ ↑n ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: q : ℚ
⊢ q⁻¹.toNNRat = q.toNNRat⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: a : ℚ≥0
b : ℕ
⊢ (fun q ↦ ⌈↑q⌉₊) a ≤ b ↔ a ≤ ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: p q : ℚ
hp : 0 ≤ p
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: q : ℚ≥0
⊢ ⌊q⌋₊ = q.num / q.den

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.SetInterval

Goal state before:
pp: a b : ℕ
⊢ (range ⇑castOrderEmbedding).OrdConnected

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: p q : ℚ
hq : 0 ≤ q
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.SetInterval

Goal state before:
pp: a : ℕ
⊢ Nat.cast '' Iic a = Icc 0 ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.SetInterval

Goal state before:
pp: a : ℕ
⊢ Nat.cast '' Iio a = Ico 0 ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Cast.SetInterval

Goal state before:
pp: a : ℕ
⊢ IsUpperSet (range ⇑castOrderEmbedding)

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: q✝ : ℚ≥0
α : ℚ≥0 → Sort u_1
h : (m n : ℕ) → α (↑m / ↑n)
q : ℚ≥0
⊢ α q

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
x : ℚ≥0
⊢ ⌈↑x⌉₊ = ⌈x⌉₊

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ≥0
⊢ (q₁ * q₂).num = q₁.num * q₂.num / (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ≥0
⊢ (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ⌊↑x⌋ = ⌊↑x⌋

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ≥0
⊢ q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ⌈↑x⌉ = ⌈↑x⌉

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
m : ℕ
⊢ ⌈↑m⌉₊ = ↑m

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
m : ℕ
⊢ IsNat r m → IsNat ⌈r⌉₊ m

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
m : ℕ
⊢ ⌈↑(Int.negOfNat m)⌉₊ = ↑0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
m : ℕ
⊢ IsInt r (Int.negOfNat m) → IsNat ⌈r⌉₊ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈↑n / ↑d⌉₊ = res
⊢ ⌈↑n / ↑d⌉₊ = ↑⌈↑n / ↑d⌉₊

Tactic:
← @NNRat.ceil_cast R

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈↑n / ↑d⌉₊ = res
⊢ ⌈↑n / ↑d⌉₊ = ↑⌈↑(↑n / ↑d)⌉₊
Module: Mathlib.Data.NNRat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ≥0
⊢ q₁.num * q₂.num = (q₁ * q₂).num * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈↑n / ↑d⌉₊ = res
⊢ IsNat ⌈r⌉₊ res

Tactic:
by

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: R : Type u_1
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsRat r (Int.negOfNat n) d
⊢ IsNat ⌈r⌉₊ 0

Tactic:
by

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

Goal state before:
pp: n p : ℕ
hp : Prime p
h✝ : p ≤ n + 1
h : p = n + 1
⊢ p ∣ n + 1

Tactic:
by

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

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ p ∣ (n + 1)! ↔ p ≤ n + 1

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hm : m ≠ 1
⊢ m.Coprime n ! ↔ n < m.minFac

Tactic:
by

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

Goal state before:
pp: p n : ℕ
hp : Prime p
hn : n < p
⊢ p.Coprime n !

Tactic:
by

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

Goal state before:
pp: p n k : ℕ
hp : Prime p
hn : n < p
hk : k ≤ n
⊢ p.Coprime (n.descFactorial k)

Tactic:
by

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

Goal state before:
pp: p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
⊢ p ∣ (a + b).choose a

Tactic:
by

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

Goal state before:
pp: p a b : ℕ
hp : Prime p
hb : b < p
ha : a ≤ b
⊢ p.Coprime (b.choose a)

Tactic:
by

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

Goal state before:
pp: a b : ℕ
l : List ℕ
co : List.Pairwise Coprime l
⊢ a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a b : ℕ
s : ι → ℕ
i : ι
l : List ι
ih : List.Pairwise (Coprime on s) l → (a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i])
co : List.Pairwise (Coprime on s) (i :: l)
⊢ (s i).Coprime (List.map s l).prod

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a b : ℕ
s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
⊢ a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i]

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
x✝ : List.Pairwise (Coprime on s) []
⊢ ∀ i ∈ [], 0 ≡ a i [MOD s i]

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
⊢ (s i).Coprime (List.map s l).prod

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
⊢ { k // ∀ i_1 ∈ i :: l, k ≡ a i_1 [MOD s i_1] }

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ (s i).Coprime (List.map s l).prod

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ 10 % 3 = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ 10 % 9 = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑10 ≡ -1 [ZMOD ↑11]

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑n ≡ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum [ZMOD 11]

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
hs : ∀ i ∈ l, s i ≠ 0
⊢ ↑(chineseRemainderOfList a s l co) < (List.map s l).prod

Tactic:
by

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

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ (b'.digits n).sum

Tactic:
by

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

Goal state before:
pp: b b' : ℕ
c : ℤ
h : ↑b ∣ ↑b' - c
n : ℕ
⊢ b ∣ n ↔ ↑b ∣ ofDigits c (b'.digits n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑11 ∣ ↑10 - -1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ 11 ∣ n ↔ 11 ∣ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : (digits 10 n).Palindrome
h : Even (digits 10 n).length
dig : List ℤ := List.map (fun n ↦ ↑n) (digits 10 n)
⊢ Even dig.length

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : (digits 10 n).Palindrome
h : Even (digits 10 n).length
⊢ 11 ∣ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
n : ℕ
hn_fac : IsUnit ↑n !
m : ℕ
hmn : m ≤ n
⊢ IsUnit ↑m !

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
K : Type u_2
inst✝² : Semifield K
inst✝¹ : CharZero K
inst✝ : Algebra K A
n : ℕ
this : IsUnit ↑n !
⊢ IsUnit ↑n !

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
K : Type u_2
inst✝² : Semifield K
inst✝¹ : CharZero K
inst✝ : Algebra K A
n : ℕ
⊢ IsUnit ↑n !

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ (s i).Coprime (List.map s l).prod

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l : List ι
co : List.Pairwise (Coprime on s) l
z : ℕ
hz : ∀ i ∈ l, z ≡ a i [MOD s i]
⊢ z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝² : Ring A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP A p
n : ℕ
⊢ IsUnit ↑n ! ↔ n < p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : ↑p ^ m = 0
this : ∃ a b, ↑p ^ m * a + ↑n * b = 1
⊢ IsUnit ↑n

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
hlp : (List.map s l).prod = (List.map s l').prod
⊢ ∀ i ∈ l', s i ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
n p : ℕ
hp : IsNilpotent ↑p
h : p.Coprime n
⊢ IsUnit ↑n

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
hlp : (List.map s l).prod = (List.map s l').prod
⊢ ↑z < (List.map s l).prod

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
n✝ p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
n : ℕ
ih : n < p → IsUnit ↑n !
h : n + 1 < p
⊢ n < p

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
⊢ ↑(chineseRemainderOfList a s l co) = ↑(chineseRemainderOfList a s l' ⋯)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
⊢ ∀ i ∈ l, s i ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
n✝ p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
n : ℕ
ih : n < p → IsUnit ↑n !
h : n + 1 < p
⊢ 0 < n + 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : {x | x ∈ l'}.Pairwise (Coprime on s)
⊢ {x | x ∈ l}.Pairwise (Coprime on s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
n p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
h : n < p
⊢ IsUnit ↑n !

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : {x | x ∈ l'}.Pairwise (Coprime on s)
co : {x | x ∈ l}.Pairwise (Coprime on s)
lco : List.Pairwise (Coprime on s) l
⊢ ∀ {m' : Multiset ι} {e : ↑l = m'} {nod'' : m'.Nodup} {hs'' : ∀ i ∈ m', s i ≠ 0}
    {co'' : {x | x ∈ m'}.Pairwise (Coprime on s)},
    ↑(Eq.ndrec (motive := fun m ↦
          m.Nodup → (∀ i ∈ m, s i ≠ 0) → {x | x ∈ m}.Pairwise (Coprime on s) → { k // ∀ i ∈ m, k ≡ a i [MOD s i] })
          (fun nod x co ↦ chineseRemainderOfList a s l ⋯) e nod'' hs'' co'') =
      ↑(chineseRemainderOfList a s l lco)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k ∈ Finset.antidiagonal m
⊢ ↑(m.choose k.1) = ↑m ! * (↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ

Tactic:
by

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

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
hs : ∀ i ∈ l, s i ≠ 0
co' : {x | x ∈ l'}.Pairwise (Coprime on s)
co : {x | x ∈ l}.Pairwise (Coprime on s)
lco : List.Pairwise (Coprime on s) l
this :
  ∀ {m' : Multiset ι} {e : ↑l = m'} {nod'' : m'.Nodup} {hs'' : ∀ i ∈ m', s i ≠ 0}
    {co'' : {x | x ∈ m'}.Pairwise (Coprime on s)},
    ↑(Eq.ndrec (motive := fun m ↦
          m.Nodup → (∀ i ∈ m, s i ≠ 0) → {x | x ∈ m}.Pairwise (Coprime on s) → { k // ∀ i ∈ m, k ≡ a i [MOD s i] })
          (fun nod x co ↦ chineseRemainderOfList a s l ⋯) e nod'' hs'' co'') =
      ↑(chineseRemainderOfList a s l lco)
⊢ Eq.ndrec (motive := fun x ↦
      x.Nodup → (∀ i ∈ x, s i ≠ 0) → {x_1 | x_1 ∈ x}.Pairwise (Coprime on s) → { k // ∀ i ∈ x, k ≡ a i [MOD s i] })
      (fun nod x co ↦ chineseRemainderOfList a s l ⋯) ⋯ nod' hs' co' =
    chineseRemainderOfList a s l' ⋯

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ↑n.divisors = {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.divisors = Finset.image (fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) (Finset.Iic n.factorization)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Function.Injective fun x ↦ (↑x).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.divisors =
    Finset.map { toFun := fun x ↦ (↑x).prod fun x1 x2 ↦ x1 ^ x2, inj' := ⋯ } (Finset.Iic n.factorization).attach

Tactic:
by

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

Goal state before:
pp: n m : ℕ
⊢ n.dist m = m.dist n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.dist n = 0

Tactic:
by

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

Goal state before:
pp: n m : ℕ
h : n.dist m = 0
⊢ n = m

Tactic:
by

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

Goal state before:
pp: n m : ℕ
h : n = m
⊢ n.dist m = 0

Tactic:
by

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

Goal state before:
pp: n m : ℕ
h : n ≤ m
⊢ n.dist m = m - n

Tactic:
by

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

Goal state before:
pp: n m : ℕ
h : m ≤ n
⊢ n.dist m = n - m

Tactic:
by

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

Goal state before:
pp: n m : ℕ
⊢ m ≤ n.dist m + n

Tactic:
by

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

Goal state before:
pp: n m : ℕ
⊢ m ≤ n + n.dist m

Tactic:
by

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

Goal state before:
pp: n m : ℕ
⊢ n ≤ n.dist m + m

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, s i ≠ 0
pp : {x | x ∈ Quot.mk (⇑(List.isSetoid ι)) l}.Pairwise (Coprime on s)
⊢ ∀ i ∈ l, s i ≠ 0

Tactic:
by

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

Goal state before:
pp: n m : ℕ
⊢ n ≤ m + n.dist m

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.dist 0 = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ dist 0 n = n

Tactic:
by

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

Goal state before:
pp: n k m : ℕ
⊢ (n + k).dist (m + k) = n.dist m

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
m : Multiset ι
nod : m.Nodup
hs : ∀ i ∈ m, s i ≠ 0
pp : {x | x ∈ m}.Pairwise (Coprime on s)
⊢ ↑(chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s m).prod

Tactic:
by

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

Goal state before:
pp: k n m : ℕ
⊢ (k + n).dist (k + m) = n.dist m

Tactic:
by

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

Goal state before:
pp: n m k l : ℕ
h : n + m = k + l
⊢ n.dist k = l.dist m

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ ∀ i ∈ t.val, s i ≠ 0

Tactic:
by

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

Goal state before:
pp: n m k : ℕ
⊢ n.dist k ≤ n.dist m + m.dist k

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ {x | x ∈ t.val}.Pairwise (Coprime on s)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ { k // ∀ i ∈ t, k ≡ a i [MOD s i] }

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∣ n

Tactic:
by

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

Goal state before:
pp: n k m : ℕ
⊢ (n * k).dist (m * k) = n.dist m * k

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑n.properDivisors = {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

Tactic:
by

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

Goal state before:
pp: k n m : ℕ
⊢ (k * n).dist (k * m) = k * n.dist m

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.properDivisors = Finset.image (fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) (Finset.Iio n.factorization)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.properDivisors =
    Finset.map { toFun := fun x ↦ (↑x).prod fun x1 x2 ↦ x1 ^ x2, inj' := ⋯ } (Finset.Iio n.factorization).attach

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ ↑(chineseRemainderOfFinset a s t hs pp) < ∏ i ∈ t, s i

Tactic:
by

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

Goal state before:
pp: i j : ℕ
⊢ i.dist j = max i j - min i j

Tactic:
by

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

Goal state before:
pp: i j : ℕ
⊢ i.succ.dist j.succ = i.dist j

Tactic:
by

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

Goal state before:
pp: i j : ℕ
h : i ≠ j
⊢ 0 < i.dist j

Tactic:
by

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

Goal state before:
pp: a n : ℕ
⊢ n.floorRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
by

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

Goal state before:
pp: a : ℕ
⊢ floorRoot 0 a = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.floorRoot 0 = 0

Tactic:
by

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

Goal state before:
pp: a : ℕ
⊢ floorRoot 1 a = a

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.floorRoot 1 = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
a : ℕ
⊢ n.floorRoot (a ^ n) = a

Tactic:
by

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

Goal state before:
pp: a n : ℕ
⊢ n.floorRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0

Tactic:
by

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

Goal state before:
pp: a n : ℕ
⊢ ¬(n ≠ 0 ∧ a ≠ 0) ↔ n = 0 ∨ a = 0

Tactic:
by

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

Goal state before:
pp: n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ 0 ≤ a.factorization ⌊/⌋ n

Tactic:
by

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

Goal state before:
pp: n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ n ≠ 0

Tactic:
by

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

Goal state before:
pp: n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ 0 < n

Tactic:
by

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

Goal state before:
pp: n a : ℕ
⊢ (n.floorRoot a).factorization = a.factorization ⌊/⌋ n

Tactic:
by

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

Goal state before:
pp: a b n : ℕ
⊢ a ^ n ∣ b ↔ a ∣ n.floorRoot b

Tactic:
by

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

Goal state before:
pp: a n : ℕ
⊢ n.ceilRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
by

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

Goal state before:
pp: a : ℕ
⊢ ceilRoot 0 a = 0

Tactic:
by

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

Goal state before:
pp: a : ℕ
⊢ ceilRoot 0 a = 0

Tactic:
by simp [ceilRoot]

Goal state after: