ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u<VAR>inst✝⁹ : CommRing k<VAR>G : Type u<VAR>inst✝⁸ : Group G<VAR>V : Type v<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module k V<VAR>inst✝⁵ : Module (MonoidAlgebra k G) V<VAR>inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V<VAR>W : Type w<VAR>inst✝³ : AddCommGroup W<VAR>inst✝² : Module k W<VAR>inst✝¹ : Module (MonoidAlgebra k G) W<VAR>inst✝ : IsScalarTower k (MonoidAlgebra k G) W<VAR>π : W →ₗ[k] V<VAR>i : V →ₗ[MonoidAlgebra k G] W<VAR>h : ∀ (v : V), π (i v) = v<VAR>g : G<VAR>v : V<GOAL>(π.conjugate g) (i v) = v
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p q : α → Prop<VAR>a' : α<GOAL>∃! a, a = a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>mα : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : MeasurableEmbedding g<VAR>hf : MeasurableEmbedding f<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (g ∘ f '' s)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderBot α<VAR>a b x : α<GOAL>⊥ ⋖ a ↔ IsAtom a
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>I : Ideal R<VAR>x✝ : P'<GOAL>x✝ ∈ (canonicalEquiv S P P') ↑I ↔ x✝ ∈ ↑I
<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<GOAL>IsClosed (range inl)
<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<GOAL>IsOpen (range inr)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
<VAR>hp : Fact (Nat.Prime 2)<GOAL>∃ a b k, 0 < k ∧ k < 2 ∧ a ^ 2 + b ^ 2 + 1 = k * 2
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hodd : Odd p<GOAL>∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hodd : Odd p<VAR>a b : ℕ<VAR>ha : a ≤ p / 2<VAR>hb : b ≤ p / 2<VAR>hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]<GOAL>∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hodd : Odd p<VAR>a b : ℕ<VAR>ha : a ≤ p / 2<VAR>hb : b ≤ p / 2<VAR>hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]<VAR>k : ℤ<VAR>hk : ↑a ^ 2 + ↑b ^ 2 - -1 = ↑p * k<GOAL>∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hodd : Odd p<VAR>a b : ℕ<VAR>ha : a ≤ p / 2<VAR>hb : b ≤ p / 2<VAR>hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]<VAR>k : ℤ<VAR>hk : ↑a ^ 2 + ↑b ^ 2 + 1 = k * ↑p<GOAL>∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hodd : Odd p<VAR>a b : ℕ<VAR>ha : a ≤ p / 2<VAR>hb : b ≤ p / 2<VAR>hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]<VAR>k : ℤ<VAR>hk : ↑a ^ 2 + ↑b ^ 2 + 1 = k * ↑p<VAR>hk₀ : 0 < k<GOAL>∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hodd : Odd p<VAR>a b : ℕ<VAR>ha : a ≤ p / 2<VAR>hb : b ≤ p / 2<VAR>hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]<VAR>k : ℕ<VAR>hk : ↑a ^ 2 + ↑b ^ 2 + 1 = ↑k * ↑p<VAR>hk₀ : 0 < ↑k<GOAL>∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hodd : Odd p<VAR>a b : ℕ<VAR>ha : a ≤ p / 2<VAR>hb : b ≤ p / 2<VAR>hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]<VAR>k : ℕ<VAR>hk : ↑a ^ 2 + ↑b ^ 2 + 1 = ↑k * ↑p<VAR>hk₀ : 0 < ↑k<GOAL>k < p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hodd : Odd p<VAR>a b : ℕ<VAR>ha : a ≤ p / 2<VAR>hb : b ≤ p / 2<VAR>hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]<VAR>k : ℕ<VAR>hk₀ : 0 < ↑k<VAR>hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p<GOAL>k < p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hodd : Odd p<VAR>a b : ℕ<VAR>ha : a ≤ p / 2<VAR>hb : b ≤ p / 2<VAR>hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]<VAR>k : ℕ<VAR>hk₀ : 0 < ↑k<VAR>hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p<GOAL>2 * a < p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hodd : Odd p<VAR>a b : ℕ<VAR>ha : a ≤ p / 2<VAR>hb : b ≤ p / 2<VAR>hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]<VAR>k : ℕ<VAR>hk₀ : 0 < ↑k<VAR>hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p<GOAL>2 * b < p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hodd : Odd p<VAR>a b : ℕ<VAR>ha : a ≤ p / 2<VAR>hb : b ≤ p / 2<VAR>hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]<VAR>k : ℕ<VAR>hk₀ : 0 < ↑k<VAR>hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p<GOAL>2 * 1 < p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hodd : Odd p<VAR>a b : ℕ<VAR>ha : a ≤ p / 2<VAR>hb : b ≤ p / 2<VAR>hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]<VAR>k : ℕ<VAR>hk₀ : 0 < ↑k<VAR>hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p<GOAL>2 * 0 < p
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>g : G<VAR>q : G ⧸ H<GOAL>↑(H.transferFunction g q) = q
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>x : L<VAR>hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)<VAR>hx' : ¬x = 0<GOAL>∃ n, n • x = ⁅coroot α, x⁆
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>x : L<VAR>hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)<VAR>hx' : ¬x = 0<VAR>h e f : L<VAR>isSl2 : IsSl2Triple h e f<VAR>he : e ∈ rootSpace H ⇑α<VAR>hf : f ∈ rootSpace H (-⇑α)<GOAL>∃ n, n • x = ⁅coroot α, x⁆
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>x : L<VAR>hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)<VAR>hx' : ¬x = 0<VAR>e f : L<VAR>he : e ∈ rootSpace H ⇑α<VAR>hf : f ∈ rootSpace H (-⇑α)<VAR>isSl2 : IsSl2Triple (↑(coroot α)) e f<GOAL>∃ n, n • x = ⁅coroot α, x⁆
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>x : L<VAR>hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)<VAR>hx' : ¬x = 0<VAR>e f : L<VAR>he : e ∈ rootSpace H ⇑α<VAR>hf : f ∈ rootSpace H (-⇑α)<VAR>isSl2 : IsSl2Triple (↑(coroot α)) e f<VAR>this : isSl2.HasPrimitiveVectorWith x ((chainTop (⇑α) β) (coroot α))<GOAL>∃ n, n • x = ⁅coroot α, x⁆
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>x : L<VAR>hx : x ∈ rootSpace H ⇑(chainTop (⇑α) β)<VAR>hx' : ¬x = 0<VAR>e f : L<VAR>he : e ∈ rootSpace H ⇑α<VAR>hf : f ∈ rootSpace H (-⇑α)<VAR>isSl2 : IsSl2Triple (↑(coroot α)) e f<VAR>this : isSl2.HasPrimitiveVectorWith x ((chainTop (⇑α) β) (coroot α))<VAR>μ : ℕ<VAR>hμ : (chainTop (⇑α) β) (coroot α) = ↑μ<GOAL>∃ n, n • x = ⁅coroot α, x⁆
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : Zero β✝<VAR>inst✝¹ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β✝<VAR>β : Type u_5<VAR>inst✝ : AddMonoid β<VAR>f g : α →ₛ β<VAR>hf : f.FinMeasSupp μ<VAR>hg : g.FinMeasSupp μ<GOAL>(f + g).FinMeasSupp μ
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>inst✝² : Zero β✝<VAR>inst✝¹ : Zero γ<VAR>μ : Measure α<VAR>f✝ : α →ₛ β✝<VAR>β : Type u_5<VAR>inst✝ : AddMonoid β<VAR>f g : α →ₛ β<VAR>hf : f.FinMeasSupp μ<VAR>hg : g.FinMeasSupp μ<GOAL>(map (fun p => p.1 + p.2) (f.pair g)).FinMeasSupp μ
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f g : ↥(lp (fun i => ℝ) ⊤)<VAR>n : ℕ<VAR>C : ℝ<VAR>inst✝² : MetricSpace α✝<VAR>x : ℕ → α✝<VAR>a b : α✝<VAR>α : Type u<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : SeparableSpace α<GOAL>∃ f, Isometry f
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f g : ↥(lp (fun i => ℝ) ⊤)<VAR>n : ℕ<VAR>C : ℝ<VAR>inst✝² : MetricSpace α✝<VAR>x : ℕ → α✝<VAR>a b : α✝<VAR>α : Type u<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : SeparableSpace α<VAR>h : univ = ∅<GOAL>∃ f, Isometry f
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f g : ↥(lp (fun i => ℝ) ⊤)<VAR>n : ℕ<VAR>C : ℝ<VAR>inst✝² : MetricSpace α✝<VAR>x : ℕ → α✝<VAR>a b : α✝<VAR>α : Type u<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : SeparableSpace α<VAR>h : univ.Nonempty<GOAL>∃ f, Isometry f
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t<VAR>hnzd : ↑n.factorial ∈ nonZeroDivisors R<GOAL>n < rootMultiplicity t p
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t<VAR>hnzd : ↑n.factorial ∈ nonZeroDivisors R<VAR>h' : rootMultiplicity t p ≤ n<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>hnzd : ↑n.factorial ∈ nonZeroDivisors R<VAR>h' : rootMultiplicity t p ≤ n<VAR>hroot : ((⇑derivative)^[rootMultiplicity t p] p).IsRoot t<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>hnzd : ↑n.factorial ∈ nonZeroDivisors R<VAR>h' : rootMultiplicity t p ≤ n<VAR>hroot : (rootMultiplicity t p).factorial • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>hnzd : ↑n.factorial ∈ nonZeroDivisors R<VAR>h' : rootMultiplicity t p ≤ n<VAR>hroot : (rootMultiplicity t p).factorial • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0<VAR>q : R<VAR>hq : ↑n.factorial = ↑(rootMultiplicity t p).factorial * q<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>h' : rootMultiplicity t p ≤ n<VAR>hroot : (rootMultiplicity t p).factorial • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0<VAR>q : R<VAR>hnzd : ↑(rootMultiplicity t p).factorial ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R<VAR>hq : ↑n.factorial = ↑(rootMultiplicity t p).factorial * q<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>h' : rootMultiplicity t p ≤ n<VAR>hroot : eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0<VAR>q : R<VAR>hnzd : ↑(rootMultiplicity t p).factorial ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R<VAR>hq : ↑n.factorial = ↑(rootMultiplicity t p).factorial * q<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure α<VAR>s : Set α<GOAL>(sum μ) s = 0 ↔ ∀ (i : ι), (μ i) s = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<GOAL>a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<GOAL>a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
<VAR>a b c d✝ m n k : ℕ<VAR>p q : ℕ → Prop<VAR>ha : 0 < a<VAR>d : ℕ<GOAL>a * c = a * b * d ↔ c = b * d
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f✝ : α → β<VAR>ι : Sort u_2<VAR>T : TopologicalSpace α<VAR>f : β → α<VAR>hf : Surjective f<VAR>a : β<GOAL>map f (𝓝 a) = 𝓝 (f a)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{u₂, u₁} C<VAR>inst✝ : GaloisCategory C<VAR>X : C<GOAL>∃ ι, ∃ (x : Finite ι), ∃ f x, ∀ (i : ι), IsConnected (f i)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{u₂, u₁} C<VAR>inst✝ : GaloisCategory C<VAR>X : C<VAR>ι : Type<VAR>f : ι → C<VAR>g : (i : ι) → f i ⟶ X<VAR>hl : IsColimit (Cofan.mk X g)<VAR>hc : ∀ (i : ι), IsConnected (f i)<VAR>hf : Finite ι<GOAL>∃ ι, ∃ (x : Finite ι), ∃ f x, ∀ (i : ι), IsConnected (f i)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : LinearOrderedField α<VAR>inst✝⁴ : LinearOrderedField β<VAR>inst✝³ : FloorRing α<VAR>inst✝² : FloorRing β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RingHomClass F α β<VAR>a✝ : α<VAR>b : β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<GOAL>round (f a) = round a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : LinearOrderedField α<VAR>inst✝⁴ : LinearOrderedField β<VAR>inst✝³ : FloorRing α<VAR>inst✝² : FloorRing β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RingHomClass F α β<VAR>a✝ : α<VAR>b : β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<VAR>H : f 2 = 2<GOAL>round (f a) = round a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ≥0<VAR>hfi : Integrable (fun x => ↑(f x)) μ<GOAL>∫⁻ (a : α), ↑(f a) ∂μ = ENNReal.ofReal (∫ (a : α), ↑(f a) ∂μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ≥0<VAR>hfi : Integrable (fun x => ↑(f x)) μ<GOAL>∫⁻ (a : α), ↑(f a) ∂μ = ENNReal.ofReal (∫⁻ (a : α), ↑(f a) ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ≥0<VAR>hfi : Integrable (fun x => ↑(f x)) μ<GOAL>∫⁻ (a : α), ↑(f a) ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ≥0<VAR>hfi : Integrable (fun x => ↑(f x)) μ<GOAL>∫⁻ (a : α), ↑(f a) ∂μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ≥0<VAR>hfi : Integrable (fun x => ↑(f x)) μ<GOAL>∫⁻ (a : α), ↑(f a) ∂μ < ⊤ ↔ HasFiniteIntegral (fun x => ↑(f x)) μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f✝ g : ι → α<VAR>inst✝² : CommSemiring α<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<GOAL>∏ i : ι, ∑ j ∈ t i, f i j = ∑ x ∈ piFinset t, ∏ i : ι, f i (x i)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>α : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedRing 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>x : 𝕜<GOAL>‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖ * ‖1‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>α : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedRing 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>x : 𝕜<GOAL>‖x • 1‖ = ‖x‖ * ‖1‖
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝² : DivisionSemiring α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSemiring α<VAR>f g : ι → α<VAR>a a₁ a₂ : α<VAR>h : a ≠ 0<GOAL>(Summable fun i => f i / a) ↔ Summable f
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>inst✝ : Field k<GOAL>0⁻¹ = 0
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>((monomial (n + 1)) a).coeff 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s' : Finset α<VAR>t✝ t' : Finset β<VAR>a : α<VAR>b : β<VAR>s : Finset α<VAR>t : Finset β<GOAL>⇑{ toFun := Prod.swap, inj' := ⋯ } '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<GOAL>legendreSym p (-1) = χ₄ ↑p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : α → Measure β<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((dirac a).bind f) s = (f a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : α → Measure β<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((fun μ => μ s) ∘ f) a = (f a) s
<VAR>α : Type u_1<VAR>inst✝² : LT α<VAR>inst✝¹ : DecidableRel LT.lt<VAR>inst✝ : DecidableEq α<VAR>lt_irrefl : ∀ (x : α), ¬x < x<VAR>lt_trans : ∀ {x y z : α}, x < y → y < z → x < z<VAR>lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y<VAR>this : OrientedCmp fun x x_1 => compareOfLessAndEq x x_1<VAR>x y z : α<VAR>yx : compareOfLessAndEq x y ≠ Ordering.gt<VAR>zy : compareOfLessAndEq y z ≠ Ordering.gt<GOAL>compareOfLessAndEq x z ≠ Ordering.gt
<VAR>α : Type u_1<VAR>inst✝² : LT α<VAR>inst✝¹ : DecidableRel LT.lt<VAR>inst✝ : DecidableEq α<VAR>lt_irrefl : ∀ (x : α), ¬x < x<VAR>lt_trans : ∀ {x y z : α}, x < y → y < z → x < z<VAR>lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y<VAR>this : OrientedCmp fun x x_1 => compareOfLessAndEq x x_1<VAR>x y z : α<VAR>yx : ¬y < x<VAR>zy : ¬z < y<GOAL>¬z < x
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<GOAL>(⨆ μ, eigenspace T ↑μ)ᗮ = ⊥
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>π : α✝ → Type u_5<VAR>δ : α✝ → Sort u_6<VAR>s✝ : Set α✝<VAR>f g : (i : α✝) → δ i<VAR>inst✝¹ : (j : α✝) → Decidable (j ∈ s✝)<VAR>ι : Type u_7<VAR>α : ι → Type u_8<VAR>s : Set ι<VAR>t t' : (i : ι) → Set (α i)<VAR>inst✝ : (x : ι) → Decidable (x ∈ s)<GOAL>univ.pi (s.piecewise t t') = s.pi t ∩ sᶜ.pi t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>inst✝ : AddMonoid β<VAR>f g : Multiplicative ℕ →* α<VAR>h : f (ofAdd 1) = g (ofAdd 1)<VAR>n : Multiplicative ℕ<GOAL>f n = g n
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>h : IsCompl p q<VAR>x : E<GOAL>((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ x ∈ q
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>h : IsCompl p q<VAR>x : E<GOAL>((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ q
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) '' Icc b c = Icc (b - a) (c - a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>M : Type u_5<VAR>inst✝ : CommMonoid M<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f g : ι → M<VAR>h : ∀ i ∈ s, f i ~ᵤ g i<GOAL>∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>n : ℕ<VAR>i j : Fin (n + 2)<VAR>H : i ≤ j<GOAL>X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ j.succ) = X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ i.castSucc)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>e e' : PartialEquiv α β<VAR>he : e ≈ e'<VAR>s : Set β<GOAL>e.source ∩ ↑e ⁻¹' s = e'.source ∩ ↑e' ⁻¹' s
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : Epi (f ≫ g)<GOAL>Epi g
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hij : i ≠ j<VAR>hj : j ∈ s<GOAL>eval (v j) (Lagrange.basis s v i) = 0
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hij : i ≠ j<VAR>hj : j ∈ s<GOAL>∃ a ∈ s.erase i, eval (v j) (basisDivisor (v i) (v a)) = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<GOAL>(3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈).natDegree ≤ 4
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>M : ModuleCat R<VAR>inst✝ : Flat R ↑M<VAR>C : ShortComplex (ModuleCat R)<VAR>hC : C.Exact<GOAL>(C.map (tensorRight M)).Exact
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>M : ModuleCat R<VAR>inst✝ : Flat R ↑M<VAR>C : ShortComplex (ModuleCat R)<VAR>hC : Function.Exact ⇑C.f ⇑C.g<GOAL>Function.Exact ⇑(C.map (tensorRight M)).f ⇑(C.map (tensorRight M)).g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>a✝¹ : α<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>((κ.withDensity 0) a✝¹) s✝ = (0 a✝¹) s✝