ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>x y : R<GOAL>{ toFun := fun x => op (star x), invFun := __src✝.invFun, left_inv := ⋯, right_inv := ⋯ }.toFun (x * y) = { toFun := fun x => op (star x), invFun := __src✝.invFun, left_inv := ⋯, right_inv := ⋯ }.toFun x * { toFun := fun x => op (star x), invFun := __src✝.invFun, left_inv := ⋯, right_inv := ⋯ }.toFun y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f g : Filter α<VAR>inst✝ : Preorder β<VAR>l : Filter α<VAR>u v : α → β<VAR>hu : IsBoundedUnder (fun x x_1 => x ≤ x_1) l u<VAR>hv : v ≤ᶠ[l] u<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) l v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f g : Filter α<VAR>inst✝ : Preorder β<VAR>l : Filter α<VAR>u v : α → β<VAR>hu : IsBoundedUnder (fun x x_1 => x ≤ x_1) l u<VAR>hv : v ≤ᶠ[l] u<GOAL>∀ (a : β), (∀ᶠ (x : β) in map u l, (fun x x_1 => x ≤ x_1) x a) → ∀ᶠ (x : β) in map v l, (fun x x_1 => x ≤ x_1) x a
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p 0)) ⊆ (divisors 0).erase 1
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : n ≠ 0<GOAL>Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : n ≠ 0<VAR>t : ℕ<VAR>ht : t ∈ Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n))<GOAL>t ∈ n.divisors.erase 1
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : n ≠ 0<VAR>t : ℕ<VAR>ht : ∃ a < padicValNat p n, p ^ (a + 1) = t<GOAL>t ∈ n.divisors.erase 1
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : n ≠ 0<VAR>k : ℕ<VAR>hk : k < padicValNat p n<GOAL>p ^ (k + 1) ∈ n.divisors.erase 1
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : n ≠ 0<VAR>k : ℕ<VAR>hk : k < padicValNat p n<GOAL>p ^ (k + 1) ≠ 1 ∧ p ^ (k + 1) ∣ n ∧ n ≠ 0
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : n ≠ 0<VAR>k : ℕ<VAR>hk : k < padicValNat p n<GOAL>p ^ (k + 1) ≠ 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l✝ : Filter α<VAR>inst✝ : SemilatticeSup β<VAR>l : Filter α<VAR>f g h : α → β<VAR>hf : f ≤ᶠ[l] h<VAR>hg : g ≤ᶠ[l] h<GOAL>f ⊔ g ≤ᶠ[l] h
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>s t : Set α<VAR>x : α<VAR>inst✝ : Bornology β<VAR>f : α → β<GOAL>comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>s✝ t : Set α<VAR>x : α<VAR>inst✝ : Bornology β<VAR>f : α → β<VAR>h : comap f (cobounded β) ≤ cobounded α<VAR>s : Set α<VAR>hs : IsBounded s<GOAL>IsBounded (f '' s)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>s✝ t✝ : Set α<VAR>x : α<VAR>inst✝ : Bornology β<VAR>f : α → β<VAR>h : comap f (cobounded β) ≤ cobounded α<VAR>s : Set α<VAR>hs : IsBounded s<VAR>t : Set β<VAR>ht : t ∈ cobounded β<VAR>hts : f ⁻¹' t ⊆ sᶜ<GOAL>IsBounded (f '' s)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>s✝ t✝ : Set α<VAR>x : α<VAR>inst✝ : Bornology β<VAR>f : α → β<VAR>h : comap f (cobounded β) ≤ cobounded α<VAR>s : Set α<VAR>hs : IsBounded s<VAR>t : Set β<VAR>ht : t ∈ cobounded β<VAR>hts : s ⊆ f ⁻¹' tᶜ<GOAL>IsBounded (f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>s t✝ : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>hy : y ∈ s<VAR>t : 𝕜<VAR>ht₀ : 0 ≤ t<VAR>ht₁ : t ≤ 1<GOAL>x + t • (y - x) ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>s t✝ : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>hy : y ∈ s<VAR>t : 𝕜<VAR>ht₀ : 0 ≤ t<VAR>ht₁ : t ≤ 1<GOAL>x + t • (y - x) ∈ [x-[𝕜]y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>s t✝ : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>hy : y ∈ s<VAR>t : 𝕜<VAR>ht₀ : 0 ≤ t<VAR>ht₁ : t ≤ 1<GOAL>x + t • (y - x) ∈ (fun θ => x + θ • (y - x)) '' Icc 0 1
<VAR>x✝ y x : ℝ<GOAL>√(x * x) = |x|
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h₂ : ∀ (z : ℂ), (f z).re = z.re<VAR>z : ℂ<GOAL>(f z).im = z.im ∨ (f z).im = -z.im
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h₂ : ∀ (z : ℂ), (f z).re = z.re<VAR>z : ℂ<VAR>h₁ : ‖f z‖ = ‖z‖<GOAL>(f z).im = z.im ∨ (f z).im = -z.im
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h₂ : ∀ (z : ℂ), (f z).re = z.re<VAR>z : ℂ<VAR>h₁ : √(normSq (f z)) = √(normSq z)<GOAL>(f z).im = z.im ∨ (f z).im = -z.im
<VAR>α : Type u_1<VAR>inst✝¹ : AddCommGroupWithOne α<VAR>inst✝ : CharZero α<VAR>a b n : ℕ<GOAL>↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [MOD n]
<VAR>x : ℝ<GOAL>-deriv arcsin x = -(1 / √(1 - x ^ 2))
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁✝ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l₁ : List α<VAR>f : α → List β<GOAL>(l₁.bind f).Nodup ↔ (∀ x ∈ l₁, (f x).Nodup) ∧ Pairwise (fun a b => (f a).Disjoint (f b)) l₁
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁✝ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l₁ : List α<VAR>f : α → List β<GOAL>(Pairwise (fun a b => (f a).Disjoint (f b)) l₁ ∧ ∀ (l : List β) (x : α), f x = l → x ∈ l₁ → l.Nodup) ↔ Pairwise (fun a b => (f a).Disjoint (f b)) l₁ ∧ ∀ x ∈ l₁, (f x).Nodup
<VAR>a b p q : ℝ≥0<VAR>h : p.IsConjExponent q<GOAL>p / q = p - 1
<VAR>a b p q : ℝ≥0<VAR>h : p.IsConjExponent q<GOAL>p = (p - 1) * q
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>a b : F<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<GOAL>quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Fintype F<VAR>inst✝ : DecidableEq F<VAR>a b : F<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>hab : a * b ≠ 0<GOAL>quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝ : NormedSpace ℝ F<VAR>L : E →L[𝕜] F<GOAL>Continuous fun φ => ∫ (x : X), L (↑↑φ x) ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝ : NormedSpace ℝ F<VAR>L : E →L[𝕜] F<GOAL>Continuous fun x => ∫ (x_1 : X), ↑↑(L.compLp x) x_1 ∂μ
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁵ : OrderedSemiring 𝕜<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : TopologicalSpace F<VAR>inst✝² : AddCancelCommMonoid E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>z : E<GOAL>StrictConvex 𝕜 ((fun x => x + z) ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>i : ℕ<VAR>h : i < l.enum.length<GOAL>i < l.length
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>f : α → β<VAR>u₁ : UniformSpace α<VAR>u₂ : ι → UniformSpace β<GOAL>Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔ ∀ (i : ι), Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β)
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Fintype ι₁<VAR>inst✝¹ : Finite ι₂<VAR>inst✝ : DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>f g : M₁ →ₗ[R] M₂<GOAL>(fun i => ((toMatrix b₁ b₂) (f + g)).toMvPolynomial i) = (fun i => ((toMatrix b₁ b₂) f).toMvPolynomial i) + fun i => ((toMatrix b₁ b₂) g).toMvPolynomial i
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω = i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>this : {ω | τ ω = i} = {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i}<GOAL>MeasurableSet {ω | τ ω = i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>this : {ω | τ ω = i} = {ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i}<GOAL>MeasurableSet ({ω | τ ω ≤ i} ∩ {ω | τ ω ≥ i})
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>inst✝ : SigmaFinite μ<VAR>f_int : IntegrableOn f s μ<VAR>g_int : IntegrableOn g s μ<VAR>hs : MeasurableSet s<VAR>hfg : f ≤ᶠ[ae (μ.restrict s)] g<GOAL>(μ.prod volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>inst✝ : SigmaFinite μ<VAR>f_int : IntegrableOn f s μ<VAR>g_int : IntegrableOn g s μ<VAR>hs : MeasurableSet s<VAR>hfg : f ≤ᶠ[ae (μ.restrict s)] g<VAR>h : g - f =ᶠ[ae (μ.restrict s)] fun x => ↑(g x - f x).toNNReal<GOAL>(μ.prod volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>inst✝ : SigmaFinite μ<VAR>f_int : IntegrableOn f s μ<VAR>g_int : IntegrableOn g s μ<VAR>hs : MeasurableSet s<VAR>hfg : f ≤ᶠ[ae (μ.restrict s)] g<VAR>h : g - f =ᶠ[ae (μ.restrict s)] fun x => ↑(g x - f x).toNNReal<GOAL>(fun y => ENNReal.ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun a => ↑(g a - f a).toNNReal
<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>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<GOAL>W.negAddY P Q = ((P y * Q z ^ 3 - Q y * P z ^ 3) * (W.addX P Q * (P z * Q z) ^ 2 - P x * Q z ^ 2 * addZ P Q ^ 2) + P y * Q z ^ 3 * addZ P Q ^ 3) / (P z * Q z) ^ 3
<VAR>a✝ b n a : ℤ<VAR>h : 0 ≤ a<GOAL>image (fun x => x % a) (Ico n (n + a)) = Ico 0 a
<VAR>a b n : ℤ<VAR>h : 0 ≤ 0<GOAL>image (fun x => x % 0) (Ico n (n + 0)) = Ico 0 0
<VAR>a✝ b n a : ℤ<VAR>h : 0 ≤ a<VAR>ha : 0 < a<GOAL>image (fun x => x % a) (Ico n (n + a)) = Ico 0 a
<VAR>a✝ b n a : ℤ<VAR>h : 0 ≤ a<VAR>ha : 0 < a<VAR>i : ℤ<GOAL>i ∈ image (fun x => x % a) (Ico n (n + a)) ↔ i ∈ Ico 0 a
<VAR>a✝ b n a : ℤ<VAR>h : 0 ≤ a<VAR>ha : 0 < a<VAR>i : ℤ<GOAL>(∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ 0 ≤ i ∧ i < a
<VAR>a✝ b n a : ℤ<VAR>h : 0 ≤ a<VAR>ha : 0 < a<VAR>i : ℤ<VAR>hia : 0 ≤ i ∧ i < a<GOAL>∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
<VAR>a✝ b n a : ℤ<VAR>h : 0 ≤ a<VAR>ha : 0 < a<VAR>i : ℤ<VAR>hia : 0 ≤ i ∧ i < a<VAR>hn : n % a + a * (n / a) = n<GOAL>∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
<VAR>a✝ b n a : ℤ<VAR>h : 0 ≤ a<VAR>ha : 0 < a<VAR>i : ℤ<VAR>hia : 0 ≤ i ∧ i < a<VAR>hn : n % a + a * (n / a) = n<VAR>hi : i < n % a<GOAL>∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
<VAR>a✝ b n a : ℤ<VAR>h : 0 ≤ a<VAR>ha : 0 < a<VAR>i : ℤ<VAR>hia : 0 ≤ i ∧ i < a<VAR>hn : n % a + a * (n / a) = n<VAR>hi : n % a ≤ i<GOAL>∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β : Type v<VAR>β' : Type u_2<VAR>γ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β<VAR>inst✝³ : OmegaCompletePartialOrder γ<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>c : Chain (α →𝒄 β)<VAR>c' : Chain α<GOAL>(ωSup (c.map toMono)) (ωSup c') = ωSup (c'.map (ωSup (c.map toMono)))
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β : Type v<VAR>β' : Type u_2<VAR>γ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β<VAR>inst✝³ : OmegaCompletePartialOrder γ<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>c : Chain (α →𝒄 β)<VAR>c' : Chain α<GOAL>∀ (c_1 : β), (ωSup (c.map toMono)) (ωSup c') ≤ c_1 ↔ ωSup (c'.map (ωSup (c.map toMono))) ≤ c_1
<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>hom : (i j : ι) → C.X i ⟶ D.X j<VAR>g : D ⟶ E<VAR>n : ι<GOAL>(nullHomotopicMap hom ≫ g).f n = (nullHomotopicMap fun i j => hom i j ≫ g.f j).f n
<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>hom : (i j : ι) → C.X i ⟶ D.X j<VAR>g : D ⟶ E<VAR>n : ι<GOAL>(C.dFrom n ≫ hom (c.next n) n + hom n (c.prev n) ≫ D.dTo n) ≫ g.f n = C.dFrom n ≫ hom (c.next n) n ≫ g.f n + (hom n (c.prev n) ≫ g.f (c.prev n)) ≫ E.dTo n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ts : List α<GOAL>map (map f) ts.permutations = (map f ts).permutations
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>φ : G →* H<GOAL>Subsingleton (Quot Setoid.r)
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>φ : G →* H<GOAL>Subsingleton (Quot fun x y => x⁻¹ * y ∈ ⊤)
<VAR>n : ℕ<VAR>i : Fin (n + 2)<GOAL>δ i ≫ δ i.castSucc = δ i ≫ δ i.succ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NonUnitalNormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>x : E<GOAL>‖x * x⋆‖ = ‖x‖ * ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NonUnitalNormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>x : E<GOAL>‖x⋆⋆ * x⋆‖ = ‖x‖ * ‖x‖
<VAR>M₀ : Type u_1<VAR>inst✝⁸ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁷ : MonoidWithZero M<VAR>inst✝⁶ : MonoidWithZero M'<VAR>inst✝⁵ : CommMonoidWithZero M₁<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : CommRing R'<VAR>inst✝² : FunLike F M M'<VAR>inst✝¹ : NoZeroDivisors M'<VAR>inst✝ : MonoidWithZeroHomClass F M M'<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S : Submonoid M<VAR>hS : S ≤ M⁰<GOAL>Submonoid.map f S ≤ M'⁰
<VAR>M₀ : Type u_1<VAR>inst✝⁸ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁷ : MonoidWithZero M<VAR>inst✝⁶ : MonoidWithZero M'<VAR>inst✝⁵ : CommMonoidWithZero M₁<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : CommRing R'<VAR>inst✝² : FunLike F M M'<VAR>inst✝¹ : NoZeroDivisors M'<VAR>inst✝ : MonoidWithZeroHomClass F M M'<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S : Submonoid M<VAR>hS : S ≤ M⁰<VAR>h✝ : Subsingleton M<GOAL>Submonoid.map f S ≤ M'⁰
<VAR>M₀ : Type u_1<VAR>inst✝⁸ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁷ : MonoidWithZero M<VAR>inst✝⁶ : MonoidWithZero M'<VAR>inst✝⁵ : CommMonoidWithZero M₁<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : CommRing R'<VAR>inst✝² : FunLike F M M'<VAR>inst✝¹ : NoZeroDivisors M'<VAR>inst✝ : MonoidWithZeroHomClass F M M'<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S : Submonoid M<VAR>hS : S ≤ M⁰<VAR>h✝ : Nontrivial M<GOAL>Submonoid.map f S ≤ M'⁰
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<GOAL>(rightShiftAddEquiv K L n a n' hn') 0 = 0
<VAR>C : Type u<VAR>inst✝¹⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹⁷ : Category.{?u.73757, u_1} A<VAR>inst✝¹⁶ : Category.{?u.73761, u_2} B<VAR>F✝ : A ⥤ B<VAR>D : Type u_3<VAR>E : Type u_4<VAR>inst✝¹⁵ : Category.{max v u, u_3} D<VAR>inst✝¹⁴ : Category.{max v u, u_4} E<VAR>F : D ⥤ E<VAR>inst✝¹³ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝¹² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝¹¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝⁹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝⁸ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>inst✝⁷ : ConcreteCategory D<VAR>inst✝⁶ : ConcreteCategory E<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝⁴ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : PreservesLimits (forget E)<VAR>inst✝¹ : (forget D).ReflectsIsomorphisms<VAR>inst✝ : (forget E).ReflectsIsomorphisms<VAR>P : Cᵒᵖ ⥤ D<GOAL>(sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P = { val := (J.sheafifyCompIso F P).inv }
<VAR>C : Type u<VAR>inst✝¹⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹⁷ : Category.{?u.73757, u_1} A<VAR>inst✝¹⁶ : Category.{?u.73761, u_2} B<VAR>F✝ : A ⥤ B<VAR>D : Type u_3<VAR>E : Type u_4<VAR>inst✝¹⁵ : Category.{max v u, u_3} D<VAR>inst✝¹⁴ : Category.{max v u, u_4} E<VAR>F : D ⥤ E<VAR>inst✝¹³ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝¹² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝¹¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝⁹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝⁸ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>inst✝⁷ : ConcreteCategory D<VAR>inst✝⁶ : ConcreteCategory E<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝⁴ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : PreservesLimits (forget E)<VAR>inst✝¹ : (forget D).ReflectsIsomorphisms<VAR>inst✝ : (forget E).ReflectsIsomorphisms<VAR>P : Cᵒᵖ ⥤ D<GOAL>((plusPlusAdjunction J E).homEquiv (((whiskeringRight Cᵒᵖ D E).obj F).obj P) ((plusPlusSheaf J D ⋙ sheafCompose J F).obj P)) ((sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P) = ((plusPlusAdjunction J E).homEquiv (((whiskeringRight Cᵒᵖ D E).obj F).obj P) ((plusPlusSheaf J D ⋙ sheafCompose J F).obj P)) { val := (J.sheafifyCompIso F P).inv }
<VAR>C : Type u<VAR>inst✝¹⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹⁷ : Category.{?u.73757, u_1} A<VAR>inst✝¹⁶ : Category.{?u.73761, u_2} B<VAR>F✝ : A ⥤ B<VAR>D : Type u_3<VAR>E : Type u_4<VAR>inst✝¹⁵ : Category.{max v u, u_3} D<VAR>inst✝¹⁴ : Category.{max v u, u_4} E<VAR>F : D ⥤ E<VAR>inst✝¹³ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝¹² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝¹¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝⁹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝⁸ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>inst✝⁷ : ConcreteCategory D<VAR>inst✝⁶ : ConcreteCategory E<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝⁴ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : PreservesLimits (forget E)<VAR>inst✝¹ : (forget D).ReflectsIsomorphisms<VAR>inst✝ : (forget E).ReflectsIsomorphisms<VAR>P : Cᵒᵖ ⥤ D<VAR>e_1✝ : (((whiskeringRight Cᵒᵖ D E).obj F).obj P ⟶ (sheafToPresheaf J E).obj ((plusPlusSheaf J D ⋙ sheafCompose J F).obj P)) = ((𝟭 (Cᵒᵖ ⥤ E)).obj (P ⋙ F) ⟶ (sheafToPresheaf J E).obj ((plusPlusSheaf J D ⋙ sheafCompose J F).obj P))<GOAL>((plusPlusAdjunction J E).homEquiv (((whiskeringRight Cᵒᵖ D E).obj F).obj P) ((plusPlusSheaf J D ⋙ sheafCompose J F).obj P)) ((sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P) = (plusPlusAdjunction J E).unit.app (P ⋙ F) ≫ (sheafToPresheaf J E).map ((sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P)
<VAR>C : Type u<VAR>inst✝¹⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹⁷ : Category.{?u.73757, u_1} A<VAR>inst✝¹⁶ : Category.{?u.73761, u_2} B<VAR>F✝ : A ⥤ B<VAR>D : Type u_3<VAR>E : Type u_4<VAR>inst✝¹⁵ : Category.{max v u, u_3} D<VAR>inst✝¹⁴ : Category.{max v u, u_4} E<VAR>F : D ⥤ E<VAR>inst✝¹³ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝¹² : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝¹¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝⁹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝⁸ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>inst✝⁷ : ConcreteCategory D<VAR>inst✝⁶ : ConcreteCategory E<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝⁴ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : PreservesLimits (forget E)<VAR>inst✝¹ : (forget D).ReflectsIsomorphisms<VAR>inst✝ : (forget E).ReflectsIsomorphisms<VAR>P : Cᵒᵖ ⥤ D<VAR>e_1✝ : (((whiskeringRight Cᵒᵖ D E).obj F).obj P ⟶ (sheafToPresheaf J E).obj ((plusPlusSheaf J D ⋙ sheafCompose J F).obj P)) = ((𝟭 (Cᵒᵖ ⥤ E)).obj (P ⋙ F) ⟶ (sheafToPresheaf J E).obj ((plusPlusSheaf J D ⋙ sheafCompose J F).obj P))<GOAL>((plusPlusAdjunction J E).homEquiv (((whiskeringRight Cᵒᵖ D E).obj F).obj P) ((plusPlusSheaf J D ⋙ sheafCompose J F).obj P)) { val := (J.sheafifyCompIso F P).inv } = whiskerRight ((plusPlusAdjunction J D).unit.app P) F
<VAR>x : ℝ<VAR>hx : -(π / 2) ≤ x<VAR>hx₀ : x ≤ 0<GOAL>sin x ≤ 2 / π * x
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>n : ℕ<VAR>u : ℕ → α<VAR>hu : MonotoneOn u (Iic n)<VAR>us : ∀ i ≤ n, u i ∈ s<GOAL>∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
<VAR>𝕂 : Type u_1<VAR>inst✝⁵ : RCLike 𝕂<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕂 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕂 F<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕂] F<VAR>a : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕂 n f a<VAR>hf' : HasFDerivAt f (↑f') a<VAR>hn : 1 ≤ n<GOAL>ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)
<VAR>𝕂 : Type u_1<VAR>inst✝⁵ : RCLike 𝕂<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕂 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕂 F<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕂] F<VAR>a : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕂 n f a<VAR>hf' : HasFDerivAt f (↑f') a<VAR>hn : 1 ≤ n<VAR>this : hf.localInverse hf' hn (f a) = a<GOAL>ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)