ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>x : ↥U<VAR>h : IsUnit ((X.presheaf.germ x) f)<VAR>V : Opens ↑↑X.toPresheafedSpace<VAR>hxV : ↑x ∈ V<VAR>g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))<VAR>W : Opens ↑↑X.toPresheafedSpace := U ⊓ V<VAR>hxW : ↑x ∈ W<VAR>heq : (X.presheaf.germ ⟨↑x, hxW⟩) ((X.presheaf.map (U.infLELeft V).op) f * (X.presheaf.map (U.infLERight V).op) g) = (X.presheaf.germ ⟨↑x, hxW⟩) 1<VAR>W' : Opens ↑↑X.toPresheafedSpace<VAR>hxW' : ↑x ∈ W'<VAR>i₁ i₂ : W' ⟶ W<VAR>heq' : (X.presheaf.map i₁.op) ((X.presheaf.map (U.infLELeft V).op) f * (X.presheaf.map (U.infLERight V).op) g) = (X.presheaf.map i₂.op) 1<GOAL>IsUnit ((X.presheaf.map (i₁ ≫ U.infLELeft V).op) f)
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>x : ↥U<VAR>h : IsUnit ((X.presheaf.germ x) f)<VAR>V : Opens ↑↑X.toPresheafedSpace<VAR>hxV : ↑x ∈ V<VAR>g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))<VAR>W : Opens ↑↑X.toPresheafedSpace := U ⊓ V<VAR>hxW : ↑x ∈ W<VAR>heq : (X.presheaf.germ ⟨↑x, hxW⟩) ((X.presheaf.map (U.infLELeft V).op) f * (X.presheaf.map (U.infLERight V).op) g) = (X.presheaf.germ ⟨↑x, hxW⟩) 1<VAR>W' : Opens ↑↑X.toPresheafedSpace<VAR>hxW' : ↑x ∈ W'<VAR>i₁ i₂ : W' ⟶ W<VAR>heq' : (X.presheaf.map i₁.op) ((X.presheaf.map (U.infLELeft V).op) f) * (X.presheaf.map i₁.op) ((X.presheaf.map (U.infLERight V).op) g) = 1<GOAL>IsUnit ((X.presheaf.map (i₁ ≫ U.infLELeft V).op) f)
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>x : ↥U<VAR>h : IsUnit ((X.presheaf.germ x) f)<VAR>V : Opens ↑↑X.toPresheafedSpace<VAR>hxV : ↑x ∈ V<VAR>g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))<VAR>W : Opens ↑↑X.toPresheafedSpace := U ⊓ V<VAR>hxW : ↑x ∈ W<VAR>heq : (X.presheaf.germ ⟨↑x, hxW⟩) ((X.presheaf.map (U.infLELeft V).op) f * (X.presheaf.map (U.infLERight V).op) g) = (X.presheaf.germ ⟨↑x, hxW⟩) 1<VAR>W' : Opens ↑↑X.toPresheafedSpace<VAR>hxW' : ↑x ∈ W'<VAR>i₁ i₂ : W' ⟶ W<VAR>heq' : (X.presheaf.map (i₁ ≫ U.infLELeft V).op) f * (X.presheaf.map ((U.infLERight V).op ≫ i₁.op)) g = 1<GOAL>IsUnit ((X.presheaf.map (i₁ ≫ U.infLELeft V).op) f)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S : C ⥤ D<VAR>T : D<VAR>𝒢 : Set C<VAR>h𝒢 : IsSeparating 𝒢<GOAL>IsSeparating ((proj S T).obj ⁻¹' 𝒢)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S : C ⥤ D<VAR>T : D<VAR>𝒢 : Set C<VAR>h𝒢 : IsSeparating 𝒢<VAR>X Y : CostructuredArrow S T<VAR>f g : X ⟶ Y<VAR>hfg : ∀ G ∈ (proj S T).obj ⁻¹' 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g<VAR>G : C<VAR>hG : G ∈ 𝒢<VAR>h : G ⟶ X.left<GOAL>h ≫ f.left = h ≫ g.left
<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✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hcont : ContinuousOn f [[a, b]]<VAR>hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hint : IntervalIntegrable f' volume a b<GOAL>∫ (y : ℝ) in a..b, f' y = f b - f a
<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✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hcont : ContinuousOn f [[a, b]]<VAR>hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hint : IntervalIntegrable f' volume a b<VAR>hab : a ≤ b<GOAL>∫ (y : ℝ) in a..b, f' y = f b - f a
<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✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hcont : ContinuousOn f [[a, b]]<VAR>hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hint : IntervalIntegrable f' volume a b<VAR>hab : b ≤ a<GOAL>∫ (y : ℝ) in a..b, f' y = f b - f a
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f'✝ : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>g : γ → δ<VAR>f' : β' → α' → δ<VAR>g₁ : β → β'<VAR>g₂ : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)<GOAL>g '' image2 f s t = image2 f' (g₁ '' t) (g₂ '' s)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f'✝ : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>g : γ → δ<VAR>f' : β' → α' → δ<VAR>g₁ : β → β'<VAR>g₂ : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)<GOAL>g '' image2 (fun a b => f b a) t s = image2 f' (g₁ '' t) (g₂ '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>f : α ≃. β<VAR>a₁ a₂ : α<VAR>b : β<VAR>h₁ : b ∈ f a₁<VAR>h₂ : b ∈ f a₂<GOAL>a₁ = a₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>f : α ≃. β<VAR>a₁ a₂ : α<VAR>b : β<VAR>h₁ : a₁ ∈ f.symm b<VAR>h₂ : a₂ ∈ f.symm b<GOAL>a₁ = a₂
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝¹ : MetricSpace X<VAR>inst✝ : MetricSpace Y<VAR>x y : X ⊕ Y<GOAL>Sum.dist x y = Sum.dist y x
<VAR>α : Type u<VAR>β : Type u_1<VAR>x : α<VAR>inst✝ : LinearOrderedRing α<VAR>k : ℕ<VAR>h : Odd (k + 1 + 1)<GOAL>0 < ∑ i ∈ range (k + 1 + 1), x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>x : α<VAR>inst✝ : LinearOrderedRing α<VAR>k : ℕ<VAR>h : ¬Even (k + 1 + 1)<GOAL>0 < ∑ i ∈ range (k + 1 + 1), x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>x : α<VAR>inst✝ : LinearOrderedRing α<VAR>k : ℕ<VAR>h : ¬Even (k + 1 + 1)<VAR>hx : x + 1 < 0<GOAL>0 < ∑ i ∈ range (k + 1 + 1), x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>x : α<VAR>inst✝ : LinearOrderedRing α<VAR>k : ℕ<VAR>h : ¬Even (k + 1 + 1)<VAR>hx : x + 1 = 0<GOAL>0 < ∑ i ∈ range (k + 1 + 1), x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>x : α<VAR>inst✝ : LinearOrderedRing α<VAR>k : ℕ<VAR>h : ¬Even (k + 1 + 1)<VAR>hx : 0 < x + 1<GOAL>0 < ∑ i ∈ range (k + 1 + 1), x ^ i
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>frontier (sphere x r) = sphere x r
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>h : K ≤ K'<VAR>x : ↥K'<GOAL>x ∈ ofLe h ↔ ↑x ∈ K
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>h : K ≤ K'<VAR>x : ↥K'<GOAL>(∃ y, ⟨↑y, ⋯⟩ = x) ↔ ↑x ∈ K
<VAR>α β γ : Type u<VAR>S S' : Set (α → ℕ)<VAR>f : (α → ℕ) → ℕ<VAR>g : α → β<VAR>d : DiophFn f<GOAL>DiophFn fun v => f (v ∘ g)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>Hf : ∀ a ∈ s, f a ∈ t<VAR>n : ℕ<VAR>hn : ∀ a ∈ t, n ≤ (filter (fun x => f x = a) s).card<GOAL>n * t.card = ∑ _a ∈ t, n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>Hf : ∀ a ∈ s, f a ∈ t<VAR>n : ℕ<VAR>hn : ∀ a ∈ t, n ≤ (filter (fun x => f x = a) s).card<GOAL>∑ a ∈ t, (filter (fun x => f x = a) s).card = s.card
<VAR>xl xr : Type u<VAR>x x' : PGame<VAR>h : x' ⧏ x<GOAL>x.insertLeft x' ≈ x
<VAR>xl xr : Type u<VAR>x x' : PGame<VAR>h : x' ⧏ x<GOAL>x.insertLeft x' ≤ x ∧ x ≤ x.insertLeft x'
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : IsUnifLocDoublingMeasure μ<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>K : ℝ<VAR>R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)<GOAL>VitaliFamily μ
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : IsUnifLocDoublingMeasure μ<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>K : ℝ<VAR>R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)<VAR>Rpos : 0 < R<GOAL>VitaliFamily μ
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : IsUnifLocDoublingMeasure μ<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>K : ℝ<VAR>R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)<VAR>Rpos : 0 < R<VAR>A : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * μ (closedBall x r)<GOAL>VitaliFamily μ
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>h : m = n✝<VAR>n : ℕ<GOAL>n ∣ m ↔ n ∣ n✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>a : α<GOAL>Irreducible (Associates.mk a) ↔ Irreducible a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>a : α<GOAL>(¬IsUnit a ∧ ∀ (a_1 a_2 : α), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) ↔ ¬IsUnit a ∧ ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>a : α<GOAL>(∀ (a_1 a_2 : α), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) ↔ ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F (α ::: Cofix F α)<GOAL>(mk x).dest = x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F (α ::: Cofix F α)<VAR>this : mk ∘ dest = _root_.id<GOAL>(mk x).dest = x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<GOAL>pi f = ⊥ ↔ ∃ i, f i = ⊥
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>inst✝ : DivisionRing K<VAR>n_le_m : n ≤ m<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.nums m = g.nums n
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁸ : Field F✝<VAR>inst✝⁷ : Field E✝<VAR>inst✝⁶ : Algebra F✝ E✝<VAR>inst✝⁵ : FiniteDimensional F✝ E✝<VAR>inst✝⁴ : Algebra.IsSeparable F✝ E✝<VAR>F : Type u_3<VAR>E : Type u_4<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : FiniteDimensional F E<VAR>α : E<GOAL>F⟮α⟯ = ⊤ ↔ (minpoly F α).natDegree = finrank F E
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁸ : Field F✝<VAR>inst✝⁷ : Field E✝<VAR>inst✝⁶ : Algebra F✝ E✝<VAR>inst✝⁵ : FiniteDimensional F✝ E✝<VAR>inst✝⁴ : Algebra.IsSeparable F✝ E✝<VAR>F : Type u_3<VAR>E : Type u_4<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : FiniteDimensional F E<VAR>α : E<GOAL>F⟮α⟯ = ⊤ ↔ finrank F ↥F⟮α⟯ = finrank F ↥⊤
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁸ : Field F✝<VAR>inst✝⁷ : Field E✝<VAR>inst✝⁶ : Algebra F✝ E✝<VAR>inst✝⁵ : FiniteDimensional F✝ E✝<VAR>inst✝⁴ : Algebra.IsSeparable F✝ E✝<VAR>F : Type u_3<VAR>E : Type u_4<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : FiniteDimensional F E<VAR>α : E<VAR>h : F⟮α⟯ = ⊤<GOAL>finrank F ↥F⟮α⟯ = finrank F ↥⊤
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l l' : ℝ≥0<VAR>hl' : l' ≠ 0<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ s<VAR>hfφ : HasConstantSpeedOnWith (f ∘ φ) s l<VAR>hf : HasConstantSpeedOnWith f (φ '' s) l'<VAR>x : ℝ<VAR>xs : x ∈ s<VAR>y : ℝ<VAR>ys : y ∈ s<GOAL>φ y = (fun y => ↑l / ↑l' * (y - x) + φ x) y
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l l' : ℝ≥0<VAR>hl' : l' ≠ 0<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ s<VAR>hfφ : HasConstantSpeedOnWith (f ∘ φ) s l<VAR>hf : HasConstantSpeedOnWith f (φ '' s) l'<VAR>x : ℝ<VAR>xs : x ∈ s<VAR>y : ℝ<VAR>ys : y ∈ s<GOAL>(φ y - φ x) * ↑l' = (y - x) * ↑l
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l l' : ℝ≥0<VAR>hl' : l' ≠ 0<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ s<VAR>hfφ : HasConstantSpeedOnWith (f ∘ φ) s l<VAR>hf : LocallyBoundedVariationOn f (φ '' s) ∧ ∀ ⦃x : ℝ⦄, x ∈ φ '' s → ∀ ⦃y : ℝ⦄, y ∈ φ '' s → variationOnFromTo f (φ '' s) x y = ↑l' * (y - x)<VAR>x : ℝ<VAR>xs : x ∈ s<VAR>y : ℝ<VAR>ys : y ∈ s<GOAL>(φ y - φ x) * ↑l' = (y - x) * ↑l
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l l' : ℝ≥0<VAR>hl' : l' ≠ 0<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ s<VAR>hfφ : LocallyBoundedVariationOn (f ∘ φ) s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo (f ∘ φ) s x y = ↑l * (y - x)<VAR>hf : LocallyBoundedVariationOn f (φ '' s) ∧ ∀ ⦃x : ℝ⦄, x ∈ φ '' s → ∀ ⦃y : ℝ⦄, y ∈ φ '' s → variationOnFromTo f (φ '' s) x y = ↑l' * (y - x)<VAR>x : ℝ<VAR>xs : x ∈ s<VAR>y : ℝ<VAR>ys : y ∈ s<GOAL>(φ y - φ x) * ↑l' = (y - x) * ↑l
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l l' : ℝ≥0<VAR>hl' : l' ≠ 0<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ s<VAR>hfφ : LocallyBoundedVariationOn (f ∘ φ) s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo (f ∘ φ) s x y = ↑l * (y - x)<VAR>hf : LocallyBoundedVariationOn f (φ '' s) ∧ ∀ ⦃x : ℝ⦄, x ∈ φ '' s → ∀ ⦃y : ℝ⦄, y ∈ φ '' s → variationOnFromTo f (φ '' s) x y = ↑l' * (y - x)<VAR>x : ℝ<VAR>xs : x ∈ s<VAR>y : ℝ<VAR>ys : y ∈ s<GOAL>(y - x) * ↑l = (φ y - φ x) * ↑l'
<VAR>α : Sort u_1<VAR>β : α → Sort u_2<VAR>fst✝¹ : α<VAR>snd✝¹ : β fst✝¹<VAR>fst✝ : α<VAR>snd✝ : β fst✝<GOAL>⟨fst✝¹, snd✝¹⟩ = ⟨fst✝, snd✝⟩ ↔ ⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fst ∧ HEq ⟨fst✝¹, snd✝¹⟩.snd ⟨fst✝, snd✝⟩.snd
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>g : S →+* T<VAR>f : R →+* S<GOAL>Subring.map g f.range = (g.comp f).range
<VAR>a : UnitAddCircle<VAR>x : ℝ<GOAL>sinKernel (-a) x = -sinKernel a x
<VAR>x a' : ℝ<GOAL>sinKernel (-↑a') x = -sinKernel (↑a') x
<VAR>m n : ℕ<VAR>a b : ℤ<VAR>c : ℕ<GOAL>↑a = ↑b ↔ ↑c ∣ b - a
<VAR>m : Type u → Type u<VAR>inst✝ : Monad m<VAR>α β : Type u<VAR>f : β → α → β<VAR>x✝ y✝ : FreeMonoid α<GOAL>{ toFun := fun xs => op (flip (List.foldl f) (FreeMonoid.toList xs)), map_one' := ⋯ }.toFun (x✝ * y✝) = { toFun := fun xs => op (flip (List.foldl f) (FreeMonoid.toList xs)), map_one' := ⋯ }.toFun x✝ * { toFun := fun xs => op (flip (List.foldl f) (FreeMonoid.toList xs)), map_one' := ⋯ }.toFun y✝
<VAR>m : Type u → Type u<VAR>inst✝ : Monad m<VAR>α β : Type u<VAR>f : β → α → β<VAR>x✝ y✝ : FreeMonoid α<GOAL>(op fun a => List.foldl f (List.foldl f a (FreeMonoid.toList x✝)) (FreeMonoid.toList y✝)) = (op fun a => List.foldl f a (FreeMonoid.toList x✝)) * op fun a => List.foldl f a (FreeMonoid.toList y✝)
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MulZeroOneClass M₀<VAR>h : 0 = 1<VAR>a : M₀<GOAL>a = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>p q : Submodule R (CliffordAlgebra Q)<GOAL>Submodule.map reverse (p * q) = Submodule.map reverse q * Submodule.map reverse p
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝³ : Monoid M<VAR>inst✝² : LinearOrder M<VAR>inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : M<VAR>h : a * b ≤ c ^ 2<GOAL>min a b ≤ c
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>x : PrimeSpectrum R<GOAL>x ∈ imageOfDf f ↔ x ∈ ⇑(PrimeSpectrum.comap C) '' (zeroLocus {f})ᶜ
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>x : PrimeSpectrum R<VAR>hx : x ∈ imageOfDf f<GOAL>{ asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ } ∈ (zeroLocus {f})ᶜ
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>x : PrimeSpectrum R<VAR>hx : x ∈ imageOfDf f<GOAL>(PrimeSpectrum.comap C) { asIdeal := Ideal.map C x.asIdeal, isPrime := ⋯ } = x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>x : PrimeSpectrum R<GOAL>x ∈ ⇑(PrimeSpectrum.comap C) '' (zeroLocus {f})ᶜ → x ∈ imageOfDf f
<VAR>x : ℝ<GOAL>↑(↑x).abs = ↑|x|
<VAR>x : ℝ<GOAL>↑↑(Real.nnabs x) = ↑↑(Real.nnabs x)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>y : β<GOAL>y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s ∩ ϕ t ⁻¹' n).Nonempty
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>y : β<GOAL>(∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty) ↔ ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocSemiring R<VAR>r : R<VAR>n : ℕ<VAR>inst✝ : n.AtLeastTwo<GOAL>OfNat.ofNat n * r = n • r
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x : R<GOAL>Wbtw R 1 x 0 ↔ x ∈ Set.Icc 0 1
<VAR>α : Type u<VAR>l✝ l' l : List α<VAR>k : ℕ<VAR>this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length<GOAL>(l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k
<VAR>α : Type u<VAR>l✝ l' l : List α<VAR>k : ℕ<VAR>this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length<VAR>n : ℕ<VAR>hn : n < (l.rotate k).cyclicPermutations.length<VAR>hn' : n < (l.cyclicPermutations.rotate k).length<GOAL>(l.rotate k).cyclicPermutations.get ⟨n, hn⟩ = (l.cyclicPermutations.rotate k).get ⟨n, hn'⟩
<VAR>α : Type u<VAR>l✝ l' l : List α<VAR>k : ℕ<VAR>this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length<VAR>n : ℕ<VAR>hn : n < (l.rotate k).cyclicPermutations.length<VAR>hn' : n < (l.cyclicPermutations.rotate k).length<GOAL>l.rotate ((↑⟨n, hn⟩ + k) % l.length) = l.cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % l.cyclicPermutations.length, ⋯⟩
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ : ComposableArrows C n<VAR>F G : ComposableArrows C 1<VAR>left : F.left = G.left<VAR>right : F.right = G.right<VAR>w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯<GOAL>F.map' 0 1 ⋯ ⋯ ≫ (eqToIso right).hom = (eqToIso left).hom ≫ G.map' 0 1 ⋯ ⋯
<VAR>C : Type u<VAR>inst✝¹⁰ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁹ : Category.{max v u, w} D<VAR>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : (forget D).ReflectsIsomorphisms<VAR>K : Type w'<VAR>inst✝² : SmallCategory K<VAR>inst✝¹ : FinCategory K<VAR>inst✝ : HasLimitsOfShape K D<VAR>P : Cᵒᵖ ⥤ D<GOAL>J.toSheafify P ≫ (plusPlusIsoSheafify J D P).hom = toSheafify J P
<VAR>C : Type u<VAR>inst✝¹⁰ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁹ : Category.{max v u, w} D<VAR>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : (forget D).ReflectsIsomorphisms<VAR>K : Type w'<VAR>inst✝² : SmallCategory K<VAR>inst✝¹ : FinCategory K<VAR>inst✝ : HasLimitsOfShape K D<VAR>P : Cᵒᵖ ⥤ D<VAR>e_1✝ : (P ⟶ sheafify J P) = ((𝟭 (Cᵒᵖ ⥤ D)).obj P ⟶ (sheafToPresheaf J D).obj ((presheafToSheaf J D).obj P))<VAR>e_3✝ : P = (𝟭 (Cᵒᵖ ⥤ D)).obj P<VAR>e_4✝ : J.sheafify P = (plusPlusSheaf J D ⋙ sheafToPresheaf J D).obj P<GOAL>J.toSheafify = (plusPlusAdjunction J D).unit.app
<VAR>C : Type u<VAR>inst✝¹⁰ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁹ : Category.{max v u, w} D<VAR>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : (forget D).ReflectsIsomorphisms<VAR>K : Type w'<VAR>inst✝² : SmallCategory K<VAR>inst✝¹ : FinCategory K<VAR>inst✝ : HasLimitsOfShape K D<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>e_1✝ : (P✝ ⟶ sheafify J P✝) = ((𝟭 (Cᵒᵖ ⥤ D)).obj P✝ ⟶ (sheafToPresheaf J D).obj ((presheafToSheaf J D).obj P✝))<VAR>e_3✝ : P✝ = (𝟭 (Cᵒᵖ ⥤ D)).obj P✝<VAR>e_4✝ : J.sheafify P✝ = (plusPlusSheaf J D ⋙ sheafToPresheaf J D).obj P✝<VAR>P : Cᵒᵖ ⥤ D<GOAL>J.toPlus P ≫ J.plusMap (J.toPlus P) = (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ 𝟙 (J.sheafify P)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>hf : Injective ⇑f<VAR>p : R[X]<GOAL>(map f p).coeff (map f p).natDegree = f (p.coeff p.natDegree)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s✝ t : ι → α<VAR>a b : α<VAR>s : Set β<VAR>f : β → α<GOAL>IsLUB (f '' s) (⨆ x ∈ s, f x)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>a : α<GOAL>filter (fun x => a == x) l = replicate (count a l) a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))<GOAL>span {(mk W) (C (X - C x₂)), (mk W) (Y - C (C (eval x₂ (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁))))} = span {(mk W) (C (X - C x₂)), (mk W) (Y - C (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁))}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))<GOAL>span {(mk W) (C (X - C x₂)), (mk W) (Y - C (C (eval x₂ (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁))) + C (X - C x₂) * C (C (-W.slope x₁ x₂ y₁ y₂)))} = span {(mk W) (C (X - C x₂)), (mk W) (Y - C (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁))}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))<GOAL>Y - C (C (eval x₂ (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁))) + C (X - C x₂) * C (C (-W.slope x₁ x₂ y₁ y₂)) = Y - C (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁)