ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>K : Subgroup G<VAR>hK : K ⊔ N = ⊤<VAR>h3 : K ≠ ⊤<VAR>h4 : (comap K.subtype N).index = N.index<GOAL>∃ H, N.IsComplement' H
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>K : Subgroup G<VAR>hK : K ⊔ N = ⊤<VAR>h3 : K ≠ ⊤<VAR>h4 : (comap K.subtype N).index = N.index<VAR>h5 : Nat.card ↥K < Nat.card G<GOAL>∃ H, N.IsComplement' H
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>K : Subgroup G<VAR>hK : K ⊔ N = ⊤<VAR>h3 : K ≠ ⊤<VAR>h4 : (comap K.subtype N).index = N.index<VAR>h5 : Nat.card ↥K < Nat.card G<VAR>h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index<GOAL>∃ H, N.IsComplement' H
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>K : Subgroup G<VAR>hK : K ⊔ N = ⊤<VAR>h3 : K ≠ ⊤<VAR>h4 : (comap K.subtype N).index = N.index<VAR>h5 : Nat.card ↥K < Nat.card G<VAR>h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index<VAR>H : Subgroup ↥K<VAR>hH : (comap K.subtype N).IsComplement' H<GOAL>∃ H, N.IsComplement' H
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>K : Subgroup G<VAR>hK : K ⊔ N = ⊤<VAR>h3 : K ≠ ⊤<VAR>h4 : (comap K.subtype N).index = N.index<VAR>h5 : Nat.card ↥K < Nat.card G<VAR>h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index<VAR>H : Subgroup ↥K<VAR>hH : Nat.card ↥(map K.subtype H) = N.index<GOAL>∃ H, N.IsComplement' H
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>K : Subgroup G<VAR>hK : K ⊔ N = ⊤<VAR>h3 : K ≠ ⊤<VAR>h4 : (comap K.subtype N).index = N.index<VAR>h5 : Nat.card ↥K < Nat.card G<VAR>h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index<VAR>H : Subgroup ↥K<VAR>hH : Nat.card ↥(map K.subtype H) = N.index<VAR>h7 : Nat.card ↥N * Nat.card ↥(map K.subtype H) = Nat.card G<GOAL>∃ H, N.IsComplement' H
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>K : Subgroup G<VAR>hK : K ⊔ N = ⊤<VAR>h3 : K ≠ ⊤<VAR>h4 : (comap K.subtype N).index = N.index<VAR>h5 : Nat.card ↥K < Nat.card G<VAR>h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index<VAR>H : Subgroup ↥K<VAR>hH : Nat.card ↥(map K.subtype H) = N.index<VAR>h7 : Nat.card ↥N * Nat.card ↥(map K.subtype H) = Nat.card G<VAR>h8 : (Nat.card ↥N).Coprime (Nat.card ↥(map K.subtype H))<GOAL>∃ H, N.IsComplement' H
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹³ : Ring R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M'<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R M'<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : StrongRankCondition R<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : (i : η) → AddCommGroup (φ i)<VAR>inst✝² : (i : η) → Module R (φ i)<VAR>inst✝¹ : ∀ (i : η), Module.Free R (φ i)<VAR>inst✝ : Fintype η<GOAL>Module.rank R (η → R) = ↑(Fintype.card η)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>m : OuterMeasure α<GOAL>m ≤ μ.toOuterMeasure ↔ ∀ (s : Set α), MeasurableSet s → m s ≤ μ s
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>W.Ψ ↑n = C (W.preΨ' n) * if Even n then W.ψ₂ else 1
<VAR>k✝ : Type u<VAR>inst✝³ : Field k✝<VAR>k : Type u_1<VAR>K : Type u_2<VAR>inst✝² : Field k<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Field K<VAR>f : K →+* k<VAR>p : K[X]<GOAL>Splits f p
<VAR>k✝ : Type u<VAR>inst✝³ : Field k✝<VAR>k : Type u_1<VAR>K : Type u_2<VAR>inst✝² : Field k<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Field K<VAR>f : K →+* k<VAR>p : K[X]<GOAL>Splits f p ↔ Splits (RingHom.id k) (map f p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<GOAL>s ∪ t =ᶠ[ae μ] t ↔ s ≤ᶠ[ae μ] t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Lattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>ha : a₁ ∈ Icc a₂ b₂<VAR>hb : b₁ ∈ Icc a₂ b₂<GOAL>[[a₁, b₁]] ⊆ Icc a₂ b₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Lattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>ha : a₂ ≤ a₁ ∧ a₁ ≤ b₂<VAR>hb : a₂ ≤ b₁ ∧ b₁ ≤ b₂<GOAL>[[a₁, b₁]] ⊆ Icc a₂ b₂
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : Flat R M<VAR>i : N →ₗ[R] M<VAR>r : M →ₗ[R] N<VAR>h : r ∘ₗ i = LinearMap.id<GOAL>Flat R N
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>i : N →ₗ[R] M<VAR>r : M →ₗ[R] N<VAR>h : r ∘ₗ i = LinearMap.id<GOAL>∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor N (Submodule.subtype I))
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>i : N →ₗ[R] M<VAR>r : M →ₗ[R] N<VAR>h : r ∘ₗ i = LinearMap.id<VAR>I : Ideal R<VAR>hI : I.FG<GOAL>Function.Injective ⇑(rTensor N (Submodule.subtype I))
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>i : N →ₗ[R] M<VAR>r : M →ₗ[R] N<VAR>h : r ∘ₗ i = LinearMap.id<VAR>I : Ideal R<VAR>hI : I.FG<VAR>h₁ : Function.Injective ⇑(lTensor R i)<GOAL>Function.Injective ⇑(rTensor N (Submodule.subtype I))
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>i : N →ₗ[R] M<VAR>r : M →ₗ[R] N<VAR>h : r ∘ₗ i = LinearMap.id<VAR>I : Ideal R<VAR>hI : I.FG<VAR>h₁ : Function.Injective ⇑(lTensor R i)<GOAL>Function.Injective ⇑(lTensor R i ∘ₗ rTensor N (Submodule.subtype I))
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>i : N →ₗ[R] M<VAR>r : M →ₗ[R] N<VAR>h : r ∘ₗ i = LinearMap.id<VAR>I : Ideal R<VAR>hI : I.FG<VAR>h₁ : Function.Injective ⇑(lTensor R i)<GOAL>Function.Injective ⇑(rTensor M (Submodule.subtype I) ∘ₗ lTensor (↥I) i)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>i : N →ₗ[R] M<VAR>r : M →ₗ[R] N<VAR>h : r ∘ₗ i = LinearMap.id<VAR>I : Ideal R<VAR>hI : I.FG<VAR>h₁ : Function.Injective ⇑(lTensor R i)<GOAL>Function.Injective ⇑(lTensor (↥I) i)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>i : N →ₗ[R] M<VAR>r : M →ₗ[R] N<VAR>h : r ∘ₗ i = LinearMap.id<VAR>I : Ideal R<VAR>hI : I.FG<VAR>h₁ : Function.Injective ⇑(lTensor R i)<GOAL>Function.RightInverse ⇑(lTensor (↥I) i) ⇑(lTensor (↥I) r)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>i : N →ₗ[R] M<VAR>r : M →ₗ[R] N<VAR>h : r ∘ₗ i = LinearMap.id<VAR>I : Ideal R<VAR>hI : I.FG<VAR>h₁ : Function.Injective ⇑(lTensor R i)<VAR>x : ↥I ⊗[R] N<GOAL>(lTensor (↥I) r) ((lTensor (↥I) i) x) = x
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>i : N →ₗ[R] M<VAR>r : M →ₗ[R] N<VAR>h : r ∘ₗ i = LinearMap.id<VAR>I : Ideal R<VAR>hI : I.FG<VAR>h₁ : Function.Injective ⇑(lTensor R i)<VAR>x : ↥I ⊗[R] N<GOAL>(lTensor (↥I) LinearMap.id) x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>IsPiSystem (⋃ a, {Ioi ↑a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>⋃ a, {Ioi ↑a} = Ioi '' (Rat.cast '' univ)
<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>x : Set ℝ<GOAL>x ∈ ⋃ a, {Ioi ↑a} ↔ x ∈ Ioi '' (Rat.cast '' univ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>ha : 0 < a<GOAL>AntitoneOn (fun x => x⁻¹) (Set.Icc a b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>ha : 0 < a<VAR>x✝ : α<GOAL>x✝ = x✝ - 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s t✝ t : Set ((i : ι) → α i)<GOAL>t ∈ measurableCylinders α ↔ ∃ s S, MeasurableSet S ∧ t = cylinder s S
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.94604, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.94611, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.94618, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.94670, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ'✝ ℱ ℱ' : Sheaf K A<VAR>i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val<VAR>this : ∀ (X : Dᵒᵖ), IsIso ((sheafHom i.hom).app X)<GOAL>ℱ.val ≅ ℱ'.val
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.94604, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.94611, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.94618, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.94670, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ'✝ ℱ ℱ' : Sheaf K A<VAR>i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val<VAR>this✝ : ∀ (X : Dᵒᵖ), IsIso ((sheafHom i.hom).app X)<VAR>this : IsIso (sheafHom i.hom)<GOAL>ℱ.val ≅ ℱ'.val
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>x✝ : Finmap β<GOAL>(keysLookupEquiv.symm (keysLookupEquiv x✝)).keys = (↑(keysLookupEquiv x✝)).1
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>ρ : Measure (α × β)<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>ρ.snd s = ρ (Prod.snd ⁻¹' s)
<VAR>J : Type u<VAR>inst✝⁵ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>inst✝⁴ : IsCofilteredOrEmpty J<VAR>inst✝³ : ∀ (j : J), Nonempty (F.obj j)<VAR>inst✝² : ∀ (j : J), Finite (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>inst✝¹ : Nonempty J<VAR>inst✝ : Finite ↑F.sections<VAR>this✝ : (j : J) → Fintype (F.obj j)<VAR>this : Fintype ↑F.sections<GOAL>∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
<VAR>J : Type u<VAR>inst✝⁵ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>inst✝⁴ : IsCofilteredOrEmpty J<VAR>inst✝³ : ∀ (j : J), Nonempty (F.obj j)<VAR>inst✝² : ∀ (j : J), Finite (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>inst✝¹ : Nonempty J<VAR>inst✝ : Finite ↑F.sections<VAR>this✝ : (j : J) → Fintype (F.obj j)<VAR>this : Fintype ↑F.sections<VAR>card_le : ∀ (j : J), Fintype.card (F.obj j) ≤ Fintype.card ↑F.sections<GOAL>∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
<VAR>J : Type u<VAR>inst✝⁵ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>inst✝⁴ : IsCofilteredOrEmpty J<VAR>inst✝³ : ∀ (j : J), Nonempty (F.obj j)<VAR>inst✝² : ∀ (j : J), Finite (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>inst✝¹ : Nonempty J<VAR>inst✝ : Finite ↑F.sections<VAR>this✝ : (j : J) → Fintype (F.obj j)<VAR>this : Fintype ↑F.sections<VAR>card_le : ∀ (j : J), Fintype.card (F.obj j) ≤ Fintype.card ↑F.sections<VAR>fn : J → ℕ := fun j => Fintype.card ↑F.sections - Fintype.card (F.obj j)<GOAL>∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
<VAR>J : Type u<VAR>inst✝⁵ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j k : J<VAR>s : Set (F.obj i✝)<VAR>inst✝⁴ : IsCofilteredOrEmpty J<VAR>inst✝³ : ∀ (j : J), Nonempty (F.obj j)<VAR>inst✝² : ∀ (j : J), Finite (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>inst✝¹ : Nonempty J<VAR>inst✝ : Finite ↑F.sections<VAR>this✝ : (j : J) → Fintype (F.obj j)<VAR>this : Fintype ↑F.sections<VAR>card_le : ∀ (j : J), Fintype.card (F.obj j) ≤ Fintype.card ↑F.sections<VAR>fn : J → ℕ := fun j => Fintype.card ↑F.sections - Fintype.card (F.obj j)<VAR>i : J<VAR>f : i ⟶ Function.argmin fn ⋯<GOAL>Fintype.card (F.obj i) ≤ Fintype.card (F.obj (Function.argmin fn ⋯))
<VAR>J : Type u<VAR>inst✝⁵ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j k : J<VAR>s : Set (F.obj i✝)<VAR>inst✝⁴ : IsCofilteredOrEmpty J<VAR>inst✝³ : ∀ (j : J), Nonempty (F.obj j)<VAR>inst✝² : ∀ (j : J), Finite (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>inst✝¹ : Nonempty J<VAR>inst✝ : Finite ↑F.sections<VAR>this✝ : (j : J) → Fintype (F.obj j)<VAR>this : Fintype ↑F.sections<VAR>card_le : ∀ (j : J), Fintype.card (F.obj j) ≤ Fintype.card ↑F.sections<VAR>fn : J → ℕ := fun j => Fintype.card ↑F.sections - Fintype.card (F.obj j)<VAR>i : J<VAR>f : i ⟶ Function.argmin fn ⋯<GOAL>Fintype.card ↑F.sections - Fintype.card (F.obj (Function.argmin fn ⋯)) ≤ Fintype.card ↑F.sections - Fintype.card (F.obj i)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>X✝ Y✝ : C ⥤ D<VAR>τ : X✝ ⟶ Y✝<VAR>H : D ⥤ E<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>H.map (X✝.map f) ≫ H.map (τ.app Y) = H.map (τ.app X) ≫ H.map (Y✝.map f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>X✝ Y✝ : C ⥤ D<VAR>τ : X✝ ⟶ Y✝<VAR>X Y : D ⥤ E<VAR>f : X ⟶ Y<VAR>x✝ : C<GOAL>f.app (X✝.obj x✝) ≫ Y.map (τ.app x✝) = X.map (τ.app x✝) ≫ f.app (Y✝.obj x✝)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y<GOAL>Continuous (lift f hf) ↔ Continuous f
<VAR>τ : Type u_1<VAR>inst✝³ : AddCommGroup τ<VAR>inst✝² : TopologicalSpace τ<VAR>inst✝¹ : TopologicalAddGroup τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>ϕ : Flow τ α<VAR>t : τ<GOAL>Continuous (ϕ.toFun t)
<VAR>τ : Type u_1<VAR>inst✝³ : AddCommGroup τ<VAR>inst✝² : TopologicalSpace τ<VAR>inst✝¹ : TopologicalAddGroup τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>ϕ : Flow τ α<VAR>t : τ<GOAL>Continuous (Function.curry (uncurry ϕ.toFun) t)
<VAR>τ : Type u_1<VAR>inst✝³ : AddCommGroup τ<VAR>inst✝² : TopologicalSpace τ<VAR>inst✝¹ : TopologicalAddGroup τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>ϕ : Flow τ α<VAR>t : τ<GOAL>Continuous (uncurry ϕ.toFun)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y Y' : ModuleCat S<VAR>g : Y ⟶ Y'<VAR>m1 : Module R S := Module.compHom S f<VAR>m2✝ : Module R ↑Y := Module.compHom (↑Y) f<VAR>m2 : Module R ↑Y' := Module.compHom (↑Y') f<GOAL>(restrictScalars f ⋙ extendScalars f).map g ≫ (fun x => Counit.map f) Y' = (fun x => Counit.map f) Y ≫ (𝟭 (ModuleCat S)).map g
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y Y' : ModuleCat S<VAR>g : Y ⟶ Y'<VAR>m1 : Module R S := Module.compHom S f<VAR>m2✝ : Module R ↑Y := Module.compHom (↑Y) f<VAR>m2 : Module R ↑Y' := Module.compHom (↑Y') f<GOAL>∀ (x : ↑((restrictScalars f ⋙ extendScalars f).obj Y)), ((restrictScalars f ⋙ extendScalars f).map g ≫ (fun x => Counit.map f) Y') x = ((fun x => Counit.map f) Y ≫ (𝟭 (ModuleCat S)).map g) x
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y Y' : ModuleCat S<VAR>g : Y ⟶ Y'<VAR>m1 : Module R S := Module.compHom S f<VAR>m2✝ : Module R ↑Y := Module.compHom (↑Y) f<VAR>m2 : Module R ↑Y' := Module.compHom (↑Y') f<VAR>z : ↑((restrictScalars f ⋙ extendScalars f).obj Y)<GOAL>((restrictScalars f ⋙ extendScalars f).map g ≫ (fun x => Counit.map f) Y') z = ((fun x => Counit.map f) Y ≫ (𝟭 (ModuleCat S)).map g) z
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y Y' : ModuleCat S<VAR>g : Y ⟶ Y'<VAR>m1 : Module R S := Module.compHom S f<VAR>m2✝ : Module R ↑Y := Module.compHom (↑Y) f<VAR>m2 : Module R ↑Y' := Module.compHom (↑Y') f<GOAL>((restrictScalars f ⋙ extendScalars f).map g ≫ (fun x => Counit.map f) Y') 0 = ((fun x => Counit.map f) Y ≫ (𝟭 (ModuleCat S)).map g) 0
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y Y' : ModuleCat S<VAR>g : Y ⟶ Y'<VAR>m1 : Module R S := Module.compHom S f<VAR>m2✝ : Module R ↑Y := Module.compHom (↑Y) f<VAR>m2 : Module R ↑Y' := Module.compHom (↑Y') f<VAR>s' : ↑((restrictScalars f).obj (mk S))<VAR>y : ↑((restrictScalars f).obj Y)<GOAL>((restrictScalars f ⋙ extendScalars f).map g ≫ (fun x => Counit.map f) Y') (s' ⊗ₜ[R] y) = ((fun x => Counit.map f) Y ≫ (𝟭 (ModuleCat S)).map g) (s' ⊗ₜ[R] y)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y Y' : ModuleCat S<VAR>g : Y ⟶ Y'<VAR>m1 : Module R S := Module.compHom S f<VAR>m2✝ : Module R ↑Y := Module.compHom (↑Y) f<VAR>m2 : Module R ↑Y' := Module.compHom (↑Y') f<VAR>z₁ z₂ : ↑((restrictScalars f).obj (mk S)) ⊗[R] ↑((restrictScalars f).obj Y)<VAR>ih₁ : ((restrictScalars f ⋙ extendScalars f).map g ≫ (fun x => Counit.map f) Y') z₁ = ((fun x => Counit.map f) Y ≫ (𝟭 (ModuleCat S)).map g) z₁<VAR>ih₂ : ((restrictScalars f ⋙ extendScalars f).map g ≫ (fun x => Counit.map f) Y') z₂ = ((fun x => Counit.map f) Y ≫ (𝟭 (ModuleCat S)).map g) z₂<GOAL>((restrictScalars f ⋙ extendScalars f).map g ≫ (fun x => Counit.map f) Y') (z₁ + z₂) = ((fun x => Counit.map f) Y ≫ (𝟭 (ModuleCat S)).map g) (z₁ + z₂)
<VAR>s : String<VAR>p : Pos<VAR>h : Pos.Valid s p<VAR>h₂ : p < s.endPos<GOAL>Pos.Valid s (s.next p)
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some '' Ioo a b = Ioo ↑a ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace α<VAR>a : α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>inst✝ : Decidable (a ∈ s)<GOAL>∫⁻ (x : α) in s, f x ∂dirac a = if a ∈ s then f a else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace α<VAR>a : α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>inst✝ : Decidable (a ∈ s)<GOAL>(∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → E<VAR>c a : ℝ<VAR>ha : 0 < a<GOAL>IntegrableOn (fun x => f (x * a)) (Ioi c) volume ↔ IntegrableOn f (Ioi (c * a)) volume
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>b ≤ max a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h : a * (b / c) ≤ d<VAR>hc : 0 < c<GOAL>b * a ≤ d * c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h : a * b / c ≤ d<VAR>hc : 0 < c<GOAL>b * a ≤ d * c
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹¹ : CommSemiring R✝<VAR>inst✝¹⁰ : NonUnitalRing A✝<VAR>inst✝⁹ : Module R✝ A✝<VAR>inst✝⁸ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁷ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : Semifield R<VAR>inst✝⁵ : Semifield S<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra S A<VAR>a : A<VAR>f : S → R<VAR>inst✝ : IsScalarTower R S A<VAR>h : SpectrumRestricts a f<GOAL>⇑(algebraMap R S) '' spectrum R a = spectrum S a
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹¹ : CommSemiring R✝<VAR>inst✝¹⁰ : NonUnitalRing A✝<VAR>inst✝⁹ : Module R✝ A✝<VAR>inst✝⁸ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁷ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : Semifield R<VAR>inst✝⁵ : Semifield S<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra S A<VAR>a : A<VAR>f : S → R<VAR>inst✝ : IsScalarTower R S A<VAR>h : SpectrumRestricts a f<GOAL>⇑(algebraMap R S) '' spectrum R a ⊆ spectrum S a