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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Profinite
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj
              { toTop := (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop, is_compact := ⋯, is_hausdorff := ⋯,
                prop := ⋯ }).map
          f ≫
        InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app Y).hom =
      InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app X).hom ≫ F.map f

Tactic:
intro j k f
      ext ⟨g, p⟩
      exact (p f).symm

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
H :
  ((ConcreteCategory.hom h) y).down =
    ({ toFun := ULift.up ∘ fun x ↦ if x ∈ V then 0 else 1, continuous_toFun := ⋯ } y).down
⊢ False

Tactic:
rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H

Goal state after:
case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
H : ((ConcreteCategory.hom h).toFun y).down = { down := 0 }.down
⊢ False
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.cons.false.refl
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := (fst✝¹, fst✝, snd✝).2.1, stk := update S k (fst✝¹, fst✝, snd✝).2.2 }
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some (Λ'.clear p k q), var := some a, stk := update S k Sk }
    { l := some q, var := fst✝, stk := update S k snd✝ }

Tactic:
convert! @IH _ (update S k Sk) _ using 2

Goal state after:
case e'_2
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := (fst✝¹, fst✝, snd✝).2.1, stk := update S k (fst✝¹, fst✝, snd✝).2.2 }
⊢ update S k snd✝ = update (update S k Sk) k (fst✝¹, fst✝, snd✝).2.2

case cons.cons.false.refl.convert_2
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.clear p k q), var := s, stk := S }
        { l := some q, var := (fst✝¹, fst✝, snd✝).2.1, stk := update S k (fst✝¹, fst✝, snd✝).2.2 }
⊢ splitAtPred p (update S k Sk k) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2)
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj
              { toTop := (CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop, is_compact := ⋯,
                is_hausdorff := ⋯, prop := ⋯ }).map
          f ≫
        ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app Y).hom) =
      ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app X).hom) ≫
        F.map f

Tactic:
intro j k f
      ext ⟨g, p⟩
      exact (p f).symm

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: case mp
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : LightProfinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
H :
  ((ConcreteCategory.hom h) y).down =
    ({ toFun := ULift.up ∘ fun x ↦ if x ∈ V then 0 else 1, continuous_toFun := ⋯ } y).down
⊢ False

Tactic:
rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H

Goal state after:
case mp
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : LightProfinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
H : ((ConcreteCategory.hom h).toFun y).down = { down := 0 }.down
⊢ False
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case refine_2
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ c.eval v
this : v' ∈ c.eval v → ∃ b₂, TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step tr) i
⊢ halt v' ∈ eval (TM2.step tr) i

Tactic:
obtain ⟨_, ⟨⟩, h⟩ := this hv

Goal state after:
case refine_2
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ c.eval v
this : v' ∈ c.eval v → ∃ b₂, TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step tr) i
h : halt v' ∈ eval (TM2.step tr) i
⊢ halt v' ∈ eval (TM2.step tr) i
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case comp.refine_1
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.comp g) k ⊆ S
H'✝ : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k) ⊆ S
⊢ codeSupp f k ⊆ S

pp: case comp.refine_2
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.comp g) k ⊆ S
H'✝ : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k) ⊆ S
x✝ : codeSupp' f k ⊆ S
⊢ Supports (codeSupp' f k) S

Tactic:
· simp only [codeSupp', codeSupp, Finset.union_subset_iff] at h H ⊢
      exact ⟨h.2.2, H.2⟩

Goal state after:
case comp.refine_2
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.comp g) k ⊆ S
H'✝ : trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
H' : codeSupp g (Cont'.comp f k) ⊆ S
h : codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ codeSupp' f k) ⊆ S
x✝ : codeSupp' f k ⊆ S
⊢ Supports (codeSupp' f k) S
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : TopCat
⊢ Function.Surjective ⇑(ConcreteCategory.hom (topCatAdjunction.counit.app X))

Tactic:
exact (topCatAdjunctionCounit_bijective _).2

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

Goal state before:
pp: X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
⊢ ∀ (j : CostructuredArrow toProfinite.op S),
    colimit.ι
          (CostructuredArrow.proj toProfinite.op S ⋙
            toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
          j ≫
        ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
          S =
      colimit.ι
          (CostructuredArrow.proj toProfinite.op S ⋙
            toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
          j ≫
        ((lanPresheafNatIso fun x ↦
                  isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) x).hom ≫
              counitApp X).app
          S

Tactic:
intro ⟨Y, _, g⟩

Goal state after:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
⊢ colimit.ι
        (CostructuredArrow.proj toProfinite.op S ⋙
          toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
        S =
    colimit.ι
        (CostructuredArrow.proj toProfinite.op S ⋙
          toProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafNatIso fun x ↦
                isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) x).hom ≫
            counitApp X).app
        S
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
⊢ ∀ (j : CostructuredArrow toLightProfinite.op S),
    colimit.ι
          (CostructuredArrow.proj toLightProfinite.op S ⋙
            toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
          j ≫
        ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
          S =
      colimit.ι
          (CostructuredArrow.proj toLightProfinite.op S ⋙
            toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
          j ≫
        ((lanPresheafNatIso fun x ↦
                  isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))
                    x).hom ≫
              counitApp X).app
          S

Tactic:
intro ⟨Y, _, g⟩

Goal state after:
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✝
⊢ colimit.ι
        (CostructuredArrow.proj toLightProfinite.op S ⋙
          toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
        S =
    colimit.ι
        (CostructuredArrow.proj toLightProfinite.op S ⋙
          toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        { left := Y, right := right✝, hom := g } ≫
      ((lanPresheafNatIso fun x ↦
                isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x).hom ≫
            counitApp X).app
        S
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X✝ : CondensedSet
X : TopCat
⊢ Function.Surjective ⇑(ConcreteCategory.hom (topCatAdjunction.counit.app X))

Tactic:
exact (topCatAdjunctionCounit_bijective _).2

Goal state after:
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X : CondensedSet
⊢ IsIso compactlyGeneratedAdjunction.counit

Tactic:
by
  rw [NatTrans.isIso_iff_isIso_app]
  intro X
  exact inferInstanceAs (IsIso (compactlyGeneratedAdjunctionCounitIso X).hom)

Goal state after:
Module: Mathlib.Control.Fix

Goal state before:
pp: α : 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
this : p (Nat.find h')
⊢ Part.fix f x = Fix.approx f (Nat.find h').succ x

Tactic:
generalize hk : Nat.find h' = k

Goal state after:
α : 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
this : p (Nat.find h')
k : ℕ
hk : Nat.find h' = k
⊢ Part.fix f x = Fix.approx f k.succ x
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i ↦ Subtype.val) <$$> u✝ = x ↔ ((fun i ↦ Subtype.val) ⊚ f P n α) <$$> u✝ = x

Tactic:
dsimp +unfoldPartialApp [(· ⊚ ·)]

Goal state after:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i ↦ Subtype.val) <$$> u✝ = x ↔ (fun i x ↦ ↑(f P n α i x)) <$$> u✝ = x
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α : Type w
x y : ContT r m α
h : ∀ (f : α → m r), x.run f = y.run f
⊢ x = y

Tactic:
by
  unfold ContT; ext; apply h

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

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : ExceptT ε m α) (next : Label ω (ExceptT ε m) γ → α → ExceptT ε m ω),
    (callCC fun f ↦ cmd >>= next f) = do
      let x ← cmd
      callCC fun f ↦ next f x

Tactic:
by
    intros; simp only [callCC, ExceptT.callCC, ExceptT.run_bind, callCC_bind_right]; ext
    dsimp
    congr with ⟨⟩ <;> simp [@callCC_dummy m _]

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
i : ℕ
⊢ { toFun := approx ⇑f, monotone' := ⋯ } i ≤ X

Tactic:
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.Data.ENat.BigOperators

Goal state before:
pp: case singleton
α : Type u_1
s : Finset α
f g : α → ℕ∞
a✝ : α
Hlt : ∀ i ∈ {a✝}, f i < g i
⊢ ∑ i ∈ {a✝}, f i < ∑ i ∈ {a✝}, g i

Tactic:
simp [Hlt _ (mem_singleton_self _)]

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

Goal state before:
pp: C : FloatCfg
e : ℤ
m : ℕ
v : ValidFinite e m
m' : ℕ := m.succ
ss : m'.size = m.size
⊢ ValidFinite e m'

Tactic:
unfold ValidFinite at *

Goal state after:
C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m.size - ↑prec) emin
m' : ℕ := m.succ
ss : m'.size = m.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.size - ↑prec) emin
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
e : ℤ
m' : ℕ
v : ValidFinite e m'.succ
ss : m'.size = m'.succ.size
⊢ ValidFinite e m'

Tactic:
unfold ValidFinite at *

Goal state after:
C : FloatCfg
e : ℤ
m' : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.succ.size - ↑prec) emin
ss : m'.size = m'.succ.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.size - ↑prec) emin
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j

Tactic:
rw [eq_one_of_ne_zero i hi] at hij ⊢
        by_cases hj : j = 0
        · simp [hj] at hij; exact False.elim (h hij.symm)
        · rw [eq_one_of_ne_zero j hj]

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

Goal state before:
pp: α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ map id (lookmap f l) = l

Tactic:
lookmap_map_eq,

Goal state after:
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ map id l = l

case h
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ ∀ (a b : α), b ∈ f a → id a = id b
Module: Mathlib.Data.List.Lookmap

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

Tactic:
rw [← map_id (l.lookmap f), lookmap_map_eq, map_id]

Goal state after:
case h
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ ∀ (a b : α), b ∈ f a → id a = id b
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)
⊢ insertRec H0 IH ∅ = H0

Tactic:
by
  change @insertRec α β _ C H0 IH ⟨[], _⟩ = H0
  rw [insertRec]

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h✝ : ¬a' = x.fst
h' : ¬a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

Tactic:
simp [kerase_cons_ne, *]

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : f a = 0
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
suffices f.toAList.lookup a = none by simp [h, this]
      simp [lookup_eq_none, h]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∑ x_1 ∈ (Finset.range d).attach, (unitVec d ↑x_1 ⊗ x.slice ↑x_1 ⋯).slice i hid = x.slice i hid

Tactic:
simp only [slice_unitVec_mul hid]

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (∑ x_1 ∈ (Finset.range d).attach, if i = ↑x_1 then x.slice ↑x_1 ⋯ else 0) = x.slice i hid
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: n : ℕ
⊢ (negOfNat n).bodd = n.bodd

Tactic:
cases n <;> simp +decide

Goal state after:
case succ
n✝ : ℕ
⊢ (negOfNat (n✝ + 1)).bodd = !n✝.bodd
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ bit b ↑n = ↑(Nat.bit b n)

Tactic:
by
  rw [bit_val, Nat.bit_val]
  cases b <;> rfl

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

Goal state before:
pp: b : Bool
n : ℕ
⊢ bit b -[n+1] = -[Nat.bit (!b) n+1]

Tactic:
by
  rw [bit_val, Nat.bit_val]
  cases b <;> rfl

Goal state after:
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:
← Nat.cast_le (α := ℤ),

Goal state after:
a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ ↑(↑a - ↑b).natAbs ≤ ↑n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
m n : ℤ
k : ℕ
⊢ (bitwise f m n).testBit k = f (m.testBit k) (n.testBit k)

Tactic:
by
  cases m <;> cases n <;> simp only [testBit, bitwise, natBitwise]
  · by_cases h : f false false <;> simp [h]
  · by_cases h : f false true <;> simp [h]
  · by_cases h : f true false <;> simp [h]
  · by_cases h : f true true <;> simp [h]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l ++ rtakeWhile p l = l

Tactic:
simp only [rdropWhile, rtakeWhile]

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ (dropWhile p l.reverse).reverse ++ (takeWhile p l.reverse).reverse = l
Module: Mathlib.Data.List.DropRight

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

Tactic:
rw [← List.reverse_append, takeWhile_append_dropWhile, reverse_reverse]

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

Goal state before:
pp: case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (#[].push head✝) = head✝ :: (tl ++ [f a])

Tactic:
modifyLast.go_concat,

Goal state after:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ (#[].push head✝).toListAppend (modifyLast.go f (tl ++ [a]) #[]) = head✝ :: (tl ++ [f a])
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case neg.inr
α : Type u_1
p i : ℕ
w : List α
per : w.HasPeriod p
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
⊢ w[i % p]? = w[i]?

Tactic:
| inr large =>

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

Goal state before:
pp: case refine_4.refine_1
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
    by_cases z_in : z ∈ Y₂
    · obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
      exact ⟨w, .inl hw, hyz.trans hzw⟩
    · exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ⌊↑x⌋ = ⌊↑x⌋

Tactic:
rw [Int.floor_eq_iff, ← coe_floor]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌊x⌋₊ ≤ ↑x ∧ ↑x < ↑↑⌊x⌋₊ + 1
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
n✝ p : ℕ
hp : IsNilpotent ↑p
inst✝ : Fact (Nat.Prime p)
n : ℕ
ih : n < p → IsUnit ↑n !
h : n + 1 < p
⊢ ¬p ∣ n + 1

Tactic:
exact Nat.not_dvd_of_pos_of_lt (by lia) h

Goal state after: