awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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
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 ⋯) =
            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)
⊢ ∃ (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

Tactic:
obtain ⟨l, hl, rfl⟩ := hp

Premises used: rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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' < 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

Premises used: Profinite.NobelingProof.Products.limitOrdinal, Profinite.NobelingProof.contained_eq_proj
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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
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 ⋯) =
            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)
⊢ ∃ (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)

Tactic:
obtain ⟨o', ho'⟩ := hl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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)

Tactic:
⟨o', ho'.1, eval (π C (ord I · < o')) ⟨l, ho'.2⟩, ⟨l, ho'.2, rfl⟩, ?_⟩

Premises used: Profinite.NobelingProof.π, Subtype.mk, Profinite.NobelingProof.ord, And.right, And.left, And.intro, LT.lt, Exists.intro, Profinite.NobelingProof.GoodProducts.eval, rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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
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 ⋯)) =
    eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) l hl)
⊢ ∃ (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)

Tactic:
refine ⟨o', ho'.1, eval (π C (ord I · < o')) ⟨l, ho'.2⟩, ⟨l, ho'.2, rfl⟩, ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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
⊢ (π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 ⋯)) =
    eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) l hl)

Tactic:
Products.eval_πs C (Products.prop_of_isGood C _ ho'.2)

Premises used: Profinite.NobelingProof.Products.eval_πs, Profinite.NobelingProof.Products.prop_of_isGood, And.right, Profinite.NobelingProof.GoodProducts.eval
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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
⊢ (π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 ⋯)) =
    eval C (Subtype.mk (p := fun (a : Products I) ↦ Products.isGood C a) l hl)

Tactic:
exact Products.eval_πs C (Products.prop_of_isGood C _ ho'.2)

Premises used: Profinite.NobelingProof.Products.eval_πs, Profinite.NobelingProof.Products.prop_of_isGood, And.right
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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
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 ⋯))
⊢ ∃ (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:
obtain ⟨o', h, _, ⟨l, hl, rfl⟩, rfl⟩ := hp

Premises used: rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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 ⋯))

Tactic:
⟨l, ?_, (Products.eval_πs C (Products.prop_of_isGood  C _ hl)).symm⟩

Premises used: Profinite.NobelingProof.Products.eval_πs, Profinite.NobelingProof.Products.prop_of_isGood, Exists.intro, Eq.symm
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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
h₁ : Products.isGood C 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 ⋯))

Tactic:
refine ⟨l, ?_, (Products.eval_πs C (Products.prop_of_isGood  C _ hl)).symm⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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
h₁ : Products.isGood (π C fun (x : I) ↦ ord I x < o) l
⊢ Products.isGood C l

Tactic:
rw [contained_eq_proj C o hsC]

Premises used: Profinite.NobelingProof.contained_eq_proj
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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 fun (x : I) ↦ ord I x < o) l

Tactic:
Products.isGood_mono C (le_of_lt h) hl

Premises used: le_of_lt, Profinite.NobelingProof.Products.isGood_mono
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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 fun (x : I) ↦ ord I x < o) l

Tactic:
exact Products.isGood_mono C (le_of_lt h) hl

Premises used: le_of_lt, Profinite.NobelingProof.Products.isGood_mono
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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
⊢ Eq (α := (↑(range C) : Type u) → 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)
    fun (p : (↑(range C) : Type u)) ↦ (↑p : LocallyConstant (↑C : Type u) ℤ)

Tactic:
rfl

Premises used: Set.Mem, iSup, setOf, Set.range, Set.iUnion, rfl, Profinite.NobelingProof.GoodProducts.range, Set
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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
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) ℤ)
⊢ 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) ℤ)

Tactic:
rw [GoodProducts.linearIndependent_iff_range, ← range_equiv_factorization C ho hsC]

Premises used: Profinite.NobelingProof.GoodProducts.range_equiv_factorization, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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 ℤ (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:
linearIndependent_equiv (range_equiv C ho hsC)

Premises used: linearIndependent_equiv, Profinite.NobelingProof.GoodProducts.range_equiv
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
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 ℤ (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:
exact linearIndependent_equiv (range_equiv C ho hsC)

Premises used: linearIndependent_equiv, Profinite.NobelingProof.GoodProducts.range_equiv
-- Module: Mathlib.Topology.Category.Profinite.Product
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
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) : ι))
⊢ 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
-- Module: Mathlib.Topology.Category.Profinite.Product
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
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) : ι))
⊢ 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:
rw [← hy.2]

Premises used: And.right
-- Module: Mathlib.Topology.Category.Profinite.Product
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) : ι))
        ((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:
⟨y, hy.1, rfl⟩

Premises used: Set.Mem, setOf, And.left, And.intro, Exists.intro, Set.image, rfl, Profinite.IndexFunctor.obj
-- Module: Mathlib.Topology.Category.Profinite.Product
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) : ι))
        ((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:
exact ⟨y, hy.1, rfl⟩
-- Module: Mathlib.Topology.Category.Profinite.Product
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)
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
⊢ ∃ (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

Premises used: Subtype.prop
-- Module: Mathlib.Topology.Category.Profinite.Product
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)
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:
⟨⟨y, hy.1⟩, Subtype.ext hy.2⟩

Premises used: Subtype.mk, And.right, And.left, Exists.intro, Subtype.ext
-- Module: Mathlib.Topology.Category.Profinite.Product
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)
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:
exact ⟨⟨y, hy.1⟩, Subtype.ext hy.2⟩
-- Module: Mathlib.Topology.Category.Profinite.Product
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
h : ∀ (i : ι), J i → K i
⊢ Eq (α := (↑C : Type u) → (↑(obj (X := X) C J) : Type u))
    (Function.comp (β := (↑(obj (X := X) C K) : Type u))
      (⇑(map (X := X) C (J := J) (K := K) h) : (a : (↑(obj C K) : Type u)) → (↑(obj C J) : Type u))
      (⇑(π_app (X := X) C K) : (a : (↑C : Type u)) → (↑(obj C K) : Type u)))
    (⇑(π_app (X := X) C J) : (a : (↑C : Type u)) → (↑(obj C J) : Type u))

Tactic:
rfl

Premises used: Subtype.map, Set.Mem, Set.MapsTo.restrict, rfl
-- Module: Mathlib.Topology.Category.Profinite.Product
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₁ : ∀ (i : ι), (↑a : (i : ι) → X i) i = (↑b : (i : ι) → X i) i
⊢ a = b

Tactic:
ext i