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

Goal state before:
pp: case refine_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux
      (tr
        ((fun x ↦
            Λ'.read fun s ↦ (if s = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) main) (unrev q))
          o))
      o
      (update
        (update (update (elim (trList L) [] c d) main (trList L.tail)) rev
          ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)))
        rev
        ((fun s ↦ ((fun x ↦ some Γ'.cons) s).getD default) o ::
          update (update (elim (trList L) [] c d) main (trList L.tail)) rev
            ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)) rev)))
    { l := some q, var := none, stk := elim (trList [L.headI]) [] c d }

Tactic:
tr

Goal state after:
case refine_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux
      (goto fun s ↦ (if s = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) main) (unrev q)) o
      (update
        (update (update (elim (trList L) [] c d) main (trList L.tail)) rev
          ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)))
        rev
        ((fun s ↦ ((fun x ↦ some Γ'.cons) s).getD default) o ::
          update (update (elim (trList L) [] c d) main (trList L.tail)) rev
            ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)) rev)))
    { l := some q, var := none, stk := elim (trList [L.headI]) [] c d }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case nil
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux
      (tr
        ((fun x ↦
            Λ'.read fun s ↦
              (if s = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) stack) (unrev q))
          (some Γ'.consₗ)))
      (some Γ'.consₗ)
      (update
        (update (update (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
          ([].reverseAux (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)))
        rev
        ((fun s ↦ ((fun x ↦ some Γ'.cons) s).getD default) (some Γ'.consₗ) ::
          update (update (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
            ([].reverseAux (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)) rev)))
    { l := some q, var := none, stk := elim (trList ([].headI :: L₁)) [] [] L₃ }

Tactic:
tr

Goal state after:
case nil
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    (TM2.stepAux
      (goto fun s ↦ (if s = some Γ'.consₗ then id else Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) stack) (unrev q))
      (some Γ'.consₗ)
      (update
        (update (update (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
          ([].reverseAux (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)))
        rev
        ((fun s ↦ ((fun x ↦ some Γ'.cons) s).getD default) (some Γ'.consₗ) ::
          update (update (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
            ([].reverseAux (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)) rev)))
    { l := some q, var := none, stk := elim (trList ([].headI :: L₁)) [] [] L₃ }
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pos.bit0
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih✝ :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ : List Γ'
⊢ { l := some (unrev q), var := some Γ'.bit0, stk := elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d } ∈
    some (TM2.stepAux (tr q.succ) s (elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d))

Tactic:
tr

Goal state after:
case pos.bit0
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih✝ :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ : List Γ'
⊢ { l := some (unrev q), var := some Γ'.bit0, stk := elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d } ∈
    some
      (TM2.stepAux
        (pop' main
          (branch (fun s ↦ decide (s = some Γ'.bit1)) (push rev (fun x ↦ Γ'.bit0) (goto fun x ↦ q.succ))
            (branch (fun s ↦ decide (s = some Γ'.cons))
              (push main (fun x ↦ Γ'.cons) (push main (fun x ↦ Γ'.bit1) (goto fun x ↦ unrev q)))
              (push main (fun x ↦ Γ'.bit1) (goto fun x ↦ unrev q)))))
        s (elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d))
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 (tr (q₁.pred q₂)) s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    { l := some q₂, var := none, stk := elim (Γ'.cons :: trList v) [] c d }

Tactic:
tr

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)
    (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 }
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
A : Set X
h : IsClopen A
x : X
⊢ IsOpen[inst✝²] (ofPred ((fun x y ↦ x ∈ A ↔ y ∈ A) x))

Tactic:
by_cases hx : x ∈ A <;> simp [hx, h.1, h.2, ← compl_ofPred]

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

Goal state before:
pp: X : Profinite
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone))

Tactic:
refine ⟨fun a b h => ?_, fun a => ?_⟩

Goal state after:
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

case refine_2
X : Profinite
a : (fun X ↦ ↑X.toTop) (limitCone X.diagram).pt
⊢ ∃ a_1, (ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone)) a_1 = a
Module: Mathlib.Topology.Category.Profinite.AsLimit

Goal state before:
pp: X : Profinite
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((limitConeIsLimit X.diagram).lift X.asLimitCone))

Tactic:
by
      refine ⟨fun a b h => ?_, fun a => ?_⟩
      · 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
      · obtain ⟨b, hb⟩ :=
          DiscreteQuotient.exists_of_compat (fun S => a.val S) fun _ _ h => a.prop (homOfLE h)
        use b
        -- ext S : 3 -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` does not work, replaced with following
        -- three lines.
        apply Subtype.ext
        apply funext
        rintro S
        -- Porting note: end replacement block
        apply hb

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

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

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨⟨effectiveEpiStruct f h⟩⟩⟩

Goal state after:
X Y : LightProfinite
f : X ⟶ Y
h : EffectiveEpi f
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)
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 (Cont'.fix f (trCont k)))) s (elim (trList v) [] [] (trContStack (Cont.fix f k)))) c

Tactic:
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 (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)) }

Tactic:
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.Topology.Category.LightProfinite.Basic

Goal state before:
pp: S : LightDiagram
⊢ SecondCountableTopology ↑S.cone.pt.toTop

Tactic:
rw [← TopologicalSpace.Clopens.countable_iff_secondCountable]
  refine @Countable.of_equiv _ _ ?_ (LocallyConstant.equivClopens (X := S.cone.pt))
  refine @Function.Surjective.countable
    (Σ (n : ℕ), LocallyConstant ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩) (Fin 2)) _ ?_ ?_ ?_
  · apply @instCountableSigma _ _ _ ?_
    intro n
    refine @Finite.to_countable _ ?_
    refine @Finite.of_injective _ ((S.diagram ⋙ FintypeCat.toProfinite).obj ⟨n⟩ → (Fin 2)) ?_ _
      LocallyConstant.coe_injective
    refine @Pi.finite _ _ ?_ _
    simp only [Functor.comp_obj]
    exact show (Finite (S.diagram.obj _)) from inferInstance
  · exact fun a ↦ a.snd.comap (S.cone.π.app ⟨a.fst⟩).hom.hom
  · intro a
    obtain ⟨n, g, h⟩ := Profinite.exists_locallyConstant S.cone S.isLimit a
    exact ⟨⟨unop n, g⟩, h.symm⟩

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 g,
    LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
have hff := fun a : α => exists_locallyConstant_fin_two _ hC (ff a)

Goal state after:
case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
hff : ∀ (a : α), ∃ j g, ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
⊢ ∃ j g,
    LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Module: Mathlib.Logic.Function.FiberPartition

Goal state before:
pp: Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
⊢ preimage f a ∈ ↑a

Tactic:
mem_iff_eq_image,

Goal state after:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
⊢ f (preimage f a) = image f a
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type ?u.19} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
⊢ TM2.SupportsStmt S (tr (Λ'.ret (Cont'.fix a✝¹ a✝)))

Tactic:
have R := @Finset.mem_union_right

Goal state after:
case fix
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type ?u.19} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
R : ∀ {α : Type ?u.21} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
⊢ TM2.SupportsStmt S (tr (Λ'.ret (Cont'.fix a✝¹ a✝)))
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
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
⊢ ι (f x) = ι h2.choose

pp: case inj
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
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
⊢ Function.Injective ι

Tactic:
· rw [h2.choose_spec]
    exact h1

Goal state after:
case inj
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
h1 : ι (f x) = gg ((ConcreteCategory.hom (C.π.app j)) x)
h2 : ∃ a, ι a = gg ((ConcreteCategory.hom (C.π.app j)) x)
⊢ Function.Injective ι
Module: Mathlib.Topology.Category.LightProfinite.AsLimit

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

Tactic:
apply Function.Surjective.of_comp (g := S.proj m)

Goal state after:
S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ Function.Surjective (⇑(ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(ConcreteCategory.hom (S.proj m)))
Module: Mathlib.Topology.Category.LightProfinite.Extend

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

Tactic:
simp [← Functor.map_comp]

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

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

Tactic:
exact trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) H)

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

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

Tactic:
exact trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) H)

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

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

Tactic:
exact trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) 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})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ (ConcreteCategory.hom (Y.map (sigmaIso f).hom.op ≫ (sigmaComparison Y fun a ↦ ↑(fiber f a).toTop) ≫ ↾fun g ↦ g a))
      ((ConcreteCategory.hom (counitAppApp S Y)) f) =
    counitAppAppImage f a

Tactic:
types_comp_apply

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})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ (ConcreteCategory.hom ((sigmaComparison Y fun a ↦ ↑(fiber f a).toTop) ≫ ↾fun g ↦ g a))
      ((ConcreteCategory.hom (Y.map (sigmaIso f).hom.op)) ((ConcreteCategory.hom (counitAppApp S Y)) f)) =
    counitAppAppImage f a
Module: Mathlib.Condensed.Discrete.Characterization

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

Tactic:
let e : CondensedSet.{u} ≌ Sheaf (coherentTopology Profinite) _ :=
    (Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).symm

Goal state after:
X : CondensedSet
h : (S : Profinite) → IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op)
e : CondensedSet ≌ Sheaf (coherentTopology Profinite) (Type (u + 1)) :=
  (Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).symm
⊢ LocallyConstant.functor.essImage X
Module: Mathlib.Topology.Category.LightProfinite.Sequence

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

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_eq_zero] at h
      assumption_mod_cast

Goal state after:
case refine_1.some.some
n m : ℕ
h : natUnionInftyEmbedding (Option.some n) = natUnionInftyEmbedding (Option.some m)
⊢ Option.some n = Option.some m
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
X Y : LightCondensed A
f : X ⟶ Y
⊢ IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : ToType (Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y

Tactic:
rw [coherentTopology.isLocallySurjective_iff,
    regularTopology.isLocallySurjective_iff]
  simp_rw [LightProfinite.effectiveEpi_iff_surjective]

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

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
X✝ Y✝ : LightProfiniteᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (lanPresheaf F).map x✝ ≫
      (match Y✝ with
        | Opposite.op S => lanPresheafIso (hF S)).hom =
    (match X✝ with
        | Opposite.op S => lanPresheafIso (hF S)).hom ≫
      F.map x✝

Tactic:
simp only [lanPresheaf, pointwiseLeftKanExtension_map,
    lanPresheafIso_hom, Opposite.op_unop]

Goal state after:
S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
X✝ Y✝ : LightProfiniteᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ colimit.desc (CostructuredArrow.proj toLightProfinite.op X✝ ⋙ toLightProfinite.op ⋙ F)
        { pt := colimit (CostructuredArrow.proj toLightProfinite.op Y✝ ⋙ toLightProfinite.op ⋙ F),
          ι :=
            {
              app := fun g ↦
                colimit.ι (CostructuredArrow.proj toLightProfinite.op Y✝ ⋙ toLightProfinite.op ⋙ F)
                  ((CostructuredArrow.map x✝).obj g),
              naturality := ⋯ } } ≫
      colimit.desc (CostructuredArrow.proj toLightProfinite.op Y✝ ⋙ toLightProfinite.op ⋙ F)
        (LightProfinite.Extend.cocone F (Opposite.unop Y✝)) =
    colimit.desc (CostructuredArrow.proj toLightProfinite.op X✝ ⋙ toLightProfinite.op ⋙ F)
        (LightProfinite.Extend.cocone F (Opposite.unop X✝)) ≫
      F.map x✝