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

Goal state before:
pp: case push
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : K'
s✝ : Option Γ' → Option Γ'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k✝ s✝ q)
HS₁ : trStmts₁ (Λ'.push k✝ s✝ q) ⊆ S
⊢ Supports (trStmts₁ (Λ'.push k✝ s✝ q)) S

Tactic:
simp [trStmts₁, -Finset.singleton_subset_iff] at HS₁ ⊢

Goal state after:
case push
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : K'
s✝ : Option Γ' → Option Γ'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.push k✝ s✝ q)
HS₁ : insert (Λ'.push k✝ s✝ q) (trStmts₁ q) ⊆ S
⊢ Supports (insert (Λ'.push k✝ s✝ q) (trStmts₁ q)) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case read
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), Λ'.Supports S (q a) → trStmts₁ (q a) ⊆ S → Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : trStmts₁ (Λ'.read q) ⊆ S
⊢ Supports (trStmts₁ (Λ'.read q)) S

Tactic:
simp [trStmts₁, -Finset.singleton_subset_iff] at HS₁ ⊢

Goal state after:
case read
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Option Γ' → Λ'
q_ih : ∀ (a : Option Γ'), Λ'.Supports S (q a) → trStmts₁ (q a) ⊆ S → Supports (trStmts₁ (q a)) S
H₁ : Λ'.Supports S (Λ'.read q)
HS₁ : insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s)) ⊆ S
⊢ Supports (insert (Λ'.read q) (Finset.univ.biUnion fun s ↦ trStmts₁ (q s))) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : trStmts₁ q.succ ⊆ S
⊢ Supports (trStmts₁ q.succ) S

Tactic:
simp [trStmts₁, -Finset.singleton_subset_iff] at HS₁ ⊢

Goal state after:
case succ
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : Λ'.Supports S q₁ → trStmts₁ q₁ ⊆ S → Supports (trStmts₁ q₁) S
q₂_ih : Λ'.Supports S q₂ → trStmts₁ q₂ ⊆ S → Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : trStmts₁ (q₁.pred q₂) ⊆ S
⊢ Supports (trStmts₁ (q₁.pred q₂)) S

Tactic:
simp [trStmts₁, -Finset.singleton_subset_iff] at HS₁ ⊢

Goal state after:
case pred
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : Λ'.Supports S q₁ → trStmts₁ q₁ ⊆ S → Supports (trStmts₁ q₁) S
q₂_ih : Λ'.Supports S q₂ → trStmts₁ q₂ ⊆ S → Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case ret
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : Cont'
H₁ : Λ'.Supports S (Λ'.ret k✝)
HS₁ : trStmts₁ (Λ'.ret k✝) ⊆ S
⊢ Supports (trStmts₁ (Λ'.ret k✝)) S

Tactic:
simp [trStmts₁, -Finset.singleton_subset_iff] at HS₁ ⊢

Goal state after:
case ret
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : Cont'
H₁ : Λ'.Supports S (Λ'.ret k✝)
HS₁ : {Λ'.ret k✝} ⊆ S
⊢ Supports {Λ'.ret k✝} S
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})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ (ConcreteCategory.hom (Y.map (sigmaIncl f a).op)) ((ConcreteCategory.hom (counitAppApp S Y)) f) =
    counitAppAppImage f a

Tactic:
← sigmaComparison_comp_sigmaIso,

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})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ (ConcreteCategory.hom
        ((Y.mapIso (sigmaIso f).op).hom ≫ (sigmaComparison Y fun a ↦ ↑(fiber f a).toTop) ≫ ↾fun g ↦ g a))
      ((ConcreteCategory.hom (counitAppApp S Y)) f) =
    counitAppAppImage f a
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)
⊢ counitAppAppImage (comap (TopCat.Hom.hom g.unop.hom) f) a =
    (ConcreteCategory.hom (Y.map (componentHom f g.unop a).op))
      ((ConcreteCategory.hom
          (Y.map
            (sigmaIncl f
                (Fiber.mk (⇑f)
                  ((ConcreteCategory.hom g.unop) (preimage (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a)))).op))
        ((ConcreteCategory.hom (counitAppApp (unop S) Y)) f))

Tactic:
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.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
a : Fiber ⇑(map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f)
⊢ (ConcreteCategory.hom
        (((functor P hs).obj X).obj.map (sigmaIncl (map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f) a).op))
      ((ConcreteCategory.hom ((ObjectProperty.homMk (counitApp ((functor P hs).obj X).obj)).hom.app (op S)))
        (map (fun x ↦ LocallyConstant.const PUnit.{u + 1} x) f)) =
    (ConcreteCategory.hom
        (((functor P hs).obj X).obj.map (sigmaIncl (map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f) a).op))
      f

Tactic:
incl_of_counitAppApp

Goal state after:
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
a : Fiber ⇑(map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f)
⊢ counitAppAppImage (map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f) a =
    (ConcreteCategory.hom
        (((functor P hs).obj X).obj.map (sigmaIncl (map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f) a).op))
      f
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))
x : X.obj.obj (op (of P PUnit.{u + 1}))
this✝ : Preregular (CompHausLike P)
this : PreservesFiniteProducts ((sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))).obj X) :=
  @CompHausLike.LocallyConstant.adjunction._proof_2 P inst✝² inst✝¹ hs X this✝
a : Fiber ⇑((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)
⊢ (ConcreteCategory.hom
        (X.obj.map (sigmaIncl ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a).op))
      ((ConcreteCategory.hom (((counit P hs).app X).hom.app (op (of P PUnit.{u + 1}))))
        ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)) =
    (ConcreteCategory.hom
        (X.obj.map (sigmaIncl ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a).op))
      x

Tactic:
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
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))
x : X.obj.obj (op (of P PUnit.{u + 1}))
this✝ : Preregular (CompHausLike P)
this : PreservesFiniteProducts ((sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))).obj X) :=
  @CompHausLike.LocallyConstant.adjunction._proof_2 P inst✝² inst✝¹ hs X this✝
a : Fiber ⇑((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x)
⊢ counitAppAppImage ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a =
    (ConcreteCategory.hom
        (X.obj.map (sigmaIncl ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a).op))
      x
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: 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)
s : Cocone ((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X)
i : I
f : LocallyConstant (↑(toProfinite.obj (F.obj i)).toTop) X
⊢ (ConcreteCategory.hom
        (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i) ≫
          (isColimitLocallyConstantPresheaf c X hc).desc s))
      f =
    (ConcreteCategory.hom (s.ι.app (Opposite.op i))) f

Tactic:
rw [(isColimitLocallyConstantPresheaf c X hc).fac]

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

Goal state before:
pp: S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts F
X✝ Y✝ : FintypeCatᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (toProfinite.op ⋙ F).map x✝ ≫ (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop Y✝))).hom =
    (isoFinYonedaComponents F (toProfinite.obj (Opposite.unop X✝))).hom ≫ (finYoneda F).map x✝

Tactic:
simp only [comp_obj, op_obj, finYoneda_obj, Functor.comp_map, op_map]
    ext
    simp only [isoFinYonedaComponents_hom, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply,
      ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, toProfinite_obj,
      ← Functor.map_comp_apply]
    rfl

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
s : Cocone ((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X)
n : ℕᵒᵖ
f : LocallyConstant (↑(toLightProfinite.obj (F.obj n)).toTop) X
⊢ (ConcreteCategory.hom
        (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op n) ≫
          (isColimitLocallyConstantPresheaf c X hc).desc s))
      f =
    (ConcreteCategory.hom (s.ι.app (Opposite.op n))) f

Tactic:
rw [(isColimitLocallyConstantPresheaf c X hc).fac]

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

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
X✝ Y✝ : LightProfiniteᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ colimit.desc (CostructuredArrow.proj toLightProfinite.op X✝ ⋙ toLightProfinite.op ⋙ F)
        { pt := colimit (CostructuredArrow.proj toLightProfinite.op Y✝ ⋙ toLightProfinite.op ⋙ F),
          ι :=
            {
              app := fun g ↦
                colimit.ι (CostructuredArrow.proj toLightProfinite.op Y✝ ⋙ toLightProfinite.op ⋙ F)
                  ((CostructuredArrow.map x✝).obj g),
              naturality := ⋯ } } ≫
      colimit.desc (CostructuredArrow.proj toLightProfinite.op Y✝ ⋙ toLightProfinite.op ⋙ F)
        (LightProfinite.Extend.cocone F (Opposite.unop Y✝)) =
    colimit.desc (CostructuredArrow.proj toLightProfinite.op X✝ ⋙ toLightProfinite.op ⋙ F)
        (LightProfinite.Extend.cocone F (Opposite.unop X✝)) ≫
      F.map x✝

Tactic:
exact colimit.hom_ext fun _ ↦ (by simp)

Goal state after:
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
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (LightProfinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (counitAppApp (LightProfinite.of (Opposite.unop Y).obj) X)) f)

Tactic:
incl_of_counitAppApp

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
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (LightProfinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    counitAppAppImage f x
Module: Mathlib.Control.Fix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
⊢ ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f (n + 1).succ x'

Tactic:
intro x' _
    rw [Fix.approx, WellFounded.fix_eq, fixAux]
    congr
    ext : 1
    have hh : ¬(Fix.approx f z.val x).Dom := by
      apply Nat.find_min h'
      lia
    rw [succ_add_eq_add_succ] at _this hk
    rw [assert_pos hh, n_ih (Upto.succ z hh) _this hk]

Goal state after:
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 : Option α
⊢ Option.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) x = Comp.mk (Option.traverse f <$> Option.traverse g x)

Tactic:
by
  cases x <;> (simp [Option.traverse, Option.mapM, functor_norm] <;> rfl)

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
F : Realizer α
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)

Tactic:
by
  have := toTopsp_isTopologicalBasis F.F; rwa [F.eq] at this

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : f.Realizer
x : F.σ
h : f ≠ ⊥
hF : F.F.f x ⊆ ∅
⊢ { a // a ∈ ∅ ∧ 𝓝 a ⊓ f ≠ ⊥ }

Tactic:
suffices f = ⊥ from absurd this h

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : f.Realizer
x : F.σ
h : f ≠ ⊥
hF : F.F.f x ⊆ ∅
⊢ f = ⊥
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: case nil
b : Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) []
⊢ count (!b) [] ≤ count b [] + 1

Tactic:
exact zero_le

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → f i ∈ t i)
⊢ f i ∈ t i

Tactic:
by_cases hi : i ∈ s
    · exact h.2 hi
    · rw [notMem_support_iff.1 (mt h.1 hi), notMem_support_iff.1 (notMem_mono ht hi)]
      exact zero_mem_zero

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

Goal state before:
pp: case neg
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
h' : ¬j = i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j

Tactic:
have : castLE h j ≠ castLE h i := by simp [h']

Goal state after:
case neg
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
h' : ¬j = i
this : castLE h j ≠ castLE h i
⊢ take m h (update v (castLE h i) x) j = update (take m h v) i x j
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
x : ↑T'.toTop
hx : (⇑(ConcreteCategory.hom (snd S' ℕ∪{∞})) ∘ ⇑(ConcreteCategory.hom π')) x = ∞
⊢ x ∈ ⇑(ConcreteCategory.hom (π' ≫ snd S' ℕ∪{∞})) ⁻¹' {∞}

Tactic:
simpa using hx

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u_1
inst✝³ : FinEnum α✝
β : α✝ → Type u_2
inst✝² : (a : α✝) → FinEnum (β a)
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
⊢ ∀ (x : (hp : p) → α hp), x ∈ map (fun x x_1 ↦ x) (FinEnum.toList (α hp))

Tactic:
intro x; simpa using ⟨x hp, rfl⟩

Goal state after:
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) = [] ↔ ∀ (b_1 : β a), ¬⟨a, b_1⟩ ∈ ⟨a', b⟩ :: l

Tactic:
by
    by_cases h : a = a'
    · subst a'
      simp only [lookupAll_cons_eq, mem_cons, Sigma.mk.inj_iff, heq_eq_eq, true_and, not_or,
        false_iff, not_forall, not_and, not_not, reduceCtorEq]
      use b
      simp
    · simp [h, lookupAll_eq_nil]

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a' = a
⊢ ((kextract a l).fst, ⟨a', b⟩ :: (kextract a l).snd) = (dlookup a (⟨a', b⟩ :: l), kerase a (⟨a', b⟩ :: l))

Tactic:
· simp [Ne.symm h, kextract_eq_dlookup_kerase a l, kerase]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
s : Finset α
t : Finset β
⊢ pimage f s ⊆ t ↔ ∀ x ∈ s, ∀ y ∈ f x, y ∈ t

Tactic:
simp [subset_iff, @forall_comm _ β]

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

Goal state before:
pp: case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a l : List (ι →₀ M)
hd : List.Pairwise (Disjoint on Finsupp.support) l
hl : a.Perm l
⊢ List.Pairwise (Disjoint on Finsupp.support) a

Tactic:
exact hl.symm.pairwise hd fun h ↦ _root_.Disjoint.symm h

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✝ : AddGroup N
f g : α →₀ N
⊢ f.neLocus (f - g) = g.support

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ f.neLocus (f + -g) = g.support
Module: Mathlib.Data.Int.Fib.Lemmas

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

Tactic:
sub_eq_add_neg,

Goal state after:
i : ℕ
hn : ¬i + 1 = 0
⊢ fib (-↑i) * fib (-↑(i + 1) + -1) + -fib (-↑(i + 1)) ^ 2 = (-1) ^ (-↑(i + 1)).natAbs
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ (↑a - ↑b).natAbs ≤ n

Tactic:
by
  rw [← Nat.cast_le (α := ℤ), natCast_natAbs]
  exact abs_sub_le_of_nonneg_of_le (natCast_nonneg a) (ofNat_le.mpr a_le_n)
    (natCast_nonneg b) (ofNat_le.mpr b_le_n)

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

Goal state before:
pp: case append_singleton
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n : ℕ
⊢ take ((xs ++ [x]).length - n) (xs ++ [x]) = (drop n (xs ++ [x]).reverse).reverse

Tactic:
cases n
    · simp [take_length_add_append]
    · simp [take_append, IH]

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

Goal state before:
pp: n : ℕ
⊢ Ico 0 n = range n

Tactic:
by rw [Ico, Nat.sub_zero, range_eq_range']

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

Goal state before:
pp: case inl
n m l : ℕ
hml : m ≤ l
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n m

Tactic:
filter_lt_of_top_le hml

Goal state after:
case inl
n m l : ℕ
hml : m ≤ l
⊢ Ico n m = Ico n m
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
⊢ splitBy.loop r (b :: l) a g gs = gs.reverse ++ splitBy.loop r (b :: l) a g []

Tactic:
simp_rw [splitBy.loop]

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
⊢ (match r a b with
    | true => splitBy.loop r l b (a :: g) gs
    | false => splitBy.loop r l b [] ((a :: g).reverse :: gs)) =
    gs.reverse ++
      match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => splitBy.loop r l b [] [(a :: g).reverse]