ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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.75509, u_2} W<VAR>inst✝⁸ : Preadditive W<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_3} W₁<VAR>inst✝⁶ : Category.{u_7, 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>α : Type u_5<VAR>inst✝³ : AddRightCancelSemigroup α<VAR>inst✝² : One α<VAR>inst✝¹ : DecidableEq α<VAR>F : W₁ ⥤ W₂<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X : α → W₁<VAR>d : (n : α) → X (n + 1) ⟶ X n<VAR>sq : ∀ (n : α), d (n + 1) ≫ d n = 0<GOAL>(F.mapHomologicalComplex (ComplexShape.down α)).obj (of X d sq) = of (fun n => F.obj (X n)) (fun n => F.map (d 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.75509, u_2} W<VAR>inst✝⁸ : Preadditive W<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_3} W₁<VAR>inst✝⁶ : Category.{u_7, 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>α : Type u_5<VAR>inst✝³ : AddRightCancelSemigroup α<VAR>inst✝² : One α<VAR>inst✝¹ : DecidableEq α<VAR>F : W₁ ⥤ W₂<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X : α → W₁<VAR>d : (n : α) → X (n + 1) ⟶ X n<VAR>sq : ∀ (n : α), d (n + 1) ≫ d n = 0<GOAL>∀ (i j : α), (ComplexShape.down α).Rel i j → ((F.mapHomologicalComplex (ComplexShape.down α)).obj (of X d sq)).d i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (of (fun n => F.obj (X n)) (fun n => F.map (d n)) ⋯).d i j
<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.75509, u_2} W<VAR>inst✝⁸ : Preadditive W<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_3} W₁<VAR>inst✝⁶ : Category.{u_7, 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>α : Type u_5<VAR>inst✝³ : AddRightCancelSemigroup α<VAR>inst✝² : One α<VAR>inst✝¹ : DecidableEq α<VAR>F : W₁ ⥤ W₂<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X : α → W₁<VAR>d : (n : α) → X (n + 1) ⟶ X n<VAR>sq : ∀ (n : α), d (n + 1) ≫ d n = 0<VAR>j : α<GOAL>((F.mapHomologicalComplex (ComplexShape.down α)).obj (of X d sq)).d (j + 1) j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (of (fun n => F.obj (X n)) (fun n => F.map (d n)) ⋯).d (j + 1) j
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>d : ℕ<VAR>f : K⟦X⟧<GOAL>Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d)) ↔ ∀ n < d, (PowerSeries.coeff K n) f = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>d : ℕ<VAR>f : K⟦X⟧<VAR>this : PowerSeries.X ^ d ∣ f ↔ ∀ n < d, (PowerSeries.coeff K n) f = 0<GOAL>Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d)) ↔ ∀ n < d, (PowerSeries.coeff K n) f = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>d : ℕ<VAR>f : K⟦X⟧<VAR>this : PowerSeries.X ^ d ∣ f ↔ ∀ n < d, (PowerSeries.coeff K n) f = 0<GOAL>(PowerSeries.idealX K).intValuation f ≤ ↑(Multiplicative.ofAdd (-↑d)) ↔ Ideal.span {PowerSeries.X} ^ d ∣ Ideal.span {f}
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : PseudoMetricSpace γ<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>δ : Type u_2<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology δ<VAR>f : α ↪ δ<VAR>g₁ g₂ : α →ᵇ β<VAR>h₁ h₂ : δ →ᵇ β<GOAL>dist (extend f g₁ h₁) (extend f g₂ h₂) = max (dist g₁ g₂) (dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ))
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : PseudoMetricSpace γ<VAR>f✝ g : α →ᵇ β<VAR>x✝ : α<VAR>C : ℝ<VAR>δ : Type u_2<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology δ<VAR>f : α ↪ δ<VAR>g₁ g₂ : α →ᵇ β<VAR>h₁ h₂ : δ →ᵇ β<VAR>x : δ<GOAL>dist ((extend f g₁ h₁) x) ((extend f g₂ h₂) x) ≤ max (dist g₁ g₂) (dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ))
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : PseudoMetricSpace γ<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>δ : Type u_2<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology δ<VAR>f : α ↪ δ<VAR>g₁ g₂ : α →ᵇ β<VAR>h₁ h₂ : δ →ᵇ β<GOAL>dist g₁ g₂ ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : PseudoMetricSpace γ<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>δ : Type u_2<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology δ<VAR>f : α ↪ δ<VAR>g₁ g₂ : α →ᵇ β<VAR>h₁ h₂ : δ →ᵇ β<GOAL>dist (h₁.restrict (range ⇑f)ᶜ) (h₂.restrict (range ⇑f)ᶜ) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasPullbacks C<VAR>P Q R : C<VAR>f : P ⟶ R<VAR>g : Q ⟶ R<VAR>p : Pseudoelement P<VAR>q : Pseudoelement Q<VAR>x : Over P<VAR>y : Over Q<VAR>h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧<GOAL>∃ s, pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasPullbacks C<VAR>P Q R : C<VAR>f : P ⟶ R<VAR>g : Q ⟶ R<VAR>p : Pseudoelement P<VAR>q : Pseudoelement Q<VAR>x : Over P<VAR>y : Over Q<VAR>h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧<VAR>Z : C<VAR>a : Z ⟶ ((fun g => app f g) x).left<VAR>b : Z ⟶ ((fun g_1 => app g g_1) y).left<VAR>ea : Epi a<VAR>eb : Epi b<VAR>comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom<GOAL>∃ s, pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasPullbacks C<VAR>P Q R : C<VAR>f : P ⟶ R<VAR>g : Q ⟶ R<VAR>p : Pseudoelement P<VAR>q : Pseudoelement Q<VAR>x : Over P<VAR>y : Over Q<VAR>h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧<VAR>Z : C<VAR>a : Z ⟶ ((fun g => app f g) x).left<VAR>b : Z ⟶ ((fun g_1 => app g g_1) y).left<VAR>ea : Epi a<VAR>eb : Epi b<VAR>comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom<VAR>l : Z ⟶ pullback f g<VAR>hl₁ : l ≫ pullback.fst f g = a ≫ x.hom<VAR>hl₂ : l ≫ pullback.snd f g = b ≫ y.hom<GOAL>∃ s, pseudoApply (pullback.fst f g) s = ⟦x⟧ ∧ pseudoApply (pullback.snd f g) s = ⟦y⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b✝ a b : α<VAR>s : Finset α<VAR>h : a ≠ b<VAR>x : α<GOAL>x ∈ (insert a s).erase b ↔ x ∈ insert a (s.erase b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b✝ a b : α<VAR>s : Finset α<VAR>h : a ≠ b<VAR>x : α<VAR>this : x ≠ b ∧ x = a ↔ x = a<GOAL>x ∈ (insert a s).erase b ↔ x ∈ insert a (s.erase b)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p q : Submodule R M<VAR>x : M<VAR>xm : x ∈ ⊥<VAR>y : M<VAR>ym : y ∈ ⊥<GOAL>x = y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMul S R<VAR>inst✝ : IsScalarTower S R M<VAR>p q : Submodule R M<VAR>x : M<VAR>xm : x ∈ ⊥<VAR>y : M<VAR>ym : y ∈ ⊥<GOAL>0 = y
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>x : ⨁ (i : ι), A i<GOAL>1 * x = x
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>x : ⨁ (i : ι), A i<GOAL>(mulHom A) One.one = AddMonoidHom.id (⨁ (i : ι), A i)
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>x : ⨁ (i : ι), A i<GOAL>∀ (i : ι) (y : A i), ((mulHom A) One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>x : ⨁ (i : ι), A i<VAR>i : ι<VAR>xi : A i<GOAL>((mulHom A) ((of A 0) GradedMonoid.GOne.one)) ((of A i) xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>x : ⨁ (i : ι), A i<VAR>i : ι<VAR>xi : A i<GOAL>(of A (0 + i)) (GradedMonoid.GMul.mul GradedMonoid.GOne.one xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m : ι<VAR>h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s<GOAL>n ≤ hitting u s n m ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m : ι<VAR>h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s<GOAL>n ≤ m
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m : ι<VAR>h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s<VAR>h : ¬n ≤ m<GOAL>False
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m : ι<VAR>h_exists : ∃ j ∈ ∅, u j ω ∈ s<VAR>h : ¬n ≤ m<GOAL>False
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>j₁ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>b₂ : B<GOAL>a₁ = a₁ * ↑GradedMonoid.GOne.one
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>hs : 1 < s.card<VAR>a : α<GOAL>∃ b ∈ s, b ≠ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>hs : 1 < s.card<VAR>a x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<GOAL>∃ b ∈ s, b ≠ a
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<GOAL>(↑a)⁻¹.toNNReal = (↑a).toNNReal⁻¹
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>(↑0)⁻¹.toNNReal = (↑0).toNNReal⁻¹
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>ha : a ≠ 0<GOAL>(↑a)⁻¹.toNNReal = (↑a).toNNReal⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>∫⁻ (x : α), 0 ∂μ ≠ ⊤
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>f : σ → τ<VAR>h : φ.IsHomogeneous n<GOAL>((rename f) φ).IsHomogeneous n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>f : σ → τ<VAR>h : φ.IsHomogeneous n<GOAL>(∑ x ∈ φ.support, (rename f) ((monomial x) (coeff x φ))).IsHomogeneous n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>f : σ → τ<VAR>h : φ.IsHomogeneous n<GOAL>(∑ x ∈ φ.support, (monomial (mapDomain f x)) (coeff x φ)).IsHomogeneous n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>f : σ → τ<VAR>h : φ.IsHomogeneous n<GOAL>∀ d ∈ φ.support, (mapDomain f d).degree = n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>f : σ → τ<VAR>h : φ.IsHomogeneous n<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ φ.support<GOAL>(mapDomain f d).degree = n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>f : σ → τ<VAR>h : φ.IsHomogeneous n<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ φ.support<GOAL>(d.sum fun a m => (AddMonoidHom.id ℕ) m) = n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>f : σ → τ<VAR>h : φ.IsHomogeneous n<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ φ.support<GOAL>(d.sum fun a m => (AddMonoidHom.id ℕ) m) = (weight 1) d
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.197151, u_1} C<VAR>inst✝³ : Category.{?u.197155, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cocycle K F m<VAR>β : Cochain K G n<VAR>h : n + 1 = m<VAR>eq : δ n m β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0<GOAL>δ n m (liftCochain φ (↑α) β h) = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>X✝ Y✝ : C ⥤ D<VAR>η : X✝ ⟶ Y✝<VAR>A : Augmented C<VAR>n : SimplexCategoryᵒᵖ<GOAL>η.app (A.left.obj n) ≫ Y✝.map (A.hom.app n) ≫ 𝟙 (Y✝.obj A.right) = (X✝.map (A.hom.app n) ≫ 𝟙 (X✝.obj A.right)) ≫ η.app A.right
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<GOAL>∃ a, (quadraticChar F) ↑a = -1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>x✝ : ∃ a, (quadraticChar F) a = -1<VAR>a : F<VAR>ha : (quadraticChar F) a = -1<GOAL>IsUnit a
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>hF : ringChar F ≠ 2<VAR>x✝ : ∃ a, (quadraticChar F) a = -1<VAR>a : F<VAR>ha : ¬IsUnit a<GOAL>¬(quadraticChar F) a = -1
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>map valEmbedding (Ioo a b) = Ioo ↑a ↑b
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<VAR>v : V<GOAL>(s.weightedVSubOfPoint (v +ᵥ p) b) w = (s.weightedVSubOfPoint p (-v +ᵥ b)) w
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<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 : C ⟶ D<VAR>h : Homotopy f g<VAR>i j : ι<VAR>w : ¬c.Rel j i<GOAL>(-h.hom) i j = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<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 : C ⟶ D<VAR>h : Homotopy f g<VAR>i : ι<GOAL>g.f i = (dNext i) (-h.hom) + (prevD i) (-h.hom) + f.f i
<VAR>p q : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hq : Fact (Nat.Prime q)<VAR>n m : ℕ<VAR>neq : q ≠ p<GOAL>padicValNat q (p ^ n * q ^ m) = m
<VAR>p q : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hq : Fact (Nat.Prime q)<VAR>n m : ℕ<VAR>neq : q ≠ p<GOAL>padicValNat q (q ^ m * p ^ n) = m
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i →L[𝕜] E₁ i<VAR>m : (i : ι) → E i<GOAL>‖g‖ * ∏ i : ι, ‖f i‖ * ‖m i‖ = (‖g‖ * ∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>a b c : ℤ<VAR>h : a + b = c<VAR>x✝ : CochainComplex C ℤ<VAR>i✝ : ℤ<GOAL>((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b c h).hom.app x✝).f i✝ = ((shiftFunctorAdd' C a b c h).hom.app x✝).f i✝
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime (x + z * y) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel ν<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set (β × ℝ)<VAR>hs : MeasurableSet s<GOAL>((ν ⊗ₖ IsCondKernelCDF.toKernel f hf) a) s = (κ a) s
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>h : ∀ V ∈ 𝓤 α, SymmetricRel V → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y V<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α ∧ SymmetricRel V<GOAL>∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ id V}
<VAR>x y✝ z : ℝ<VAR>n✝ : ℕ<VAR>hx : 0 ≤ x<VAR>y : ℝ<VAR>n : ℤ<GOAL>x ^ (y * ↑n) = (x ^ y) ^ n
<VAR>k n m : Nat<VAR>H : k.Coprime n<GOAL>((k * m).gcd n).Coprime k
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>i : Γ<VAR>hi : ↑i < x.orderTop<GOAL>x.coeff i = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>i : Γ<VAR>hi : ↑i < orderTop 0<GOAL>coeff 0 i = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>i : Γ<VAR>hi : ↑i < x.orderTop<VAR>hx : x ≠ 0<GOAL>x.coeff i = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>i : Γ<VAR>hx : x ≠ 0<VAR>hi : x.coeff i ≠ 0<GOAL>¬↑i < x.orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>i : Γ<VAR>hx : x ≠ 0<VAR>hi : i ∈ x.support<GOAL>¬↑i < x.orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>i : Γ<VAR>hx : x ≠ 0<VAR>hi : i ∈ x.support<GOAL>¬i < ⋯.min ⋯
<VAR>s : ℝ<GOAL>Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π
<VAR>s : ℝ<GOAL>↑(Gamma s * Gamma (s + 1 / 2)) = ↑(Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π)
<VAR>K✝ : Type u<VAR>V : Type v<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Ring K<VAR>inst✝² : IsDomain K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : FiniteDimensional F K<VAR>x : K<VAR>H : x ≠ 0<GOAL>∃ y, x * y = 1
<VAR>K✝ : Type u<VAR>V : Type v<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Ring K<VAR>inst✝² : IsDomain K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : FiniteDimensional F K<VAR>x : K<VAR>H : x ≠ 0<VAR>this : Surjective ⇑(LinearMap.mulLeft F x)<GOAL>∃ y, x * y = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>s t✝ : Set β<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : β → E<VAR>a : α<VAR>hs : MeasurableSet s<VAR>t : Set β<GOAL>∫ (x : β) in t, f x ∂(κ.restrict hs) a = ∫ (x : β) in t ∩ s, f x ∂κ a
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : SuccOrder β<VAR>inst✝¹ : IsSuccArchimedean β<VAR>inst✝ : Nonempty β<VAR>s : β → Set α<VAR>H : ∀ (n : β), IsConnected (s n)<VAR>K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty<VAR>i✝ j i : β<VAR>x✝ : i ∈ Ico j i✝<GOAL>(s (succ i) ∩ s i).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : SuccOrder β<VAR>inst✝¹ : IsSuccArchimedean β<VAR>inst✝ : Nonempty β<VAR>s : β → Set α<VAR>H : ∀ (n : β), IsConnected (s n)<VAR>K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty<VAR>i✝ j i : β<VAR>x✝ : i ∈ Ico j i✝<GOAL>(s i ∩ s (succ i)).Nonempty
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝¹ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<GOAL>∫⁻ (x : E), pdf X ℙ μ x ∂μ = ℙ Set.univ
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<GOAL>IsTopologicalBasis {s | ∃ x n, s = cylinder x n}
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<GOAL>∀ u ∈ {s | ∃ x n, s = cylinder x n}, IsOpen u
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<GOAL>∀ (a : (n : ℕ) → E n) (u : Set ((n : ℕ) → E n)), a ∈ u → IsOpen u → ∃ v ∈ {s | ∃ x n, s = cylinder x n}, a ∈ v ∧ v ⊆ u
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : NonAssocSemiring R<VAR>d n : ℕ<GOAL>∑ ij ∈ antidiagonal n, (d + ij.2).choose d = (d + n).choose d + (d + n).choose d.succ
<VAR>R : Type u_1<VAR>inst✝⁴ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>x y : M<GOAL>SameRay R (-x) y ↔ SameRay R x (-y)
<VAR>σ K : Type u<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Field K<VAR>inst✝ : Finite σ<VAR>p : MvPolynomial σ K<VAR>h : ∀ (v : σ → K), (eval v) p = 0<VAR>hp : p ∈ restrictDegree σ K (Fintype.card K - 1)<VAR>p' : R σ K := ⟨p, hp⟩<VAR>this : p' ∈ ker (evalᵢ σ K)<GOAL>p' = 0
<VAR>α : Type u_1<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>h : (node s l x r).Sized<GOAL>node s l x r = l.node' x r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>z : Sym2 α<VAR>h : a ∈ z<GOAL>Mem.other h = Mem.other' h
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>f : α → Computation β<GOAL>(pure a).bind f = f a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>f : α → Computation β<GOAL>IsBisimulation fun c₁ c₂ => c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>f : α → Computation β<GOAL>(pure a).bind f = (pure a).bind f ∧ f a = f a ∨ (pure a).bind f = corec (Bind.f f) (Sum.inr (f a))
<VAR>a : ℤ<VAR>ha0 : 0 < a<GOAL>(↑a)⁻¹.num = 1
<VAR>a : ℤ<VAR>ha0 : 0 < a<GOAL>(↑1 / ↑a).num = 1
<VAR>a : ℤ<VAR>ha0 : 0 < a<GOAL>(Int.natAbs 1).Coprime a.natAbs
<VAR>a : ℤ<VAR>ha0 : 0 < a<GOAL>Nat.Coprime 1 a.natAbs
<VAR>n : ℕ<GOAL>logTaylor n 0 = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<GOAL>a < ↑⌊a⌋₊ + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>a : Fin (n + 1) → ℕ<GOAL>(map d) a = a 0 + (∑ x : Fin n, a x.succ * d ^ ↑x) * d
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<GOAL>countP p l ≤ l.length
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<GOAL>(filter p l).length ≤ l.length
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>X Y Z T : C<VAR>n m : ℕ<VAR>β : Ext Y Z m<VAR>p : ℕ<VAR>h : n + m = p<VAR>this : HasDerivedCategory C := HasDerivedCategory.standard C<GOAL>(comp 0 β h).hom = hom 0