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

Goal state before:
pp: A : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ExtremallyDisconnected A
inst✝³ : CompactSpace A
inst✝² : T2Space A
B C : Type u
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
⊢ ∀ [CompactSpace B] [T2Space B] [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
_

Goal state after:
A : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : ExtremallyDisconnected A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space A
B C : Type u
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : CompactSpace B
⊢ ∀ [T2Space B] [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A : Type u
inst✝⁶ : TopologicalSpace A
inst✝⁵ : ExtremallyDisconnected A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space A
B C : Type u
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace C
inst✝ : CompactSpace B
⊢ ∀ [T2Space B] [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
_

Goal state after:
A : Type u
inst✝⁷ : TopologicalSpace A
inst✝⁶ : ExtremallyDisconnected A
inst✝⁵ : CompactSpace A
inst✝⁴ : T2Space A
B C : Type u
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace C
inst✝¹ : CompactSpace B
inst✝ : T2Space B
⊢ ∀ [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A : Type u
inst✝⁷ : TopologicalSpace A
inst✝⁶ : ExtremallyDisconnected A
inst✝⁵ : CompactSpace A
inst✝⁴ : T2Space A
B C : Type u
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace C
inst✝¹ : CompactSpace B
inst✝ : T2Space B
⊢ ∀ [CompactSpace C] [T2Space C] {f : A → C} {g : B → C},
    Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
_

Goal state after:
A : Type u
inst✝⁸ : TopologicalSpace A
inst✝⁷ : ExtremallyDisconnected A
inst✝⁶ : CompactSpace A
inst✝⁵ : T2Space A
B C : Type u
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace C
inst✝² : CompactSpace B
inst✝¹ : T2Space B
inst✝ : CompactSpace C
⊢ ∀ [T2Space C] {f : A → C} {g : B → C}, Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A : Type u
inst✝⁸ : TopologicalSpace A
inst✝⁷ : ExtremallyDisconnected A
inst✝⁶ : CompactSpace A
inst✝⁵ : T2Space A
B C : Type u
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace C
inst✝² : CompactSpace B
inst✝¹ : T2Space B
inst✝ : CompactSpace C
⊢ ∀ [T2Space C] {f : A → C} {g : B → C}, Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
_

Goal state after:
A : Type u
inst✝⁹ : TopologicalSpace A
inst✝⁸ : ExtremallyDisconnected A
inst✝⁷ : CompactSpace A
inst✝⁶ : T2Space A
B C : Type u
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace C
inst✝³ : CompactSpace B
inst✝² : T2Space B
inst✝¹ : CompactSpace C
inst✝ : T2Space C
⊢ ∀ {f : A → C} {g : B → C}, Continuous f → Continuous g → Surjective g → ∃ h, Continuous h ∧ g ∘ h = f
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
inst✝ : Projective X
A B : Type u
⊢ ∀ [inst : TopologicalSpace A] [inst_1 : TopologicalSpace B] [CompactSpace A] [T2Space A] [CompactSpace B] [T2Space B]
    {f : ↑X.toTop → B} {g : A → B}, Continuous f → Continuous g → Function.Surjective g → ∃ h, Continuous h ∧ g ∘ h = f

Tactic:
_

Goal state after:
X : CompHaus
inst✝¹ : Projective X
A B : Type u
inst✝ : TopologicalSpace A
⊢ ∀ [inst : TopologicalSpace B] [CompactSpace A] [T2Space A] [CompactSpace B] [T2Space B] {f : ↑X.toTop → B}
    {g : A → B}, Continuous f → Continuous[inst✝, _] g → Function.Surjective g → ∃ h, Continuous[_, inst✝] h ∧ g ∘ h = f
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
inst✝¹ : Projective X
A B : Type u
inst✝ : TopologicalSpace A
⊢ ∀ [inst : TopologicalSpace B] [CompactSpace A] [T2Space A] [CompactSpace B] [T2Space B] {f : ↑X.toTop → B}
    {g : A → B}, Continuous f → Continuous[inst✝, _] g → Function.Surjective g → ∃ h, Continuous[_, inst✝] h ∧ g ∘ h = f

Tactic:
_

Goal state after:
X : CompHaus
inst✝² : Projective X
A B : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ ∀ [CompactSpace A] [T2Space A] [CompactSpace B] [T2Space B] {f : ↑X.toTop → B} {g : A → B},
    Continuous[_, inst✝] f →
      Continuous[inst✝¹, inst✝] g → Function.Surjective g → ∃ h, Continuous[_, inst✝¹] h ∧ g ∘ h = f
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
inst✝² : Projective X
A B : Type u
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ ∀ [CompactSpace A] [T2Space A] [CompactSpace B] [T2Space B] {f : ↑X.toTop → B} {g : A → B},
    Continuous[_, inst✝] f →
      Continuous[inst✝¹, inst✝] g → Function.Surjective g → ∃ h, Continuous[_, inst✝¹] h ∧ g ∘ h = f

Tactic:
_

Goal state after:
X : CompHaus
inst✝³ : Projective X
A B : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : CompactSpace A
⊢ ∀ [T2Space A] [CompactSpace B] [T2Space B] {f : ↑X.toTop → B} {g : A → B},
    Continuous[_, inst✝¹] f →
      Continuous[inst✝², inst✝¹] g → Function.Surjective g → ∃ h, Continuous[_, inst✝²] h ∧ g ∘ h = f
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
inst✝³ : Projective X
A B : Type u
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : CompactSpace A
⊢ ∀ [T2Space A] [CompactSpace B] [T2Space B] {f : ↑X.toTop → B} {g : A → B},
    Continuous[_, inst✝¹] f →
      Continuous[inst✝², inst✝¹] g → Function.Surjective g → ∃ h, Continuous[_, inst✝²] h ∧ g ∘ h = f

Tactic:
_

Goal state after:
X : CompHaus
inst✝⁴ : Projective X
A B : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : CompactSpace A
inst✝ : T2Space A
⊢ ∀ [CompactSpace B] [T2Space B] {f : ↑X.toTop → B} {g : A → B},
    Continuous[_, inst✝²] f →
      Continuous[inst✝³, inst✝²] g → Function.Surjective g → ∃ h, Continuous[_, inst✝³] h ∧ g ∘ h = f
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
inst✝⁴ : Projective X
A B : Type u
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : CompactSpace A
inst✝ : T2Space A
⊢ ∀ [CompactSpace B] [T2Space B] {f : ↑X.toTop → B} {g : A → B},
    Continuous[_, inst✝²] f →
      Continuous[inst✝³, inst✝²] g → Function.Surjective g → ∃ h, Continuous[_, inst✝³] h ∧ g ∘ h = f

Tactic:
_

Goal state after:
X : CompHaus
inst✝⁵ : Projective X
A B : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace B
inst✝² : CompactSpace A
inst✝¹ : T2Space A
inst✝ : CompactSpace B
⊢ ∀ [T2Space B] {f : ↑X.toTop → B} {g : A → B},
    Continuous[_, inst✝³] f →
      Continuous[inst✝⁴, inst✝³] g → Function.Surjective g → ∃ h, Continuous[_, inst✝⁴] h ∧ g ∘ h = f
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : CompHaus
inst✝⁵ : Projective X
A B : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace B
inst✝² : CompactSpace A
inst✝¹ : T2Space A
inst✝ : CompactSpace B
⊢ ∀ [T2Space B] {f : ↑X.toTop → B} {g : A → B},
    Continuous[_, inst✝³] f →
      Continuous[inst✝⁴, inst✝³] g → Function.Surjective g → ∃ h, Continuous[_, inst✝⁴] h ∧ g ∘ h = f

Tactic:
_

Goal state after:
X : CompHaus
inst✝⁶ : Projective X
A B : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : CompactSpace A
inst✝² : T2Space A
inst✝¹ : CompactSpace B
inst✝ : T2Space B
⊢ ∀ {f : ↑X.toTop → B} {g : A → B},
    Continuous[_, inst✝⁴] f →
      Continuous[inst✝⁵, inst✝⁴] g → Function.Surjective g → ∃ h, Continuous[_, inst✝⁵] h ∧ g ∘ h = f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case hf
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
⊢ IsOpen U → IsOpen (Sigma.mk i '' U)

Tactic:
_

Goal state after:
case hf
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
h₀✝ : ∀ (i : ι), ExtremallyDisconnected (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
a✝ : IsOpen U
⊢ IsOpen (Sigma.mk i '' U)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
⊢ IsOpen (closure U)

Tactic:
by
    by_cases! Un : U = ∅
    · simp_all
    · exact ((preirreducibleSpace_iff_open_dense X).mp h hU Un).closure_eq ▸ isOpen_univ

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

Goal state before:
pp: X : Type u_1
inst✝² : Finite X
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
U : Set X
⊢ IsOpen[(CompHaus.of X).toTop.str] U → IsOpen[(CompHaus.of X).toTop.str] (closure[(CompHaus.of X).toTop.str] U)

Tactic:
_

Goal state after:
X : Type u_1
inst✝² : Finite X
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
U : Set X
a✝ : IsOpen[(CompHaus.of X).toTop.str] U
⊢ IsOpen[(CompHaus.of X).toTop.str] (closure[(CompHaus.of X).toTop.str] U)
Module: Mathlib.Topology.Category.Stonean.Limits

Goal state before:
pp: X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
X✝ : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y
⊢ ∀ ⦃Y B : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y⦄ (f : X✝ ⟶ B) (g : Y ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g

Tactic:
_

Goal state after:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
X✝ Y✝ : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y
⊢ ∀ ⦃B : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y⦄ (f : X✝ ⟶ B) (g : Y✝ ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
Module: Mathlib.Topology.Category.Stonean.Limits

Goal state before:
pp: X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
X✝ Y✝ : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y
⊢ ∀ ⦃B : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y⦄ (f : X✝ ⟶ B) (g : Y✝ ⟶ B),
    IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g

Tactic:
_

Goal state after:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
X✝ Y✝ B✝ : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y
⊢ ∀ (f : X✝ ⟶ B✝) (g : Y✝ ⟶ B✝), IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g
Module: Mathlib.Topology.Category.Stonean.Limits

Goal state before:
pp: X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
X✝ Y✝ B✝ : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y
⊢ ∀ (f : X✝ ⟶ B✝) (g : Y✝ ⟶ B✝), IsOpenEmbedding ⇑(ConcreteCategory.hom f) → HasExplicitPullback f g

Tactic:
_

Goal state after:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
X✝ Y✝ B✝ : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y
f✝ : X✝ ⟶ B✝
⊢ ∀ (g : Y✝ ⟶ B✝), IsOpenEmbedding ⇑(ConcreteCategory.hom f✝) → HasExplicitPullback f✝ g
Module: Mathlib.Topology.Category.Stonean.Limits

Goal state before:
pp: X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
X✝ Y✝ B✝ : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y
f✝ : X✝ ⟶ B✝
⊢ ∀ (g : Y✝ ⟶ B✝), IsOpenEmbedding ⇑(ConcreteCategory.hom f✝) → HasExplicitPullback f✝ g

Tactic:
_

Goal state after:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
X✝ Y✝ B✝ : CompHausLike fun Y ↦ ExtremallyDisconnected ↑Y
f✝ : X✝ ⟶ B✝
g✝ : Y✝ ⟶ B✝
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom f✝) → HasExplicitPullback f✝ g✝
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
⊢ ∀ [Epi f], ∃ f', f' ≫ f = φ

Tactic:
_

Goal state after:
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
⊢ ∃ f', f' ≫ f = φ
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
f : B ⟶ C
⊢ ∀ [Epi f], ∃ f', f' ≫ f = φ

Tactic:
_

Goal state after:
X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
f : B ⟶ C
inst✝ : Epi f
⊢ ∃ f', f' ≫ f = φ
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X B C : Stonean
φ : X ⟶ C
f : B ⟶ C
⊢ ∀ [Epi f], ∃ f', f' ≫ f = φ

Tactic:
_

Goal state after:
X B C : Stonean
φ : X ⟶ C
f : B ⟶ C
inst✝ : Epi f
⊢ ∃ f', f' ≫ f = φ
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux
      (pop' main
        (branch (fun s ↦ decide (s = some Γ'.bit0)) (push rev (fun x ↦ Γ'.bit1) (goto fun x ↦ q₁.pred q₂))
          (branch (fun s ↦ natEnd (s.getD default)) (goto fun x ↦ q₁)
            (peek' main
              (branch (fun s ↦ natEnd (s.getD default)) (goto fun x ↦ unrev q₂)
                (push rev (fun x ↦ Γ'.bit0) (goto fun x ↦ unrev q₂)))))))
      s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }

Tactic:
simp only [pop', TM2.stepAux]

Goal state after:
case cons.succ.zero
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
      { l := some (q₁.pred q₂), var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
        stk :=
          update
            (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
              (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
            rev
            (Γ'.bit1 ::
              update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
                (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail rev) }
    else
      bif natEnd ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?.getD default) then
        { l := some q₁, var := (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?,
          stk :=
            update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
              (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail }
      else
        TM2.stepAux
          (peek' main
            (branch (fun s ↦ natEnd (s.getD default)) (goto fun x ↦ unrev q₂)
              (push rev (fun x ↦ Γ'.bit0) (goto fun x ↦ unrev q₂))))
          (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
          (update (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
            (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail))
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }
Module: Mathlib.Topology.Category.Profinite.AsLimit

Goal state before:
pp: case refine_1
X : Profinite
a b : (fun X ↦ ↑X.toTop) X.asLimitCone.pt
h :
  (ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone)) a =
    (ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone)) b
⊢ a = b

Tactic:
refine DiscreteQuotient.eq_of_forall_proj_eq fun S => ?_
        apply_fun fun f : (limitCone.{u, u} X.diagram).pt => f.val S at h
        exact h

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

Goal state before:
pp: X✝ : CompHausLike fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X
⊢ ∀ ⦃Y : CompHausLike fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X⦄ (f : X✝ ⟶ Y),
    EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
_

Goal state after:
X✝ Y✝ : CompHausLike fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X
⊢ ∀ (f : X✝ ⟶ Y✝), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
Module: Mathlib.Topology.Category.LightProfinite.Basic

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

Tactic:
ext ⟨g, p⟩

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
j k : J
f : j ⟶ k
g : (j : J) → ↑(((F ⋙ lightProfiniteToCompHaus) ⋙ compHausToTop).obj j)
p :
  g ∈
    {u |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (((F ⋙ lightProfiniteToCompHaus) ⋙ compHausToTop).map f)) (u i) = u j}
⊢ (ConcreteCategory.hom
        (((Functor.const J).obj
                { toTop := (CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop, is_compact := ⋯,
                  is_hausdorff := ⋯, prop := ⋯ }).map
            f ≫
          ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app k).hom)))
      ⟨g, p⟩ =
    (ConcreteCategory.hom
        (ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app j).hom) ≫
          F.map f))
      ⟨g, p⟩
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: X✝ : LightDiagram
⊢ ∀ {Y : LightDiagram} (f : X✝ ⟶ Y),
    (lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).map f ≫
        (lightDiagramToProfinite.preimageIso
            (Iso.refl
              (lightDiagramToProfinite.obj
                ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj Y)))).hom =
      (lightDiagramToProfinite.preimageIso
            (Iso.refl
              (lightDiagramToProfinite.obj
                ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj X✝)))).hom ≫
        (𝟭 LightDiagram).map f

Tactic:
_

Goal state after:
X✝ Y✝ : LightDiagram
⊢ ∀ (f : X✝ ⟶ Y✝),
    (lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).map f ≫
        (lightDiagramToProfinite.preimageIso
            (Iso.refl
              (lightDiagramToProfinite.obj
                ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj Y✝)))).hom =
      (lightDiagramToProfinite.preimageIso
            (Iso.refl
              (lightDiagramToProfinite.obj
                ((lightDiagramToLightProfinite ⋙ lightProfiniteToLightDiagram).obj X✝)))).hom ≫
        (𝟭 LightDiagram).map f
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 π))
Z B : C
π : Z ⟶ B
⊢ ∀ [EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective
      ⇑(ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯))

Tactic:
_

Goal state after:
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 π))
Z B : C
π : Z ⟶ B
inst✝ : EffectiveEpi π
⊢ ∀ [inst : HasPullback π π],
    Function.Bijective
      ⇑(ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯))
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 π))
Z B : C
π : Z ⟶ B
inst✝ : EffectiveEpi π
⊢ ∀ [inst : HasPullback π π],
    Function.Bijective
      ⇑(ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯))

Tactic:
_

Goal state after:
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 π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯))
Module: Mathlib.Logic.Function.FiberPartition

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : Y → Z
g : X → Y
a : Fiber (f ∘ g)
⊢ f (g (preimage (f ∘ g) a)) = image f (mk f (g (preimage (f ∘ g) a)))

Tactic:
mk_image

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : Y → Z
g : X → Y
a : Fiber (f ∘ g)
⊢ f (g (preimage (f ∘ g) a)) = f (g (preimage (f ∘ g) a))
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: case refine_1
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 π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
a b : (fun X ↦ X) ((yonedaPresheaf G X).obj (op B))
h :
  (ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)) a =
    (ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)) b
⊢ a = b

pp: case refine_2
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 π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
x✝ :
  (fun X ↦ X)
    ↑{x |
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
          (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
a : (yonedaPresheaf G X).obj (op Z)
ha :
  a ∈
    {x |
      (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
⊢ ∃ a_1,
    (ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)) a_1 = ⟨a, ha⟩

Tactic:
· simp only [yonedaPresheaf, comp, Quiver.Hom.unop_op, TypeCat.Fun.coe_mk,
      Set.coe_ofPred, mapToEqualizer, Set.mem_ofPred_eq, ConcreteCategory.hom_ofHom,
      Subtype.mk.injEq, mk.injEq] at h
    simp only [yonedaPresheaf, unop_op]
    ext x
    obtain ⟨y, hy⟩ := (hq Z B π).surjective x
    rw [← hy]
    exact congr_fun h y

Goal state after:
case refine_2
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 π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
x✝ :
  (fun X ↦ X)
    ↑{x |
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
          (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
a : (yonedaPresheaf G X).obj (op Z)
ha :
  a ∈
    {x |
      (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op)) x =
        (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op)) x}
⊢ ∃ a_1,
    (ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)) a_1 = ⟨a, ha⟩