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

Goal state before:
pp: f g : Code
k : Cont'
⊢ codeSupp (f.case g) k = trStmts₁ (trNormal (f.case g) k) ∪ (codeSupp f k ∪ codeSupp g k)

Tactic:
by

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

Goal state before:
pp: f : Code
k : Cont'
⊢ codeSupp f.fix k = trStmts₁ (trNormal f.fix k) ∪ codeSupp f (Cont'.fix f k)

Tactic:
by

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

Goal state before:
pp: fs : Code
k : Cont'
⊢ contSupp (Cont'.cons₁ fs k) =
    trStmts₁
        (move₂ (fun x ↦ false) main aux
          (move₂ (fun s ↦ decide (s = Γ'.consₗ)) stack main (move₂ (fun x ↦ false) aux stack (trNormal fs k.cons₂)))) ∪
      codeSupp fs k.cons₂

Tactic:
by

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

Goal state before:
pp: f : Code
k : Cont'
⊢ contSupp (Cont'.fix f k) = codeSupp f (Cont'.fix f k)

Tactic:
by

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

Goal state before:
pp: K S : Finset Λ'
q : Λ'
⊢ Supports (insert q K) S ↔ TM2.SupportsStmt S (tr q) ∧ Supports K S

Tactic:
by

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

Goal state before:
pp: S : Finset Λ'
q : Λ'
⊢ Supports {q} S ↔ TM2.SupportsStmt S (tr q)

Tactic:
by

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

Goal state before:
pp: K₁ K₂ S : Finset Λ'
⊢ Supports (K₁ ∪ K₂) S ↔ Supports K₁ S ∧ Supports K₂ S

Tactic:
by

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

Goal state before:
pp: K : Option Γ' → Finset Λ'
S : Finset Λ'
⊢ Supports (Finset.univ.biUnion K) S ↔ ∀ (a : Option Γ'), Supports (K a) S

Tactic:
by

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

Goal state before:
pp: S : Finset Λ'
k : K'
q : Λ'
H : Λ'.Supports S q
x✝ : Option Γ'
⊢ Λ'.Supports S ((fun s ↦ (if s = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) k) (unrev q)) x✝)

Tactic:
by

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

Goal state before:
pp: case halt
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
H₁ : contSupp Cont'.halt ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret Cont'.halt))

Tactic:
| halt =>

Goal state after:
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝¹ : TopologicalSpace X
inst✝ : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
⊢ EqualizerCondition (yonedaPresheaf G X)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X✝ : Type w'
inst✝² : TopologicalSpace X✝
P : TopCat → Prop
X : TopCat
inst✝¹ : CompHausLike.HasExplicitFiniteCoproducts P
inst✝ : CompHausLike.HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ Presheaf.IsSheaf (coherentTopology (CompHausLike P)) (yonedaPresheaf (CompHausLike.compHausLikeToTop P) ↑X)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X✝¹ : Type w'
inst✝² : TopologicalSpace X✝¹
P : TopCat → Prop
X : TopCat
inst✝¹ : CompHausLike.HasExplicitFiniteCoproducts P
inst✝ : CompHausLike.HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
⊢ ∀ ⦃X Y : (CompHausLike P)ᵒᵖ⦄ (f_1 : X ⟶ Y),
    ((TopCat.toSheafCompHausLike P X✝ hs).obj.map f_1 ≫ ↾fun g ↦ (TopCat.Hom.hom f).comp g) =
      (↾fun g ↦ (TopCat.Hom.hom f).comp g) ≫ (TopCat.toSheafCompHausLike P Y✝ hs).obj.map f_1

Tactic:
by

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

Goal state before:
pp: S : Finset Λ'
k : Cont'
H₁ : contSupp k ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret k))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
⊢ ∀ (i : Fiber f),
    Continuous fun a ↦
      match ⟨i, a⟩ with
      | ⟨a, x⟩ => ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
⊢ Injective ⇑(sigmaIsoHom f)

Tactic:
by

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

Goal state before:
pp: case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a ↦ ⋯.some
gg : α → LocallyConstant (↑(F.obj j0).toTop) (Fin 2) :=
  fun a ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant (↑(F.obj j0).toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : ↑C.pt.toTop
⊢ (LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)) x =
    (g a) ((ConcreteCategory.hom (C.π.app j0 ≫ F.map (fs a))) x)

Tactic:
rw [C.w]

Goal state after:
case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a ↦ ⋯.some
gg : α → LocallyConstant (↑(F.obj j0).toTop) (Fin 2) :=
  fun a ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant (↑(F.obj j0).toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : ↑C.pt.toTop
⊢ (LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)) x =
    (g a) ((ConcreteCategory.hom (C.π.app (j a))) x)
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))
x : ↑↑b
⊢ ↑↑x ∈ ↑(Fiber.mk f ↑(Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b))

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
⊢ ∃ j g,
    LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝¹ : TopologicalSpace S
l : LocallyConstant S Y
inst✝ : CompactSpace S
x : Fiber ⇑l
⊢ CompactSpace ↑↑x

Tactic:
by

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

Goal state before:
pp: 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
⊢ ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)

Tactic:
by

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

Goal state before:
pp: 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) α
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toTop
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
by

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

Goal state before:
pp: S : LightProfinite
x✝² x✝¹ : ℕᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((Functor.const ℕᵒᵖ).obj S).map x✝ ≫
      (lightToProfiniteFullyFaithful.preimageIso
            ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).inv ≫
        S.asLimitConeAux.π.app x✝¹ =
    ((lightToProfiniteFullyFaithful.preimageIso
            ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).inv ≫
        S.asLimitConeAux.π.app x✝²) ≫
      S.diagram.map x✝

Tactic:
by

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

Goal state before:
pp: S : LightProfinite
x✝ : ℕᵒᵖ
⊢ S.asLimitConeAux.π.app x✝ =
    (lightToProfiniteFullyFaithful.preimageIso ((Cone.forget (S.diagram ⋙ lightToProfinite)).mapIso S.isoMapCone)).hom ≫
      S.asLimitCone.π.app x✝

Tactic:
by

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

Goal state before:
pp: S : LightProfinite
n : ℕ
⊢ lightToProfinite.map (S.proj n) =
    (lightToProfinite.obj S).asLimitCone.π.app
      ((IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))

Tactic:
by

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

Goal state before:
pp: S : LightProfinite
n : ℕ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (S.proj n))

Tactic:
by

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

Goal state before:
pp: S : LightProfinite
n : ℕ
⊢ ⇑(ConcreteCategory.hom (S.transitionMap n)) ∘ ⇑(ConcreteCategory.hom (S.proj (n + 1))) =
    ⇑(ConcreteCategory.hom (S.proj n))

Tactic:
by

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

Goal state before:
pp: S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ ⇑(ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(ConcreteCategory.hom (S.proj m)) =
    ⇑(ConcreteCategory.hom (S.proj n))

Tactic:
by

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

Goal state before:
pp: S : LightProfinite
n : ℕ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (S.transitionMap n))

Tactic:
by

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

Goal state before:
pp: S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ Function.Surjective ⇑(ConcreteCategory.hom (S.transitionMapLE h))

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
by

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

Goal state before:
pp: S : Finset Λ'
q : Λ'
H₁ : Λ'.Supports S q
HS₁ : trStmts₁ q ⊆ S
⊢ Supports (trStmts₁ q) S

Tactic:
by

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

Goal state before:
pp: S : Finset Λ'
q : Λ'
K : Finset Λ'
H₁ : Λ'.Supports S q
H₂ : trStmts₁ q ∪ K ⊆ S
H₃ : K ⊆ S → Supports K S
⊢ Supports (trStmts₁ q ∪ K) S

Tactic:
by

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ (functor c).Initial

Tactic:
by

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ (functorOp c).Final

Tactic:
by

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

Goal state before:
pp: S : Finset Λ'
c : Code
k : Cont'
Hk : codeSupp c k ⊆ S
⊢ Λ'.Supports S (trNormal c k)

Tactic:
by

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
C : Type u_1
inst✝ : Category.{v_1, u_1} C
G : LightProfinite ⥤ C
S : LightProfinite
x✝¹ x✝ : StructuredArrow S toLightProfinite
f : x✝¹ ⟶ x✝
⊢ ((const (StructuredArrow S toLightProfinite)).obj (G.obj S)).map f ≫ G.map x✝.hom =
    G.map x✝¹.hom ≫ (StructuredArrow.proj S toLightProfinite ⋙ toLightProfinite ⋙ G).map f

Tactic:
by

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

Goal state before:
pp: I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g

Tactic:
by

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
C : Type u_1
inst✝ : Category.{v_1, u_1} C
G : LightProfiniteᵒᵖ ⥤ C
S : LightProfinite
x✝¹ x✝ : CostructuredArrow toLightProfinite.op (Opposite.op S)
f : x✝¹ ⟶ x✝
⊢ (CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ G).map f ≫ G.map x✝.hom =
    G.map x✝¹.hom ≫ ((const (CostructuredArrow toLightProfinite.op (Opposite.op S))).obj (G.obj (Opposite.op S))).map f

Tactic:
by

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

Goal state before:
pp: I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
⊢ (functor c).Initial

Tactic:
by

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

Goal state before:
pp: I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
⊢ (functorOp c).Final

Tactic:
by

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

Goal state before:
pp: I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
C : Type u_1
inst✝ : Category.{v_1, u_1} C
G : Profinite ⥤ C
S : Profinite
x✝¹ x✝ : StructuredArrow S toProfinite
f : x✝¹ ⟶ x✝
⊢ ((const (StructuredArrow S toProfinite)).obj (G.obj S)).map f ≫ G.map x✝.hom =
    G.map x✝¹.hom ≫ (StructuredArrow.proj S toProfinite ⋙ toProfinite ⋙ G).map f

Tactic:
by

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

Goal state before:
pp: I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
C : Type u_1
inst✝ : Category.{v_1, u_1} C
G : Profiniteᵒᵖ ⥤ C
S : Profinite
x✝¹ x✝ : CostructuredArrow toProfinite.op (Opposite.op S)
f : x✝¹ ⟶ x✝
⊢ (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ G).map f ≫ G.map x✝.hom =
    G.map x✝¹.hom ≫ ((const (CostructuredArrow toProfinite.op (Opposite.op S))).obj (G.obj (Opposite.op S))).map f

Tactic:
by

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)
Q : CompHausLike P
Z : Type (max u w)
r : LocallyConstant (↑Q.toTop) Z
a : Fiber ⇑r
inst✝ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
⊢ ((X.mapIso (sigmaIso r).op).hom ≫ (sigmaComparison X fun a ↦ ↑(fiber r a).toTop) ≫ ↾fun g ↦ g a) =
    X.map (sigmaIncl r a).op

Tactic:
by

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

Goal state before:
pp: S : Finset Λ'
c : Code
k : Cont'
H : codeSupp c k ⊆ S
⊢ Supports (codeSupp' c k) S

Tactic:
by

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

Goal state before:
pp: case halt
S : Finset Λ'
H : contSupp Cont'.halt ⊆ S
⊢ Supports (contSupp Cont'.halt) S

Tactic:
| halt =>

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})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
h :
  ∀ (a : Fiber ⇑f),
    (ConcreteCategory.hom (X.map (sigmaIncl f a).op)) x = (ConcreteCategory.hom (X.map (sigmaIncl f a).op)) y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: S : Finset Λ'
k : Cont'
H : contSupp k ⊆ S
⊢ Supports (contSupp k) S

Tactic:
by

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})))
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:
by

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
a : Fiber ⇑(comap (TopCat.Hom.hom g.hom) f)
x : ↑(fiber (comap (TopCat.Hom.hom g.hom) f) a).toTop
⊢ (ConcreteCategory.hom g) ↑x ∈
    ↑(Fiber.mk (⇑f) ((ConcreteCategory.hom g) (preimage (⇑(comap (TopCat.Hom.hom g.hom) f)) a)))

Tactic:
by

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
a : Fiber ⇑(comap (TopCat.Hom.hom g.hom) f)
⊢ Continuous fun x ↦ ⟨(ConcreteCategory.hom g) ↑x, ⋯⟩

Tactic:
by

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
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
⊢ ∀ ⦃X Y_1 : (CompHausLike P)ᵒᵖ⦄ (f : X ⟶ Y_1),
    ((functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).map f ≫
        match Y_1 with
        | op S => counitAppApp S Y) =
      (match X with
        | op S => counitAppApp S Y) ≫
        Y.map f

Tactic:
by

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)
X : Type (max u w)
⊢ Presheaf.IsSheaf (coherentTopology (CompHausLike P)) (functorToPresheaves.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
α : Type u_3
R✝ : Type u_4
R : Type u_5
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
⊢ ∀ (r : R) (x : LocallyConstant X Y),
    (constRingHom.comp (algebraMap R Y)) r * x = x * (constRingHom.comp (algebraMap R Y)) r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
α : Type u_3
R✝ : Type u_4
R : Type u_5
inst✝² : CommSemiring R
inst✝¹ : Semiring Y
inst✝ : Algebra R Y
⊢ ∀ (r : R) (x : LocallyConstant X Y), r • x = (constRingHom.comp (algebraMap R Y)) r * x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
α : Type u_3
R✝ : Type u_4
R : Type u_5
Z : Type u_6
inst✝¹ : MulOneClass Y
inst✝ : MulOneClass Z
f : Y →* Z
⊢ map (⇑f) 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
α : Type u_3
R✝ : Type u_4
R : Type u_5
Z : Type u_6
inst✝¹ : MulOneClass Y
inst✝ : MulOneClass Z
f : Y →* Z
⊢ ∀ (x y : LocallyConstant X Y), map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
α : Type u_3
R✝¹ : Type u_4
R✝ : Type u_5
Z : Type u_6
R : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : AddCommMonoid Z
inst✝ : Module R Z
f : Y →ₗ[R] Z
⊢ ∀ (x y : LocallyConstant X Y), map (⇑f) (x + y) = map (⇑f) x + map (⇑f) y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
α : Type u_3
R✝¹ : Type u_4
R✝ : Type u_5
Z : Type u_6
R : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : AddCommMonoid Z
inst✝ : Module R Z
f : Y →ₗ[R] Z
⊢ ∀ (m : R) (x : LocallyConstant X Y), map (⇑f) (m • x) = (RingHom.id R) m • map (⇑f) x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Algebra

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
α : Type u_3
R✝¹ : Type u_4
R✝ : Type u_5
Z : Type u_6
R : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring Y
inst✝² : Algebra R Y
inst✝¹ : Semiring Z
inst✝ : Algebra R Z
f : Y →ₐ[R] Z
x✝ : R
⊢ (↑↑(mapRingHom ↑f)).toFun ((algebraMap R (LocallyConstant X Y)) x✝) = (algebraMap R (LocallyConstant X Z)) x✝

Tactic:
by

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

Goal state before:
pp: X : CondensedSet
h : (S : Profinite) → IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op)
⊢ LocallyConstant.functor.essImage X

Tactic:
by

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

Goal state before:
pp: X : CondensedSet
⊢ [Condensed.IsDiscrete X, IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X),
      (discrete (Type (u + 1))).essImage X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op))].TFAE

Tactic:
by

Goal state after: