awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
⊢ range C = ⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C (↑e : Ordinal.{u})
have h : ∀ (p : LocallyConstant (↑C : Type u) ℤ),
  p ∈ range C ↔
    Membership.mem (γ := Set (LocallyConstant (↑C : Type u) ℤ))
      (⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C (↑e : Ordinal.{u})) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
p : LocallyConstant (↑C : Type u) ℤ
⊢ p ∈ range C ↔
    Membership.mem (γ := Set (LocallyConstant (↑C : Type u) ℤ))
      (⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C (↑e : Ordinal.{u})) p
have h : (∃ (a : Products I) (b : Products.isGood C a),
    eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) = p) ↔
  ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
    (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
        eval (π C fun (x : I) ↦ ord I x < a)
            (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 sorry) =
          x) ∧
      (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          x =
        p
Tactic: simp only [smaller, range, Set.mem_iUnion, Set.mem_image, Set.mem_range, Subtype.exists]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
p : LocallyConstant (↑C : Type u) ℤ
⊢ (∃ (a : Products I) (b : Products.isGood C a),
      eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) = p) ↔
    ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
      (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
          eval (π C fun (x : I) ↦ ord I x < a)
              (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 ⋯) =
            x) ∧
        (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
            x =
          p
have h : ∀
  (hp :
    ∃ (a : Products I) (b : Products.isGood C a),
      eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) = p),
  ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
    (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
        eval (π C fun (x : I) ↦ ord I x < a)
            (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 sorry) =
          x) ∧
      (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          x =
        p
Tactic: refine ⟨fun hp ↦ ?_, fun hp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
p : LocallyConstant (↑C : Type u) ℤ
h :
  ∀
    (hp :
      ∃ (a : Products I) (b : Products.isGood C a),
        eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) = p),
    ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
      (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
          eval (π C fun (x : I) ↦ ord I x < a)
              (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 ⋯) =
            x) ∧
        (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
            x =
          p
⊢ (∃ (a : Products I) (b : Products.isGood C a),
      eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) = p) ↔
    ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
      (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
          eval (π C fun (x : I) ↦ ord I x < a)
              (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 ⋯) =
            x) ∧
        (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
            x =
          p
have h₁ : ∀
  (hp :
    ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
      (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
          eval (π C fun (x : I) ↦ ord I x < a)
              (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 sorry) =
            x) ∧
        (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
            x =
          p),
  ∃ (a : Products I) (b : Products.isGood C a),
    eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) = p
Tactic: refine ⟨fun hp ↦ ?_, fun hp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
p : LocallyConstant (↑C : Type u) ℤ
hp :
  ∃ (a : Products I) (b : Products.isGood C a),
    eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) = p
⊢ ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
    (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
        eval (π C fun (x : I) ↦ ord I x < a)
            (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 ⋯) =
          x) ∧
      (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          x =
        p
have h : ∀ (l : Products I) (hl : Products.isGood C l),
  ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
    (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
        eval (π C fun (x : I) ↦ ord I x < a)
            (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 sorry) =
          x) ∧
      (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          x =
        eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) l hl)
Tactic: obtain ⟨l, hl, rfl⟩ := hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
l : Products I
hl : Products.isGood C l
⊢ ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
    (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
        eval (π C fun (x : I) ↦ ord I x < a)
            (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 ⋯) =
          x) ∧
      (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          x =
        eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) l hl)
have hl₁ : ∃ o' < o, Products.isGood (π C fun (x : I) ↦ ord I x < o') l
Tactic: rw [contained_eq_proj C o hsC, Products.limitOrdinal C ho] at hl
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
l : Products I
hl_1 : Products.isGood C l
hl : ∃ o' < o, Products.isGood (π C fun (x : I) ↦ ord I x < o') l
⊢ ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
    (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
        eval (π C fun (x : I) ↦ ord I x < a)
            (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 ⋯) =
          x) ∧
      (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          x =
        eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) l hl_1)
have h : ∀ (o' : Ordinal.{u}) (ho' : o' < o ∧ Products.isGood (π C fun (x : I) ↦ ord I x < o') l),
  ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
    (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
        eval (π C fun (x : I) ↦ ord I x < a)
            (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 sorry) =
          x) ∧
      (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          x =
        eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) l hl_1)
Tactic: obtain ⟨o', ho'⟩ := hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
l : Products I
hl : Products.isGood C l
o' : Ordinal.{u}
ho' : o' < o ∧ Products.isGood (π C fun (x : I) ↦ ord I x < o') l
⊢ ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
    (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
        eval (π C fun (x : I) ↦ ord I x < a)
            (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 ⋯) =
          x) ∧
      (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          x =
        eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) l hl)
have h : (πs C o' : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o') : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
    (eval (π C fun (x : I) ↦ ord I x < o')
      (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o') l) l sorry)) =
  eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) l hl)
Tactic: refine ⟨o', ho'.1, eval (π C (ord I · < o')) ⟨l, ho'.2⟩, ⟨l, ho'.2, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
p : LocallyConstant (↑C : Type u) ℤ
hp :
  ∃ (a : Ordinal.{u}) (h : a < o) (x : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ),
    (∃ (a_1 : Products I) (h_1 : Products.isGood (π C fun (x : I) ↦ ord I x < a) a_1),
        eval (π C fun (x : I) ↦ ord I x < a)
            (Subtype.mk (p := fun (a_2 : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < a) a_2) a_1 ⋯) =
          x) ∧
      (πs C a : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < a) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
          x =
        p
⊢ ∃ (a : Products I) (b : Products.isGood C a),
    eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) = p
have h : ∀ (o' : Ordinal.{u}) (h : o' < o) (l : Products I) (hl : Products.isGood (π C fun (x : I) ↦ ord I x < o') l),
  ∃ (a : Products I) (b : Products.isGood C a),
    eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) =
      (πs C o' : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o') : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o')
          (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o') a) l sorry))
Tactic: obtain ⟨o', h, _, ⟨l, hl, rfl⟩, rfl⟩ := hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
o' : Ordinal.{u}
h : o' < o
l : Products I
hl : Products.isGood (π C fun (x : I) ↦ ord I x < o') l
⊢ ∃ (a : Products I) (b : Products.isGood C a),
    eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) a b) =
      (πs C o' : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o') : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < o')
          (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o') a) l ⋯))
have h₁ : Products.isGood C l
Tactic: refine ⟨l, ?_, (Products.eval_πs C (Products.prop_of_isGood  C _ hl)).symm⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
o' : Ordinal.{u}
h : o' < o
l : Products I
hl : Products.isGood (π C fun (x : I) ↦ ord I x < o') l
⊢ Products.isGood C l
have h₁ : Products.isGood (π C fun (x : I) ↦ ord I x < o) l
Tactic: rw [contained_eq_proj C o hsC]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
⊢ LinearIndependent (ι := { l : Products I // Products.isGood C l }) ℤ (eval C) ↔
    LinearIndependent ℤ (M := LocallyConstant (↑C : Type u) ℤ)
      fun (p : (↑(⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C (↑e : Ordinal.{u})) : Type u)) ↦
      (↑p : LocallyConstant (↑C : Type u) ℤ)
have rw : LinearIndependent ℤ (M := LocallyConstant (↑C : Type u) ℤ)
    ((fun (p : (↑(⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C (↑e : Ordinal.{u})) : Type u)) ↦
        (↑p : LocallyConstant (↑C : Type u) ℤ)) ∘
      (range_equiv C ho hsC).toFun) ↔
  LinearIndependent ℤ (M := LocallyConstant (↑C : Type u) ℤ)
    fun (p : (↑(⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C (↑e : Ordinal.{u})) : Type u)) ↦
    (↑p : LocallyConstant (↑C : Type u) ℤ)
Tactic: rw [GoodProducts.linearIndependent_iff_range, ← range_equiv_factorization C ho hsC]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (goal)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
h : ∀ (i : ι), J i → K i
x : (i : (↑K : Type u)) → X (↑i : ι)
hx : x ∈ obj (X := X) C K
⊢ Membership.mem (α := (i : (↑J : Type u)) → X (↑(Set.inclusion (s := J) (t := K) h i) : ι)) (obj (X := X) C J)
    ((precomp (X := fun (i : (↑K : Type u)) ↦ X (↑i : ι)) (Set.inclusion (s := J) (t := K) h) :
          (a : (i : (↑K : Type u)) → X (↑i : ι)) → (i : (↑J : Type u)) → X (↑(Set.inclusion h i) : ι))
        x :
      (i : (↑J : Type u)) → X (↑(Set.inclusion (s := J) (t := K) h i) : ι))
have obtain : ∀ (y : (i : ι) → X i)
  (hy : y ∈ C ∧ (precomp (X := X) (Subtype.val (p := K)) : (a : (i : ι) → X i) → (i : Subtype K) → X (↑i : ι)) y = x),
  Membership.mem (α := (i : (↑J : Type u)) → X (↑(Set.inclusion (s := J) (t := K) h i) : ι)) (obj (X := X) C J)
    ((precomp (X := fun (i : (↑K : Type u)) ↦ X (↑i : ι)) (Set.inclusion (s := J) (t := K) h) :
          (a : (i : (↑K : Type u)) → X (↑i : ι)) → (i : (↑J : Type u)) → X (↑(Set.inclusion h i) : ι))
        x :
      (i : (↑J : Type u)) → X (↑(Set.inclusion (s := J) (t := K) h i) : ι))
Tactic: obtain ⟨y, hy⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (goal)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
h : ∀ (i : ι), J i → K i
x : (i : (↑K : Type u)) → X (↑i : ι)
y : (i : ι) → X i
hy : y ∈ C ∧ (precomp (X := X) (Subtype.val (p := K)) : (a : (i : ι) → X i) → (i : Subtype K) → X (↑i : ι)) y = x
⊢ Membership.mem (α := (i : (↑J : Type u)) → X (↑(Set.inclusion (s := J) (t := K) h i) : ι)) (obj (X := X) C J)
    ((precomp (X := fun (i : (↑K : Type u)) ↦ X (↑i : ι)) (Set.inclusion (s := J) (t := K) h) :
          (a : (i : (↑K : Type u)) → X (↑i : ι)) → (i : (↑J : Type u)) → X (↑(Set.inclusion h i) : ι))
        x :
      (i : (↑J : Type u)) → X (↑(Set.inclusion (s := J) (t := K) h i) : ι))
have rw : Membership.mem (α := (i : (↑J : Type u)) → X (↑(Set.inclusion (s := J) (t := K) h i) : ι)) (obj (X := X) C J)
  ((precomp (X := fun (i : (↑K : Type u)) ↦ X (↑i : ι)) (Set.inclusion (s := J) (t := K) h) :
        (a : (i : (↑K : Type u)) → X (↑i : ι)) → (i : (↑J : Type u)) → X (↑(Set.inclusion h i) : ι))
      ((precomp (X := X) (Subtype.val (p := K)) : (a : (i : ι) → X i) → (i : Subtype K) → X (↑i : ι)) y :
        (i : Subtype K) → X (↑i : ι)) :
    (i : (↑J : Type u)) → X (↑(Set.inclusion (s := J) (t := K) h i) : ι))
Tactic: rw [← hy.2]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (goal)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J : ι → Prop
x : (↑(obj (X := X) C J) : Type u)
⊢ ∃ (a : (↑C : Type u)), (π_app (X := X) C J : (a : (↑C : Type u)) → (↑(obj C J) : Type u)) a = x
have obtain : ∀ (y : (i : ι) → X i)
  (hy :
    y ∈ C ∧
      (precomp (X := X) (Subtype.val (p := J)) : (a : (i : ι) → X i) → (i : Subtype J) → X (↑i : ι)) y =
        (↑x : (i : { i : ι // J i }) → X (↑i : ι))),
  ∃ (a : (↑C : Type u)), (π_app (X := X) C J : (a : (↑C : Type u)) → (↑(obj C J) : Type u)) a = x
Tactic: obtain ⟨y, hy⟩ := x.prop
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (goal)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : (↑C : Type u)
h :
  ∀ (J : Finset ι),
    Eq (α := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
      ((π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) a :
        (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
      ((π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) b :
        (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
⊢ a = b
have a₁ : ∀ (i : ι), (↑a : (i : ι) → X i) i = (↑b : (i : ι) → X i) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (hypothesis)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : (↑C : Type u)
h :
  ∀ (J : Finset ι),
    Eq (α := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
      ((π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) a :
        (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
      ((π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) b :
        (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
i : ι
⊢ (↑a : (i : ι) → X i) i = (↑b : (i : ι) → X i) i
have h₁ : Eq (α := (↑(obj (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) : Type u))
  ((π_app (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x :
        (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ {i}) : Type u))
      a :
    (↑(obj (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) : Type u))
  ((π_app (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x :
        (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ {i}) : Type u))
      b :
    (↑(obj (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) : Type u))
Tactic: specialize h ({i} : Finset ι)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (hypothesis)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : (↑C : Type u)
i : ι
h :
  Eq (α := (↑(obj (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) : Type u))
    ((π_app (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x :
          (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ {i}) : Type u))
        a :
      (↑(obj (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) : Type u))
    ((π_app (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x :
          (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ {i}) : Type u))
        b :
      (↑(obj (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) : Type u))
⊢ (↑a : (i : ι) → X i) i = (↑b : (i : ι) → X i) i
have h₁ : Eq.{u + 1} (α := (i_1 : ↥{i}) → X (↑i_1 : ι))
  (↑((π_app (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x :
          (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ {i}) : Type u))
        a) :
    (i_1 : ↥{i}) → X (↑i_1 : ι))
  (↑((π_app (X := X) C fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x :
          (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ {i}) : Type u))
        b) :
    (i_1 : ↥{i}) → X (↑i_1 : ι))
Tactic: rw [Subtype.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (goal)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J_1 K : ι → Prop
inst_1 : ∀ (i : ι), T2Space (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
J : (Finset ι)ᵒᵖ
⊢ CompactSpace.{u} (↑(obj (X := X) C fun (x : ι) ↦ x ∈ unop J) : Type u)
have rw : IsCompact (X := (i : ↥(unop J)) → X (↑i : ι)) (obj (X := X) C fun (x : ι) ↦ x ∈ unop J)
Tactic: rw [← isCompact_iff_compactSpace]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (goal)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J_1 K : ι → Prop
inst_1 : ∀ (i : ι), T2Space (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace.{u} (↑C : Type u)
a :
  (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 (indexFunctor (X := X) (C := C) hC)).pt
J : Finset ι
s : (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)
⊢ IsClosed (X := (↑C : Type u))
    (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
      (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) {s})
have refine : IsClosed (X := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)) {s}
Tactic: refine IsClosed.preimage (π_app C (· ∈ J)).continuous ?_