ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>F : Type u_8<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F N S<VAR>inst✝ : AddMonoidHomClass F N S<VAR>f : M → N<VAR>g : F<VAR>x y : M<GOAL>polar (⇑g ∘ f) x y = g (polar f x y)
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<GOAL>RingHom.OfLocalizationSpan @RingHom.FiniteType
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<GOAL>RingHom.OfLocalizationFiniteSpan @RingHom.FiniteType
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType<VAR>this✝ : Algebra R S := f.toAlgebra<VAR>this : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<GOAL>f.FiniteType
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType<VAR>this✝¹ : Algebra R S := f.toAlgebra<VAR>this✝ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<GOAL>f.FiniteType
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<GOAL>f.FiniteType
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<GOAL>⊤.FG
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<GOAL>⊤.FG
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<GOAL>Algebra.adjoin R ↑(s.attach.biUnion sf) = ⊤
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<GOAL>⨆ x, Algebra.adjoin R ↑(sf x) = ⊤
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<GOAL>⊤ ≤ ⨆ x, Algebra.adjoin R ↑(sf x)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<GOAL>x ∈ ⨆ x, Algebra.adjoin R ↑(sf x)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<GOAL>∀ (r : ↑↑s), ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<GOAL>∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<VAR>n₁ : ℕ<VAR>hn₁ : ⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • (algebraMap S (Localization.Away (f ↑r))) x ∈ Algebra.adjoin R ↑(s₁ r)<GOAL>∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<VAR>n₁ : ℕ<VAR>hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ * x) ∈ Algebra.adjoin R ↑(s₁ r)<GOAL>∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<VAR>n₁ : ℕ<VAR>hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ * x) ∈ Algebra.adjoin R ↑(s₁ r)<VAR>n₂ : ℕ<VAR>hn₂ : ⟨(fun x => ↑r ^ x) n₂, ⋯⟩ • ((algebraMap R S) ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ * x) ∈ Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))<GOAL>∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<VAR>n₁ : ℕ<VAR>hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ * x) ∈ Algebra.adjoin R ↑(s₁ r)<VAR>n₂ : ℕ<VAR>hn₂ : ↑r ^ (n₂ + n₁) • x ∈ Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))<GOAL>∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<VAR>n₁ : ℕ<VAR>hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ * x) ∈ Algebra.adjoin R ↑(s₁ r)<VAR>n₂ : ℕ<VAR>hn₂ : ↑r ^ (n₂ + n₁) • x ∈ Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S) ↑r)) (s₁ r))<GOAL>∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Algebra.adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<VAR>n₁ : ℕ<VAR>hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨(fun x => ↑r ^ x) n₁, ⋯⟩ * x) ∈ Algebra.adjoin R ↑(s₁ r)<VAR>n₂ : ℕ<VAR>hn₂ : ↑r ^ (n₂ + n₁) • x ∈ Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S) ↑r)) (s₁ r))<GOAL>↑r ^ (n₂ + n₁) • x ∈ Subalgebra.toSubmodule (⨆ x, Algebra.adjoin R ↑(sf x))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_4, u_1} C<VAR>inst✝⁵ : Category.{u_3, u_2} D<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝² : HasHomotopyCofiber φ<VAR>H : C ⥤ D<VAR>inst✝¹ : H.Additive<VAR>inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)<VAR>n : ℤ<GOAL>H.map ((inr φ).f n) ≫ (mapHomologicalComplexXIso φ H n).hom = (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n
<VAR>R : Type u_1<VAR>p m n : ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : ExpChar R p<VAR>inst✝ : PerfectRing R p<GOAL>(iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n
<VAR>R : Type u_1<VAR>p m n : ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : ExpChar R p<VAR>inst✝ : PerfectRing R p<GOAL>(frobeniusEquiv R p ^ n).symm = (frobeniusEquiv R p).symm ^ n
<VAR>α : Type u_1<VAR>inst✝ : AddCommMonoid α<VAR>x a : α<GOAL>term 0 x a = a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>x : ℕ<VAR>hx : p.natDegree < x<GOAL>(⇑derivative)^[x] p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>n✝ : ℕ<VAR>ih : ∀ m < n✝, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0<VAR>p : R[X]<VAR>x : ℕ<VAR>hx : p.natDegree < x<VAR>h : p.natDegree = n✝<GOAL>(⇑derivative)^[x] p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>x : ℕ<VAR>hx : p.natDegree < x<VAR>ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0<GOAL>(⇑derivative)^[x] p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0<VAR>t : ℕ<VAR>hx : p.natDegree < t.succ<GOAL>(⇑derivative)^[t.succ] p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0<VAR>t : ℕ<VAR>hx : p.natDegree < t.succ<GOAL>(⇑derivative)^[t] (derivative p) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0<VAR>t : ℕ<VAR>hx : p.natDegree < t.succ<VAR>hp : ¬p.natDegree = 0<GOAL>(⇑derivative)^[t] (derivative p) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0<VAR>t : ℕ<VAR>hx : p.natDegree < t.succ<VAR>hp : ¬p.natDegree = 0<VAR>this : (derivative p).natDegree < p.natDegree<GOAL>(⇑derivative)^[t] (derivative p) = 0
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P✝ Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S✝ : Sieve X<VAR>R✝ : Presieve X<VAR>P : Cᵒᵖ ⥤ Type w<VAR>S : Sieve X<VAR>R : Presieve X<VAR>h : S.arrows ≤ R<VAR>hS : IsSheafFor P S.arrows<VAR>trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows<GOAL>IsSheafFor P R
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P✝ Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S✝ : Sieve X<VAR>R✝ : Presieve X<VAR>P : Cᵒᵖ ⥤ Type w<VAR>S : Sieve X<VAR>R : Presieve X<VAR>h : S.arrows ≤ R<VAR>hS : IsSheafFor P S.arrows<VAR>trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows<GOAL>IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t