ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>T2Space α<VAR>f : β → αᵐᵒᵖ<GOAL>∑' (x : β), MulOpposite.unop (f x) = MulOpposite.unop (∑' (x : β), f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>StarAddMonoid α<VAR>ContinuousStar α<VAR>f : β → α<VAR>a : α<VAR>h : HasSum f a<GOAL>HasSum (fun b => star (f b)) (star a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>StarAddMonoid α<VAR>ContinuousStar α<VAR>f : β → α<VAR>hf : Summable f<GOAL>Summable fun b => star (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>StarAddMonoid α<VAR>ContinuousStar α<VAR>f : β → α<VAR>hf : Summable fun b => star (f b)<GOAL>Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>StarAddMonoid α<VAR>ContinuousStar α<VAR>f : β → α<GOAL>(Summable fun b => star (f b)) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>StarAddMonoid α<VAR>ContinuousStar α<VAR>f : β → α<GOAL>Summable (star f) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommMonoid α<VAR>TopologicalSpace α<VAR>StarAddMonoid α<VAR>ContinuousStar α<VAR>f : β → α<VAR>T2Space α<GOAL>star (∑' (b : β), f b) = ∑' (b : β), star (f b)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>self : OpenAddSubgroup G<GOAL>IsOpen (↑self).carrier
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>self : OpenSubgroup G<GOAL>IsOpen (↑self).carrier
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<GOAL>Function.Injective OpenSubgroup.toSubgroup
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<GOAL>Function.Injective OpenAddSubgroup.toAddSubgroup
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>U : OpenAddSubgroup G<GOAL>↑↑U = ↑U
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>U : OpenSubgroup G<GOAL>↑↑U = ↑U
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>U : OpenAddSubgroup G<VAR>g : G<GOAL>g ∈ ↑U ↔ g ∈ U
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>U : OpenSubgroup G<VAR>g : G<GOAL>g ∈ ↑U ↔ g ∈ U
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>U V : OpenSubgroup G<VAR>h : ∀ (x : G), x ∈ U ↔ x ∈ V<GOAL>U = V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>U V : OpenAddSubgroup G<VAR>h : ∀ (x : G), x ∈ U ↔ x ∈ V<GOAL>U = V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>U : OpenAddSubgroup G<GOAL>IsOpen ↑U
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>U : OpenSubgroup G<GOAL>IsOpen ↑U
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>U : OpenSubgroup G<GOAL>↑U ∈ 𝓝 1
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>U : OpenAddSubgroup G<GOAL>↑U ∈ 𝓝 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>x : G<GOAL>x ∈ ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>x : G<GOAL>x ∈ ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<GOAL>↑⊤ = Set.univ
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<GOAL>↑⊤ = Set.univ
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<GOAL>↑⊤ = ⊤
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<GOAL>↑⊤ = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>ContinuousMul G<VAR>U : OpenSubgroup G<GOAL>IsClosed ↑U
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>ContinuousAdd G<VAR>U : OpenAddSubgroup G<GOAL>IsClosed ↑U
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>ContinuousAdd G<VAR>U : OpenAddSubgroup G<GOAL>IsClopen ↑U
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>ContinuousMul G<VAR>U : OpenSubgroup G<GOAL>IsClopen ↑U
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>H : Type u_2<VAR>AddGroup H<VAR>TopologicalSpace H<VAR>U : OpenAddSubgroup G<VAR>V : OpenAddSubgroup H<GOAL>↑(U.sum V) = ↑U ×ˢ ↑V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>H : Type u_2<VAR>Group H<VAR>TopologicalSpace H<VAR>U : OpenSubgroup G<VAR>V : OpenSubgroup H<GOAL>↑(U.prod V) = ↑U ×ˢ ↑V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>H : Type u_2<VAR>Group H<VAR>TopologicalSpace H<VAR>U : OpenSubgroup G<VAR>V : OpenSubgroup H<GOAL>↑(U.prod V) = (↑U).prod ↑V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>H : Type u_2<VAR>AddGroup H<VAR>TopologicalSpace H<VAR>U : OpenAddSubgroup G<VAR>V : OpenAddSubgroup H<GOAL>↑(U.sum V) = (↑U).prod ↑V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>U V : OpenSubgroup G<GOAL>↑(U ⊓ V) = ↑U ∩ ↑V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>U V : OpenAddSubgroup G<GOAL>↑(U ⊓ V) = ↑U ∩ ↑V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>U V : OpenSubgroup G<GOAL>↑(U ⊓ V) = ↑U ⊓ ↑V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>U V : OpenAddSubgroup G<GOAL>↑(U ⊓ V) = ↑U ⊓ ↑V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>U V : OpenSubgroup G<VAR>x : G<GOAL>x ∈ U ⊓ V ↔ x ∈ U ∧ x ∈ V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>U V : OpenAddSubgroup G<VAR>x : G<GOAL>x ∈ U ⊓ V ↔ x ∈ U ∧ x ∈ V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>U V : OpenAddSubgroup G<GOAL>↑U ≤ ↑V ↔ U ≤ V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>U V : OpenSubgroup G<GOAL>↑U ≤ ↑V ↔ U ≤ V
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>N : Type u_2<VAR>AddGroup N<VAR>TopologicalSpace N<VAR>H : OpenAddSubgroup N<VAR>f : G →+ N<VAR>hf : Continuous ⇑f<GOAL>↑(OpenAddSubgroup.comap f hf H) = ⇑f ⁻¹' ↑H
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>N : Type u_2<VAR>Group N<VAR>TopologicalSpace N<VAR>H : OpenSubgroup N<VAR>f : G →* N<VAR>hf : Continuous ⇑f<GOAL>↑(OpenSubgroup.comap f hf H) = ⇑f ⁻¹' ↑H
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>N : Type u_2<VAR>Group N<VAR>TopologicalSpace N<VAR>H : OpenSubgroup N<VAR>f : G →* N<VAR>hf : Continuous ⇑f<GOAL>↑(OpenSubgroup.comap f hf H) = Subgroup.comap f ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>N : Type u_2<VAR>AddGroup N<VAR>TopologicalSpace N<VAR>H : OpenAddSubgroup N<VAR>f : G →+ N<VAR>hf : Continuous ⇑f<GOAL>↑(OpenAddSubgroup.comap f hf H) = AddSubgroup.comap f ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>N : Type u_2<VAR>AddGroup N<VAR>TopologicalSpace N<VAR>H : OpenAddSubgroup N<VAR>f : G →+ N<VAR>hf : Continuous ⇑f<VAR>x : G<GOAL>x ∈ OpenAddSubgroup.comap f hf H ↔ f x ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>N : Type u_2<VAR>Group N<VAR>TopologicalSpace N<VAR>H : OpenSubgroup N<VAR>f : G →* N<VAR>hf : Continuous ⇑f<VAR>x : G<GOAL>x ∈ OpenSubgroup.comap f hf H ↔ f x ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>N : Type u_2<VAR>Group N<VAR>TopologicalSpace N<VAR>P : Type u_3<VAR>Group P<VAR>TopologicalSpace P<VAR>K : OpenSubgroup P<VAR>f₂ : N →* P<VAR>hf₂ : Continuous ⇑f₂<VAR>f₁ : G →* N<VAR>hf₁ : Continuous ⇑f₁<GOAL>OpenSubgroup.comap f₁ hf₁ (OpenSubgroup.comap f₂ hf₂ K) = OpenSubgroup.comap (f₂.comp f₁) ⋯ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>N : Type u_2<VAR>AddGroup N<VAR>TopologicalSpace N<VAR>P : Type u_3<VAR>AddGroup P<VAR>TopologicalSpace P<VAR>K : OpenAddSubgroup P<VAR>f₂ : N →+ P<VAR>hf₂ : Continuous ⇑f₂<VAR>f₁ : G →+ N<VAR>hf₁ : Continuous ⇑f₁<GOAL>OpenAddSubgroup.comap f₁ hf₁ (OpenAddSubgroup.comap f₂ hf₂ K) = OpenAddSubgroup.comap (f₂.comp f₁) ⋯ K
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>ContinuousAdd G<VAR>H : AddSubgroup G<VAR>g : G<VAR>hg : ↑H ∈ 𝓝 g<GOAL>IsOpen ↑H
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>ContinuousMul G<VAR>H : Subgroup G<VAR>g : G<VAR>hg : ↑H ∈ 𝓝 g<GOAL>IsOpen ↑H
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>ContinuousMul G<VAR>H₁ H₂ : Subgroup G<VAR>h : H₁ ≤ H₂<VAR>h₁ : IsOpen ↑H₁<GOAL>IsOpen ↑H₂
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>ContinuousAdd G<VAR>H₁ H₂ : AddSubgroup G<VAR>h : H₁ ≤ H₂<VAR>h₁ : IsOpen ↑H₁<GOAL>IsOpen ↑H₂
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>ContinuousMul G<VAR>H : Subgroup G<VAR>U : OpenSubgroup G<VAR>h : ↑U ≤ H<GOAL>IsOpen ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>ContinuousAdd G<VAR>H : AddSubgroup G<VAR>U : OpenAddSubgroup G<VAR>h : ↑U ≤ H<GOAL>IsOpen ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>ContinuousAdd G<VAR>H : AddSubgroup G<VAR>h_1_int : 0 ∈ interior ↑H<GOAL>IsOpen ↑H
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>ContinuousMul G<VAR>H : Subgroup G<VAR>h_1_int : 1 ∈ interior ↑H<GOAL>IsOpen ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>ContinuousAdd G<VAR>U V : OpenAddSubgroup G<GOAL>↑(U ⊔ V) = ↑U ⊔ ↑V
<VAR>G : Type u_1<VAR>Group G<VAR>TopologicalSpace G<VAR>ContinuousMul G<VAR>U V : OpenSubgroup G<GOAL>↑(U ⊔ V) = ↑U ⊔ ↑V
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>TopologicalSpace M<VAR>TopologicalAddGroup M<VAR>Module R M<VAR>U P : Submodule R M<VAR>h : U ≤ P<VAR>hU : IsOpen ↑U<GOAL>IsOpen ↑P
<VAR>R : Type u_1<VAR>CommRing R<VAR>TopologicalSpace R<VAR>TopologicalRing R<VAR>U I : Ideal R<VAR>h : U ≤ I<VAR>hU : IsOpen ↑U<GOAL>IsOpen ↑I
<VAR>I : Type u<VAR>J : I → Prop<VAR>(i : I) → Decidable (J i)<GOAL>Continuous (Profinite.NobelingProof.Proj J)
<VAR>I : Type u<VAR>C : Set (I → Bool)<VAR>J : I → Prop<VAR>(i : I) → Decidable (J i)<GOAL>∀ (a : ↑C) (a_1 : I), ↑(Profinite.NobelingProof.ProjRestrict C J a) a_1 = Profinite.NobelingProof.Proj J (↑a) a_1
<VAR>I : Type u<VAR>C : Set (I → Bool)<VAR>J : I → Prop<VAR>(i : I) → Decidable (J i)<GOAL>Continuous (Profinite.NobelingProof.ProjRestrict C J)
<VAR>I : Type u<VAR>J : I → Prop<VAR>(i : I) → Decidable (J i)<VAR>x : I → Bool<VAR>h : ∀ (i : I), x i ≠ false → J i<GOAL>Profinite.NobelingProof.Proj J x = x
<VAR>I : Type u<VAR>C : Set (I → Bool)<VAR>J : I → Prop<VAR>(i : I) → Decidable (J i)<VAR>hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i<GOAL>Profinite.NobelingProof.π C J = C
<VAR>I : Type u<VAR>J K : I → Prop<VAR>(i : I) → Decidable (J i)<VAR>(i : I) → Decidable (K i)<VAR>h : ∀ (i : I), J i → K i<GOAL>Profinite.NobelingProof.Proj J ∘ Profinite.NobelingProof.Proj K = Profinite.NobelingProof.Proj J
<VAR>I : Type u<VAR>C : Set (I → Bool)<VAR>J K : I → Prop<VAR>(i : I) → Decidable (J i)<VAR>(i : I) → Decidable (K i)<VAR>h : ∀ (i : I), J i → K i<GOAL>Profinite.NobelingProof.π (Profinite.NobelingProof.π C K) J = Profinite.NobelingProof.π C J
<VAR>I : Type u<VAR>C : Set (I → Bool)<VAR>J K : I → Prop<VAR>(i : I) → Decidable (J i)<VAR>(i : I) → Decidable (K i)<VAR>h : ∀ (i : I), J i → K i<GOAL>∀ (a : ↑(Profinite.NobelingProof.π C K)) (a_1 : I), ↑(Profinite.NobelingProof.ProjRestricts C h a) a_1 = Profinite.NobelingProof.Proj J (↑a) a_1
<VAR>I : Type u<VAR>C : Set (I → Bool)<VAR>J K : I → Prop<VAR>(i : I) → Decidable (J i)<VAR>(i : I) → Decidable (K i)<VAR>h : ∀ (i : I), J i → K i<GOAL>Continuous (Profinite.NobelingProof.ProjRestricts C h)
<VAR>I : Type u<VAR>C : Set (I → Bool)<VAR>J K : I → Prop<VAR>(i : I) → Decidable (J i)<VAR>(i : I) → Decidable (K i)<VAR>h : ∀ (i : I), J i → K i<GOAL>Function.Surjective (Profinite.NobelingProof.ProjRestricts C h)
<VAR>I : Type u<VAR>C : Set (I → Bool)<VAR>J : I → Prop<VAR>(i : I) → Decidable (J i)<GOAL>Profinite.NobelingProof.ProjRestricts C ⋯ = id
<VAR>I : Type u<VAR>C : Set (I → Bool)<VAR>J K L : I → Prop<VAR>(i : I) → Decidable (J i)<VAR>(i : I) → Decidable (K i)<VAR>(i : I) → Decidable (L i)<VAR>hJK : ∀ (i : I), J i → K i<VAR>hKL : ∀ (i : I), K i → L i<GOAL>Profinite.NobelingProof.ProjRestricts C hJK ∘ Profinite.NobelingProof.ProjRestricts C hKL = Profinite.NobelingProof.ProjRestricts C ⋯
<VAR>I : Type u<VAR>C : Set (I → Bool)<VAR>J K : I → Prop<VAR>(i : I) → Decidable (J i)<VAR>(i : I) → Decidable (K i)<VAR>h : ∀ (i : I), J i → K i<GOAL>Profinite.NobelingProof.ProjRestricts C h ∘ Profinite.NobelingProof.ProjRestrict C K = Profinite.NobelingProof.ProjRestrict C J
<VAR>I : Type u<VAR>C : Set (I → Bool)<VAR>J : I → Prop<VAR>(i : I) → Decidable (J i)<GOAL>Function.Bijective ⇑(Profinite.NobelingProof.iso_map C J)
<VAR>I : Type u<VAR>LinearOrder I<VAR>l m : Profinite.NobelingProof.Products I<GOAL>l < m ↔ List.Lex (fun x x_1 => x < x_1) ↑l ↑m
<VAR>I : Type u<VAR>LinearOrder I<VAR>Inhabited I<VAR>i : I<VAR>l : Profinite.NobelingProof.Products I<VAR>hi : i ∈ ↑l<GOAL>i ≤ (↑l).head!
<VAR>I : Type u<VAR>LinearOrder I<VAR>Inhabited I<VAR>q l : Profinite.NobelingProof.Products I<VAR>h : q < l<VAR>hq : ↑q ≠ []<GOAL>(↑q).head! ≤ (↑l).head!
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<GOAL>Function.Injective (Profinite.NobelingProof.GoodProducts.eval C)
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<GOAL>(Profinite.NobelingProof.GoodProducts.equiv_range C).toFun = Set.rangeFactorization (Profinite.NobelingProof.GoodProducts.eval C)
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<GOAL>LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval C) ↔ LinearIndependent ℤ fun (p : ↑(Profinite.NobelingProof.GoodProducts.range C)) => ↑p
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>l : Profinite.NobelingProof.Products I<VAR>x : ↑C<GOAL>(Profinite.NobelingProof.Products.eval C l) x = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>l : Profinite.NobelingProof.Products I<VAR>J : I → Prop<VAR>h : ∀ a ∈ ↑l, J a<VAR>(j : I) → Decidable (J j)<GOAL>⇑(Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C J) l) ∘ Profinite.NobelingProof.ProjRestrict C J = ⇑(Profinite.NobelingProof.Products.eval C l)
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>l : Profinite.NobelingProof.Products I<VAR>J K : I → Prop<VAR>h : ∀ a ∈ ↑l, J a<VAR>(j : I) → Decidable (J j)<VAR>(j : I) → Decidable (K j)<VAR>hJK : ∀ (i : I), J i → K i<GOAL>⇑(Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C J) l) ∘ Profinite.NobelingProof.ProjRestricts C hJK = ⇑(Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C K) l)
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>l : Profinite.NobelingProof.Products I<VAR>J : I → Prop<VAR>(j : I) → Decidable (J j)<VAR>h : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C J) l<VAR>a : I<GOAL>a ∈ ↑l → J a
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<GOAL>⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval C)) ↔ ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.Products.eval C))
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>l : Profinite.NobelingProof.Products I<VAR>hl : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun x => x ∈ s) l<GOAL>Profinite.NobelingProof.Products.eval C l = (Profinite.NobelingProof.πJ C s) (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun x => x ∈ s) l)
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>s : Finset I<GOAL>⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.spanFinBasis C s))
<VAR>I : Type u<VAR>C : Set (I → Bool)<VAR>x : ↑C<VAR>l : List (LocallyConstant ↑C ℤ)<GOAL>l.prod x = (List.map (⇑(LocallyConstant.evalMonoidHom x)) l).prod
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x y : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)<VAR>h : y = x<GOAL>(Profinite.NobelingProof.factors C s x).prod y = 1
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)<VAR>a : I<VAR>hx : ↑x a = true<GOAL>Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun x => x ∈ s) a ∈ Profinite.NobelingProof.factors C s x
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x y : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)<VAR>a : I<VAR>ha : ↑y a = true<VAR>hx : ↑x a = false<GOAL>1 - Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun x => x ∈ s) a ∈ Profinite.NobelingProof.factors C s x
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x y : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)<VAR>h : y ≠ x<GOAL>(Profinite.NobelingProof.factors C s x).prod y = 0
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)<GOAL>(Profinite.NobelingProof.factors C s x).prod = Profinite.NobelingProof.spanFinBasis C s x
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>a : I<VAR>as : List I<VAR>ha : List.Chain' (fun x x_1 => x > x_1) (a :: as)<VAR>c : Profinite.NobelingProof.Products I →₀ ℤ<VAR>hc : ↑c.support ⊆ {m | ↑m ≤ as}<GOAL>(c.sum fun a_1 b => Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun x => x ∈ s) a * b • Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun x => x ∈ s) a_1) ∈ Submodule.span ℤ (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<GOAL>⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun x => x ∈ s)))
<VAR>I : Type u<VAR>LinearOrder I<VAR>C : Set (I → Bool)<VAR>hC : IsClosed C<VAR>f : LocallyConstant ↑C ℤ<GOAL>∃ s g, f = LocallyConstant.comap { toFun := Profinite.NobelingProof.ProjRestrict C fun x => x ∈ s, continuous_toFun := ⋯ } g
<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>⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval C))
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>i : I<VAR>ho : Profinite.NobelingProof.ord I i < Ordinal.type fun x x_1 => x < x_1<GOAL>Profinite.NobelingProof.term I ho = i
<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<GOAL>Profinite.NobelingProof.ord I (Profinite.NobelingProof.term I ho) = 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>i : I<GOAL>Profinite.NobelingProof.ord I i = o ↔ Profinite.NobelingProof.term I ho = i
<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 : Ordinal.{u}<VAR>h : Profinite.NobelingProof.Products.isGood C l<VAR>hsC : Profinite.NobelingProof.contained C o<VAR>i : I<VAR>hi : i ∈ ↑l<GOAL>Profinite.NobelingProof.ord I i < o
<VAR>I : Type u<VAR>LinearOrder I<GOAL>LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval ∅)
<VAR>I : Type u<VAR>LinearOrder I<GOAL>{m | m < Profinite.NobelingProof.Products.nil} = ∅
<VAR>I : Type u<VAR>LinearOrder I<GOAL>Profinite.NobelingProof.Products.isGood {fun x => false} Profinite.NobelingProof.Products.nil
<VAR>I : Type u<VAR>LinearOrder I<GOAL>Submodule.span ℤ (Profinite.NobelingProof.Products.eval {fun x => false} '' {Profinite.NobelingProof.Products.nil}) = ⊤
<VAR>I : Type u<VAR>LinearOrder I<GOAL>LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval {fun x => false})
<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>h : Profinite.NobelingProof.contained C o<GOAL>C = 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>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<GOAL>IsClosed (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>C : Set (I → Bool)<VAR>o : Ordinal.{u}<GOAL>Profinite.NobelingProof.contained (Profinite.NobelingProof.π C 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>g : LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ℤ<GOAL>∀ (a : ↑C), ((Profinite.NobelingProof.πs C o) g) a = g (Profinite.NobelingProof.ProjRestrict C (fun x => Profinite.NobelingProof.ord I x < o) a)
<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>f : LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ℤ<GOAL>⇑((Profinite.NobelingProof.πs C o) f) = ⇑f ∘ Profinite.NobelingProof.ProjRestrict 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>C : Set (I → Bool)<VAR>o : Ordinal.{u}<GOAL>Function.Injective ⇑(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₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>g : LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₁) ℤ<GOAL>∀ (a : ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₂)), ((Profinite.NobelingProof.πs' C h) g) a = g (Profinite.NobelingProof.ProjRestricts C ⋯ a)
<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₂<VAR>f : LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₁) ℤ<GOAL>((Profinite.NobelingProof.πs' C h) f).toFun = f.toFun ∘ Profinite.NobelingProof.ProjRestricts 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₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<GOAL>Function.Injective ⇑(Profinite.NobelingProof.πs' C h)
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>l m : Profinite.NobelingProof.Products I<VAR>o : Ordinal.{u}<VAR>h₁ : m < l<VAR>h₂ : ∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o<VAR>i : I<GOAL>i ∈ ↑m → Profinite.NobelingProof.ord I i < o
<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 : Ordinal.{u}<VAR>hlt : ∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o<GOAL>(Profinite.NobelingProof.πs C o) (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) 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>l : Profinite.NobelingProof.Products I<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>hlt : ∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o₁<GOAL>(Profinite.NobelingProof.πs' C h) (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₁) l) = Profinite.NobelingProof.Products.eval (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>l : Profinite.NobelingProof.Products I<VAR>o : Ordinal.{u}<VAR>hl : ∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o<GOAL>Profinite.NobelingProof.Products.eval C '' {m | m < l} = ⇑(Profinite.NobelingProof.πs C o) '' (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) '' {m | m < l})
<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 : ∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o₁<GOAL>Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₂) '' {m | m < l} = ⇑(Profinite.NobelingProof.πs' C h) '' (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₁) '' {m | m < l})
<VAR>I : Type u<VAR>LinearOrder I<VAR>IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>Inhabited I<VAR>l : Profinite.NobelingProof.Products I<VAR>o : Ordinal.{u}<VAR>h : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) l<VAR>hn : ↑l ≠ []<GOAL>Profinite.NobelingProof.ord I (↑l).head! < o