ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.68425, u_1} C<VAR>inst✝⁶ : Category.{?u.68429, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)<GOAL>(HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ₁).mor₃ ≫ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app K₁ ≫ (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ₁).mor₃ ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a) ≫ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app K₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.68425, u_1} C<VAR>inst✝⁶ : Category.{?u.68429, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)<GOAL>(HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ₁).mor₃ ≫ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) 1 ⋙ HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a ≫ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app K₂ = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ₁).mor₃ ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a) ≫ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app K₂
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>cs.lengthParity w = Multiplicative.ofAdd ↑(cs.length w)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>hω : ω.length = cs.length (cs.wordProd ω)<GOAL>cs.lengthParity (cs.wordProd ω) = Multiplicative.ofAdd ↑(cs.length (cs.wordProd ω))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J I : Box ι<VAR>r : (ι → ℝ) → ↑(Ioi 0)<GOAL>∃ π, π.IsPartition ∧ π.IsHenstock ∧ π.IsSubordinate r ∧ (∀ J ∈ π, ∃ m, ∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) ∧ π.distortion = I.distortion
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J✝ I : Box ι<VAR>r : (ι → ℝ) → ↑(Ioi 0)<VAR>J : Box ι<VAR>x✝ : J ≤ I<VAR>hJ : ∀ J' ∈ splitCenter J, ∃ π, π.IsPartition ∧ π.IsHenstock ∧ π.IsSubordinate r ∧ (∀ J ∈ π, ∃ m, ∀ (i : ι), J.upper i - J.lower i = (J'.upper i - J'.lower i) / 2 ^ m) ∧ π.distortion = J'.distortion<GOAL>∃ π, π.IsPartition ∧ π.IsHenstock ∧ π.IsSubordinate r ∧ (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧ π.distortion = J.distortion
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J I : Box ι<VAR>r : (ι → ℝ) → ↑(Ioi 0)<VAR>z : ι → ℝ<VAR>x✝ : z ∈ Box.Icc I<GOAL>∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → ∃ π, π.IsPartition ∧ π.IsHenstock ∧ π.IsSubordinate r ∧ (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧ π.distortion = J.distortion
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>c : α<VAR>H : ∀ (x : ι), f x ≤ c<GOAL>∀ b ∈ range f, b ≤ c
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>hX : Memℒp X 2 μ<VAR>hXint : ∫ (x : Ω), X x ∂μ = 0<GOAL>variance X μ = ∫ (x : Ω), (X ^ 2) x ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>hX : Memℒp X 2 μ<VAR>hXint : ∫ (x : Ω), X x ∂μ = 0<GOAL>∫ (x : Ω), X x ^ 2 ∂μ = ∫ (x : Ω), (X ^ 2) x ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>hX : Memℒp X 2 μ<VAR>hXint : ∫ (x : Ω), X x ∂μ = 0<GOAL>Integrable (fun ω => X ω ^ 2) μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>hX : Memℒp X 2 μ<VAR>hXint : ∫ (x : Ω), X x ∂μ = 0<GOAL>0 ≤ᶠ[ae μ] fun ω => X ω ^ 2
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ∂(κ + η) a = (κ a) s
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<VAR>h_le : κ ≤ κ + η<GOAL>∫⁻ (x : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ∂(κ + η) a = (κ a) s
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>e : Basis ι R M<VAR>f : M ≃ₗ[R] M'<VAR>v : Basis ι R M<VAR>v' : Basis ι R M'<GOAL>IsUnit ((toMatrix v v') ↑f).det
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>e : Basis ι R M<VAR>f : M ≃ₗ[R] M'<VAR>v : Basis ι R M<VAR>v' : Basis ι R M'<GOAL>?B * (toMatrix v v') ↑f = 1
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>e : Basis ι R M<VAR>f : M ≃ₗ[R] M'<VAR>v : Basis ι R M<VAR>v' : Basis ι R M'<GOAL>Matrix ι ι R
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝³ : DecidablePred p<VAR>inst✝² : DecidablePred q<VAR>s✝ t✝ : Finset α<VAR>inst✝¹ : DecidableEq α<VAR>s t : Finset α<VAR>inst✝ : (i : α) → Decidable (i ∈ t)<VAR>i : α<GOAL>i ∈ filter (fun i => i ∈ t) s ↔ i ∈ s ∩ t
<VAR>I : Type u<VAR>inst✝³ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X₁ X₂ : GradedObject I C<VAR>inst✝ : X₁.HasTensor X₂<VAR>A : C<VAR>j : I<VAR>f g : tensorObj X₁ X₂ j ⟶ A<VAR>h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g<GOAL>f = g
<VAR>I : Type u<VAR>inst✝³ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X₁ X₂ : GradedObject I C<VAR>inst✝ : X₁.HasTensor X₂<VAR>A : C<VAR>j : I<VAR>f g : tensorObj X₁ X₂ j ⟶ A<VAR>h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g<GOAL>∀ (i : I × I) (hij : (match i with | (i, j) => i + j) = j), (((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂).ιMapObj (fun x => match x with | (i, j) => i + j) i j hij ≫ f = (((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂).ιMapObj (fun x => match x with | (i, j) => i + j) i j hij ≫ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (LowerSet α)<VAR>s t : LowerSet α<VAR>a : α<VAR>f : (i : ι) → κ i → LowerSet α<GOAL>↑(⨆ i, ⨆ j, f i j) = ⋃ i, ⋃ j, ↑(f i j)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>x y : γ<GOAL>0 = dist x y ↔ x = y
<VAR>x y : ℝ*<VAR>hx : x.InfinitePos<VAR>hy₁ : ¬y.Infinitesimal<VAR>hy₂ : 0 < y<VAR>r : ℝ<GOAL>↑r < x * y
<VAR>x y : ℝ*<VAR>hx : x.InfinitePos<VAR>hy₁ : ¬y.Infinitesimal<VAR>hy₂ : 0 < y<VAR>r : ℝ<VAR>hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)<GOAL>↑r < x * y
<VAR>x y : ℝ*<VAR>hx : x.InfinitePos<VAR>hy₁ : ¬y.Infinitesimal<VAR>hy₂ : 0 < y<VAR>r : ℝ<VAR>hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)<VAR>r₁ : ℝ<VAR>hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)<GOAL>↑r < x * y
<VAR>x y : ℝ*<VAR>hx : x.InfinitePos<VAR>hy₁ : ¬y.Infinitesimal<VAR>hy₂ : 0 < y<VAR>r : ℝ<VAR>hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)<VAR>r₁ : ℝ<VAR>hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)<VAR>hyr : 0 < r₁ ∧ ↑r₁ ≤ y<GOAL>↑r < x * y
<VAR>x y : ℝ*<VAR>hx : x.InfinitePos<VAR>hy₁ : ¬y.Infinitesimal<VAR>hy₂ : 0 < y<VAR>r : ℝ<VAR>hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)<VAR>r₁ : ℝ<VAR>hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)<VAR>hyr : 0 < r₁ ∧ ↑r₁ ≤ y<GOAL>↑(r / r₁) * ↑r₁ < x * y
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S✝<VAR>inst✝ : NonAssocSemiring T<VAR>S : Set (Subsemiring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : Group G<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : UniformSpace G<VAR>inst✝ : UniformGroup G<VAR>p : ι → Prop<VAR>b : ι → Set G<VAR>h : (𝓝 1).HasBasis p b<GOAL>(𝓝 1).HasBasis p fun i => {f | ∀ (x : α), toFun f x ∈ b i}
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : Group G<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : UniformSpace G<VAR>inst✝ : UniformGroup G<VAR>p : ι → Prop<VAR>b : ι → Set G<VAR>h : (𝓝 1).HasBasis p b<VAR>x✝¹ : ι<VAR>x✝ : α →ᵤ G<GOAL>(∀ (x : α), toFun x✝ x ∈ b x✝¹) ↔ (1, x✝) ∈ UniformFun.gen α G {x | x.2 / x.1 ∈ b x✝¹}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hsm : MeasurableSet s<VAR>hfs : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤<GOAL>∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ - ∫⁻ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d✝ k N : ℕ<VAR>x : Fin n → ℕ<VAR>d : ℕ<GOAL>(fun a => ∑ i : Fin n, a i * d ^ ↑i) 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d✝ k N : ℕ<VAR>x : Fin n → ℕ<VAR>d : ℕ<VAR>a b : Fin n → ℕ<GOAL>{ toFun := fun a => ∑ i : Fin n, a i * d ^ ↑i, map_zero' := ⋯ }.toFun (a + b) = { toFun := fun a => ∑ i : Fin n, a i * d ^ ↑i, map_zero' := ⋯ }.toFun a + { toFun := fun a => ∑ i : Fin n, a i * d ^ ↑i, map_zero' := ⋯ }.toFun b
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle y (y - x) = ↑(Real.arctan (‖x‖ / ‖y‖))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle y (y - x)).sign = 1<GOAL>o.oangle y (y - x) = ↑(Real.arctan (‖x‖ / ‖y‖))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<GOAL>Continuous fun a => a ^ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>k : ℕ<GOAL>Continuous fun a => a ^ (k + 1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>k : ℕ<GOAL>Continuous fun a => a * a ^ k
<VAR>K : Type u_1<VAR>n : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n K<VAR>h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖<GOAL>A.det ≠ 0
<VAR>K : Type u_1<VAR>n : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n K<VAR>h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖<GOAL>A.transpose.det ≠ 0
<VAR>G : Type u<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝ : (i : ι) → Monoid (M i)<VAR>j : ι<VAR>hj : exponent (M j) = 0<GOAL>exponent ((i : ι) → M i) = 0
<VAR>G : Type u<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝ : (i : ι) → Monoid (M i)<VAR>j : ι<VAR>hj : ¬∃ n, 0 < n ∧ ∀ (g : M j), g ^ n = 1<GOAL>¬∃ n, 0 < n ∧ ∀ (g : (i : ι) → M i), g ^ n = 1
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>f : F.obj X ⟶ Y<GOAL>F.map (adj.unit.app X ≫ G.map f) ≫ adj.counit.app Y = f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>f : F.obj X ⟶ Y<GOAL>(F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X)) ≫ (𝟭 D).map f = f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>f : F.obj X ⟶ Y<VAR>e_4✝ : (𝟭 D).obj (F.obj X) = F.obj X<GOAL>F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>f : F.obj X ⟶ Y<VAR>e_4✝ : (𝟭 D).obj (F.obj X) = F.obj X<VAR>t : (fun s => s.app X) (whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ whiskerLeft F adj.counit) = (fun s => s.app X) (NatTrans.id (𝟭 C ⋙ F))<GOAL>F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>f : F.obj X ⟶ Y<VAR>e_4✝ : (𝟭 D).obj (F.obj X) = F.obj X<VAR>t : F.map (adj.unit.app X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)<GOAL>F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>f : F.obj X ⟶ Y<VAR>e_4✝ : (𝟭 D).obj (F.obj X) = F.obj X<VAR>t : F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)<GOAL>F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>g : X ⟶ G.obj Y<GOAL>adj.unit.app X ≫ G.map (F.map g ≫ adj.counit.app Y) = g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>g : X ⟶ G.obj Y<GOAL>(𝟭 C).map g ≫ adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>g : X ⟶ G.obj Y<VAR>e_4✝ : (𝟭 C).obj (G.obj Y) = G.obj Y<GOAL>adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>g : X ⟶ G.obj Y<VAR>e_4✝ : (𝟭 C).obj (G.obj Y) = G.obj Y<VAR>t : (fun t => t.app Y) (whiskerLeft G adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G) = (fun t => t.app Y) (NatTrans.id (G ⋙ 𝟭 C))<GOAL>adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>g : X ⟶ G.obj Y<VAR>e_4✝ : (𝟭 C).obj (G.obj Y) = G.obj Y<VAR>t : adj.unit.app (G.obj Y) ≫ 𝟙 (G.obj (F.obj (G.obj Y))) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)<GOAL>adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>g : X ⟶ G.obj Y<VAR>e_4✝ : (𝟭 C).obj (G.obj Y) = G.obj Y<VAR>t : adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)<GOAL>adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<GOAL>QuotientAddGroup.mk '' Ioc a (a + p) = univ
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : TopologicalSpace 𝕜<VAR>inst✝¹ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝ : Archimedean 𝕜<GOAL>(range fun x => ↑↑x) = univ
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝ : Preorder α<VAR>f : ℤ → α<VAR>hf : Monotone f<VAR>n a : ℤ<VAR>h1 : f n < f a<VAR>h2 : f a < f (n + 1)<GOAL>False
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>Q : QuadraticMap R M N<VAR>inst✝ : Invertible 2<VAR>x y : M<GOAL>LinearMap.IsOrtho (associated Q) x y ↔ Q.IsOrtho x y
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} B<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>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>F₁ F₂ : B ⥤ C ⥤ D<VAR>h : uncurry.obj F₁ = uncurry.obj F₂<GOAL>F₁ = F₂
<VAR>c : Char<VAR>cs t : List Char<VAR>i : Nat<GOAL>go₂ (c :: cs ++ t) { byteIdx := i } { byteIdx := utf8Len (c :: cs) + i } = c :: cs
<VAR>c : Char<VAR>cs t : List Char<VAR>i : Nat<GOAL>go₂ (cs ++ t) { byteIdx := i + c.utf8Size } { byteIdx := utf8Len cs + c.utf8Size + i } = cs
<VAR>c : Char<VAR>cs t : List Char<VAR>i : Nat<GOAL>utf8Len cs + c.utf8Size + i = utf8Len cs + (i + c.utf8Size)
<VAR>op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}<VAR>a o : Ordinal.{u}<VAR>hao : a < o<VAR>H : IsNormal (op a)<VAR>ho : Principal op o<VAR>ho' : o.IsLimit<GOAL>op a o = o
<VAR>op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}<VAR>a o : Ordinal.{u}<VAR>hao : a < o<VAR>H : IsNormal (op a)<VAR>ho : Principal op o<VAR>ho' : o.IsLimit<GOAL>op a o ≤ o
<VAR>op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}<VAR>a o : Ordinal.{u}<VAR>hao : a < o<VAR>H : IsNormal (op a)<VAR>ho : Principal op o<VAR>ho' : o.IsLimit<GOAL>∀ i < o, op a i ≤ o
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range n, exp A ^ k = mk fun p => ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p !)⁻¹
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ x ∈ Finset.range n, { toFun := fun f => mk fun n => ↑x ^ n * (coeff A n) f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } (exp A) = mk fun p => ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p !)⁻¹
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n n✝ : ℕ<GOAL>(coeff A n✝) (∑ x ∈ Finset.range n, { toFun := fun f => mk fun n => ↑x ^ n * (coeff A n) f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } (exp A)) = (coeff A n✝) (mk fun p => ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p !)⁻¹)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : MulZeroClass α<VAR>s✝ t s : Finset α<GOAL>0 * s ⊆ 0
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝¹⁰ : LinearOrder ι<VAR>inst✝⁹ : LocallyFiniteOrder ι<VAR>inst✝⁸ : OrderBot ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : DiscreteTopology ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : SecondCountableTopology E<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n✝ : ι<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>n : ι<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>h_sf_min : SigmaFinite (μ.trim ⋯)<GOAL>(stoppedValue f fun x => min (σ x) (τ x)) =ᶠ[ae μ] μ[stoppedValue f τ|hσ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝¹⁰ : LinearOrder ι<VAR>inst✝⁹ : LocallyFiniteOrder ι<VAR>inst✝⁸ : OrderBot ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : DiscreteTopology ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : SecondCountableTopology E<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n✝ : ι<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>n : ι<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>h_sf_min : SigmaFinite (μ.trim ⋯)<GOAL>μ[stoppedValue f τ|⋯.measurableSpace] =ᶠ[ae μ] μ[stoppedValue f τ|hσ.measurableSpace]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝¹⁰ : LinearOrder ι<VAR>inst✝⁹ : LocallyFiniteOrder ι<VAR>inst✝⁸ : OrderBot ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : DiscreteTopology ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : SecondCountableTopology E<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n✝ : ι<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>n : ι<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>h_sf_min : SigmaFinite (μ.trim ⋯)<GOAL>∀ᵐ (x : Ω) ∂μ.restrict {x | σ x ≤ τ x}, (μ[stoppedValue f τ|⋯.measurableSpace]) x = (μ[stoppedValue f τ|hσ.measurableSpace]) x
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : CompleteSpace E<VAR>ι : Type u_3<VAR>inst✝¹⁰ : LinearOrder ι<VAR>inst✝⁹ : LocallyFiniteOrder ι<VAR>inst✝⁸ : OrderBot ι<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : DiscreteTopology ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : BorelSpace ι<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : SecondCountableTopology E<VAR>ℱ : Filtration ι m<VAR>τ σ : Ω → ι<VAR>f : ι → Ω → E<VAR>i n✝ : ι<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>h : Martingale f ℱ μ<VAR>hτ : IsStoppingTime ℱ τ<VAR>hσ : IsStoppingTime ℱ σ<VAR>n : ι<VAR>hτ_le : ∀ (x : Ω), τ x ≤ n<VAR>h_sf_min : SigmaFinite (μ.trim ⋯)<GOAL>∀ᵐ (x : Ω) ∂μ.restrict {x | σ x ≤ τ x}ᶜ, (μ[stoppedValue f τ|⋯.measurableSpace]) x = (μ[stoppedValue f τ|hσ.measurableSpace]) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝ : Ring α<VAR>h : Periodic f c<VAR>n : ℕ<GOAL>f (↑n * c - x) = f (-x)