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

Goal state before:
pp: case h
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑(toCompHaus.obj X).toTop
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
f' : ↑(toCompHaus.obj X).toTop → ↑B.toTop
h : Continuous f' ∧ ⇑(TopCat.Hom.hom f.hom) ∘ f' = ⇑(TopCat.Hom.hom φ.hom)
⊢ ofHom (fun x ↦ True) { toFun := f', continuous_toFun := ⋯ } ≫ f = φ

Tactic:
ext

Goal state after:
case h
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑(toCompHaus.obj X).toTop
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
f' : ↑(toCompHaus.obj X).toTop → ↑B.toTop
h : Continuous f' ∧ ⇑(TopCat.Hom.hom f.hom) ∘ f' = ⇑(TopCat.Hom.hom φ.hom)
a✝ : ↑(toCompHaus.obj X).toTop
⊢ (ConcreteCategory.hom (ofHom (fun x ↦ True) { toFun := f', continuous_toFun := ⋯ } ≫ f)) a✝ =
    (ConcreteCategory.hom φ) a✝
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: case h
X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑(toProfinite.obj X).toTop
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
f' : ↑(toProfinite.obj X).toTop → ↑B.toTop
h : Continuous f' ∧ ⇑(TopCat.Hom.hom f.hom) ∘ f' = ⇑(TopCat.Hom.hom φ.hom)
⊢ ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := f', continuous_toFun := ⋯ } ≫ f = φ

Tactic:
ext

Goal state after:
case h
X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑(toProfinite.obj X).toTop
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
f' : ↑(toProfinite.obj X).toTop → ↑B.toTop
h : Continuous f' ∧ ⇑(TopCat.Hom.hom f.hom) ∘ f' = ⇑(TopCat.Hom.hom φ.hom)
a✝ : ↑(toProfinite.obj X).toTop
⊢ (ConcreteCategory.hom (ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := f', continuous_toFun := ⋯ } ≫ f)) a✝ =
    (ConcreteCategory.hom φ) a✝
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: case h
X B C : Stonean
φ : X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑X.toTop
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
f' : ↑X.toTop → ↑B.toTop
h : Continuous f' ∧ ⇑(TopCat.Hom.hom f.hom) ∘ f' = ⇑(TopCat.Hom.hom φ.hom)
⊢ ofHom (fun X ↦ ExtremallyDisconnected ↑X) { toFun := f', continuous_toFun := ⋯ } ≫ f = φ

Tactic:
ext

Goal state after:
case h
X B C : Stonean
φ : X ⟶ C
f : B ⟶ C
inst✝ : Epi f
this : ExtremallyDisconnected ↑X.toTop
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
f' : ↑X.toTop → ↑B.toTop
h : Continuous f' ∧ ⇑(TopCat.Hom.hom f.hom) ∘ f' = ⇑(TopCat.Hom.hom φ.hom)
a✝ : ↑X.toTop
⊢ (ConcreteCategory.hom (ofHom (fun X ↦ ExtremallyDisconnected ↑X) { toFun := f', continuous_toFun := ⋯ } ≫ f)) a✝ =
    (ConcreteCategory.hom φ) a✝
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
⊢ Projective X ↔ ExtremallyDisconnected ↑X.toTop

Tactic:
constructor

Goal state after:
case mp
X : CompHaus
⊢ Projective X → ExtremallyDisconnected ↑X.toTop

case mpr
X : CompHaus
⊢ ExtremallyDisconnected ↑X.toTop → Projective X
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝ : Set X
⊢ (∃ a, d.proj ⁻¹' {a} = x✝) ↔ ∃ y, x✝ = {x | d.toSetoid x y}

Tactic:
constructor

Goal state after:
case mp
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝ : Set X
⊢ (∃ a, d.proj ⁻¹' {a} = x✝) → ∃ y, x✝ = {x | d.toSetoid x y}

case mpr
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝ : Set X
⊢ (∃ y, x✝ = {x | d.toSetoid x y}) → ∃ a, d.proj ⁻¹' {a} = x✝
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: case mp
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝¹ : Set X
x✝ : ∃ a, d.proj ⁻¹' {a} = x✝¹
y : Quotient d.toSetoid
h : d.proj ⁻¹' {y} = x✝¹
⊢ x✝¹ = {x | d.toSetoid x y.out}

Tactic:
ext

Goal state after:
case mp
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝² : Set X
x✝¹ : ∃ a, d.proj ⁻¹' {a} = x✝²
y : Quotient d.toSetoid
h : d.proj ⁻¹' {y} = x✝²
x✝ : X
⊢ x✝ ∈ x✝² ↔ x✝ ∈ {x | d.toSetoid x y.out}
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝¹ : Set X
x✝ : ∃ y, x✝¹ = {x | d.toSetoid x y}
y : X
h : x✝¹ = {x | d.toSetoid x y}
⊢ d.proj ⁻¹' {d.proj y} = x✝¹

Tactic:
ext

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
d : DiscreteQuotient X
x✝² : Set X
x✝¹ : ∃ y, x✝² = {x | d.toSetoid x y}
y : X
h : x✝² = {x | d.toSetoid x y}
x✝ : X
⊢ x✝ ∈ d.proj ⁻¹' {d.proj y} ↔ x✝ ∈ x✝²
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_3
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
⊢ U0 ∈ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V} ↔
    U0 ∈ {S | ∃ U F_1, (∀ i ∈ F_1, U i ∈ T i) ∧ S = ⋂ i ∈ F_1, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i}

Tactic:
constructor

Goal state after:
case e'_3.mp
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
⊢ U0 ∈ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V} →
    U0 ∈ {S | ∃ U F_1, (∀ i ∈ F_1, U i ∈ T i) ∧ S = ⋂ i ∈ F_1, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i}

case e'_3.mpr
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
⊢ U0 ∈ {S | ∃ U F_1, (∀ i ∈ F_1, U i ∈ T i) ∧ S = ⋂ i ∈ F_1, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i} →
    U0 ∈ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V}
Module: Mathlib.Condensed.Light.Basic

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

Tactic:
ext

Goal state after:
C : Type w
inst✝ : Category.{v, w} C
X Y : LightCondensed C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S
x✝ : LightProfiniteᵒᵖ
⊢ f.hom.app x✝ = g.hom.app x✝
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
⊢ TotallyDisconnectedSpace ↑(CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop ∧
    SecondCountableTopology ↑(CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop

Tactic:
constructor

Goal state after:
case left
J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
⊢ TotallyDisconnectedSpace ↑(CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop

case right
J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
⊢ SecondCountableTopology ↑(CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
⊢ TotallyDisconnectedSpace ↑(CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop ∧
    SecondCountableTopology ↑(CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop

Tactic:
by
        constructor
        · infer_instance
        · change SecondCountableTopology ({ u : ∀ j : J, F.obj j | _ } : Type _)
          apply IsInducing.subtypeVal.secondCountableTopology

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

Goal state before:
pp: X Y : LightProfinite
f : X ⟶ Y
⊢ (forget LightProfinite).ReflectsIsomorphisms

Tactic:
constructor

Goal state after:
X Y : LightProfinite
f : X ⟶ Y
⊢ ∀ {A B : LightProfinite} (f : A ⟶ B) [IsIso ((forget LightProfinite).map f)], IsIso f
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: X Y : LightProfinite
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
constructor

Goal state after:
case mp
X Y : LightProfinite
f : X ⟶ Y
⊢ Epi f → Function.Surjective ⇑(ConcreteCategory.hom f)

case mpr
X Y : LightProfinite
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3.refine_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
⊢ x ∈ U ↔ x ∈ ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹' ⋃ s ∈ G, W s

Tactic:
constructor

Goal state after:
case refine_3.refine_2.mp
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := ⋯
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := ⋯
W : ↑S → Set ↑(F.obj j0).toTop := ⋯
x : ↑C.pt.toTop
⊢ x ∈ U → x ∈ ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹' ⋃ s ∈ G, W s

case refine_3.refine_2.mpr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := ⋯
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := ⋯
W : ↑S → Set ↑(F.obj j0).toTop := ⋯
x : ↑C.pt.toTop
⊢ x ∈ ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹' ⋃ s ∈ G, W s → x ∈ U
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case refine_1
c✝ : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c✝ Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c✝ v) i
x : TM2.Cfg (fun x ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step tr) i
c : Cfg
hc₁ : TrCfg c x
hc₂ : c ∈ eval step (stepNormal c✝ Cont.halt v)
⊢ ∃ a ∈ c✝.eval v, halt a = x

Tactic:
simp only [stepNormal_eval, Part.map_eq_map, Part.mem_map_iff] at hc₂

Goal state after:
case refine_1
c✝ : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c✝ Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c✝ v) i
x : TM2.Cfg (fun x ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step tr) i
c : Cfg
hc₁ : TrCfg c x
hc₂ : ∃ a ∈ c✝.eval v, Cfg.halt a = c
⊢ ∃ a ∈ c✝.eval v, halt a = x
Module: Mathlib.Topology.Category.TopCat.Yoneda

Goal state before:
pp: Y : Type w'
inst✝ : TopologicalSpace Y
α : Type
X : α → TopCat
⊢ (piComparison (yonedaPresheaf' Y) fun x ↦ op (X x)) ≫ (Types.productIso fun i ↦ C(↑(X i), Y)).hom =
    (yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
      (equivEquivIso (sigmaEquiv Y fun x ↦ ↑(X x))).inv

Tactic:
ext

Goal state after:
Y : Type w'
inst✝ : TopologicalSpace Y
α : Type
X : α → TopCat
x✝¹ : (yonedaPresheaf' Y).obj (∏ᶜ fun x ↦ op (X x))
x✝ : α
a✝ : ↑(X x✝)
⊢ ((ConcreteCategory.hom
            ((piComparison (yonedaPresheaf' Y) fun x ↦ op (X x)) ≫ (Types.productIso fun i ↦ C(↑(X i), Y)).hom)).toFun
        x✝¹ x✝)
      a✝ =
    ((ConcreteCategory.hom
            ((yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
              (equivEquivIso (sigmaEquiv Y fun x ↦ ↑(X x))).inv)).toFun
        x✝¹ x✝)
      a✝
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ (q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))) ∧
    (q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q)))

Tactic:
constructor

Goal state after:
case succ.left
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' = unrev q → trStmts₁ (unrev q) ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))

case succ.right
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ insert q.succ (insert (unrev q) (trStmts₁ q))
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₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (trStmts₁ q₁ ∪ trStmts₁ q₂) S

Tactic:
refine supports_union.2 ⟨?_, ?_⟩

Goal state after:
case pred.refine_1
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
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (trStmts₁ q₁) S

case pred.refine_2
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
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (trStmts₁ q₂) S
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)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
⊢ (∀ (d : StructuredArrow c.pt toProfinite), ∃ c_1, Nonempty ((e.inverse ⋙ functor c).obj c_1 ⟶ d)) ∧
    ∀ {d : StructuredArrow c.pt toProfinite} {c_1 : ULiftHom (ULift.{w, u} I)}
      (s s' : (e.inverse ⋙ functor c).obj c_1 ⟶ d),
      ∃ c' t, (e.inverse ⋙ functor c).map t ≫ s = (e.inverse ⋙ functor c).map t ≫ s'

Tactic:
constructor

Goal state after:
case left
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)
e : I ≌ ULiftHom (ULift.{w, u} I) := ⋯
⊢ ∀ (d : StructuredArrow c.pt toProfinite), ∃ c_1, Nonempty ((e.inverse ⋙ functor c).obj c_1 ⟶ d)

case right
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)
e : I ≌ ULiftHom (ULift.{w, u} I) := ⋯
⊢ ∀ {d : StructuredArrow c.pt toProfinite} {c_1 : ULiftHom (ULift.{w, u} I)}
    (s s' : (e.inverse ⋙ functor c).obj c_1 ⟶ d),
    ∃ c' t, (e.inverse ⋙ functor c).map t ≫ s = (e.inverse ⋙ functor c).map t ≫ 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)
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:
ext

Goal state after:
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✝ : X.obj (op Q)
⊢ (ConcreteCategory.hom
          ((X.mapIso (sigmaIso r).op).hom ≫ (sigmaComparison X fun a ↦ ↑(fiber r a).toTop) ≫ ↾fun g ↦ g a)).toFun
      x✝ =
    (ConcreteCategory.hom (X.map (sigmaIncl r a).op)).toFun x✝
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:
ext

Goal state after:
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
x✝ : X
⊢ ((constRingHom.comp (algebraMap R Y)) r✝ * x✝¹) x✝ = (x✝¹ * (constRingHom.comp (algebraMap R Y)) r✝) x✝
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
x✝ : X
⊢ ((constRingHom.comp (algebraMap R Y)) r✝ * x✝¹) x✝ = (x✝¹ * (constRingHom.comp (algebraMap R Y)) r✝) x✝

Tactic:
exact Algebra.commutes' _ _

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

Goal state after:
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
x✝ : X
⊢ (r✝ • x✝¹) x✝ = ((constRingHom.comp (algebraMap R Y)) r✝ * x✝¹) x✝
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: X : CondensedSet
tfae_1_iff_2 : Condensed.IsDiscrete X ↔ IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ (discrete (Type (u + 1))).essImage X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
⊢ [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:
tfae_have 1 ↔ 6 :=
    (Sheaf.isConstant_iff_of_equivalence (coherentTopology Profinite)
      (coherentTopology CompHaus) profiniteToCompHaus Profinite.isTerminalPUnit
      CompHaus.isTerminalPUnit _).symm

Goal state after:
X : CondensedSet
tfae_1_iff_2 : Condensed.IsDiscrete X ↔ IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ (discrete (Type (u + 1))).essImage X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X)
⊢ [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