ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹² : CommRing R<VAR>M N P Q : Type u<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : AddCommGroup P<VAR>inst✝⁸ : AddCommGroup Q<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Coalgebra R M<VAR>inst✝² : Coalgebra R N<VAR>inst✝¹ : Coalgebra R P<VAR>inst✝ : Coalgebra R Q<GOAL>(tensor_μ (ModuleCat R)ᵒᵖ (Opposite.op (ModuleCat.mk M), Opposite.op ((ofComon R).obj (Comon_.Mon_OpOpToComon_obj' (ModuleCat R) (Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R N).toComonObj ⊗ Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R P).toComonObj))).toModuleCat) (Opposite.op (ModuleCat.mk M), Opposite.op ((ofComon R).obj (Comon_.Mon_OpOpToComon_obj' (ModuleCat R) (Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R N).toComonObj ⊗ Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R P).toComonObj))).toModuleCat)).unop ∘ₗ map Coalgebra.comul Coalgebra.comul = ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ map Coalgebra.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map Coalgebra.comul Coalgebra.comul)
<VAR>R : Type u<VAR>inst✝¹² : CommRing R<VAR>M N P Q : Type u<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : AddCommGroup P<VAR>inst✝⁸ : AddCommGroup Q<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Coalgebra R M<VAR>inst✝² : Coalgebra R N<VAR>inst✝¹ : Coalgebra R P<VAR>inst✝ : Coalgebra R Q<GOAL>(tensor_μ (ModuleCat R)ᵒᵖ (Opposite.op (ModuleCat.mk M), Opposite.op ((ofComon R).obj (Comon_.Mon_OpOpToComon_obj' (ModuleCat R) (Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R N).toComonObj ⊗ Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R P).toComonObj))).toModuleCat) (Opposite.op (ModuleCat.mk M), Opposite.op ((ofComon R).obj (Comon_.Mon_OpOpToComon_obj' (ModuleCat R) (Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R N).toComonObj ⊗ Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R P).toComonObj))).toModuleCat)).unop ∘ₗ map Coalgebra.comul (Comon_.Mon_OpOpToComon_obj' (ModuleCat R) (Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R N).toComonObj ⊗ Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R P).toComonObj)).comul = ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ map Coalgebra.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map Coalgebra.comul Coalgebra.comul)
<VAR>R : Type u<VAR>inst✝¹² : CommRing R<VAR>M N P Q : Type u<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : AddCommGroup P<VAR>inst✝⁸ : AddCommGroup Q<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Coalgebra R M<VAR>inst✝² : Coalgebra R N<VAR>inst✝¹ : Coalgebra R P<VAR>inst✝ : Coalgebra R Q<GOAL>(tensor_μ (ModuleCat R)ᵒᵖ (Opposite.op (ModuleCat.mk M), Opposite.op ((ofComon R).obj (Comon_.Mon_OpOpToComon_obj' (ModuleCat R) (Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R N).toComonObj ⊗ Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R P).toComonObj))).toModuleCat) (Opposite.op (ModuleCat.mk M), Opposite.op ((ofComon R).obj (Comon_.Mon_OpOpToComon_obj' (ModuleCat R) (Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R N).toComonObj ⊗ Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R P).toComonObj))).toModuleCat)).unop ∘ₗ map Coalgebra.comul ((tensor_μ (ModuleCat R)ᵒᵖ (Opposite.op (ModuleCat.mk N), Opposite.op (ModuleCat.mk P)) (Opposite.op (ModuleCat.mk N), Opposite.op (ModuleCat.mk P))).unop ∘ₗ map Coalgebra.comul Coalgebra.comul) = ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ map Coalgebra.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map Coalgebra.comul Coalgebra.comul)
<VAR>R : Type u<VAR>inst✝¹² : CommRing R<VAR>M N P Q : Type u<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : AddCommGroup P<VAR>inst✝⁸ : AddCommGroup Q<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Coalgebra R M<VAR>inst✝² : Coalgebra R N<VAR>inst✝¹ : Coalgebra R P<VAR>inst✝ : Coalgebra R Q<GOAL>↑(tensorTensorTensorComm R M M ↑((ofComon R).obj (Comon_.Mon_OpOpToComon_obj' (ModuleCat R) (Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R N).toComonObj ⊗ Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R P).toComonObj))).toModuleCat ↑((ofComon R).obj (Comon_.Mon_OpOpToComon_obj' (ModuleCat R) (Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R N).toComonObj ⊗ Comon_.Comon_ToMon_OpOp_obj' (ModuleCat R) (of R P).toComonObj))).toModuleCat) ∘ₗ map Coalgebra.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map Coalgebra.comul Coalgebra.comul) = ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ map Coalgebra.comul (↑(tensorTensorTensorComm R N N P P) ∘ₗ map Coalgebra.comul Coalgebra.comul)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>((map f) (OuterMeasure.ofFunction m m_empty)) s ≤ m (f ⁻¹' s)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<GOAL>(OuterMeasure.ofFunction m m_empty) (f ⁻¹' s) ≤ m (f ⁻¹' s)
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>T : Type u_1<VAR>inst✝⁴ : CommSemiring T<VAR>inst✝³ : Algebra R T<VAR>inst✝² : IsLocalization S T<VAR>A : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>a : R<VAR>s : ↥S<GOAL>(algebraMap T (LocalizedModule S A)) (IsLocalization.mk' T a s) = mk ((algebraMap R A) a) s
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>T : Type u_1<VAR>inst✝⁴ : CommSemiring T<VAR>inst✝³ : Algebra R T<VAR>inst✝² : IsLocalization S T<VAR>A : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>a : R<VAR>s : ↥S<GOAL>IsLocalization.mk' T a s • 1 = mk ((algebraMap R A) a) s
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>T : Type u_1<VAR>inst✝⁴ : CommSemiring T<VAR>inst✝³ : Algebra R T<VAR>inst✝² : IsLocalization S T<VAR>A : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>a : R<VAR>s : ↥S<GOAL>IsLocalization.mk' T a s • mk 1 1 = mk ((algebraMap R A) a) s
<VAR>α : Type u_1<VAR>n : Num<GOAL>n.natSize = (↑n).size
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s t : Finset α<VAR>n : ℕ<VAR>a : α<GOAL>mulRothNumber {a} = 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s t : Finset α<VAR>n : ℕ<VAR>a : α<GOAL>ThreeGPFree ↑{a}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s t : Finset α<VAR>n : ℕ<VAR>a : α<GOAL>ThreeGPFree {a}
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : R →+* S<GOAL>((map f) p).degrees ⊆ p.degrees
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ : α →. β<VAR>f : β →. γ<VAR>g : α →. β<VAR>s : Set γ<VAR>x✝ : α<GOAL>x✝ ∈ (f.comp g).preimage s ↔ x✝ ∈ g.preimage (f.preimage s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ : α →. β<VAR>f : β →. γ<VAR>g : α →. β<VAR>s : Set γ<VAR>x✝ : α<GOAL>(∃ y x, y ∈ s ∧ x ∈ g x✝ ∧ y ∈ f x) ↔ ∃ y x, (x ∈ s ∧ x ∈ f y) ∧ y ∈ g x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ : α →. β<VAR>f : β →. γ<VAR>g : α →. β<VAR>s : Set γ<VAR>x✝ : α<GOAL>(∃ b, ∃ a ∈ s, b ∈ g x✝ ∧ a ∈ f b) ↔ ∃ y x, (x ∈ s ∧ x ∈ f y) ∧ y ∈ g x✝
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝¹ : CommMonoid M<VAR>a : M<VAR>l✝ l₁ l₂ : List M<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α → M<VAR>l : List α<GOAL>(map f (filter (fun b => decide (p b)) l)).prod * (map f (filter (fun x => decide ¬p x) l)).prod = (map f l).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝¹ : CommMonoid M<VAR>a : M<VAR>l✝ l₁ l₂ : List M<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α → M<VAR>l : List α<GOAL>(map (fun a => if p a then f a else f a) l).prod = (map f l).prod
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>inst✝ : SecondCountableTopology X<VAR>s : Set X<GOAL>⨆ x, limsup dimH (𝓝[s] x).smallSets = dimH s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>inst✝ : SecondCountableTopology X<VAR>s : Set X<VAR>x : X<GOAL>limsup dimH (𝓝[s] x).smallSets ≤ dimH s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>inst✝ : SecondCountableTopology X<VAR>s : Set X<GOAL>dimH s ≤ ⨆ x, limsup dimH (𝓝[s] x).smallSets
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>x y z : L<GOAL>(⁅x, traceForm R L M⁆ y) z = (0 y) z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝ : IsEmpty β<GOAL>∏' (b : β), f b = 1
<VAR>ι : Type u_1<VAR>ι' : 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>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝¹ : ι<VAR>c : R<VAR>x : M<VAR>b' : Basis ι' R M'<VAR>i✝ i : ι'<GOAL>(b'.repr ((b.prod b') (Sum.inr i✝)).2) i = (b'.repr (b' i✝)) i
<VAR>ι : Type u_1<VAR>ι' : 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>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝¹ : ι<VAR>c : R<VAR>x : M<VAR>b' : Basis ι' R M'<VAR>i✝ i : ι'<GOAL>(Finsupp.single (Sum.inr i✝) 1) (Sum.inr i) = (Finsupp.single i✝ 1) i
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>f : R[X]<VAR>hp : 0 < p<GOAL>((expand R p) f).leadingCoeff = f.leadingCoeff
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : Fintype ι<VAR>p : ι → P<VAR>n : ℕ<VAR>hc : Fintype.card ι = n + 2<GOAL>AffineIndependent k p ↔ ¬finrank k ↥(vectorSpan k (Set.range p)) ≤ n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<GOAL>IsRegular (X ^ n)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<GOAL>IsLeftRegular (X ^ n)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>P Q : R[X]<VAR>hPQ : X ^ n * P = X ^ n * Q<VAR>i : ℕ<GOAL>P.coeff i = Q.coeff i
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s✝ : Set α<VAR>m : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>c : G<VAR>s : Set α<GOAL>c • s ∈ ae μ ↔ s ∈ ae μ
<VAR>P : MorphismProperty Scheme<VAR>inst✝ : P.RespectsIso<VAR>restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)<VAR>of_sSup_eq_top : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f<GOAL>IsLocalAtSource P
<VAR>P : MorphismProperty Scheme<VAR>inst✝ : P.RespectsIso<VAR>restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)<VAR>of_sSup_eq_top : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : X.OpenCover<VAR>H : P f<VAR>i : 𝒰.J<GOAL>P (𝒰.map i ≫ f)
<VAR>P : MorphismProperty Scheme<VAR>inst✝ : P.RespectsIso<VAR>restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)<VAR>of_sSup_eq_top : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : X.OpenCover<VAR>H : ∀ (i : 𝒰.J), P (𝒰.map i ≫ f)<VAR>i : 𝒰.J<GOAL>P ((Scheme.Hom.opensRange (𝒰.map i)).ι ≫ f)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : DivisionCommMonoid α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>n : ℤ<GOAL>(map (fun i => f i ^ n) m).prod = (map f m).prod ^ n
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : DivisionCommMonoid α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>n : ℤ<GOAL>map (fun i => f i ^ n) m = map (⇑(zpowGroupHom n)) (map f m)
<VAR>m : ℕ∞<VAR>hm : m ≠ 0<GOAL>ℵ₀ * ↑m = ℵ₀
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f✝ f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>f : α' → β' → γ<VAR>g : α → α'<VAR>h : β → β'<GOAL>image2 f (range g) (range h) = range fun x => f (g x.1) (h x.2)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>hf : ∀ (x : S) (y : R'), f x * g y = g y * f x<VAR>this : Module S A := Module.compHom A f.toRingHom<GOAL>S' →ₐ[R] A
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>hf : ∀ (x : S) (y : R'), f x * g y = g y * f x<VAR>this✝ : Module S A := Module.compHom A f.toRingHom<VAR>this : IsScalarTower R S A<GOAL>S' →ₐ[R] A
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>hf : ∀ (x : S) (y : R'), f x * g y = g y * f x<VAR>this✝¹ : Module S A := Module.compHom A f.toRingHom<VAR>this✝ : IsScalarTower R S A<VAR>this : IsScalarTower S A A<GOAL>S' →ₐ[R] A
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>hf : ∀ (x : S) (y : R'), f x * g y = g y * f x<VAR>this✝² : Module S A := Module.compHom A f.toRingHom<VAR>this✝¹ : IsScalarTower R S A<VAR>this✝ : IsScalarTower S A A<VAR>this : ∀ (x : R'), (⋯.lift g.toLinearMap) ((algebraMap R' S') x) = g x<GOAL>S' →ₐ[R] A
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>hf : ∀ (x : S) (y : R'), f x * g y = g y * f x<VAR>this✝² : Module S A := Module.compHom A f.toRingHom<VAR>this✝¹ : IsScalarTower R S A<VAR>this✝ : IsScalarTower S A A<VAR>this : ∀ (x : R'), (⋯.lift g.toLinearMap) ((algebraMap R' S') x) = g x<GOAL>(↑R (⋯.lift g.toLinearMap)) 1 = 1
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>hf : ∀ (x : S) (y : R'), f x * g y = g y * f x<VAR>this✝² : Module S A := Module.compHom A f.toRingHom<VAR>this✝¹ : IsScalarTower R S A<VAR>this✝ : IsScalarTower S A A<VAR>this : ∀ (x : R'), (⋯.lift g.toLinearMap) ((algebraMap R' S') x) = g x<GOAL>∀ (x y : S'), (↑R (⋯.lift g.toLinearMap)) (x * y) = (↑R (⋯.lift g.toLinearMap)) x * (↑R (⋯.lift g.toLinearMap)) y
<VAR>q✝ q : ℚ<GOAL>q⁻¹ = ↑q.den /. q.num
<VAR>X : Scheme<VAR>x : ↑↑X.toPresheafedSpace<VAR>U V : X.Opens<VAR>hU : IsAffineOpen U<VAR>hV : IsAffineOpen V<VAR>hxU : x ∈ U<VAR>hxV : x ∈ V<GOAL>hU.fromSpecStalk hxU = hV.fromSpecStalk hxV
<VAR>X : Scheme<VAR>x : ↑↑X.toPresheafedSpace<VAR>U V : X.Opens<VAR>hU : IsAffineOpen U<VAR>hV : IsAffineOpen V<VAR>hxU : x ∈ U<VAR>hxV : x ∈ V<VAR>U' : Opens ↑↑X.toPresheafedSpace<VAR>h₁ : U' ∈ X.affineOpens<VAR>h₂ : x ∈ U'<VAR>h₃ : U' ≤ U ⊓ V<GOAL>hU.fromSpecStalk hxU = hV.fromSpecStalk hxV
<VAR>A B : Grp<VAR>f : A ⟶ B<GOAL>↑(MonoidHom.range f) = {x | h x = g x}
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>b : ↑B<GOAL>b ∈ ↑(MonoidHom.range f) → b ∈ {x | h x = g x}
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>b : ↑B<VAR>hb : h b = g b<VAR>r : b ∉ ↑(MonoidHom.range f)<GOAL>False
<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<GOAL>CompactSpace ↑↑X.toPresheafedSpace