ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f✝ : α → β<VAR>f : α → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<GOAL>∃ g, LipschitzWith K g ∧ EqOn f g s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f✝ : α → β<VAR>f : α → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<VAR>g : α → ℝ := fun y => ⨅ x, f ↑x + ↑K * dist y ↑x<GOAL>∃ g, LipschitzWith K g ∧ EqOn f g s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f✝ : α → β<VAR>f : α → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<VAR>g : α → ℝ := fun y => ⨅ x, f ↑x + ↑K * dist y ↑x<VAR>B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)<GOAL>∃ g, LipschitzWith K g ∧ EqOn f g s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f✝ : α → β<VAR>f : α → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<VAR>g : α → ℝ := fun y => ⨅ x, f ↑x + ↑K * dist y ↑x<VAR>B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)<VAR>E : EqOn f g s<GOAL>∃ g, LipschitzWith K g ∧ EqOn f g s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f✝ : α → β<VAR>f : α → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<VAR>g : α → ℝ := fun y => ⨅ x, f ↑x + ↑K * dist y ↑x<VAR>B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)<VAR>E : EqOn f g s<VAR>x y : α<GOAL>g x ≤ g y + ↑K * dist x y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f✝ : α → β<VAR>f : α → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<VAR>g : α → ℝ := fun y => ⨅ x, f ↑x + ↑K * dist y ↑x<VAR>B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)<VAR>E : EqOn f g s<VAR>x y : α<GOAL>g x - ↑K * dist x y ≤ g y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f✝ : α → β<VAR>f : α → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<VAR>g : α → ℝ := fun y => ⨅ x, f ↑x + ↑K * dist y ↑x<VAR>B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)<VAR>E : EqOn f g s<VAR>x y : α<VAR>z : ↑s<GOAL>g x - ↑K * dist x y ≤ f ↑z + ↑K * dist y ↑z
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f✝ : α → β<VAR>f : α → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<VAR>g : α → ℝ := fun y => ⨅ x, f ↑x + ↑K * dist y ↑x<VAR>B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)<VAR>E : EqOn f g s<VAR>x y : α<VAR>z : ↑s<GOAL>g x ≤ f ↑z + ↑K * dist y ↑z + ↑K * dist x y
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>n d : F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hd : d ≠ 0<GOAL>W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (n / (P z * Q z * d)) = (n * (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 - Q x * P z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2) + P y * Q z ^ 3 * d ^ 3) / (P z * Q z * d) ^ 3
<VAR>x n : ℂ<GOAL>(starRingEnd ℂ) x ^ n = if x.arg = π then x ^ n else (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)
<VAR>x n : ℂ<GOAL>(if x = 0 then if n = 0 then 1 else 0 else cexp ((if x.arg = π then log x else (starRingEnd ℂ) (log x)) * n)) = if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n) else if x = 0 then if n = 0 then 1 else 0 else cexp ((starRingEnd ℂ) (log x) * n)
<GOAL>Primrec' fun v => v.head - v.tail.head
<VAR>this : Primrec' fun v => (fun a b => b - a) v.head v.tail.head<GOAL>Primrec' fun v => v.head - v.tail.head
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace Y<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s✝ : Set X<VAR>inst✝⁴ : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : SecondCountableTopologyEither X R<VAR>f g : X → R<VAR>s : Set X<VAR>hf : LocallyIntegrableOn f s μ<VAR>hg : ContinuousOn g s<VAR>hs : IsOpen s<GOAL>LocallyIntegrableOn (fun x => g x * f x) s μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝¹⁰ : MeasurableSpace X<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : MeasurableSpace Y<VAR>inst✝⁷ : TopologicalSpace Y<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>f✝ g✝ : X → E<VAR>μ : Measure X<VAR>s✝ : Set X<VAR>inst✝⁴ : OpensMeasurableSpace X<VAR>A K : Set X<VAR>inst✝³ : LocallyCompactSpace X<VAR>inst✝² : T2Space X<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : SecondCountableTopologyEither X R<VAR>f g : X → R<VAR>s : Set X<VAR>hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ<VAR>hg : ContinuousOn g s<VAR>hs : IsOpen s<GOAL>∀ k ⊆ s, IsCompact k → IntegrableOn (fun x => g x * f x) k μ
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : StrictOrderedSemiring Γ<VAR>σ : Type u_3<VAR>inst✝ : Finite σ<VAR>f g : HahnSeries (σ →₀ ℕ) R<VAR>n : σ →₀ ℕ<GOAL>(MvPowerSeries.coeff R n) ({ toFun := fun f => f.coeff, invFun := fun f => { coeff := f, isPWO_support' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun (f * g)) = (MvPowerSeries.coeff R n) ({ toFun := fun f => f.coeff, invFun := fun f => { coeff := f, isPWO_support' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun f * { toFun := fun f => f.coeff, invFun := fun f => { coeff := f, isPWO_support' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun g)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : StrictOrderedSemiring Γ<VAR>σ : Type u_3<VAR>inst✝ : Finite σ<VAR>f g : HahnSeries (σ →₀ ℕ) R<VAR>n : σ →₀ ℕ<GOAL>(MvPowerSeries.coeff R n) (f * g).coeff = ∑ p ∈ antidiagonal n, (MvPowerSeries.coeff R p.1) f.coeff * (MvPowerSeries.coeff R p.2) g.coeff
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>n : σ<VAR>f : MvPolynomial σ R<VAR>d : ℕ<GOAL>degreeOf n f ≤ d ↔ ∀ m ∈ f.support, m n ≤ d
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>x y : 𝕎 R<GOAL>(x + y).coeff 0 = x.coeff 0 + y.coeff 0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α✝<VAR>ι✝ : Type u_5<VAR>π : ι✝ → Type u_6<VAR>inst✝¹ : (i : ι✝) → TopologicalSpace (π i)<VAR>ι : Type u_7<VAR>α : ι → Type u_8<VAR>inst✝ : (i : ι) → TopologicalSpace (α i)<VAR>s : (i : ι) → Set (α i)<VAR>I : Set ι<VAR>hs : ∀ i ∈ I, Dense (s i)<GOAL>Dense (I.pi s)
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(cos ↑x).im = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>I J : Finset ι<VAR>hP : IsProjectiveMeasureFamily P<VAR>S : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>T : Set ((i : { x // x ∈ J }) → α ↑i)<VAR>hT : MeasurableSet T<VAR>h_eq : cylinder I S = cylinder J T<VAR>hJI : J ⊆ I<GOAL>(P I) S = (P J) T
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : β → F (α ::: (Cofix F α ⊕ β))<VAR>x : β<GOAL>(corec' g x).dest = (TypeVec.id ::: Sum.elim _root_.id (corec' g)) <$$> g x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : β → F (α ::: (Cofix F α ⊕ β))<VAR>x : β<GOAL>(TypeVec.id ::: corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g)) <$$> Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g (Sum.inr x) = (TypeVec.id ::: Sum.elim _root_.id (corec' g)) <$$> g x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : β → F (α ::: (Cofix F α ⊕ β))<VAR>x : β<GOAL>corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) = Sum.elim _root_.id (corec' g)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : β → F (α ::: (Cofix F α ⊕ β))<VAR>x : β<VAR>i : Cofix F α<GOAL>corec (MvFunctor.map (TypeVec.id ::: fun x => x) ∘ Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val) (Sum.inl i) = i
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : β → F (α ::: (Cofix F α ⊕ β))<VAR>x i : β<GOAL>corec (MvFunctor.map (TypeVec.id ::: fun x => x) ∘ Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val) (Sum.inr i) = corec (Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g) (Sum.inr i)
<VAR>x y : ℝ<VAR>h : x * y < 1<GOAL>arctan x + arctan y = arctan ((x + y) / (1 - x * y))
<VAR>x y : ℝ<VAR>h : x * y < 1<GOAL>arctan (tan (arctan x + arctan y)) = arctan ((x + y) / (1 - x * y))
<VAR>x y : ℝ<VAR>h : x * y < 1<GOAL>-(π / 2) < arctan x + arctan y
<VAR>x y : ℝ<VAR>h : x * y < 1<GOAL>arctan x + arctan y < π / 2
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝¹¹ : Fintype m<VAR>inst✝¹⁰ : DecidableEq m<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : DecidableEq n<VAR>inst✝⁷ : (i : m) → Fintype (n' i)<VAR>inst✝⁶ : (i : m) → DecidableEq (n' i)<VAR>inst✝⁵ : Field 𝕂<VAR>inst✝⁴ : Ring 𝔸<VAR>inst✝³ : TopologicalSpace 𝔸<VAR>inst✝² : TopologicalRing 𝔸<VAR>inst✝¹ : Algebra 𝕂 𝔸<VAR>inst✝ : T2Space 𝔸<VAR>v : (i : m) → Matrix (n' i) (n' i) 𝔸<GOAL>exp 𝕂 (blockDiagonal' v) = blockDiagonal' (exp 𝕂 v)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<GOAL>∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>s_count : s.Countable<VAR>s_dense : Dense s<GOAL>∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>hs : sphere 0 1 ⊆ closure s<GOAL>∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>hs : sphere 0 1 ⊆ closure s<GOAL>∀ (a : E), (∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) a v) → DifferentiableAt ℝ f a
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>s_count : s.Countable<VAR>s_dense : Dense s<VAR>hs : sphere 0 1 ⊆ closure s<VAR>x : E<VAR>L : E →L[ℝ] ℝ<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<GOAL>DifferentiableAt ℝ f x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s✝ : Finset α<VAR>inst✝ : DecidableEq α<VAR>s : Finset ι<VAR>f : ι → Finset α<VAR>a : α<GOAL>a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i
<VAR>x : ℝ≥0∞<VAR>n : ℕ<VAR>z : ℝ<GOAL>x ^ (↑n * z) = (x ^ n) ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν'✝ ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>h1 : μ ≪ ν<VAR>ν' : Measure α<VAR>s : Set α<VAR>hs : (ν + ν') s = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν'✝ ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>h1 : μ ≪ ν<VAR>ν' : Measure α<VAR>s : Set α<VAR>hs : ν s = 0 ∧ ν' s = 0<GOAL>μ s = 0
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>a / b ≤ a⁻¹ * b ↔ a ≤ b
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>a * a ≤ b * b ↔ a ≤ b
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>hsum : Summable fun x => ‖f x‖<GOAL>HasProd (fun p => (1 - f ↑p)⁻¹) (∑' (n : ℕ), f n)
<VAR>F : Type u_1<VAR>inst✝¹ : NormedField F<VAR>inst✝ : CompleteSpace F<VAR>f : ℕ →*₀ F<VAR>hsum : Summable fun x => ‖f x‖<VAR>H : (fun p => (1 - f ↑p)⁻¹) = fun p => ∑' (e : ℕ), f (↑p ^ e)<GOAL>HasProd (fun p => (1 - f ↑p)⁻¹) (∑' (n : ℕ), f n)
<VAR>R✝ : Type u<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Semiring A<VAR>f : R →+* A<VAR>H : Function.Injective ⇑f<VAR>p : ℕ<VAR>inst✝ : ExpChar A p<GOAL>ExpChar R p
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ ν ν₁ ν₂ μ : Measure α<GOAL>μ ⟂ₘ μ ↔ μ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ ν ν₁ ν₂ μ : Measure α<GOAL>μ ⟂ₘ μ → μ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ ν ν₁ ν₂ μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s = 0<VAR>hμs_compl : μ sᶜ = 0<GOAL>μ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ ν ν₁ ν₂ μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s = 0<VAR>hμs_compl : μ sᶜ = 0<GOAL>μ univ = 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>W X X' Y Y' Z : C<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ Y'<VAR>h' : Y' ⟶ Z<GOAL>f ≫ g ≫ h ≫ e.unit.app Z = f' ≫ g' ≫ h' ≫ e.unit.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.45519, u_1} C<VAR>inst✝³ : Category.{?u.45523, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>inst✝ : HasZeroObject C<VAR>cc : CokernelCofork S.f<VAR>hcc : IsColimit cc<GOAL>Mono ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.45519, u_1} C<VAR>inst✝³ : Category.{?u.45523, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>inst✝ : HasZeroObject C<VAR>cc : CokernelCofork S.f<VAR>hcc : IsColimit cc<VAR>this : S.HasHomology<GOAL>Mono ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.45519, u_1} C<VAR>inst✝³ : Category.{?u.45523, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>inst✝ : HasZeroObject C<VAR>cc : CokernelCofork S.f<VAR>hcc : IsColimit cc<VAR>this : S.HasHomology<GOAL>Arrow.mk ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) ≅ Arrow.mk S.fromOpcycles
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.45519, u_1} C<VAR>inst✝³ : Category.{?u.45523, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>inst✝ : HasZeroObject C<VAR>cc : CokernelCofork S.f<VAR>hcc : IsColimit cc<VAR>this : S.HasHomology<GOAL>(hcc.coconePointUniqueUpToIso S.opcyclesIsCokernel).hom ≫ (Arrow.mk S.fromOpcycles).hom = (Arrow.mk ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).hom ≫ (Iso.refl (Arrow.mk ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).right).hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.45519, u_1} C<VAR>inst✝³ : Category.{?u.45523, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>inst✝ : HasZeroObject C<VAR>cc : CokernelCofork S.f<VAR>hcc : IsColimit cc<VAR>this : S.HasHomology<GOAL>Cofork.π cc ≫ (hcc.coconePointUniqueUpToIso S.opcyclesIsCokernel).hom ≫ (Arrow.mk S.fromOpcycles).hom = Cofork.π cc ≫ (Arrow.mk ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).hom ≫ (Iso.refl (Arrow.mk ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).right).hom
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<GOAL>totalDegree 0 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<GOAL>(C 0).totalDegree = 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a b c : α<GOAL>|a| < |b| ↔ a * a < b * b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a b c : α<GOAL>|a| < |b| ↔ |a| * |a| < |b| * |b|
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<GOAL>cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<GOAL>cosh x * cosh (2 * x) + sinh x * sinh (2 * x) = 4 * cosh x ^ 3 - 3 * cosh x
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<GOAL>cosh x * (cosh x ^ 2 + sinh x ^ 2) + sinh x * (2 * sinh x * cosh x) = 4 * cosh x ^ 3 - 3 * cosh x
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<VAR>h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2<GOAL>cosh x * (cosh x ^ 2 + sinh x ^ 2) + sinh x * (2 * sinh x * cosh x) = 4 * cosh x ^ 3 - 3 * cosh x
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<VAR>h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2<GOAL>cosh x * (cosh x ^ 2 + (cosh x ^ 2 - 1)) + 2 * cosh x * (cosh x ^ 2 - 1) = 4 * cosh x ^ 3 - 3 * cosh x
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>e : K ≌ J<VAR>s : Cocone (e.functor ⋙ F)<VAR>k : K<GOAL>(((whiskering e.inverse ⋙ precompose (F.leftUnitor.inv ≫ whiskerRight e.counitIso.inv F ≫ (e.inverse.associator e.functor F).inv)) ⋙ whiskering e.functor).obj s).ι.app k ≫ (Iso.refl (((whiskering e.inverse ⋙ precompose (F.leftUnitor.inv ≫ whiskerRight e.counitIso.inv F ≫ (e.inverse.associator e.functor F).inv)) ⋙ whiskering e.functor).obj s).pt).hom = ((𝟭 (Cocone (e.functor ⋙ F))).obj s).ι.app k
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>h : edist x y = 0<GOAL>edist z x = edist z y
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>h : edist x y = 0<GOAL>edist x z = edist y z
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Cardinal.univ.{u, v} ≤ univ.{u, v}.cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Cardinal.{max (u + 1) v}<VAR>h : c < Cardinal.univ.{u, v}<GOAL>c < univ.{u, v}.cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Cardinal.{u}<VAR>h : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}<GOAL>Cardinal.lift.{max (u + 1) v, u} c < univ.{u, v}.cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Cardinal.{u}<VAR>h : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}<VAR>S : Set Ordinal.{u}<VAR>H : Unbounded (fun x x_1 => x < x_1) S<VAR>Se : #↑S = (type fun x x_1 => x < x_1).cof<GOAL>Cardinal.lift.{max (u + 1) v, u} c < univ.{u, v}.cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Cardinal.{u}<VAR>h : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}<VAR>S : Set Ordinal.{u}<VAR>H : Unbounded (fun x x_1 => x < x_1) S<VAR>Se : #↑S = (type fun x x_1 => x < x_1).cof<GOAL>Cardinal.lift.{u + 1, u} c < #↑S
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Cardinal.{u}<VAR>h✝ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}<VAR>S : Set Ordinal.{u}<VAR>H : Unbounded (fun x x_1 => x < x_1) S<VAR>Se : #↑S = (type fun x x_1 => x < x_1).cof<VAR>h : Cardinal.lift.{u + 1, u} c ≥ #↑S<GOAL>False
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Cardinal.{u}<VAR>h✝ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}<VAR>S : Set Ordinal.{u}<VAR>H : Unbounded (fun x x_1 => x < x_1) S<VAR>Se : #↑S = (type fun x x_1 => x < x_1).cof<VAR>h : Cardinal.lift.{u + 1, u} c ≥ #↑S<VAR>a : Cardinal.{u}<VAR>e : Cardinal.lift.{u + 1, u} a = #↑S<GOAL>False
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h✝ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}<VAR>S : Set Ordinal.{u}<VAR>H : Unbounded (fun x x_1 => x < x_1) S<VAR>Se : #↑S = (type fun x x_1 => x < x_1).cof<VAR>h : Cardinal.lift.{u + 1, u} c ≥ #↑S<VAR>a : Cardinal.{u}<VAR>e✝ : Cardinal.lift.{u + 1, u} a = #↑S<VAR>α : Type u<VAR>e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S<GOAL>False
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h✝ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}<VAR>S : Set Ordinal.{u}<VAR>H : Unbounded (fun x x_1 => x < x_1) S<VAR>Se : #↑S = (type fun x x_1 => x < x_1).cof<VAR>h : Cardinal.lift.{u + 1, u} c ≥ #↑S<VAR>a : Cardinal.{u}<VAR>e✝ : Cardinal.lift.{u + 1, u} a = #↑S<VAR>α : Type u<VAR>e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S<VAR>f : ULift.{u + 1, u} α ≃ ↑S<GOAL>False
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h✝¹ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}<VAR>S : Set Ordinal.{u}<VAR>H : Unbounded (fun x x_1 => x < x_1) S<VAR>Se : #↑S = (type fun x x_1 => x < x_1).cof<VAR>h✝ : Cardinal.lift.{u + 1, u} c ≥ #↑S<VAR>a : Cardinal.{u}<VAR>e✝ : Cardinal.lift.{u + 1, u} a = #↑S<VAR>α : Type u<VAR>e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S<VAR>f✝ : ULift.{u + 1, u} α ≃ ↑S<VAR>f : α ≃ ↑S<VAR>g : α → Ordinal.{u} := fun a => ↑(f a)<VAR>o : Ordinal.{u} := succ (sup g)<VAR>b : Ordinal.{u}<VAR>h : b ∈ S<VAR>l : ¬(fun x x_1 => x < x_1) b o<GOAL>False
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h✝¹ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}<VAR>S : Set Ordinal.{u}<VAR>H : Unbounded (fun x x_1 => x < x_1) S<VAR>Se : #↑S = (type fun x x_1 => x < x_1).cof<VAR>h✝ : Cardinal.lift.{u + 1, u} c ≥ #↑S<VAR>a : Cardinal.{u}<VAR>e✝ : Cardinal.lift.{u + 1, u} a = #↑S<VAR>α : Type u<VAR>e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S<VAR>f✝ : ULift.{u + 1, u} α ≃ ↑S<VAR>f : α ≃ ↑S<VAR>g : α → Ordinal.{u} := fun a => ↑(f a)<VAR>o : Ordinal.{u} := succ (sup g)<VAR>b : Ordinal.{u}<VAR>h : b ∈ S<VAR>l : ¬(fun x x_1 => x < x_1) b o<GOAL>b ≤ sup g