ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>this✝² : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L<VAR>H : (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv = (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)<VAR>this✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : Algebra.IsIntegral A B<GOAL>Submodule.map (↑(FractionRing.algEquiv B L)).toLinearMap (Submodule.traceDual A (FractionRing A) 1) = Submodule.traceDual A K 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>this✝² : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L<VAR>H : (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv = (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)<VAR>this✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : Algebra.IsIntegral A B<GOAL>Submodule.traceDual A K (Submodule.map (FractionRing.algEquiv B L) 1) = Submodule.traceDual A K 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : f₀ =ᶠ[𝓝 x] f₁<VAR>h' : ∀ (y : E), f₀' y = f₁' y<GOAL>HasStrictFDerivAt f₀ f₀' x ↔ HasStrictFDerivAt f₁ f₁' x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : f₀ =ᶠ[𝓝 x] f₁<VAR>h' : ∀ (y : E), f₀' y = f₁' y<GOAL>∀ (x : E × E), f₀ x.1 = f₁ x.1 ∧ f₀ x.2 = f₁ x.2 → (fun p => f₀ p.1 - f₀ p.2 - f₀' (p.1 - p.2)) x = (fun p => f₁ p.1 - f₁ p.2 - f₁' (p.1 - p.2)) x
<VAR>c : RBColor<VAR>α✝ : Type u_1<VAR>t : RBNode α✝<VAR>n : Nat<VAR>h : match c with | black => ∃ n', n = n' + 1 ∧ RedRed True t n' | red => ∃ c, t.Balanced c n<GOAL>∃ n', RedRed (c = black) t n'
<VAR>m n : ℕ<GOAL>(m + n).Coprime n ↔ m.Coprime n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s : Set α<VAR>inst✝ : Bornology α<VAR>S : Set (Set α)<VAR>hs : S.Finite<GOAL>IsBounded (⋃₀ S) ↔ ∀ s ∈ S, IsBounded s
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>k : ℕ<VAR>hi : (X ^ k).content = 1<GOAL>(X ^ (k + 1)).content = 1
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧<VAR>i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves<VAR>j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves<GOAL>-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧ = ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight (Sum.inl (i, j))⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧<VAR>i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves<VAR>j : (mk α✝ β✝ a✝¹ a✝).LeftMoves<GOAL>-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧ = ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight (Sum.inr (i, j))⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧ ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)<GOAL>∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧ ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)<VAR>i : α✝¹<VAR>j : β✝<GOAL>⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight (Sum.inl (i, j))⟧ = -⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧ ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)<VAR>i : β✝¹<VAR>j : α✝<GOAL>⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight (Sum.inr (i, j))⟧ = -⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧<VAR>i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves<VAR>j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves<GOAL>-⟦a✝³ i * -mk α✝ β✝ a✝¹ a✝⟧ = ⟦a✝³ i * mk α✝ β✝ a✝¹ a✝⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧<VAR>i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves<VAR>j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves<GOAL>-⟦mk α✝¹ β✝¹ a✝³ a✝² * -a✝ j⟧ = ⟦mk α✝¹ β✝¹ a✝³ a✝² * a✝ j⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧<VAR>i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves<VAR>j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves<GOAL>-⟦a✝³ i * -a✝ j⟧ = ⟦a✝³ i * a✝ j⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧<VAR>i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves<VAR>j : (mk α✝ β✝ a✝¹ a✝).LeftMoves<GOAL>-⟦-a✝² i * mk α✝ β✝ a✝¹ a✝⟧ = ⟦a✝² i * mk α✝ β✝ a✝¹ a✝⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧<VAR>i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves<VAR>j : (mk α✝ β✝ a✝¹ a✝).LeftMoves<GOAL>-⟦-mk α✝¹ β✝¹ a✝³ a✝² * a✝¹ j⟧ = ⟦mk α✝¹ β✝¹ a✝³ a✝² * a✝¹ j⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧<VAR>i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves<VAR>j : (mk α✝ β✝ a✝¹ a✝).LeftMoves<GOAL>-⟦-a✝² i * a✝¹ j⟧ = ⟦a✝² i * a✝¹ j⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧ ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)<VAR>i : α✝¹<VAR>j : β✝<GOAL>⟦a✝³ i * mk α✝ β✝ a✝¹ a✝⟧ = -⟦a✝³ i * -mk α✝ β✝ a✝¹ a✝⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧ ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)<VAR>i : α✝¹<VAR>j : β✝<GOAL>⟦mk α✝¹ β✝¹ a✝³ a✝² * a✝ j⟧ = -⟦mk α✝¹ β✝¹ a✝³ a✝² * -a✝ j⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧ ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)<VAR>i : α✝¹<VAR>j : β✝<GOAL>⟦a✝³ i * a✝ j⟧ = -⟦a✝³ i * -a✝ j⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧ ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)<VAR>i : β✝¹<VAR>j : α✝<GOAL>⟦a✝² i * mk α✝ β✝ a✝¹ a✝⟧ = -⟦-a✝² i * mk α✝ β✝ a✝¹ a✝⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧ ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)<VAR>i : β✝¹<VAR>j : α✝<GOAL>⟦mk α✝¹ β✝¹ a✝³ a✝² * a✝¹ j⟧ = -⟦-mk α✝¹ β✝¹ a✝³ a✝² * a✝¹ j⟧
<VAR>P : Game → Prop<VAR>α✝¹ β✝¹ : Type u_1<VAR>a✝³ : α✝¹ → PGame<VAR>a✝² : β✝¹ → PGame<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<VAR>h : (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧ ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves), P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)<VAR>i : β✝¹<VAR>j : α✝<GOAL>⟦a✝² i * a✝¹ j⟧ = -⟦-a✝² i * a✝¹ j⟧
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β : ι → Type u_4<VAR>mβ : (i : ι) → MeasurableSpace (β i)<VAR>_mα : MeasurableSpace α<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>π : ι → Set (Set Ω)<VAR>s : ι → Set Ω<VAR>S : Finset ι<VAR>f : (x : ι) → Ω → β x<VAR>inst✝ : Fintype ι<VAR>h : iIndep m κ μ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i : ι, (κ a) (s i)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β : ι → Type u_4<VAR>mβ : (i : ι) → MeasurableSpace (β i)<VAR>_mα : MeasurableSpace α<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>π : ι → Set (Set Ω)<VAR>s : ι → Set Ω<VAR>S : Finset ι<VAR>f : (x : ι) → Ω → β x<VAR>inst✝ : Fintype ι<VAR>h : iIndep m κ μ<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>a : α<VAR>ha : (κ a) (⋂ i ∈ Finset.univ, s i) = ∏ i : ι, (κ a) (s i)<GOAL>(κ a) (⋂ i, s i) = ∏ i : ι, (κ a) (s i)
<VAR>R : Type u_1<VAR>inst✝¹⁴ : CommRing R<VAR>S : Type u_2<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>I : Ideal S<VAR>inst✝¹¹ : Module.Finite R S<VAR>inst✝¹⁰ : Module.Free R S<VAR>M : Submonoid R<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁹ : CommRing Rₘ<VAR>inst✝⁸ : Algebra R Rₘ<VAR>inst✝⁷ : CommRing Sₘ<VAR>inst✝⁶ : Algebra S Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : IsLocalization M Rₘ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<GOAL>spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)
<VAR>R : Type u_1<VAR>inst✝¹⁴ : CommRing R<VAR>S : Type u_2<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>I : Ideal S<VAR>inst✝¹¹ : Module.Finite R S<VAR>inst✝¹⁰ : Module.Free R S<VAR>M : Submonoid R<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁹ : CommRing Rₘ<VAR>inst✝⁸ : Algebra R Rₘ<VAR>inst✝⁷ : CommRing Sₘ<VAR>inst✝⁶ : Algebra S Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : IsLocalization M Rₘ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>h✝ : Subsingleton R<GOAL>spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)
<VAR>R : Type u_1<VAR>inst✝¹⁴ : CommRing R<VAR>S : Type u_2<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>I : Ideal S<VAR>inst✝¹¹ : Module.Finite R S<VAR>inst✝¹⁰ : Module.Free R S<VAR>M : Submonoid R<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁹ : CommRing Rₘ<VAR>inst✝⁸ : Algebra R Rₘ<VAR>inst✝⁷ : CommRing Sₘ<VAR>inst✝⁶ : Algebra S Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : IsLocalization M Rₘ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>h✝ : Nontrivial R<GOAL>spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)
<VAR>R : Type u_1<VAR>inst✝¹⁴ : CommRing R<VAR>S : Type u_2<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>I : Ideal S<VAR>inst✝¹¹ : Module.Finite R S<VAR>inst✝¹⁰ : Module.Free R S<VAR>M : Submonoid R<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁹ : CommRing Rₘ<VAR>inst✝⁸ : Algebra R Rₘ<VAR>inst✝⁷ : CommRing Sₘ<VAR>inst✝⁶ : Algebra S Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : IsLocalization M Rₘ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>h✝ : Nontrivial R<VAR>b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S<GOAL>spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)
<VAR>R : Type u_1<VAR>inst✝¹⁴ : CommRing R<VAR>S : Type u_2<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>I : Ideal S<VAR>inst✝¹¹ : Module.Finite R S<VAR>inst✝¹⁰ : Module.Free R S<VAR>M : Submonoid R<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁹ : CommRing Rₘ<VAR>inst✝⁸ : Algebra R Rₘ<VAR>inst✝⁷ : CommRing Sₘ<VAR>inst✝⁶ : Algebra S Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : IsLocalization M Rₘ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>h✝ : Nontrivial R<VAR>b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S<GOAL>spanNorm Rₘ (map (algebraMap S Sₘ) I) = span (⇑(algebraMap R Rₘ) ∘ ⇑(Algebra.norm R) '' ↑I)
<VAR>R : Type u_1<VAR>inst✝¹⁴ : CommRing R<VAR>S : Type u_2<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>I : Ideal S<VAR>inst✝¹¹ : Module.Finite R S<VAR>inst✝¹⁰ : Module.Free R S<VAR>M : Submonoid R<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁹ : CommRing Rₘ<VAR>inst✝⁸ : Algebra R Rₘ<VAR>inst✝⁷ : CommRing Sₘ<VAR>inst✝⁶ : Algebra S Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : IsLocalization M Rₘ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>h✝ : Nontrivial R<VAR>b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S<GOAL>↑(map (algebraMap S Sₘ) I) ⊆ ⇑(Algebra.norm Rₘ) ⁻¹' ↑(Submodule.span Rₘ (⇑(algebraMap R Rₘ) ∘ ⇑(Algebra.norm R) '' ↑I))
<VAR>R : Type u_1<VAR>inst✝¹⁴ : CommRing R<VAR>S : Type u_2<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>I : Ideal S<VAR>inst✝¹¹ : Module.Finite R S<VAR>inst✝¹⁰ : Module.Free R S<VAR>M : Submonoid R<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁹ : CommRing Rₘ<VAR>inst✝⁸ : Algebra R Rₘ<VAR>inst✝⁷ : CommRing Sₘ<VAR>inst✝⁶ : Algebra S Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : IsLocalization M Rₘ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>h✝ : Nontrivial R<VAR>b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S<GOAL>↑I ⊆ ⇑(algebraMap R Rₘ) ∘ ⇑(Algebra.norm R) ⁻¹' ↑(Submodule.span Rₘ (⇑(Algebra.norm Rₘ) '' ↑(map (algebraMap S Sₘ) I)))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>z + 1 ≤ ⌈a⌉ ↔ ↑z < a
<VAR>α : Type u_1<VAR>s : Heap α<VAR>le : α → α → Bool<VAR>n : Nat<VAR>tl : Heap α<VAR>hwf : WF le n s<VAR>eq : Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl<GOAL>WF le 0 tl
<VAR>n : ℕ<VAR>f g : Vector ℕ n → ℕ<VAR>h : Vector ℕ (n + 2) → ℕ<VAR>hf : Primrec' f<VAR>hg : Primrec' g<VAR>hh : Primrec' h<GOAL>Primrec' fun v => Nat.rec (g v) (fun y IH => h (y ::ᵥ IH ::ᵥ v)) (f v)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>⊥ = x ⊓ y ⊓ x \ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ y ⊓ x \ y = x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y = (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(y ⊓ (x ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y = (y ⊓ x ⊔ x ⊓ y \ x) ⊓ x \ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(y ⊓ x ⊔ x ⊓ y \ x) ⊓ x \ y = x ⊓ y ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ y ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y = x ⊓ y \ x ⊓ x \ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ x \ y ⊓ y \ x = x \ y ⊓ y \ x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<GOAL>⟪0, x⟫_𝕜 = 0
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>hP : (↑P).relindex (↑P).normalizer ≠ 0<GOAL>¬p ∣ (↑P).index
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>hP : (↑P).relindex (↑P).normalizer ≠ 0<GOAL>¬p ∣ (↑P).relindex (↑P).normalizer * Nat.card (Sylow p G)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>hP : (↑P).relindex (↑P).normalizer ≠ 0<VAR>this : (↑(P.subtype ⋯)).Normal<GOAL>¬p ∣ (↑P).relindex (↑P).normalizer * Nat.card (Sylow p G)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>hP : (↑P).relindex (↑P).normalizer ≠ 0<VAR>this✝ : (↑(P.subtype ⋯)).Normal<VAR>this : (↑(P.subtype ⋯)).FiniteIndex<GOAL>¬p ∣ (↑P).relindex (↑P).normalizer * Nat.card (Sylow p G)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>this✝ : (↑(P.subtype ⋯)).Normal<VAR>this : (↑(P.subtype ⋯)).FiniteIndex<VAR>hP : ¬p ∣ (↑(P.subtype ⋯)).index<GOAL>¬p ∣ (↑P).relindex (↑P).normalizer * Nat.card (Sylow p G)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀✝ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>x₀ : F<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g x₀<VAR>f : F → E := fun x => g (x₀ - x)<GOAL>Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀✝ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>x₀ : F<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g x₀<VAR>f : F → E := fun x => g (x₀ - x)<VAR>If : Integrable f μ<GOAL>Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))