ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : ↑((forget₂ C Ab).obj D.L₀.X₃)<VAR>x₂ : ↑((forget₂ C Ab).obj D.L₁.X₂)<VAR>x₁ : ↑((forget₂ C Ab).obj D.L₂.X₁)<VAR>h₂ : ((forget₂ C Ab).map D.L₁.g) x₂ = ((forget₂ C Ab).map D.v₀₁.τ₃) x₃<VAR>h₁ : ((forget₂ C Ab).map D.L₂.f) x₁ = ((forget₂ C Ab).map D.v₁₂.τ₂) x₂<VAR>e : forget₂ C Ab ⋙ forget Ab ≅ forget C<GOAL>((forget₂ C Ab).map D.δ) x₃ = ((forget₂ C Ab).map D.v₂₃.τ₁) x₁
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : ↑((forget₂ C Ab).obj D.L₀.X₃)<VAR>x₂ : ↑((forget₂ C Ab).obj D.L₁.X₂)<VAR>x₁ : ↑((forget₂ C Ab).obj D.L₂.X₁)<VAR>h₂ : ((forget₂ C Ab).map D.L₁.g) x₂ = ((forget₂ C Ab).map D.v₀₁.τ₃) x₃<VAR>h₁ : ((forget₂ C Ab).map D.L₂.f) x₁ = ((forget₂ C Ab).map D.v₁₂.τ₂) x₂<VAR>e : forget₂ C Ab ⋙ forget Ab ≅ forget C<GOAL>e.hom.app D.L₃.X₁ (((forget₂ C Ab).map D.δ) x₃) = e.hom.app D.L₃.X₁ (((forget₂ C Ab).map D.v₂₃.τ₁) x₁)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : ↑((forget₂ C Ab).obj D.L₀.X₃)<VAR>x₂ : ↑((forget₂ C Ab).obj D.L₁.X₂)<VAR>x₁ : ↑((forget₂ C Ab).obj D.L₂.X₁)<VAR>h₂ : ((forget₂ C Ab).map D.L₁.g) x₂ = ((forget₂ C Ab).map D.v₀₁.τ₃) x₃<VAR>h₁ : ((forget₂ C Ab).map D.L₂.f) x₁ = ((forget₂ C Ab).map D.v₁₂.τ₂) x₂<VAR>e : forget₂ C Ab ⋙ forget Ab ≅ forget C<GOAL>D.L₁.g (e.hom.app D.L₁.X₂ x₂) = D.v₀₁.τ₃ (e.hom.app D.L₀.X₃ x₃)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>inst✝³ : HasForget₂ C Ab<VAR>inst✝² : Abelian C<VAR>inst✝¹ : (forget₂ C Ab).Additive<VAR>inst✝ : (forget₂ C Ab).PreservesHomology<VAR>D : SnakeInput C<VAR>x₃ : ↑((forget₂ C Ab).obj D.L₀.X₃)<VAR>x₂ : ↑((forget₂ C Ab).obj D.L₁.X₂)<VAR>x₁ : ↑((forget₂ C Ab).obj D.L₂.X₁)<VAR>h₂ : ((forget₂ C Ab).map D.L₁.g) x₂ = ((forget₂ C Ab).map D.v₀₁.τ₃) x₃<VAR>h₁ : ((forget₂ C Ab).map D.L₂.f) x₁ = ((forget₂ C Ab).map D.v₁₂.τ₂) x₂<VAR>e : forget₂ C Ab ⋙ forget Ab ≅ forget C<GOAL>D.L₂.f (e.hom.app D.L₂.X₁ x₁) = D.v₁₂.τ₂ (e.hom.app D.L₁.X₂ x₂)
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<GOAL>(↑P).normalizer = ⊤
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>heq : (↑P).normalizer = ⊤<GOAL>(↑P).normalizer = ⊤
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝³ : Group G<VAR>inst✝² : Finite G<VAR>hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite (Sylow p G)<VAR>P : Sylow p G<VAR>K : Subgroup G<VAR>hK : IsCoatom K<VAR>hNK : (↑P).normalizer ≤ K<GOAL>(↑P).normalizer = ⊤
<VAR>C : Type u_2<VAR>D : Type ?u.77901<VAR>inst✝¹ : Category.{u_3, u_2} C<VAR>inst✝ : Category.{?u.77909, ?u.77901} D<VAR>K L : Coverage C<VAR>P : Cᵒᵖ ⥤ Type u_1<GOAL>IsSheaf (toGrothendieck C (K ⊔ L)) P ↔ IsSheaf (toGrothendieck C K) P ∧ IsSheaf (toGrothendieck C L) P
<VAR>C : Type u_2<VAR>D : Type ?u.77901<VAR>inst✝¹ : Category.{u_3, u_2} C<VAR>inst✝ : Category.{?u.77909, ?u.77901} D<VAR>K L : Coverage C<VAR>P : Cᵒᵖ ⥤ Type u_1<VAR>h : IsSheaf (toGrothendieck C K) P ∧ IsSheaf (toGrothendieck C L) P<GOAL>IsSheaf (toGrothendieck C (K ⊔ L)) P
<VAR>C : Type u_2<VAR>D : Type ?u.77901<VAR>inst✝¹ : Category.{u_3, u_2} C<VAR>inst✝ : Category.{?u.77909, ?u.77901} D<VAR>K L : Coverage C<VAR>P : Cᵒᵖ ⥤ Type u_1<VAR>h : (∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.covering X, IsSheafFor P R<GOAL>IsSheaf (toGrothendieck C (K ⊔ L)) P
<VAR>C : Type u_2<VAR>D : Type ?u.77901<VAR>inst✝¹ : Category.{u_3, u_2} C<VAR>inst✝ : Category.{?u.77909, ?u.77901} D<VAR>K L : Coverage C<VAR>P : Cᵒᵖ ⥤ Type u_1<VAR>h : (∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.covering X, IsSheafFor P R<GOAL>∀ {X : C}, ∀ R ∈ (K ⊔ L).covering X, IsSheafFor P R
<VAR>N k : ℕ<GOAL>↑(N.roughNumbersUpTo k).card ≤ ↑N * ∑ p ∈ N.succ.primesBelow \ k.primesBelow, 1 / ↑p
<VAR>N k : ℕ<GOAL>↑(N.roughNumbersUpTo k).card ≤ ∑ x ∈ N.succ.primesBelow \ k.primesBelow, ↑N / ↑x
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>n : ℕ<VAR>d : σ →₀ ℕ<GOAL>(coeff R d) (f ^ n) = ∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff R (l i)) f
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>n : ℕ<VAR>d : σ →₀ ℕ<GOAL>f ^ n = ∏ x ∈ range n, f
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l r : List α<VAR>i : ℕ<GOAL>∀ (h1 : i + (a :: l).length < ((a :: l).reverseAux r).length) (h2 : i < r.length), ((a :: l).reverseAux r).get ⟨i + (a :: l).length, h1⟩ = r.get ⟨i, h2⟩
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l r : List α<VAR>i : ℕ<GOAL>∀ (h1 : i + 1 + l.length < ((a :: l).reverseAux r).length) (h2 : i < r.length), ((a :: l).reverseAux r).get ⟨i + 1 + l.length, h1⟩ = r.get ⟨i, h2⟩
<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>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : α × β → E<VAR>F : E → ℝ≥0∞<VAR>hf : Integrable f (μ.prod ν)<VAR>hg : Integrable g (μ.prod ν)<GOAL>∫⁻ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ = ∫⁻ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ
<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>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : α × β → E<VAR>F : E → ℝ≥0∞<VAR>hf : Integrable f (μ.prod ν)<VAR>hg : Integrable g (μ.prod ν)<GOAL>(fun x => F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) =ᶠ[ae μ] fun x => F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν)
<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>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : α × β → E<VAR>F : E → ℝ≥0∞<VAR>hf : Integrable f (μ.prod ν)<VAR>hg : Integrable g (μ.prod ν)<VAR>a✝ : α<VAR>h2f : Integrable (fun y => f (a✝, y)) ν<VAR>h2g : Integrable (fun y => g (a✝, y)) ν<GOAL>F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν - ∫ (y : β), g (a✝, y) ∂ν)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>x✝ : ℝ<GOAL>logDeriv cosh x✝ = tanh x✝
<VAR>α : Type u<VAR>a : α<VAR>inst✝⁴ : Group α<VAR>H : Type u_1<VAR>G : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Group H<VAR>inst✝² : Group G<VAR>inst✝¹ : FunLike F H G<VAR>inst✝ : MonoidHomClass F H G<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>x : H<VAR>hx : ∀ (x_1 : H), x_1 ∈ zpowers x<VAR>n : ℤ<GOAL>f ((fun x_1 => x ^ x_1) n) ∈ zpowers (f x)
<VAR>x y : ℂ<GOAL>cosh x ^ 2 - sinh x ^ 2 = 1
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K✝ : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : IsCyclotomicExtension {n} A B<VAR>inst✝⁴ : CommRing L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝³ : Field K✝<VAR>inst✝² : Algebra K✝ L<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : Algebra K L<VAR>hodd : Odd ↑n<GOAL>(Algebra.norm K) ζ = 1
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K✝ : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : IsCyclotomicExtension {n} A B<VAR>inst✝⁴ : CommRing L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝³ : Field K✝<VAR>inst✝² : Algebra K✝ L<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : Algebra K L<VAR>hodd : Odd ↑n<VAR>hz : (Algebra.norm K) (ζ ^ ↑n) = (Algebra.norm K) 1<GOAL>(Algebra.norm K) ζ = 1
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K✝ : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : IsCyclotomicExtension {n} A B<VAR>inst✝⁴ : CommRing L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝³ : Field K✝<VAR>inst✝² : Algebra K✝ L<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : Algebra K L<VAR>hodd : Odd ↑n<VAR>hz : (Algebra.norm K) ζ ^ ↑n = 1 ^ ↑n<GOAL>(Algebra.norm K) ζ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : List α<VAR>h : t ⊆ s<GOAL>(s ++ t).dedup ~ s.dedup
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>s' : Set ((i : ι) → F' i)<GOAL>DifferentiableOn 𝕜 (fun f => f i) s'
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>s' : Set ((i : ι) → F' i)<VAR>h : DifferentiableOn 𝕜 (fun f i' => f i') s' → ∀ (i : ι), DifferentiableOn 𝕜 (fun x => x i) s'<GOAL>DifferentiableOn 𝕜 (fun f => f i) s'
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>s' : Set ((i : ι) → F' i)<VAR>h : DifferentiableOn 𝕜 (fun f i' => f i') s' → ∀ (i : ι), DifferentiableOn 𝕜 (fun x => x i) s'<GOAL>DifferentiableOn 𝕜 (fun f i' => f i') s'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I J : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>map f I = map f J ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : Semiring S<VAR>inst✝² : Semiring T<VAR>inst✝¹ : FunLike F R S<VAR>rcf : RingHomClass F R S<VAR>inst✝ : FunLike G T S<VAR>rcg : RingHomClass G T S<VAR>f✝ : F<VAR>g✝ : G<VAR>f : S →+* R<VAR>g : T →+* S<GOAL>Ideal.comap g (ker f) = ker (f.comp g)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>EB : Type u_4<VAR>inst✝³ : NormedAddCommGroup EB<VAR>inst✝² : NormedSpace 𝕜 EB<VAR>HB : Type u_5<VAR>inst✝¹ : TopologicalSpace HB<VAR>inst✝ : ChartedSpace HB B<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>e : PartialHomeomorph (B × F) (B × F)<VAR>U : Set B<VAR>hU : e.source = U ×ˢ univ<VAR>h : ∀ x ∈ U, ∃ φ u, ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x)) u) (h2φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(φ x).symm) u), (e.restr (u ×ˢ univ)).EqOnSource (FiberwiseLinear.partialHomeomorph φ hu ⋯ ⋯)<GOAL>∃ Φ U, ∃ (hU₀ : IsOpen U) (hΦ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(Φ x)) U) (h2Φ : SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun x => ↑(Φ x).symm) U), e.EqOnSource (FiberwiseLinear.partialHomeomorph Φ hU₀ ⋯ ⋯)
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>S : NonUnitalSubalgebra R A<VAR>h : S = ⊤<VAR>x : A<GOAL>x ∈ ⊤
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>S : NonUnitalSubalgebra R A<VAR>h : ∀ (x : A), x ∈ S<VAR>x : A<GOAL>x ∈ S ↔ x ∈ ⊤
<VAR>α✝ : Type u<VAR>β : Type v<VAR>α : Type u_1<VAR>a : α<VAR>f : Filter α<VAR>t : TopologicalSpace α<GOAL>t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen {b}
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite E<GOAL>∃ α, F⟮α⟯ = ⊤
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite E<VAR>α : Eˣ<VAR>hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α<GOAL>∃ α, F⟮α⟯ = ⊤
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite E<VAR>α : Eˣ<VAR>hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α<GOAL>F⟮↑α⟯ = ⊤
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite E<VAR>α : Eˣ<VAR>hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α<GOAL>⊤ ≤ F⟮↑α⟯
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p q : FreeAddMonoid (𝕜 × ((i : ι) → E i))<GOAL>projectiveSeminormAux (p + q) ≤ projectiveSeminormAux p + projectiveSeminormAux q
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p q : FreeAddMonoid (𝕜 × ((i : ι) → E i))<GOAL>(List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) (p + q)).sum ≤ (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p).sum + (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) q).sum
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p q : FreeAddMonoid (𝕜 × ((i : ι) → E i))<GOAL>(List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) (FreeAddMonoid.toList p) ++ List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) (FreeAddMonoid.toList q)).sum ≤ (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p).sum + (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) q).sum
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p q : FreeAddMonoid (𝕜 × ((i : ι) → E i))<GOAL>(List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) (FreeAddMonoid.toList p)).sum + (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) (FreeAddMonoid.toList q)).sum ≤ (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p).sum + (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) q).sum
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>ι : Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<GOAL>↑((piEquivOfFintype I fun x => R).trans (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm) ∘ₗ ofTensorProduct I (ι → R) = LinearMap.id
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>ι : Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<GOAL>↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm ∘ₗ ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) = LinearMap.id
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R : ℝ<VAR>z w : ℂ<VAR>f : ℂ → E<GOAL>∫ (θ : ℝ) in 0 ..2 * π, circleTransform R z w f θ = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(z, R), (z - w)⁻¹ • f z
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R : ℝ<VAR>z w : ℂ<VAR>f : ℂ → E<GOAL>∫ (θ : ℝ) in 0 ..2 * π, (2 * ↑π * I)⁻¹ • ((0 + ↑R * cexp (↑θ * I)) * I) • (z + ↑R * cexp (↑θ * I) - w)⁻¹ • f (z + ↑R * cexp (↑θ * I)) = (2 * ↑π * I)⁻¹ • ∫ (θ : ℝ) in 0 ..2 * π, ((0 + ↑R * cexp (↑θ * I)) * I) • (z + ↑R * cexp (↑θ * I) - w)⁻¹ • f (z + ↑R * cexp (↑θ * I))
<VAR>u : XgcdType<VAR>a b : ℕ+<GOAL>(1 * (↑a - 1 + 1) + 0 * (↑b - 1 + 1), 0 * (↑a - 1 + 1) + 1 * (↑b - 1 + 1)) = (↑a, ↑b)
<VAR>u : XgcdType<VAR>a b : ℕ+<GOAL>(↑a - 1 + 1 + 0, 0 + (↑b - 1 + 1)) = (↑a, ↑b)
<VAR>u : XgcdType<VAR>a b : ℕ+<VAR>this : 0 < ↑a<GOAL>(↑a - 1 + 1 + 0, 0 + (↑b - 1 + 1)) = (↑a, ↑b)
<VAR>u : XgcdType<VAR>a b : ℕ+<VAR>this✝ : 0 < ↑a<VAR>this : 0 < ↑b<GOAL>(↑a - 1 + 1 + 0, 0 + (↑b - 1 + 1)) = (↑a, ↑b)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>X : Ω → E<VAR>ℙ : Measure Ω<VAR>μ : autoParam (Measure E) _auto✝<VAR>s : Set E<GOAL>∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ ≤ (map X ℙ) s
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>X : Ω → E<VAR>ℙ : Measure Ω<VAR>μ : autoParam (Measure E) _auto✝<VAR>s : Set E<GOAL>(withDensity μ (pdf X ℙ μ)) s ≤ (map X ℙ) s
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁸ : Category.{u_13, u_1} C₁<VAR>inst✝⁷ : Category.{u_15, u_2} C₂<VAR>inst✝⁶ : Category.{u_16, u_3} C₃<VAR>inst✝⁵ : Category.{u_11, u_4} C₄<VAR>inst✝⁴ : Category.{?u.292327, u_5} C₁₂<VAR>inst✝³ : Category.{u_14, u_6} C₂₃<VAR>F✝ F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>F : C₁ ⥤ C₂₃ ⥤ C₄<VAR>G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₂₃ : BifunctorComp₂₃IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝² : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>inst✝¹ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>F₁₂ : ?m.294682<VAR>G : ?m.294685<VAR>ρ₁₂ : ?m.294688<VAR>inst✝ : ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<VAR>j : J<VAR>A : C₄<VAR>f g : mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A<VAR>h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j), ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g<GOAL>f = g
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁸ : Category.{u_13, u_1} C₁<VAR>inst✝⁷ : Category.{u_15, u_2} C₂<VAR>inst✝⁶ : Category.{u_16, u_3} C₃<VAR>inst✝⁵ : Category.{u_11, u_4} C₄<VAR>inst✝⁴ : Category.{?u.292327, u_5} C₁₂<VAR>inst✝³ : Category.{u_14, u_6} C₂₃<VAR>F✝ F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>F : C₁ ⥤ C₂₃ ⥤ C₄<VAR>G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₂₃ : BifunctorComp₂₃IndexData r<VAR>X₁ : GradedObject I₁ C₁<VAR>X₂ : GradedObject I₂ C₂<VAR>X₃ : GradedObject I₃ C₃<VAR>inst✝² : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>inst✝¹ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>F₁₂ : ?m.294682<VAR>G : ?m.294685<VAR>ρ₁₂ : ?m.294688<VAR>inst✝ : ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<VAR>j : J<VAR>A : C₄<VAR>f g : mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A<VAR>h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j), ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g<GOAL>∀ (i : ↑(r ⁻¹' {j})), Cofan.inj (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j) i ≫ f = Cofan.inj (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j) i ≫ g
<VAR>S : LightProfinite<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>⇑(S.transitionMapLE h) ∘ ⇑(S.proj m) = ⇑(S.proj n)
<VAR>S : LightProfinite<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>⇑(S.transitionMapLE h) ∘ ⇑(S.proj m) = ⇑(S.proj m ≫ S.diagram.map (Opposite.op (homOfLE h)))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>R : Type u_6<VAR>inst✝¹ : NonAssocRing R<VAR>inst✝ : Fintype R<VAR>p : ℕ<VAR>hn : card R = p<VAR>hR : ∀ i < p, ↑i = 0 → i = 0<VAR>n : ℕ<GOAL>↑n = 0 ↔ p ∣ n
<VAR>G : Type u_1<VAR>H✝ : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>R : Type u_6<VAR>inst✝¹ : NonAssocRing R<VAR>inst✝ : Fintype R<VAR>p : ℕ<VAR>hn : card R = p<VAR>hR : ∀ i < p, ↑i = 0 → i = 0<VAR>n : ℕ<VAR>H : ↑p = 0<GOAL>↑n = 0 ↔ p ∣ n