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

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
X✝ Y✝ : TopCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : TopCat.toGeneratedByTopCat.map a₁✝ = TopCat.toGeneratedByTopCat.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext x

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
X✝ Y✝ : TopCat
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : TopCat.toGeneratedByTopCat.map a₁✝ = TopCat.toGeneratedByTopCat.map a₂✝
x : ↑X✝
⊢ (ConcreteCategory.hom a₁✝) x = (ConcreteCategory.hom a₂✝) x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ
a✝ : f ∈ ⊤
⊢ ((Finsupp.onFinset Finset.univ f.toFun ⋯).sum fun i a ↦ a • spanFinBasis C s i) = f

Tactic:
ext x

Goal state after:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ
a✝ : f ∈ ⊤
x : ↑(π C fun x ↦ x ∈ s)
⊢ ((Finsupp.onFinset Finset.univ f.toFun ⋯).sum fun i a ↦ a • spanFinBasis C s i) x = f x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
⊢ π C J = C

Tactic:
ext x

Goal state after:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
⊢ x ∈ π C J ↔ x ∈ C
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
⊢ π (π C K) J = π C J

Tactic:
ext x

Goal state after:
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
x : I → Bool
⊢ x ∈ π (π C K) J ↔ x ∈ π C J
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
x : (𝟭 (Type u_1)).obj X
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J✝ K L : I → Prop
inst✝³ : (i : I) → Decidable (J✝ i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
J : (Finset I)ᵒᵖ
⊢ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := ProjRestricts C ⋯, continuous_toFun := ⋯ } =
    𝟙 (of ↑(π C fun x ↦ x ∈ unop J))

Tactic:
simp only [projRestricts_eq_id C (· ∈ (unop J))]; rfl

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
s t : Finset I
f : unop (op t) ⊆ unop (op s)
⊢ (spanFunctor hC).map (op { down := { down := f } }) ≫
      (CompHausLike.isoOfBijective (ConcreteCategory.ofHom (iso_map C fun x ↦ x ∈ unop (op t))) ⋯).hom =
    (CompHausLike.isoOfBijective (ConcreteCategory.ofHom (iso_map C fun x ↦ x ∈ unop (op s))) ⋯).hom ≫
      (indexFunctor hC).map (op { down := { down := f } })

Tactic:
ext x

Goal state after:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝³ : (i : I) → Decidable (J i)
inst✝² : (i : I) → Decidable (K i)
inst✝¹ : (i : I) → Decidable (L i)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
s t : Finset I
f : unop (op t) ⊆ unop (op s)
x : ↑((spanFunctor hC).obj (op s)).toTop
⊢ (ConcreteCategory.hom
        ((spanFunctor hC).map (op { down := { down := f } }) ≫
          (CompHausLike.isoOfBijective (ConcreteCategory.ofHom (iso_map C fun x ↦ x ∈ unop (op t))) ⋯).hom))
      x =
    (ConcreteCategory.hom
        ((CompHausLike.isoOfBijective (ConcreteCategory.ofHom (iso_map C fun x ↦ x ∈ unop (op s))) ⋯).hom ≫
          (indexFunctor hC).map (op { down := { down := f } })))
      x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
⊢ ⇑(eval (π C J) l) ∘ ProjRestrict C J = ⇑(eval C l)

Tactic:
ext x

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (⇑(eval (π C J) l) ∘ ProjRestrict C J) x = (eval C l) x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ C0 C ho ∪ C1 C ho = C

Tactic:
ext x

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
⊢ x ∈ C0 C ho ∪ C1 C ho ↔ x ∈ C
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
y : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
⊢ (Linear_CC' C hsC ho) ((πs C o) y) = 0

Tactic:
ext x

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
y : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
x : ↑(C' C ho)
⊢ ((Linear_CC' C hsC ho) ((πs C o) y)) x = 0 x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hsC : ¬ord I i < Order.succ o → ¬x i = true
hi✝ : o ≤ ord I i
hi : o < ord I i
⊢ false = x i

Tactic:
simp only [not_lt, Bool.not_eq_true, Order.succ_le_iff] at hsC

Goal state after:
case inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi✝ : o ≤ ord I i
hi : o < ord I i
hsC : o < ord I i → x i = false
⊢ false = x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ord I i = o
⊢ true = x i

pp: case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ord I i < o
⊢ x i = x i

pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ¬ord I i < o
⊢ false = x i

Tactic:
· rw [ord_term ho] at hi
    rw [← hx.2, hi]

Goal state after:
case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ord I i < o
⊢ x i = x i

case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ¬ord I i < o
⊢ false = x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x ↦ false} ℤ
a✝ : f ∈ ⊤
⊢ ↑(f default) = f

Tactic:
ext x

Goal state after:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x ↦ false} ℤ
a✝ : f ∈ ⊤
x : ↑{fun x ↦ false}
⊢ ↑(f default) x = f x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hsC : ¬ord I i < Order.succ o → ¬x i = true
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
⊢ false = x i

Tactic:
simp only [not_lt, Bool.not_eq_true, Order.succ_le_iff] at hsC

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
hsC : o < ord I i → x i = false
⊢ false = x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Function.Bijective (range_equiv_smaller_toFun C o)

Tactic:
dsimp +unfoldPartialApp [range_equiv_smaller_toFun]
  refine ⟨fun a b hab ↦ ?_, fun ⟨a, b, hb⟩ ↦ ?_⟩
  · ext1
    simp only [Subtype.mk.injEq] at hab
    exact injective_πs C o hab
  · use ⟨b, hb.1⟩
    simpa only [Subtype.mk.injEq] using hb.2

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ eval (π C fun x ↦ ord I x < o₂) ⟨l, ⋯⟩ = (πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)

Tactic:
ext x

Goal state after:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
x : ↑(π C fun x ↦ ord I x < o₂)
⊢ (eval (π C fun x ↦ ord I x < o₂) ⟨l, ⋯⟩) x = ((πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)) x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ ↑l
h' : ¬ord I i < o
⊢ eval C l = 0

Tactic:
ext x

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ ↑l
h' : ¬ord I i < o
x : ↑C
⊢ (eval C l) x = 0 x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
c : I → Bool
hc : c ∈ C
⊢ c ∈ {fun x ↦ false}

Tactic:
ext x

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
c : I → Bool
hc : c ∈ C
x : I
⊢ c x = false
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: S : Profinite
C : { C // IsClopen C }
⊢ ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {false})ᶜ = ↑C

Tactic:
ext x

Goal state after:
S : Profinite
C : { C // IsClopen C }
x : ↑S.toTop
⊢ x ∈ ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {false})ᶜ ↔ x ∈ ↑C
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: S : Profinite
C : { C // IsClopen C }
⊢ (fun a ↦ decide (a ∈ ↑C)) ⁻¹' {true} = ↑C

Tactic:
ext x

Goal state after:
S : Profinite
C : { C // IsClopen C }
x : ↑S.toTop
⊢ x ∈ (fun a ↦ decide (a ∈ ↑C)) ⁻¹' {true} ↔ x ∈ ↑C
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case hf
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ False

Tactic:
apply hh.2 ∘ of_decide_eq_true

Goal state after:
case hf
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (b ∈ C) = true
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ LinearIndependent ℤ (eval C ∘ ⇑(sum_equiv C hsC ho)) ↔
    LinearIndependent ℤ (Sum.elim (fun l ↦ Products.eval C ↑l) fun l ↦ Products.eval C ↑l)

Tactic:
← sum_equiv_comp_eval_eq_elim C hsC ho

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ LinearIndependent ℤ (eval C ∘ ⇑(sum_equiv C hsC ho)) ↔ LinearIndependent ℤ (eval C ∘ (sum_equiv C hsC ho).toFun)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
⊢ (Linear_CC' C hsC ho) (e C (term I ho) * eval C ⟨↑l.Tail, ⋯⟩) = eval (C' C ho) (Tail ⟨term I ho :: ↑l.Tail, hlc⟩)

Tactic:
ext x

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
⊢ ((Linear_CC' C hsC ho) (e C (term I ho) * eval C ⟨↑l.Tail, ⋯⟩)) x =
    (eval (C' C ho) (Tail ⟨term I ho :: ↑l.Tail, hlc⟩)) x
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X : UniformSpaceCat
Y : CpltSepUniformSpace
f : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace
⊢ (extensionHom (X.completionHom ≫ f)).hom = f

Tactic:
ext x

Goal state after:
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace
x : (completionFunctor.obj X).toUniformSpace.carrier
⊢ (ConcreteCategory.hom (extensionHom (X.completionHom ≫ f)).hom) x = (ConcreteCategory.hom f) x
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ (fun f ↦ X.completionHom ≫ f.hom) ((fun f ↦ extensionHom f) f) = f

Tactic:
ext x

Goal state after:
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : X.carrier
⊢ (ConcreteCategory.hom ((fun f ↦ X.completionHom ≫ f.hom) ((fun f ↦ extensionHom f) f))) x = (ConcreteCategory.hom f) x
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ { toFun := fun f ↦ X'.completionHom ≫ f.hom, invFun := fun f ↦ extensionHom f, left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    completionFunctor.map f ≫
      { toFun := fun f ↦ X.completionHom ≫ f.hom, invFun := fun f ↦ extensionHom f, left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
ext x

Goal state after:
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
x : (completionFunctor.obj X').α
⊢ ↑(ConcreteCategory.hom
          ({ toFun := fun f ↦ X'.completionHom ≫ f.hom, invFun := fun f ↦ extensionHom f, left_inv := ⋯,
                right_inv := ⋯ }.symm
            (f ≫ g)))
      x =
    ↑(ConcreteCategory.hom
          (completionFunctor.map f ≫
            { toFun := fun f ↦ X.completionHom ≫ f.hom, invFun := fun f ↦ extensionHom f, left_inv := ⋯,
                  right_inv := ⋯ }.symm
              g))
      x
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
⊢ IsCompactSystem {s | IsCompact s ∧ IsClosed s}

Tactic:
refine IsCompactSystem.of_nonempty_iInter fun C hC_cc h_nonempty ↦ ?_

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), C i ∈ {s | IsCompact s ∧ IsClosed s}
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ (⋂ i, C i).Nonempty
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
⊢ (f.concat g).comp IccInclusionLeft = f

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
x : ↑(Icc a b)
⊢ ((f.concat g).comp IccInclusionLeft) x = f x
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
hfin✝ : tα.Finite
htα : univ ⊆ ⋃ x ∈ tα, U x
val✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
hfin : tβ.Finite
htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂
val✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g : (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨f, hf⟩ = (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨g, hg⟩
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
F_f_g : F (f x') = F (g x')
⊢ dist (f x') (F (f x')) + dist (g x') (F (f x')) = dist (f x') (F (f x')) + dist (g x') (F (g x'))

Tactic:
by rw [F_f_g]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: case inr
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
x : α
hx : x ∈ Icc b c
hxb : x ≠ b
⊢ ((f.concat g).comp IccInclusionRight) ⟨x, hx⟩ = g ⟨x, hx⟩

Tactic:
· have h : ¬ x ≤ b := lt_of_le_of_ne hx.1 (Ne.symm hxb) |>.not_ge
    simp [concat, hb, IccInclusionRight, h, IccExtendCM, projIccCM, projIcc, inclusion, hx.2, hx.1]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.LocallyConstant

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : IsTopologicalSemiring Y
r : R
⊢ ↑((algebraMap R (LocallyConstant X Y)) r) = (algebraMap R C(X, Y)) r

Tactic:
ext x

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : IsTopologicalSemiring Y
r : R
x : X
⊢ ↑((algebraMap R (LocallyConstant X Y)) r) x = ((algebraMap R C(X, Y)) r) x
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: case refine_2
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
    Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
      match x with
      | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
i : ι
f : C(X i, Y × Z)
⊢ Continuous[inst✝⁴ i, inst✝¹] (g ∘ ⇑f)

Tactic:
exact (h i (ContinuousMap.snd.comp f) i (ContinuousMap.fst.comp f)).comp
      (Continuous.prodMk continuous_id continuous_id)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
⊢ some '' Metric.eball a r = Metric.eball (some a) r

Tactic:
ext x

Goal state after:
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
⊢ x ∈ some '' Metric.eball a r ↔ x ∈ Metric.eball (some a) r
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
h : none ∈ Metric.eball (some a) r
⊢ none ∈ some '' Metric.eball a r

Tactic:
simp at h

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
⊢ ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑g

Tactic:
rw [eventually_nhdsSet_iff_forall] at *
  intro x hx
  apply ((hf x hx).and (h x hx).eventually_nhds).mono
  intro y hy
  convert! hy.1 using 1
  exact Germ.coe_eq.mpr hy.2

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x : X
f : ↑(Ω^ N X x)
g : (N → ↑I) → X
h : g = ⇑f
⊢ copy f g h = f

Tactic:
ext x

Goal state after:
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
f : ↑(Ω^ N X x✝)
g : (N → ↑I) → X
h : g = ⇑f
x : N → ↑I
⊢ (copy f g h) x = f x
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: a : ℕ → Fin 3
h : ∀ (n : ℕ), a n ≠ 1
⊢ ofDigits a ∈ cantorSet

Tactic:
by
  simp only [cantorSet, Set.mem_iInter]
  intro i
  induction i generalizing a with
  | zero =>
    simp only [preCantorSet_zero, Set.mem_Icc]
    exact ⟨ofDigits_nonneg a, ofDigits_le_one a⟩
  | succ i ih =>
    simp only [preCantorSet, Set.mem_union, Set.mem_image, ← exists_or]
    use ofDigits (fun i ↦ a (i + 1))
    have : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i := ih (by solve_by_elim)
    simp only [this, ofDigits_eq_sum_add_ofDigits a 1, Finset.range_one, ofDigitsTerm,
      Nat.cast_ofNat, Finset.sum_singleton, zero_add, pow_one, true_and, field]
    specialize h 0
    generalize a 0 = x at h
    fin_cases x <;> simp at ⊢ h

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
⊢ Prod.snd '' ⇑(Homeomorph.preimageImageRestrict α S s) '' (fun x ↦ ↑x) ⁻¹' s = S.domRestrict '' s

Tactic:
ext x

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
x : (i : ↑S) → α ↑i
⊢ x ∈ Prod.snd '' ⇑(Homeomorph.preimageImageRestrict α S s) '' (fun x ↦ ↑x) ⁻¹' s ↔ x ∈ S.domRestrict '' s
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case hg
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun n ↦ x - 3⁻¹ ^ n) Filter.atTop (nhds x)

Tactic:
rw [← tendsto_sub_nhds_zero_iff]

Goal state after:
case hg
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun x_1 ↦ x - 3⁻¹ ^ x_1 - x) Filter.atTop (nhds 0)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ cantorSet = {x | ∃ a, (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x}

Tactic:
ext x

Goal state after:
x : ℝ
⊢ x ∈ cantorSet ↔ x ∈ {x | ∃ a, (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x}