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

Goal state before:
pp: case zero
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S ((Stmt.move d)^[0] q) = SupportsStmt S q

Tactic:
simp only [*, iterate]

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

Goal state before:
pp: case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
n✝ : ℕ
a✝ : ∀ {q : Stmt Bool (Λ' Γ Λ σ) σ}, SupportsStmt S ((Stmt.move d)^[n✝] q) = SupportsStmt S q
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S ((Stmt.move d)^[n✝ + 1] q) = SupportsStmt S q

Tactic:
simp only [*, iterate]

Goal state after:
case succ
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
S : Finset (Λ' Γ Λ σ)
d : Dir
n✝ : ℕ
a✝ : ∀ {q : Stmt Bool (Λ' Γ Λ σ) σ}, SupportsStmt S ((Stmt.move d)^[n✝] q) = SupportsStmt S q
q : Stmt Bool (Λ' Γ Λ σ) σ
⊢ SupportsStmt S (Stmt.move d q) = SupportsStmt S q
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ (addBottom L).head.1 = true

Tactic:
rw [addBottom, ListBlank.head_cons]

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

Goal state before:
pp: case rfind
n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
IHf : ∃ c, ∀ (v : List.Vector ℕ (n + 1)), c.eval ↑v = pure <$> ↑f v
⊢ ∃ c,
    ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> (fun v ↦ Nat.rfind fun n_1 ↦ Part.some (decide (f (n_1 ::ᵥ v) = 0))) v

Tactic:
| @rfind n f _ IHf =>

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

Goal state before:
pp: c : Code
h : c.Ok
v : List ℕ
⊢ StateTransition.eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v

Tactic:
by
  rw [h, ← bind_pure_comp]; congr; funext v
  exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.single rfl, rfl⟩)

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

Goal state before:
pp: case refine_1.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝¹ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst✝ : Inhabited Λ
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct K Γ σ k✝
q✝ : TM2.Stmt Γ Λ σ
IH :
  TM2.SupportsStmt S q✝ →
    (∀ x ∈ trStmts₁ q✝, x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧ ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ' K Γ Λ σ), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ l' ∈ trStmts₁ q✝, TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ' K Γ Λ σ
h : l ∈ trStmts₁ q✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)

Tactic:
· exact IH₂ _ h

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

Goal state before:
pp: case fix
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet (Cont.fix f k) v) = Cfg.halt <$> (Cont.fix f k).eval v

Tactic:
rw [Cont.eval, stepRet]; simp only
    split_ifs; · exact IH
    simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)]
    congr; funext; rw [bind_pure_comp, ← IH]
    exact reaches_eval (ReflTransGen.single rfl)

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

Goal state before:
pp: X Y : Profinite
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ᶜ
⊢ y ∉ C

Tactic:
rintro ⟨y', hy'⟩

Goal state after:
X Y : Profinite
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ᶜ
y' : (fun X ↦ ↑X.toTop) X
hy' : (ConcreteCategory.hom f) y' = y
⊢ False
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: case mp
X Y : Profinite
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
⊢ False

Tactic:
have hUy : U ∈ 𝓝 y := hC.compl_mem_nhds hyU

Goal state after:
case mp
X Y : Profinite
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
⊢ False
Module: Mathlib.Topology.Category.Profinite.Basic

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

Tactic:
constructor
  · dsimp [Function.Surjective]
    contrapose!
    rintro ⟨y, hy⟩ hf
    let C := Set.range f
    have hC : IsClosed C := (isCompact_range f.hom.hom.continuous).isClosed
    let U := Cᶜ
    have hyU : y ∈ U := by
      refine Set.mem_compl ?_
      rintro ⟨y', hy'⟩
      exact hy y' hy'
    have hUy : U ∈ 𝓝 y := hC.compl_mem_nhds hyU
    obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_isClopen.mem_nhds_iff.mp hUy
    classical
      let Z := of (ULift.{u} <| Fin 2)
      let g : Y ⟶ Z := ofHom _
        ⟨(LocallyConstant.ofIsClopen hV).map ULift.up, LocallyConstant.continuous _⟩
      let h : Y ⟶ Z := ofHom _ ⟨fun _ => ⟨1⟩, continuous_const⟩
      have H : h = g := by
        rw [← cancel_epi f]
        ext x
        dsimp [g, LocallyConstant.ofIsClopen]
        rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, ConcreteCategory.hom_ofHom,
          ContinuousMap.coe_mk, Function.comp_apply, if_neg]
        refine mt (fun α => hVU α) ?_
        simp [U, C]
      apply_fun fun e => (e y).down at H
      dsimp [g, LocallyConstant.ofIsClopen] at H
      rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Function.comp_apply, if_pos hyV] at H
      exact top_ne_bot H
  · rw [← CategoryTheory.ofHom_epi_iff_surjective]
    apply (forget Profinite).epi_of_epi_map

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos.refine_2
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
C_chain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) C
hC : Nonempty ↑C
a : A
c : ↑C
⊢ (↑c ∩ X ⁻¹' {a}).Nonempty

Tactic:
rw [← image_inter_nonempty_iff, (C_sub c.mem).right, univ_inter]
      exact singleton_nonempty a

Goal state after:
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)
U : Set ↑(⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
hU : IsOpen U
⊢ IsOpen (closure U)

Tactic:
by
    have h : IsClopen (i ⁻¹' (Set.range f)) :=
      ⟨IsClosed.preimage i.hom.hom.continuous (isCompact_range f.hom.hom.continuous).isClosed,
        IsOpen.preimage i.hom.hom.continuous hi.isOpen_range⟩
    rw [← (closure U).preimage_image_eq Subtype.coe_injective,
      ← h.1.isClosedEmbedding_subtypeVal.closure_image_eq U]
    exact isOpen_induced (ExtremallyDisconnected.open_closure _
      (h.2.isOpenEmbedding_subtypeVal.isOpenMap U hU))

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

Goal state before:
pp: X : Stonean
⊢ ∀ {E X_1 : CompHaus} (f : toCompHaus.obj X ⟶ X_1) (e : E ⟶ X_1) [Epi e], ∃ f', f' ≫ e = f

Tactic:
intro B C φ f _

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
⊢ ∀ {E X_1 : Profinite} (f : toProfinite.obj X ⟶ X_1) (e : E ⟶ X_1) [Epi e], ∃ f', f' ≫ e = f

Tactic:
intro B C φ f _

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 : Stonean
⊢ ∀ {E X_1 : Stonean} (f : X ⟶ X_1) (e : E ⟶ X_1) [Epi e], ∃ f', f' ≫ e = f

Tactic:
intro B C φ f _

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

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

Tactic:
exact fun ⟨y, h⟩ ↦ ⟨d.proj y, by ext; simp [h, proj, Quotient.eq]⟩

Goal state after:
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: case refine_2
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ inst✝³ = generateFrom {s | IsClopen s}

Tactic:
apply IsTopologicalBasis.eq_generateFrom
    exact loc_compact_Haus_tot_disc_of_zero_dim

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

Goal state before:
pp: case cons₁.refine_2.refine_5.refine_2
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    { l := some (trNormal fs (trCont k).cons₂), var := none,
      stk :=
        update
          (update
            (update
              (update (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
                ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
              main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main))
            aux (none.elim id List.cons []))
          stack
          (update
              (update (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
                ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
              main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) aux ++
            update
              (update (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
                ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
              main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) stack) }
    s'

Tactic:
simp only [TM2.step, Option.mem_def, Option.elim, elim_update_stack, elim_main,
      List.append_nil, elim_update_main, id_eq, elim_update_aux,
      elim_aux, elim_stack]

Goal state after:
case cons₁.refine_2.refine_5.refine_2
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal fs (trCont (Cont.cons₂ v k))), var := none,
      stk := elim (trList as) [] [] (trContStack (Cont.cons₂ v k)) }
    s'
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some (trNormal fs (trCont k).cons₂), var := none,
      stk := elim (trList as) [] [] (trList v ++ Γ'.consₗ :: trLList (contStack k)) }
    s'
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: 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ᶜ
⊢ y ∉ C

Tactic:
rintro ⟨y', hy'⟩

Goal state after:
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ᶜ
y' : (fun X ↦ ↑X.toTop) X
hy' : (ConcreteCategory.hom f) y' = y
⊢ False
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
⊢ False

Tactic:
have hUy : U ∈ 𝓝 y := hC.compl_mem_nhds hyU

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
⊢ False
Module: Mathlib.Condensed.Epi

Goal state before:
pp: A : Type u'
inst✝⁹ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁸ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁷ : ConcreteCategory A FA
inst✝⁶ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁵ : PreservesFiniteProducts (CategoryTheory.forget A)
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝³ : (extensiveTopology Stonean).WEqualsLocallyBijective A
inst✝² : HasSheafify (extensiveTopology Stonean) A
inst✝¹ : (extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)
inst✝ : Balanced (Sheaf (extensiveTopology Stonean) A)
⊢ Epi f ↔ ∀ (S : Stonean), Function.Surjective ⇑(hom (f.hom.app (op S.compHaus)))

Tactic:
← (StoneanCompHaus.equivalence A).inverse.epi_map_iff_epi,

Goal state after:
A : Type u'
inst✝⁹ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁸ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁷ : ConcreteCategory A FA
inst✝⁶ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁵ : PreservesFiniteProducts (CategoryTheory.forget A)
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝³ : (extensiveTopology Stonean).WEqualsLocallyBijective A
inst✝² : HasSheafify (extensiveTopology Stonean) A
inst✝¹ : (extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)
inst✝ : Balanced (Sheaf (extensiveTopology Stonean) A)
⊢ Epi ((StoneanCompHaus.equivalence A).inverse.map f) ↔
    ∀ (S : Stonean), Function.Surjective ⇑(hom (f.hom.app (op S.compHaus)))
Module: Mathlib.Topology.Category.Sequential

Goal state before:
pp: X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : SequentialSpace X✝
X Y : Sequential
f : ↑X.toTop ≃ₜ ↑Y.toTop
x : ↑Y.toTop
⊢ (ConcreteCategory.hom
        (InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ }) ≫
          InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f, continuous_toFun := ⋯ })))
      x =
    (ConcreteCategory.hom (𝟙 Y)) x

Tactic:
exact f.apply_symm_apply x

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g

Tactic:
have D_clopen i : IsClopen (D i) := IsClopen.preimage (isClopen_discrete {f' i}) hg'

Goal state after:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g
Module: Mathlib.Topology.Category.CompactlyGenerated

Goal state before:
pp: X✝ : Type w
inst✝¹ : TopologicalSpace X✝
inst✝ : UCompactlyGeneratedSpace X✝
X Y : CompactlyGenerated
f : ↑X.toTop ≃ₜ ↑Y.toTop
x : ↑Y.toTop
⊢ (ConcreteCategory.hom
        (ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ } ≫ ofHom { toFun := ⇑f, continuous_toFun := ⋯ }))
      x =
    (ConcreteCategory.hom (𝟙 Y)) x

Tactic:
exact f.apply_symm_apply x

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

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := fun n ↦ { k // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) := fun n k ↦ ⟨⋯.choose, ⋯⟩
k_seq : (n : ℕ) → lifts n := fun n ↦ Nat.rec ⟨k0, h_down0⟩ next n
h_down : ∀ (n : ℕ), f ≫ ↑(k_seq n) = g ≫ lightToProfinite.map (S.proj n)
h_up : ∀ (n : ℕ), ↑(k_seq (n + 1)) ≫ lightToProfinite.map (S.transitionMap n) = ↑(k_seq n)
⊢ ∃ h, f ≫ h = g

Tactic:
let k_cone : Cone (S.diagram ⋙ lightToProfinite) :=
      { pt := Y, π := NatTrans.ofOpSequence (fun n ↦ (k_seq n).val) (fun n ↦ (h_up n).symm) }

Goal state after:
S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := fun n ↦ { k // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) := fun n k ↦ ⟨⋯.choose, ⋯⟩
k_seq : (n : ℕ) → lifts n := fun n ↦ Nat.rec ⟨k0, h_down0⟩ next n
h_down : ∀ (n : ℕ), f ≫ ↑(k_seq n) = g ≫ lightToProfinite.map (S.proj n)
h_up : ∀ (n : ℕ), ↑(k_seq (n + 1)) ≫ lightToProfinite.map (S.transitionMap n) = ↑(k_seq n)
k_cone : Cone (S.diagram ⋙ lightToProfinite) := { pt := Y, π := NatTrans.ofOpSequence (fun n ↦ ↑(k_seq n)) ⋯ }
⊢ ∃ h, f ≫ h = g
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case binaturality
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ η✝.app (bicompl t F G β✝ β'✝) (bitraverse (traverse f✝) (traverse f'✝) x✝) =
    bitraverse (traverse (η✝.app β✝ ∘ f✝)) (traverse (η✝.app β'✝ ∘ f'✝)) x✝

Tactic:
dsimp only [bicompl]
    simp [binaturality, naturality_pf]

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

Goal state before:
pp: σ : Type u
G : Type u → Type u
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
x : σ ⊕ α
⊢ Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x

Tactic:
cases x <;> simp [Sum.traverse, functor_norm] <;> rfl

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : StateT σ m α) (next : Label ω (StateT σ m) γ → α → StateT σ m ω),
    (callCC fun f ↦ cmd >>= next f) = do
      let x ← cmd
      callCC fun f ↦ next f x

Tactic:
intros
    simp only [callCC, StateT.callCC, StateT.run_bind, callCC_bind_right]; ext; rfl

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
f : Option α✝
⊢ Option.map (⇑e.symm) (Option.map (⇑e) f) = f

Tactic:
by cases f <;> simp

Goal state after:
Module: Mathlib.Control.ULiftable

Goal state before:
pp: s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
f : Option β✝
⊢ Option.map (⇑e) (Option.map (⇑e.symm) f) = f

Tactic:
by cases f <;> simp

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

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : T2Space S
inst✝³ : TopologicalSpace T
inst✝² : CompactSpace T
inst✝¹ : TopologicalSpace X
inst✝ : T1Space (OnePoint X)
π : T → S × OnePoint X
hπ : Continuous π
⊢ CompactSpace ↑(S' π)

Tactic:
rw [← isCompact_iff_compactSpace, show S' π =
    ⋂ (n : OnePoint X) (m : OnePoint X), {x | (π (x n).val).1 = (π (x m).val).1} by aesop]
  have (x : OnePoint X) : CompactSpace <| (Prod.snd ∘ π) ⁻¹' {x} :=
    isCompact_iff_compactSpace.mp (IsClosed.preimage (by fun_prop) isClosed_singleton).isCompact
  refine (isClosed_iInter fun n ↦ isClosed_iInter fun m ↦ isClosed_eq ?_ ?_).isCompact
  all_goals fun_prop

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

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝² : Traversable t
inst✝¹ : LawfulTraversable t
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α✝ β✝ : Type u
x✝¹ : α✝ → β✝
x✝ : t' α✝
⊢ traverse (pure ∘ x✝¹) x✝ = pure (x✝¹ <$> x✝)

Tactic:
by rw [h₂, Equiv.traverse_eq_map_id, h₀]

Goal state after: