ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>inst✝ : ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<GOAL>Subpresheaf.sheafify J (imagePresheaf (whiskerRight f (forget A))) = ⊤ ↔ Subpresheaf.sheafify J (imagePresheaf (whiskerRight (whiskerRight f (forget A)) (forget (Type w')))) = ⊤
<VAR>α : Type u_1<VAR>s : Set ℝ<VAR>t : Set ℝ≥0<VAR>u : Set ℝ≥0∞<VAR>h : t.OrdConnected<GOAL>(ofNNReal '' t).OrdConnected
<VAR>α : Type u_1<VAR>s : Set ℝ<VAR>t : Set ℝ≥0<VAR>u : Set ℝ≥0∞<VAR>h : t.OrdConnected<VAR>x : ℝ≥0<VAR>hx : x ∈ t<VAR>y : ℝ≥0<VAR>hy : y ∈ t<VAR>z : ℝ≥0∞<VAR>hz : z ∈ Icc ↑x ↑y<GOAL>z ∈ ofNNReal '' t
<VAR>α : Type u_1<VAR>s : Set ℝ<VAR>t : Set ℝ≥0<VAR>u : Set ℝ≥0∞<VAR>h : t.OrdConnected<VAR>x : ℝ≥0<VAR>hx : x ∈ t<VAR>y : ℝ≥0<VAR>hy : y ∈ t<VAR>z : ℝ≥0<VAR>hz : ↑z ∈ Icc ↑x ↑y<GOAL>↑z ∈ ofNNReal '' t
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<VAR>hn : n ≠ 1<GOAL>IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<VAR>hn : n ≠ 1<VAR>h : ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1<GOAL>IsPrimePow n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n : ℕ<VAR>hn : n ≠ 1<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>h : n / p ^ n.factorization p = 1<GOAL>IsPrimePow n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n : ℕ<VAR>hn : n ≠ 1<VAR>p : ℕ<VAR>pp : Nat.Prime p<VAR>h : n / p ^ n.factorization p = 1<GOAL>∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n p : ℕ<VAR>hn : p ^ n.factorization p ≠ 1<VAR>pp : Nat.Prime p<VAR>h : n / p ^ n.factorization p = 1<GOAL>∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ n.factorization p
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n p : ℕ<VAR>hn : p ^ n.factorization p ≠ 1<VAR>pp : Nat.Prime p<VAR>h : n / p ^ n.factorization p = 1<GOAL>0 < n.factorization p
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k n p : ℕ<VAR>pp : Nat.Prime p<VAR>h : n / p ^ n.factorization p = 1<VAR>hn : n.factorization p ≤ 0<GOAL>p ^ n.factorization p = 1
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.simple i * (cs.simple i * w) = w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>inst✝ : InfConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_mono : Monotone f<VAR>hbdd : BddBelow (range f)<GOAL>Tendsto f atBot (𝓝 (⨅ i, f i))
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>head✝ : Sigma β<VAR>l₁ : List (Sigma β)<VAR>l₂ : List (Sigma β)<VAR>h : a ∉ (head✝ :: l₁).keys<GOAL>kerase a (head✝ :: l₁ ++ l₂) = head✝ :: l₁ ++ kerase a l₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>head✝ : Sigma β<VAR>l₁ : List (Sigma β)<VAR>l₂ : List (Sigma β)<VAR>h : ¬a = head✝.fst ∧ a ∉ l₁.keys<GOAL>kerase a (head✝ :: l₁ ++ l₂) = head✝ :: l₁ ++ kerase a l₂
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝ : NormedSpace ℝ F<VAR>hf : AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y ∂(condexpKernel μ m) ω) μ
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝ : NormedSpace ℝ F<VAR>hf : AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝ : NormedSpace ℝ F<VAR>hf : AEStronglyMeasurable f μ<VAR>h : AEStronglyMeasurable' (MeasurableSpace.comap id (m ⊓ mΩ)) (fun a => ∫ (y : Ω), f (id a, y).2 ∂(condDistrib id id μ) (id a)) μ<GOAL>AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : Ω → F<VAR>inst✝ : NormedSpace ℝ F<VAR>hf : AEStronglyMeasurable f μ<VAR>h : AEStronglyMeasurable' (m ⊓ mΩ) (fun a => ∫ (y : Ω), f (id a, y).2 ∂(condDistrib id id μ) (id a)) μ<GOAL>AEStronglyMeasurable' m (fun ω => ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ
<VAR>o : Ordinal.{u_1}<GOAL>o.toPGame.Numeric
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, k.toPGame.Numeric<GOAL>o.toPGame.Numeric
<VAR>o : Ordinal.{u_1}<VAR>IH : ∀ k < o, k.toPGame.Numeric<GOAL>∀ (i : o.toPGame.LeftMoves), (o.toPGame.moveLeft i).Numeric
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : Nontrivial A<VAR>k : 𝕜<VAR>a : A<VAR>ha : (σ a).Nonempty<GOAL>σ (k • a) = k • σ a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : Nontrivial A<VAR>a : A<VAR>ha : (σ a).Nonempty<GOAL>σ (0 • a) = 0 • σ a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : Nontrivial A<VAR>k : 𝕜<VAR>a : A<VAR>ha : (σ a).Nonempty<VAR>h : k ≠ 0<GOAL>σ (k • a) = k • σ a
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<GOAL>ker f = ⊥ ↔ ∀ (m : M), f m = 0 → m = 0
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>inst✝¹ : IsDomain K<VAR>L : Type u_1<VAR>inst✝ : CommGroupWithZero L<VAR>φ : K[X] →*₀ L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>p q : K[X]<GOAL>(liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = φ p / φ q
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>inst✝¹ : IsDomain K<VAR>L : Type u_1<VAR>inst✝ : CommGroupWithZero L<VAR>φ : K[X] →*₀ L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>p : K[X]<GOAL>(liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) 0) = φ p / φ 0
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>inst✝¹ : IsDomain K<VAR>L : Type u_1<VAR>inst✝ : CommGroupWithZero L<VAR>φ : K[X] →*₀ L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>(liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = φ p / φ q
<VAR>a : ℂ<VAR>r : ℝ<GOAL>volume (Metric.ball a r) = ENNReal.ofReal r ^ 2 * ↑NNReal.pi
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s✝ : Finset α<VAR>a : α<VAR>g : γ ↪ α<VAR>s : Finset γ<GOAL>fold op b f (map g s) = fold op b (f ∘ ⇑g) s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : ConditionallyCompleteLinearOrder R<VAR>inst✝ : Fintype S<VAR>f : S → WithTop R<GOAL>trop (⨅ i, f i) = ∑ i : S, trop (f i)
<VAR>L : Type u_1<VAR>inst✝ : CompleteLattice L<VAR>a b : L<GOAL>(fun u => {x | x u}) (a ⊓ b) = (fun u => {x | x u}) a ⊓ (fun u => {x | x u}) b
<VAR>L : Type u_1<VAR>inst✝ : CompleteLattice L<VAR>S : Set L<VAR>x✝ : PT L<GOAL>x✝ ∈ { toFun := fun u => {x | x u}, map_inf' := ⋯, map_top' := ⋯ }.toFun (sSup S) ↔ x✝ ∈ sSup ({ toFun := fun u => {x | x u}, map_inf' := ⋯, map_top' := ⋯ }.toFun '' S)
<VAR>a b p q : ℝ≥0<VAR>h✝ : p.IsConjExponent q<VAR>h : 1 < p<GOAL>p.IsConjExponent q ↔ q = p / (p - 1)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ l₁ l₂ : List α<VAR>n : ℕ<VAR>a : α<VAR>h : l₁.length = n<GOAL>takeD l₁.length (l₁ ++ l₂) a = l₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>s : CommSq f g h i<GOAL>F.map f ≫ F.map h = F.map g ≫ F.map i
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<VAR>x : ↑X<GOAL>⟦H.evalAt x⟧ = eqToHom ⋯ ≫ (π.map H.uliftMap).map ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))) ≫ eqToHom ⋯
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<VAR>x : ↑X<GOAL>HEq ⟦H.evalAt x⟧ ((π.map H.uliftMap).map ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))))
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<VAR>x : ↑X<GOAL>HEq ⟦H.evalAt x⟧ (Path.Homotopic.Quotient.mapFn ((prodToProdTop (TopCat.of (ULift.{u, 0} ↑I)) X).map (⟦unitInterval.upath01⟧, 𝟙 (fromTop x))) H.uliftMap)
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<VAR>x : ↑X<GOAL>∀ (t : ↑I), (H.evalAt x) t = ((fun q => q.map ⋯) (unitInterval.upath01.prod (Path.refl (fromTop x).as))) t
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>i : m<GOAL>(v ⬝ᵥ fun j => diagonal w j i) = v i * w i
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>i : m<VAR>this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0<GOAL>(v ⬝ᵥ fun j => diagonal w j i) = v i * w i
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>S : Submonoid R<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>t : Set R<VAR>ht : Ideal.span t = ⊤<VAR>Mₚ : ↑t → Type u_1<VAR>inst✝⁵ : (g : ↑t) → AddCommMonoid (Mₚ g)<VAR>inst✝⁴ : (g : ↑t) → Module R (Mₚ g)<VAR>Rₚ : ↑t → Type u<VAR>inst✝³ : (g : ↑t) → CommRing (Rₚ g)<VAR>inst✝² : (g : ↑t) → Algebra R (Rₚ g)<VAR>h₁ : ∀ (g : ↑t), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝¹ : (g : ↑t) → Module (Rₚ g) (Mₚ g)<VAR>inst✝ : ∀ (g : ↑t), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : ↑t) → M →ₗ[R] Mₚ g<VAR>h₂ : ∀ (g : ↑t), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : ↑t), Finite (Rₚ g) (Mₚ g)<GOAL>Finite R M
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>S : Submonoid R<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>t : Set R<VAR>ht : ∃ s', ↑s' ⊆ t ∧ Ideal.span ↑s' = ⊤<VAR>Mₚ : ↑t → Type u_1<VAR>inst✝⁵ : (g : ↑t) → AddCommMonoid (Mₚ g)<VAR>inst✝⁴ : (g : ↑t) → Module R (Mₚ g)<VAR>Rₚ : ↑t → Type u<VAR>inst✝³ : (g : ↑t) → CommRing (Rₚ g)<VAR>inst✝² : (g : ↑t) → Algebra R (Rₚ g)<VAR>h₁ : ∀ (g : ↑t), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝¹ : (g : ↑t) → Module (Rₚ g) (Mₚ g)<VAR>inst✝ : ∀ (g : ↑t), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : ↑t) → M →ₗ[R] Mₚ g<VAR>h₂ : ∀ (g : ↑t), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : ↑t), Finite (Rₚ g) (Mₚ g)<GOAL>Finite R M
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>S : Submonoid R<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>t : Set R<VAR>Mₚ : ↑t → Type u_1<VAR>inst✝⁵ : (g : ↑t) → AddCommMonoid (Mₚ g)<VAR>inst✝⁴ : (g : ↑t) → Module R (Mₚ g)<VAR>Rₚ : ↑t → Type u<VAR>inst✝³ : (g : ↑t) → CommRing (Rₚ g)<VAR>inst✝² : (g : ↑t) → Algebra R (Rₚ g)<VAR>h₁ : ∀ (g : ↑t), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝¹ : (g : ↑t) → Module (Rₚ g) (Mₚ g)<VAR>inst✝ : ∀ (g : ↑t), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : ↑t) → M →ₗ[R] Mₚ g<VAR>h₂ : ∀ (g : ↑t), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : ↑t), Finite (Rₚ g) (Mₚ g)<VAR>t' : Finset R<VAR>hc : ↑t' ⊆ t<VAR>ht' : Ideal.span ↑t' = ⊤<GOAL>Finite R M
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>S : Submonoid R<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>t : Set R<VAR>Mₚ : ↑t → Type u_1<VAR>inst✝⁵ : (g : ↑t) → AddCommMonoid (Mₚ g)<VAR>inst✝⁴ : (g : ↑t) → Module R (Mₚ g)<VAR>Rₚ : ↑t → Type u<VAR>inst✝³ : (g : ↑t) → CommRing (Rₚ g)<VAR>inst✝² : (g : ↑t) → Algebra R (Rₚ g)<VAR>h₁ : ∀ (g : ↑t), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝¹ : (g : ↑t) → Module (Rₚ g) (Mₚ g)<VAR>inst✝ : ∀ (g : ↑t), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : ↑t) → M →ₗ[R] Mₚ g<VAR>h₂ : ∀ (g : ↑t), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : ↑t), Finite (Rₚ g) (Mₚ g)<VAR>t' : Finset R<VAR>hc : ↑t' ⊆ t<VAR>ht' : Ideal.span ↑t' = ⊤<VAR>this : ∀ (g : { x // x ∈ t' }), IsLocalization.Away (↑g) (Rₚ ⟨↑g, ⋯⟩)<GOAL>Finite R M
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>S : Submonoid R<VAR>M : Type w<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>t : Set R<VAR>Mₚ : ↑t → Type u_1<VAR>inst✝⁵ : (g : ↑t) → AddCommMonoid (Mₚ g)<VAR>inst✝⁴ : (g : ↑t) → Module R (Mₚ g)<VAR>Rₚ : ↑t → Type u<VAR>inst✝³ : (g : ↑t) → CommRing (Rₚ g)<VAR>inst✝² : (g : ↑t) → Algebra R (Rₚ g)<VAR>h₁ : ∀ (g : ↑t), IsLocalization.Away (↑g) (Rₚ g)<VAR>inst✝¹ : (g : ↑t) → Module (Rₚ g) (Mₚ g)<VAR>inst✝ : ∀ (g : ↑t), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : ↑t) → M →ₗ[R] Mₚ g<VAR>h₂ : ∀ (g : ↑t), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : ↑t), Finite (Rₚ g) (Mₚ g)<VAR>t' : Finset R<VAR>hc : ↑t' ⊆ t<VAR>ht' : Ideal.span ↑t' = ⊤<VAR>this✝ : ∀ (g : { x // x ∈ t' }), IsLocalization.Away (↑g) (Rₚ ⟨↑g, ⋯⟩)<VAR>this : ∀ (g : { x // x ∈ t' }), IsLocalizedModule (Submonoid.powers ↑g) ((fun g => f ⟨↑g, ⋯⟩) g)<GOAL>Finite R M
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>n : Num<GOAL>↑↑n = ↑n
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>x : α<VAR>u : Fin 0 → α<GOAL>Set.range (vecCons x u) = {x}
<VAR>A : Type u_1<VAR>inst✝¹ : AddCancelCommMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>p q : A × A<VAR>n : A<VAR>hp : p ∈ antidiagonal n<VAR>hq : q ∈ antidiagonal n<GOAL>p = q ↔ p.2 = q.2
<VAR>A : Type u_1<VAR>inst✝¹ : AddCancelCommMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>p q : A × A<VAR>n : A<VAR>hp : p ∈ antidiagonal n<VAR>hq : q ∈ antidiagonal n<GOAL>p.swap = q.swap ↔ p.2 = q.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<VAR>inst✝ : DecidableEq α<GOAL>G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<VAR>inst✝ : DecidableEq α<GOAL>(((↑{c}).Pairwise G.Adj ∧ ∀ b_1 ∈ ↑{c}, b ≠ b_1 → G.Adj b b_1) ∧ ∀ b_1 ∈ insert b ↑{c}, a ≠ b_1 → G.Adj a b_1) ∧ {a, b, c}.card = 3 ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a₁ a₂ a₃ : α<VAR>b₁ b₂ b₃ : β<VAR>p₁ p₁' : Path a₁ a₂<VAR>p₂ p₂' : Path b₁ b₂<VAR>q₁ : Homotopic.Quotient a₁ a₂<VAR>q₂ : Homotopic.Quotient b₁ b₂<VAR>r₁ : Homotopic.Quotient a₂ a₃<VAR>r₂ : Homotopic.Quotient b₂ b₃<VAR>c₁ c₂ : α × β<VAR>p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)<GOAL>prod (projLeft p) (projRight p) = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a₁ a₂ a₃ : α<VAR>b₁ b₂ b₃ : β<VAR>p₁ p₁' : Path a₁ a₂<VAR>p₂ p₂' : Path b₁ b₂<VAR>q₁ : Homotopic.Quotient a₁ a₂<VAR>q₂ : Homotopic.Quotient b₁ b₂<VAR>r₁ : Homotopic.Quotient a₂ a₃<VAR>r₂ : Homotopic.Quotient b₂ b₃<VAR>c₁ c₂ : α × β<VAR>a✝ : Path (a₁, b₁) (a₂, b₂)<GOAL>prod (projLeft ⟦a✝⟧) (projRight ⟦a✝⟧) = ⟦a✝⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a₁ a₂ a₃ : α<VAR>b₁ b₂ b₃ : β<VAR>p₁ p₁' : Path a₁ a₂<VAR>p₂ p₂' : Path b₁ b₂<VAR>q₁ : Homotopic.Quotient a₁ a₂<VAR>q₂ : Homotopic.Quotient b₁ b₂<VAR>r₁ : Homotopic.Quotient a₂ a₃<VAR>r₂ : Homotopic.Quotient b₂ b₃<VAR>c₁ c₂ : α × β<VAR>a✝ : Path (a₁, b₁) (a₂, b₂)<GOAL>prod ⟦a✝.map ⋯⟧ ⟦a✝.map ⋯⟧ = ⟦a✝⟧
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>r✝ s : R<VAR>x✝ y✝ : M<VAR>x y : R<VAR>r : M<GOAL>(x + y) • r = x • r + y • r
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>S R✝ : Sieve X<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>G : D ⥤ E<VAR>R : Sieve ((F ⋙ G).obj X)<VAR>Y✝ : C<VAR>f✝ : Y✝ ⟶ X<GOAL>(functorPullback (F ⋙ G) R).arrows f✝ ↔ (functorPullback F (functorPullback G R)).arrows f✝
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : C<VAR>p : X ⟶ X<VAR>hp : p ≫ p = p<GOAL>(𝟙 X - p) ≫ (𝟙 X - p) = 𝟙 X - p
<VAR>α : Type u<VAR>l : List α<GOAL>l.rotate l.length = l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s✝ s₁ s₂ : Set α<VAR>t✝ t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>s : Set α<VAR>t : Set β<VAR>x : β<VAR>y : α<GOAL>(x, y) ∈ Prod.swap ⁻¹' s ×ˢ t ↔ (x, y) ∈ t ×ˢ s
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)<GOAL>ConcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)<GOAL>ConvexOn 𝕜 s (-f)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)<VAR>x✝ y✝ z✝ : 𝕜<VAR>hx : x✝ ∈ s<VAR>hz : z✝ ∈ s<VAR>hxy : x✝ < y✝<VAR>hyz : y✝ < z✝<GOAL>((-f) y✝ - (-f) x✝) / (y✝ - x✝) ≤ ((-f) z✝ - (-f) y✝) / (z✝ - y✝)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)<VAR>x✝ y✝ z✝ : 𝕜<VAR>hx : x✝ ∈ s<VAR>hz : z✝ ∈ s<VAR>hxy : x✝ < y✝<VAR>hyz : y✝ < z✝<GOAL>-(((-f) z✝ - (-f) y✝) / (z✝ - y✝)) ≤ -(((-f) y✝ - (-f) x✝) / (y✝ - x✝))
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)<VAR>x✝ y✝ z✝ : 𝕜<VAR>hx : x✝ ∈ s<VAR>hz : z✝ ∈ s<VAR>hxy : x✝ < y✝<VAR>hyz : y✝ < z✝<GOAL>(f z✝ - f y✝) / (z✝ - y✝) ≤ (f y✝ - f x✝) / (y✝ - x✝)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u_4<VAR>S'' : Type u_5<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>g : P'.Hom P''<VAR>x : P.Cotangent<GOAL>((map (g.comp f)) x).val = ((↑S (map g) ∘ₗ map f) x).val
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u_4<VAR>S'' : Type u_5<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>g : P'.Hom P''<VAR>x : ↥P.ker<GOAL>((map (g.comp f)) (mk x)).val = ((↑S (map g) ∘ₗ map f) (mk x)).val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r C : ℝ<VAR>f u : ℕ → α<VAR>n : ℕ<GOAL>dist (∑ k ∈ Finset.range (n + 1), u k) (∑ k ∈ Finset.range n, u k) = ‖u n‖
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>¬Subsingleton α ↔ Nontrivial α
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>r : R<VAR>n : ℕ<GOAL>eval r (descPochhammer R n) = eval (r - ↑n + 1) (ascPochhammer R n)
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>T₁ T₂ : Set α<VAR>hT₁ : T₁ ⊆ S<VAR>hT₂ : T₂ ⊆ S<GOAL>sSup (T₁ ∩ T₂) = sSup T₁ ⊓ sSup T₂
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>T₁ T₂ : Set α<VAR>hT₁ : T₁ ⊆ S<VAR>hT₂ : T₂ ⊆ S<GOAL>sSup (T₁ ∩ T₂) ≤ sSup T₁ ⊓ sSup T₂
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>T₁ T₂ : Set α<VAR>hT₁ : T₁ ⊆ S<VAR>hT₂ : T₂ ⊆ S<GOAL>sSup T₁ ⊓ sSup T₂ ≤ sSup (T₁ ∩ T₂)
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>T₁ T₂ : Set α<VAR>hT₁ : T₁ ⊆ S<VAR>hT₂ : T₂ ⊆ S<VAR>X : Set α<VAR>hX : X ⊆ S<VAR>hX' : sSup T₁ ⊓ sSup T₂ = sSup X<GOAL>sSup T₁ ⊓ sSup T₂ ≤ sSup (T₁ ∩ T₂)
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>T₁ T₂ : Set α<VAR>hT₁ : T₁ ⊆ S<VAR>hT₂ : T₂ ⊆ S<VAR>X : Set α<VAR>hX : X ⊆ S<VAR>hX' : sSup T₁ ⊓ sSup T₂ = sSup X<GOAL>sSup X ≤ sSup (T₁ ∩ T₂)
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>T₁ T₂ : Set α<VAR>hT₁ : T₁ ⊆ S<VAR>hT₂ : T₂ ⊆ S<VAR>X : Set α<VAR>hX : X ⊆ S<VAR>hX' : sSup T₁ ⊓ sSup T₂ = sSup X<GOAL>∀ b ∈ X, b ≤ sSup (T₁ ∩ T₂)
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>T₁ T₂ : Set α<VAR>hT₁ : T₁ ⊆ S<VAR>hT₂ : T₂ ⊆ S<VAR>X : Set α<VAR>hX : X ⊆ S<VAR>hX' : sSup T₁ ⊓ sSup T₂ = sSup X<VAR>I : α<VAR>hI : I ∈ X<GOAL>I ≤ sSup (T₁ ∩ T₂)
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>T₁ T₂ : Set α<VAR>hT₁ : T₁ ⊆ S<VAR>hT₂ : T₂ ⊆ S<VAR>X : Set α<VAR>hX : X ⊆ S<VAR>hX' : sSup T₁ ⊓ sSup T₂ = sSup X<VAR>I : α<VAR>hI : I ∈ X<GOAL>I ∈ T₁ ∩ T₂