ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁹ : SeminormedAddCommGroup V<VAR>inst✝⁸ : PseudoMetricSpace P<VAR>inst✝⁷ : NormedAddTorsor V P<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : MetricSpace Q<VAR>inst✝⁴ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 V<VAR>inst✝¹ : NormedSpace 𝕜 W<VAR>inst✝ : Invertible 2<VAR>p₁ p₂ : P<GOAL>dist (midpoint 𝕜 p₁ p₂) p₂ = ‖2‖⁻¹ * dist p₁ p₂
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>p q : ℚ<VAR>K : Type u_5<VAR>inst✝ : LinearOrderedField K<VAR>hq : 0 < q<GOAL>0 < ↑q
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>p q : ℚ<VAR>K : Type u_5<VAR>inst✝ : LinearOrderedField K<VAR>hq : 0 < q<GOAL>0 < ↑q.num / ↑q.den
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>T.mor₃ = 0 ↔ Mono T.mor₁
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h : T.invRotate.mor₁ = 0 ↔ Mono T.invRotate.mor₂<GOAL>T.mor₃ = 0 ↔ Mono T.mor₁
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h : -(CategoryTheory.shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁ = 0 ↔ Mono T.mor₁<GOAL>T.mor₃ = 0 ↔ Mono T.mor₁
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h : -(CategoryTheory.shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁ = 0 ↔ Mono T.mor₁<GOAL>T.mor₃ = 0 ↔ (CategoryTheory.shiftFunctor C (-1)).map T.mor₃ = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CommSemiring α<VAR>β : Type u_2<VAR>inst✝ : CommRing β<GOAL>(monomial { order := 2, coeffs := ![1, 1] }.order) 1 - ∑ i : Fin { order := 2, coeffs := ![1, 1] }.order, (monomial ↑i) ({ order := 2, coeffs := ![1, 1] }.coeffs i) = X ^ 2 - (X + 1)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>x : M₂<GOAL>x ∈ map (snd R M M₂) (p.prod q) ↔ x ∈ q
<VAR>d : ℤ<VAR>a : Solution₁ d<GOAL>(1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n) ↔ IsFundamental a
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n<GOAL>IsFundamental a
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n<VAR>h₀ : 0 < d<GOAL>IsFundamental a
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<GOAL>IsFundamental a
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<VAR>a₁ : Solution₁ d<VAR>ha₁ : IsFundamental a₁<GOAL>IsFundamental a
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<VAR>a₁ : Solution₁ d<VAR>ha₁ : IsFundamental a₁<VAR>b : Solution₁ d<VAR>hb₂ : ∀ (y : Solution₁ d), (fun a₁ => 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n) y → y = b<GOAL>IsFundamental a
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<GOAL>∑ k ∈ range n, ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<VAR>hne : ∀ (m : ℕ), ↑m ! ≠ 0<GOAL>∑ k ∈ range n, ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<VAR>hne : ∀ (m : ℕ), ↑m ! ≠ 0<VAR>h_cauchy : ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) = PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!<VAR>hps : ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !<GOAL>∑ k ∈ range n, ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<VAR>hne : ∀ (m : ℕ), ↑m ! ≠ 0<VAR>h_cauchy : ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) = PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!<VAR>hps : ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !<GOAL>∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)! * ↑p ! = ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<VAR>hne : ∀ (m : ℕ), ↑m ! ≠ 0<VAR>h_cauchy : ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) = PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!<VAR>hps : ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !<VAR>x : ℕ<VAR>x✝ : x ∈ range (p + 1)<GOAL>bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x) / ↑(p + 1)! * ↑p ! = bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x) / (↑p + 1)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<VAR>hne : ∀ (m : ℕ), ↑m ! ≠ 0<VAR>h_cauchy : ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) = PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!<VAR>hps : ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !<VAR>x : ℕ<VAR>x✝ : x ∈ range (p + 1)<GOAL>bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x) * ↑p ! * (↑p + 1) = bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x) * ((↑p + 1) * ↑p !)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : Monoid α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : F<VAR>a : Set α<VAR>as : List (Set α)<GOAL>⇑f '' (a :: as).prod = (List.map (fun s => ⇑f '' s) (a :: as)).prod
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ : ℝ<VAR>δ_nn : 0 ≤ δ<VAR>h : ∀ (ε : ℝ) (B : Set Ω), δ < ε → MeasurableSet B → μ B ≤ ν (thickening ε B) + ENNReal.ofReal ε<GOAL>levyProkhorovDist μ ν ≤ δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ : ℝ<VAR>δ_nn : 0 ≤ δ<VAR>h : ∀ (ε : ℝ) (B : Set Ω), δ < ε → MeasurableSet B → μ B ≤ ν (thickening ε B) + ENNReal.ofReal ε<GOAL>levyProkhorovEDist μ ν ≤ ENNReal.ofReal δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ : ℝ<VAR>δ_nn : 0 ≤ δ<VAR>h : ∀ (ε : ℝ) (B : Set Ω), δ < ε → MeasurableSet B → μ B ≤ ν (thickening ε B) + ENNReal.ofReal ε<GOAL>∀ (ε : ℝ≥0∞) (B : Set Ω), ENNReal.ofReal δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : PseudoEMetricSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>δ : ℝ<VAR>δ_nn : 0 ≤ δ<VAR>h : ∀ (ε : ℝ) (B : Set Ω), δ < ε → MeasurableSet B → μ B ≤ ν (thickening ε B) + ENNReal.ofReal ε<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_gt : ENNReal.ofReal δ < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>ε_gt' : δ < ε.toReal<GOAL>ε = ENNReal.ofReal ε.toReal
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.38229, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝² : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>inst✝¹ : Preregular C<VAR>inst✝ : FinitaryExtensive C<VAR>h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f<GOAL>IsSheaf (coherentTopology C) F ↔ Nonempty (PreservesFiniteProducts F) ∧ EqualizerCondition F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.38229, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝² : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>inst✝¹ : Preregular C<VAR>inst✝ : FinitaryExtensive C<VAR>h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f<GOAL>IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F ↔ Nonempty (PreservesFiniteProducts F) ∧ EqualizerCondition F
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 E'<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝³ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : MeasurableAdd G<VAR>inst✝ : MeasurableNeg G<VAR>x₀ : G<VAR>h : ConvolutionExistsAt (fun x => ‖f x‖) (fun x => ‖g x‖) x₀ (mul ℝ ℝ) μ<VAR>hmf : AEStronglyMeasurable f μ<VAR>hmg : AEStronglyMeasurable g (Measure.map (fun t => x₀ - t) μ)<GOAL>ConvolutionExistsAt f g x₀ L μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 E'<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝³ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : MeasurableAdd G<VAR>inst✝ : MeasurableNeg G<VAR>x₀ : G<VAR>h : ConvolutionExistsAt (fun x => ‖f x‖) (fun x => ‖g x‖) x₀ (mul ℝ ℝ) μ<VAR>hmf : AEStronglyMeasurable f μ<VAR>hmg : AEStronglyMeasurable g (Measure.map (fun t => x₀ - t) μ)<VAR>x : G<GOAL>‖(L (f x)) (g (x₀ - x))‖ ≤ ‖L‖ * ((mul ℝ ℝ) ((fun x => ‖f x‖) x)) ((fun x => ‖g x‖) (x₀ - x))
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 E'<VAR>inst✝⁵ : NormedSpace 𝕜 E''<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝³ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : MeasurableAdd G<VAR>inst✝ : MeasurableNeg G<VAR>x₀ : G<VAR>h : ConvolutionExistsAt (fun x => ‖f x‖) (fun x => ‖g x‖) x₀ (mul ℝ ℝ) μ<VAR>hmf : AEStronglyMeasurable f μ<VAR>hmg : AEStronglyMeasurable g (Measure.map (fun t => x₀ - t) μ)<VAR>x : G<GOAL>‖(L (f x)) (g (x₀ - x))‖ ≤ ‖L‖ * (fun x => ‖f x‖) x * (fun x => ‖g x‖) (x₀ - x)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>S : Type u_7<VAR>R : Type u_8<VAR>m' : l → Type u_9<VAR>n' : l → Type u_10<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : Zero R<VAR>inst✝ : DecidableEq l<VAR>A : X → (i : l) → Matrix (m' i) (n' i) R<VAR>hA : Continuous A<VAR>x✝¹ : (i : l) × m' i<VAR>x✝ : (i : l) × n' i<VAR>i₁ : l<VAR>i₂ : m' i₁<VAR>j₁ : l<VAR>j₂ : n' j₁<GOAL>Continuous fun a => blockDiagonal' (A a) ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>S : Type u_7<VAR>R : Type u_8<VAR>m' : l → Type u_9<VAR>n' : l → Type u_10<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : Zero R<VAR>inst✝ : DecidableEq l<VAR>A : X → (i : l) → Matrix (m' i) (n' i) R<VAR>hA : Continuous A<VAR>x✝¹ : (i : l) × m' i<VAR>x✝ : (i : l) × n' i<VAR>i₁ : l<VAR>i₂ : m' i₁<VAR>j₁ : l<VAR>j₂ : n' j₁<GOAL>Continuous fun a => if h : i₁ = j₁ then A a i₁ i₂ (cast ⋯ j₂) else 0
<VAR>X : Type u_1<VAR>x : X<VAR>a : FreeAbelianGroup X<GOAL>x ∈ a.support ↔ (coeff x) a ≠ 0
<VAR>X : Type u_1<VAR>x : X<VAR>a : FreeAbelianGroup X<GOAL>(toFinsupp a) x ≠ 0 ↔ (coeff x) a ≠ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : Zero β<VAR>inst✝² : FunLike F α β<VAR>inst✝¹ : ZeroHomClass F α β<VAR>a : α<VAR>f : F<VAR>hf : Injective ⇑f<VAR>inst✝ : NeZero a<GOAL>f a ≠ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : Zero β<VAR>inst✝² : FunLike F α β<VAR>inst✝¹ : ZeroHomClass F α β<VAR>a : α<VAR>f : F<VAR>hf : Injective ⇑f<VAR>inst✝ : NeZero a<GOAL>f a ≠ f 0
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q : ℝ≥0<VAR>p : ℝ≥0∞<GOAL>p = 0 ∨ p = ⊤ ∨ 0 < p.toReal
<VAR>α✝ : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁵ : Inv G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableInv G<VAR>m : MeasurableSpace α<VAR>f✝ : α → G<VAR>μ : Measure α<VAR>G₀ : Type u_4<VAR>inst✝² : GroupWithZero G₀<VAR>inst✝¹ : MeasurableSpace G₀<VAR>inst✝ : MeasurableInv G₀<VAR>f : α → G₀<VAR>h : AEMeasurable (fun x => (f x)⁻¹) μ<GOAL>AEMeasurable f μ
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<GOAL>(eval P) (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 - (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6)) = P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 - (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.164386, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ : ComposableArrows C n<VAR>F G : ComposableArrows C (n + 1)<VAR>α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>β : F.δ₀ ≅ G.δ₀<VAR>w : F.map' 0 1 ⋯ ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 ⋯ ⋯<GOAL>G.map' 0 1 ⋯ ⋯ ≫ app' β.inv 0 ⋯ = α.inv ≫ F.map' 0 1 ⋯ ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.164386, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ : ComposableArrows C n<VAR>F G : ComposableArrows C (n + 1)<VAR>α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>β : F.δ₀ ≅ G.δ₀<VAR>w : F.map' 0 1 ⋯ ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 ⋯ ⋯<GOAL>F.map' 0 1 ⋯ ⋯ ≫ 𝟙 (F.δ₀.obj ⟨0, ⋯⟩) = F.map' 0 1 ⋯ ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.164386, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ : ComposableArrows C n<VAR>F G : ComposableArrows C (n + 1)<VAR>α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>β : F.δ₀ ≅ G.δ₀<VAR>w : F.map' 0 1 ⋯ ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 ⋯ ⋯<GOAL>F.map (homOfLE ⋯) ≫ 𝟙 (F.obj 1) = F.map (homOfLE ⋯)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.164386, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ : ComposableArrows C n<VAR>F G : ComposableArrows C (n + 1)<VAR>α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>β : F.δ₀ ≅ G.δ₀<VAR>w : F.map' 0 1 ⋯ ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 ⋯ ⋯<GOAL>homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯ = 𝟙 F
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.164386, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ : ComposableArrows C n<VAR>F G : ComposableArrows C (n + 1)<VAR>α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>β : F.δ₀ ≅ G.δ₀<VAR>w : F.map' 0 1 ⋯ ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 ⋯ ⋯<GOAL>app' (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯) 0 ⋯ = app' (𝟙 F) 0 ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.164386, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ : ComposableArrows C n<VAR>F G : ComposableArrows C (n + 1)<VAR>α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>β : F.δ₀ ≅ G.δ₀<VAR>w : F.map' 0 1 ⋯ ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 ⋯ ⋯<GOAL>δ₀Functor.map (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯) = δ₀Functor.map (𝟙 F)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.164386, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ : ComposableArrows C n<VAR>F G : ComposableArrows C (n + 1)<VAR>α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>β : F.δ₀ ≅ G.δ₀<VAR>w : F.map' 0 1 ⋯ ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 ⋯ ⋯<GOAL>homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w = 𝟙 G
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.164386, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ : ComposableArrows C n<VAR>F G : ComposableArrows C (n + 1)<VAR>α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>β : F.δ₀ ≅ G.δ₀<VAR>w : F.map' 0 1 ⋯ ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 ⋯ ⋯<GOAL>app' (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w) 0 ⋯ = app' (𝟙 G) 0 ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.164386, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ : ComposableArrows C n<VAR>F G : ComposableArrows C (n + 1)<VAR>α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>β : F.δ₀ ≅ G.δ₀<VAR>w : F.map' 0 1 ⋯ ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 ⋯ ⋯<GOAL>δ₀Functor.map (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w) = δ₀Functor.map (𝟙 G)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>h : a = b⁻¹ * c<GOAL>b * a = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>h : b * a = c<GOAL>a = b⁻¹ * c
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<GOAL>re (I * z) = -im z
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>x : ↥s<VAR>hxe : ↑x ∈ e.source<GOAL>↑e ↑x ∈ (e.subtypeRestr hs).target
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>x : ↥s<VAR>hxe : ↑x ∈ e.source<GOAL>↑e ↑x ∈ ↑e.symm ⁻¹' (s.partialHomeomorphSubtypeCoe hs).target
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>x : ↥s<VAR>hxe : ↑x ∈ e.source<GOAL>↑x ∈ ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>inst✝ : Nonempty α<VAR>s : Set α<VAR>f : α → β<VAR>a : α<VAR>b : β<VAR>h : ∃ a ∈ s, f a = b<GOAL>invFunOn f s b ∈ s ∧ f (invFunOn f s b) = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>inst✝ : Nonempty α<VAR>s : Set α<VAR>f : α → β<VAR>a : α<VAR>b : β<VAR>h : ∃ a ∈ s, f a = b<GOAL>Classical.choose h ∈ s ∧ f (Classical.choose h) = b
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>carrier : Set R<VAR>zero_mem : 0 ∈ carrier<VAR>add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier<VAR>neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier<VAR>mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier<VAR>mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier<VAR>x : R<GOAL>x ∈ mk' carrier zero_mem ⋯ ⋯ ⋯ ⋯ ↔ x ∈ carrier
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>carrier : Set R<VAR>zero_mem : 0 ∈ carrier<VAR>add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier<VAR>neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier<VAR>mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier<VAR>mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier<VAR>x : R<GOAL>(mk' carrier zero_mem ⋯ ⋯ ⋯ ⋯).ringCon x 0 ↔ x ∈ carrier
<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>U U' : Y.Opens<VAR>V V' : X.Opens<VAR>e : V ≤ f ⁻¹ᵁ U<VAR>i : op U' ⟶ op U<GOAL>Y.presheaf.map i ≫ f.appLE U V e = f.appLE U' V ⋯
<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>U U' : Y.Opens<VAR>V V' : X.Opens<VAR>e : V ≤ f ⁻¹ᵁ U<VAR>i : op U' ⟶ op U<GOAL>f.app U' ≫ X.presheaf.map (((Opens.map f.val.base).map i.unop).op ≫ (homOfLE e).op) = f.appLE U' V ⋯
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>inst✝ : LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>ι : Type u<VAR>R : ι → ι → Prop<VAR>x : F (α ::: ι)<VAR>f : ι → ι<VAR>hh : ∀ (x : ι), R (f x) x<GOAL>LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>inst✝ : LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>ι : Type u<VAR>R : ι → ι → Prop<VAR>x : F (α ::: ι)<VAR>f : ι → ι<VAR>hh : ∀ (x : ι), R (f x) x<VAR>this : LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) ((TypeVec.id ::: _root_.id) <$$> x)<GOAL>LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) x
<VAR>c : Code<VAR>k k' : Cont<VAR>v : List ℕ<GOAL>stepNormal c (k.then k') v = (stepNormal c k v).then k'
<VAR>a b✝ m n✝ p✝ n p b : ℕ<VAR>pp : Prime p<VAR>hn : n ≠ 0<VAR>hb : n ≤ p ^ b<VAR>x : ℕ<GOAL>x ∈ Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n) ↔ x ∈ Finset.filter (fun i => p ^ i ∣ n) (Icc 1 b)
<VAR>a b✝ m n✝ p✝ n p b : ℕ<VAR>pp : Prime p<VAR>hn : n ≠ 0<VAR>hb : n ≤ p ^ b<VAR>x : ℕ<GOAL>p ^ x ∣ n → 1 ≤ x → (x < n ↔ x ≤ b)
<VAR>a b✝ m n✝ p✝ n p b : ℕ<VAR>pp : Prime p<VAR>hn : n ≠ 0<VAR>hb : n ≤ p ^ b<VAR>x : ℕ<VAR>h1 : p ^ x ∣ n<GOAL>x < n ↔ x ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : (a : Ordinal.{u_4}) → a < 0 → Ordinal.{max u_4 u_5}<GOAL>blsub 0 f = 0
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>hx : x ≠ 0<GOAL>o.oangle (-x) x = ↑π
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a✝ b✝ c✝ d e : α<VAR>m n : ℤ<VAR>a : α<VAR>h : 0 < a<VAR>b c : α<VAR>hc₀ : 0 < c<VAR>hc : b * c < a<GOAL>b < c⁻¹ * a
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hd : Directed (fun x x_1 => x ⊆ x_1) s<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict (⋃ i, s i)) t = ⨆ i, (μ.restrict (s i)) t