ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>disc : TotallyDisconnectedSpace X<VAR>x y : X<VAR>h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y<GOAL>∀ (i : { s // IsClopen s ∧ y ∈ s }), x ∈ ↑i
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>disc : TotallyDisconnectedSpace X<VAR>x y : X<VAR>h : ∀ (Q : DiscreteQuotient X), Q.proj x = Q.proj y<VAR>U : Set X<VAR>hU1 : IsClopen U<VAR>hU2 : y ∈ U<GOAL>x ∈ ↑⟨U, ⋯⟩
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.L₂'.Exact
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.op.L₁'.Exact
<VAR>a b : Prop<VAR>l : List Prop<VAR>h_chain : Chain (fun x x_1 => x → x_1) a (b :: l)<VAR>h_last : l.getLastD b → a<GOAL>(a :: b :: l).TFAE
<VAR>C : Type u'<VAR>inst✝⁴ : Category.{v', u'} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>inst✝¹ : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝ : HasWeakSheafify J AddCommGrp<VAR>P : PresheafOfModules R₀<VAR>F : SheafOfModules R<VAR>f : (sheafification α).obj P ⟶ F<GOAL>((sheafificationHomEquiv α) f).hom = ((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)) ((SheafOfModules.toSheaf R).map f)
<VAR>C : Type u'<VAR>inst✝⁴ : Category.{v', u'} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>inst✝¹ : J.WEqualsLocallyBijective AddCommGrp<VAR>inst✝ : HasWeakSheafify J AddCommGrp<VAR>P : PresheafOfModules R₀<VAR>F : SheafOfModules R<VAR>f : (sheafification α).obj P ⟶ F<GOAL>CategoryTheory.toSheafify J P.presheaf ≫ f.val.hom = (sheafificationAdjunction J AddCommGrp).unit.app P.presheaf ≫ (sheafToPresheaf J AddCommGrp).map ((SheafOfModules.toSheaf R).map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<VAR>P : α → Prop<GOAL>(∀ x ∈ Ι a b, P x) ↔ (∀ x ∈ Ioc a b, P x) ∧ ∀ x ∈ Ioc b a, P x
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁹ : LinearOrder ι<VAR>μ : Measure Ω<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>f : Ω → E<VAR>inst✝⁵ : atTop.IsCountablyGenerated<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>hτ : IsStoppingTime ℱ τ<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>i : ι<GOAL>μ[f|hτ.measurableSpace] =ᶠ[ae (μ.restrict {x | τ x = i})] μ[f|↑ℱ i]
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁹ : LinearOrder ι<VAR>μ : Measure Ω<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>f : Ω → E<VAR>inst✝⁵ : atTop.IsCountablyGenerated<VAR>inst✝⁴ : TopologicalSpace ι<VAR>inst✝³ : OrderTopology ι<VAR>inst✝² : FirstCountableTopology ι<VAR>inst✝¹ : SigmaFiniteFiltration μ ℱ<VAR>hτ : IsStoppingTime ℱ τ<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>i : ι<VAR>t : Set Ω<GOAL>MeasurableSet ({x | τ x = i} ∩ t) ↔ MeasurableSet ({x | τ x = i} ∩ t)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>K : Compacts G<VAR>hU : (interior U).Nonempty<GOAL>↑(index (↑K) U) / ↑(index (↑K₀) U) ≤ ↑(index ↑K ↑K₀)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>K : Compacts G<VAR>hU : (interior U).Nonempty<GOAL>index (↑K) U ≤ index ↑K ↑K₀ * index (↑K₀) U
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>K : Compacts G<VAR>hU : (interior U).Nonempty<GOAL>0 < index (↑K₀) U
<VAR>a b✝ c d m n : ℤ<VAR>C : ℤ → Sort u_1<VAR>z b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<GOAL>HEq H0 (match b - b with | ofNat n => inductionOn'.pos b H0 Hs n | -[n+1] => inductionOn'.neg b H0 Hp n)
<VAR>a b✝ c d m n : ℤ<VAR>C : ℤ → Sort u_1<VAR>z b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<GOAL>cast ?m.13083 H0 = match 0 with | ofNat n => inductionOn'.pos b H0 Hs n | -[n+1] => inductionOn'.neg b H0 Hp n
<VAR>a b✝ c d m n : ℤ<VAR>C : ℤ → Sort u_1<VAR>z b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<GOAL>C b = (fun x => C x) (b + 0)
<VAR>N : ℕ<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>∑ n ∈ Finset.range N, term (n + 1) s = 1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)
<VAR>N : ℕ<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>∑ n ∈ Finset.range N, (1 / (s - 1) * (1 / ↑(n + 1) ^ (s - 1) - 1 / (↑(n + 1) + 1) ^ (s - 1)) - ↑(n + 1) / s * (1 / ↑(n + 1) ^ s - 1 / (↑(n + 1) + 1) ^ s)) = 1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)
<VAR>N : ℕ<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>∑ x ∈ Finset.range N, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) - ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) = 1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>F : Type u_1<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : Semiring S<VAR>inst✝² : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f✝ : F<VAR>F' : Type u_2<VAR>inst✝¹ : EquivLike F' R S<VAR>inst✝ : RingEquivClass F' R S<VAR>f : F'<GOAL>ker f = ⊥
<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>p₁ : Submodule R M<VAR>p₂ : Submodule R M₂<GOAL>p₁.prod p₂ = ⊥ ↔ p₁ = ⊥ ∧ p₂ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Topology.IsUpperSet α<VAR>s : Set α<VAR>a : α<GOAL>closure {a} = Iic a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Topology.IsUpperSet α<VAR>s : Set α<VAR>a : α<GOAL>↑(LowerSet.Iic a) = Iic a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t S U : Set X<VAR>hU' : IsOpen U<VAR>h₁ : U ⊆ S<VAR>h₂ : S ⊆ t<VAR>z : X<VAR>hz : z ∈ U<VAR>ht : IsIrreducible t<VAR>u v : Set X<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x✝ : X<VAR>hx : x✝ ∈ S<VAR>hx'✝ : x✝ ∈ u<VAR>y : X<VAR>hy : y ∈ S<VAR>hy' : y ∈ v<VAR>x : X<VAR>hx' : x ∈ U ∧ x ∈ u ∧ x ∈ v<GOAL>(S ∩ (u ∩ v)).Nonempty
<VAR>R : Type u<VAR>ι : Type v<VAR>A : Type w<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid A<VAR>inst✝¹ : Module R A<VAR>inst✝ : Coalgebra R A<VAR>i j : ι<GOAL>(comul ∘ₗ lapply i) ∘ₗ lsingle j = (TensorProduct.map (lapply i) (lapply i) ∘ₗ comul) ∘ₗ lsingle j
<VAR>R : Type u<VAR>ι : Type v<VAR>A : Type w<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid A<VAR>inst✝¹ : Module R A<VAR>inst✝ : Coalgebra R A<VAR>i j : ι<GOAL>(comul ∘ₗ lapply i) ∘ₗ lsingle j = TensorProduct.map (lapply i ∘ₗ lsingle j) (lapply i ∘ₗ lsingle j) ∘ₗ comul
<VAR>R : Type u<VAR>ι : Type v<VAR>A : Type w<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid A<VAR>inst✝¹ : Module R A<VAR>inst✝ : Coalgebra R A<VAR>i : ι<GOAL>(comul ∘ₗ lapply i) ∘ₗ lsingle i = TensorProduct.map (lapply i ∘ₗ lsingle i) (lapply i ∘ₗ lsingle i) ∘ₗ comul
<VAR>R : Type u<VAR>ι : Type v<VAR>A : Type w<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid A<VAR>inst✝¹ : Module R A<VAR>inst✝ : Coalgebra R A<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>(comul ∘ₗ lapply i) ∘ₗ lsingle j = TensorProduct.map (lapply i ∘ₗ lsingle j) (lapply i ∘ₗ lsingle j) ∘ₗ comul
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>u : ↥circle<VAR>v : E<GOAL>‖u • v‖ = ‖v‖
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>hn : ¬G.Adj s t<VAR>e : Sym2 V<GOAL>e ∈ (G.replaceVertex s t).edgeSet ↔ e ∈ G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>hn : ¬G.Adj s t<VAR>e : Sym2 V<GOAL>∀ (x y : V), s(x, y) ∈ (G.replaceVertex s t).edgeSet ↔ s(x, y) ∈ G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>hn : ¬G.Adj s t<VAR>e : Sym2 V<GOAL>∀ (x y : V), (if x = t then if y = t then False else G.Adj s y else if y = t then G.Adj x s else G.Adj x y) ↔ G.Adj x y ∧ ¬(G.Adj x y ∧ (t = x ∨ t = y)) ∨ s(x, y) ∈ (fun x => s(x, t)) '' G.neighborSet s
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>hn : ¬G.Adj s t<VAR>e : Sym2 V<VAR>x✝ y✝ : V<VAR>h✝¹ : x✝ = t<VAR>h✝ : y✝ = t<GOAL>False ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x => s(x, t)) '' G.neighborSet s
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>hn : ¬G.Adj s t<VAR>e : Sym2 V<VAR>x✝ y✝ : V<VAR>h✝¹ : x✝ = t<VAR>h✝ : ¬y✝ = t<GOAL>G.Adj s y✝ ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x => s(x, t)) '' G.neighborSet s
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>hn : ¬G.Adj s t<VAR>e : Sym2 V<VAR>x✝ y✝ : V<VAR>h✝¹ : ¬x✝ = t<VAR>h✝ : y✝ = t<GOAL>G.Adj x✝ s ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x => s(x, t)) '' G.neighborSet s
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>hn : ¬G.Adj s t<VAR>e : Sym2 V<VAR>x✝ y✝ : V<VAR>h✝¹ : ¬x✝ = t<VAR>h✝ : ¬y✝ = t<GOAL>G.Adj x✝ y✝ ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x => s(x, t)) '' G.neighborSet s
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<GOAL>0 < logb b x ↔ 1 < x
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<GOAL>logb b 1 < logb b x ↔ 1 < x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁵ : EquivLike F α β<VAR>inst✝⁴ : LE α<VAR>inst✝³ : OrderTop α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : OrderTop β<VAR>inst✝ : OrderIsoClass F α β<VAR>f : F<VAR>a : α<VAR>this : TopHomClass F α β := OrderIsoClass.toTopHomClass<GOAL>f a = ⊤ ↔ a = ⊤
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<GOAL>(∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<GOAL>(KernelFork.ofι (HomologicalComplex.iCycles (inhomogeneousCochains A) 0) ⋯).mapOfIsLimit ⋯.fIsKernel (dZeroArrowIso A).hom ≫ A.ρ.invariants.subtype = iCocycles A 0 ≫ ↑(zeroCochainsLequiv A)
<VAR>R : Type u_1<GOAL>Ω 1 = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹¹ : Category.{u_3, u_1} C<VAR>inst✝¹⁰ : Category.{u_4, u_2} D<VAR>inst✝⁹ : HasZeroMorphisms C<VAR>inst✝⁸ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁷ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝⁶ : F.PreservesZeroMorphisms<VAR>inst✝⁵ : S₁.HasHomology<VAR>inst✝⁴ : S₂.HasHomology<VAR>inst✝³ : (S₁.map F).HasHomology<VAR>inst✝² : (S₂.map F).HasHomology<VAR>inst✝¹ : F.PreservesRightHomologyOf S₁<VAR>inst✝ : F.PreservesRightHomologyOf S₂<GOAL>homologyMap (F.mapShortComplex.map φ) ≫ (S₂.homologyData.right.map F).homologyIso.hom ≫ F.map S₂.homologyData.right.homologyIso.inv = ((S₁.homologyData.right.map F).homologyIso.hom ≫ F.map S₁.homologyData.right.homologyIso.inv) ≫ F.map (homologyMap φ)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Semiring α<VAR>I : Ideal α<VAR>a b : α<VAR>inst✝ : IsDomain α<VAR>h : ⊥ = ⊤<GOAL>1 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Semiring α<VAR>I : Ideal α<VAR>a b : α<VAR>inst✝ : IsDomain α<VAR>x✝ y✝ : α<VAR>h : x✝ * y✝ ∈ ⊥<GOAL>x✝ * y✝ = 0
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<GOAL>{ str := { data := l ++ (m₁ ++ c :: m₂) ++ r }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l + utf8Len (m₁ ++ c :: m₂) } }.get { byteIdx := utf8Len m₁ } = c
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>i : Δ' ⟶ Δ<VAR>inst✝ : Mono i<VAR>hi : Isδ₀ i<GOAL>(if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = K.d Δ.len Δ'.len
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>i : Δ' ⟶ Δ<VAR>inst✝ : Mono i<VAR>hi : Isδ₀ i<GOAL>Δ ≠ Δ'
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ'' : SimplexCategory<VAR>i : Δ ⟶ Δ<VAR>inst✝ : Mono i<VAR>hi : Isδ₀ i<GOAL>False
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : C<VAR>Y : Over X<VAR>S : Sieve Y.left<VAR>Z : Over X<VAR>f : Z ⟶ Y<GOAL>((overEquiv Y).symm S).arrows f ↔ S.arrows f.left
<VAR>p q r : ℕ+<VAR>hs : List.Sorted (fun x x_1 => x ≤ x_1) [p, q, r]<VAR>x✝ : [p, q, r].length = 3<VAR>H : 1 < sumInv ↑[p, q, r]<VAR>hqr : q ≤ r<VAR>hpq : p ≤ q<GOAL>Admissible ↑[p, q, r]
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Fintype ι<VAR>q : P<GOAL>∑ i : ι, (b.coord i) q = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Fintype ι<VAR>q : P<VAR>hq : q ∈ affineSpan k (range ⇑b)<GOAL>∑ i : ι, (b.coord i) q = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Fintype ι<VAR>w : ι → k<VAR>hw : ∑ i : ι, w i = 1<VAR>hq : (Finset.affineCombination k Finset.univ ⇑b) w ∈ affineSpan k (range ⇑b)<GOAL>∑ i : ι, (b.coord i) ((Finset.affineCombination k Finset.univ ⇑b) w) = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : AffineSpace V P<VAR>inst✝² : Ring k<VAR>inst✝¹ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>inst✝ : Fintype ι<VAR>w : ι → k<VAR>hw : ∑ i : ι, w i = 1<VAR>hq : (Finset.affineCombination k Finset.univ ⇑b) w ∈ affineSpan k (range ⇑b)<VAR>x✝ : ι<VAR>a✝ : x✝ ∈ Finset.univ<GOAL>(b.coord x✝) ((Finset.affineCombination k Finset.univ ⇑b) w) = w x✝
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>x : Gˣ<GOAL>x ∈ H.units ↔ ↑x ∈ H
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : MonovaryOn f g s<GOAL>ConvexOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : MonovaryOn f g s<GOAL>ConcaveOn 𝕜 s (f • -g)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>f : α → β<GOAL>∏ x ∈ s.attach, f ↑x = ∏ x ∈ s, f x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q✝ : R[X]<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hpq : p ∣ q<VAR>hq : q ≠ 0<VAR>h₁ : q.natDegree ≤ p.natDegree<GOAL>IsUnit q.leadingCoeff
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α ≃ₜ β<GOAL>Tendsto { toFun := ⇑f, continuous_toFun := ⋯ }.toFun (cocompact α) (cocompact β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α ≃ₜ β<VAR>K : Set β<VAR>hK : IsCompact K<GOAL>IsCompact ({ toFun := ⇑f, continuous_toFun := ⋯ }.toFun ⁻¹' K)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α ≃ₜ β<VAR>K : Set β<VAR>hK : IsCompact K<GOAL>IsCompact (⇑f.symm '' K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space Y<VAR>f : X ≃ Y<VAR>hf : Continuous ⇑f<GOAL>Continuous ⇑f.symm
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space Y<VAR>f : X ≃ Y<VAR>hf : Continuous ⇑f<GOAL>∀ (s : Set X), IsClosed s → IsClosed (⇑f.symm ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space Y<VAR>f : X ≃ Y<VAR>hf : Continuous ⇑f<VAR>C : Set X<VAR>hC : IsClosed C<GOAL>IsClosed (⇑f.symm ⁻¹' C)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space Y<VAR>f : X ≃ Y<VAR>hf : Continuous ⇑f<VAR>C : Set X<VAR>hC : IsClosed C<VAR>hC' : IsClosed (⇑f '' C)<GOAL>IsClosed (⇑f.symm ⁻¹' C)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>inst✝¹ : S₁.HasLeftHomology<VAR>inst✝ : S₂.HasLeftHomology<VAR>h₀ : S₁.X₁ ⟶ S₂.X₁<VAR>h₀_f : h₀ ≫ S₂.f = 0<VAR>h₁ : S₁.X₂ ⟶ S₂.X₁<VAR>h₂ : S₁.X₃ ⟶ S₂.X₂<VAR>h₃ : S₁.X₃ ⟶ S₂.X₃<VAR>g_h₃ : S₁.g ≫ h₃ = 0<GOAL>leftHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝⁴ : SeminormedGroup E<VAR>inst✝³ : SeminormedGroup F<VAR>inst✝² : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : T0Space E<VAR>a : E<GOAL>0 < ‖a‖ ↔ a ≠ 1
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝⁹ : TopologicalSpace α✝<VAR>inst✝⁸ : MeasurableSpace α✝<VAR>inst✝⁷ : OpensMeasurableSpace α✝<VAR>inst✝⁶ : MeasurableSpace δ<VAR>inst✝⁵ : LinearOrder α✝<VAR>inst✝⁴ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<GOAL>borel α = MeasurableSpace.generateFrom {S | ∃ l u, l < u ∧ Ico l u = S}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>x : L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsGalois K L<GOAL>(algebraMap K L) ((Algebra.trace K L) x) = ∑ σ : L ≃ₐ[K] L, σ x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>x : L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsGalois K L<GOAL>(algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((Algebra.trace K L) x)) = (algebraMap L (AlgebraicClosure L)) (∑ σ : L ≃ₐ[K] L, σ x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>x : L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsGalois K L<GOAL>(algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((Algebra.trace K L) x)) = ∑ x_1 : L ≃ₐ[K] L, (algebraMap L (AlgebraicClosure L)) (x_1 x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²⁰ : CommRing R<VAR>inst✝¹⁹ : CommRing S<VAR>inst✝¹⁸ : CommRing T<VAR>inst✝¹⁷ : Algebra R S<VAR>inst✝¹⁶ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Field L<VAR>inst✝¹³ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹² : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹¹ : Field F<VAR>inst✝¹⁰ : Algebra R L<VAR>inst✝⁹ : Algebra L F<VAR>inst✝⁸ : Algebra R F<VAR>inst✝⁷ : IsScalarTower R L F<VAR>inst✝⁶ : Algebra K F<VAR>inst✝⁵ : IsScalarTower K L F<VAR>E : Type u_7<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : IsAlgClosed E<VAR>x : L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : IsGalois K L<GOAL>(algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((Algebra.trace K L) x)) = ∑ x : L →ₐ[K] AlgebraicClosure L, ?a.f✝ x