ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Profinite.NobelingProof.Products I<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>hl : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₁) l<GOAL>Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₂) l
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<GOAL>Function.Bijective (Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun C o)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<GOAL>(fun p => ↑p) ∘ (Profinite.NobelingProof.GoodProducts.range_equiv_smaller C o).toFun = ⇑(Profinite.NobelingProof.πs C o) ∘ fun p => ↑p
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<GOAL>LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)) ↔ LinearIndependent ℤ fun (p : ↑(Profinite.NobelingProof.GoodProducts.smaller C o)) => ↑p
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<GOAL>Profinite.NobelingProof.GoodProducts.smaller C o₁ ⊆ Profinite.NobelingProof.GoodProducts.smaller C o₂
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>l : Profinite.NobelingProof.Products I<GOAL>Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) l ↔ ∃ o' < o, Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o') l
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>hsC : Profinite.NobelingProof.contained C o<GOAL>Profinite.NobelingProof.GoodProducts.range C = ⋃ e, Profinite.NobelingProof.GoodProducts.smaller C ↑e
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>hsC : Profinite.NobelingProof.contained C o<GOAL>(fun p => ↑p) ∘ (Profinite.NobelingProof.GoodProducts.range_equiv C ho hsC).toFun = fun p => ↑p
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>hsC : Profinite.NobelingProof.contained C o<GOAL>LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval C) ↔ LinearIndependent ℤ fun (p : ↑(⋃ e, Profinite.NobelingProof.GoodProducts.smaller C ↑e)) => ↑p
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>IsClosed (Profinite.NobelingProof.C0 C ho)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>IsClosed (Profinite.NobelingProof.C1 C ho)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Profinite.NobelingProof.contained (Profinite.NobelingProof.π (Profinite.NobelingProof.C1 C ho) fun x => Profinite.NobelingProof.ord I x < o) o
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Profinite.NobelingProof.C0 C ho ∪ Profinite.NobelingProof.C1 C ho = C
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>IsClosed (Profinite.NobelingProof.C' C ho)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Profinite.NobelingProof.contained (Profinite.NobelingProof.C' C ho) o
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>o : Ordinal.{u}<GOAL>Continuous (Profinite.NobelingProof.SwapTrue o)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>f : ↑(Profinite.NobelingProof.π (Profinite.NobelingProof.C1 C ho) fun x => Profinite.NobelingProof.ord I x < o)<GOAL>Profinite.NobelingProof.SwapTrue o ↑f ∈ Profinite.NobelingProof.C1 C ho
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Continuous (Profinite.NobelingProof.CC'₀ C ho)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Continuous (Profinite.NobelingProof.CC'₁ C hsC ho)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>y : LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ℤ<GOAL>(Profinite.NobelingProof.Linear_CC' C hsC ho) ((Profinite.NobelingProof.πs C o) y) = 0
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x : I → Bool<VAR>hx : x ∈ Profinite.NobelingProof.C0 C ho<GOAL>Profinite.NobelingProof.Proj (fun x => Profinite.NobelingProof.ord I x < o) x = x
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x : I → Bool<VAR>hx : x ∈ Profinite.NobelingProof.C1 C ho<GOAL>Profinite.NobelingProof.SwapTrue o (Profinite.NobelingProof.Proj (fun x => Profinite.NobelingProof.ord I x < o) x) = x
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>f : LocallyConstant ↑C ℤ<VAR>hf : (Profinite.NobelingProof.Linear_CC' C hsC ho) f = 0<GOAL>∃ y, (Profinite.NobelingProof.πs C o) y = f
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<GOAL>CategoryTheory.Mono (ModuleCat.ofHom (Profinite.NobelingProof.πs C o))
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>(CategoryTheory.ShortComplex.mk (ModuleCat.ofHom (Profinite.NobelingProof.πs C o)) (ModuleCat.ofHom (Profinite.NobelingProof.Linear_CC' C hsC ho)) ⋯).Exact
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Profinite.NobelingProof.GoodProducts C = Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ∪ Profinite.NobelingProof.GoodProducts.MaxProducts C ho
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Function.Injective (Profinite.NobelingProof.GoodProducts.sum_to C ho)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Set.range (Profinite.NobelingProof.GoodProducts.sum_to C ho) = Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ∪ Profinite.NobelingProof.GoodProducts.MaxProducts C ho
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Profinite.NobelingProof.GoodProducts.eval C ∘ (Profinite.NobelingProof.GoodProducts.sum_equiv C hsC ho).toFun = Sum.elim (fun l => Profinite.NobelingProof.Products.eval C ↑l) fun l => Profinite.NobelingProof.Products.eval C ↑l
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval C) ↔ LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.SumEval C ho)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Set.range (Profinite.NobelingProof.GoodProducts.eval C) = Set.range (Sum.elim (fun l => Profinite.NobelingProof.Products.eval C ↑l) fun l => Profinite.NobelingProof.Products.eval C ↑l)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>Profinite.NobelingProof.GoodProducts.SumEval C ho ∘ Sum.inl = ⇑(ModuleCat.ofHom (Profinite.NobelingProof.πs C o)) ∘ Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>o : Ordinal.{u}<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x : I → Bool<GOAL>Profinite.NobelingProof.SwapTrue o x (Profinite.NobelingProof.term I ho) = true
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>x : I → Bool<GOAL>x ∈ Profinite.NobelingProof.C' C ho → x (Profinite.NobelingProof.term I ho) = false
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>o : Ordinal.{u}<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>Inhabited I<VAR>l : Profinite.NobelingProof.Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = Profinite.NobelingProof.term I ho<GOAL>↑l = Profinite.NobelingProof.term I ho :: ↑l.Tail
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>o : Ordinal.{u}<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>Inhabited I<VAR>l : Profinite.NobelingProof.Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = Profinite.NobelingProof.term I ho<VAR>hlc : List.Chain' (fun x x_1 => x > x_1) (Profinite.NobelingProof.term I ho :: ↑l.Tail)<GOAL>l = ⟨Profinite.NobelingProof.term I ho :: ↑l.Tail, hlc⟩
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>Inhabited I<VAR>l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)<GOAL>(↑↑l).head! = Profinite.NobelingProof.term I ho
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)<GOAL>↑↑l = Profinite.NobelingProof.term I ho :: ↑(↑l).Tail
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>l : List I<VAR>a : I<VAR>hla : List.Chain' (fun x x_1 => x > x_1) (a :: l)<GOAL>Profinite.NobelingProof.Products.eval C ⟨a :: l, hla⟩ = Profinite.NobelingProof.e C a * Profinite.NobelingProof.Products.eval C ⟨l, ⋯⟩
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>Inhabited I<VAR>l : Profinite.NobelingProof.Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = Profinite.NobelingProof.term I ho<GOAL>(Profinite.NobelingProof.Linear_CC' C hsC ho) (Profinite.NobelingProof.Products.eval C l) = Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.C' C ho) l.Tail
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)<GOAL>(Profinite.NobelingProof.Linear_CC' C hsC ho) (Profinite.NobelingProof.Products.eval C ↑l) = Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.C' C ho) (↑l).Tail
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>(⇑(Profinite.NobelingProof.Linear_CC' C hsC ho) ∘ fun l => Profinite.NobelingProof.Products.eval C ↑l) = fun l => Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.C' C ho) (↑l).Tail
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)<VAR>q : Profinite.NobelingProof.Products I<VAR>hq : q < (↑l).Tail<GOAL>List.Chain' (fun x x_1 => x > x_1) (Profinite.NobelingProof.term I ho :: ↑q)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>q : ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o))<VAR>l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)<GOAL>List.Lex (fun x x_1 => x < x_1) ↑↑q ↑↑l
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)))<GOAL>Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.C' C ho) (↑l).Tail
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)))<GOAL>Function.Injective (Profinite.NobelingProof.GoodProducts.MaxToGood C hC hsC ho h₁)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : Profinite.NobelingProof.contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)))<GOAL>LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.C' C ho)) → LinearIndependent (ι := ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) ℤ (⇑(ModuleCat.ofHom (Profinite.NobelingProof.Linear_CC' C hsC ho)) ∘ Profinite.NobelingProof.GoodProducts.SumEval C ho ∘ Sum.inr)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<GOAL>Profinite.NobelingProof.P I 0
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<GOAL>(∀ o' < o, Profinite.NobelingProof.P I o') → Profinite.NobelingProof.P I o
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>μ : Ordinal.{u}<GOAL>Profinite.NobelingProof.P I μ
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>hC : IsClosed C<GOAL>LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval C)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>S : Profinite<VAR>ι : ↑S.toTop → I → Bool<VAR>hι : ClosedEmbedding ι<GOAL>Module.Free ℤ (LocallyConstant ↑S.toTop ℤ)
<VAR>S : Profinite<GOAL>ClosedEmbedding (Profinite.Nobeling.ι S)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>i : ι<GOAL>TopCat.Presheaf.SheafConditionEqualizerProducts.res F U ≫ CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i))) { as := i } = F.map (TopologicalSpace.Opens.leSupr U i).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>TopCat.Presheaf.SheafConditionEqualizerProducts.res F U ≫ TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U = TopCat.Presheaf.SheafConditionEqualizerProducts.res F U ≫ TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes F U
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>(TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U).pt = F.obj (Opposite.op (iSup U))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>(TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U).ι = TopCat.Presheaf.SheafConditionEqualizerProducts.res F U
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>(TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U).π.app CategoryTheory.Limits.WalkingParallelPair.zero = TopCat.Presheaf.SheafConditionEqualizerProducts.res F U
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<GOAL>(TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U).π.app CategoryTheory.Limits.WalkingParallelPair.one = TopCat.Presheaf.SheafConditionEqualizerProducts.res F U ≫ TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op ⋙ F)<GOAL>(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj F U c).pt = c.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op ⋙ F)<VAR>Z : CategoryTheory.Limits.WalkingParallelPair<GOAL>(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj F U c).π.app Z = CategoryTheory.Limits.WalkingParallelPair.casesOn Z (CategoryTheory.Limits.Pi.lift fun i => c.π.app (Opposite.op (CategoryTheory.Pairwise.single i))) (CategoryTheory.Limits.Pi.lift fun b => c.π.app (Opposite.op (CategoryTheory.Pairwise.pair b.1 b.2)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>c c' : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op ⋙ F)<VAR>f : c ⟶ c'<GOAL>((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).map f).hom = f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op ⋙ F)<VAR>Z : CategoryTheory.Limits.WalkingParallelPair<GOAL>((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).obj c).π.app Z = CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.Limits.Pi.lift fun i => c.π.app (Opposite.op (CategoryTheory.Pairwise.single i))) (CategoryTheory.Limits.Pi.lift fun b => c.π.app (Opposite.op (CategoryTheory.Pairwise.pair b.1 b.2))) Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op ⋙ F)<GOAL>((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).obj c).pt = c.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)<VAR>x : (CategoryTheory.Pairwise ι)ᵒᵖ<GOAL>(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj F U c).π.app x = Opposite.rec' (fun x => CategoryTheory.Pairwise.casesOn x (fun i => c.π.app CategoryTheory.Limits.WalkingParallelPair.zero ≫ CategoryTheory.Limits.Pi.π (fun i => F.obj (Opposite.op (U i))) i) fun i j => c.π.app CategoryTheory.Limits.WalkingParallelPair.one ≫ CategoryTheory.Limits.Pi.π (fun p => F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j)) x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)<GOAL>(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj F U c).pt = c.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)<GOAL>((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U).obj c).pt = c.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasProducts C<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<VAR>ι : Type v'<VAR>U : ι → TopologicalSpace.Opens ↑X<VAR>c c' : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)<VAR>f : c ⟶ c'<GOAL>((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U).map f).hom = f.hom