mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f✝ : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T✝ : CompHausLike P
g✝ : T✝ ⟶ S✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)
⊢ (ConcreteCategory.hom (Y.map (sigmaIncl (comap (TopCat.Hom.hom g.unop.hom) f) a).op))
      ((ConcreteCategory.hom (counitAppApp (unop T) Y)) (comap (TopCat.Hom.hom g.unop.hom) f)) =
    (ConcreteCategory.hom (Y.map (sigmaIncl (comap (TopCat.Hom.hom g.unop.hom) f) a).op))
      ((ConcreteCategory.hom (Y.map g)) ((ConcreteCategory.hom (counitAppApp (unop S) Y)) f))

Tactic:
rw [incl_of_counitAppApp, ← Functor.map_comp_apply, incl_comap,
      Functor.map_comp_apply, incl_of_counitAppApp]

Goal state after:
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f✝ : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T✝ : CompHausLike P
g✝ : T✝ ⟶ S✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)
⊢ counitAppAppImage (comap (TopCat.Hom.hom g.unop.hom) f) a =
    (ConcreteCategory.hom (Y.map (componentHom f g.unop a).op))
      (counitAppAppImage f
        (Fiber.mk (⇑f) ((ConcreteCategory.hom g.unop) (preimage (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a))))
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: X : LightCondSet
h : (S : LightProfinite) → IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ LocallyConstant.functor.essImage X

Tactic:
let i : X.obj ≅ (LightCondSet.LocallyConstant.functor.obj _).obj :=
    LightCondensed.isoLocallyConstantOfIsColimit _ h
  exact ⟨_, ⟨((sheafToPresheaf _ _).preimageIso i.symm)⟩⟩

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

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
⊢ (unit P hs).app
        (((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1}))).obj X) ≫
      ((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1}))).map
        ((counit P hs).app X) =
    𝟙 (((sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj (op (of P PUnit.{u + 1}))).obj X)

Tactic:
by
    ext (x : X.obj.obj _)
    dsimp
    have := CompHausLike.preregular hs
    let : PreservesFiniteProducts ((sheafToPresheaf (coherentTopology _) _).obj X) :=
      inferInstanceAs (PreservesFiniteProducts X.obj)
    apply presheaf_ext ((unit P hs).app _ x)
    intro a
    erw [incl_of_counitAppApp]
    simp only [counitAppAppImage]
    erw [← map_eq_image _ a ⟨PUnit.unit, by simp [mem_iff_eq_image, ← map_preimage_eq_image]⟩]
    rfl

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

Goal state before:
pp: case refine_1
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
f : LocallyConstant (↑c.pt.toTop) X
⊢ ∃ i xi, f = (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi

Tactic:
obtain ⟨j, h⟩ := Profinite.exists_locallyConstant.{_, u} c hc f

Goal state after:
case refine_1
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
f : LocallyConstant (↑c.pt.toTop) X
j : I
h : ∃ g, f = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) g
⊢ ∃ i xi, f = (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝² : X✝ ⟶ Y✝
x✝¹ : F.obj (Opposite.op (toLightProfinite.obj (Opposite.unop X✝)))
x✝ : (Opposite.unop Y✝).obj
⊢ (ConcreteCategory.hom
          (F.map (toLightProfinite.map x✝².unop).op ≫
            (isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop Y✝))).hom)).toFun
      x✝¹ x✝ =
    (ConcreteCategory.hom
          ((isoFinYonedaComponents F (toLightProfinite.obj (Opposite.unop X✝))).hom ≫ (finYoneda F).map x✝²)).toFun
      x✝¹ x✝

Tactic:
simp only [isoFinYonedaComponents_hom, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply,
      ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, toLightProfinite_obj,
      ← Functor.map_comp_apply]

Goal state after:
S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝² : X✝ ⟶ Y✝
x✝¹ : F.obj (Opposite.op (toLightProfinite.obj (Opposite.unop X✝)))
x✝ : (Opposite.unop Y✝).obj
⊢ (ConcreteCategory.hom
        (F.map ((toLightProfinite.map x✝².unop).op ≫ (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) x✝).op)))
      x✝¹ =
    (ConcreteCategory.hom ((finYoneda F).map x✝²))
      (fun x ↦ (ConcreteCategory.hom (F.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) x).op)) x✝¹) x✝
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case e_a
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj
      (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
this : Finite ↑(fiber f x).toTop
y : ↑(fiber f x).toTop
⊢ (ConcreteCategory.hom (isoFinYonedaComponents X (fiber f x)).hom)
      ((ConcreteCategory.hom (X.map (sigmaIncl f x).op))
        ((ConcreteCategory.hom (isoFinYonedaComponents X (LightProfinite.of (Opposite.unop Y).obj)).inv) ⇑f))
      y =
    (ConcreteCategory.hom (isoFinYonedaComponents X (fiber f x)).hom)
      ((ConcreteCategory.hom (X.map (CompHausLike.isTerminalPUnit.from (fiber f x)).op)) (Function.Fiber.image (⇑f) x))
      y

Tactic:
simp only [toLightProfinite_obj, isoFinYonedaComponents_hom, TypeCat.hom_ofHom,
    TypeCat.Fun.coe_mk, ← map_comp_apply, ← op_comp]

Goal state after:
case e_a
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj
      (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
this : Finite ↑(fiber f x).toTop
y : ↑(fiber f x).toTop
⊢ (ConcreteCategory.hom (X.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) y ≫ sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (LightProfinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom
        (X.map
          (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) y ≫ CompHausLike.isTerminalPUnit.from (fiber f x)).op))
      (Function.Fiber.image (⇑f) x)
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x : t α
⊢ sequence (pure <$> x) = pure x

Tactic:
simp [sequence, traverse_map, id_traverse]

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

Goal state before:
pp: α : Type ?u.3
⊢ (fun p ↦ ((Equiv.refl α).symm.trans p).trans (Equiv.refl α)) = id

Tactic:
by ext; simp

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

Goal state before:
pp: α✝ β✝ γ✝ : Type ?u.3
x✝¹ : α✝ ≃ β✝
x✝ : β✝ ≃ γ✝
⊢ (fun p ↦ ((x✝¹.trans x✝).symm.trans p).trans (x✝¹.trans x✝)) =
    (fun p ↦ (x✝.symm.trans p).trans x✝) ∘ fun p ↦ (x✝¹.symm.trans p).trans x✝¹

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type ?u.4
⊢ (fun s ↦ Finset.map (Equiv.refl α).toEmbedding s) = id

Tactic:
by ext; simp

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

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ : Type u
x✝ : WriterT ω M α✝
⊢ id <$> x✝ = x✝

Tactic:
by ext; simp

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

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
x✝¹ : α✝
x✝ : α✝ → WriterT ω M β✝
⊢ pure x✝¹ >>= x✝ = x✝ x✝¹

Tactic:
by ext; simp

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

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
x✝¹ : α✝ → β✝
x✝ : WriterT ω M α✝
⊢ (do
      let y ← x✝
      pure (x✝¹ y)) =
    x✝¹ <$> x✝

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
f : Option α✝
⊢ Option.map (⇑e.symm) (Option.map (⇑e) f) = f

Tactic:
cases f <;> simp

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
f : Option β✝
⊢ Option.map (⇑e) (Option.map (⇑e.symm) f) = f

Tactic:
cases f <;> simp

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)
⊢ ∀ (i : ℕ), (approxChain f) i ≤ Part.fix ⇑f

Tactic:
simp only [Fix.approxChain]

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ∀ (i : ℕ), { toFun := approx ⇑f, monotone' := ⋯ } i ≤ Part.fix ⇑f
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
⊢ ∀ (i : ℕ), (approxChain f) i ≤ X

Tactic:
simp only [Fix.approxChain]

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
⊢ ∀ (i : ℕ), { toFun := approx ⇑f, monotone' := ⋯ } i ≤ X
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case pos
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : (π t).2 = none
⊢ ∃ a, coverToFun (fibreIncl π σ) (π_r π σ) a = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩

Tactic:
exact ⟨Sum.inr ⟨(⟨⟨t, ht⟩, by grind⟩, ⟨⟨t', ht'⟩, by grind⟩), by grind⟩, by grind⟩

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

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
X : LightCondMod R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi ((lightProfiniteToLightCondSet ⋙ free R).map (cover π))
g : (lightProfiniteToLightCondSet ⋙ free R).obj T ⟶ X
r_inf : T ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
σ : S ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
⊢ Cocone
    (parallelPair (lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π))
        (lightProfiniteToLightCondSet.map (CompHausLike.pullback.snd π π)) ⋙
      free R)

Tactic:
refine Cocone.ofCofork (Cofork.ofπ (g -
    (lightProfiniteToLightCondSet ⋙ free R).map
      (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd _ _)) ≫ g +
    (lightProfiniteToLightCondSet ⋙ free R).map
      (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd _ _) ≫ π ≫ fst _ _ ≫ σ ≫
        LightProfinite.fibreIncl ∞ (π ≫ snd _ _)) ≫ g) ?_)

Goal state after:
R : Type
inst✝¹ : CommRing R
X : LightCondMod R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi ((lightProfiniteToLightCondSet ⋙ free R).map (cover π))
g : (lightProfiniteToLightCondSet ⋙ free R).obj T ⟶ X
r_inf : T ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
σ : S ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
⊢ (parallelPair (lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π))
              (lightProfiniteToLightCondSet.map (CompHausLike.pullback.snd π π)) ⋙
            free R).map
        WalkingParallelPairHom.left ≫
      (g - (lightProfiniteToLightCondSet ⋙ free R).map (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫ g +
        (lightProfiniteToLightCondSet ⋙ free R).map
            (r_inf ≫
              LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
          g) =
    (parallelPair (lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π))
              (lightProfiniteToLightCondSet.map (CompHausLike.pullback.snd π π)) ⋙
            free R).map
        WalkingParallelPairHom.right ≫
      (g - (lightProfiniteToLightCondSet ⋙ free R).map (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫ g +
        (lightProfiniteToLightCondSet ⋙ free R).map
            (r_inf ≫
              LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫
                π ≫ fst S ℕ∪{∞} ≫ σ ≫ LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞})) ≫
          g)
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ DFinsupp.toMultiset.comp toDFinsupp = AddMonoidHom.id (Multiset α)

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toDFinsupp.comp DFinsupp.toMultiset = AddMonoidHom.id (Π₀ (x : α), ℕ)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: case empty
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
⊢ ⨅ i, ∑ a ∈ ∅, f i a = ∑ a ∈ ∅, ⨅ i, f i a

Tactic:
simp only [Finset.sum_empty, ciInf_const]

Goal state after:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℕ∞
Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i
⊢ ∃ i ∈ s, f i ≤ g i

Tactic:
contrapose! Hle
  apply sum_lt_sum_of_nonempty hs Hle

Goal state after:
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
⊢ emin ≤ emin + ↑prec - 1

Tactic:
rw [add_sub_assoc]
    apply le_add_of_nonneg_right
    apply sub_nonneg_of_le
    apply Int.ofNat_le_ofNat_of_le
    exact C.precPos

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

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
⊢ take m h (update v (castLE h i) x) = update (take m h v) i x

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
⊢ take m h (update v i x) = take m h v

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
j : Fin m
⊢ take m h (update v i x) j = take m h v j
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: case h_2
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 α
n✝ : ℕ
heq✝ : card α = n✝.succ
⊢ (let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n✝)) ↑↑(finChoice n✝)) inst✝ ⋯
      (option fN (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin n✝))))) =
    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:
· rcases Nat.succ.inj <| (card α).succ_pred_eq_of_pos h |>.trans ‹_› with rfl; rfl

Goal state after:
Module: Mathlib.Data.Finite.Vector

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ Finite (Vector α n)

Tactic:
have := Fintype.ofFinite α
  infer_instance

Goal state after:
Module: Mathlib.Data.Finite.Vector

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ Finite (Sym α n)

Tactic:
have := Fintype.ofFinite α
  infer_instance

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

Goal state before:
pp: case swap.none.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
simpa [h₁, lookmap_cons_some _ _ h₂] using Perm.swap _ _ _

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys
⊢ { entries := c :: l, nodupKeys := h } = insert c.fst c.snd { entries := l, nodupKeys := ⋯ }

Tactic:
by
  simpa [insert] using (kerase_of_notMem_keys <| notMem_keys_of_nodupKeys_cons h).symm

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

Goal state after:
α : 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 : List (Sigma β)
hl : l.NodupKeys
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ insertRec H0 IH (insert c.fst c.snd { entries := l, nodupKeys := hl }) =
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
⊢ insert a b (s₁ ∪ s₂) = insert a b s₁ ∪ s₂

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by
  by_cases hs : s.Nonempty <;> by_cases ht : t.Nonempty
  · exact s.exists_between hs ht H
  · exact let ⟨p, hp⟩ := exists_gt (s.max' hs); ⟨p, by simp_all⟩
  · exact let ⟨p, hp⟩ := exists_lt (t.min' ht); ⟨p, by simp_all⟩
  · exact Nonempty.elim ‹_› fun p ↦ ⟨p, by simp_all⟩

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ kerase a (hd :: tl) = hd :: tl₁ ++ tl₂

Tactic:
by
            simp [e, h₃]

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

Tactic:
by_cases e : a = hd.1
    · subst e
      exact ⟨hd.2, [], tl, by simp, by cases hd; rfl, by simp⟩
    · simp only [keys_cons, mem_cons] at h
      rcases h with h | h
      · exact absurd h e
      rcases ih h with ⟨b, tl₁, tl₂, h₁, h₂, h₃⟩
      exact ⟨b, hd :: tl₁, tl₂, not_mem_cons_of_ne_of_not_mem e h₁, by (rw [h₂]; rfl), by
            simp [e, h₃]⟩

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : DecidableEq M
inst✝¹ : Zero M
inst✝ : Zero N
f g : α →₀ N
F : N → M
F0 : F 0 = 0
hF : Function.Injective F
⊢ (mapRange F F0 f).neLocus (mapRange F F0 g) = f.neLocus g

Tactic:
by
  ext
  simpa only [mem_neLocus] using! hF.ne_iff

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
⊢ CPRankMax 1 x

Tactic:
have h' := CPRankMax.succ 0 x 0 h CPRankMax.zero

Goal state after:
α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
h' : CPRankMax (0 + 1) (x + 0)
⊢ CPRankMax 1 x
Module: Mathlib.Data.Int.NatPrime

Goal state before:
pp: p : ℕ
p_prime : Nat.Prime p
m n : ℤ
k l : ℕ
hpm : ↑(p ^ k) ∣ m
hpn : ↑(p ^ l) ∣ n
hpmn : ↑(p ^ (k + l + 1)) ∣ m * n
hpm' : p ^ k ∣ m.natAbs
hpn' : p ^ l ∣ n.natAbs
hpmn' : p ^ (k + l + 1) ∣ m.natAbs * n.natAbs
hsd : p ^ (k + 1) ∣ m.natAbs ∨ p ^ (l + 1) ∣ n.natAbs :=
  Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul p_prime hpm' hpn' hpmn'
hsd1 : p ^ (k + 1) ∣ m.natAbs
⊢ ↑(p ^ (k + 1)) ∣ m

Tactic:
by apply Int.dvd_natAbs.1; apply Int.natCast_dvd_natCast.2 hsd1

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

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).ldiff (bit b n) = bit (a && !b) (m.ldiff n)

Tactic:
← bitwise_diff,

Goal state after:
a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ bitwise (fun a b ↦ a && !b) (bit a m) (bit b n) = bit (a && !b) (bitwise (fun a b ↦ a && !b) m n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
k : ℕ
⊢ (m.ldiff n).testBit k = (m.testBit k && !n.testBit k)

Tactic:
← bitwise_diff,

Goal state after:
m n : ℤ
k : ℕ
⊢ (bitwise (fun a b ↦ a && !b) m n).testBit k = (m.testBit k && !n.testBit k)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n k : ℕ
⊢ -[m+1] >>> (↑n + ↑k) = -[m+1] >>> ↑n >>> ↑k

Tactic:
by
    rw [shiftRight_negSucc, shiftRight_negSucc, ← Int.natCast_add, shiftRight_negSucc,
      Nat.shiftRight_add]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l = l ↔ ∀ (hl : 0 < l.length), ¬p l[0] = true

Tactic:
by
  rcases l with - | ⟨hd, tl⟩
  · simp
  · rw [dropWhile]
    by_cases h_p_hd : p hd
    · simp only [h_p_hd, length_cons, Nat.zero_lt_succ, getElem_cons_zero, not_true_eq_false,
        imp_false, iff_false]
      intro h
      replace h := congrArg length h
      have := length_dropWhile_le p tl
      simp at h
      lia
    · simp [h_p_hd]

Goal state after: