ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>inst✝ : Finite 𝒰.J<VAR>H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace<VAR>val✝ : Fintype 𝒰.J<GOAL>CompactSpace ↑↑X.toPresheafedSpace
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>inst✝ : Finite 𝒰.J<VAR>H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace<VAR>val✝ : Fintype 𝒰.J<GOAL>IsCompact (⋃ i, Set.range ⇑(𝒰.map i).val.base)
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>inst✝ : Finite 𝒰.J<VAR>H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace<VAR>val✝ : Fintype 𝒰.J<GOAL>∀ (i : 𝒰.J), IsCompact (Set.range ⇑(𝒰.map i).val.base)
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>inst✝ : Finite 𝒰.J<VAR>H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace<VAR>val✝ : Fintype 𝒰.J<VAR>i : 𝒰.J<GOAL>IsCompact (Set.range ⇑(𝒰.map i).val.base)
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>inst✝ : Finite 𝒰.J<VAR>H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace<VAR>val✝ : Fintype 𝒰.J<VAR>i : 𝒰.J<GOAL>CompactSpace ↑(Set.range ⇑(𝒰.map i).val.base)
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>X Y : C<VAR>D : Type u₂<VAR>inst✝⁷ : Category.{w, u₂} D<VAR>E : Type u₃<VAR>inst✝⁶ : Category.{w', u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A A' B B' : C<VAR>inst✝⁵ : HasBinaryProduct A B<VAR>inst✝⁴ : HasBinaryProduct A' B'<VAR>inst✝³ : HasBinaryProduct (F.obj A) (F.obj B)<VAR>inst✝² : HasBinaryProduct (F.obj A') (F.obj B')<VAR>inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))<VAR>inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)<GOAL>prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd) = G.map (prod.lift (F.map prod.fst) (F.map prod.snd)) ≫ prod.lift (G.map prod.fst) (G.map prod.snd)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<GOAL>(f.cycleOf x).IsCycle ↔ f x ≠ x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>hx : (f.cycleOf x).IsCycle<GOAL>f x ≠ x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>hx : (f.cycleOf x).IsCycle<GOAL>¬f.cycleOf x = 1
<VAR>u v : Level<VAR>n nn n' : ℕ<VAR>pn : NormNum.IsNat n nn<VAR>pn' : nn = n'.succ<GOAL>List.range n = 0 :: List.map Nat.succ (List.range n')
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : r₁ ≤ 0<VAR>hr₂ : r₂ ≤ r₁<GOAL>Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)
<VAR>f : ℕ → ℂ<VAR>s s' : ℂ<VAR>h : s.re ≤ s'.re<VAR>hf : LSeriesSummable f s<GOAL>LSeriesSummable f s'
<VAR>f : ℕ → ℂ<VAR>s s' : ℂ<VAR>h : s.re ≤ s'.re<VAR>hf : Summable fun x => ‖term f s x‖<GOAL>Summable fun x => ‖term f s' x‖
<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<GOAL>FermatLastTheoremFor 3
<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<GOAL>FermatLastTheoremWith ℤ 3
<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>hF : a ^ 3 + b ^ 3 = c ^ 3<GOAL>False
<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>hF : a ^ 3 + b ^ 3 = c ^ 3<VAR>h1 : 3 ∣ a * b * c<GOAL>False
<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>hF : a ^ 3 + b ^ 3 = c ^ 3<VAR>h1 : (3 ∣ a ∨ 3 ∣ b) ∨ 3 ∣ c<GOAL>False
<VAR>H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3<VAR>a b c : ℤ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>hF : a ^ 3 + b ^ 3 + (-c) ^ 3 = 0<VAR>h1 : (3 ∣ a ∨ 3 ∣ b) ∨ 3 ∣ c<GOAL>False
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>inst✝ : CompleteLattice α<VAR>c : ClosureOperator α<VAR>p✝ p : α → Prop<VAR>hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)<VAR>a : α<GOAL>a ≤ (fun a => ⨅ b, ↑b) a
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs F (𝓝 μ)<VAR>nonzero : μ ≠ 0<GOAL>Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs F (𝓝 μ)<VAR>nonzero : μ ≠ 0<GOAL>∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ((ProbabilityMeasure.toFiniteMeasure ∘ fun i => (μs i).normalize) i).testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : Associates α<VAR>hm : p ∈ a.factors<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>p : Associates α<VAR>hm : p ∈ factors 0<GOAL>p ∣ 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : Associates α<VAR>hm : p ∈ a.factors<VAR>ha0 : a ≠ 0<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : Associates α<VAR>hm : p ∈ a.factors<VAR>ha0 : a ≠ 0<VAR>a0 : α<VAR>nza : a0 ≠ 0<VAR>ha' : Associates.mk a0 = a<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : Associates α<VAR>hm : p ∈ a.factors<VAR>ha0 : a ≠ 0<VAR>a0 : α<VAR>nza : a0 ≠ 0<VAR>ha' : Associates.mk a0 = a<GOAL>p ∣ a.factors.prod
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : Associates α<VAR>ha0 : a ≠ 0<VAR>a0 : α<VAR>hm : p ∈ ↑(factors' a0)<VAR>nza : a0 ≠ 0<VAR>ha' : Associates.mk a0 = a<GOAL>p ∣ FactorSet.prod ↑(factors' a0)
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : Associates α<VAR>ha0 : a ≠ 0<VAR>a0 : α<VAR>hm : p ∈ ↑(factors' a0)<VAR>nza : a0 ≠ 0<VAR>ha' : Associates.mk a0 = a<GOAL>p ∣ (Multiset.map Subtype.val (factors' a0)).prod
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : Associates α<VAR>ha0 : a ≠ 0<VAR>a0 : α<VAR>hm : p ∈ ↑(factors' a0)<VAR>nza : a0 ≠ 0<VAR>ha' : Associates.mk a0 = a<GOAL>p ∈ Multiset.map Subtype.val (factors' a0)
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a p : Associates α<VAR>ha0 : a ≠ 0<VAR>a0 : α<VAR>hm : p ∈ ↑(factors' a0)<VAR>nza : a0 ≠ 0<VAR>ha' : Associates.mk a0 = a<GOAL>∃ a ∈ factors' a0, ↑a = p
<VAR>R : Type u<GOAL>(√2)⁻¹ * (√2)⁻¹ = 2⁻¹
<VAR>R : Type u<GOAL>(√2 * √2)⁻¹ = 2⁻¹
<VAR>R✝ : Type u<VAR>M✝ : Type v<VAR>N : Type w<VAR>inst✝⁹ : Ring R✝<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R✝ N<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>f : M ≃ₗ[R] M₂<GOAL>toNat (Module.rank R M) = toNat (Module.rank R M₂)
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f✝ g✝ : α →ᵇ β<VAR>x✝ : α<VAR>C✝ : ℝ<VAR>G : β → γ<VAR>C : ℝ≥0<VAR>H : LipschitzWith C G<VAR>f g : α →ᵇ β<VAR>x : α<GOAL>dist (f x) (g x) ≤ dist f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>h : SecondCountableTopologyEither α β<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>AEStronglyMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>h : SecondCountableTopologyEither α β<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>IsSeparable (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>h : SecondCountableTopologyEither α β<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>h✝ : SecondCountableTopology α<GOAL>IsSeparable (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>h : SecondCountableTopologyEither α β<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>h✝ : SecondCountableTopology β<GOAL>IsSeparable (f '' s)
<VAR>x y : ℂ<GOAL>cosh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (cosh x)
<VAR>x y : ℂ<GOAL>(starRingEnd ℂ) (cexp x + cexp (-x)) / 2 = (starRingEnd ℂ) (cexp x + cexp (-x)) / (starRingEnd ℂ) 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LE α<VAR>inst✝¹ : MulOneClass α<VAR>i : IsSymmOp α α fun x x_1 => x * x_1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : MulLECancellable a<GOAL>a ≤ b * a ↔ 1 ≤ b
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>A B : C<GOAL>prod.map (𝟙 (F.obj A)) ((expComparison F A).app B) ≫ (exp.ev (F.obj A)).app (F.obj B) = inv (prodComparison F A (A ⟹ B)) ≫ F.map ((exp.ev A).app B)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>A B : C<VAR>e_1✝ : (F.obj A ⨯ (exp A ⋙ F).obj B ⟶ (𝟭 D).obj (F.obj B)) = ((prod.functor.obj (F.obj A)).obj ((exp A ⋙ F).obj B) ⟶ (𝟭 D).obj (F.obj B))<VAR>e_3✝ : (F.obj A ⨯ F.obj (A ⟹ B)) = (F ⋙ prod.functor.obj (F.obj A)).obj (A ⟹ B)<VAR>e_4✝ : F.obj (A ⨯ A ⟹ B) = (prod.functor.obj A ⋙ F).obj (A ⟹ B)<GOAL>inv (prodComparison F A (A ⟹ B)) = (prodComparisonNatIso F A).inv.app (A ⟹ B)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>A B : C<VAR>e_1✝ : (F.obj A ⨯ (exp A ⋙ F).obj B ⟶ (𝟭 D).obj (F.obj B)) = ((prod.functor.obj (F.obj A)).obj ((exp A ⋙ F).obj B) ⟶ (𝟭 D).obj (F.obj B))<VAR>e_3✝ : (F.obj A ⨯ F.obj (A ⟹ B)) = (F ⋙ prod.functor.obj (F.obj A)).obj (A ⟹ B)<VAR>e_4✝ : F.obj (A ⨯ A ⟹ B) = (prod.functor.obj A ⋙ F).obj (A ⟹ B)<GOAL>prodComparison F A (A ⟹ B) ≫ (prodComparisonNatIso F A).inv.app (A ⟹ B) = 𝟙 (F.obj (A ⨯ A ⟹ B))
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>e : R<GOAL>IsIdempotentElem (toSpanSingleton R R e) ↔ IsIdempotentElem e
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>e : R<GOAL>(∀ (x : R), x * (e * e) = x * e) ↔ e * e = e
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>x✝ y✝ : E<VAR>inst✝ : Invertible 2<VAR>x y : E<GOAL>midpoint 𝕜 x y ∈ [x-[𝕜]y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>x✝ y✝ : E<VAR>inst✝ : Invertible 2<VAR>x y : E<GOAL>midpoint 𝕜 x y ∈ ⇑(AffineMap.lineMap x y) '' Icc 0 1
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>h : LiftPropWithinAt P g s x<VAR>hs : s ∈ 𝓝 x<GOAL>LiftPropAt P g x
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<GOAL>⋯.measurableSpace = hτ.measurableSpace ⊓ ↑f i
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : DivisionMonoid M<VAR>a b : M<VAR>ha : a ∈ center M<VAR>hb : b ∈ center M<GOAL>a / b ∈ center M
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : DivisionMonoid M<VAR>a b : M<VAR>ha : a ∈ center M<VAR>hb : b ∈ center M<GOAL>a * b⁻¹ ∈ center M
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<GOAL>(modifyNth f n l)[n]? = f <$> l[n]?
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{?u.82998, u_1} D<VAR>F G : C ⥤ D<VAR>η : F ⟶ G<VAR>X Y : WithTerminal C<VAR>f : X ⟶ Y<GOAL>(map F).map f ≫ (fun X => match X with | of x => η.app x | star => 𝟙 star) Y = (fun X => match X with | of x => η.app x | star => 𝟙 star) X ≫ (map G).map f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>x : γ<VAR>s : (i : ι) → κ i → Set γ<GOAL>x ∈ ⋂ i, ⋂ j, s i j ↔ ∀ (i : ι) (j : κ i), x ∈ s i j
<VAR>p : ZFSet → Prop<VAR>x y : ZFSet<GOAL>Hereditarily p x → p ∅
<VAR>p : ZFSet → Prop<VAR>x y : ZFSet<GOAL>∀ (x : ZFSet), (∀ y ∈ x, Hereditarily p y → p ∅) → Hereditarily p x → p ∅
<VAR>p : ZFSet → Prop<VAR>x y✝ y : ZFSet<VAR>IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅<VAR>h : Hereditarily p y<GOAL>p ∅
<VAR>p : ZFSet → Prop<VAR>x y : ZFSet<VAR>IH : ∀ y ∈ ∅, Hereditarily p y → p ∅<VAR>h : Hereditarily p ∅<GOAL>p ∅
<VAR>p : ZFSet → Prop<VAR>x y✝ y : ZFSet<VAR>IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅<VAR>h : Hereditarily p y<VAR>a : ZFSet<VAR>ha : a ∈ y.toSet<GOAL>p ∅
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>i j : Fin (n + 1)<VAR>h : i < j<VAR>x : α i<VAR>p : (k : Fin n) → α (i.succAbove k)<GOAL>i.insertNth x p j = Eq.recOn ⋯ (p (j.pred ⋯))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : E<GOAL>↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ⟪v, w⟫_𝕜 • v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : E<GOAL>↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ↑(‖v‖ ^ 2) • ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : s ∈ 𝓝 x<GOAL>mfderivWithin I I' f s x = mfderiv I I' f x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<GOAL>P.IsUniform G 1
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<GOAL>(P.nonUniforms G 1).card ≤ P.parts.card * (P.parts.card - 1)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<GOAL>P.parts.offDiag.card ≤ P.parts.card * (P.parts.card - 1)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>a : R<GOAL>(coeff R m) ((monomial R n) a * φ) = if n ≤ m then a * (coeff R (m - n)) φ else 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>r : R<VAR>hnil : IsNilpotent r<GOAL>IsUnit (r + 1)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>r : R<VAR>hnil : IsNilpotent r<GOAL>IsUnit (-r - 1)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x z : P<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>ht1 : t ≤ 1<VAR>hy : (lineMap x z) t ∈ s<VAR>ht1' : t < 1<VAR>ht0' : 0 < t<GOAL>SameRay R (x -ᵥ (lineMap x z) t) ((lineMap x z) t -ᵥ z)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x z : P<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>ht1 : t ≤ 1<VAR>hy : (lineMap x z) t ∈ s<VAR>ht1' : t < 1<VAR>ht0' : 0 < t<GOAL>(1 - t) • (x -ᵥ (lineMap x z) t) = t • ((lineMap x z) t -ᵥ z)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x z : P<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>ht1 : t ≤ 1<VAR>hy : (lineMap x z) t ∈ s<VAR>ht1' : t < 1<VAR>ht0' : 0 < t<GOAL>(-(1 - t) * t) • (z -ᵥ x) = (t * (t + -1)) • (z -ᵥ x)
<VAR>R : Type u_1<VAR>inst✝ : Mul R<VAR>a : R<VAR>ca : ∀ (b : R), Commute a b<VAR>h : IsRightRegular a<GOAL>IsLeftRegular a
<VAR>R : Type u_1<VAR>inst✝ : Mul R<VAR>a : R<VAR>h : IsRightRegular a<VAR>ca : ∀ (b : R), Commute b a<GOAL>IsLeftRegular a
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>x : R<VAR>hx : f x = 0<VAR>y : R<VAR>f_mul : f (x * y) ≤ 0<GOAL>f (x * y) = 0
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>t : Finset β<GOAL>edgeDensity r ∅ t = 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝¹ : Finset α<VAR>f : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : CommMonoid N<VAR>s✝ : Finset ι<VAR>g : ι → α →₀ M<VAR>h : α → M → N<VAR>h_zero : ∀ (a : α), h a 0 = 1<VAR>h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h<GOAL>∏ i ∈ Finset.cons a s has, (g i).prod h = (∑ i ∈ Finset.cons a s has, g i).prod h
<VAR>K : Type uK<VAR>V : Type uV<VAR>inst✝³ : CommRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Free K V<VAR>v : V<GOAL>(∀ (φ : Dual K V), φ v = 0) ↔ v = 0
<VAR>K : Type uK<VAR>V : Type uV<VAR>inst✝³ : CommRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Free K V<VAR>v : V<GOAL>(∀ (φ : Dual K V), φ v = 0) ↔ ∀ (x : Dual K V), ((eval K V) v) x = 0 x
<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<VAR>H : Summable fun i => a * f i<GOAL>Summable f
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set R<GOAL>IsClosed (zeroLocus s)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set R<GOAL>∃ s_1, zeroLocus s = zeroLocus s_1