ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x : ℝ<VAR>h1 : 0 ≤ x<VAR>h2 : x ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h3 : |x| = x<VAR>h4 : |x| ≤ 1<VAR>h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))<GOAL>rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)
<VAR>x : ℝ<VAR>h1 : 0 ≤ x<VAR>h2 : x ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h3 : |x| = x<VAR>h4 : |x| ≤ 1<VAR>h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))<GOAL>rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)
<VAR>x : ℝ<VAR>h1 : 0 ≤ x<VAR>h2 : x ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h3 : |x| = x<VAR>h4 : |x| ≤ 1<VAR>h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))<VAR>h'' : rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))<GOAL>rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)
<VAR>x : ℝ<VAR>h1 : 0 ≤ x<VAR>h2 : x ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h3 : |x| = x<VAR>h4 : |x| ≤ 1<VAR>h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))<VAR>h'' : rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))<VAR>t : rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n.succ / (↑n.factorial * ↑n))<GOAL>rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>hdeg : 1 < f.natDegree<GOAL>h.coeff h.root = Pi.single 1 1
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>μ : Measure G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>g : G<GOAL>MeasurePreserving (fun x => x / g) μ μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>a : α<GOAL>(pure a).IsCountablyGenerated
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>a : α<GOAL>(𝓟 {a}).IsCountablyGenerated
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : Nonempty γ<VAR>ι : Sort u_4<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iInf g)<VAR>Af : Antitone f<VAR>bdd : autoParam (BddBelow (range g)) _auto✝<GOAL>f (⨅ i, g i) = ⨆ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : Nonempty γ<VAR>ι : Sort u_4<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iInf g)<VAR>Af : Antitone f<VAR>bdd : autoParam (BddBelow (range g)) _auto✝<GOAL>sSup (range (f ∘ g)) = sSup (range fun i => f (g i))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>hI : a₂ ≤ b₂<VAR>ha : a₂ ≤ a₁<VAR>hb : b₁ < b₂<GOAL>Icc a₁ b₁ ⊂ Icc a₂ b₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>hI : a₂ ≤ b₂<VAR>ha : a₂ ≤ a₁<VAR>hb : b₁ < b₂<GOAL>Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedRing A<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : IntervalIntegrable f volume a b<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => f (x * c)) volume (a / c) (b / c)
<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>f : Filter β<VAR>u : β → α<VAR>b : α<VAR>hb : b ∈ upperBounds (range u)<GOAL>∀ (x : β), u x ≤ b
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>hH : H.relindex L ≠ 0<VAR>hK : K.relindex L ≠ 0<GOAL>(H ⊓ K).relindex L ≠ 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>hK : K.relindex L ≠ 0<VAR>hH : H.relindex (K ⊓ L) ≠ 0<GOAL>(H ⊓ K).relindex L ≠ 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>hK : (K ⊓ L).relindex L ≠ 0<VAR>hH : (H ⊓ (K ⊓ L)).relindex (K ⊓ L) ≠ 0<GOAL>(H ⊓ K ⊓ L).relindex L ≠ 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>hK : (K ⊓ L).relindex L ≠ 0<VAR>hH : (H ⊓ (K ⊓ L)).relindex (K ⊓ L) ≠ 0<GOAL>(H ⊓ (K ⊓ L)).relindex L ≠ 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i✝ j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>i : ι<VAR>hit : i ∈ t<VAR>hit' : i ∉ filter (fun i => w i ≠ 0) t<GOAL>w i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set β<VAR>h : f '' (f ⁻¹' s) = s<GOAL>f '' (f ⁻¹' s) ⊆ range f
<VAR>K : Type uK<VAR>V : Type uV<VAR>inst✝³ : CommRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Free K V<VAR>v : V<GOAL>(eval K V) v = 0 ↔ v = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>Fintype.card (ZMod p)ˣ = p - 1
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>z : N<VAR>w v : P<GOAL>(f.lift hg) z * w = v ↔ g (f.sec z).1 * w = g ↑(f.sec z).2 * v
<GOAL>Tendsto tan (𝓝[>] (-(π / 2))) atBot
<VAR>ι : Sort u_1<VAR>a b : ℝ<VAR>h : a ≤ b<VAR>c : ι → Set ↑(Icc a b)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<GOAL>∃ t, ↑(t 0) = a ∧ Monotone t ∧ (∃ m, ∀ n ≥ m, ↑(t n) = b) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i
<VAR>ι : Sort u_1<VAR>a b : ℝ<VAR>h : a ≤ b<VAR>c : ι → Set ↑(Icc a b)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i<GOAL>∃ t, ↑(t 0) = a ∧ Monotone t ∧ (∃ m, ∀ n ≥ m, ↑(t n) = b) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i
<VAR>ι : Sort u_1<VAR>a b : ℝ<VAR>h : a ≤ b<VAR>c : ι → Set ↑(Icc a b)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i<VAR>hδ : 0 < δ / 2<GOAL>∃ t, ↑(t 0) = a ∧ Monotone t ∧ (∃ m, ∀ n ≥ m, ↑(t n) = b) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i
<VAR>ι : Sort u_1<VAR>a b : ℝ<VAR>h : a ≤ b<VAR>c : ι → Set ↑(Icc a b)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i<VAR>hδ : 0 < δ / 2<VAR>n : ℕ<GOAL>∃ i, Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ⊆ c i
<VAR>ι : Sort u_1<VAR>a b : ℝ<VAR>h : a ≤ b<VAR>c : ι → Set ↑(Icc a b)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i<VAR>hδ : 0 < δ / 2<VAR>n : ℕ<VAR>i : ι<VAR>hsub : Metric.ball (addNSMul h (δ / 2) n) δ ⊆ c i<GOAL>∃ i, Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ⊆ c i
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedField 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x✝ y x : E<GOAL>↑‖x‖₊ ≤ egauge 𝕜 (closedBall 0 1) x
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : Subgroup G<VAR>g : ι → G<VAR>hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ<GOAL>H.index ≤ s.card
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>interior sᶜ = (closure s)ᶜ
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<GOAL>(X • A.map ⇑C + B.map ⇑C).det.coeff (Fintype.card n) = A.det
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<GOAL>∑ b : Equiv.Perm n, (sign b • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (b i) i).coeff (Fintype.card n) = ∑ σ : Equiv.Perm n, sign σ • ∏ i : n, A (σ i) i
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<GOAL>∀ x ∈ Finset.univ, (sign x • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (x i) i).coeff (Fintype.card n) = sign x • ∏ i : n, A (x i) i
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<GOAL>∀ (x : Equiv.Perm n), (sign x • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (x i) i).coeff (Fintype.card n) = sign x • ∏ i : n, A (x i) i
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>g : Equiv.Perm n<GOAL>(sign g • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff (Fintype.card n) = sign g • ∏ i : n, A (g i) i
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>g : Equiv.Perm n<GOAL>∏ i : n, A (g i) i = (∏ i : n, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff (Fintype.card n)
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>g : Equiv.Perm n<GOAL>∏ i : n, A (g i) i = (∏ i : n, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff (Fintype.card n * 1)
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>g : Equiv.Perm n<VAR>x✝ : n<VAR>a✝ : x✝ ∈ Finset.univ<GOAL>A (g x✝) x✝ = ((X • A.map ⇑C + B.map ⇑C) (g x✝) x✝).coeff 1
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>g : Equiv.Perm n<GOAL>∀ p ∈ Finset.univ, ((X • A.map ⇑C + B.map ⇑C) (g p) p).natDegree ≤ 1
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : NonUnitalNonAssocSemiring A<VAR>inst✝⁷ : Module R A<VAR>inst✝⁶ : IsScalarTower R A A<VAR>inst✝⁵ : SMulCommClass R A A<VAR>inst✝⁴ : NonUnitalNonAssocSemiring B<VAR>inst✝³ : Module R B<VAR>inst✝² : IsScalarTower R B B<VAR>inst✝¹ : SMulCommClass R B B<VAR>S : NonUnitalSubalgebra R A<VAR>ι : Type u_1<VAR>inst✝ : Nonempty ι<VAR>K : ι → NonUnitalSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)<VAR>T : NonUnitalSubalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>h : K i ≤ T<VAR>x✝ : ↥(K i)<GOAL>((iSupLift K dir f hf T hT).comp (inclusion h)) x✝ = (f i) x✝
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>f : F<GOAL>{x | x ∈ map (⇑f) s}.Pairwise Commute
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>f : F<GOAL>{x | ∃ a ∈ s, f a = x}.Pairwise Commute
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>f : F<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>a✝ : f x ≠ f y<GOAL>Commute (f x) (f y)
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝⁴ : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>s : A' ⥤ Type (max v₁ u₁)<VAR>inst✝² : HasLimits A'<VAR>inst✝¹ : PreservesLimits s<VAR>inst✝ : s.ReflectsIsomorphisms<GOAL>IsSheaf J P' ↔ IsSheaf J (P' ⋙ s)
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝⁴ : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>s : A' ⥤ Type (max v₁ u₁)<VAR>inst✝² : HasLimits A'<VAR>inst✝¹ : PreservesLimits s<VAR>inst✝ : s.ReflectsIsomorphisms<VAR>this : HasLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, u₂} A'<GOAL>IsSheaf J P' ↔ IsSheaf J (P' ⋙ s)
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝⁴ : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>s : A' ⥤ Type (max v₁ u₁)<VAR>inst✝² : HasLimits A'<VAR>inst✝¹ : PreservesLimits s<VAR>inst✝ : s.ReflectsIsomorphisms<VAR>this✝ : HasLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, u₂} A'<VAR>this : PreservesLimitsOfSize.{v₁, max v₁ u₁, max u₁ v₁, max u₁ v₁, u₂, max (u₁ + 1) (v₁ + 1)} s<GOAL>IsSheaf J P' ↔ IsSheaf J (P' ⋙ s)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S✝ : L.Substructure M<VAR>ι : Sort u_3<VAR>S : ι → L.Substructure M<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.843926, u_1} C<VAR>X✝ Y✝ Z : C<VAR>inst✝¹ : HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>inst✝ : Mono i₃<GOAL>(fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁) ≫ f = (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ≫ g
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.843926, u_1} C<VAR>X✝ Y✝ Z : C<VAR>inst✝¹ : HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>inst✝ : Mono i₃<GOAL>lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯ ≫ fst (fst f' g') i₁ = lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯ ≫ fst (snd f' g') i₂
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.843926, u_1} C<VAR>X✝ Y✝ Z : C<VAR>inst✝¹ : HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>inst✝ : Mono i₃<GOAL>lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁) (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫ lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯ = 𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂))
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.843926, u_1} C<VAR>X✝ Y✝ Z : C<VAR>inst✝¹ : HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>inst✝ : Mono i₃<GOAL>(lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁) (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫ lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯) ≫ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) = 𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂)
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.843926, u_1} C<VAR>X✝ Y✝ Z : C<VAR>inst✝¹ : HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>inst✝ : Mono i₃<GOAL>(lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁) (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫ lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯) ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) = 𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.843926, u_1} C<VAR>X✝ Y✝ Z : C<VAR>inst✝¹ : HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>inst✝ : Mono i₃<GOAL>lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯ ≫ lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁) (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ = 𝟙 (pullback f g)
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.843926, u_1} C<VAR>X✝ Y✝ Z : C<VAR>inst✝¹ : HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>inst✝ : Mono i₃<GOAL>(lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯ ≫ lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁) (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯) ≫ fst f g = 𝟙 (pullback f g) ≫ fst f g
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.843926, u_1} C<VAR>X✝ Y✝ Z : C<VAR>inst✝¹ : HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>inst✝ : Mono i₃<GOAL>(lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯ ≫ lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁) (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯) ≫ snd f g = 𝟙 (pullback f g) ≫ snd f g
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.90051, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>T₁ T₂ : (Triangle C)ᵒᵖ<VAR>φ : T₁ ⟶ T₂<GOAL>((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₁).obj₁) ≫ (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₁).mor₃.op) ≫ (shiftFunctor Cᵒᵖ 1).map φ.unop.hom₃.op = φ.unop.hom₁.op ≫ (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₂).obj₁) ≫ (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₂).mor₃.op
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.90051, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>T₁ T₂ : (Triangle C)ᵒᵖ<VAR>φ : T₁ ⟶ T₂<GOAL>(opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₁).obj₁) ≫ (shiftFunctor Cᵒᵖ 1).map ((shiftFunctor C 1).map φ.unop.hom₁).op ≫ (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₂).mor₃.op = (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₁).obj₁) ≫ (shiftFunctor Cᵒᵖ 1).map ((shiftFunctor C 1).map φ.unop.hom₁.op.unop).op ≫ (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₂).mor₃.op
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : α → F'<GOAL>μ[f|⊥] =ᶠ[ae μ] fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : α → F'<GOAL>0[f|⊥] =ᶠ[ae 0] fun x => (0 Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂0
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>f : α → F'<VAR>hμ : NeZero μ<GOAL>μ[f|⊥] =ᶠ[ae μ] fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a : α<VAR>ha : 0 < a<GOAL>(Ioi a)⁻¹ = Ioo 0 a⁻¹
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>i j k : ι<VAR>inst✝ : K.HasHomology i<GOAL>K.ExactAt i ↔ IsZero (K.sc i).homology
<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>F✝ G H I : C ⥤ D<VAR>X Y : C<VAR>e : X ≅ Y<VAR>F : C ⥤ D ⥤ E<VAR>Z : D<GOAL>(F.map e.inv).app Z ≫ (F.map e.hom).app Z = 𝟙 ((F.obj Y).obj Z)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (K →+* ℂ) → ℂ<GOAL>x ∈ Submodule.span ℤ (Set.range ⇑(latticeBasis K)) ↔ x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (K →+* ℂ) → ℂ<GOAL>x ∈ Submodule.span ℤ (⇑(canonicalEmbedding K).toIntAlgHom.toLinearMap '' Set.range ⇑(integralBasis K)) ↔ x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (K →+* ℂ) → ℂ<GOAL>x ∈ ⇑(canonicalEmbedding K).toIntAlgHom.toLinearMap '' ↑(Submodule.span ℤ (Set.range ⇑(integralBasis K))) ↔ x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (K →+* ℂ) → ℂ<GOAL>(∃ x_1 ∈ ↑(Submodule.span ℤ (Set.range ⇑(integralBasis K))), (canonicalEmbedding K).toIntAlgHom.toLinearMap x_1 = x) ↔ ∃ x_1 ∈ (algebraMap (𝓞 K) K).range, (canonicalEmbedding K) x_1 = x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (K →+* ℂ) → ℂ<GOAL>(∃ x_1 ∈ (algebraMap (𝓞 K) K).range, (canonicalEmbedding K).toIntAlgHom.toLinearMap x_1 = x) ↔ ∃ x_1 ∈ (algebraMap (𝓞 K) K).range, (canonicalEmbedding K) x_1 = x
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>a b : α<VAR>h : normalize b = b<GOAL>gcd a b = b ↔ b ∣ a
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<GOAL>eval₂ f x p = eval₂ (f.comp (Subring.closure ↑p.coeffs).subtype) x p.restriction
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<VAR>i : ℕ<VAR>hin : i ≤ n<VAR>hpi : ↑p ^ i = 0<GOAL>i = n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<VAR>i : ℕ<VAR>hin : i ≤ n<VAR>hpi : i ≠ n<GOAL>↑p ^ i ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<VAR>i : ℕ<VAR>hpi : i ≠ n<VAR>hin : i < n<GOAL>↑p ^ i ≠ 0