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

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

Tactic:
rcases l₁ with - | ⟨a', l₁⟩

Goal state after:
case some.nil
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
o : α
h₁ : ∀ x ∈ [], p x = false
h₂ : Option.elim' (a :: L = [] ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = [] ++ a_1 :: l₂) (some o)
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    ([], some o, l₂)

case some.cons
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
o a' : α
l₁ : List α
h₁ : ∀ x ∈ a' :: l₁, p x = false
h₂ : Option.elim' (a :: L = a' :: l₁ ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = a' :: l₁ ++ a_1 :: l₂) (some o)
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a' :: l₁, some o, l₂)
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Profinite
j : J
⊢ ∀ ⦃Y : J⦄ (f : j ⟶ Y),
    ((Functor.const J).obj
              { toTop := (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop, is_compact := ⋯, is_hausdorff := ⋯,
                prop := ⋯ }).map
          f ≫
        InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app Y).hom =
      InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app j).hom ≫ F.map f

Tactic:
k

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Profinite
j k : J
⊢ ∀ (f : j ⟶ k),
    ((Functor.const J).obj
              { toTop := (CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop, is_compact := ⋯, is_hausdorff := ⋯,
                prop := ⋯ }).map
          f ≫
        InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app k).hom =
      InducedCategory.homMk ((CompHaus.limitCone (F ⋙ profiniteToCompHaus)).π.app j).hom ≫ F.map f
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case pos
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
x : X
hx : x ∈ U
⊢ ∃ a, f a = x

pp: case neg
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
x : X
hx : x ∉ U
⊢ ∃ a, f a = x

Tactic:
· exact ⟨⟨(x, false), Or.inr ⟨subset_closure hx, mem_singleton _⟩⟩, rfl⟩

Goal state after:
case neg
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := Uᶜ ×ˢ {true}
Z₂ : Set (X × Bool) := closure U ×ˢ {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : ↑Z → X := Prod.fst ∘ Subtype.val
f_cont : Continuous f
x : X
hx : x ∉ U
⊢ ∃ a, f a = x
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 ρ
a : A
⊢ ∃ a_1, ρ a_1 = a

Tactic:
by
    rcases (E_onto ▸ mem_univ a : a ∈ X₁ '' E) with ⟨d, ⟨hd, rfl⟩⟩; exact ⟨⟨d, hd⟩, rfl⟩

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

Goal state before:
pp: 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
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

Tactic:
induction E using Finset.induction_on with

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
j : J
⊢ ∀ ⦃Y : J⦄ (f : j ⟶ Y),
    ((Functor.const J).obj
              { toTop := (CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop, is_compact := ⋯,
                is_hausdorff := ⋯, prop := ⋯ }).map
          f ≫
        ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app Y).hom) =
      ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app j).hom) ≫
        F.map f

Tactic:
k

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : CountableCategory J
F : J ⥤ LightProfinite
j k : J
⊢ ∀ (f : j ⟶ k),
    ((Functor.const J).obj
              { toTop := (CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).pt.toTop, is_compact := ⋯,
                is_hausdorff := ⋯, prop := ⋯ }).map
          f ≫
        ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app k).hom) =
      ConcreteCategory.ofHom (TopCat.Hom.hom ((CompHaus.limitCone (F ⋙ lightProfiniteToCompHaus)).π.app j).hom) ≫
        F.map f
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
hx : x ∈ ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹' ⋃ s ∈ G, W s
⊢ x ∈ U

Tactic:
simp_rw [W, Set.preimage_iUnion, Set.mem_iUnion] at hx

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
hx :
  ∃ i,
    ∃ (_ : i ∈ G),
      x ∈
        ⇑(ConcreteCategory.hom (C.π.app j0)) ⁻¹'
          if h : i ∈ G then ⇑(ConcreteCategory.hom (F.map (f i ⋯))) ⁻¹' V i else Set.univ
⊢ x ∈ U
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) = gg ((ConcreteCategory.hom (C.π.app j)) x)

Tactic:
exact h1

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

Goal state before:
pp: S : LightProfinite
n : ℕ
⊢ ⇑(ConcreteCategory.hom (S.transitionMap n)) ∘ ⇑(ConcreteCategory.hom (S.proj (n + 1))) =
    ⇑(ConcreteCategory.hom (S.proj n))

Tactic:
← S.proj_comp_transitionMap n

Goal state after:
S : LightProfinite
n : ℕ
⊢ ⇑(ConcreteCategory.hom (S.transitionMap n)) ∘ ⇑(ConcreteCategory.hom (S.proj (n + 1))) =
    ⇑(ConcreteCategory.hom (S.proj (n + 1) ≫ S.diagram.map (Opposite.op (homOfLE ⋯))))
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 (Presheaf.coherentExtensiveEquivalence.functor.map ((StoneanCompHaus.equivalence A).inverse.map f)) ↔
    ∀ (S : Stonean), Function.Surjective ⇑(hom (f.hom.app (op S.compHaus)))

Tactic:
← isLocallySurjective_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)
⊢ IsLocallySurjective
      (Presheaf.coherentExtensiveEquivalence.functor.map ((StoneanCompHaus.equivalence A).inverse.map f)) ↔
    ∀ (S : Stonean), Function.Surjective ⇑(hom (f.hom.app (op S.compHaus)))
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
⊢ Epi f ↔
    ∀ (S : LightProfinite) (y : 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:
← isLocallySurjective_iff_epi'

Goal state after:
X Y : LightCondSet
f : X ⟶ Y
⊢ IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : 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
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
⊢ Epi f ↔
    ∀ (S : LightProfinite) (y : ↑(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:
← isLocallySurjective_iff_epi'

Goal state after:
R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
⊢ IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : ↑(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
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)
n : ℕ
k : Y ⟶ lightToProfinite.obj (S.component n)
h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)
⊢ g ≫ lightToProfinite.map (S.proj n) = g ≫ lightToProfinite.map (S.proj (n + 1) ≫ S.transitionMap n)

Tactic:
← S.proj_comp_transitionMap n

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)
n : ℕ
k : Y ⟶ lightToProfinite.obj (S.component n)
h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)
⊢ g ≫ lightToProfinite.map (S.proj (n + 1) ≫ S.diagram.map (Opposite.op (homOfLE ⋯))) =
    g ≫ lightToProfinite.map (S.proj (n + 1) ≫ S.transitionMap n)
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
z : Upto p
⊢ p (k + ↑z) → Nat.find h' = k + ↑z → ⋯.fix (fixAux f) z x = Fix.approx f (k + 1) x

Tactic:
intro _this

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
⊢ Nat.find h' = k + ↑z → ⋯.fix (fixAux f) z x = Fix.approx f (k + 1) x
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = List.foldl f x (toList xs)

Tactic:
← FreeMonoid.toList_ofList (toList xs),

Goal state after:
α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = List.foldl f x (FreeMonoid.toList (FreeMonoid.ofList (toList xs)))
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x ↦ { down := l.down + 1 }) { down := 0 } ys).down = ys.length

Tactic:
← Nat.add_zero ys.length

Goal state after:
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
ys : List α
⊢ (List.foldl (fun l x ↦ { down := l.down + 1 }) { down := 0 } ys).down = ys.length + 0
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x✝ : Chain (Unit → Part α)
⊢ f (Part.ωSup (x✝.map (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup ((x✝.map (toUnitMono { toFun := f, monotone' := ⋯ })).map (Pi.evalOrderHom PUnit.unit))

Tactic:
erw [hc.map_ωSup]

Goal state after:
α : Type u_1
f : Part α → Part α
hc : ωScottContinuous f
x✝ : Chain (Unit → Part α)
⊢ ωSup ((x✝.map (Pi.evalOrderHom PUnit.unit)).map { toFun := f, monotone' := ⋯ }) =
    Part.ωSup ((x✝.map (toUnitMono { toFun := f, monotone' := ⋯ })).map (Pi.evalOrderHom PUnit.unit))
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
F : Realizer α
s : Set α
a : α
⊢ (a ∉ s → ∃ b, a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔ (∀ (b : F.σ), a ∈ F.F.f b → ∃ z, z ∈ F.F.f b ∩ s) → a ∈ s

Tactic:
have := Classical.propDecidable; rw [not_imp_comm]
          simp [not_exists, not_and, not_forall, and_comm]

Goal state after:
Module: Mathlib.Data.DFinsupp.FiniteInfinite

Goal state before:
pp: ι✝ : Type u
γ : Type w
β : ι✝ → Type v
β₁ : ι✝ → Type v₁
β₂ : ι✝ → Type v₂
ι : Type u_1
π : ι → Type u_2
inst✝² : ∀ (i : ι), Nontrivial (π i)
inst✝¹ : (i : ι) → Zero (π i)
inst✝ : Infinite ι
⊢ Infinite (Π₀ (i : ι), π i)

Tactic:
let := Classical.decEq ι; choose m hm using fun i => exists_ne (0 : π i)
  exact Infinite.of_injective _ (DFinsupp.single_left_injective hm)

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ g.toFun i = 0 }
i : ι
h : i ∉ ↑fs + ↑gs
hf : f i = 0
hg : g i = 0
⊢ Icc (f i) (g i) = 0

Tactic:
hf,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ g.toFun i = 0 }
i : ι
h : i ∉ ↑fs + ↑gs
hf : f i = 0
hg : g i = 0
⊢ Icc 0 (g i) = 0
Module: Mathlib.Data.Fin.Init

Goal state before:
pp: k : ℕ
inst✝ : NeZero k
a : Fin k
⊢ a ^^^ 0 = a

Tactic:
grind [Fin.xor_val, Fin.val_zero, Nat.mod_eq_of_lt]

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

Goal state before:
pp: case swap
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
rcases h₁ : f a with - | c

Goal state after:
case swap.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

case swap.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
⊢ ∀ x ∈ ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val,
    ∀ y ∈ ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, x.fst = y.fst → x = y

Tactic:
simp only [Finset.mem_val, Finset.mem_sigma, Option.mem_toFinset, Option.mem_def]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
⊢ ∀ (x : (a : α) × β a),
    x.fst ∈ (↑f).1 ∧ (↑f).2 x.fst = some x.snd →
      ∀ (y : (a : α) × β a), y.fst ∈ (↑f).1 ∧ (↑f).2 y.fst = some y.snd → x.fst = y.fst → x = y
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: α : Type u_1
x : Multiset α
⊢ traverse pure x = pure x

Tactic:
by
  induction x using Quotient.inductionOn
  simp [traverse]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : a₁ ≠ a₂
p : a₁ ∈ l.keys
q : ¬a₂ ∈ l.keys
⊢ a₁ ∈ (kerase a₂ l).keys

Tactic:
simp [q, p]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ map Sigma.fst (eraseP (fun s ↦ decide (a = s.fst)) l) = eraseP (fun x ↦ a == x) (map Sigma.fst l)

Tactic:
eraseP_map,

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ map Sigma.fst (eraseP (fun s ↦ decide (a = s.fst)) l) = map Sigma.fst (eraseP ((fun x ↦ a == x) ∘ Sigma.fst) l)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u_1
inst✝ : SizeOf α
l r : List α
a : α
h : sizeOf l ≤ sizeOf r
⊢ sizeOf (a :: l) ≤ sizeOf (a :: r)

Tactic:
rw [cons.sizeOf_spec, cons.sizeOf_spec]

Goal state after:
α : Type u_1
inst✝ : SizeOf α
l r : List α
a : α
h : sizeOf l ≤ sizeOf r
⊢ 1 + sizeOf a + sizeOf l ≤ 1 + sizeOf a + sizeOf r
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a * a = b * b

Tactic:
exact natAbs_eq_iff_mul_self_eq

Goal state after:
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: case mpr.right
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) % b = r

Tactic:
· rw [add_mul_emod_self_left, ← emod_abs, emod_eq_of_lt hz hb]

Goal state after:
Module: Mathlib.Data.Int.NatPrime

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ k.natAbs * k.natAbs

Tactic:
← natAbs_mul,

Goal state after:
p : ℕ
hp : Nat.Prime p
k : ℤ
h : ↑p ∣ k ^ 2
⊢ p ∣ (k * k).natAbs
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b ↑n).lnot = bit (!b) (↑n).lnot

Tactic:
simp [lnot]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b -[n+1]).lnot = bit (!b) -[n+1].lnot

Tactic:
simp [lnot]

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v : ℕ
x : ℤ
⊢ x ∈ map castEmbedding ({x ∈ Ioc a b | x ≡ v [MOD r]}) ↔ x ∈ {x ∈ Ioc ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}

Tactic:
simp only [mem_map, mem_filter, mem_Ioc, castEmbedding_apply]

Goal state after:
a b r v : ℕ
x : ℤ
⊢ (∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) ↔ (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]