mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
⊢ IsTotallySeparated univ

Tactic:
by
    intro x _ y _ hxy
    obtain ⟨U, V, hUV⟩ := T2Space.t2 hxy
    refine ⟨closure U, (closure U)ᶜ, ExtremallyDisconnected.open_closure U hUV.1,
      by simp only [isOpen_compl_iff, isClosed_closure], subset_closure hUV.2.2.1, ?_,
      by simp only [Set.union_compl_self, Set.subset_univ], disjoint_compl_right⟩
    rw [Set.mem_compl_iff, mem_closure_iff]
    push Not
    refine ⟨V, ⟨hUV.2.1, hUV.2.2.2.1, ?_⟩⟩
    rw [← Set.disjoint_iff_inter_eq_empty, disjoint_comm]
    exact hUV.2.2.2.2

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
⊢ C ⊆ S → IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c

Tactic:
C_sub

Goal state after:
A D : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace D
inst✝¹ : T1Space A
inst✝ : CompactSpace D
X : D → A
X_cont : Continuous X
X_surj : Surjective X
S : Set (Set D) := {E | IsClosed E ∧ X '' E = univ}
C : Set (Set D)
C_sub : C ⊆ S
⊢ IsChain (fun x1 x2 ↦ x1 ⊆ x2) C → ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case case
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepNormal (f.case g) k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
rw [stepNormal]
    simp only
    obtain ⟨s', h⟩ := pred_ok _ _ s v _ _
    revert h; rcases v.headI with - | n <;> intro h
    · obtain ⟨c, h₁, h₂⟩ := IHf k _ s'
      exact ⟨_, h₁, h.trans h₂⟩
    · obtain ⟨c, h₁, h₂⟩ := IHg k _ s'
      exact ⟨_, h₁, h.trans h₂⟩

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 := ⋯ }
⊢ False

Tactic:
let h : Y ⟶ Z := CompHausLike.ofHom _ ⟨fun _ => ⟨1⟩, continuous_const⟩

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 := ⋯ }
⊢ False
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pos
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
c : Cfg'
h₁ : TrCfg (stepRet k v.tail) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (Λ'.ret (trCont k)), var := (trList v).head?, stk := elim (trList v.tail) [] [] (trContStack k) } c
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux (tr (Λ'.ret (trCont (Cont.fix f k)))) s (elim (trList v) [] [] (trContStack (Cont.fix f k)))) c

Tactic:
rw [trCont, tr]

Goal state after:
case pos
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
c : Cfg'
h₁ : TrCfg (stepRet k v.tail) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (Λ'.ret (trCont k)), var := (trList v).head?, stk := elim (trList v.tail) [] [] (trContStack k) } c
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux
      (pop' main
        (goto fun s ↦
          bif natEnd (s.getD default) then Λ'.ret (trCont k)
          else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      s (elim (trList v) [] [] (trContStack (Cont.fix f k))))
    c
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case neg
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.fix f k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
    s'
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux (tr (Λ'.ret (trCont (Cont.fix f k)))) s (elim (trList v) [] [] (trContStack (Cont.fix f k))))
    { l := some (trNormal f (trCont (Cont.fix f k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }

Tactic:
rw [trCont, tr]

Goal state after:
case neg
f : Code
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.fix f k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
    s'
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux
      (pop' main
        (goto fun s ↦
          bif natEnd (s.getD default) then Λ'.ret (trCont k)
          else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      s (elim (trList v) [] [] (trContStack (Cont.fix f k))))
    { l := some (trNormal f (Cont'.fix f (trCont k))), var := some Γ'.cons,
      stk := elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) }
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f✝ : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T✝ : CompHausLike P
g✝ : T✝ ⟶ S✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
⊢ (ConcreteCategory.hom
          ((functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).map g ≫
            match T with
            | op S => counitAppApp S Y)).toFun
      f =
    (ConcreteCategory.hom
          ((match S with
            | op S => counitAppApp S Y) ≫
            Y.map g)).toFun
      f

Tactic:
apply presheaf_ext (f.comap g.unop.hom.hom)

Goal state after:
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f✝ : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T✝ : CompHausLike P
g✝ : T✝ ⟶ S✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
⊢ ∀ (a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)),
    (ConcreteCategory.hom (Y.map (sigmaIncl (comap (TopCat.Hom.hom g.unop.hom) f) a).op))
        ((ConcreteCategory.hom
              ((functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).map g ≫
                match T with
                | op S => counitAppApp S Y)).toFun
          f) =
      (ConcreteCategory.hom (Y.map (sigmaIncl (comap (TopCat.Hom.hom g.unop.hom) f) a).op))
        ((ConcreteCategory.hom
              ((match S with
                | op S => counitAppApp S Y) ≫
                Y.map g)).toFun
          f)
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
⊢ [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 ↔ 5 :=
    have : functor.Faithful := inferInstance
    have : functor.Full := inferInstance
    -- These `have` statements above shouldn't be needed, but they are.
    Sheaf.isConstant_iff_isIso_counit_app' _ CompHaus.isTerminalPUnit adjunction _

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)
⊢ [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
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
  tfae_have 1 ↔ 2 := Sheaf.isConstant_iff_isIso_counit_app _ _ _
  tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
  tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _ CompHaus.isTerminalPUnit adjunction _
  tfae_have 1 ↔ 5 :=
    have : functor.Faithful := inferInstance
    have : functor.Full := inferInstance
    -- These `have` statements above shouldn't be needed, but they are.
    Sheaf.isConstant_iff_isIso_counit_app' _ CompHaus.isTerminalPUnit adjunction _
  tfae_have 1 ↔ 6 :=
    (Sheaf.isConstant_iff_of_equivalence (coherentTopology Profinite)
      (coherentTopology CompHaus) profiniteToCompHaus Profinite.isTerminalPUnit
      CompHaus.isTerminalPUnit _).symm
  tfae_have 7 → 4 := fun h ↦
    mem_locallyConstant_essImage_of_isColimit_mapCocone X (fun S ↦ (h S).some)
  tfae_have 4 → 7 := fun ⟨Y, ⟨i⟩⟩ S ↦
    ⟨IsColimit.mapCoconeEquiv (isoWhiskerLeft profiniteToCompHaus.op
      ((sheafToPresheaf _ _).mapIso i))
      (Condensed.isColimitLocallyConstantPresheafDiagram Y S)⟩
  tfae_finish

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

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
⊢ IsIso
    ((constantSheafAdj (coherentTopology CompHaus) (Type (u + 1)) CompHaus.isTerminalPUnit).counit.app
      ((sheafCompose (coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M)))

Tactic:
have : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Faithful :=
    inferInstanceAs (discrete _).Faithful

Goal state after:
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
this : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Faithful
⊢ IsIso
    ((constantSheafAdj (coherentTopology CompHaus) (Type (u + 1)) CompHaus.isTerminalPUnit).counit.app
      ((sheafCompose (coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M)))
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X profiniteToCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)
F : Profiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)
⊢ IsSheaf (coherentTopology Profinite) (F ⋙ CategoryTheory.forget A)

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]

Goal state after:
A : Type u_1
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X profiniteToCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)
F : Profiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A) ∧ EqualizerCondition (F ⋙ CategoryTheory.forget A)
Module: Mathlib.Condensed.Explicit

Goal state before:
pp: A : Type u_1
inst✝⁴ : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)
F : CompHausᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)
⊢ IsSheaf (coherentTopology CompHaus) (F ⋙ CategoryTheory.forget A)

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]

Goal state after:
A : Type u_1
inst✝⁴ : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)
F : CompHausᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A) ∧ EqualizerCondition (F ⋙ CategoryTheory.forget A)
Module: Mathlib.Topology.Category.LightProfinite.Sequence

Goal state before:
pp: case refine_1.some.some
n m : ℕ
h : natUnionInftyEmbedding (Option.some n) = natUnionInftyEmbedding (Option.some m)
⊢ Option.some n = Option.some m

Tactic:
· simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, inv_inj, add_left_inj,
        Nat.cast_inj] at h
      rw [h]

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)
F : LightProfiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)
⊢ IsSheaf (coherentTopology LightProfinite) (F ⋙ CategoryTheory.forget A)

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]

Goal state after:
A : Type u_1
inst✝⁴ : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : ReflectsFiniteLimits (CategoryTheory.forget A)
F : LightProfiniteᵒᵖ ⥤ A
inst✝ : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A) ∧ EqualizerCondition (F ⋙ CategoryTheory.forget A)
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ᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
⊢ (↾fun f ↦ ⇑f) ≫ (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (locallyConstantPresheaf
            (X.obj
              (Opposite.op
                (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
                  PUnit.{u + 1})))).map
        g ≫
      counitAppApp (Opposite.unop S) X

Tactic:
erw [(counitApp.{u, u} X).naturality]

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✝
⊢ (↾fun f ↦ ⇑f) ≫ (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv ≫ X.map g =
    (counitApp X).app (toLightProfinite.op.obj Y) ≫ X.map g
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
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero → ⋯.fix (fixAux f) Upto.zero x = Fix.approx f (k + 1) x

Tactic:
revert this

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
k : ℕ
⊢ p (k + ↑Upto.zero) → Nat.find h' = k + ↑Upto.zero → ⋯.fix (fixAux f) Upto.zero x = Fix.approx f (k + 1) x
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case nil
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) [] = Comp.mk (List.traverse f <$> List.traverse g [])

Tactic:
simp! [*, functor_norm]

Goal state after:
case nil
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ pure [] = Comp.mk (pure (pure []))
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case cons
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) tail✝ = Comp.mk (List.traverse f <$> List.traverse g tail✝)
⊢ List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (head✝ :: tail✝) =
    Comp.mk (List.traverse f <$> List.traverse g (head✝ :: tail✝))

Tactic:
simp! [*, functor_norm]

Goal state after:
case cons
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) tail✝ = Comp.mk (List.traverse f <$> List.traverse g tail✝)
⊢ Comp.mk ((fun a ↦ (fun x2 ↦ cons <$> f a <*> x2) ∘ List.traverse f) <$> g head✝ <*> List.traverse g tail✝) =
    Comp.mk ((fun a ↦ List.traverse f ∘ cons a) <$> g head✝ <*> List.traverse g tail✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case nil
α β : Type u_1
f : α → β
⊢ List.traverse (pure ∘ f) [] = pure (f <$> [])

Tactic:
simp! [*, functor_norm]

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case cons
α β : Type u_1
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : List.traverse (pure ∘ f) tail✝ = pure (f <$> tail✝)
⊢ List.traverse (pure ∘ f) (head✝ :: tail✝) = pure (f <$> (head✝ :: tail✝))

Tactic:
simp! [*, functor_norm]

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
⊢ (fun {α} ↦ η.app α) (List.traverse f []) = List.traverse ((fun {α} ↦ η.app α) ∘ f) []

Tactic:
simp! [*, functor_norm]

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
head✝ : α
tail✝ : List α
tail_ih✝ : (fun {α} ↦ η.app α) (List.traverse f tail✝) = List.traverse ((fun {α} ↦ η.app α) ∘ f) tail✝
⊢ (fun {α} ↦ η.app α) (List.traverse f (head✝ :: tail✝)) = List.traverse ((fun {α} ↦ η.app α) ∘ f) (head✝ :: tail✝)

Tactic:
simp! [*, functor_norm]

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ α β : Type u
f : α → β
val✝ : σ
⊢ Sum.traverse (pure ∘ f) (inl val✝) = pure (f <$> inl val✝)

Tactic:
simp! [*, functor_norm]

Goal state after:
case inl
σ α β : Type u
f : α → β
val✝ : σ
⊢ pure (inl val✝) = pure (f <$> inl val✝)
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inr
σ α β : Type u
f : α → β
val✝ : α
⊢ Sum.traverse (pure ∘ f) (inr val✝) = pure (f <$> inr val✝)

Tactic:
simp! [*, functor_norm]

Goal state after:
case inr
σ α β : Type u
f : α → β
val✝ : α
⊢ pure (inr (f val✝)) = pure (f <$> inr val✝)
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (Prod.snd ∘ π ⁻¹' {↑i})

Tactic:
exact .preimage (continuous_snd.comp hπ) ⟨fun h ↦ by simp_all, by simp⟩

Goal state after: