ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>C' : Type ?u.94612<VAR>D : Type u_2<VAR>D' : Type ?u.94618<VAR>H : Type u_3<VAR>H' : Type ?u.94624<VAR>inst✝⁷ : Category.{u_4, u_1} C<VAR>inst✝⁶ : Category.{?u.94632, ?u.94612} C'<VAR>inst✝⁵ : Category.{u_5, u_2} D<VAR>inst✝⁴ : Category.{?u.94640, ?u.94618} D'<VAR>inst✝³ : Category.{u_6, u_3} H<VAR>inst✝² : Category.{?u.94648, ?u.94624} H'<VAR>RF RF' RF'' : D ⥤ H<VAR>F F' F'' : C ⥤ H<VAR>e : F ≅ F'<VAR>L : C ⥤ D<VAR>α : F ⟶ L ⋙ RF<VAR>α' : F' ⟶ L ⋙ RF'<VAR>α'' : F'' ⟶ L ⋙ RF''<VAR>α'₂ : F ⟶ L ⋙ RF'<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : RF.IsRightDerivedFunctor α W<GOAL>F.HasRightDerivedFunctor W
<VAR>C : Type u_1<VAR>C' : Type ?u.94612<VAR>D : Type u_2<VAR>D' : Type ?u.94618<VAR>H : Type u_3<VAR>H' : Type ?u.94624<VAR>inst✝⁷ : Category.{u_4, u_1} C<VAR>inst✝⁶ : Category.{?u.94632, ?u.94612} C'<VAR>inst✝⁵ : Category.{u_5, u_2} D<VAR>inst✝⁴ : Category.{?u.94640, ?u.94618} D'<VAR>inst✝³ : Category.{u_6, u_3} H<VAR>inst✝² : Category.{?u.94648, ?u.94624} H'<VAR>RF RF' RF'' : D ⥤ H<VAR>F F' F'' : C ⥤ H<VAR>e : F ≅ F'<VAR>L : C ⥤ D<VAR>α : F ⟶ L ⋙ RF<VAR>α' : F' ⟶ L ⋙ RF'<VAR>α'' : F'' ⟶ L ⋙ RF''<VAR>α'₂ : F ⟶ L ⋙ RF'<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : RF.IsRightDerivedFunctor α W<VAR>this : RF.IsLeftKanExtension α<GOAL>F.HasRightDerivedFunctor W
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H ≤ H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H ≤ H
<VAR>x y : PartENat<VAR>h : x < y + 1<GOAL>x ≤ y
<VAR>x : PartENat<VAR>h : x < ⊤ + 1<GOAL>x ≤ ⊤
<VAR>x : PartENat<VAR>n : ℕ<VAR>h : x < ↑n + 1<GOAL>x ≤ ↑n
<VAR>n m : ℕ<VAR>h : ↑m < ↑n + 1<GOAL>↑m ≤ ↑n
<VAR>n m : ℕ<VAR>h : ↑m < ↑n + 1<GOAL>m ≤ n
<VAR>n m : ℕ<VAR>h : ↑m < ↑n + 1<GOAL>m < n.succ
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Bool<VAR>l : List α<VAR>a : α<VAR>al : a ∈ l<VAR>pa : p a = true<GOAL>(eraseP p l).length + 1 = l.length
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>p : α → Bool<VAR>l : List α<VAR>a : α<VAR>al : a ∈ l<VAR>pa : p a = true<VAR>w✝ : α<VAR>l₁ l₂ : List α<VAR>left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true<VAR>left✝ : p w✝ = true<VAR>h₁ : l = l₁ ++ w✝ :: l₂<VAR>h₂ : eraseP p l = l₁ ++ l₂<GOAL>(eraseP p l).length + 1 = l.length
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>p : α → Bool<VAR>l : List α<VAR>a : α<VAR>al : a ∈ l<VAR>pa : p a = true<VAR>w✝ : α<VAR>l₁ l₂ : List α<VAR>left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true<VAR>left✝ : p w✝ = true<VAR>h₁ : l = l₁ ++ w✝ :: l₂<VAR>h₂ : eraseP p l = l₁ ++ l₂<GOAL>l₁.length + l₂.length + 1 = l₁.length + (w✝ :: l₂).length
<VAR>x y : ℝ<GOAL>rexp (x - y) = rexp x / rexp y
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<GOAL>order 1 = 0
<VAR>l : List Bool<VAR>hl : Chain' (fun x x_1 => x ≠ x_1) l<VAR>b : Bool<GOAL>l.length - 1 ≤ 2 * count b l
<VAR>l : List Bool<VAR>hl : Chain' (fun x x_1 => x ≠ x_1) l<VAR>b : Bool<GOAL>l.length - 1 ≤ if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>h : J(a | p) = -1<VAR>x y : ℤ<VAR>hxy : ↑p ∣ x ^ 2 - a * y ^ 2<GOAL>↑p ∣ x ∧ ↑p ∣ y
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M N : Bimod X Y<VAR>P Q : Bimod Y Z<VAR>f : M ⟶ N<VAR>g : P ⟶ Q<GOAL>(M.whiskerLeft g ≫ whiskerRight f Q).hom = (whiskerRight f P ≫ N.whiskerLeft g).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M N : Bimod X Y<VAR>P Q : Bimod Y Z<VAR>f : M ⟶ N<VAR>g : P ⟶ Q<GOAL>coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫ (M.whiskerLeft g ≫ whiskerRight f Q).hom = coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫ (whiskerRight f P ≫ N.whiskerLeft g).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M N : Bimod X Y<VAR>P Q : Bimod Y Z<VAR>f : M ⟶ N<VAR>g : P ⟶ Q<GOAL>coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫ colimMap (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) ((M.X ⊗ Y.X) ◁ g.hom) (M.X ◁ g.hom) ⋯ ⋯) ≫ colimMap (parallelPairHom (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) (f.hom ▷ Y.X ▷ Q.X) (f.hom ▷ Q.X) ⋯ ⋯) = coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫ colimMap (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯) ≫ colimMap (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) ((N.X ⊗ Y.X) ◁ g.hom) (N.X ◁ g.hom) ⋯ ⋯)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M N : Bimod X Y<VAR>P Q : Bimod Y Z<VAR>f : M ⟶ N<VAR>g : P ⟶ Q<GOAL>(M.X ◁ g.hom ≫ colimit.ι (parallelPair (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft)) WalkingParallelPair.one) ≫ colimMap (parallelPairHom (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) (f.hom ▷ Y.X ▷ Q.X) (f.hom ▷ Q.X) ⋯ ⋯) = coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫ colimMap (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯) ≫ colimMap (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) ((N.X ⊗ Y.X) ◁ g.hom) (N.X ◁ g.hom) ⋯ ⋯)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M N : Bimod X Y<VAR>P Q : Bimod Y Z<VAR>f : M ⟶ N<VAR>g : P ⟶ Q<GOAL>M.X ◁ g.hom ≫ f.hom ▷ Q.X ≫ colimit.ι (parallelPair (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one = coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫ colimMap (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯) ≫ colimMap (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) ((N.X ⊗ Y.X) ◁ g.hom) (N.X ◁ g.hom) ⋯ ⋯)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M N : Bimod X Y<VAR>P Q : Bimod Y Z<VAR>f : M ⟶ N<VAR>g : P ⟶ Q<GOAL>(f.hom ▷ P.X ≫ N.X ◁ g.hom) ≫ colimit.ι (parallelPair (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one = coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫ colimMap (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯) ≫ colimMap (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) ((N.X ⊗ Y.X) ◁ g.hom) (N.X ◁ g.hom) ⋯ ⋯)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M N : Bimod X Y<VAR>P Q : Bimod Y Z<VAR>f : M ⟶ N<VAR>g : P ⟶ Q<GOAL>(f.hom ▷ P.X ≫ N.X ◁ g.hom) ≫ colimit.ι (parallelPair (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one = (f.hom ▷ P.X ≫ colimit.ι (parallelPair (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) WalkingParallelPair.one) ≫ colimMap (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) ((N.X ⊗ Y.X) ◁ g.hom) (N.X ◁ g.hom) ⋯ ⋯)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M N : Bimod X Y<VAR>P Q : Bimod Y Z<VAR>f : M ⟶ N<VAR>g : P ⟶ Q<GOAL>(f.hom ▷ P.X ≫ N.X ◁ g.hom) ≫ colimit.ι (parallelPair (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one = f.hom ▷ P.X ≫ N.X ◁ g.hom ≫ colimit.ι (parallelPair (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>n : ℕ<GOAL>((expand R p) f).coeff (n * p) = f.coeff n
<VAR>x y : ℝ<GOAL>cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x
<VAR>x y : ℝ<GOAL>↑(cosh (3 * x)) = ↑(4 * cosh x ^ 3 - 3 * cosh x)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ✝<VAR>g : Ω → ℝ<VAR>μ : Measure Ω<VAR>hf : Martingale f ℱ μ<VAR>hg : Integrable g μ<VAR>hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)<VAR>n : ℕ<GOAL>f n =ᶠ[ae μ] μ[g|↑ℱ n]
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ✝<VAR>g : Ω → ℝ<VAR>μ : Measure Ω<VAR>hf : Martingale f ℱ μ<VAR>hg : Integrable g μ<VAR>hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)<VAR>n : ℕ<GOAL>eLpNorm (f n - μ[g|↑ℱ n]) 1 μ = 0
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ✝<VAR>g : Ω → ℝ<VAR>μ : Measure Ω<VAR>hf : Martingale f ℱ μ<VAR>hg : Integrable g μ<VAR>hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)<VAR>n : ℕ<VAR>ht : Tendsto (fun m => eLpNorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)<GOAL>eLpNorm (f n - μ[g|↑ℱ n]) 1 μ = 0
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ✝<VAR>g : Ω → ℝ<VAR>μ : Measure Ω<VAR>hf : Martingale f ℱ μ<VAR>hg : Integrable g μ<VAR>hgtends : Tendsto (fun n => eLpNorm (f n - g) 1 μ) atTop (𝓝 0)<VAR>n : ℕ<VAR>ht : Tendsto (fun m => eLpNorm (μ[f m - g|↑ℱ n]) 1 μ) atTop (𝓝 0)<VAR>hev : ∀ m ≥ n, eLpNorm (μ[f m - g|↑ℱ n]) 1 μ = eLpNorm (f n - μ[g|↑ℱ n]) 1 μ<GOAL>eLpNorm (f n - μ[g|↑ℱ n]) 1 μ = 0
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : CategoryWithHomology C<VAR>inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>K L : HomologicalComplex C c<VAR>f : { as := K } ⟶ { as := L }<GOAL>quasiIso C c f ↔ (HomologicalComplex.quasiIso C c).map (quotient C c) f
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : CategoryWithHomology C<VAR>inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<GOAL>quasiIso C c ((quotient C c).map f) ↔ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)
<VAR>α : Type u_1<VAR>s✝ t : Finset α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>s ⩿ insert a s
<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✝ : OrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s t : Finset ι<VAR>i j : ι<VAR>hij : j ≠ i<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hlt : 1 < f j<VAR>hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k<GOAL>f i = ∏ k ∈ {i}, f k
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>s : Set α<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>f : ↥(Lp E 2 μ)<GOAL>⟪indicatorConstLp 2 hs hμs c, f⟫_𝕜 = ⟪c, ∫ (x : α) in s, ↑↑f x ∂μ⟫_𝕜
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v x ≠ v y<GOAL>v (x + y) = max (v x) (v y)
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v x ≠ v y<GOAL>¬v (x + y) < max (v x) (v y)
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x✝ y✝ z x y : R<VAR>h : v x ≠ v y<VAR>h' : v (x + y) < max (v x) (v y)<VAR>vyx : v y < v x<GOAL>False
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x✝ y✝ z x y : R<VAR>h : v x ≠ v y<VAR>h' : v (x + y) < v x<VAR>vyx : v y < v x<GOAL>False
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x✝ y✝ z x y : R<VAR>h : v x ≠ v y<VAR>h' : v (x + y) < v x<VAR>vyx : v y < v x<GOAL>v x < v x
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁶ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : ChartedSpace H G<VAR>inst✝³ : Monoid G<VAR>inst✝² : SmoothMul I G<VAR>g h : G<VAR>M : Type u_5<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>x : M<VAR>r : 𝕜<VAR>X Y : LeftInvariantDerivation I G<VAR>f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<VAR>f : C^⊤⟮I, G; 𝕜⟯⟨g * h⟩<GOAL>((evalAt (g * h)) X) f = ((𝒅ₕ ⋯) ((evalAt h) X)) f
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁶ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : ChartedSpace H G<VAR>inst✝³ : Monoid G<VAR>inst✝² : SmoothMul I G<VAR>g h : G<VAR>M : Type u_5<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>x : M<VAR>r : 𝕜<VAR>X Y : LeftInvariantDerivation I G<VAR>f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<VAR>f : C^⊤⟮I, G; 𝕜⟯⟨g * h⟩<GOAL>((𝒅 (𝑳 I g) ((𝑳 I h) 1) ∘ₗ 𝒅 (𝑳 I h) 1) ((evalAt 1) X)) f = ((evalAt h) X) (ContMDiffMap.comp f (𝑳 I g))
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁶ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : ChartedSpace H G<VAR>inst✝³ : Monoid G<VAR>inst✝² : SmoothMul I G<VAR>g h : G<VAR>M : Type u_5<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>x : M<VAR>r : 𝕜<VAR>X Y : LeftInvariantDerivation I G<VAR>f✝ f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<VAR>f : C^⊤⟮I, G; 𝕜⟯⟨g * h⟩<GOAL>((𝒅 (𝑳 I g) ((𝑳 I h) 1)) ((𝒅 (𝑳 I h) 1) ((evalAt 1) X))) f = ((evalAt h) X) (ContMDiffMap.comp f (𝑳 I g))
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b c : α<VAR>u : αˣ<GOAL>↑(1 / u) = 1 /ₚ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<VAR>s₁ s₂ : Multiset α<VAR>t₁ t₂ : Multiset β<VAR>a : α<VAR>b : β<VAR>x : α ⊕ β<VAR>hs : s.Nodup<VAR>ht : t.Nodup<GOAL>(s.disjSum t).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<VAR>s₁ s₂ : Multiset α<VAR>t₁ t₂ : Multiset β<VAR>a : α<VAR>b : β<VAR>x✝ : α ⊕ β<VAR>hs✝ : s.Nodup<VAR>ht✝ : t.Nodup<VAR>x : α ⊕ β<VAR>hs : x ∈ Multiset.map inl s<VAR>ht : x ∈ Multiset.map inr t<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<VAR>s₁ s₂ : Multiset α<VAR>t₁ t₂ : Multiset β<VAR>a : α<VAR>b : β<VAR>x✝ : α ⊕ β<VAR>hs✝ : s.Nodup<VAR>ht✝ : t.Nodup<VAR>x : α ⊕ β<VAR>hs : ∃ a ∈ s, inl a = x<VAR>ht : ∃ a ∈ t, inr a = x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<VAR>s₁ s₂ : Multiset α<VAR>t₁ t₂ : Multiset β<VAR>a✝ : α<VAR>b✝ : β<VAR>x : α ⊕ β<VAR>hs : s.Nodup<VAR>ht : t.Nodup<VAR>a : α<VAR>left✝¹ : a ∈ s<VAR>b : β<VAR>left✝ : b ∈ t<VAR>h : inr b = inl a<GOAL>False
<VAR>n : ℕ<GOAL>toNatOrdinal ↑n = ↑n
<VAR>n : ℕ<GOAL>toNatOrdinal (toOrdinal ↑n) = ↑n
<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>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set X<GOAL>Continuous fun f => ∫ (x : X) in s, ↑↑f 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>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set X<VAR>this : Fact (1 ≤ 1)<GOAL>Continuous fun f => ∫ (x : X) in s, ↑↑f 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>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set X<VAR>this : Fact (1 ≤ 1)<VAR>h_comp : (fun f => ∫ (x : X) in s, ↑↑f x ∂μ) = integral (μ.restrict s) ∘ fun f => ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f)<GOAL>Continuous fun f => ∫ (x : X) in s, ↑↑f 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>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set X<VAR>this : Fact (1 ≤ 1)<VAR>h_comp : (fun f => ∫ (x : X) in s, ↑↑f x ∂μ) = integral (μ.restrict s) ∘ fun f => ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f)<GOAL>Continuous (integral (μ.restrict s) ∘ fun f => ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f))
<VAR>α : Type u_1<VAR>inst✝ : NormedAddCommGroup α<VAR>f : ℕ → α<VAR>g : ℕ → ℝ<VAR>h : f =o[atTop] g<VAR>hg : 0 ≤ g<VAR>h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop<GOAL>(fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, g i
<VAR>α : Type u_1<VAR>inst✝ : NormedAddCommGroup α<VAR>f : ℕ → α<VAR>g : ℕ → ℝ<VAR>h : f =o[atTop] g<VAR>hg : 0 ≤ g<VAR>h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop<VAR>A : ∀ (i : ℕ), ‖g i‖ = g i<GOAL>(fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, g i
<VAR>α : Type u_1<VAR>inst✝ : NormedAddCommGroup α<VAR>f : ℕ → α<VAR>g : ℕ → ℝ<VAR>h : f =o[atTop] g<VAR>hg : 0 ≤ g<VAR>h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop<VAR>A : ∀ (i : ℕ), ‖g i‖ = g i<VAR>B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i<GOAL>(fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, g i
<VAR>α : Type u_1<VAR>inst✝ : NormedAddCommGroup α<VAR>f : ℕ → α<VAR>g : ℕ → ℝ<VAR>h : f =o[atTop] g<VAR>hg : 0 ≤ g<VAR>h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop<VAR>A : ∀ (i : ℕ), ‖g i‖ = g i<VAR>B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i<GOAL>∀ (ε : ℝ), 0 < ε → ∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ range x, f i‖ ≤ ε * ‖∑ i ∈ range x, g i‖
<VAR>α : Type u_1<VAR>inst✝ : NormedAddCommGroup α<VAR>f : ℕ → α<VAR>g : ℕ → ℝ<VAR>h : f =o[atTop] g<VAR>hg : 0 ≤ g<VAR>h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop<VAR>A : ∀ (i : ℕ), ‖g i‖ = g i<VAR>B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ range x, f i‖ ≤ ε * ‖∑ i ∈ range x, g i‖
<VAR>α : Type u_1<VAR>inst✝ : NormedAddCommGroup α<VAR>f : ℕ → α<VAR>g : ℕ → ℝ<VAR>h : f =o[atTop] g<VAR>hg : 0 ≤ g<VAR>h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop<VAR>A : ∀ (i : ℕ), ‖g i‖ = g i<VAR>B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>N : ℕ<VAR>hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b<GOAL>∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ range x, f i‖ ≤ ε * ‖∑ i ∈ range x, g i‖
<VAR>α : Type u_1<VAR>inst✝ : NormedAddCommGroup α<VAR>f : ℕ → α<VAR>g : ℕ → ℝ<VAR>h : f =o[atTop] g<VAR>hg : 0 ≤ g<VAR>h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop<VAR>A : ∀ (i : ℕ), ‖g i‖ = g i<VAR>B : ∀ (n : ℕ), ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>N : ℕ<VAR>hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b<VAR>this : (fun x => ∑ i ∈ range N, f i) =o[atTop] fun n => ∑ i ∈ range n, g i<GOAL>∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ range x, f i‖ ≤ ε * ‖∑ i ∈ range x, g i‖