ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<VAR>this : κ = κ'.comapRight h_prod_embed<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>κ : Kernel α (β × Ω)<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) ℝ<VAR>inst✝ : IsSFiniteKernel η<VAR>hη : (κ.map (Prod.map id (embeddingReal Ω)) ⋯).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω)) ⋯<VAR>e : Ω → ℝ := embeddingReal Ω<VAR>he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω<VAR>κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e) ⋯<VAR>hη' : κ'.fst ⊗ₖ η = κ'<VAR>h_prod_embed : MeasurableEmbedding (Prod.map id e)<VAR>this : κ = κ'.comapRight h_prod_embed<GOAL>κ.fst ⊗ₖ borelMarkovFromReal Ω η = (κ'.fst ⊗ₖ η).comapRight h_prod_embed
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>f : α → β<VAR>u₁ : ι → UniformSpace α<VAR>u₂ : UniformSpace β<VAR>i : ι<VAR>hf : UniformContinuous f<GOAL>Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>f : α → β<VAR>u₁ : ι → UniformSpace α<VAR>u₂ : UniformSpace β<VAR>i : ι<VAR>hf : UniformContinuous f<GOAL>Tendsto (fun x => (f x.1, f x.2)) (⨅ i, 𝓤 α) (𝓤 β)
<VAR>R : Type u_1<VAR>M✝ : Type u_2<VAR>N✝ : Type u_3<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R M✝<VAR>inst✝⁶ : AddCommMonoid N✝<VAR>inst✝⁵ : Module R N✝<VAR>S : Type u_4<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Module R S<VAR>inst✝² : SMulCommClass R R S<VAR>inst✝¹ : SMulCommClass R S S<VAR>inst✝ : IsScalarTower R S S<VAR>M N : Submodule R S<VAR>ι : Type u_5<VAR>m : ι → ↥M<VAR>hc : ∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n<VAR>i : ι<VAR>n : ↥N<GOAL>(mulLeftMap N m ∘ₗ Finsupp.lsingle i) n = (N.mulRightMap m ∘ₗ Finsupp.lsingle i) n
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0∞<VAR>hp1 : 1 ≤ p<GOAL>(a ^ p + b ^ p) ^ (1 / p) ≤ a + b
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0∞<VAR>hp1 : 1 ≤ p<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p⁻¹⁻¹
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0∞<VAR>hp1 : 1 ≤ p<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁴ : OrderedRing α<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module α β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : PosSMulReflectLT α β<VAR>ha : a < 0<GOAL>0 < a • b ↔ b < 0
<VAR>M₀ : Type u_1<VAR>inst✝⁵ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁴ : MonoidWithZero M<VAR>inst✝³ : MonoidWithZero M'<VAR>inst✝² : CommMonoidWithZero M₁<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommRing R'<VAR>x y r : R<VAR>hr : r ∈ R⁰<VAR>h : x * r = y * r<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ✝ : Measure α<VAR>κ✝ η : Kernel α β<VAR>μ : Measure α<VAR>κ : Kernel α β<VAR>h : ¬IsSFiniteKernel κ<GOAL>μ ⊗ₘ κ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ✝ : Measure α<VAR>κ✝ η : Kernel α β<VAR>μ : Measure α<VAR>κ : Kernel α β<VAR>h : ¬IsSFiniteKernel κ<GOAL>¬IsSFiniteKernel (Kernel.prodMkLeft Unit κ)
<VAR>I : Type u<VAR>inst✝⁴ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : MonoidalCategory C<VAR>X₁ X₂ Y₁ Y₂ : GradedObject I C<VAR>f : X₁ ⟶ X₂<VAR>g : Y₁ ⟶ Y₂<VAR>inst✝¹ : X₁.HasTensor Y₁<VAR>inst✝ : X₂.HasTensor Y₂<VAR>i₁ i₂ i₁₂ : I<VAR>h : i₁ + i₂ = i₁₂<GOAL>ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h ≫ tensorHom f g i₁₂ = (f i₁ ⊗ g i₂) ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h
<VAR>I : Type u<VAR>inst✝⁴ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : MonoidalCategory C<VAR>X₁ X₂ Y₁ Y₂ : GradedObject I C<VAR>f : X₁ ⟶ X₂<VAR>g : Y₁ ⟶ Y₂<VAR>inst✝¹ : X₁.HasTensor Y₁<VAR>inst✝ : X₂.HasTensor Y₂<VAR>i₁ i₂ i₁₂ : I<VAR>h : i₁ + i₂ = i₁₂<GOAL>ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h ≫ tensorHom f g i₁₂ = f i₁ ▷ Y₁ i₂ ≫ X₂ i₁ ◁ g i₂ ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : IsDomain R<GOAL>Irreducible W.polynomial
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : IsDomain R<VAR>h : ¬Irreducible W.polynomial<GOAL>False
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : IsDomain R<VAR>h : ¬Irreducible W.polynomial<VAR>f g : R[X]<VAR>h0 : W.polynomial.coeff 0 = f * g<VAR>h1 : W.polynomial.coeff 1 = f + g<GOAL>False
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : IsDomain R<VAR>h : ¬Irreducible W.polynomial<VAR>f g : R[X]<VAR>h0 : { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly = f * g<VAR>h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly = f + g<GOAL>False
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : IsDomain R<VAR>h : ¬Irreducible W.polynomial<VAR>f g : R[X]<VAR>h0 : { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly.degree = (f * g).degree<VAR>h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree<GOAL>False
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : IsDomain R<VAR>h : ¬Irreducible W.polynomial<VAR>f g : R[X]<VAR>h0 : 3 = f.degree + g.degree<VAR>h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree<GOAL>False
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : IsDomain R<VAR>h : ¬Irreducible W.polynomial<VAR>f g : R[X]<VAR>h0 : 3 = f.degree + g.degree<VAR>h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree<GOAL>1 < (f + g).degree
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : IsDomain R<VAR>h✝ : ¬Irreducible W.polynomial<VAR>f g : R[X]<VAR>h0 : 3 = f.degree + g.degree<VAR>h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree<VAR>h : f.degree = 0 ∧ g.degree = 3<GOAL>1 < (f + g).degree
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : IsDomain R<VAR>h✝ : ¬Irreducible W.polynomial<VAR>f g : R[X]<VAR>h0 : 3 = f.degree + g.degree<VAR>h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree<VAR>h : f.degree = 1 ∧ g.degree = 2<GOAL>1 < (f + g).degree
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : IsDomain R<VAR>h✝ : ¬Irreducible W.polynomial<VAR>f g : R[X]<VAR>h0 : 3 = f.degree + g.degree<VAR>h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree<VAR>h : f.degree = 2 ∧ g.degree = 1<GOAL>1 < (f + g).degree
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : IsDomain R<VAR>h✝ : ¬Irreducible W.polynomial<VAR>f g : R[X]<VAR>h0 : 3 = f.degree + g.degree<VAR>h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree<VAR>h : f.degree = 3 ∧ g.degree = 0<GOAL>1 < (f + g).degree
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f g : E → ℝ<VAR>hf : UniformConcaveOn s φ f<VAR>hφ : 0 ≤ φ<GOAL>ConcaveOn ℝ s f
<GOAL>∀ (X : Scheme), Presieve.IsSheaf zariskiTopology (yoneda.obj X)
<VAR>X : Scheme<GOAL>Presieve.IsSheaf zariskiTopology (yoneda.obj X)
<VAR>X : Scheme<GOAL>∀ {X_1 : Scheme}, ∀ R ∈ zariskiPretopology.coverings X_1, Presieve.IsSheafFor (yoneda.obj X) R
<VAR>X Y : Scheme<VAR>𝓤 : Y.OpenCover<VAR>x : Presieve.FamilyOfElements (yoneda.obj X) (Presieve.ofArrows 𝓤.obj 𝓤.map)<VAR>hx : x.Compatible<GOAL>∃! t, x.IsAmalgamation t
<VAR>X Y : Scheme<VAR>𝓤 : Y.OpenCover<VAR>x : Presieve.FamilyOfElements (yoneda.obj X) (Presieve.ofArrows 𝓤.obj 𝓤.map)<VAR>hx : x.Compatible<VAR>e : Y ⟶ X := 𝓤.glueMorphisms (fun j => x (𝓤.map j) ⋯) ⋯<GOAL>∃! t, x.IsAmalgamation t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>C : Ordinal.{u_4} → Sort u_5<VAR>H₁ : C 0<VAR>H₂ : (o : Ordinal.{u_4}) → C o → C (succ o)<VAR>H₃ : (o : Ordinal.{u_4}) → o.IsLimit → ((o' : Ordinal.{u_4}) → o' < o → C o') → C o<GOAL>limitRecOn 0 H₁ H₂ H₃ = H₁
<VAR>α : Type u<VAR>l : List α<VAR>a : α<VAR>n : ℕ<GOAL>(a :: l).rotate (n + 1) = (l ++ [a]).rotate n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>h : ∀ a ∈ s, n ≤ (filter (fun x => a ∈ x) B).card<GOAL>s.card * n ≤ ∑ t ∈ B, (s ∩ t).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>h : ∀ a ∈ s, n ≤ (filter (fun x => a ∈ x) B).card<GOAL>∑ x ∈ s, (filter (fun x_1 => x ∈ x_1) B).card ≤ ∑ t ∈ B, (s ∩ t).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>h : ∀ a ∈ s, n ≤ (filter (fun x => a ∈ x) B).card<GOAL>(∑ x ∈ s, ∑ a ∈ B, if x ∈ a then 1 else 0) ≤ ∑ x ∈ B, ∑ a ∈ s, if a ∈ x then 1 else 0
<VAR>α : Type u_1<VAR>t : Ordnode α<GOAL>t.dual.findMax = t.findMin
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : DecidableEq β<GOAL>image2 f (↑s) (↑t ∩ ↑t') ⊆ image2 f ↑s ↑t ∩ image2 f ↑s ↑t'
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : R<VAR>hroot : f.IsRoot x<VAR>hmo : f.Monic<VAR>i : ℕ<VAR>hi : f.natDegree ≤ i<GOAL>x ^ i ∈ 𝓟
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : R<VAR>hroot : f.IsRoot x<VAR>hmo : f.Monic<VAR>i : ℕ<VAR>hi : f.natDegree ≤ i<VAR>k : ℕ<VAR>hk : i = f.natDegree + k<GOAL>x ^ i ∈ 𝓟
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : R<VAR>hroot : f.IsRoot x<VAR>hmo : f.Monic<VAR>i : ℕ<VAR>hi : f.natDegree ≤ i<VAR>k : ℕ<VAR>hk : i = f.natDegree + k<GOAL>x ^ f.natDegree * x ^ k ∈ 𝓟
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : R<VAR>hroot : f.IsRoot x<VAR>hmo : f.Monic<VAR>i : ℕ<VAR>hi : f.natDegree ≤ i<VAR>k : ℕ<VAR>hk : i = f.natDegree + k<GOAL>x ^ f.natDegree ∈ 𝓟
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : R<VAR>hroot : x ^ f.natDegree + ∑ i : Fin f.natDegree, f.coeff ↑i * x ^ ↑i = 0<VAR>hmo : f.Monic<VAR>i : ℕ<VAR>hi : f.natDegree ≤ i<VAR>k : ℕ<VAR>hk : i = f.natDegree + k<GOAL>x ^ f.natDegree ∈ 𝓟
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : R<VAR>hroot : x ^ f.natDegree + ∑ i : Fin f.natDegree, f.coeff ↑i * x ^ ↑i = 0<VAR>hmo : f.Monic<VAR>i : ℕ<VAR>hi : f.natDegree ≤ i<VAR>k : ℕ<VAR>hk : i = f.natDegree + k<GOAL>∑ i : Fin f.natDegree, f.coeff ↑i * x ^ ↑i ∈ 𝓟
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → β<VAR>b : β<VAR>a : α<VAR>l : List α<GOAL>foldr (fun x => f) b (a :: l) = f^[(a :: l).length] b
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H : IsCoprime x (y * z)<GOAL>IsCoprime x z
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H : IsCoprime x (z * y)<GOAL>IsCoprime x 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 : Set X<VAR>t : Set Y<VAR>x : X<VAR>y : Y<VAR>h : e.IsImage s t<GOAL>e.IsImage (interior s) (interior t)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : CommRing 𝕜<VAR>inst✝⁵ : NoZeroDivisors 𝕜<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : TopologicalRing 𝕜<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a : ↑(characterSpace 𝕜 A)<GOAL>((fun a => { toFun := fun φ => φ a, continuous_toFun := ⋯ }) 1) a = 1 a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : CommRing 𝕜<VAR>inst✝⁵ : NoZeroDivisors 𝕜<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : TopologicalRing 𝕜<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a b : A<VAR>a✝ : ↑(characterSpace 𝕜 A)<GOAL>({ toFun := fun a => { toFun := fun φ => φ a, continuous_toFun := ⋯ }, map_one' := ⋯ }.toFun (a * b)) a✝ = ({ toFun := fun a => { toFun := fun φ => φ a, continuous_toFun := ⋯ }, map_one' := ⋯ }.toFun a * { toFun := fun a => { toFun := fun φ => φ a, continuous_toFun := ⋯ }, map_one' := ⋯ }.toFun b) a✝
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : CommRing 𝕜<VAR>inst✝⁵ : NoZeroDivisors 𝕜<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : TopologicalRing 𝕜<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a✝ : ↑(characterSpace 𝕜 A)<GOAL>((↑{ toFun := fun a => { toFun := fun φ => φ a, continuous_toFun := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }).toFun 0) a✝ = 0 a✝
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : CommRing 𝕜<VAR>inst✝⁵ : NoZeroDivisors 𝕜<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : TopologicalRing 𝕜<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a b : A<VAR>a✝ : ↑(characterSpace 𝕜 A)<GOAL>((↑{ toFun := fun a => { toFun := fun φ => φ a, continuous_toFun := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }).toFun (a + b)) a✝ = ((↑{ toFun := fun a => { toFun := fun φ => φ a, continuous_toFun := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }).toFun a + (↑{ toFun := fun a => { toFun := fun φ => φ a, continuous_toFun := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }).toFun b) a✝
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : CommRing 𝕜<VAR>inst✝⁵ : NoZeroDivisors 𝕜<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : TopologicalRing 𝕜<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra 𝕜 A<VAR>k : 𝕜<VAR>a✝ : ↑(characterSpace 𝕜 A)<GOAL>((↑↑{ toFun := fun a => { toFun := fun φ => φ a, continuous_toFun := ⋯ }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }).toFun ((algebraMap 𝕜 A) k)) a✝ = ((algebraMap 𝕜 C(↑(characterSpace 𝕜 A), 𝕜)) k) a✝
<VAR>z x✝ y x : ℝ<GOAL>√x = x ^ (1 / 2)
<VAR>z x✝ y x : ℝ<VAR>h : 0 ≤ x<GOAL>√x = x ^ (1 / 2)
<VAR>z x✝ y x : ℝ<VAR>h : x < 0<GOAL>√x = x ^ (1 / 2)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<GOAL>map f (affineSpan k s) = affineSpan k (⇑f '' s)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<GOAL>map f (affineSpan k ∅) = affineSpan k (⇑f '' ∅)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<VAR>p : P₁<VAR>hp : p ∈ s<GOAL>map f (affineSpan k s) = affineSpan k (⇑f '' s)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<VAR>p : P₁<VAR>hp : p ∈ s<GOAL>(map f (affineSpan k s)).direction = (affineSpan k (⇑f '' s)).direction
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<VAR>p : P₁<VAR>hp : p ∈ s<GOAL>(↑(map f (affineSpan k s)) ∩ ↑(affineSpan k (⇑f '' s))).Nonempty
<VAR>α✝ : Type u_1<VAR>m : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>p q : Set α✝ → Prop<VAR>U✝ : Set α✝<VAR>ε : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>pa qa : Set α → Prop<VAR>H : μ.InnerRegularWRT pa qa<VAR>f : α ≃ᵐ β<VAR>pb qb : Set β → Prop<VAR>hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)<VAR>hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)<VAR>U : Set β<VAR>hU : qb U<VAR>r : ℝ≥0∞<VAR>hr : r < (map (⇑f) μ) U<GOAL>∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K
<VAR>α✝ : Type u_1<VAR>m : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>p q : Set α✝ → Prop<VAR>U✝ : Set α✝<VAR>ε : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>pa qa : Set α → Prop<VAR>H : μ.InnerRegularWRT pa qa<VAR>f : α ≃ᵐ β<VAR>pb qb : Set β → Prop<VAR>hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)<VAR>hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)<VAR>U : Set β<VAR>hU : qb U<VAR>r : ℝ≥0∞<VAR>hr : r < μ (⇑f ⁻¹' U)<GOAL>∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K
<VAR>α✝ : Type u_1<VAR>m : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>p q : Set α✝ → Prop<VAR>U✝ : Set α✝<VAR>ε : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>pa qa : Set α → Prop<VAR>H : μ.InnerRegularWRT pa qa<VAR>f : α ≃ᵐ β<VAR>pb qb : Set β → Prop<VAR>hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)<VAR>hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)<VAR>U : Set β<VAR>hU : qb U<VAR>r : ℝ≥0∞<VAR>hr : r < μ (⇑f ⁻¹' U)<VAR>K : Set α<VAR>hKU : K ⊆ ⇑f ⁻¹' U<VAR>hKc : pa K<VAR>hK : r < μ K<GOAL>∃ K ⊆ U, pb K ∧ r < (map (⇑f) μ) K
<VAR>α✝ : Type u_1<VAR>m : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>p q : Set α✝ → Prop<VAR>U✝ : Set α✝<VAR>ε : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>pa qa : Set α → Prop<VAR>H : μ.InnerRegularWRT pa qa<VAR>f : α ≃ᵐ β<VAR>pb qb : Set β → Prop<VAR>hAB : ∀ (U : Set β), qb U → qa (⇑f ⁻¹' U)<VAR>hAB' : ∀ (K : Set α), pa K → pb (⇑f '' K)<VAR>U : Set β<VAR>hU : qb U<VAR>r : ℝ≥0∞<VAR>hr : r < μ (⇑f ⁻¹' U)<VAR>K : Set α<VAR>hKU : K ⊆ ⇑f ⁻¹' U<VAR>hKc : pa K<VAR>hK : r < μ K<GOAL>r < (map (⇑f) μ) (⇑f '' K)