ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>f : V ≃ₗᵢ[ℝ] V<VAR>hd : 0 < LinearMap.det ↑f.toLinearEquiv<VAR>this✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<VAR>this : o.oangle (o.rightAngleRotation x) (f (o.rightAngleRotation x)) = o.oangle x (f x)<GOAL>↑(o.rotation (o.oangle x (f x))).toLinearEquiv ((o.basisRightAngleRotation x hx) ⟨1, ⋯⟩) = ↑f.toLinearEquiv ((o.basisRightAngleRotation x hx) ⟨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✝² : InvolutiveInv G<VAR>inst✝¹ : MeasurableInv G<VAR>μ : Measure G<VAR>inst✝ : μ.IsInvInvariant<VAR>A : Set G<GOAL>μ A⁻¹ = μ A
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<GOAL>(cyclotomic n R).natDegree = n.totient
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<GOAL>WithBot.unbot' 0 ↑n.totient = n.totient
<VAR>n m : ℕ<VAR>i : Fin (n + 1)<VAR>h : i ≠ 0<VAR>h' : optParam (i.rev ≠ last n) ⋯<GOAL>(i.pred h).rev = i.rev.castPred h'
<VAR>S : Type u_1<VAR>inst✝ : Ring S<VAR>a b : ℕ<GOAL>↑(a.descFactorial 2) = ↑a * (↑a - 1)
<VAR>S : Type u_1<VAR>inst✝ : Ring S<VAR>a b : ℕ<GOAL>Polynomial.eval (↑(a - (2 - 1))) (ascPochhammer S 2) = ↑a * (↑a - 1)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w✝ : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>hf : ContinuousOn f (sphere z R)<VAR>hw : w ∈ ball z R<GOAL>Continuous (circleTransform R z w f)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w✝ : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>hf : ContinuousOn f (sphere z R)<VAR>hw : w ∈ ball z R<GOAL>Continuous (deriv (circleMap z R))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w✝ : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>hf : ContinuousOn f (sphere z R)<VAR>hw : w ∈ ball z R<GOAL>Continuous fun x => (circleMap z R x - w)⁻¹
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w✝ : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>hf : ContinuousOn f (sphere z R)<VAR>hw : w ∈ ball z R<GOAL>Continuous fun x => f (circleMap z R x)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>(N₁Γ₀.app K).inv = (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫ (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>((Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫ (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).inv = (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫ (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.L₀.Exact
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₀.X₂), x₂ ≫ S.L₀.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A : C<VAR>x₂ : A ⟶ S.L₀.X₂<VAR>hx₂ : x₂ ≫ S.L₀.g = 0<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A : C<VAR>x₂ : A ⟶ S.L₀.X₂<VAR>hx₂ : x₂ ≫ S.L₀.g = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>hπ₁ : Epi π₁<VAR>y₁ : A₁ ⟶ S.L₁.X₁<VAR>hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A : C<VAR>x₂ : A ⟶ S.L₀.X₂<VAR>hx₂ : x₂ ≫ S.L₀.g = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>hπ₁ : Epi π₁<VAR>y₁ : A₁ ⟶ S.L₁.X₁<VAR>hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f<VAR>hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A : C<VAR>x₂ : A ⟶ S.L₀.X₂<VAR>hx₂ : x₂ ≫ S.L₀.g = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>hπ₁ : Epi π₁<VAR>y₁ : A₁ ⟶ S.L₁.X₁<VAR>hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f<VAR>hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0<VAR>x₁ : A₁ ⟶ S.L₀.X₁<VAR>hx₁ : x₁ ≫ S.v₀₁.τ₁ = y₁<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₀.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A : C<VAR>x₂ : A ⟶ S.L₀.X₂<VAR>hx₂ : x₂ ≫ S.L₀.g = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>hπ₁ : Epi π₁<VAR>y₁ : A₁ ⟶ S.L₁.X₁<VAR>hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f<VAR>hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0<VAR>x₁ : A₁ ⟶ S.L₀.X₁<VAR>hx₁ : x₁ ≫ S.v₀₁.τ₁ = y₁<GOAL>π₁ ≫ x₂ = x₁ ≫ S.L₀.f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>l : ι →₀ R<VAR>i : ι<GOAL>(ε i) (lc e l) = l i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>l : ι →₀ R<VAR>i : ι<GOAL>(ε i) (l i • e i) = l i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>l : ι →₀ R<VAR>i : ι<GOAL>∀ (b : ι), l b ≠ 0 → b ≠ i → (ε i) (l b • e b) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>e : ι → M<VAR>ε : ι → Dual R M<VAR>inst✝ : DecidableEq ι<VAR>h : DualBases e ε<VAR>l : ι →₀ R<VAR>i : ι<GOAL>l i = 0 → (ε i) (0 • e i) = 0
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>f✝ : α✝ → β✝<VAR>α : Sort u<VAR>β : α → Sort v<VAR>f : (a : α) → β a<VAR>β' : α → Sort v<VAR>f' : (a : α) → β' a<VAR>h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')<VAR>this : ∀ (a : α), HEq (f a) (f' a)<GOAL>HEq f f'
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>f✝ : α✝ → β✝<VAR>α : Sort u<VAR>β : α → Sort v<VAR>f : (a : α) → β a<VAR>β' : α → Sort v<VAR>f' : (a : α) → β' a<VAR>h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')<VAR>this✝ : ∀ (a : α), HEq (f a) (f' a)<VAR>this : β = β'<GOAL>HEq f f'
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>f✝ : α✝ → β✝<VAR>α : Sort u<VAR>β : α → Sort v<VAR>f f' : (a : α) → β a<VAR>h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')<VAR>this : ∀ (a : α), HEq (f a) (f' a)<GOAL>HEq f f'
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>f✝ : α✝ → β✝<VAR>α : Sort u<VAR>β : α → Sort v<VAR>f f' : (a : α) → β a<VAR>h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')<VAR>this : ∀ (a : α), HEq (f a) (f' a)<GOAL>f = f'
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>f✝ : α✝ → β✝<VAR>α : Sort u<VAR>β : α → Sort v<VAR>f f' : (a : α) → β a<VAR>h : ∀ (a a' : α), HEq a a' → HEq (f a) (f' a')<VAR>this : ∀ (a : α), HEq (f a) (f' a)<VAR>a : α<GOAL>f a = f' a
<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✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>Y X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>f : Y ⟶ X<GOAL>(colimMap (J.diagramPullback P f) ≫ colimit.pre (J.diagram P Y) (J.pullback f).op) ((colimit.ι (J.diagram P X) (op S)) ((Meq.equiv P S).symm x)) = (colimit.ι (J.diagram P Y) (op (S.pullback f))) ((Meq.equiv P (S.pullback f)).symm (x.pullback f))
<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✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>Y X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>f : Y ⟶ X<GOAL>(colimit.ι (J.diagram P Y) ((J.pullback f).op.obj (op S))) (((J.diagramPullback P f).app (op S)) ((Meq.equiv P S).symm x)) = (colimit.ι (J.diagram P Y) (op (S.pullback f))) ((Meq.equiv P (S.pullback f)).symm (x.pullback f))
<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✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>Y X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>f : Y ⟶ X<GOAL>((J.diagramPullback P f).app (op S)) ((Meq.equiv P S).symm x) = (Meq.equiv P (S.pullback f)).symm (x.pullback f)
<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✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>Y X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>f : Y ⟶ X<GOAL>(Meq.equiv P (unop ((J.pullback f).op.obj (op S)))) (((J.diagramPullback P f).app (op S)) ((Meq.equiv P S).symm x)) = (Meq.equiv P (unop ((J.pullback f).op.obj (op S)))) ((Meq.equiv P (S.pullback f)).symm (x.pullback f))
<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✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>Y X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>f : Y ⟶ X<GOAL>(Meq.equiv P (unop ((J.pullback f).op.obj (op S)))) (((J.diagramPullback P f).app (op S)) ((Meq.equiv P S).symm x)) = x.pullback f
<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✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>Y X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>f : Y ⟶ X<VAR>i : (unop ((J.pullback f).op.obj (op S))).Arrow<GOAL>↑((Meq.equiv P (unop ((J.pullback f).op.obj (op S)))) (((J.diagramPullback P f).app (op S)) ((Meq.equiv P S).symm x))) i = ↑(x.pullback f) i
<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✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>Y X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>f : Y ⟶ X<VAR>i : (unop ((J.pullback f).op.obj (op S))).Arrow<GOAL>(Multiequalizer.ι ((S.pullback f).index P) i) ((Multiequalizer.lift ((S.pullback f).index P) (multiequalizer (S.index P)) (fun I => Multiequalizer.ι (S.index P) (Cover.Arrow.base I)) ⋯) ((Meq.equiv P S).symm x)) = ↑x { Y := i.Y, f := i.f ≫ f, hf := ⋯ }
<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✝³ : ConcreteCategory D<VAR>inst✝² : PreservesLimits (forget D)<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>Y X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x : Meq P S<VAR>f : Y ⟶ X<VAR>i : (unop ((J.pullback f).op.obj (op S))).Arrow<GOAL>↑x i.base = ↑x { Y := i.Y, f := i.f ≫ f, hf := ⋯ }
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DenselyOrdered α<GOAL>Ioo a b = 0 ↔ ¬a < b
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c : F<VAR>h0 : p ≠ 0<VAR>hμ : μ ≠ 0<VAR>h_top : ¬p = ⊤<GOAL>eLpNorm (fun x => c) p μ = ↑‖c‖₊ * μ Set.univ ^ (1 / p.toReal)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting<VAR>inst✝ : HasBinaryBiproducts C<VAR>n : ℤ<GOAL>((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.f ≫ (mappingConeHomOfDegreewiseSplitIso S σ).inv).f n = (-mappingCone.inr (homOfDegreewiseSplit S σ)).f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting<VAR>inst✝ : HasBinaryBiproducts C<VAR>n : ℤ<VAR>h : (S.map (eval C (ComplexShape.up ℤ) (n + 1))).f ≫ (σ (n + 1)).r = 𝟙 (S.map (eval C (ComplexShape.up ℤ) (n + 1))).X₁<GOAL>((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.f ≫ (mappingConeHomOfDegreewiseSplitIso S σ).inv).f n = (-mappingCone.inr (homOfDegreewiseSplit S σ)).f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting<VAR>inst✝ : HasBinaryBiproducts C<VAR>n : ℤ<VAR>h : S.f.f (n + 1) ≫ (σ (n + 1)).r = 𝟙 (S.X₁.X (n + 1))<GOAL>S.f.f (n + 1) ≫ (S.g.f (n + 1) ≫ (mappingCone.inl (homOfDegreewiseSplit S σ)).v (n + 1) n ⋯ - (σ (n + 1)).r ≫ 𝟙 (S.X₁.X (n + 1)) ≫ (mappingCone.inr (homOfDegreewiseSplit S σ)).f n) = -(mappingCone.inr (homOfDegreewiseSplit S σ)).f n
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>a b : ℝ<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in Ioi a, g (b * x) = b⁻¹ • ∫ (x : ℝ) in Ioi (b * a), g x
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>a b : ℝ<VAR>hb : 0 < b<VAR>this : ∀ (c : ℝ), MeasurableSet (Ioi c)<GOAL>∫ (x : ℝ) in Ioi a, g (b * x) = b⁻¹ • ∫ (x : ℝ) in Ioi (b * a), g x
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>a b : ℝ<VAR>hb : 0 < b<VAR>this : ∀ (c : ℝ), MeasurableSet (Ioi c)<GOAL>∫ (x : ℝ), (Ioi a).indicator (fun x => g (b * x)) x ∂volume = ∫ (x : ℝ), (Ioi (b * a)).indicator g (b * x)
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>a b : ℝ<VAR>hb : 0 < b<VAR>this : ∀ (c : ℝ), MeasurableSet (Ioi c)<VAR>x : ℝ<GOAL>(Ioi a).indicator (fun x => g (b * x)) x = (Ioi (b * a)).indicator g (b * x)
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>a b : ℝ<VAR>hb : 0 < b<VAR>this : ∀ (c : ℝ), MeasurableSet (Ioi c)<VAR>x : ℝ<GOAL>(Ioi a).indicator (fun x => g (b * x)) x = (Ioi a).indicator (g ∘ HMul.hMul b) x
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>hvw : G.Adj v w<GOAL>(G.subgraphOfAdj hvw).neighborSet u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅
<VAR>K✝ R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝³ : DivisionRing K✝<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>lift.{u, v} (Module.rank K V) < Module.rank K (V →ₗ[K] K)
<VAR>K✝ R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝³ : DivisionRing K✝<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>inst✝² : MeasurableSpace ι<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : ContinuousMul β<VAR>U : γ → ι → Ω → β<VAR>s : Finset γ<VAR>h : ∀ c ∈ s, ProgMeasurable f (U c)<GOAL>ProgMeasurable f fun i a => ∏ c ∈ s, U c i a
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>inst✝² : MeasurableSpace ι<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : ContinuousMul β<VAR>U : γ → ι → Ω → β<VAR>s : Finset γ<VAR>h : ∀ c ∈ s, ProgMeasurable f (U c)<GOAL>(fun i a => ∏ c ∈ s, U c i a) = ∏ c ∈ s, U c
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>inst✝² : MeasurableSpace ι<VAR>γ : Type u_4<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : ContinuousMul β<VAR>U : γ → ι → Ω → β<VAR>s : Finset γ<VAR>h : ∀ c ∈ s, ProgMeasurable f (U c)<VAR>i : ι<VAR>a : Ω<GOAL>∏ c ∈ s, U c i a = (∏ c ∈ s, U c) i a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : NormedSpace ℝ E<VAR>r : ℝ<VAR>x y : E<GOAL>⟪(r • x, y).1, (r • x, y).2⟫_𝕜 = r • ⟪(x, y).1, (x, y).2⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : NormedSpace ℝ E<VAR>r : ℝ<VAR>x y : E<GOAL>⟪(x, r • y).1, (x, r • y).2⟫_𝕜 = r • ⟪(x, y).1, (x, y).2⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : NormedSpace ℝ E<VAR>x y : E<GOAL>‖⟪(x, y).1, (x, y).2⟫_𝕜‖ ≤ 1 * ‖x‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : NormedSpace ℝ E<VAR>x y : E<GOAL>‖⟪(x, y).1, (x, y).2⟫_𝕜‖ ≤ ‖x‖ * ‖y‖
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulRightInvariant<GOAL>QuasiMeasurePreserving Inv.inv μ μ
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulRightInvariant<GOAL>QuasiMeasurePreserving Inv.inv μ.inv.inv μ.inv.inv
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : Ring R<GOAL>(cyclotomic n R).Monic
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : Ring R<GOAL>(map (Int.castRingHom R) (cyclotomic n ℤ)).Monic
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f✝ : α → M<VAR>δ : Type u_3<VAR>inst✝ : CommGroup δ<VAR>f : ℕ → δ<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>∏ k ∈ Ico m n, f k = (∏ k ∈ range n, f k) / ∏ k ∈ range m, f k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : AddCommMonoid P<VAR>F : Type u_13<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : AddMonoidHomClass F M N<VAR>f : M →+ N<VAR>a b : α →₀ M<GOAL>mapRange ⇑f ⋯ (a + b) = mapRange ⇑f ⋯ a + mapRange ⇑f ⋯ b
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>i : ι<VAR>r : A<VAR>x✝ : r ∈ ⊤<GOAL>↑(((decompose 𝒜) r) i) ∈ ⊤
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : dist p3 p1 = dist p3 p2<GOAL>∠ p3 (midpoint ℝ p1 p2) p2 = π / 2
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Free R M'<VAR>ι : Type w<GOAL>Module.rank R (ι →₀ R) = lift.{u, w} #ι
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Finset α<VAR>a b : α<GOAL>preimage 1 (fun x => x * b) ⋯ = {b⁻¹}
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>U : Set E<GOAL>IsOpen U ↔ ∀ x ∈ U, ∃ s, ∃ r > 0, (s.sup p).ball x r ⊆ U
<VAR>α : Type u_1<VAR>inst✝ : Semigroup α<VAR>s : Set α<VAR>a b : α<GOAL>op b • op a • s = op (a * b) • s
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>this : WfDvdMonoid R<GOAL>∃ n, Associated x (ϖ ^ n)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>this : WfDvdMonoid R<VAR>fx : Multiset R<VAR>hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x<GOAL>∃ n, Associated x (ϖ ^ n)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>this : WfDvdMonoid R<VAR>fx : Multiset R<VAR>hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x<GOAL>Associated x (ϖ ^ Multiset.card fx)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>this : WfDvdMonoid R<VAR>fx : Multiset R<VAR>hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x<VAR>H : Associated fx.prod x<GOAL>Associated x (ϖ ^ Multiset.card fx)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>this : WfDvdMonoid R<VAR>fx : Multiset R<VAR>hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x<VAR>H : Associates.mk fx.prod = Associates.mk x<GOAL>Associates.mk x = Associates.mk (ϖ ^ Multiset.card fx)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>this : WfDvdMonoid R<VAR>fx : Multiset R<VAR>hfx : (∀ b ∈ fx, Irreducible b) ∧ Associated fx.prod x<VAR>H : Associates.mk fx.prod = Associates.mk x<GOAL>(Multiset.map Associates.mk fx).prod = (Multiset.replicate (Multiset.card fx) (Associates.mk ϖ)).prod