mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i : m₂
j : n
⊢ (-A₁.fromRows A₂) (Sum.inr i) j = (-A₁).fromRows (-A₂) (Sum.inr i) j

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix n m₁ R
A₂ : Matrix n m₂ R
i : n
j : m₁
⊢ (-A₁.fromCols A₂) i (Sum.inl j) = (-A₁).fromCols (-A₂) i (Sum.inl j)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix n m₁ R
A₂ : Matrix n m₂ R
i : n
j : m₂
⊢ (-A₁.fromCols A₂) i (Sum.inr j) = (-A₁).fromCols (-A₂) i (Sum.inr j)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₁
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₂
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₁
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₂
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₁
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₁
val✝ : n₂
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₁
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
val✝¹ : m₂
val✝ : n₂
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Semiring R
val✝ : m₁
j✝ : n
⊢ fromRows 0 0 (Sum.inl val✝) j✝ = 0 (Sum.inl val✝) j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Semiring R
val✝ : m₂
j✝ : n
⊢ fromRows 0 0 (Sum.inr val✝) j✝ = 0 (Sum.inr val✝) j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Semiring R
i✝ : m
val✝ : n₁
⊢ fromCols 0 0 i✝ (Sum.inl val✝) = 0 i✝ (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Semiring R
i✝ : m
val✝ : n₂
⊢ fromCols 0 0 i✝ (Sum.inr val✝) = 0 i✝ (Sum.inr val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₁
val✝ : n₁
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₁
val✝ : n₂
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₂
val✝ : n₁
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₂
val✝ : n₂
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
val✝ : n₁
j✝ : m
⊢ (A₁.fromCols A₂)ᴴ (Sum.inl val✝) j✝ = A₁ᴴ.fromRows A₂ᴴ (Sum.inl val✝) j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Star R
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
val✝ : n₂
j✝ : m
⊢ (A₁.fromCols A₂)ᴴ (Sum.inr val✝) j✝ = A₁ᴴ.fromRows A₂ᴴ (Sum.inr val✝) j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i✝ : n
val✝ : m₁
⊢ (A₁.fromRows A₂)ᴴ i✝ (Sum.inl val✝) = A₁ᴴ.fromCols A₂ᴴ i✝ (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
i✝ : n
val✝ : m₂
⊢ (A₁.fromRows A₂)ᴴ i✝ (Sum.inr val✝) = A₁ᴴ.fromCols A₂ᴴ i✝ (Sum.inr val✝)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t x : Multiset α
⊢ x ∈ Finset.map equivDFinsupp.symm.toEmbedding (Finset.Icc (toDFinsupp s) (toDFinsupp t)) ↔ s ≤ x ∧ x ≤ t

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ (y : α), y ∈ Y → y < a
⊢ {a} ≠ ∅

Tactic:
simp

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

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

Tactic:
simp

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

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

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

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)
⊢ ∀ a ∈ l, (s i).Coprime (s a)

Tactic:
intro j

Goal state after:
ι : 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)
j : ι
⊢ j ∈ l → (s i).Coprime (s j)
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:
simp

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)
⊢ ∀ a ∈ l, (s i).Coprime (s a)

Tactic:
intro j

Goal state after:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
j : ι
⊢ j ∈ l → (s i).Coprime (s j)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case property
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k // ∀ i ∈ l, k ≡ a i [MOD s i] }
k : { k // k ≡ a i [MOD s i] ∧ k ≡ ↑ih [MOD (List.map s l).prod] }
⊢ ∀ a_1 ∈ l, ↑k ≡ a a_1 [MOD s a_1]

Tactic:
intro j

Goal state after:
case property
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k // ∀ i ∈ l, k ≡ a i [MOD s i] }
k : { k // k ≡ a i [MOD s i] ∧ k ≡ ↑ih [MOD (List.map s l).prod] }
j : ι
⊢ j ∈ l → ↑k ≡ a j [MOD s j]
Module: Mathlib.Data.Nat.ChineseRemainder

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

Tactic:
simp

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
⊢ ∀ a ∈ l, (s i).Coprime (s a)

Tactic:
intro j

Goal state after:
ι : 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
j : ι
⊢ j ∈ l → (s i).Coprime (s j)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case cons
ι : 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
this : (s i).Coprime (List.map s l).prod
⊢ ∀ x ∈ l, ¬s x = 0

Tactic:
intro j

Goal state after:
case cons
ι : 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
this : (s i).Coprime (List.map s l).prod
j : ι
⊢ j ∈ l → ¬s j = 0
Module: Mathlib.Data.Nat.Digits.Div

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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]
⊢ ∀ a ∈ l, (s i).Coprime (s a)

Tactic:
intro j

Goal state after:
ι : 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]
j : ι
⊢ j ∈ l → (s i).Coprime (s j)
Module: Mathlib.Data.Nat.Factorial.NatCast

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

Tactic:
simp

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

Goal state before:
pp: case pos.inl
a : ℕ
⊢ factorization 0 = a.factorization ⌊/⌋ 0

Tactic:
simp

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

Goal state before:
pp: case pos.inr
n : ℕ
⊢ factorization 0 = factorization 0 ⌊/⌋ n

Tactic:
simp

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

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

Goal state before:
pp: case inl
a b : ℕ
⊢ a ^ 0 ∣ b ↔ a ∣ floorRoot 0 b

Tactic:
simp

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

Goal state before:
pp: case inr.inl
a n : ℕ
hn : n ≠ 0
⊢ a ^ n ∣ 0 ↔ a ∣ n.floorRoot 0

Tactic:
simp

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

Goal state before:
pp: case pos.inl
a : ℕ
⊢ factorization 0 = a.factorization ⌈/⌉ 0

Tactic:
simp

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

Goal state before:
pp: case pos.inr
n : ℕ
⊢ factorization 0 = factorization 0 ⌈/⌉ n

Tactic:
simp

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

Goal state before:
pp: case pos
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : (k % p, k / p) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ 1 * ↑((n % p).choose (k % p, k / p).1 * (n / p).choose (k % p, k / p).2) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
simp

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

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
⊢ ↑(n.choose k) ≡
    ↑((n / p ^ zero).choose (k / p ^ zero)) * ↑(∏ i ∈ range zero, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (n - fib n.greatestFib).greatestFib < (n.greatestFib - 2).succ

Tactic:
greatestFib_lt,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n - fib n.greatestFib < fib (n.greatestFib - 2).succ
Module: Mathlib.Data.Nat.Hyperoperation

Goal state before:
pp: m k : ℕ
⊢ hyperoperation 1 m k = m + k

Tactic:
induction k with grind

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

Goal state before:
pp: m k : ℕ
⊢ hyperoperation 2 m k = m * k

Tactic:
induction k with grind

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

Goal state before:
pp: m k : ℕ
⊢ hyperoperation 3 m k = m ^ k

Tactic:
induction k with grind

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

Goal state before:
pp: n k : ℕ
⊢ hyperoperation (n + 4) 0 k = if Even k then 1 else 0

Tactic:
induction k with grind

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

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ 1 ∈ Icc 1 (n - 1) ∧ n.choose 1 ≠ 0

Tactic:
simp

Goal state after:
n : ℕ
h : IsPrimePow n
⊢ 1 ≤ n - 1 ∧ ¬n = 0
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
⊢ sInf {x | p x ∧ ∀ k < 0, nth p k < x} = sInf (Set.ofPred p)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn : 1 < n
hpn : ¬IsPrimePow n
⊢ (Icc 1 (n - 1)).gcd n.choose = 1

Tactic:
by
  contrapose! hpn
  obtain ⟨q, hq, h⟩ := Nat.exists_prime_and_dvd hpn
  simp_rw [Finset.dvd_gcd_iff, ← modEq_zero_iff_dvd] at h
  have : Fact (Nat.Prime q) := ⟨hq⟩
  have := eq_pow_multiplicity_of_choose_modEq_zero_nat (zero_lt_of_lt hn) h
  refine (isPrimePow_nat_iff n).mpr ⟨q, _, hq, Dvd.multiplicity_pos ?_, this.symm⟩
  specialize h 1 (by grind)
  rw [choose_one_right, modEq_zero_iff_dvd] at h
  exact h

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

Goal state before:
pp: case inl.inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < 0
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k

Tactic:
exact absurd h (zero_le _).not_gt

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

Goal state before:
pp: α : Type u
lt : α → α → Prop
inst✝ : DecidableRel lt
a b : α
⊢ cmpUsing lt a b = Ordering.eq ↔ ¬lt a b ∧ ¬lt b a

Tactic:
simp

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

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ BddBelow {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
simp

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

Goal state before:
pp: n : PosNum
⊢ ↑n + ↑n + 1 ≤ ↑n + ↑n + ↑n

Tactic:
simp

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

Goal state before:
pp: p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
⊢ nth (fun i ↦ p (i + m)) n + m = nth p n

Tactic:
refine nth_comp_of_strictMono (strictMono_id.add_const m) (fun k hk ↦ ?_)
    (fun hf ↦ lt_card_toFinset_of_nth_ne_zero h hf)
  by_contra hn
  simp_rw [id_eq, Set.mem_range, eq_comm] at hn
  exact h0 _ (not_le.mp fun h ↦ hn (le_iff_exists_add'.mp h)) hk

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

Goal state before:
pp: case succ
p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
ihk : (∀ (hf : (Set.ofPred p).Finite), k < #hf.toFinset) → count p (nth p k) = k
hn : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
⊢ nth p k ∉ {n ∈ range (nth p k) | p n}

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
α : Type u_1
inst✝ : AddGroupWithOne α
e : pred' 1 = Num.zero
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑1 + -↑1 + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑(↑a - 1) = ↑a - ↑1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ ↑(↑b - 1) = ↑b - ↑1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ ↑↑p.pred'.succ' = ↑p

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case lt
a b : PosNum
⊢ Ordering.rec (↑b < ↑a) (b = a) (↑a < ↑b) Ordering.lt →
    Ordering.rec (-↑a < -↑b) (neg a = neg b) (-↑b < -↑a) Ordering.lt

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case gt
a b : PosNum
⊢ Ordering.rec (↑b < ↑a) (b = a) (↑a < ↑b) Ordering.gt →
    Ordering.rec (-↑a < -↑b) (neg a = neg b) (-↑b < -↑a) Ordering.gt

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
ht : nil.Sized
⊢ nil.size = 0 ↔ nil = nil

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℤ
⊢ ↑↑0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℤ
⊢ ∀ (k : ℤ), 0 ≤ k → ↑↑k = k → ↑↑(k + 1) = k + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℤ
⊢ ∀ (k : ℤ), k ≤ 0 → ↑↑k = k → ↑↑(k - 1) = k - 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
x✝ : ↑m ∣ ↑n
k : ℤ
e : ↑n = ↑m * k
⊢ ↑(↑m * k) = m * ↑k

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ ↑r = ↑r₂ + ↑(Num.pos d) ↔ ↑↑r = ↑(↑r₂ + ↑d)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: d : PosNum
⊢ ↑1 + ↑d * (↑0 + ↑0) = ↑one

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit0
d n : PosNum
IH : ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
⊢ ↑(d.divMod n.bit0).2 + ↑d * ↑(d.divMod n.bit0).1 = ↑n.bit0 ∧ ↑(d.divMod n.bit0).2 < ↑d

Tactic:
unfold divMod
    -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
    revert IH; obtain ⟨q, r⟩ := divMod d n; intro IH
    simp only at IH ⊢
    apply divMod_to_nat_aux
    · simp only [Num.cast_bit0, cast_bit0]
      rw [← two_mul, ← two_mul, mul_left_comm, ← mul_add, ← IH.1]
    · simpa using IH.2

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ ↑(0 / 0) = ↑0 / ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ ↑(0 % 0) = ↑0 % ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case h₂
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) ≤ ↑(pos a) * (↑(pos a) / ↑(pos a))

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
⊢ ↑↑(n.div' d) = ↑(pos n) / ↑(pos d)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
⊢ -↑↑(n.div' d) = ↑(pos n) / ↑(neg d)

Tactic:
simp

Goal state after: