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

Goal state before:
pp: 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
⊢ (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

Tactic:
ext (_ | _) (_ | _)

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

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✝)

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✝)

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✝)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: 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
⊢ (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

Tactic:
ext (_ | _) (_ | _)

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

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✝)

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✝)

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✝)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
⊢ A * B₁.fromCols B₂ = (A * B₁).fromCols (A * B₂)

Tactic:
ext _ (_ | _)

Goal state after:
case inl
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
i✝ : m
val✝ : n₁
⊢ (A * B₁.fromCols B₂) i✝ (Sum.inl val✝) = (A * B₁).fromCols (A * B₂) i✝ (Sum.inl val✝)

case inr
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
i✝ : m
val✝ : n₂
⊢ (A * B₁.fromCols B₂) i✝ (Sum.inr val✝) = (A * B₁).fromCols (A * B₂) i✝ (Sum.inr val✝)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
inst✝ : Semiring R
⊢ fromCols 0 0 = 0

Tactic:
ext _ (_ | _)

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

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✝)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: 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
⊢ A₁.fromRows A₂ * B₁.fromCols B₂ = fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)

Tactic:
ext (_ | _) (_ | _)

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

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✝)

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✝)

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✝)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂)

Tactic:
ext _ (_ | _)

Goal state after:
case inl
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
i✝ : m
val✝ : n₁
⊢ (A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂) i✝ (Sum.inl val✝) =
    (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂) i✝ (Sum.inl val✝)

case inr
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
i✝ : m
val✝ : n₂
⊢ (A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂) i✝ (Sum.inr val✝) =
    (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂) i✝ (Sum.inr val✝)
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: 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
⊢ (A₁.fromRows A₂)ᴴ = A₁ᴴ.fromCols A₂ᴴ

Tactic:
ext _ (_ | _)

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

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✝)
Module: Mathlib.Data.Multiset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.Ioc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s) - 1

Tactic:
by
  rw [Finset.card_Ioc_eq_card_Icc_sub_one, card_Icc]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))

pp: case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))

pp: case refine_4
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ ∀ (y : α), y ∈ Y₁ + (Y₂ - Z₁) → ∃ z, z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z

Tactic:
· rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]

Goal state after:
case refine_3
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))

case refine_4
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ ∀ (y : α), y ∈ Y₁ + (Y₂ - Z₁) → ∃ z, z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z
Module: Mathlib.Data.Multiset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ #(Finset.Iic s) = ∏ i ∈ s.toFinset, (count i s + 1)

Tactic:
Iic_eq_Icc,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ #(Finset.Icc ⊥ s) = ∏ i ∈ s.toFinset, (count i s + 1)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case cons.mp
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
⊢ (a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]) → ∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]

Tactic:
rintro ⟨h0, hs⟩ i

Goal state after:
case cons.mp
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h0 : a ≡ b [MOD m]
hs : ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
i : Fin (l.length + 1)
⊢ a ≡ b [MOD (m :: l).get i]
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
⊢ n = 0 → n.greatestFib = 0

Tactic:
rintro rfl

Goal state after:
⊢ greatestFib 0 = 0
Module: Mathlib.Data.Nat.Choose.Lucas

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

Tactic:
Nat.div_eq_of_lt ha₂,

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑(choose 0 0) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ∏ i ∈ range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case refine_1
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ n.minFac ^ (k - 1) ≤ n - 1

Tactic:
refine le_sub_one_of_lt ?_

Goal state after:
case refine_1
n : ℕ
h : IsPrimePow n
k : ℕ
left✝ : k ≤ log 2 n
k_pos : 0 < k
hn₁ : n = n.minFac ^ k
isPrime : Nat.Prime n.minFac
this : n.minFac ^ (k - 1) ≤ n.minFac ^ k
⊢ n.minFac ^ (k - 1) < n
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
this : multiplicity n.minFac ((Icc 1 (n - 1)).gcd n.choose) = 1
⊢ (Icc 1 (n - 1)).gcd n.choose = n.minFac

Tactic:
Nat.prod_primeFactors_coe_pow_factorization ne_zero,

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
this : multiplicity n.minFac ((Icc 1 (n - 1)).gcd n.choose) = 1
⊢ ∏ p, ↑p ^ ((Icc 1 (n - 1)).gcd n.choose).factorization ↑p = n.minFac
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case inr
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (Set.ofPred p).Infinite
⊢ a ≤ nth p k

Tactic:
rcases subset_range_nth ha with ⟨n, rfl⟩
    rwa [nth_lt_nth hf, Nat.lt_succ_iff, ← nth_le_nth hf] at h

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

Goal state before:
pp: case pos
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∀ (hf : (Set.ofPred p).Finite), a < #hf.toFinset
⊢ p (nth p a)

Tactic:
exact nth_mem a h'

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑↑(neg p) = ↑(neg p)

Tactic:
rw [cast_neg, cast_neg, Int.cast_neg, PosNum.cast_to_int]

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
hn : nth p (count p a) < a
⊢ False

Tactic:
nth_count hpa,

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
hn : a < a
⊢ False
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
this : (↑p).bit1 = (ZNum.pos p).bit1
⊢ ↑p.bit1 = ZNum.pos p.bit1

Tactic:
rwa [← ZNum.bit1_of_bit1] at this

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

Goal state before:
pp: p : PosNum
⊢ (ZNum.pos p).pred.succ = ZNum.pos p

Tactic:
ZNum.pred,

Goal state after:
p : PosNum
⊢ p.pred'.toZNum.succ = ZNum.pos p
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : r.size = 0 → l.size ≤ 1
H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size
H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
⊢ Valid' o₁ (l.balanceR x r) o₂

Tactic:
rw [Valid'.dual_iff, dual_balanceR]
  have := hr.dual.balanceL_aux hl.dual
  rw [size_dual, size_dual] at this
  exact this H₁ H₂ H₃

Goal state after:
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: case mp
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
m : ℕ+
⊢ PNat.find h = m → p m ∧ ∀ (n : ℕ+), n < m → ¬p n

Tactic:
rintro rfl

Goal state after:
case mp
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ p (PNat.find h) ∧ ∀ (n : ℕ+), n < PNat.find h → ¬p n
Module: Mathlib.Data.PNat.Interval

Goal state before:
pp: a b : ℕ+
⊢ #(Ico a b) = ↑b - ↑a

Tactic:
by
  rw [← Nat.card_Ico, ← map_subtype_embedding_Ico, card_map]

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

Goal state before:
pp: case node.nil.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
⊢ node 3 (node lls lll llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((node lls lll llx llr).node' lx nil).node' x nil
    else ((node lls lll llx llr).node' lx nil).rotateR x nil

Tactic:
have : size lll = 0 ∧ size llr = 0 := by
          have := balancedSz_zero.1 hl.1
          rwa [size, sl.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this

Goal state after:
case node.nil.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
this : lll.size = 0 ∧ llr.size = 0
⊢ node 3 (node lls lll llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((node lls lll llx llr).node' lx nil).node' x nil
    else ((node lls lll llx llr).node' lx nil).rotateR x nil
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
⊢ u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y

Tactic:
mul_comm u.x,

Goal state after:
u : XgcdType
⊢ u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.y * u.x
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMaxOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : i < j
b : α j
⊢ ∃ b, ⟨i, a⟩ < b

Tactic:
exact ⟨⟨j, b⟩, left _ _ h⟩

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : NoMinOrder ι
inst✝ : ∀ (i : ι), Nonempty (α i)
i : ι
a : α i
j : ι
h : j < i
b : α j
⊢ ∃ b, b < ⟨i, a⟩

Tactic:
exact ⟨⟨j, b⟩, left _ _ h⟩

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t ↦ (↑t).2) <$$> abs ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = y

Tactic:
yeq,

Goal state after:
case h.right
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a ⟹ α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)
⊢ (fun i t ↦ (↑t).2) <$$> abs ⟨a, fun i j ↦ ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = abs ⟨a, f₁⟩
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
⊢ (∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ) →
    ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u

Tactic:
grind [liftP_iff]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ M.dest (P F) (corecF g x) = (TypeVec.id ::: corecF g) <$$> repr (g x)

Tactic:
corecF,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ M.dest (P F) (M.corec (P F) (fun x ↦ repr (g x)) x) =
    (TypeVec.id ::: M.corec (P F) fun x ↦ repr (g x)) <$$> repr (g x)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : Cofix F α
⊢ ∀ (b : Cofix F α), r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b

Tactic:
apply Quot.inductionOn
            (motive := fun c =>
              ∀ b, r c b → Quot.lift (Quot.mk r') h₁ c = Quot.lift (Quot.mk r') h₁ b) c

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := ⋯
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : Cofix F α
⊢ ∀ (a : (P F).M α) (b : Cofix F α),
    r (Quot.mk Mcongr a) b → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a) = Quot.lift (Quot.mk r') h₁ b
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ ∃ l', Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size

Tactic:
exists t_l.size

Goal state after:
case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ Raised (erase x t_l).size t_l.size ∧ BalancedSz t_l.size t_r.size
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.right
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a → α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ (fun t ↦ (↑t).2) <$> abs ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩ = y

Tactic:
yeq,

Goal state after:
case h.right
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a → α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ (fun t ↦ (↑t).2) <$> abs ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩ = abs ⟨a, f₁⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ (corecF g x).dest = (P F).map (corecF g) (repr (g x))

Tactic:
corecF,

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ (PFunctor.M.corec (fun x ↦ repr (g x)) x).dest = (P F).map (PFunctor.M.corec fun x ↦ repr (g x)) (repr (g x))
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ ((prod.fst ⊚ subtypeVal R) ⊚ h) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x

Tactic:
comp_assoc,

Goal state after:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst✝¹ : MvFunctor F'
inst✝ : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ R
hh : subtypeVal R ⊚ h = (f ⊗' g) ⊚ prod.diag
⊢ (prod.fst ⊚ subtypeVal R ⊚ h) <$$> x = f <$$> x ∧ (prod.snd ⊚ subtypeVal R) <$$> h <$$> x = g <$$> x