mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
⊢ False

Tactic:
have G₁_comp : IsCompact G₁ᶜ := IsClosed.isCompact G₁_open.isClosed_compl

Goal state after:
A E : Type u
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace E
inst✝³ : ExtremallyDisconnected A
inst✝² : T2Space A
inst✝¹ : T2Space E
inst✝ : CompactSpace E
ρ : E → A
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ
x₁ x₂ : E
hρx : ρ x₁ = ρ x₂
hx : ¬x₁ = x₂
G₁ G₂ : Set E
G₁_open : IsOpen G₁
G₂_open : IsOpen G₂
hx₁ : x₁ ∈ G₁
hx₂ : x₂ ∈ G₂
disj : Disjoint G₁ G₂
G₁_comp : IsCompact G₁ᶜ
⊢ False
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
⊢ ∃ h, Continuous h ∧ f ∘ h = φ

Tactic:
let D : Set <| A × B := {x | φ x.fst = f x.snd}

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}
⊢ ∃ h, Continuous h ∧ f ∘ h = φ
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: A : Type u
inst✝³ : TopologicalSpace A
inst✝² : ExtremallyDisconnected A
inst✝¹ : CompactSpace A
inst✝ : T2Space A
⊢ Projective A

Tactic:
by
  -- let $B$ and $C$ be compact; let $f : B \twoheadrightarrow C$ and $\phi : A \to C$ be continuous
  intro B C _ _ _ _ _ _ φ f φ_cont f_cont f_surj
  -- let $D := \{(a, b) : \phi(a) = f(b)\}$ with projections $\pi_1 : D \to A$ and $\pi_2 : D \to B$
  let D : Set <| A × B := {x | φ x.fst = f x.snd}
  have D_comp : CompactSpace D := isCompact_iff_compactSpace.mp
    (isClosed_eq (φ_cont.comp continuous_fst) (f_cont.comp continuous_snd)).isCompact
  -- apply Lemma 2.4 to get closed $E$ satisfying "Zorn subset condition"
  let X₁ : D → A := Prod.fst ∘ Subtype.val
  have X₁_cont : Continuous X₁ := continuous_fst.comp continuous_subtype_val
  have X₁_surj : X₁.Surjective := fun a => ⟨⟨⟨a, _⟩, (f_surj <| φ a).choose_spec.symm⟩, rfl⟩
  rcases exists_compact_surjective_zorn_subset X₁_cont X₁_surj with ⟨E, _, E_onto, E_min⟩
  -- apply Lemma 2.3 to get homeomorphism $\pi_1|_E : E \to A$
  let ρ : E → A := E.domRestrict X₁
  have ρ_cont : Continuous ρ := X₁_cont.continuousOn.domRestrict
  have ρ_surj : ρ.Surjective := fun a => by
    rcases (E_onto ▸ mem_univ a : a ∈ X₁ '' E) with ⟨d, ⟨hd, rfl⟩⟩; exact ⟨⟨d, hd⟩, rfl⟩
  let ρ' := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
  -- prove $\rho := \pi_2|_E \circ \pi_1|_E^{-1}$ satisfies $\phi = f \circ \rho$
  let X₂ : D → B := Prod.snd ∘ Subtype.val
  have X₂_cont : Continuous X₂ := continuous_snd.comp continuous_subtype_val
  refine ⟨E.domRestrict X₂ ∘ ρ'.symm,
    ⟨X₂_cont.continuousOn.domRestrict.comp ρ'.symm.continuous, ?_⟩⟩
  suffices f ∘ E.domRestrict X₂ = φ ∘ ρ' by
    rw [← comp_assoc, this, comp_assoc, Homeomorph.self_comp_symm, comp_id]
  ext x
  exact x.val.mem.symm

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

Goal state before:
pp: case neg
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this✝ : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun i ↦ Option.casesOn i C0 C'
x : X
hx : ∃ i, x ∈ D i
hx0 : x ∉ C0
hxD : x ∉ D none
⊢ ∃ i, x ∈ C i

Tactic:
obtain ⟨none | j, hi⟩ := hx; {grind}
        have hxD' : x ∈ ⋃ i, D' i := mem_iUnion.mpr ⟨j, by grind⟩
        obtain ⟨k, hk⟩ := mem_iUnion.mp <| C'_cover_D' hxD'
        exact ⟨some k, hk⟩

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

Goal state before:
pp: case cons.succ
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ Reaches₁ (TM2.step tr) { l := some (q₁.pred q₂), var := s, stk := elim (trList ((n + 1) :: v)) [] c d }
    (Nat.rec { l := some q₁, var := none, stk := elim (trList ((n + 1) :: v).tail) [] c d }
      (fun n_1 x ↦ { l := some q₂, var := none, stk := elim (trList (n_1 :: ((n + 1) :: v).tail)) [] c d })
      ((n + 1) :: v).headI)

Tactic:
simp only [trList, trNat.eq_1, trNum, Nat.cast_succ, Num.add_one, Num.succ,
    List.tail_cons, List.headI_cons]

Goal state after:
case cons.succ
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ Reaches₁ (TM2.step tr)
    { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum (↑n).succ' ++ Γ'.cons :: trList v) [] c d }
    { l := some q₂, var := none,
      stk :=
        elim
          ((match ↑n with
            | Num.zero => []
            | Num.pos n => trPosNum n) ++
            Γ'.cons :: trList v)
          [] c d }
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case 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
⊢ ∀ (j : J), TopologicalSpace.IsTopologicalBasis {W | IsClopen W}

pp: case refine_2
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
⊢ ∀ (i j : J) (f : i ⟶ j),
    ∀ V ∈ {W | IsClopen W}, ⇑(ConcreteCategory.hom ((F ⋙ toTopCat).map f)) ⁻¹' V ∈ {W | IsClopen W}

pp: case refine_3
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
hB :
  TopologicalSpace.IsTopologicalBasis
    {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
⊢ ∃ j V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V

Tactic:
· intro i
    change TopologicalSpace.IsTopologicalBasis {W : Set (F.obj i) | IsClopen W}
    apply isTopologicalBasis_isClopen

Goal state after:
case refine_2
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
⊢ ∀ (i j : J) (f : i ⟶ j),
    ∀ V ∈ {W | IsClopen W}, ⇑(ConcreteCategory.hom ((F ⋙ toTopCat).map f)) ⁻¹' V ∈ {W | IsClopen W}

case refine_3
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
hB :
  TopologicalSpace.IsTopologicalBasis
    {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
⊢ ∃ j V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
Module: Mathlib.Topology.Category.LightProfinite.Limits

Goal state before:
pp: X Y Z : LightProfinite
f : X ⟶ Z
g : Y ⟶ Z
h : Function.Surjective ⇑(ConcreteCategory.hom g)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (CompHausLike.pullback.fst f g))

Tactic:
intro x

Goal state after:
X Y Z : LightProfinite
f : X ⟶ Z
g : Y ⟶ Z
h : Function.Surjective ⇑(ConcreteCategory.hom g)
x : ↑X.toTop
⊢ ∃ a, (ConcreteCategory.hom (CompHausLike.pullback.fst f g)) a = x
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case copy
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy

Tactic:
| copy q q_ih =>

Goal state after:
case copy
q' q : Λ'
q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
⊢ q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
⊢ Function.FactorsThrough ⇑a ⇑(ConcreteCategory.hom (G.map π))

Tactic:
intro x

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x : ↑(G.obj Z)
⊢ ∀ ⦃b : ↑(G.obj Z)⦄, (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) b → a x = a b
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
a b : (fun X ↦ X) ((yonedaPresheaf G X).obj (op B))
h :
  (ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)) a =
    (ConcreteCategory.hom (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)) b
⊢ a = b

Tactic:
simp only [yonedaPresheaf, comp, Quiver.Hom.unop_op, TypeCat.Fun.coe_mk,
      Set.coe_ofPred, mapToEqualizer, Set.mem_ofPred_eq, ConcreteCategory.hom_ofHom,
      Subtype.mk.injEq, mk.injEq] at h

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝³ : TopologicalSpace X
inst✝² : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap ⇑(ConcreteCategory.hom (G.map π))
Z B : C
π : Z ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
a b : (fun X ↦ X) ((yonedaPresheaf G X).obj (op B))
h : ⇑a ∘ ⇑(TopCat.Hom.hom (G.map π)) = ⇑b ∘ ⇑(TopCat.Hom.hom (G.map π))
⊢ a = b
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case copy
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : trStmts₁ q.copy ⊆ S
⊢ Supports (trStmts₁ q.copy) S

Tactic:
| copy q q_ih =>

Goal state after:
case copy
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.copy
HS₁ : trStmts₁ q.copy ⊆ S
⊢ Supports (trStmts₁ q.copy) S
Module: Mathlib.Topology.Category.Profinite.Extend

Goal state before:
pp: I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
C : Type u_1
inst✝ : Category.{v_1, u_1} C
G : Profiniteᵒᵖ ⥤ C
S : Profinite
x✝¹ x✝ : CostructuredArrow toProfinite.op (Opposite.op S)
f : x✝¹ ⟶ x✝
this : (toProfinite.map f.left.unop).op ≫ x✝.hom = x✝¹.hom
⊢ (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ G).map f ≫ G.map x✝.hom =
    G.map x✝¹.hom ≫ ((const (CostructuredArrow toProfinite.op (Opposite.op S))).obj (G.obj (Opposite.op S))).map f

Tactic:
simp [← map_comp, this]

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

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g✝ : T ⟶ S
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
this : Preregular (CompHausLike P)
⊢ functorToPresheaves.map (g.hom.app (op (of P PUnit.{u + 1}))) ≫ counitApp Y.obj = counitApp X.obj ≫ g.hom

Tactic:
ext S (f : LocallyConstant _ _)

Goal state after:
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f✝ : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g✝ : T ⟶ S✝
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
this : Preregular (CompHausLike P)
S : (CompHausLike P)ᵒᵖ
f : LocallyConstant (↑(unop S).toTop) (X.obj.obj (op (of P PUnit.{u + 1})))
⊢ (ConcreteCategory.hom ((functorToPresheaves.map (g.hom.app (op (of P PUnit.{u + 1}))) ≫ counitApp Y.obj).app S)).toFun
      f =
    (ConcreteCategory.hom ((counitApp X.obj ≫ g.hom).app S)).toFun f
Module: Mathlib.Topology.Category.LightProfinite.Sequence

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

Tactic:
simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, inv_eq_zero] at h

Goal state after:
case refine_1.some.none
n : ℕ
h : ↑n + 1 = 0
⊢ Option.some n = none
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
⊢ ∀ (a : Function.Fiber ⇑f),
    (ConcreteCategory.hom (X.map (sigmaIncl f a).op))
        ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
      (ConcreteCategory.hom (X.map (sigmaIncl f a).op))
        ((ConcreteCategory.hom (counitAppApp (Profinite.of (Opposite.unop Y).obj) X)) f)

Tactic:
intro x

Goal state after:
case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (counitAppApp (Profinite.of (Opposite.unop Y).obj) X)) f)
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case e_a
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj
      (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) PUnit.{u + 1})))
⊢ ∀ (a : Function.Fiber ⇑f),
    (ConcreteCategory.hom (X.map (sigmaIncl f a).op))
        ((ConcreteCategory.hom
              ((↾fun f ↦ ⇑f) ≫ (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv)).toFun
          f) =
      (ConcreteCategory.hom (X.map (sigmaIncl f a).op))
        ((ConcreteCategory.hom ((counitApp X).app (Opposite.op (toLightProfinite.obj (Opposite.unop Y))))).toFun f)

Tactic:
intro x

Goal state after:
case e_a
X : LightProfiniteᵒᵖ ⥤ Type u
inst✝ : PreservesFiniteProducts X
hX : (S : LightProfinite) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toLightProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj
      (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom
            ((↾fun f ↦ ⇑f) ≫ (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))).inv)).toFun
        f) =
    (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom ((counitApp X).app (Opposite.op (toLightProfinite.obj (Opposite.unop Y))))).toFun f)
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
β γ : Type u
f : β → γ
x✝ : t β
⊢ (traverse (pure ∘ f) x✝).run = ((pure ∘ map f) x✝).run

Tactic:
exact traverse_eq_map_id _ _

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
⊢ (fun i t ↦ (↑t).1) <$$> u✝ = x ∧ (fun i t ↦ (↑t).2) <$$> u✝ = y ↔
    (fun i t ↦ (↑t).1) <$$> f' rr n α <$$> u✝ = x ∧ (fun i t ↦ (↑t).2) <$$> f' rr n α <$$> u✝ = y

Tactic:
simp +unfoldPartialApp only [map_map, TypeVec.comp]

Goal state after:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
⊢ (fun i t ↦ (↑t).1) <$$> u✝ = x ∧ (fun i t ↦ (↑t).2) <$$> u✝ = y ↔
    (fun i x ↦ (↑(f' rr n α i x)).1) <$$> u✝ = x ∧ (fun i x ↦ (↑(f' rr n α i x)).2) <$$> u✝ = y
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ Part.fix ⇑f ≤ ωSup (approxChain f)

Tactic:
intro x

Goal state after:
case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
⊢ Part.fix (⇑f) x ≤ ωSup (approxChain f) x
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ Part.fix g = g (Part.fix g)

Tactic:
rw [fix_eq_ωSup_of_ωScottContinuous hc, hc.map_ωSup]

Goal state after:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup (approxChain { toFun := g, monotone' := ⋯ }) =
    ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ })
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ count (!b) l ≤ count b l + 1

Tactic:
cases l

Goal state after:
case nil
b : Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) []
⊢ count (!b) [] ≤ count b [] + 1

case cons
b head✝ : Bool
tail✝ : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝)
⊢ count (!b) (head✝ :: tail✝) ≤ count b (head✝ :: tail✝) + 1
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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (f.rangeIcc g).support ⊆ f.support ∪ g.support

Tactic:
intro x

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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
⊢ x ∈ (f.rangeIcc g).support → x ∈ f.support ∪ g.support
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
⊢ Function.Injective ⇑(ConcreteCategory.hom (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞})))

Tactic:
exact Subtype.val_injective

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u
β✝ : α✝ → Type v
α : Type ?u.19
β : Type ?u.20
f : α → β
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Injective f
⊢ ∀ (x : α), x ∈ List.filterMap (partialInv f) (toList β)

Tactic:
intro x

Goal state after:
α✝ : Type u
β✝ : α✝ → Type v
α : Type ?u.19
β : Type ?u.20
f : α → β
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Injective f
x : α
⊢ x ∈ List.filterMap (partialInv f) (toList β)
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
⊢ ∀ (x : Sigma β), x ∈ List.flatMap (fun a ↦ List.map (Sigma.mk a) (toList (β a))) (toList α)

Tactic:
intro x

Goal state after:
α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
x : Sigma β
⊢ x ∈ List.flatMap (fun a ↦ List.map (Sigma.mk a) (toList (β a))) (toList α)
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse UInt8.ofFin UInt8.toFin

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : UInt8
⊢ UInt8.ofFin x.toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse UInt8.ofFin UInt8.toFin

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 8)
⊢ (UInt8.ofFin x).toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ LeftInverse UInt16.ofFin UInt16.toFin

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : UInt16
⊢ UInt16.ofFin x.toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
⊢ RightInverse UInt16.ofFin UInt16.toFin

Tactic:
intro x

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 16)
⊢ (UInt16.ofFin x).toFin = x