awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
S : LightProfinite
inst :
  Nonempty.{u + 1}
    (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this_1 :
  ∀ (n : ℕ),
    Finite.{u + 1}
      (↑((lightToProfinite.obj (S.component n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
this_2 :
  Nonempty.{u + 1}
    (↑((lightToProfinite.obj (S.component 0)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
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)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)) (h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)) (h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)),
    ∃ (k' : Y ⟶ lightToProfinite.obj (S.component (n + 1))),
      k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : (n : ℕ) → Type (max 0 u) :=
  fun (n : ℕ) ↦ { k : Y ⟶ lightToProfinite.obj (S.component n) // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) :=
  fun (n : ℕ) (k : lifts n) ↦
    Subtype.mk (p := fun (k : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ↦
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)))
      (⋯.choose (p := fun (k' : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ↦
        k' ≫ lightToProfinite.map (S.transitionMap n) = (↑k : Y ⟶ lightToProfinite.obj (S.component n)) ∧
          f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))))
      ⋯
k_seq : (n : ℕ) → lifts n :=
  fun (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ lifts x)
      (Subtype.mk (p := fun (k : Y ⟶ lightToProfinite.obj (S.component Nat.zero)) ↦
        f ≫ k = g ≫ lightToProfinite.map (S.proj Nat.zero)) k0 h_down0)
      next n
h_down : ∀ (n : ℕ), f ≫ (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n)) = g ≫ lightToProfinite.map (S.proj n)
h_up :
  ∀ (n : ℕ),
    (↑(k_seq (n + 1)) : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ≫ lightToProfinite.map (S.transitionMap n) =
      (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n))
k_cone : Cone (S.diagram ⋙ lightToProfinite) :=
  { pt := Y, π := NatTrans.ofOpSequence (fun (n : ℕ) ↦ (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n))) ⋯ }
n : ℕᵒᵖ
⊢ g ≫ (lightToProfinite.mapCone S.asLimitCone).π.app n = (k_cone.extend f).π.app n

Tactic:
simp [show k_cone.π.app n = (k_seq n.unop).1 from rfl, h_down]

Premises used: rfl
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
S : LightProfinite
inst :
  Nonempty.{u + 1}
    (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this_1 :
  ∀ (n : ℕ),
    Finite.{u + 1}
      (↑((lightToProfinite.obj (S.component n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
this_2 :
  Nonempty.{u + 1}
    (↑((lightToProfinite.obj (S.component 0)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
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)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)) (h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)) (h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)),
    ∃ (k' : Y ⟶ lightToProfinite.obj (S.component (n + 1))),
      k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : (n : ℕ) → Type (max 0 u) :=
  fun (n : ℕ) ↦ { k : Y ⟶ lightToProfinite.obj (S.component n) // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) :=
  fun (n : ℕ) (k : lifts n) ↦
    Subtype.mk (p := fun (k : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ↦
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)))
      (⋯.choose (p := fun (k' : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ↦
        k' ≫ lightToProfinite.map (S.transitionMap n) = (↑k : Y ⟶ lightToProfinite.obj (S.component n)) ∧
          f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))))
      ⋯
k_seq : (n : ℕ) → lifts n :=
  fun (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ lifts x)
      (Subtype.mk (p := fun (k : Y ⟶ lightToProfinite.obj (S.component Nat.zero)) ↦
        f ≫ k = g ≫ lightToProfinite.map (S.proj Nat.zero)) k0 h_down0)
      next n
h_down : ∀ (n : ℕ), f ≫ (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n)) = g ≫ lightToProfinite.map (S.proj n)
h_up :
  ∀ (n : ℕ),
    (↑(k_seq (n + 1)) : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ≫ lightToProfinite.map (S.transitionMap n) =
      (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n))
k_cone : Cone (S.diagram ⋙ lightToProfinite) :=
  { pt := Y, π := NatTrans.ofOpSequence (fun (n : ℕ) ↦ (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n))) ⋯ }
⊢ g = (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)

Tactic:
have hg : g = (isLimitOfPreserves _ S.asLimit).lift (k_cone.extend f) := by
      apply (isLimitOfPreserves _ S.asLimit).uniq (k_cone.extend f)
      intro n
      simp [show k_cone.π.app n = (k_seq n.unop).1 from rfl, h_down]
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
S : LightProfinite
inst :
  Nonempty.{u + 1}
    (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this_1 :
  ∀ (n : ℕ),
    Finite.{u + 1}
      (↑((lightToProfinite.obj (S.component n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
this_2 :
  Nonempty.{u + 1}
    (↑((lightToProfinite.obj (S.component 0)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
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)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)) (h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)) (h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)),
    ∃ (k' : Y ⟶ lightToProfinite.obj (S.component (n + 1))),
      k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : (n : ℕ) → Type (max 0 u) :=
  fun (n : ℕ) ↦ { k : Y ⟶ lightToProfinite.obj (S.component n) // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) :=
  fun (n : ℕ) (k : lifts n) ↦
    Subtype.mk (p := fun (k : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ↦
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)))
      (⋯.choose (p := fun (k' : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ↦
        k' ≫ lightToProfinite.map (S.transitionMap n) = (↑k : Y ⟶ lightToProfinite.obj (S.component n)) ∧
          f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))))
      ⋯
k_seq : (n : ℕ) → lifts n :=
  fun (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ lifts x)
      (Subtype.mk (p := fun (k : Y ⟶ lightToProfinite.obj (S.component Nat.zero)) ↦
        f ≫ k = g ≫ lightToProfinite.map (S.proj Nat.zero)) k0 h_down0)
      next n
h_down : ∀ (n : ℕ), f ≫ (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n)) = g ≫ lightToProfinite.map (S.proj n)
h_up :
  ∀ (n : ℕ),
    (↑(k_seq (n + 1)) : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ≫ lightToProfinite.map (S.transitionMap n) =
      (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n))
k_cone : Cone (S.diagram ⋙ lightToProfinite) :=
  { pt := Y, π := NatTrans.ofOpSequence (fun (n : ℕ) ↦ (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n))) ⋯ }
hg : g = (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)
rw :
  f ≫ (isLimitOfPreserves lightToProfinite S.asLimit).lift k_cone =
    (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)
⊢ f ≫ (isLimitOfPreserves lightToProfinite S.asLimit).lift k_cone = g

Tactic:
rw [hg]
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
S : LightProfinite
inst :
  Nonempty.{u + 1}
    (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this_1 :
  ∀ (n : ℕ),
    Finite.{u + 1}
      (↑((lightToProfinite.obj (S.component n)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
this_2 :
  Nonempty.{u + 1}
    (↑((lightToProfinite.obj (S.component 0)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
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)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)) (h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)) (h_down : f ≫ k = g ≫ lightToProfinite.map (S.proj n)),
    ∃ (k' : Y ⟶ lightToProfinite.obj (S.component (n + 1))),
      k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : (n : ℕ) → Type (max 0 u) :=
  fun (n : ℕ) ↦ { k : Y ⟶ lightToProfinite.obj (S.component n) // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) :=
  fun (n : ℕ) (k : lifts n) ↦
    Subtype.mk (p := fun (k : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ↦
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)))
      (⋯.choose (p := fun (k' : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ↦
        k' ≫ lightToProfinite.map (S.transitionMap n) = (↑k : Y ⟶ lightToProfinite.obj (S.component n)) ∧
          f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))))
      ⋯
k_seq : (n : ℕ) → lifts n :=
  fun (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ lifts x)
      (Subtype.mk (p := fun (k : Y ⟶ lightToProfinite.obj (S.component Nat.zero)) ↦
        f ≫ k = g ≫ lightToProfinite.map (S.proj Nat.zero)) k0 h_down0)
      next n
h_down : ∀ (n : ℕ), f ≫ (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n)) = g ≫ lightToProfinite.map (S.proj n)
h_up :
  ∀ (n : ℕ),
    (↑(k_seq (n + 1)) : Y ⟶ lightToProfinite.obj (S.component (n + 1))) ≫ lightToProfinite.map (S.transitionMap n) =
      (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n))
k_cone : Cone (S.diagram ⋙ lightToProfinite) :=
  { pt := Y, π := NatTrans.ofOpSequence (fun (n : ℕ) ↦ (↑(k_seq n) : Y ⟶ lightToProfinite.obj (S.component n))) ⋯ }
hg : g = (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)
n : ℕᵒᵖ
⊢ (f ≫ (isLimitOfPreserves lightToProfinite S.asLimit).lift k_cone) ≫ (lightToProfinite.mapCone S.asLimitCone).π.app n =
    (k_cone.extend f).π.app n

Tactic:
simp [-Functor.mapCone_pt, -Functor.mapCone_π_app]

Premises used: CategoryTheory.Functor.mapCone_pt, CategoryTheory.Functor.mapCone_π_app
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
S : LightProfinite
inst :
  Nonempty.{u + 1}
    (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
X Y : LightProfinite
g : X ⟶ S
f : X ⟶ Y
h : Mono f
obtain :
  ∀ (h : lightToProfinite.obj Y ⟶ lightToProfinite.obj S),
    lightToProfinite.map f ≫ h = lightToProfinite.map g → ∃ (h : Y ⟶ S), f ≫ h = g
⊢ ∃ (h : Y ⟶ S), f ≫ h = g

Tactic:
obtain ⟨h, _⟩ := Injective.factors (lightToProfinite.map g) (lightToProfinite.map f)

Premises used: CategoryTheory.Functor.map, lightToProfinite, CategoryTheory.Injective.factors
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
S : LightProfinite
inst :
  Nonempty.{u + 1}
    (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
X Y : LightProfinite
g : X ⟶ S
f : X ⟶ Y
h_1 : Mono f
h : lightToProfinite.obj Y ⟶ lightToProfinite.obj S
h_2 : lightToProfinite.map f ≫ h = lightToProfinite.map g
⊢ ∃ (h : Y ⟶ S), f ≫ h = g

Tactic:
⟨lightToProfiniteFullyFaithful.preimage h, ?_⟩

Premises used: lightToProfiniteFullyFaithful, CategoryTheory.Functor.FullyFaithful.preimage, Exists.intro
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
S : LightProfinite
inst :
  Nonempty.{u + 1}
    (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
X Y : LightProfinite
g : X ⟶ S
f : X ⟶ Y
h_1 : Mono f
h : lightToProfinite.obj Y ⟶ lightToProfinite.obj S
h_2 : lightToProfinite.map f ≫ h = lightToProfinite.map g
refine : f ≫ lightToProfiniteFullyFaithful.preimage h = g
⊢ ∃ (h : Y ⟶ S), f ≫ h = g

Tactic:
refine ⟨lightToProfiniteFullyFaithful.preimage h, ?_⟩
-- Module: Mathlib.Topology.Category.LightProfinite.Injective
Goal:
S : LightProfinite
inst :
  Nonempty.{u + 1}
    (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
X Y : LightProfinite
g : X ⟶ S
f : X ⟶ Y
h_1 : Mono f
h : lightToProfinite.obj Y ⟶ lightToProfinite.obj S
h_2 : lightToProfinite.map f ≫ h = lightToProfinite.map g
apply : lightToProfinite.map (f ≫ lightToProfiniteFullyFaithful.preimage h) = lightToProfinite.map g
⊢ f ≫ lightToProfiniteFullyFaithful.preimage h = g

Tactic:
apply lightToProfiniteFullyFaithful.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective, lightToProfiniteFullyFaithful
-- Module: Mathlib.Topology.Category.LightProfinite.Limits
Goal:
⊢ FinitaryExtensive LightProfinite

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.LightProfinite.Limits
Goal:
⊢ PreservesFiniteCoproducts lightProfiniteToCompHaus

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
⊢ IsClosedEmbedding (X := OnePoint ℕ) (Y := ℝ) (⇑natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ)

Tactic:
.of_continuous_injective_isClosedMap
    natUnionInftyEmbedding.continuous ?_ ?_

Premises used: ContinuousMap.continuous, LightProfinite.natUnionInftyEmbedding, Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
refine_1 : Function.Injective (α := OnePoint ℕ) (β := ℝ) (⇑natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ)
refine_2 : IsClosedMap (X := OnePoint ℕ) (Y := ℝ) (⇑natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ)
⊢ IsClosedEmbedding (X := OnePoint ℕ) (Y := ℝ) (⇑natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ)

Tactic:
refine .of_continuous_injective_isClosedMap
    natUnionInftyEmbedding.continuous ?_ ?_
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
h :
  Eq (α := ℝ) ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) none : ℝ)
    ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) none : ℝ)
⊢ Eq (α := OnePoint ℕ) none none

Tactic:
rfl
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
m : ℕ
h :
  Eq (α := ℝ) ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) none : ℝ)
    ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) (Option.some m) : ℝ)
⊢ 0 = HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

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

Premises used: zero_eq_inv, LightProfinite.natUnionInftyEmbedding, ContinuousMap.coe_mk, one_div
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
m : ℕ
h : 0 = HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
refine_1 refine_1₁ refine_1₂ refine_1₃ : ∀ (h : False), False
⊢ none = Option.some m

Tactic:
assumption_mod_cast
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
n : ℕ
h :
  Eq (α := ℝ) ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) (Option.some n) : ℝ)
    ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) none : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = 0

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

Premises used: inv_eq_zero, LightProfinite.natUnionInftyEmbedding, ContinuousMap.coe_mk, one_div
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
n : ℕ
h : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = 0
refine_1 refine_1₁ refine_1₂ refine_1₃ : ∀ (h : False), False
⊢ Option.some n = none

Tactic:
assumption_mod_cast
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
n m : ℕ
h :
  Eq (α := ℝ) ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) (Option.some n) : ℝ)
    ((natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ) (Option.some m) : ℝ)
⊢ n = m

Tactic:
simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, inv_inj, add_left_inj,
        Nat.cast_inj] at h

Premises used: add_left_inj, Nat.cast_inj, LightProfinite.natUnionInftyEmbedding, inv_inj, ContinuousMap.coe_mk, one_div
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
n m : ℕ
h : n = m
refine_1 refine_1₁ : Option.some m = Option.some m
⊢ Option.some n = Option.some m

Tactic:
rw [h]
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
⊢ IsClosedMap (X := OnePoint ℕ) (Y := ℝ) (⇑natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ)

Tactic:
fun _ hC => (hC.isCompact.image natUnionInftyEmbedding.continuous).isClosed

Premises used: ContinuousMap.continuous, IsClosedMap, LightProfinite.natUnionInftyEmbedding, IsClosed.isCompact, IsCompact.image, IsCompact.isClosed
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
⊢ IsClosedMap (X := OnePoint ℕ) (Y := ℝ) (⇑natUnionInftyEmbedding : (a : OnePoint ℕ) → ℝ)

Tactic:
exact fun _ hC => (hC.isCompact.image natUnionInftyEmbedding.continuous).isClosed
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
⊢ MetrizableSpace (OnePoint ℕ)

Tactic:
isClosedEmbedding_natUnionInftyEmbedding.metrizableSpace

Premises used: Topology.IsEmbedding.metrizableSpace, Topology.IsClosedEmbedding.toIsEmbedding, LightProfinite.isClosedEmbedding_natUnionInftyEmbedding
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
⊢ Countable
    (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type)

Tactic:
(inferInstance : Countable <| Option _)

Premises used: inferInstance, OnePoint
-- Module: Mathlib.Topology.Category.LightProfinite.Sequence
Goal:
Y : Type u_1
inst : TopologicalSpace Y
f :
  (↑(ℕ∪{∞}.toTop (P := fun (X : TopCat.{0}) ↦
          TotallyDisconnectedSpace (↑X : Type) ∧ SecondCountableTopology (↑X : Type))) :
      Type) →
    Y
⊢ Continuous[_, inst] f ↔ Tendsto (fun (x : ℕ) ↦ f (↑x : OnePoint ℕ)) atTop (𝓝 (f ∞))

Tactic:
continuous_iff_from_nat f

Premises used: OnePoint.continuous_iff_from_nat, OnePoint
-- Module: Mathlib.Topology.Category.Locale
Goal:
α : Type u_1
inst : Frame α
⊢ (↑(unop (of α)) : Type u_1) = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.Locale
Goal:
X Y : CompHaus
a₁ a₂ : X ⟶ Y
h : (Frm.ofHom (Opens.comap (TopCat.Hom.hom a₁.hom))).op = (Frm.ofHom (Opens.comap (TopCat.Hom.hom a₂.hom))).op
⊢ a₁ = a₂

Tactic:
ConcreteCategory.ext (Opens.comap_injective (congr_arg Frm.Hom.hom
      (Quiver.Hom.op_inj h)))

Premises used: Quiver.Hom.op_inj, Frm.Hom.hom, CategoryTheory.ConcreteCategory.ext, congr_arg, TopologicalSpace.Opens.comap_injective
-- Module: Mathlib.Topology.Category.Locale
Goal:
X Y : CompHaus
a₁ a₂ : X ⟶ Y
h : (Frm.ofHom (Opens.comap (TopCat.Hom.hom a₁.hom))).op = (Frm.ofHom (Opens.comap (TopCat.Hom.hom a₂.hom))).op
⊢ a₁ = a₂

Tactic:
exact ConcreteCategory.ext (Opens.comap_injective (congr_arg Frm.Hom.hom
      (Quiver.Hom.op_inj h)))
-- Module: Mathlib.Topology.Category.Profinite.AsLimit
Goal:
X : Profinite
⊢ Function.Bijective (α :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      X.asLimitCone.pt)
    (β :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      (limitCone X.diagram).pt)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
          X.asLimitCone.pt) ((limitConeIsLimit X.diagram).lift X.asLimitCone)) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
            X.asLimitCone.pt) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
          (limitCone X.diagram).pt)

Tactic:
⟨fun a b h => ?_, fun a => ?_⟩

Premises used: And.intro, Function.Bijective