ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N✝ : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N✝<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N✝<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N✝<VAR>g : N✝ →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>N : Submodule R M<GOAL>Exact ⇑(lTensor Q N.subtype) ⇑(lTensor Q N.mkQ)
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>f : F[X]<VAR>hf : Irreducible f<VAR>h : derivative f ≠ 0<VAR>g : F[X]<VAR>hg1 : g ∈ nonunits F[X]<VAR>_hg2 : g ≠ 0<VAR>x✝ : g ∣ f<VAR>hg4 : g ∣ derivative f<VAR>p : F[X]<VAR>hg3 : f = g * p<VAR>u : F[X]ˣ<VAR>hu : ↑u = p<GOAL>g * ↑u ∣ derivative f
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M →[L] N<VAR>s : L.Substructure M<VAR>hs : s.FG<VAR>t : Set M<VAR>ht : t.Finite ∧ (closure L).toFun t = s<GOAL>(closure L).toFun (⇑f '' t) = Substructure.map f s
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Zero α<VAR>v : l ⊕ m → α<GOAL>(of fun i j => diagonal v (Sum.inl i) (Sum.inl j)) = diagonal fun i => v (Sum.inl i)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Zero α<VAR>v : l ⊕ m → α<VAR>i j : l<GOAL>of (fun i j => diagonal v (Sum.inl i) (Sum.inl j)) i j = diagonal (fun i => v (Sum.inl i)) i j
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>h0 : ¬x.gcd y = 0<GOAL>h.IsClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>h0 : ¬x.gcd y = 0<GOAL>⋯.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>h0 : ¬x.gcd y = 0<GOAL>(x / ↑(x.gcd y)).gcd (y / ↑(x.gcd y)) = 1
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<GOAL>∃ t, t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p => closedBall p.1 p.2
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<GOAL>∃ t, t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p => closedBall p.1 p.2
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>P : Finset (α × ℝ) → Prop := fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1<VAR>F : Finset (α × ℝ) → Finset (α × ℝ)<VAR>hF : ∀ (t : Finset (α × ℝ)), P t → t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)<VAR>u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅<GOAL>∃ t, t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p => closedBall p.1 p.2
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>P : Finset (α × ℝ) → Prop := fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1<VAR>F : Finset (α × ℝ) → Finset (α × ℝ)<VAR>hF : ∀ (t : Finset (α × ℝ)), P t → t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)<VAR>u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅<VAR>u_succ : ∀ (n : ℕ), u n.succ = F (u n)<GOAL>∃ t, t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p => closedBall p.1 p.2
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>P : Finset (α × ℝ) → Prop := fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1<VAR>F : Finset (α × ℝ) → Finset (α × ℝ)<VAR>hF : ∀ (t : Finset (α × ℝ)), P t → t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)<VAR>u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅<VAR>u_succ : ∀ (n : ℕ), u n.succ = F (u n)<VAR>Pu : ∀ (n : ℕ), P (u n)<GOAL>∃ t, t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p => closedBall p.1 p.2
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>P : Finset (α × ℝ) → Prop := fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1<VAR>F : Finset (α × ℝ) → Finset (α × ℝ)<VAR>hF : ∀ (t : Finset (α × ℝ)), P t → t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)<VAR>u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅<VAR>u_succ : ∀ (n : ℕ), u n.succ = F (u n)<VAR>Pu : ∀ (n : ℕ), P (u n)<GOAL>∀ p ∈ ⋃ n, ↑(u n), p.1 ∈ s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>P : Finset (α × ℝ) → Prop := fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1<VAR>F : Finset (α × ℝ) → Finset (α × ℝ)<VAR>hF : ∀ (t : Finset (α × ℝ)), P t → t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)<VAR>u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅<VAR>u_succ : ∀ (n : ℕ), u n.succ = F (u n)<VAR>Pu : ∀ (n : ℕ), P (u n)<GOAL>∀ p ∈ ⋃ n, ↑(u n), p.2 ∈ f p.1
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>P : Finset (α × ℝ) → Prop := fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1<VAR>F : Finset (α × ℝ) → Finset (α × ℝ)<VAR>hF : ∀ (t : Finset (α × ℝ)), P t → t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)<VAR>u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅<VAR>u_succ : ∀ (n : ℕ), u n.succ = F (u n)<VAR>Pu : ∀ (n : ℕ), P (u n)<GOAL>μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) = 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : HasBesicovitchCovering α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → Set ℝ<VAR>s : Set α<VAR>hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>P : Finset (α × ℝ) → Prop := fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1<VAR>F : Finset (α × ℝ) → Finset (α × ℝ)<VAR>hF : ∀ (t : Finset (α × ℝ)), P t → t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)<VAR>u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅<VAR>u_succ : ∀ (n : ℕ), u n.succ = F (u n)<VAR>Pu : ∀ (n : ℕ), P (u n)<GOAL>(⋃ n, ↑(u n)).PairwiseDisjoint fun p => closedBall p.1 p.2
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = ideal R S
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤ ideal R S
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>ideal R S ≤ Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>a : R<VAR>m : ℕ<GOAL>(trunc (n + 1) ((C R) a)).coeff m = (Polynomial.C a).coeff m
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>a : R<VAR>m : ℕ<GOAL>(if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : 0 < p.radius<GOAL>∃ C r, ∃ (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : 0 < p.radius<VAR>r : ℝ≥0<VAR>r0 : 0 < ↑r<VAR>rlt : ↑r < p.radius<GOAL>∃ C r, ∃ (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : 0 < p.radius<VAR>r : ℝ≥0<VAR>r0 : 0 < ↑r<VAR>rlt : ↑r < p.radius<VAR>rpos : 0 < ↑r<GOAL>∃ C r, ∃ (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : 0 < p.radius<VAR>r : ℝ≥0<VAR>r0 : 0 < ↑r<VAR>rlt : ↑r < p.radius<VAR>rpos : 0 < ↑r<VAR>C : ℝ<VAR>Cpos : C > 0<VAR>hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n<GOAL>∃ C r, ∃ (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : 0 < p.radius<VAR>r : ℝ≥0<VAR>r0 : 0 < ↑r<VAR>rlt : ↑r < p.radius<VAR>rpos : 0 < ↑r<VAR>C : ℝ<VAR>Cpos : C > 0<VAR>hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n<VAR>n : ℕ<GOAL>‖p n‖ ≤ C * (↑r)⁻¹ ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : 0 < p.radius<VAR>r : ℝ≥0<VAR>r0 : 0 < ↑r<VAR>rlt : ↑r < p.radius<VAR>rpos : 0 < ↑r<VAR>C : ℝ<VAR>Cpos : C > 0<VAR>hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n<VAR>n : ℕ<GOAL>‖p n‖ ≤ C / ↑r ^ n
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁹ : Category.{v, u} V<VAR>inst✝⁸ : Preadditive V<VAR>W : Type u_2<VAR>inst✝⁷ : Category.{?u.62271, u_2} W<VAR>inst✝⁶ : Preadditive W<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>inst✝⁵ : Category.{?u.62296, u_3} W₁<VAR>inst✝⁴ : Category.{?u.62300, u_4} W₂<VAR>inst✝³ : HasZeroMorphisms W₁<VAR>inst✝² : HasZeroMorphisms W₂<VAR>c✝ : ComplexShape ι<VAR>C D E : HomologicalComplex V c✝<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>F G : W₁ ⥤ W₂<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : G.PreservesZeroMorphisms<VAR>α : F ≅ G<VAR>c : ComplexShape ι<GOAL>NatTrans.mapHomologicalComplex α.hom c ≫ NatTrans.mapHomologicalComplex α.inv c = 𝟙 (F.mapHomologicalComplex c)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁹ : Category.{v, u} V<VAR>inst✝⁸ : Preadditive V<VAR>W : Type u_2<VAR>inst✝⁷ : Category.{?u.62271, u_2} W<VAR>inst✝⁶ : Preadditive W<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>inst✝⁵ : Category.{?u.62296, u_3} W₁<VAR>inst✝⁴ : Category.{?u.62300, u_4} W₂<VAR>inst✝³ : HasZeroMorphisms W₁<VAR>inst✝² : HasZeroMorphisms W₂<VAR>c✝ : ComplexShape ι<VAR>C D E : HomologicalComplex V c✝<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>F G : W₁ ⥤ W₂<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : G.PreservesZeroMorphisms<VAR>α : F ≅ G<VAR>c : ComplexShape ι<GOAL>NatTrans.mapHomologicalComplex α.inv c ≫ NatTrans.mapHomologicalComplex α.hom c = 𝟙 (G.mapHomologicalComplex c)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝² : Add α<VAR>inst✝¹ : MulOneClass α<VAR>inst✝ : LeftDistribClass α<VAR>a b : α<GOAL>a * (1 + b) = a + a * b
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>n : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<VAR>a : R<GOAL>(coeff R n) (φ * (C σ R) a) = (coeff R n) φ * a
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ : MulChar R R'<GOAL>χ ≠ 1 ↔ ∃ a, χ ↑a ≠ 1
<VAR>m n : ℕ<GOAL>↑(m / n) = ↑m / ↑n
<VAR>m : ℕ<GOAL>↑(m / 0) = ↑m / ↑0
<VAR>m n : ℕ<VAR>hn : n ≠ 0<GOAL>↑(m / n) = ↑m / ↑n
<VAR>C : Type u_3<VAR>D : Type ?u.25151<VAR>inst✝¹ : Category.{u_2, u_3} C<VAR>inst✝ : Category.{?u.25159, ?u.25151} D<VAR>X : C<VAR>S T : Presieve X<VAR>P : Cᵒᵖ ⥤ Type u_1<VAR>H : S.FactorsThru T<VAR>hS : IsSheafFor P S<VAR>h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f<GOAL>IsSheafFor P T
<VAR>C : Type u_3<VAR>D : Type ?u.25151<VAR>inst✝¹ : Category.{u_2, u_3} C<VAR>inst✝ : Category.{?u.25159, ?u.25151} D<VAR>X : C<VAR>S T : Presieve X<VAR>P : Cᵒᵖ ⥤ Type u_1<VAR>H : S.FactorsThru T<VAR>h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f<VAR>hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t<GOAL>IsSeparatedFor P T ∧ ∀ (x : FamilyOfElements P T), x.Compatible → ∃ t, x.IsAmalgamation t
<VAR>C : Type u_3<VAR>D : Type ?u.25151<VAR>inst✝¹ : Category.{u_2, u_3} C<VAR>inst✝ : Category.{?u.25159, ?u.25151} D<VAR>X : C<VAR>S T : Presieve X<VAR>P : Cᵒᵖ ⥤ Type u_1<VAR>h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f<VAR>hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t<VAR>W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C<VAR>i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a<VAR>e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X<VAR>h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)<VAR>h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g<VAR>x : FamilyOfElements P T<VAR>hx : x.Compatible<VAR>y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) ⋯)<GOAL>∃ t, x.IsAmalgamation t
<VAR>C : Type u_3<VAR>D : Type ?u.25151<VAR>inst✝¹ : Category.{u_2, u_3} C<VAR>inst✝ : Category.{?u.25159, ?u.25151} D<VAR>X : C<VAR>S T : Presieve X<VAR>P : Cᵒᵖ ⥤ Type u_1<VAR>h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f<VAR>hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t<VAR>W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C<VAR>i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a<VAR>e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X<VAR>h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)<VAR>h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g<VAR>x : FamilyOfElements P T<VAR>hx : x.Compatible<VAR>y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) ⋯)<VAR>hy : y.Compatible<GOAL>∃ t, x.IsAmalgamation t
<VAR>C : Type u_3<VAR>D : Type ?u.25151<VAR>inst✝¹ : Category.{u_2, u_3} C<VAR>inst✝ : Category.{?u.25159, ?u.25151} D<VAR>X : C<VAR>S T : Presieve X<VAR>P : Cᵒᵖ ⥤ Type u_1<VAR>h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f<VAR>hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t<VAR>W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C<VAR>i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a<VAR>e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X<VAR>h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)<VAR>h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g<VAR>x : FamilyOfElements P T<VAR>hx : x.Compatible<VAR>y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) ⋯)<VAR>hy : y.Compatible<VAR>left✝ : IsSeparatedFor P S<VAR>h2' : ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t<VAR>z : P.obj (Opposite.op X)<VAR>hz : y.IsAmalgamation z<VAR>Y : C<VAR>g : Y ⟶ X<VAR>hg : T g<VAR>R : Presieve Y<VAR>hR1 : IsSeparatedFor P R<VAR>WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C<VAR>ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a<VAR>ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X<VAR>hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)<VAR>hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g<GOAL>P.map g.op z = x g hg
<VAR>C : Type u_3<VAR>D : Type ?u.25151<VAR>inst✝¹ : Category.{u_2, u_3} C<VAR>inst✝ : Category.{?u.25159, ?u.25151} D<VAR>X : C<VAR>S T : Presieve X<VAR>P : Cᵒᵖ ⥤ Type u_1<VAR>h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f<VAR>hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t<VAR>W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C<VAR>i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a<VAR>e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X<VAR>h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)<VAR>h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g<VAR>x : FamilyOfElements P T<VAR>hx : x.Compatible<VAR>y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) ⋯)<VAR>hy : y.Compatible<VAR>left✝ : IsSeparatedFor P S<VAR>h2' : ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t<VAR>z : P.obj (Opposite.op X)<VAR>hz : y.IsAmalgamation z<VAR>Y : C<VAR>g : Y ⟶ X<VAR>hg : T g<VAR>R : Presieve Y<VAR>hR1 : IsSeparatedFor P R<VAR>WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C<VAR>ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a<VAR>ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X<VAR>hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)<VAR>hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g<VAR>Q : C<VAR>t : Q ⟶ Y<VAR>ht : R t<GOAL>P.map t.op (P.map g.op z) = P.map t.op (x g hg)
<VAR>C : Type u_3<VAR>D : Type ?u.25151<VAR>inst✝¹ : Category.{u_2, u_3} C<VAR>inst✝ : Category.{?u.25159, ?u.25151} D<VAR>X : C<VAR>S T : Presieve X<VAR>P : Cᵒᵖ ⥤ Type u_1<VAR>h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f<VAR>hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t<VAR>W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C<VAR>i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a<VAR>e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X<VAR>h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)<VAR>h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g<VAR>x : FamilyOfElements P T<VAR>hx : x.Compatible<VAR>y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) ⋯)<VAR>hy : y.Compatible<VAR>left✝ : IsSeparatedFor P S<VAR>h2' : ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t<VAR>z : P.obj (Opposite.op X)<VAR>hz : y.IsAmalgamation z<VAR>Y : C<VAR>g : Y ⟶ X<VAR>hg : T g<VAR>R : Presieve Y<VAR>hR1 : IsSeparatedFor P R<VAR>WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C<VAR>ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a<VAR>ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X<VAR>hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)<VAR>hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g<VAR>Q : C<VAR>t : Q ⟶ Y<VAR>ht : R t<GOAL>P.map (ii ht ≫ i ⋯).op (x (e ⋯) ⋯) = P.map t.op (x g hg)
<VAR>C : Type u_3<VAR>D : Type ?u.25151<VAR>inst✝¹ : Category.{u_2, u_3} C<VAR>inst✝ : Category.{?u.25159, ?u.25151} D<VAR>X : C<VAR>S T : Presieve X<VAR>P : Cᵒᵖ ⥤ Type u_1<VAR>h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f<VAR>hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t<VAR>W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C<VAR>i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a<VAR>e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X<VAR>h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)<VAR>h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g<VAR>x : FamilyOfElements P T<VAR>hx : x.Compatible<VAR>y : FamilyOfElements P S := fun Y g hg => P.map (i hg).op (x (e hg) ⋯)<VAR>hy : y.Compatible<VAR>left✝ : IsSeparatedFor P S<VAR>h2' : ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t<VAR>z : P.obj (Opposite.op X)<VAR>hz : y.IsAmalgamation z<VAR>Y : C<VAR>g : Y ⟶ X<VAR>hg : T g<VAR>R : Presieve Y<VAR>hR1 : IsSeparatedFor P R<VAR>WW : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → R g → C<VAR>ii : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → Z ⟶ WW a<VAR>ee : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (a : R g) → WW a ⟶ X<VAR>hh1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (a : R g), S (ee a)<VAR>hh2 : ∀ ⦃Z : C⦄ ⦃g_1 : Z ⟶ Y⦄ (a : R g_1), ii a ≫ ee a = g_1 ≫ g<VAR>Q : C<VAR>t : Q ⟶ Y<VAR>ht : R t<GOAL>(ii ht ≫ i ⋯) ≫ e ⋯ = t ≫ g
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w u v : V<VAR>p : G.Walk u v<VAR>h : p.IsPath<GOAL>p.reverse.IsPath