mathlib-initiative/mathlib-tactics huggingface dataset:
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
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y✝ : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y✝
xy : ↑(G.obj (pullback π π)) :=
  (ConcreteCategory.hom (PreservesPullback.iso G π π).inv)
    ((ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype (G.map π) (G.map π)).inv) ⟨(x, y✝), hxy⟩)
ha' :
  a ((ConcreteCategory.hom (G.map (pullback.fst π π))) xy) = a ((ConcreteCategory.hom (G.map (pullback.snd π π))) xy)
h₁ :
  ∀ (y : ↑(pullback (G.map π) (G.map π))),
    (ConcreteCategory.hom (G.map (pullback.fst π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
      (ConcreteCategory.hom (pullback.fst (G.map π) (G.map π))) y
y : ↑(pullback (G.map π) (G.map π))
⊢ (ConcreteCategory.hom (G.map (pullback.snd π π))) ((ConcreteCategory.hom (PreservesPullback.iso G π π).inv) y) =
    (ConcreteCategory.hom ((PreservesPullback.iso G π π).inv ≫ G.map (pullback.snd π π))) y

Tactic:
rfl

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

Goal state before:
pp: case pred
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
⊢ (q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
    (q' = unrev q₂ → trStmts₁ (unrev q₂) ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))) ∧
      (q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂)))

Tactic:
refine ⟨fun h x h' => ?_, fun _ x h' => ?_, fun h x h' => ?_⟩

Goal state after:
case pred.refine_1
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' ∈ trStmts₁ q₁
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))

case pred.refine_2
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
x✝ : q' = unrev q₂
x : Λ'
h' : x ∈ trStmts₁ (unrev q₂)
⊢ x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))

case pred.refine_3
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' ∈ trStmts₁ q₂
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x ∈ insert (q₁.pred q₂) (trStmts₁ q₁ ∪ insert (unrev q₂) (trStmts₁ q₂))
Module: Mathlib.Topology.Category.CompHausLike.SigmaComparison

Goal state before:
pp: P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
this :
  ∀ (x : ToType (X.obj (∏ᶜ fun a ↦ Opposite.op (of P (σ a))))),
    (ConcreteCategory.hom (Pi.π (fun b ↦ X.obj (Opposite.op (of P (σ b)))) a))
        ((ConcreteCategory.hom (piComparison X fun a ↦ Opposite.op (of P (σ a)))) x) =
      (ConcreteCategory.hom (X.map (Pi.π (fun a ↦ Opposite.op (of P (σ a))) a))) x
⊢ ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ } = (finiteCoproduct.cofan fun a ↦ of P (σ a)).ι.app { as := a }

Tactic:
rfl

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) α
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)
⊢ ∀ (a : α), j a ∈ Finset.image j Finset.univ

Tactic:
grind

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

Goal state before:
pp: case zero'
k : Cont'
⊢ trStmts₁ (trNormal Code.zero' k) ⊆ codeSupp' Code.zero' k

Tactic:
rfl

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

Goal state before:
pp: case succ
k : Cont'
⊢ trStmts₁ (trNormal Code.succ k) ⊆ codeSupp' Code.succ k

Tactic:
rfl

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

Goal state before:
pp: case tail
k : Cont'
⊢ trStmts₁ (trNormal Code.tail k) ⊆ codeSupp' Code.tail k

Tactic:
rfl

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

Goal state before:
pp: case cons
k : Cont'
a✝¹ a✝ : Code
⊢ trStmts₁ (trNormal (a✝¹.cons a✝) k) ⊆ codeSupp' (a✝¹.cons a✝) k

Tactic:
rfl

Goal state after:
case cons
k : Cont'
a✝¹ a✝ : Code
⊢ trStmts₁ (trNormal (a✝¹.cons a✝) k) ⊆ codeSupp' (a✝¹.cons a✝) k
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case comp
k : Cont'
a✝¹ a✝ : Code
⊢ trStmts₁ (trNormal (a✝¹.comp a✝) k) ⊆ codeSupp' (a✝¹.comp a✝) k

Tactic:
rfl

Goal state after:
case comp
k : Cont'
a✝¹ a✝ : Code
⊢ trStmts₁ (trNormal (a✝¹.comp a✝) k) ⊆ codeSupp' (a✝¹.comp a✝) k
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case case
k : Cont'
a✝¹ a✝ : Code
⊢ trStmts₁ (trNormal (a✝¹.case a✝) k) ⊆ codeSupp' (a✝¹.case a✝) k

Tactic:
rfl

Goal state after:
case case
k : Cont'
a✝¹ a✝ : Code
⊢ trStmts₁ (trNormal (a✝¹.case a✝) k) ⊆ codeSupp' (a✝¹.case a✝) k
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix
k : Cont'
a✝ : Code
⊢ trStmts₁ (trNormal a✝.fix k) ⊆ codeSupp' a✝.fix k

Tactic:
rfl

Goal state after:
case fix
k : Cont'
a✝ : Code
⊢ trStmts₁ (trNormal a✝.fix k) ⊆ codeSupp' a✝.fix k
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
  simp [codeSupp, codeSupp', Finset.union_assoc, Finset.union_left_comm]

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 (j a))) x)

Tactic:
rfl

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
⊢ (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg) x = gg ((ConcreteCategory.hom (C.π.app j)) x)

Tactic:
rfl

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✝¹

Tactic:
rfl

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

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

Tactic:
rfl

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 + 1) ≫ S.diagram.map (Opposite.op (homOfLE ⋯))))

Tactic:
rfl

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 m ≫ S.diagram.map (Opposite.op (homOfLE h))))

Tactic:
rfl

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

Goal state before:
pp: case inr
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✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toTop) (Quotient S.toSetoid) := { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' : LocallyConstant (↑(F.obj j).toTop) (Quotient S.toSetoid)
t : ↑C.pt.toTop
hj : f' t = g' ((TopCat.Hom.hom (C.π.app j).hom) t)
⊢ f t = ff (f' t)

Tactic:
rfl

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
  simp only [Finset.union_subset_iff] at H₂
  exact supports_union.2 ⟨trStmts₁_supports H₁ H₂.1, H₃ H₂.2⟩

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✝ : X.obj (op Q)
⊢ (ConcreteCategory.hom (X.map ((sigmaIso r).hom.op ≫ (ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ }).op)))
      x✝ =
    (ConcreteCategory.hom (X.map (sigmaIncl r a).op)) x✝

Tactic:
rfl

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

Goal state before:
pp: case comp
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S

Tactic:
have H' := H; rw [contSupp_comp] at H'; have H₂ := Finset.union_subset_right H'
    exact supports_union.2 ⟨codeSupp'_supports H', IH H₂⟩

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

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f✝ : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g✝ : T ⟶ S✝
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
this : Preregular (CompHausLike P)
S : (CompHausLike P)ᵒᵖ
f : LocallyConstant (↑(unop S).toTop) (X.obj.obj (op (of P PUnit.{u + 1})))
a : Fiber ⇑(map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f)
b :
  Fiber
    ⇑(comap (TopCat.Hom.hom (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
        f)
a✝ :
  ↑(fiber
        (comap
          (TopCat.Hom.hom (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom) f)
        b).toTop
⊢ (ConcreteCategory.hom
        (sigmaIncl
            (comap
              (TopCat.Hom.hom (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
              f)
            b ≫
          sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a))
      a✝ =
    (ConcreteCategory.hom
        (ofHom P (sigmaInclIncl (⇑f) (ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1})))).1 a b) ≫
          sigmaIncl f
            (Fiber.mk ⇑f
              ↑(preimage
                  (⇑f ∘
                    ⇑(TopologicalSpace.Fiber.sigmaIncl
                        ((ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1})))).1 ∘ ⇑f) a))
                  b))))
      a✝

Tactic:
rfl

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)
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)
x : ↑↑a
⊢ ({
          toFun := fun g ↦
            comap
              (TopCat.Hom.hom
                (isTerminalPUnit.from
                    (fiber (map (⇑(ConcreteCategory.hom (↾fun x ↦ LocallyConstant.const PUnit.{u + 1} x))) f) a)).hom)
              g }
        ((map (⇑(ConcreteCategory.hom ((unit P hs).app X))) f) ↑x))
      x =
    ({
          toFun := fun g ↦
            comap
              (TopCat.Hom.hom
                (sigmaIncl (map (⇑(ConcreteCategory.hom (↾fun x ↦ LocallyConstant.const PUnit.{u + 1} x))) f) a).hom)
              g }
        f)
      x

Tactic:
rfl

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

Goal state before:
pp: case e_a
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ ((presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map
        ((Functor.const CompHausᵒᵖ).map
          (((functor R).map f).hom.app (op (CompHaus.of PUnit.{u + 1})) ≫ (functorIsoDiscreteAux₁ R Y✝).inv))).hom =
    ((presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map
        ((Functor.const CompHausᵒᵖ).map ((functorIsoDiscreteAux₁ R X✝).inv ≫ f))).hom

Tactic:
rfl

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

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
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
          (isTerminalPUnit.from
              (fiber ((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) a)).op))
      (((ConcreteCategory.hom ((unit P hs).app (X.obj.obj (op (of P PUnit.{u + 1}))))) x) ↑⟨PUnit.unit, ⋯⟩) =
    (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:
rfl

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

Goal state before:
pp: case e_a
P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ ((presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map
        ((Functor.const LightProfiniteᵒᵖ).map
          (((functor R).map f).hom.app (op (LightProfinite.of PUnit.{u + 1})) ≫
            (functorIsoDiscreteAux₁ R Y✝).inv))).hom =
    ((presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map
        ((Functor.const LightProfiniteᵒᵖ).map ((functorIsoDiscreteAux₁ R X✝).inv ≫ f))).hom

Tactic:
rfl

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

Goal state before:
pp: case refine_1.none.none
h : natUnionInftyEmbedding none = natUnionInftyEmbedding none
⊢ none = none

Tactic:
rfl

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

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

Tactic:
intro (f : LocallyConstant c.pt X)
    obtain ⟨j, h⟩ := Profinite.exists_locallyConstant.{_, u} c hc f
    exact ⟨⟨j⟩, h⟩

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

Goal state before:
pp: X✝ Y : LightCondSet
f : X✝ ⟶ Y
X : LightCondSet
x✝³ x✝² : LightProfiniteᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj.obj x✝³
⊢ { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (x✝¹ ≫ (CompHausLike.const (of PUnit.{u + 1}) s).op))) x✝,
      continuous_toFun := ⋯ } =
    (ConcreteCategory.hom (↾fun g ↦ g.comp (TopCat.Hom.hom x✝¹.unop.hom)))
      { toFun := fun s ↦ (ConcreteCategory.hom (X.obj.map (CompHausLike.const (of PUnit.{u + 1}) s).op)) x✝,
        continuous_toFun := ⋯ }

Tactic:
rfl

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

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : IsColimit (F.mapCocone S.asLimitCone.op)
⊢ ((colimit.isColimit (S.diagram.op ⋙ F)).coconePointUniqueUpToIso hF).hom =
    colimit.desc
      (Profinite.Extend.functorOp S.asLimitCone ⋙
        CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ F)
      (Cocone.whisker (Profinite.Extend.functorOp S.asLimitCone) (Profinite.Extend.cocone F S))

Tactic:
rfl

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✝
x✝¹ : F.obj (Opposite.op (toProfinite.obj (Opposite.unop X✝)))
x✝ : (Opposite.unop Y✝).obj
⊢ (ConcreteCategory.hom
        (F.map ((toProfinite.map x✝².unop).op ≫ (CompHausLike.const (Profinite.of PUnit.{u + 1}) x✝).op)))
      x✝¹ =
    (ConcreteCategory.hom ((finYoneda F).map x✝²))
      (fun x ↦ (ConcreteCategory.hom (F.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) x).op)) x✝¹) x✝

Tactic:
rfl

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

Goal state before:
pp: X✝ Y✝ : LightProfinite
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi (lightProfiniteToLightCondSet.map f)

Tactic:
rw [LightCondSet.epi_iff_locallySurjective_on_lightProfinite]
    intro S g
    refine ⟨pullback f g, pullback.snd _ _, fun y ↦ ?_, pullback.fst _ _, pullback.condition _ _⟩
    rw [LightProfinite.epi_iff_surjective] at hf
    obtain ⟨x, hx⟩ := hf (g.hom y)
    exact ⟨⟨⟨x, y⟩, hx⟩, rfl⟩

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

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ ((colimit.isColimit (S.diagram.rightOp ⋙ F)).coconePointUniqueUpToIso hF).hom =
    colimit.desc
      (LightProfinite.Extend.functorOp S.asLimitCone ⋙
        CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ F)
      (Cocone.whisker (LightProfinite.Extend.functorOp S.asLimitCone) (LightProfinite.Extend.cocone F S))

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst✝ : Epi f
S : LightProfinite
p : (LightCondensed.free R).obj S.toCondensed ⟶ Y
this :
  ∀ (S : LightProfinite) (y : ((LightCondensed.forget R).obj Y).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op φ))) y
T : LightProfinite
π : T ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
x : ((LightCondensed.forget R).obj X).obj.obj (Opposite.op T)
hx :
  (ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app (Opposite.op T))) x =
    (ConcreteCategory.hom (((LightCondensed.forget R).obj Y).obj.map (Opposite.op π)))
      ((coherentTopology LightProfinite).yonedaEquiv
        (((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p))
⊢ (lightProfiniteToLightCondSet.map π ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv (lightProfiniteToLightCondSet.obj S) Y) p).hom =
    ((coherentTopology LightProfinite).yonedaEquiv.symm (Quiver.Hom.unop (Opposite.op π)) ≫
        ((LightCondensed.freeForgetAdjunction R).homEquiv S.toCondensed Y) p).hom

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after: