mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.Extend

Goal state before:
pp: case right
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left✝² : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left✝¹ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
left✝ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s' : F.obj i ⟶ X
w' : f = c.π.app i ≫ toProfinite.map s'
⊢ StructuredArrow.Hom.right (𝟙 ((e.inverse ⋙ functor c).obj { down := i })) ≫
      StructuredArrow.Hom.right { left := left✝¹, right := s, w := w } =
    StructuredArrow.Hom.right (𝟙 ((e.inverse ⋙ functor c).obj { down := i })) ≫
      StructuredArrow.Hom.right { left := left✝, right := s', w := w' }

Tactic:
rw [w] at w'

Goal state after:
case right
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left✝² : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left✝¹ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
left✝ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s' : F.obj i ⟶ X
w'✝ : f = c.π.app i ≫ toProfinite.map s'
w' : c.π.app i ≫ toProfinite.map s = c.π.app i ≫ toProfinite.map s'
⊢ StructuredArrow.Hom.right (𝟙 ((e.inverse ⋙ functor c).obj { down := i })) ≫
      StructuredArrow.Hom.right { left := left✝¹, right := s, w := w } =
    StructuredArrow.Hom.right (𝟙 ((e.inverse ⋙ functor c).obj { down := i })) ≫
      StructuredArrow.Hom.right { left := left✝, right := s', w := w'✝ }
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj X✝) ≫ (functor R).map f =
    (functorIsoDiscreteAux₂ R X✝).inv ≫
      (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f) ≫
        (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)

Tactic:
← (discreteUnderlyingAdj (ModuleCat R)).counit_naturality

Goal state after:
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) ≫
      (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝) =
    (functorIsoDiscreteAux₂ R X✝).inv ≫
      (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f) ≫
        (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj X✝) ≫ (functor R).map f =
    (functorIsoDiscreteAux₂ R X✝).inv ≫
      (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map ((Functor.const LightProfiniteᵒᵖ).map f) ≫
        (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)

Tactic:
← (discreteUnderlyingAdj (ModuleCat R)).counit_naturality

Goal state after:
P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) ≫
      (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝) =
    (functorIsoDiscreteAux₂ R X✝).inv ≫
      (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map ((Functor.const LightProfiniteᵒᵖ).map f) ≫
        (functorIsoDiscreteAux₂ R Y✝).hom ≫ (discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj Y✝)
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : Profinite
inst✝¹ : Nonempty ↑S.toTop
inst✝ : Finite ↑S.toTop
X Y : Profinite
g : X ⟶ S
f : X ⟶ Y
x✝ : Mono f
⊢ ∃ h, f ≫ h = g

Tactic:
have (T : Profinite.{u}) [Nonempty T] : IsSplitEpi (CompHausLike.isTerminalPUnit.from T) :=
      IsSplitEpi.mk' { section_ := CompHausLike.const _ (Nonempty.some inferInstance) }
    obtain ⟨k, _, h2⟩ := exists_lift_of_finite_of_mono_of_epi f
        (CompHausLike.isTerminalPUnit.from S) g (CompHausLike.isTerminalPUnit.from Y)
      (CompHausLike.isTerminalPUnit.hom_ext _ _)
    exact ⟨k, h2⟩

Goal state after:
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ map f <$> traverse g x = traverse (map f ∘ g) x

Tactic:
map_eq_traverse_id f

Goal state after:
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ (Id.run ∘ traverse (pure ∘ f)) <$> traverse g x = traverse (map f ∘ g) x
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : List α
⊢ List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) x = Comp.mk (List.traverse f <$> List.traverse g x)

Tactic:
induction x <;> simp! [*, functor_norm] <;> rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: σ α β : Type u
f : α → β
x : σ ⊕ α
⊢ Sum.traverse (pure ∘ f) x = pure (f <$> x)

Tactic:
induction x <;> simp! [*, functor_norm] <;> rfl

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
n : ℕ
⊢ (List.foldl (fun l x ↦ { down := l.down + 1 }) { down := n } ys).down = ys.length + n

Tactic:
induction ys generalizing n with
  | nil => simp
  | cons _ _ ih => simp +arith [ih]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u} n
β : TypeVec.{v} n
f g : α ⟹ β
⊢ (∀ (i : Fin2 n), f i = g i) → f = g

Tactic:
by
  intro h; funext i; apply h

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
⊢ Part.fix ⇑f ≤ X

Tactic:
rw [fix_eq_ωSup f]
  apply ωSup_le _ _ _
  simp only [Fix.approxChain]
  intro i
  induction i with
  | zero => apply bot_le
  | succ _ i_ih =>
    trans f X
    · apply f.monotone i_ih
    · apply hX

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x : t' α
⊢ ⇑(eqv α) <$> traverse pure ((eqv α).symm x) = pure x

Tactic:
id_traverse,

Goal state after:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x : t' α
⊢ ⇑(eqv α) <$> pure ((eqv α).symm x) = pure x
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case h_fst
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
n : ↑ℕ∪{∞}.toTop
x : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop
⊢ (ConcreteCategory.hom (((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ fst S ℕ∪{∞})) x =
    (ConcreteCategory.hom
        ((lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
              (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
            y' ▷ ℕ∪{∞}) ≫
          fst S ℕ∪{∞}))
      x

pp: case h_snd
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
n : ↑ℕ∪{∞}.toTop
x : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop
⊢ (ConcreteCategory.hom (((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ snd S ℕ∪{∞})) x =
    (ConcreteCategory.hom
        ((lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
              (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
            y' ▷ ℕ∪{∞}) ≫
          snd S ℕ∪{∞}))
      x

Tactic:
exacts [x.prop n ∞, (x.val n).prop]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Type u_2
n' m : ℕ
h : m ≤ n
a : Fin n' → α
⊢ take (m * n') ⋯ («repeat» n a) = «repeat» m a

Tactic:
ext i
  simp only [take, repeat_apply, modNat, val_castLE]

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

Goal state before:
pp: α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
obtain ⟨H₁, H₂⟩ := forall_mem_cons.1 H

Goal state after:
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
⊢ lookmap f (a :: l) = lookmap g (a :: l)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (lookupAll a (⟨a', b⟩ :: l)).head? = dlookup a (⟨a', b⟩ :: l)

Tactic:
by_cases h : a = a'
    · subst h; simp
    · rw [lookupAll_cons_ne, dlookup_cons_ne, head?_lookupAll a l] <;> assumption

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by
  convert!
    Finset.exists_between (s := hsf.toFinset) (t := htf.toFinset) (by simpa) (by simpa)
      (by simpa) using
    1; simp

Goal state after:
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f : α →₀ N
a✝ : α
⊢ a✝ ∈ f.neLocus 0 ↔ a✝ ∈ f.support

Tactic:
rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (i :: is) (d :: ds)

Tactic:
rw [← h]

Goal state after:
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (↑t) (d :: ds)
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: n : ℕ
hn : n = 0
⊢ fib (-↑n + 1) * fib (-↑n - 1) - fib (-↑n) ^ 2 = (-1) ^ (-↑n).natAbs

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
⊢ CPRankMax (d :: ds).prod x

Tactic:
have :
      CPRankMax (Finset.card (Finset.attach (Finset.range d)) * prod ds)
        (∑ i ∈ Finset.attach (Finset.range d),
          unitVec d i.val ⊗ slice x i.val (mem_range.1 i.2)) :=
      cprankMax_sum (Finset.range d).attach _ fun i _ => h_summands i

Goal state after:
α : Type
inst✝ : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this : CPRankMax ((Finset.range d).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
⊢ CPRankMax (d :: ds).prod x
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
⊢ 0 < ↑r

Tactic:
positivity

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case a
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ 0 ≤ b

Tactic:
positivity

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

Goal state before:
pp: case nil
α : Type u_1
l : List α
⊢ foldl (flip cons) [] [] = [].reverse

Tactic:
simp [flip, foldl_eq_foldr_reverse, -foldr_reverse]

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

Goal state before:
pp: case cons
α : Type u_1
l : List α
head✝ : α
tail✝ : List α
tail_ih✝ : foldl (flip cons) [] tail✝ = tail✝.reverse
⊢ foldl (flip cons) [] (head✝ :: tail✝) = (head✝ :: tail✝).reverse

Tactic:
simp [flip, foldl_eq_foldr_reverse, -foldr_reverse]

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

Goal state before:
pp: α : Type u_1
l : List α
i j : ℕ
⊢ (l.rdrop i).rdrop j = l.rdrop (i + j)

Tactic:
rdrop_eq_reverse_drop_reverse,

Goal state after:
α : Type u_1
l : List α
i j : ℕ
⊢ (drop j (drop i l.reverse).reverse.reverse).reverse = (drop (i + j) l.reverse).reverse
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
⊢ (l₁ ++ l₂).rdrop l₂.length = l₁

Tactic:
rdrop_eq_reverse_drop_reverse,

Goal state after:
α : Type u_1
l₁ l₂ : List α
⊢ (drop l₂.length (l₁ ++ l₂).reverse).reverse = l₁
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k

Tactic:
rdrop_eq_reverse_drop_reverse,

Goal state after:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
⊢ (drop k (l₁ ++ l₂).reverse).reverse = l₁ ++ l₂.rdrop k
Module: Mathlib.Data.List.Palindrome

Goal state before:
pp: α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : (l ++ [y]).reverse ++ [x] = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome

Tactic:
reverse_append

Goal state after:
α : Type u_1
l✝ : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
⊢ (x :: (l ++ [y])).Palindrome
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
hnm : n < m
⊢ filter (fun x ↦ decide (x ≤ n)) (Ico n m) = [n]

Tactic:
rw [← filter_lt_of_succ_bot hnm]

Goal state after:
n m : ℕ
hnm : n < m
⊢ filter (fun x ↦ decide (x ≤ n)) (Ico n m) = filter (fun x ↦ decide (x < n + 1)) (Ico n m)
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
⊢ v.HasPeriod p

Tactic:
suffices ∀ j < v.length - p, v[j]? = v[j + p]? by simpa [hasPeriod_iff_getElem?]

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
⊢ ∀ j < v.length - p, v[j]? = v[j + p]?
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case neg
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
⊢ (take n w ++ w)[j]? = w[j % p]?

Tactic:
have j_mod : (j - n) % p = j % p := by
        calc
          (j - n) % p = (j - p * (n / p)) % p := by rw [Nat.mul_div_cancel' dvd]
          _ = j % p := sub_mul_mod ((Nat.mul_div_cancel' dvd).symm ▸ n_le_j)

Goal state after:
case neg
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
j_mod : (j - n) % p = j % p
⊢ (take n w ++ w)[j]? = w[j % p]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ y.head ⋯ ∈ m.head?

Tactic:
· simp_rw [← head_of_mem_head? hy, head_head_splitBy _ hm]
    exact head_mem_head? _

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

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

Tactic:
Prime.dvd_factorial hp

Goal state after:
n p : ℕ
hp : Prime p
⊢ p ∣ n + 1 ∨ p ≤ n ↔ p ≤ n + 1
Module: Mathlib.Data.Nat.Prime.Factorial

Goal state before:
pp: case mp
m n : ℕ
hm : m ≠ 1
h : m.minFac ≤ n
⊢ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !

Tactic:
exact ⟨m.minFac, minFac_prime hm, minFac_dvd m, Nat.dvd_factorial (minFac_pos m) h⟩

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

Goal state before:
pp: case cons
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)
⊢ a ≡ b [MOD (m :: l).prod] ↔ ∀ (i : Fin (m :: l).length), a ≡ b [MOD (m :: l).get i]

Tactic:
have : Coprime m l.prod := coprime_list_prod_right_iff.mpr (List.pairwise_cons.mp co).1
    simp only [List.prod_cons, ← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co),
      List.length_cons]
    constructor
    · rintro ⟨h0, hs⟩ i
      cases i using Fin.cases <;> simp_all
    · intro h; exact ⟨h 0, fun i => h i.succ⟩

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

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

Tactic:
simp [hn]

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

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

Tactic:
simp [hn]

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

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

Tactic:
simp [hn]

Goal state after:
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
p : ℕ
hp₁ : Nat.Prime p
hp₃ : ¬(Icc 1 (n - 1)).gcd n.choose = 0
this✝ : Fact (Nat.Prime p)
hp₂ : ∀ b ∈ Icc 1 (n - 1), n.choose b ≡ 0 [MOD p]
this : n = p ^ multiplicity p n
⊢ p = n.minFac

Tactic:
have dvd_pow : n.minFac ∣  p ^ multiplicity p n := this ▸ minFac_dvd _

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
p : ℕ
hp₁ : Nat.Prime p
hp₃ : ¬(Icc 1 (n - 1)).gcd n.choose = 0
this✝ : Fact (Nat.Prime p)
hp₂ : ∀ b ∈ Icc 1 (n - 1), n.choose b ≡ 0 [MOD p]
this : n = p ^ multiplicity p n
dvd_pow : n.minFac ∣ p ^ multiplicity p n
⊢ p = n.minFac
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Infinite
⊢ Set.range (Subtype.val ∘ ⇑(Subtype.orderIsoOfNat (Set.ofPred p))) = Set.ofPred p

Tactic:
have := hf.to_subtype

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Infinite
this : Infinite ↑(Set.ofPred p)
⊢ Set.range (Subtype.val ∘ ⇑(Subtype.orderIsoOfNat (Set.ofPred p))) = Set.ofPred p
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case refine_2
p : ℕ → Prop
x : ℕ
h : p x
hf : (Set.ofPred p).Infinite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
· rw [← @Set.mem_ofPred_eq _ _ p, ← range_nth_of_infinite hf] at h
    rcases h with ⟨n, hx⟩
    exact ⟨n, fun hf' => absurd hf' hf, hx⟩

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 : ℕ
hf : (Set.ofPred p).Finite
hn : #⋯.toFinset ≤ n
⊢ (hf.toFinset.sort fun a b ↦ a ≤ b).length ≤ n

Tactic:
simp [hn]

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

Goal state before:
pp: case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

Tactic:
rcases id ll with _ | lls
      · rcases lr with _ | ⟨_, _, lrx⟩
        · exact node 2 l x nil
        · exact node 3 (ι lx) lrx ι x
      · rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)

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

Goal state before:
pp: case node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

Tactic:
rcases id ll with _ | lls
      · rcases lr with _ | ⟨_, _, lrx⟩
        · exact node 2 l x nil
        · exact node 3 (ι lx) lrx ι x
      · rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
this : Valid' o₁ t o₂
⊢ Valid' o₁ t o₂

Tactic:
OrderDual.Preorder.dual_dual

Goal state after:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
this : Valid' o₁ t o₂
⊢ Valid' o₁ t o₂
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ nth p k < n

Tactic:
refine (count_monotone p).reflect_lt ?_

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ count p (nth p k) < count p n