ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>k✝ : ℕ<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>h : N₁.normalizer = N₁<VAR>k : ℕ<GOAL>ucs k ⊥ ≤ ucs k N₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f'✝ : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f' : α → E' × F'<GOAL>(fun x => (f' x).2) =O[l] f'
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>W a : Submodule R M<VAR>a✝ : Submodule R (Module.Dual R M)<GOAL>(⇑OrderDual.toDual ∘ dualAnnihilator) a ≤ OrderDual.toDual a✝ ↔ a ≤ (dualCoannihilator ∘ ⇑OrderDual.ofDual) (OrderDual.toDual a✝)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>W a : Submodule R M<VAR>a✝ : Submodule R (Module.Dual R M)<GOAL>a✝ ≤ a.dualAnnihilator ↔ a ≤ a✝.dualCoannihilator
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R M<VAR>i j : ι<GOAL>b.equivFun (b i) j = if i = j then 1 else 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝² : FunLike F (Set α) ℝ≥0∞<VAR>inst✝¹ : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t✝ : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>t : ℕ → Set α<GOAL>(fun x x_1 => x ≤ x_1) (μ (⨆ i, t i)) (∑' (i : ℕ), μ (t i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<GOAL>e = s((Quot.out e).2, (Quot.out e).1)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.obj Y'<VAR>h : X' ⟶ G.obj Y<VAR>k : Y ⟶ Y'<VAR>w : f ≫ g = h ≫ G.map k<GOAL>F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T₁ T₂ : Triangle Cᵒᵖ<VAR>hT₁ : T₁ ∈ distinguishedTriangles C<VAR>hT₂ : T₂ ∈ distinguishedTriangles C<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T₁ T₂ : Triangle Cᵒᵖ<VAR>hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles<VAR>hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T₁ T₂ : Triangle Cᵒᵖ<VAR>hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles<VAR>hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>c : (Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂)).obj₁ ⟶ (Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁)).obj₁<VAR>hc₁ : (Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂)).mor₁ ≫ b.unop = c ≫ (Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁)).mor₁<VAR>hc₂ : (Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂)).mor₃ ≫ (shiftFunctor C 1).map c = a.unop ≫ (Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁)).mor₃<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T₁ T₂ : Triangle Cᵒᵖ<VAR>hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles<VAR>hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃<VAR>hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop<VAR>hc₂ : (((opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁).unop ≫ (shiftFunctor C 1).map T₂.mor₃.unop) ≫ (shiftFunctor C 1).map c = a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T₁ T₂ : Triangle Cᵒᵖ<VAR>hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles<VAR>hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃<VAR>hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop<VAR>hc₂ : ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫ (((opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁).unop ≫ (shiftFunctor C 1).map T₂.mor₃.unop) ≫ (shiftFunctor C 1).map c = ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫ a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T₁ T₂ : Triangle Cᵒᵖ<VAR>hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles<VAR>hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃<VAR>hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop<VAR>hc₂ : (shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map c = ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫ a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T₁ T₂ : Triangle Cᵒᵖ<VAR>hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles<VAR>hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃<VAR>hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop<VAR>hc₂ : (shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map c = ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫ a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop<GOAL>(T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a).unop = (c.op ≫ T₂.mor₃).unop
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T₁ T₂ : Triangle Cᵒᵖ<VAR>hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles<VAR>hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃<VAR>hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop<VAR>hc₂ : (shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map c = ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫ a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop<GOAL>(shiftFunctor C 1).map (T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a).unop = (shiftFunctor C 1).map (c.op ≫ T₂.mor₃).unop
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T₁ T₂ : Triangle Cᵒᵖ<VAR>hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles<VAR>hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃<VAR>hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop<VAR>hc₂ : (shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map c = ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫ a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop<GOAL>(shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map a).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop = (((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map (a ≫ (opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁)).unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app (Opposite.op ((shiftFunctor C 1).obj (Opposite.unop ((shiftFunctor Cᵒᵖ 1).obj T₂.obj₁))))).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop
<VAR>α : Type u<VAR>inst✝ : Semiring α<VAR>x : α<GOAL>∑ i ∈ range 1, x ^ i = 1
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β<VAR>hf : Surjective f<VAR>s : Multiset β<GOAL>∃ a, map f a = s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β<VAR>hf : Surjective f<GOAL>∃ a, map f a = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β<VAR>hf : Surjective f<VAR>x : β<VAR>s : Multiset β<VAR>ih : ∃ a, map f a = s<GOAL>∃ a, map f a = x ::ₘ s
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Fintype R<VAR>R' : Type v<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : IsDomain R'<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>F' : Type u_2<VAR>inst✝¹ : Field F'<VAR>inst✝ : Fintype F'<VAR>χ : MulChar F F'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>hch₁ : ringChar F' ≠ ringChar F<VAR>hch₂ : ringChar F' ≠ 2<GOAL>(χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = χ ↑(Fintype.card F')
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Fintype R<VAR>R' : Type v<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : IsDomain R'<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>F' : Type u_2<VAR>inst✝¹ : Field F'<VAR>inst✝ : Fintype F'<VAR>χ : MulChar F F'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>hch₁ : ringChar F' ≠ ringChar F<VAR>hch₂ : ringChar F' ≠ 2<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<GOAL>(χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = χ ↑(Fintype.card F')
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Fintype R<VAR>R' : Type v<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : IsDomain R'<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>F' : Type u_2<VAR>inst✝¹ : Field F'<VAR>inst✝ : Fintype F'<VAR>χ : MulChar F F'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>hch₁ : ringChar F' ≠ ringChar F<VAR>hch₂ : ringChar F' ≠ 2<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>n' : ℕ+<VAR>hp' : Nat.Prime (ringChar F')<VAR>hc' : Fintype.card F' = ringChar F' ^ ↑n'<GOAL>(χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = χ ↑(Fintype.card F')
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Fintype R<VAR>R' : Type v<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : IsDomain R'<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>F' : Type u_2<VAR>inst✝¹ : Field F'<VAR>inst✝ : Fintype F'<VAR>χ : MulChar F F'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>hch₁ : ringChar F' ≠ ringChar F<VAR>hch₂ : ringChar F' ≠ 2<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>n' : ℕ+<VAR>hp' : Nat.Prime (ringChar F')<VAR>hc' : Fintype.card F' = ringChar F' ^ ↑n'<VAR>ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁<VAR>FF' : Type u_2 := CyclotomicField ψ.n F'<GOAL>(χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = χ ↑(Fintype.card F')
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Fintype R<VAR>R' : Type v<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : IsDomain R'<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>F' : Type u_2<VAR>inst✝¹ : Field F'<VAR>inst✝ : Fintype F'<VAR>χ : MulChar F F'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>hch₁ : ringChar F' ≠ ringChar F<VAR>hch₂ : ringChar F' ≠ 2<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>n' : ℕ+<VAR>hp' : Nat.Prime (ringChar F')<VAR>hc' : Fintype.card F' = ringChar F' ^ ↑n'<VAR>ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁<VAR>FF' : Type u_2 := CyclotomicField ψ.n F'<VAR>hchar : ringChar F' = ringChar FF'<GOAL>(χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = χ ↑(Fintype.card F')
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Fintype R<VAR>R' : Type v<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : IsDomain R'<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>F' : Type u_2<VAR>inst✝¹ : Field F'<VAR>inst✝ : Fintype F'<VAR>χ : MulChar F F'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>hch₁ : ringChar F' ≠ ringChar F<VAR>hch₂ : ringChar F' ≠ 2<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>n' : ℕ+<VAR>hp' : Nat.Prime (ringChar F')<VAR>hc' : Fintype.card F' = ringChar F' ^ ↑n'<VAR>ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁<VAR>FF' : Type u_2 := CyclotomicField ψ.n F'<VAR>hchar : ringChar F' = ringChar FF'<GOAL>(algebraMap F' FF') ((χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2)) = (algebraMap F' FF') (χ ↑(Fintype.card F'))
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Fintype R<VAR>R' : Type v<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : IsDomain R'<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>F' : Type u_2<VAR>inst✝¹ : Field F'<VAR>inst✝ : Fintype F'<VAR>χ : MulChar F F'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>hch₁ : ringChar F' ≠ ringChar F<VAR>hch₂ : ringChar F' ≠ 2<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>n' : ℕ+<VAR>hp' : Nat.Prime (ringChar F')<VAR>hc' : Fintype.card F' = ringChar F' ^ ↑n'<VAR>ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁<VAR>FF' : Type u_2 := CyclotomicField ψ.n F'<VAR>hchar : ringChar F' = ringChar FF'<GOAL>((algebraMap F' FF') (χ (-1)) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) = (algebraMap F' FF') (χ (↑(ringChar FF') ^ ↑n'))
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Fintype R<VAR>R' : Type v<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : IsDomain R'<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>F' : Type u_2<VAR>inst✝¹ : Field F'<VAR>inst✝ : Fintype F'<VAR>χ : MulChar F F'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>hch₁ : ringChar F' ≠ ringChar F<VAR>hch₂ : ringChar F' ≠ 2<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>n' : ℕ+<VAR>hp' : Nat.Prime (ringChar F')<VAR>hc' : Fintype.card F' = ringChar F' ^ ↑n'<VAR>ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁<VAR>FF' : Type u_2 := CyclotomicField ψ.n F'<VAR>hchar : ringChar F' = ringChar FF'<GOAL>((χ.ringHomComp (algebraMap F' FF')) (-1) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) = (χ.ringHomComp (algebraMap F' FF')) (↑(ringChar FF') ^ ↑n')
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Fintype R<VAR>R' : Type v<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : IsDomain R'<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>F' : Type u_2<VAR>inst✝¹ : Field F'<VAR>inst✝ : Fintype F'<VAR>χ : MulChar F F'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>hch₁ : ringChar F' ≠ ringChar F<VAR>hch₂ : ringChar F' ≠ 2<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>n' : ℕ+<VAR>hp' : Nat.Prime (ringChar F')<VAR>hc' : Fintype.card F' = ringChar F' ^ ↑n'<VAR>ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁<VAR>FF' : Type u_2 := CyclotomicField ψ.n F'<VAR>hchar : ringChar F' = ringChar FF'<VAR>this : Fact (Nat.Prime (ringChar F'))<GOAL>((χ.ringHomComp (algebraMap F' FF')) (-1) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) = (χ.ringHomComp (algebraMap F' FF')) (↑(ringChar FF') ^ ↑n')
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Fintype R<VAR>R' : Type v<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : IsDomain R'<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>F' : Type u_2<VAR>inst✝¹ : Field F'<VAR>inst✝ : Fintype F'<VAR>χ : MulChar F F'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>hch₁ : ringChar F' ≠ ringChar F<VAR>hch₂ : ringChar F' ≠ 2<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>n' : ℕ+<VAR>hp' : Nat.Prime (ringChar F')<VAR>hc' : Fintype.card F' = ringChar F' ^ ↑n'<VAR>ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁<VAR>FF' : Type u_2 := CyclotomicField ψ.n F'<VAR>hchar : ringChar F' = ringChar FF'<VAR>this✝ : Fact (Nat.Prime (ringChar F'))<VAR>this : Fact (Nat.Prime (ringChar FF'))<GOAL>((χ.ringHomComp (algebraMap F' FF')) (-1) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) = (χ.ringHomComp (algebraMap F' FF')) (↑(ringChar FF') ^ ↑n')
<VAR>R : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Fintype R<VAR>R' : Type v<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : IsDomain R'<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Fintype F<VAR>F' : Type u_2<VAR>inst✝¹ : Field F'<VAR>inst✝ : Fintype F'<VAR>χ : MulChar F F'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>hch₁✝ : ringChar F' ≠ ringChar F<VAR>hch₂ : ringChar F' ≠ 2<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>n' : ℕ+<VAR>hp' : Nat.Prime (ringChar F')<VAR>hc' : Fintype.card F' = ringChar F' ^ ↑n'<VAR>ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁✝<VAR>FF' : Type u_2 := CyclotomicField ψ.n F'<VAR>hch₁ : IsUnit ↑(ringChar FF')<VAR>hchar : ringChar F' = ringChar FF'<VAR>this✝ : Fact (Nat.Prime (ringChar F'))<VAR>this : Fact (Nat.Prime (ringChar FF'))<GOAL>((χ.ringHomComp (algebraMap F' FF')) (-1) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) = (χ.ringHomComp (algebraMap F' FF')) (↑(ringChar FF') ^ ↑n')
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>x ≤ y ∨ y ⧏ x
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>x ≤ y ∨ ¬x ≤ y
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set Y<GOAL>frontier (univ ×ˢ s) = univ ×ˢ frontier s
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>ι : Type u_3<VAR>B : ι → Set X<VAR>hB : ∀ (i : ι), IsBlock G (B i)<VAR>hι : ¬IsEmpty ι<GOAL>IsBlock G (⋂ i, B i)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>ι : Type u_3<VAR>B : ι → Set X<VAR>hB : ∀ (i : ι), IsBlock G (B i)<VAR>hι : ¬IsEmpty ι<GOAL>∀ (g : G), g • ⋂ i, B i = ⋂ i, B i ∨ Disjoint (g • ⋂ i, B i) (⋂ i, B i)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>ι : Type u_3<VAR>B : ι → Set X<VAR>hB : ∀ (i : ι), IsBlock G (B i)<VAR>hι : ¬IsEmpty ι<VAR>g : G<GOAL>g • ⋂ i, B i = ⋂ i, B i ∨ Disjoint (g • ⋂ i, B i) (⋂ i, B i)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>ι : Type u_3<VAR>B : ι → Set X<VAR>hB : ∀ (i : ι), IsBlock G (B i)<VAR>hι : ¬IsEmpty ι<VAR>g : G<GOAL>⋂ i, g • B i = ⋂ i, B i ∨ Disjoint (⋂ i, g • B i) (⋂ i, B i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<GOAL>(comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>h✝ : IsEmpty β<GOAL>(comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>h✝ : Nonempty β<GOAL>(comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f : C(X, ℝ≥0)<GOAL>φ.realContinuousMapOfNNReal ({ toFun := toReal, continuous_toFun := continuous_coe }.comp f) = φ f
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f : C(X, ℝ≥0)<GOAL>φ ({ toFun := toReal, continuous_toFun := continuous_coe }.comp f).toNNReal - φ (-{ toFun := toReal, continuous_toFun := continuous_coe }.comp f).toNNReal = φ f
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f : C(X, ℝ≥0)<GOAL>φ ({ toFun := toReal, continuous_toFun := continuous_coe }.comp f).toNNReal = φ f
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f : C(X, ℝ≥0)<GOAL>φ (-{ toFun := toReal, continuous_toFun := continuous_coe }.comp f).toNNReal = φ 0