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

Goal state before:
pp: case pos
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
k' : K
i : ℕ
h' : k' = k
⊢ (if i = (S k).length then update (L.nth i) k (some (f v)) else L.nth i) k' =
    (ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse).nth i

pp: case neg
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
k' : K
i : ℕ
h' : ¬k' = k
⊢ (if i = (S k).length then update (L.nth i) k (some (f v)) else L.nth i) k' =
    (ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse).nth i

Tactic:
· subst k'
      split_ifs with h
        <;> simp only [List.reverse_cons, Function.update_self, ListBlank.nth_mk, List.map]
      · rw [List.getI_eq_getElem _, List.getElem_append_right] <;>
        simp only [List.length_append, List.length_reverse, List.length_map, ← h,
          Nat.sub_self, List.length_singleton, List.getElem_singleton,
          le_refl, Nat.lt_succ_self]
      rw [← proj_map_nth, hL, ListBlank.nth_mk]
      rcases lt_or_gt_of_ne h with h | h
      · rw [List.getI_append]
        simpa only [List.length_map, List.length_reverse] using h
      · rw [List.getI_eq_default, List.getI_eq_default] <;>
          simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse,
            List.length_append, List.length_map]

Goal state after:
case neg
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
k' : K
i : ℕ
h' : ¬k' = k
⊢ (if i = (S k).length then update (L.nth i) k (some (f v)) else L.nth i) k' =
    (ListBlank.mk (List.map some (update S k (f v :: S k) k')).reverse).nth i
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case neg
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
n : ℕ
h2 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: ↑v)
IH :
  ∀ (a'' : List ℕ),
    (Sum.inr a'' ∈
        (cf.eval (n :: ↑v)).bind fun y ↦
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
            else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))) →
      ∀ (n : ℕ),
        a'' = n :: ↑v →
          (∀ m < n, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : ¬[f (n ::ᵥ v)].headI = 0
this :
  Sum.inl v' ∈ Part.some (Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∧
        v' ∈
          PFun.fix
            (fun v ↦
              (cf.eval v).bind fun y ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            a'
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
refine IH (n.succ::v.val) (by simp_all) _ rfl fun m h' => ?_
        obtain h | rfl := Nat.lt_succ_iff_lt_or_eq.1 h'
        exacts [hm _ h, h]

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P✝ : TopCat → Prop
α : Type w
inst✝² : Finite α
X : α → CompHausLike P✝
inst✝¹ : HasExplicitFiniteCoproduct X
P : TopCat → Prop
inst✝ : HasExplicitFiniteCoproducts P
P' : TopCat → Prop
h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop
⊢ PreservesFiniteCoproducts (toCompHausLike h)

Tactic:
by
  have : PreservesFiniteCoproducts (toCompHausLike h ⋙ compHausLikeToTop P') :=
    inferInstanceAs (PreservesFiniteCoproducts (compHausLikeToTop _))
  exact preservesFiniteCoproducts_of_reflects_of_preserves (toCompHausLike h) (compHausLikeToTop P')

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ CompactT2.Projective (StoneCech X)

Tactic:
by
  intro Y Z _tsY _tsZ _csY _t2Y _csZ _csZ f g hf hg g_sur
  let s : Z → Y := fun z => Classical.choose <| g_sur z
  have hs : g ∘ s = id := funext fun z => Classical.choose_spec (g_sur z)
  let t := s ∘ f ∘ stoneCechUnit
  have ht : Continuous t := continuous_of_discreteTopology
  let h : StoneCech X → Y := stoneCechExtend ht
  have hh : Continuous h := continuous_stoneCechExtend ht
  refine ⟨h, hh, denseRange_stoneCechUnit.equalizer (hg.comp hh) hf ?_⟩
  rw [comp_assoc, stoneCechExtend_extends ht, ← comp_assoc, hs, id_comp]

Goal state after:
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
inst✝ : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
X₁ : ↑D → A := Prod.fst ∘ Subtype.val
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : X₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X₁ '' E₀ ≠ univ
ρ : ↑E → A := E.domRestrict X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : ↑D → B := Prod.snd ∘ Subtype.val
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Tactic:
have X₂_cont : Continuous X₂ := continuous_snd.comp continuous_subtype_val

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
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x | φ x.1 = f x.2}
D_comp : CompactSpace ↑D
X₁ : ↑D → A := Prod.fst ∘ Subtype.val
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set ↑D
left✝ : CompactSpace ↑E
E_onto : X₁ '' E = univ
E_min : ∀ (E₀ : Set ↑E), E₀ ≠ univ → IsClosed E₀ → E.domRestrict X₁ '' E₀ ≠ univ
ρ : ↑E → A := E.domRestrict X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : ↑E ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : ↑D → B := Prod.snd ∘ Subtype.val
X₂_cont : Continuous X₂
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
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)
a✝ : IsOpen U
⊢ IsOpen (Sigma.mk i '' U)

Tactic:
rw [isOpen_sigma_iff]

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
⊢ ∀ (i_1 : ι), IsOpen (Sigma.mk i_1 ⁻¹' Sigma.mk i '' U)
Module: Mathlib.Topology.Category.Stonean.EffectiveEpi

Goal state before:
pp: α : Type
inst✝ : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
tfae_2_to_1 : Epi (Sigma.desc π) → EffectiveEpiFamily X π
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
⊢ (EffectiveEpiFamily (fun a ↦ toCompHaus.obj (X a)) fun a ↦ toCompHaus.map (π a)) ↔ EffectiveEpiFamily X π

Tactic:
exact ⟨fun h ↦ Stonean.toCompHaus.finite_effectiveEpiFamily_of_map _ _ h,
      fun _ ↦ inferInstance⟩

Goal state after:
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 by_cases hx : x ∈ A <;> simp [hx, h.1, h.2, ← compl_ofPred]

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
S : Cone F
x✝ : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = S.π.app j
⊢ lightProfiniteToCompHaus.map x✝ =
    lightProfiniteToCompHaus.map
      (ConcreteCategory.ofHom
        (TopCat.Hom.hom
          ((CompHaus.limitConeIsLimit (F ⋙ lightProfiniteToCompHaus)).lift (lightProfiniteToCompHaus.mapCone S)).hom))

Tactic:
apply (CompHaus.limitConeIsLimit.{v, u} _).uniq (lightProfiniteToCompHaus.mapCone S)

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
S : Cone F
x✝ : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = S.π.app j
⊢ ∀ (j : J),
    lightProfiniteToCompHaus.map x✝ ≫ (CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app j =
      (lightProfiniteToCompHaus.mapCone S).π.app j
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3.refine_2.mp
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
hx : x ∈ U
s : ↑S
hs : s ∈ G
hh : x ∈ (fun h ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) hs
⊢ x ∈ ⇑(ConcreteCategory.hom (C.π.app j0 ≫ F.map (f s ⋯))) ⁻¹' V s

Tactic:
C.w

Goal state after:
case refine_3.refine_2.mp
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
hx : x ∈ U
s : ↑S
hs : s ∈ G
hh : x ∈ (fun h ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) hs
⊢ x ∈ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3.refine_2.mpr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
s : ↑S
hs : s ∈ G
hx : x ∈ ⇑(ConcreteCategory.hom (C.π.app j0 ≫ F.map (f s ⋯))) ⁻¹' V s
⊢ x ∈ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s

Tactic:
C.w

Goal state after:
case refine_3.refine_2.mpr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
G : Finset ↑S
hG : U ⊆ ⋃ i ∈ G, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
j0 : J
hj0 : ∀ {X : J}, X ∈ Finset.image j G → Nonempty (j0 ⟶ X)
f : (s : ↑S) → s ∈ G → (j0 ⟶ j s) := fun s hs ↦ ⋯.some
W : ↑S → Set ↑(F.obj j0).toTop :=
  fun s ↦ if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ
x : ↑C.pt.toTop
s : ↑S
hs : s ∈ G
hx : x ∈ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
⊢ x ∈ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
Module: Mathlib.Logic.Function.FiberPartition

Goal state before:
pp: Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : ↑↑a
this : (fun x ↦ f ⁻¹' {↑x}) (Exists.choose ⋯) = ↑a
⊢ f ↑x = image f a

Tactic:
rw [← Set.mem_singleton_iff, ← Set.mem_preimage]

Goal state after:
Y : Type u_2
Z : Type u_3
f : Y → Z
a : Fiber f
x : ↑↑a
this : (fun x ↦ f ⁻¹' {↑x}) (Exists.choose ⋯) = ↑a
⊢ ↑x ∈ f ⁻¹' {image f a}
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case intro
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y ↦ if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toTop) (Fin 2) := (LocallyConstant.map ι f).flip
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a ↦ ⋯.some
gg : α → LocallyConstant (↑(F.obj j0).toTop) (Fin 2) :=
  fun a ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant (↑(F.obj j0).toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : ↑C.pt.toTop
⊢ (LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)) x =
    (g a) ((ConcreteCategory.hom (C.π.app j0 ≫ F.map (fs a))) x)

Tactic:
C.w

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
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a ↦ ⋯.some
gg : α → LocallyConstant (↑(F.obj j0).toTop) (Fin 2) :=
  fun a ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant (↑(F.obj j0).toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : ↑C.pt.toTop
⊢ (LocallyConstant.comap (TopCat.Hom.hom (C.π.app (j a)).hom) (g a)) x =
    (g a) ((ConcreteCategory.hom (C.π.app (j a))) x)
Module: Mathlib.Condensed.Light.TopCatAdjunction

Goal state before:
pp: X✝ Y : LightCondSet
f✝ : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
f : ℕ → ↑X
p : ↑X
h : Filter.Tendsto f Filter.atTop (nhds p)
g : OnePoint ℕ → ↑X.toLightCondSet.toTopCat :=
  (topCatAdjunctionCounitEquiv X).invFun ∘ ⇑(OnePoint.continuousMapMkNat f p h)
⊢ Continuous g

Tactic:
let x : X.toLightCondSet.obj.obj ⟨(ℕ∪{∞})⟩ := OnePoint.continuousMapMkNat f p h

Goal state after:
X✝ Y : LightCondSet
f✝ : X✝ ⟶ Y
X : TopCat
inst✝ : SequentialSpace ↑X
f : ℕ → ↑X
p : ↑X
h : Filter.Tendsto f Filter.atTop (nhds p)
g : OnePoint ℕ → ↑X.toLightCondSet.toTopCat :=
  (topCatAdjunctionCounitEquiv X).invFun ∘ ⇑(OnePoint.continuousMapMkNat f p h)
x : X.toLightCondSet.obj.obj (Opposite.op ℕ∪{∞}) := OnePoint.continuousMapMkNat f p h
⊢ Continuous g
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (c.π.app (Opposite.op 0))

Tactic:
apply Functor.epi_of_epi_map (forget R)

Goal state after:
R : Type u_1
inst✝ : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi ((forget R).map (c.π.app (Opposite.op 0)))
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type u_1
x✝ : Const α✝ β✝
⊢ bitraverse pure pure x✝ = pure x✝

Tactic:
simp [bitraverse, Const.bitraverse, functor_norm]

Goal state after:
case id_bitraverse
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ β✝ : Type u_1
x✝ : Const α✝ β✝
⊢ pure x✝ = pure x✝
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u_1
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : Const α✝ α'✝
⊢ bitraverse (Comp.mk ∘ map f✝ ∘ g✝) (Comp.mk ∘ map f'✝ ∘ g'✝) x✝ = Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)

Tactic:
simp [bitraverse, Const.bitraverse, functor_norm]

Goal state after:
case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u_1
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : Const α✝ α'✝
⊢ (Comp.mk ∘ map f✝ ∘ g✝) x✝ = Comp.mk (f✝ <$> g✝ x✝)
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : Const α✝ α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)

Tactic:
simp [bitraverse, Const.bitraverse, functor_norm]

Goal state after:
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : Const α✝ α'✝
⊢ (pure ∘ f✝) x✝ = pure (bimap f✝ f'✝ x✝)
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : Const α✝ α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ x✝) = bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) x✝

Tactic:
simp [bitraverse, Const.bitraverse, functor_norm]

Goal state after:
case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F : Type u → Type u
inst✝⁴ : Applicative F
F✝ G✝ : Type u_1 → Type u_1
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u_1
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : Const α✝ α'✝
⊢ η✝.app (Const β✝ β'✝) (f✝ x✝) = (η✝.app β✝ ∘ f✝) x✝
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.3
⊢ ⇑(Equiv.refl α).uniqueCongr = id

Tactic:
by simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: ⊢ ∀ {α β γ : Type ?u.3} (k : α ≃ β) (h : β ≃ γ), ⇑(k.trans h).uniqueCongr = ⇑h.uniqueCongr ∘ ⇑k.uniqueCongr

Tactic:
by simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: ⊢ ∀ {α β γ : Type ?u.4} (k : α ≃ β) (h : β ≃ γ),
    (fun x ↦ Fintype.ofBijective ⇑(k.trans h) ⋯) = (fun x ↦ Fintype.ofBijective ⇑h ⋯) ∘ fun x ↦ Fintype.ofBijective ⇑k ⋯

Tactic:
by simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: α β : Type u_1
f : α → β
x : Option α
⊢ Option.traverse (pure ∘ f) x = pure (f <$> x)

Tactic:
by cases x <;> rfl

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

Goal state before:
pp: σ α : Type u_1
x : σ ⊕ α
⊢ Sum.traverse pure x = x

Tactic:
by cases x <;> rfl

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

Goal state before:
pp: case none
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
⊢ ∃ a, (fun x ↦ π ↑x) a = (s, none)

Tactic:
obtain ⟨y, hy⟩ := hπ (s, none)
    exact ⟨⟨y, by grind⟩, hy⟩

Goal state after: