mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case prim.prec
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Nat.Primrec' f
a✝ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval (v.head :: (↑v).tail) =
    pure
      (pure
        (Nat.rec (f (v.head ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (v.head ::ᵥ v.tail).tail))
          (v.head ::ᵥ v.tail).head))

Tactic:
induction v.head with
      | zero => simp [prec, hf, Bind.bind]
      | succ n _ =>
      suffices ∀ a b, a + b = n →
        (n.succ :: 0 ::
          g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
              v.val.tail : List ℕ) ∈
          PFun.fix
            (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail))
              (fun x => Part.some (if v.tail.headI = 0
                then Sum.inl
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail : List ℕ)
                else Sum.inr
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail))))
            (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by
        have := Part.eq_some_iff.mpr (this _ _ (zero_add _))
        simp [prec, Part.bind_assoc, Bind.bind]
        simp_all
      intro a b e
      induction b generalizing a with
      | zero =>
        refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)
        simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]
        rfl
      | succ b IH =>
        refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH (a + 1) (by rwa [add_right_comm])⟩)
        simp only [hg, Part.bind_some, List.tail_cons, pure]
        exact Part.mem_some_iff.2 rfl

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case prim.prec
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Nat.Primrec' f
a✝ : Nat.Primrec' g
IHf : ∃ c, ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> ↑f v
IHg : ∃ c, ∀ (v : List.Vector ℕ (n + 2)), c.eval ↑v = pure <$> ↑g v
⊢ ∃ c,
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval ↑v = pure <$> (↑fun v ↦ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head) v

Tactic:
| @prec n f g _ _ IHf IHg =>

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case comp
k' : Cont
c c' : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'

Tactic:
| comp c c' _ ih' =>

Goal state after:
Module: Mathlib.Topology.Category.Stonean.Limits

Goal state before:
pp: X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ ∀ ⦃X Y B : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y⦄ (f : X ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g

Tactic:
intro _ _ _ _ _ hi

Goal state after:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi✝ : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
X✝ Y✝ B✝ : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y
f✝ : X✝ ⟶ B✝
g✝ : Y✝ ⟶ B✝
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f✝)
⊢ HasExplicitPullback f✝ g✝
Module: Mathlib.Condensed.Basic

Goal state before:
pp: C : Type w
inst✝ : Category.{v, w} C
X Y : Condensed C
f g : X ⟶ Y
h : ∀ (S : CompHausᵒᵖ), f.hom.app S = g.hom.app S
⊢ f = g

Tactic:
by
  ext
  exact h _

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some (head main q), var := s, stk := elim (trList L) [] c d }
    { l := some q, var := none, stk := elim (trList [L.headI]) [] c d }

Tactic:
let o : Option Γ' := List.casesOn L none fun _ _ => some Γ'.cons
  refine
    (move_ok (by decide)
          (splitAtPred_eq _ _ (trNat L.headI) o (trList L.tail) (trNat_natEnd _) ?_)).trans
      (TransGen.head rfl (TransGen.head rfl ?_))
  · cases L <;> simp [o]
  rw [tr]
  simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_update_main, elim_rev, elim_update_rev,
    Function.update_self, trList]
  rw [if_neg (show o ≠ some Γ'.consₗ by cases L <;> simp [o])]
  refine (clear_ok (splitAtPred_eq _ _ _ none [] ?_ ⟨rfl, rfl⟩)).trans ?_
  · exact fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)
  convert! unrev_ok using 2; simp [List.reverseAux_eq]

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x ↦ Γ') Λ' (Option Γ')
⊢ x ∈ eval (TM2.step tr) (init c v) ↔ x ∈ halt <$> c.eval v

Tactic:
reaches_eval h₂.to_reflTransGen

Goal state after:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x ↦ Γ') Λ' (Option Γ')
⊢ x ∈ eval (TM2.step tr) i ↔ x ∈ halt <$> c.eval v
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case inj
J : Type v
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun a b ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f ↦ if h : ∃ a, ι a = f then h.choose else default
x : ↑C.pt.toTop
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
a b : α
hh : ι a = ι b
hhh : ι a a = ι b a
⊢ a = b

Tactic:
dsimp [ι] at hhh

Goal state after:
case inj
J : Type v
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun a b ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f ↦ if h : ∃ a, ι a = f then h.choose else default
x : ↑C.pt.toTop
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
a b : α
hh : ι a = ι b
hhh : (if a = a then 0 else 1) = if b = a then 0 else 1
⊢ a = b
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : LightCondSet
S : LightProfiniteᵒᵖ
x : X.obj.obj S
⊢ Continuous fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x

Tactic:
suffices ∀ (i : (T : LightProfinite.{u}) × X.obj.obj ⟨T⟩),
          Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩
        rw [← continuous_sigma_iff]
        apply continuous_coinduced_rng

Goal state after:
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
⊢ ∀ ⦃x : ℕ → ↑X⦄ ⦃p : ↑X⦄,
    Filter.Tendsto x Filter.atTop (nhds p) →
      Filter.Tendsto ((topCatAdjunctionCounitEquiv X).invFun ∘ x) Filter.atTop
        (nhds ((topCatAdjunctionCounitEquiv X).invFun p))

Tactic:
intro f

Goal state after:
X✝ Y : LightCondSet
f✝ : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
f : ℕ → ↑X
⊢ ∀ ⦃p : ↑X⦄,
    Filter.Tendsto f Filter.atTop (nhds p) →
      Filter.Tendsto ((topCatAdjunctionCounitEquiv X).invFun ∘ f) Filter.atTop
        (nhds ((topCatAdjunctionCounitEquiv X).invFun p))
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝² : PreservesFiniteProducts F
X Y : Profinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))
g : X ⟶ Y
x : ↑X.toTop
⊢ (f ∘ ⇑(ConcreteCategory.hom g)) x =
    (ConcreteCategory.hom (isoFinYonedaComponents F X).hom)
      ((ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f)) x

Tactic:
rw [isoFinYonedaComponents_hom_apply]

Goal state after:
F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝² : PreservesFiniteProducts F
X Y : Profinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))
g : X ⟶ Y
x : ↑X.toTop
⊢ (f ∘ ⇑(ConcreteCategory.hom g)) x =
    (ConcreteCategory.hom (F.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) x).op))
      ((ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f))
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
X : Type u
⊢ Presheaf.IsSheaf (coherentTopology LightProfinite) (lanPresheaf (locallyConstantPresheaf X))

Tactic:
by
    rw [Presheaf.isSheaf_of_iso_iff (lanPresheafNatIso
      fun _ ↦ isColimitLocallyConstantPresheafDiagram _ _)]
    exact (CompHausLike.LocallyConstant.functor.{u, u}
      (hs := fun _ _ _ ↦ ((LightProfinite.effectiveEpi_iff_surjective _).mp)).obj X).property

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
x : ↑X.toTop
⊢ (f ∘ ⇑(ConcreteCategory.hom g)) x =
    (ConcreteCategory.hom (isoFinYonedaComponents F X).hom)
      ((ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f)) x

Tactic:
rw [isoFinYonedaComponents_hom_apply]

Goal state after:
F : LightProfiniteᵒᵖ ⥤ Type u
inst✝² : PreservesFiniteProducts F
X Y : LightProfinite
inst✝¹ : Finite ↑X.toTop
inst✝ : Finite ↑Y.toTop
f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
g : X ⟶ Y
x : ↑X.toTop
⊢ (f ∘ ⇑(ConcreteCategory.hom g)) x =
    (ConcreteCategory.hom (F.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) x).op))
      ((ConcreteCategory.hom (F.map g.op)) ((ConcreteCategory.hom (isoFinYonedaComponents F Y).inv) f))
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B P : LightCondMod R
S : LightProfinite
e : A ⟶ B
x : ↑((P ⟹ A).obj.obj (Opposite.op S))
⊢ (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S))) x =
    (ihomPoints R P B S).symm ((ihomPoints R P A S) x ≫ e)

Tactic:
apply (ihomPoints R P B S).injective

Goal state after:
R : Type u
inst✝ : CommRing R
A B P : LightCondMod R
S : LightProfinite
e : A ⟶ B
x : ↑((P ⟹ A).obj.obj (Opposite.op S))
⊢ (ihomPoints R P B S) ((ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S))) x) =
    (ihomPoints R P B S) ((ihomPoints R P B S).symm ((ihomPoints R P A S) x ≫ e))
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
n : ℕ
k : Y ⟶ lightToProfinite.obj (S.component n)
h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)
⊢ g ≫ lightToProfinite.map (S.proj n) =
    g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)

Tactic:
← Functor.map_comp,

Goal state after:
S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
n : ℕ
k : Y ⟶ lightToProfinite.obj (S.component n)
h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)
⊢ g ≫ lightToProfinite.map (S.proj n) = g ≫ lightToProfinite.map (S.proj (n + 1) ≫ S.transitionMap n)
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondSet
A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj S.toCondensed ⊗ (free R).obj P ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : (free R).obj (S'.toCondensed ⊗ P) ⟶ A
hh : (free R).map (lightProfiniteToLightCondSet.map π ▷ P) ≫ (μIso (free R) S.toCondensed P).inv ≫ g = g' ≫ e
⊢ (lightProfiniteToLightCondSet ⋙ free R).map π ▷ (free R).obj P ≫ g =
    (((μIso (free R) S'.toCondensed P).hom ≫ (free R).map (lightProfiniteToLightCondSet.map π ▷ P)) ≫
        (μIso (free R) S.toCondensed P).inv) ≫
      g

Tactic:
simp only [comp_obj, Functor.comp_map, μIso_hom, ← μ_natural_left, μIso_inv, assoc, μ_δ,
      comp_id]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ approx (⇑f) 0 ≤ approx (⇑f) (Nat.succ 0)

Tactic:
dsimp [approx]; apply @bot_le _ _ _ (f ⊥)

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
x : m α
f : α → m β
⊢ monadLift (x >>= f) = monadLift x >>= monadLift ∘ f

Tactic:
by
  ext
  simp only [bind_assoc, run_bind, run_monadLift, Function.comp_apply]

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
s : α → Prop
h : ∃ a, (fun x ↦ a = x) = s
⊢ (fun b ↦ out ⟨s, h⟩ = b) = s

Tactic:
exact Classical.choose_spec h

Goal state after:
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ blur s q = q.blur' h

Tactic:
unfold blur; congr; exact Set.union_eq_self_of_subset_right h

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

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ ↦ toLex (f ∘ ⇑σ)
σ : Fin n ≃ Fin n
hσ : f ∘ ⇑σ ≠ f ∘ ⇑(sort f)
hfσ : P (f ∘ ⇑σ)
i j : Fin n
hij₁ : i < j
hij₂ : (f ∘ ⇑σ) j < (f ∘ ⇑σ) i
⊢ ∃ c < σ, P (f ∘ ⇑c)

Tactic:
exact ⟨σ * Equiv.swap i j, Pi.lex_desc hij₁.le hij₂, h σ i j hij₁ hij₂ hfσ⟩

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

Goal state before:
pp: case succ.last
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
a✝ : ∀ (h : m < n) (i : Fin m.succ), take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
⊢ take (m + 1).succ h v (last (m + 1)) = snoc (take (m + 1) ⋯ v) (v ⟨m + 1, h⟩) (last (m + 1))

Tactic:
| last =>

Goal state after:
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
| recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) α =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
lhs

Goal state after:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
| recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) α
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : AList β
h : ¬c.fst ∈ l
⊢ insertRec H0 IH (insert c.fst c.snd l) = IH c.fst c.snd l h (insertRec H0 IH l)

Tactic:
obtain ⟨l, hl⟩ := l
  suffices @insertRec α β _ C H0 IH ⟨c :: l, nodupKeys_cons.2 ⟨h, hl⟩⟩ ≍
      IH c.1 c.2 ⟨l, hl⟩ h (@insertRec α β _ C H0 IH ⟨l, hl⟩) by
    cases c
    apply eq_of_heq
    convert! this <;> rw [insert_of_notMem h]
  rw [insertRec]
  apply cast_heq

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ AList.lookup a { entries := [⟨a, b⟩], nodupKeys := ⋯ } = some b

Tactic:
AList.lookup,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ dlookup a { entries := [⟨a, b⟩], nodupKeys := ⋯ }.entries = some b
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∈ s₁
⊢ lookup x s₁ = lookup x s₂

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
⊢ lookup x s₁ = lookup x s₂

Tactic:
· rwa [lookup_union_left hs₁, lookup_union_left_of_not_in (h _ hs₁)] at this

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
⊢ lookup x s₁ = lookup x s₂
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ ∀ ⦃i : Finset ι⦄, i ∈ (map Finsupp.support tl).toFinset → _root_.Disjoint hd.support (id i)

Tactic:
intro f

Goal state after:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
f : Finset ι
⊢ f ∈ (map Finsupp.support tl).toFinset → _root_.Disjoint hd.support (id f)
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
⊢ Injective embSigma

Tactic:
intro f

Goal state after:
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f : ι k →₀ M
⊢ ∀ ⦃a₂ : ι k →₀ M⦄, f.embSigma = a₂.embSigma → f = a₂
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
⊢ ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid

Tactic:
let := Classical.decEq β

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mpr
a b r v x : ℕ
h : (↑a ≤ ↑x ∧ ↑x < ↑b) ∧ ↑x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = ↑x

Tactic:
exact ⟨x, by simp_all [natCast_modEq_iff]⟩

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

Goal state before:
pp: case mpr
a b r v x : ℕ
h : (↑a < ↑x ∧ ↑x ≤ ↑b) ∧ ↑x ≡ ↑v [ZMOD ↑r]
⊢ ∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = ↑x

Tactic:
exact ⟨x, by simp_all [natCast_modEq_iff]⟩

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬p ((rdropWhile p l).getLast hl) = true

Tactic:
simp_rw [rdropWhile]

Goal state after:
α : Type u_1
p : α → Bool
l : List α
hl : rdropWhile p l ≠ []
⊢ ¬p ((dropWhile p l.reverse).reverse.getLast ⋯) = true
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p (dropWhile p l) = dropWhile p l

Tactic:
simp only [dropWhile_eq_self_iff]

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ ∀ (hl : 0 < (dropWhile p l).length), ¬p (dropWhile p l)[0] = true
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
⊢ rtakeWhile p [] = []

Tactic:
simp [rtakeWhile]

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

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p [] = [] ↔ ∀ (hl : [] ≠ []), ¬p ([].getLast hl) = true

Tactic:
simp [rtakeWhile]

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

Goal state before:
pp: case append_singleton
α : Type u_1
p : α → Bool
l l✝ : List α
a✝¹ : α
a✝ : rtakeWhile p l✝ = [] ↔ ∀ (hl : l✝ ≠ []), ¬p (l✝.getLast hl) = true
⊢ rtakeWhile p (l✝ ++ [a✝¹]) = [] ↔ ∀ (hl : l✝ ++ [a✝¹] ≠ []), ¬p ((l✝ ++ [a✝¹]).getLast hl) = true

Tactic:
simp [rtakeWhile]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : List α
len_eq : s.length = t.length
h_lex : Lex r s t
⊢ Shortlex r s t

Tactic:
apply Prod.lex_def.mpr
  right
  exact ⟨len_eq, h_lex⟩

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

Goal state before:
pp: α : 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
⊢ take head l ++ drop head l = l

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

Goal state after:
α : 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 = l

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
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 IH

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

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ (v ++ w)[j + u.length + p - u.length]? = v[j + p]?

pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ u.length ≤ j + u.length + p

Tactic:
· rw [getElem?_append_left]
      · exact congrArg (getElem? v) eq
      · lia

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ u.length ≤ j + u.length + p