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

Goal state before:
pp: a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' = elim a b' c d

Tactic:
by
  funext x; cases x <;> rfl

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

Goal state before:
pp: a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' = elim a b c' d

Tactic:
by
  funext x; cases x <;> rfl

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
⊢ x ∈ U → IsOpen[inst✝³] U → ∃ v ∈ fun U ↦ IsClosed[inst✝³] U ∧ IsOpen[inst✝³] U, x ∈ v ∧ v ⊆ U

Tactic:
hxU

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
⊢ IsOpen[inst✝³] U → ∃ v ∈ fun U ↦ IsClosed[inst✝³] U ∧ IsOpen[inst✝³] U, x ∈ v ∧ v ⊆ U
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: α : Type u_1
p : α → Bool
a : α
L l₁ : List α
o : Option α
l₂ : List α
h₁ : ∀ x ∈ l₁, p x = false
h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) o
⊢ splitAtPred p (a :: L) = (l₁, o, l₂)

Tactic:
rw [splitAtPred]
    have IH := splitAtPred_eq p L
    rcases o with - | o
    · rcases l₁ with - | ⟨a', l₁⟩ <;> rcases h₂ with ⟨⟨⟩, rfl⟩
      rw [h₁ a (List.Mem.head _), cond, IH L none [] _ ⟨rfl, rfl⟩]
      exact fun x h => h₁ x (List.Mem.tail _ h)
    · rcases l₁ with - | ⟨a', l₁⟩ <;> rcases h₂ with ⟨h₂, ⟨⟩⟩
      · rw [h₂, cond]
      rw [h₁ a (List.Mem.head _), cond, IH l₁ (some o) l₂ _ ⟨h₂, _⟩] <;> try rfl
      exact fun x h => h₁ x (List.Mem.tail _ h)

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

Goal state before:
pp: case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal g (Cont.comp f k) v) k v) = do
    let v ← (f.comp g).eval v
    eval step (Cfg.ret k v)

Tactic:
| comp f g IHf IHg =>

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

Goal state before:
pp: case fix
f : Code
IHf : f.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v ↦ stepNormal f (Cont.fix f k) v) k v) = do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)

Tactic:
cont_eval_fix IHf

Goal state after:
case fix
f : Code
IHf : f.Ok
k : Cont
v : List ℕ
⊢ (do
      let v ← f.fix.eval v
      eval step (Cfg.ret k v)) =
    do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)
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ᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
⊢ h = g

Tactic:
← cancel_epi f

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ᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
⊢ f ≫ h = f ≫ g
Module: Mathlib.Topology.ExtremallyDisconnected

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

Tactic:
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.Category.Stonean.Limits

Goal state before:
pp: X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ HasExplicitPullbacksOfInclusions fun Y ↦ ExtremallyDisconnected ↑Y

Tactic:
apply CompHausLike.hasPullbacksOfInclusions

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 Y : Stonean
f : X ⟶ Y
h✝ : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
⊢ h = g

Tactic:
← cancel_epi f

Goal state after:
X Y : Stonean
f : X ⟶ Y
h✝ : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
⊢ f ≫ h = f ≫ g
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
toSetoid✝¹ : Setoid X
isOpen_setOfPred_rel✝¹ : ∀ (x : X), IsOpen[inst✝] (ofPred (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOfPred_rel✝ : ∀ (x : X), IsOpen[inst✝] (ofPred (toSetoid✝ x))
x✝ :
  { toSetoid := toSetoid✝¹, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝¹ }.toSetoid =
    { toSetoid := toSetoid✝, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝ }.toSetoid
⊢ { toSetoid := toSetoid✝¹, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝¹ } =
    { toSetoid := toSetoid✝, isOpen_setOfPred_rel := isOpen_setOfPred_rel✝ }

Tactic:
by congr

Goal state after:
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ Injective (finsetClopens X)

Tactic:
by
  apply Function.Injective.of_comp (f := Set.image (fun (t : Clopens X) ↦ t.carrier) ∘ (↑))
  rw [comp_finsetClopens]
  intro ⟨_, _⟩ ⟨_, _⟩ h
  congr
  rw [Setoid.classes_inj]
  exact h

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_3.mpr.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
this :
  ∀ (S : Set (Set ↑(F.obj j))) (E : Finset J) (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S → (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ E, P e ∈ S) → ⋂ e ∈ E, P e ∈ S
e : J
he : e ∈ G
⊢ (if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ) ∈ T j

Tactic:
dif_pos he

Goal state after:
case e'_3.mpr.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
this :
  ∀ (S : Set (Set ↑(F.obj j))) (E : Finset J) (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S → (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ E, P e ∈ S) → ⋂ e ∈ E, P e ∈ S
e : J
he : e ∈ G
⊢ ⇑(ConcreteCategory.hom (F.map (g e he))) ⁻¹' U e ∈ T j
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3.refine_1
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
s : ↑S
hs : s ∈ G
⊢ IsClopen (if hs : s ∈ G then ⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V s else Set.univ)

Tactic:
dif_pos hs

Goal state after:
case refine_3.refine_1
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
s : ↑S
hs : s ∈ G
⊢ IsClopen (⇑(ConcreteCategory.hom (F.map (f s hs))) ⁻¹' V 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ᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : LightProfinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
⊢ h = g

Tactic:
← cancel_epi f

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ᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : LightProfinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
⊢ f ≫ h = f ≫ g
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: case refine_1
S : LightDiagram
⊢ Countable ((n : ℕ) × LocallyConstant (↑((S.diagram ⋙ toProfinite).obj (op n)).toTop) (Fin 2))

pp: case refine_2
S : LightDiagram
⊢ (n : ℕ) × LocallyConstant (↑((S.diagram ⋙ toProfinite).obj (op n)).toTop) (Fin 2) →
    LocallyConstant (↑S.cone.pt.toTop) (Fin 2)

pp: case refine_3
S : LightDiagram
⊢ Function.Surjective ?refine_2

Tactic:
· 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

Goal state after:
case refine_2
S : LightDiagram
⊢ (n : ℕ) × LocallyConstant (↑((S.diagram ⋙ toProfinite).obj (op n)).toTop) (Fin 2) →
    LocallyConstant (↑S.cone.pt.toTop) (Fin 2)

case refine_3
S : LightDiagram
⊢ Function.Surjective ?refine_2
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
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
let ff : S → α := f.lift

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case comp
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.comp g) k ⊆ S
⊢ Supports (codeSupp' (f.comp g) k) S

Tactic:
| comp f g IHf IHg =>

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

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology LightProfinite) (Type u)).Faithful
this : (constantSheaf (coherentTopology LightProfinite) (Type u)).Full
⊢ LightCondSet.LocallyConstant.functor.essImage
    ((sheafCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))

Tactic:
exact obj_mem_essImage LightCondSet.LocallyConstant.functor M

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝¹ n : ℕ
α✝ : TypeVec.{u} n
p✝ : α✝ ⊗ α✝ ⟹ «repeat» n Prop
n✝ : ℕ
α : TypeVec.{u} (n✝ + 1)
p : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : (fun i ↦ { x // ofRepeat (p i (prod.mk i x.1 x.2)) }) Fin2.fz
⊢ ofRepeat (p Fin2.fz (prod.mk Fin2.fz (↑x).1 (↑x).2)) = p Fin2.fz ↑x

Tactic:
by congr

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝¹ n : ℕ
α✝ : TypeVec.{u} n
p✝ : α✝ ⊗ α✝ ⟹ «repeat» n Prop
n✝ : ℕ
α : TypeVec.{u} (n✝ + 1)
p : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p Fin2.fz
⊢ p Fin2.fz ↑x = ofRepeat (p Fin2.fz (prod.mk Fin2.fz (↑x).1 (↑x).2))

Tactic:
by congr

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

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
⊢ ∃ S' T' y' π' g',
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧ Epi (cover π')

Tactic:
let y' : LightProfinite.of (S' π) ⟶ S := ConcreteCategory.ofHom ⟨y π, y_continuous π⟩

Goal state after:
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
⊢ ∃ S' T' y' π' g',
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧ Epi (cover π')
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop :=
  fun n ↦
    ⇑(ConcreteCategory.hom
        (pullback.lift π (y' ▷ ℕ∪{∞}) (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
          (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
            (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n))
          ⋯))
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
⊢ ∃ S' T' y' π' g',
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧ Epi (cover π')

Tactic:
have hσ' (x : ℕ∪{∞}) (s : LightProfinite.of (S' π)) : (π' (σ' x s)).2 = x := rfl

Goal state after:
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop :=
  fun n ↦
    ⇑(ConcreteCategory.hom
        (pullback.lift π (y' ▷ ℕ∪{∞}) (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
          (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
            (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n))
          ⋯))
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
hσ' :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).2 = x
⊢ ∃ S' T' y' π' g',
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧ Epi (cover π')
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ #(f.support.dfinsupp ⇑f) = f.prod fun i ↦ ↑(#(f i))

Tactic:
card_dfinsupp

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ ∏ i ∈ f.support, #(f i) = f.prod fun i ↦ ↑(#(f i))
Module: Mathlib.Data.Semiquot

Goal state before:
pp: case e_s
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ s ∪ q.s = s

Tactic:
exact Set.union_eq_self_of_subset_right h

Goal state after:
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
⊢ recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) α = congr x✝ inst✝ ⋯ empty

Tactic:
by
  unfold recEmptyOption
  split
  · congr 1; exact Subsingleton.allEq _ _
  · exact Nat.noConfusion <| h.symm.trans ‹_›

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
l₁ : List (Sigma β)
h₁ : l₁.NodupKeys
l₂ : List (Sigma β)
nodupKeys✝ : l₂.NodupKeys
H : { entries := l₁, nodupKeys := h₁ }.entries = { entries := l₂, nodupKeys := nodupKeys✝ }.entries
⊢ { entries := l₁, nodupKeys := h₁ } = { entries := l₂, nodupKeys := nodupKeys✝ }

Tactic:
by congr

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this : DecidableEq α := Classical.decEq α
⊢ k ∈ s₂.keys

Tactic:
have := h (mem_lookup_iff.1 (Option.get_mem (lookup_isSome.2 hk)))

Goal state after:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : ⟨k, (lookup k s₁).get ⋯⟩ ∈ s₂.entries
⊢ k ∈ s₂.keys
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
l₁ : Multiset (Sigma β)
h₁ : l₁.NodupKeys
l₂ : Multiset (Sigma β)
nodupKeys✝ : l₂.NodupKeys
H : { entries := l₁, nodupKeys := h₁ }.entries = { entries := l₂, nodupKeys := nodupKeys✝ }.entries
⊢ { entries := l₁, nodupKeys := h₁ } = { entries := l₂, nodupKeys := nodupKeys✝ }

Tactic:
by congr

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s✝ : Finmap β
h : a' ≠ a
s : AList β
⊢ lookup a' (insert a b ⟦s⟧) = lookup a' ⟦s⟧

Tactic:
simp only [insert_toFinmap, lookup_toFinmap, lookup_insert_ne h]

Goal state after: