ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : ProjectiveResolution X<VAR>β : (projectiveResolution X).complex ⟶ P.complex<VAR>hβ : (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map β = P.iso.hom<GOAL>(HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app ((projectiveResolutions C).obj X).as) ≫ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((G.mapHomologicalComplex (ComplexShape.down ℕ)).map β) = (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map β) ≫ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : ProjectiveResolution X<VAR>β : (projectiveResolution X).complex ⟶ P.complex<VAR>hβ : (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map β = P.iso.hom<GOAL>(HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app ((projectiveResolutions C).obj X).as ≫ (G.mapHomologicalComplex (ComplexShape.down ℕ)).map β) = (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app (projectiveResolution X).complex ≫ (G.mapHomologicalComplex (ComplexShape.down ℕ)).map β)
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>pn : p.natDegree < n<GOAL>(p + q).coeff n = q.coeff n
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>pn : p.natDegree < n<GOAL>(q + p).coeff n = q.coeff n
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g₁ g₂ : Fix F → α<VAR>h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)<VAR>x✝ : Fix F<VAR>a : (P F).A<VAR>f : (P F).B a → WType (P F).B<VAR>ih : ∀ (a : (P F).B a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))<GOAL>g₁ ⟦WType.mk a f⟧ = g₂ ⟦WType.mk a f⟧
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g₁ g₂ : Fix F → α<VAR>h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)<VAR>x✝ : Fix F<VAR>a : (P F).A<VAR>f : (P F).B a → WType (P F).B<VAR>ih : ∀ (a : (P F).B a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))<GOAL>g₁ (mk (abs ⟨a, fun x => ⟦f x⟧⟩)) = g₂ (mk (abs ⟨a, fun x => ⟦f x⟧⟩))
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g₁ g₂ : Fix F → α<VAR>h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)<VAR>x✝ : Fix F<VAR>a : (P F).A<VAR>f : (P F).B a → WType (P F).B<VAR>ih : ∀ (a : (P F).B a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))<GOAL>g₁ <$> abs ⟨a, fun x => ⟦f x⟧⟩ = g₂ <$> abs ⟨a, fun x => ⟦f x⟧⟩
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>g₁ g₂ : Fix F → α<VAR>h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)<VAR>x✝ : Fix F<VAR>a : (P F).A<VAR>f : (P F).B a → WType (P F).B<VAR>ih : ∀ (a : (P F).B a), g₁ (Quot.mk Setoid.r (f a)) = g₂ (Quot.mk Setoid.r (f a))<GOAL>abs ⟨a, g₁ ∘ fun x => ⟦f x⟧⟩ = abs ⟨a, g₂ ∘ fun x => ⟦f x⟧⟩
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>a b c : K<VAR>ha : a ≠ 0<VAR>h : ∀ (x : K), 0 < a * x * x + b * x + c<GOAL>discrim a b c < 0
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>a b c : K<VAR>ha : a ≠ 0<VAR>h : ∀ (x : K), 0 < a * x * x + b * x + c<VAR>this : ∀ (x : K), 0 ≤ a * x * x + b * x + c<GOAL>discrim a b c < 0
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>a b c : K<VAR>ha : a ≠ 0<VAR>h : ∀ (x : K), 0 < a * x * x + b * x + c<VAR>this : ∀ (x : K), 0 ≤ a * x * x + b * x + c<VAR>h' : discrim a b c = 0<GOAL>False
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>a b c : K<VAR>ha : a ≠ 0<VAR>h : ∀ (x : K), 0 < a * x * x + b * x + c<VAR>this✝ : ∀ (x : K), 0 ≤ a * x * x + b * x + c<VAR>h' : discrim a b c = 0<VAR>this : 0 < a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c<GOAL>False
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>a b c : K<VAR>ha : a ≠ 0<VAR>h : ∀ (x : K), 0 < a * x * x + b * x + c<VAR>this✝¹ : ∀ (x : K), 0 ≤ a * x * x + b * x + c<VAR>h' : discrim a b c = 0<VAR>this✝ : 0 < a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c<VAR>this : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0<GOAL>False
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<GOAL>(e.subtypeRestr hs).source = Subtype.val ⁻¹' e.source
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>f : α → E<VAR>hfi : Integrable f μ<VAR>fs : ι → α → E<VAR>l : Filter ι<VAR>hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ<VAR>hfs : Tendsto (fun i => ∫⁻ (x : α), ↑‖fs i x - f x‖₊ ∂μ) l (𝓝 0)<GOAL>Tendsto (fun i => setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>a a' : α<VAR>h : a ≠ a'<VAR>x✝ : M<GOAL>(lapply a ∘ₗ lsingle a') x✝ = 0 x✝
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>N : Subgroup G<VAR>tn : N.Normal<VAR>a✝ : G<VAR>h : a✝ ∈ N<VAR>a : G<VAR>hc : a ∈ conjugatesOf a✝<GOAL>a ∈ ↑N
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>N : Subgroup G<VAR>tn : N.Normal<VAR>a : G<VAR>h : a ∈ N<VAR>c : G<VAR>hc : c * a * c⁻¹ ∈ conjugatesOf a<GOAL>c * a * c⁻¹ ∈ ↑N
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommSemiring R<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>r : R<VAR>n : ℕ<GOAL>(PowerSeries.coeff A n) (__src✝.toFun ((algebraMap R (HahnSeries ℕ A)) r)) = (PowerSeries.coeff A n) ((algebraMap R (PowerSeries A)) r)
<VAR>n✝ m n : ℕ<VAR>a : Fin n<VAR>b : Fin (n + 1)<GOAL>a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
<VAR>n✝ m n : ℕ<VAR>a : Fin n<VAR>b : Fin (n + 1)<VAR>h : a.castSucc < b<GOAL>a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
<VAR>n✝ m n : ℕ<VAR>a : Fin n<VAR>b : Fin (n + 1)<VAR>h : b ≤ a.castSucc<GOAL>a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x : ℝ≥0∞<GOAL>x ∈ ⋃ n, Iio ↑n ↔ x ∈ {⊤}ᶜ
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x : ℝ≥0∞<GOAL>(∃ i, x ∈ Iio ↑i) ↔ x ∈ {⊤}ᶜ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.39244, u_1} C<VAR>inst✝³ : Category.{?u.39248, 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>d e : ℤ<VAR>γ : Cochain F K d<VAR>he : 1 + d = e<GOAL>-1 + e = d
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.39248, 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>d e : ℤ<VAR>γ : Cochain F K d<VAR>he : 1 + d = e<GOAL>(inl φ).comp ((↑(fst φ)).comp γ he) ⋯ = γ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : DecidableEq (Ideal R)<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>r X : R<VAR>hr : r ≠ 0<VAR>hX₁ : normUnit X = 1<VAR>hX : Prime X<GOAL>Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count X (normalizedFactors r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : IsBigOWith c l k₁ k₂<VAR>h₂ : IsBigOWith c' l f' g'<GOAL>IsBigOWith (c * c') l (fun x => k₁ x • f' x) fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖<VAR>h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖<GOAL>∀ᶠ (x : α) in l, ‖k₁ x • f' x‖ ≤ c * c' * ‖k₂ x • g' x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖<VAR>h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖<VAR>a✝ : α<VAR>hx₁ : ‖k₁ a✝‖ ≤ c * ‖k₂ a✝‖<VAR>hx₂ : ‖f' a✝‖ ≤ c' * ‖g' a✝‖<GOAL>‖k₁ a✝ • f' a✝‖ ≤ c * c' * ‖k₂ a✝ • g' a✝‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖<VAR>h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖<VAR>a✝ : α<VAR>hx₁ : ‖k₁ a✝‖ ≤ c * ‖k₂ a✝‖<VAR>hx₂ : ‖f' a✝‖ ≤ c' * ‖g' a✝‖<GOAL>‖k₁ a✝‖ * ‖f' a✝‖ ≤ c * c' * ‖k₂ a✝ • g' a✝‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖<VAR>h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖<VAR>a✝ : α<VAR>hx₁ : ‖k₁ a✝‖ ≤ c * ‖k₂ a✝‖<VAR>hx₂ : ‖f' a✝‖ ≤ c' * ‖g' a✝‖<GOAL>c * c' * ‖k₂ a✝ • g' a✝‖ = c * ‖k₂ a✝‖ * (c' * ‖g' a✝‖)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f₁₁ : X₁ ⟶ Y₁<VAR>f₁₂ : X₁ ⟶ Y₂<VAR>f₂₁ : X₂ ⟶ Y₁<VAR>f₂₂ : X₂ ⟶ Y₂<VAR>W X Y Z : C<VAR>f : W ⊞ X ⟶ Y ⊞ Z<VAR>inst✝ : IsIso f<GOAL>𝟙 W = 0 ∨ biprod.inl ≫ f ≫ biprod.fst ≠ 0 ∨ biprod.inl ≫ f ≫ biprod.snd ≠ 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f₁₁ : X₁ ⟶ Y₁<VAR>f₁₂ : X₁ ⟶ Y₂<VAR>f₂₁ : X₂ ⟶ Y₁<VAR>f₂₂ : X₂ ⟶ Y₂<VAR>W X Y Z : C<VAR>f : W ⊞ X ⟶ Y ⊞ Z<VAR>inst✝ : IsIso f<VAR>h : 𝟙 W ≠ 0 ∧ biprod.inl ≫ f ≫ biprod.fst = 0 ∧ biprod.inl ≫ f ≫ biprod.snd = 0<GOAL>False
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f₁₁ : X₁ ⟶ Y₁<VAR>f₁₂ : X₁ ⟶ Y₂<VAR>f₂₁ : X₂ ⟶ Y₁<VAR>f₂₂ : X₂ ⟶ Y₂<VAR>W X Y Z : C<VAR>f : W ⊞ X ⟶ Y ⊞ Z<VAR>inst✝ : IsIso f<VAR>nz : 𝟙 W ≠ 0<VAR>a₁ : biprod.inl ≫ f ≫ biprod.fst = 0<VAR>a₂ : biprod.inl ≫ f ≫ biprod.snd = 0<VAR>x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst<VAR>h₁ : x = 𝟙 W<GOAL>False
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasBinaryBiproducts C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f₁₁ : X₁ ⟶ Y₁<VAR>f₁₂ : X₁ ⟶ Y₂<VAR>f₂₁ : X₂ ⟶ Y₁<VAR>f₂₂ : X₂ ⟶ Y₂<VAR>W X Y Z : C<VAR>f : W ⊞ X ⟶ Y ⊞ Z<VAR>inst✝ : IsIso f<VAR>nz : 𝟙 W ≠ 0<VAR>a₁ : biprod.inl ≫ f ≫ biprod.fst = 0<VAR>a₂ : biprod.inl ≫ f ≫ biprod.snd = 0<VAR>x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst<VAR>h₁ : x = 𝟙 W<VAR>h₀ : x = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>f : R[X]<VAR>inst✝¹ : DistribSMul S R<VAR>inst✝ : IsScalarTower S R R<VAR>a : S<VAR>x : R<GOAL>a • (of f) x = (of f) (a • x)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>h : [].length - 1 < [].length<GOAL>False
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t : Set α<VAR>I : Set ι<VAR>hI : I.Countable<VAR>s : ι → Set α<GOAL>μ (⋃ i ∈ I, s i) = 0 ↔ ∀ i ∈ I, μ (s i) = 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t : Set α<VAR>I : Set ι<VAR>hI : I.Countable<VAR>s : ι → Set α<VAR>h : ∀ i ∈ I, μ (s i) = 0<GOAL>μ (⋃ i ∈ I, s i) = 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t : Set α<VAR>I : Set ι<VAR>hI : I.Countable<VAR>s : ι → Set α<VAR>h : ∀ i ∈ I, μ (s i) = 0<VAR>x✝ : Countable ↑I<GOAL>μ (⋃ i ∈ I, s i) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>b : β<GOAL>b ∈ (p.bindOnSupport f).support ↔ ∃ a, ∃ (h : a ∈ p.support), b ∈ (f a h).support
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<GOAL>M ∈ Set.range ⇑(scalar n) ↔ ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<VAR>x✝¹ : M ∈ Set.range ⇑(scalar n)<VAR>i j : n<VAR>x✝ : i ≠ j<VAR>r : α<VAR>hr : (scalar n) r = M<GOAL>Commute ((scalar n) r) (stdBasisMatrix i j 1)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<VAR>x✝¹ : M ∈ Set.range ⇑(scalar n)<VAR>i j : n<VAR>x✝ : i ≠ j<VAR>r : α<VAR>hr : (scalar n) r = M<GOAL>r • stdBasisMatrix i j 1 = MulOpposite.op r • stdBasisMatrix i j 1
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>(x * y).num ∣ x.num * y.num
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>∃ q, q ≠ 0 ∧ x * y = (algebraMap K[X] (RatFunc K)) (x.num * y.num) / (algebraMap K[X] (RatFunc K)) q
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>x * y = (algebraMap K[X] (RatFunc K)) (x.num * y.num) / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<GOAL>f (x, y) ≤ f (x, t) + f (t, y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<GOAL>f (x, t) ≤ f (x, z) + f (z, t)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<GOAL>f (x, z) + f (z, t) + f (t, y) - f (z, t) = f (x, z) + f (t, y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<GOAL>f (x, z) + f (t, y) ≤ ↑(GromovHausdorff.maxVar X Y) * dist x z + ↑(GromovHausdorff.maxVar X Y) * dist t y
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<GOAL>↑(GromovHausdorff.maxVar X Y) * max (dist x z) (dist t y) + ↑(GromovHausdorff.maxVar X Y) * max (dist x z) (dist t y) = 2 * ↑(GromovHausdorff.maxVar X Y) * max (dist x z) (dist y t)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<GOAL>↑(GromovHausdorff.maxVar X Y) * max (dist x z) (dist y t) + ↑(GromovHausdorff.maxVar X Y) * max (dist x z) (dist y t) = 2 * ↑(GromovHausdorff.maxVar X Y) * max (dist x z) (dist y t)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<GOAL>LinearMap.range (ι Q) ≤ evenOdd Q 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<GOAL>LinearMap.range (ι Q) ≤ LinearMap.range (ι Q) ^ ↑⟨1, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<GOAL>(N.comap f).Basis' I X ↔ N.Basis' (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>I X : Set α<GOAL>N.Basis (f '' I) (f '' X ∩ N.E) → InjOn f I → I ⊆ X → I ⊆ f ⁻¹' N.E
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>x✝ : Substring<VAR>h : x✝.Valid<VAR>e : x✝.toString.data = m₁ ++ c :: m₂<GOAL>x✝.prev { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ }
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>e : x✝.toString.data = m₁ ++ c :: m₂<VAR>l m r : List Char<VAR>h : ValidFor l m r x✝<GOAL>x✝.prev { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ }
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>l m r : List Char<VAR>h : ValidFor l m r x✝<VAR>e : m = m₁ ++ c :: m₂<GOAL>x✝.prev { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ }
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>l r : List Char<VAR>h : ValidFor l (m₁ ++ c :: m₂) r x✝<GOAL>x✝.prev { byteIdx := utf8Len m₁ + c.utf8Size } = { byteIdx := utf8Len m₁ }
<VAR>a✝ b✝ c✝ d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b c : ℕ<GOAL>(a * b + c) % b = c % b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u✝ : Set α<VAR>inst✝² : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0<VAR>g : α → ℝ≥0<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : Tendsto f u (𝓝 g)<GOAL>Measurable g