mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ i < sz.length

Tactic:
simpa using

Goal state after:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ i < sz.length
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: case h
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ (drop head l).length ≤ tail.sum

Tactic:
simpa using

Goal state after:
case h
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ l.length ≤ head + tail.sum
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α✝ : Type u_1
l✝ : List α✝
sz✝ : List ℕ
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ i < sz.length

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
l✝ : List α✝
sz✝ : List ℕ
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ i < sz.length
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ i < (map length (sz.splitLengths l)).length

Tactic:
simpa using

Goal state after:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ i < sz.length
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
this : (sz.splitLengths l)[i].length ≤ sz[i]
⊢ i < sz.length

Tactic:
simpa using

Goal state after:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
this : (sz.splitLengths l)[i].length ≤ sz[i]
⊢ i < sz.length
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
⊢ splitBy r l = [] ↔ l = []

Tactic:
have := flatten_splitBy r l

Goal state after:
α : Type u_1
r : α → α → Bool
l : List α
this : (splitBy r l).flatten = l
⊢ splitBy r l = [] ↔ l = []
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬([] ∈ [(a :: g).reverse].reverse ∨ [] ∈ splitBy.loop r l b [] [])

Tactic:
simpa using

Goal state after:
case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, ¬[] ∈ splitBy.loop r l a g []
a : α
g : List α
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ splitBy.loop r l b [] []
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
⊢ IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (gs.reverse ++ [(a :: g).reverse]).reverse

Tactic:
simpa using

Goal state after:
case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
⊢ IsChain (fun b a ↦ ∃ h hb, r (a.getLast ⋯) (b.head hb) = false) ((g.reverse ++ [a]) :: gs)
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2.hgs'
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ (a :: g).reverse :: gs

Tactic:
simpa using

Goal state after:
case h_2.hgs'
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ gs
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
inhabited_h : Inhabited n
i : l
j : m
h : (mulLeftLinearMap n R a) (Matrix.single j default 1) = 0 (Matrix.single j default 1)
⊢ a i j = 0 i j

Tactic:
simpa using

Goal state after:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
inhabited_h : Inhabited n
i : l
j : m
h : (mulLeftLinearMap n R a) (Matrix.single j default 1) = 0 (Matrix.single j default 1)
⊢ a i j = 0
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: m : Type u_2
n✝ : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix m m A
k n : ℕ
⊢ mulLeftLinearMap n✝ R a ^ n * mulLeftLinearMap n✝ R a = mulLeftLinearMap n✝ R (a ^ n) ∘ₗ mulLeftLinearMap n✝ R a

Tactic:
Module.End.mul_eq_comp,

Goal state after:
m : Type u_2
n✝ : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : Matrix m m A
k n : ℕ
⊢ (mulLeftLinearMap n✝ R a ^ n) ∘ₗ mulLeftLinearMap n✝ R a = mulLeftLinearMap n✝ R (a ^ n) ∘ₗ mulLeftLinearMap n✝ R a
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
inhabited_h : Inhabited l
i : m
j : n
h : (mulRightLinearMap l R a) (Matrix.single default i 1) = 0 (Matrix.single default i 1)
⊢ a i j = 0 i j

Tactic:
simpa using

Goal state after:
case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
inhabited_h : Inhabited l
i : m
j : n
h : (mulRightLinearMap l R a) (Matrix.single default i 1) = 0 (Matrix.single default i 1)
⊢ a i j = 0
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: l : Type u_1
m : Type u_2
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m m A
k n : ℕ
⊢ mulRightLinearMap l R a ^ n * mulRightLinearMap l R a = mulRightLinearMap l R (a ^ n) ∘ₗ mulRightLinearMap l R a

Tactic:
Module.End.mul_eq_comp,

Goal state after:
l : Type u_1
m : Type u_2
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m m A
k n : ℕ
⊢ (mulRightLinearMap l R a ^ n) ∘ₗ mulRightLinearMap l R a = mulRightLinearMap l R (a ^ n) ∘ₗ mulRightLinearMap l R a
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case refine_1
α : 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
⊢ Z₂ + (Z₁ - Y₂) ≠ ∅

Tactic:
simpa using

Goal state after:
case refine_1
α : 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
⊢ ¬Z₂ = 0 ∨ ¬Z₁ - Y₂ = 0
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
h0 : a ::ₘ M = X + {a}
h2 : ∀ (y : α), y ∈ Y → y < a
⊢ X + Y = M + Y

Tactic:
simpa using

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
h0 : a ::ₘ M = X + {a}
h2 : ∀ (y : α), y ∈ Y → y < a
⊢ M = X
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
this : a ∈ X + {b}
⊢ {a} ≤ X

Tactic:
simpa using

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
this : a ∈ X + {b}
⊢ a ∈ X
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
this : b ∈ a ::ₘ M
⊢ {b} ≤ M

Tactic:
simpa using

Goal state after:
case inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
this : b ∈ a ::ₘ M
⊢ b ∈ M
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case intro.intro.inr.empty
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
hN : ∀ (x : α), x ∈ 0 → x < a
⊢ Acc OneStep (M + 0)

Tactic:
simpa using

Goal state after:
case intro.intro.inr.empty
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
hN : ∀ (x : α), x ∈ 0 → x < a
⊢ Acc OneStep M
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
z : α
M N X Y : Multiset α
hM : M = X + Y
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    0 ≠ ∅ → M = X + Y → N = X + 0 → (∀ (y : α), y ∈ Y → ∃ z, z ∈ 0 ∧ y < z) → TransGen OneStep M N
hZ : z ::ₘ 0 ≠ ∅
hN : N = X + z ::ₘ 0
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ 0 ∧ y < z_1
⊢ ∀ (y : α), y ∈ Y → y < z

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Preorder α
z : α
M N X Y : Multiset α
hM : M = X + Y
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    0 ≠ ∅ → M = X + Y → N = X + 0 → (∀ (y : α), y ∈ Y → ∃ z, z ∈ 0 ∧ y < z) → TransGen OneStep M N
hZ : z ::ₘ 0 ≠ ∅
hN : N = X + z ::ₘ 0
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ 0 ∧ y < z_1
⊢ ∀ (y : α), y ∈ Y → y < z
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
⊢ TransGen OneStep M N

Tactic:
let Y' : Multiset α := Y.filter (· < z)

Goal state after:
case cons.inr
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x ↦ x < z) Y
⊢ TransGen OneStep M N
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case cons.inr.refine_2
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x ↦ x < z) Y
y : α
hy : y ∈ Y ∧ ¬y < z
⊢ ∃ z, z ∈ Z ∧ y < z

Tactic:
simpa using

Goal state after:
case cons.inr.refine_2
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x ↦ x < z) Y
y : α
hy : y ∈ Y ∧ ¬y < z
⊢ ∃ z, z ∈ Z ∧ y < z
Module: Mathlib.Data.NNRat.Floor

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

Tactic:
simpa using

Goal state after:
a✝ : ℚ≥0
h : a✝ < 0
⊢ a✝ < 1
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case zero
A : Type u_1
inst✝ : Semiring A
m : ℕ
hn_fac : IsUnit ↑(m + 0)!
⊢ IsUnit ↑m !

Tactic:
simpa using

Goal state after:
case zero
A : Type u_1
inst✝ : Semiring A
m : ℕ
hn_fac : IsUnit ↑(m + 0)!
⊢ IsUnit ↑m !
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:
simpa using

Goal state after:
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 !
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
a b : A
h : ↑p ^ m * a + ↑n * b = 1
⊢ ↑n * b = 1

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝ : CommRing A
n p : ℕ
h✝ : p.Coprime n
m : ℕ
hm : ↑p ^ m = 0
a b : A
h : ↑p ^ m * a + ↑n * b = 1
⊢ ↑n * b = 1
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:
simpa using

Goal state after:
ι : 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
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:
simpa using

Goal state after:
ι : 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
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:
simpa using

Goal state after:
ι : 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)
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
          rintro _ rfl _ _ _; rfl

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:
simpa using

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
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:
simpa using

Goal state after:
ι : 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] }
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:
simpa using

Goal state after:
ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ ∀ i ∈ t, ¬s i = 0
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:
simpa using

Goal state after:
ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ (↑t).Pairwise (Coprime on s)
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:
simpa using

Goal state after:
ι : Type u_1
a s : ι → ℕ
t : Finset ι
hs : ∀ i ∈ t, s i ≠ 0
pp : (↑t).Pairwise (Coprime on s)
⊢ ↑(chineseRemainderOfMultiset a s ⋯ ⋯ ⋯) < ∏ i ∈ t, s i
Module: Mathlib.Data.Nat.Factorization.Root

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

Tactic:
by
  simp [floorRoot_def, pos_iff_ne_zero.2, hn]; split_ifs <;> simp [*]

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

Goal state before:
pp: n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌈/⌉ n).support
⊢ Prime p ∧ p ∣ a ∧ ¬a = 0

Tactic:
simpa using

Goal state after:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌈/⌉ n).support
⊢ Prime p ∧ p ∣ a ∧ ¬a = 0
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ fib (a - 1) + fib a ≤ fib n

Tactic:
← fib_add_one (hl.1.2.trans_lt' zero_lt_two).ne'

Goal state after:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ fib (a + 1) ≤ fib n
Module: Mathlib.Data.Nat.Fib.Zeckendorf

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

Tactic:
simpa using

Goal state after:
n : ℕ
h : n.greatestFib = 0
⊢ n = 0
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.greatestFib - 1 ≠ 0

Tactic:
simpa using

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ n
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ p ^ (multiplicity p n + 1) ∣ p ^ multiplicity p n * m

Tactic:
simpa using

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ p ^ multiplicity p n * p ∣ p ^ multiplicity p n * m
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
⊢ n.minFac ^ 1 ∣ (Icc 1 (n - 1)).gcd n.choose

Tactic:
simpa using

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
⊢ n.minFac ∣ (Icc 1 (n - 1)).gcd n.choose
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ (Icc 1 (n - 1)).gcd n.choose = n.minFac

Tactic:
by
  have ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0 :=
    gcd_ne_zero_iff.mpr ⟨1, by simp; grind [IsPrimePow.two_le h]⟩
  have isPrime := minFac_prime_iff.mpr (IsPrimePow.ne_one h)
  have : multiplicity n.minFac ((Icc 1 (n - 1)).gcd n.choose) = 1 := by
    refine multiplicity_eq_of_dvd_of_not_dvd ?_ (minFac_sq_ndvd_gcd_choose_of_isPrimePow h)
    simpa using minFac_dvd_gcd_choose_of_isPrimePow h
  rw [Nat.prod_primeFactors_coe_pow_factorization ne_zero, primeFactors_gcd_choose_of_isPrimePow h]
  simp [← Nat.multiplicity_eq_factorization isPrime ne_zero, this]

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

Goal state before:
pp: case nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

Tactic:
exact ι x

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

Goal state before:
pp: p : ℕ → Prop
n n' : ℕ
hn' : n' ∈ Set.ofPred p
hp : n' ∉ ↑(range n)
⊢ n' ≥ n

Tactic:
simpa using

Goal state after:
p : ℕ → Prop
n n' : ℕ
hn' : n' ∈ Set.ofPred p
hp : n' ∉ ↑(range n)
⊢ n ≤ n'
Module: Mathlib.Data.Num.ZNum

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

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
e : a.succ.pred' = Num.pos a
this : ↑(-↑a) = -1 + ↑(-↑a + 1)
⊢ -↑a = -1 + (-↑a + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
this : ↑(-1 + ↑n + ↑n) = ↑(↑n + ↑n + -1)
⊢ -(↑(-n) + ↑(-n) + 1) = ↑n + ↑n - 1

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
this : ↑(-1 + ↑n + ↑n) = ↑(↑n + ↑n + -1)
⊢ -1 + (↑n + ↑n) = ↑n + (↑n + -1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(↑a + -↑b + (↑a + -↑b)) = ↑a + ↑a + (-↑b + -↑b)
⊢ ↑a - ↑b + (↑a - ↑b) = ↑a.bit0 - ↑b.bit0

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(↑a + -↑b + (↑a + -↑b)) = ↑a + ↑a + (-↑b + -↑b)
⊢ -↑b + (↑a + -↑b) = ↑a + (-↑b + -↑b)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + (-↑b + -1))) = ↑(↑a + -1 + (-↑b + -↑b))
⊢ ↑a - ↑b + (↑a - ↑b) - 1 = ↑a.bit0 - ↑b.bit1

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + (-↑b + -1))) = ↑(↑a + -1 + (-↑b + -↑b))
⊢ -↑b + (↑a + (-↑b + -1)) = ↑a + (-1 + (-↑b + -↑b))