ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<VAR>inst✝ : S.HasHomology<GOAL>leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫ S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ = (leftHomologyMap' (𝟙 S) h₁ S.leftHomologyData ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData S.homologyData.left) ≫ (S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right S.rightHomologyData) ≫ rightHomologyMap' (𝟙 S) S.rightHomologyData h₂
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<GOAL>(τ * σ * τ⁻¹).cycleType = σ.cycleType
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>f : F' ⟶ F<VAR>hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ G.obj U<GOAL>∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y), F'.map f_1 ≫ (fun U x => ⟨f.app U x, ⋯⟩) Y = (fun U x => ⟨f.app U x, ⋯⟩) X ≫ G.toPresheaf.map f_1
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>f : F' ⟶ F<VAR>hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ G.obj U<VAR>this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : F'.obj X), f.app Y (F'.map f_1 x) = F.map f_1 (f.app X x)<GOAL>∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y), F'.map f_1 ≫ (fun U x => ⟨f.app U x, ⋯⟩) Y = (fun U x => ⟨f.app U x, ⋯⟩) X ≫ G.toPresheaf.map f_1
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>f : F' ⟶ F<VAR>hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ G.obj U<VAR>this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : F'.obj X), f.app Y (F'.map f_1 x) = F.map f_1 (f.app X x)<VAR>X✝ Y✝ : Cᵒᵖ<VAR>f✝ : X✝ ⟶ Y✝<GOAL>F'.map f✝ ≫ (fun U x => ⟨f.app U x, ⋯⟩) Y✝ = (fun U x => ⟨f.app U x, ⋯⟩) X✝ ≫ G.toPresheaf.map f✝
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>f : F' ⟶ F<VAR>hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ G.obj U<VAR>this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : F'.obj X), f.app Y (F'.map f_1 x) = F.map f_1 (f.app X x)<VAR>X✝ Y✝ : Cᵒᵖ<VAR>f✝ : X✝ ⟶ Y✝<VAR>x : F'.obj X✝<GOAL>↑((F'.map f✝ ≫ (fun U x => ⟨f.app U x, ⋯⟩) Y✝) x) = ↑(((fun U x => ⟨f.app U x, ⋯⟩) X✝ ≫ G.toPresheaf.map f✝) x)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>f : F' ⟶ F<VAR>hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ G.obj U<VAR>this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : F'.obj X), f.app Y (F'.map f_1 x) = F.map f_1 (f.app X x)<VAR>X✝ Y✝ : Cᵒᵖ<VAR>f✝ : X✝ ⟶ Y✝<VAR>x : F'.obj X✝<GOAL>f.app Y✝ (F'.map f✝ x) = ↑(G.toPresheaf.map f✝ ⟨f.app X✝ x, ⋯⟩)
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<GOAL>(x + y).leadingCoeff = x.leadingCoeff
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<VAR>hx : x ≠ 0<GOAL>(x + y).leadingCoeff = x.leadingCoeff
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<VAR>hx : x ≠ 0<VAR>ho : (x + y).orderTop = x.orderTop<GOAL>(x + y).leadingCoeff = x.leadingCoeff
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>X✝ Y✝ Z : C<VAR>inst✝¹ : HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>inst✝ : Mono i₃<GOAL>map f g f' g' i₁ i₂ i₃ e₁ e₂ = (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ fst (snd f' g') i₂
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPushout f.op g.op<GOAL>(PushoutCocone.unop (colimit.cocone (span f.op g.op))).π.app WalkingCospan.left = (pushout.inl f.op g.op).unop
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s<VAR>N m n : ℕ<VAR>hm : N ≤ m<VAR>hn : N ≤ n<VAR>p : α × α<VAR>hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n<GOAL>p ∈ U N
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s<VAR>N m n : ℕ<VAR>hm : N ≤ m<VAR>hn : N ≤ n<VAR>p : α × α<VAR>hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n<GOAL>p.1 ∈ setSeq hf U_mem N
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s<VAR>N m n : ℕ<VAR>hm : N ≤ m<VAR>hn : N ≤ n<VAR>p : α × α<VAR>hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n<GOAL>p.2 ∈ setSeq hf U_mem N
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>I : Type u_1<VAR>Y : I → C<VAR>hY : J.CoversTop Y<VAR>F : Sheaf J (Type u_2)<VAR>x y : ↑F.val.sections<VAR>h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))<VAR>W : Cᵒᵖ<GOAL>↑x W = ↑y W
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>I : Type u_1<VAR>Y : I → C<VAR>hY : J.CoversTop Y<VAR>F : Sheaf J (Type u_2)<VAR>x y : ↑F.val.sections<VAR>h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))<VAR>W : Cᵒᵖ<GOAL>∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Opposite.unop W⦄, (Sieve.ofObjects Y (Opposite.unop W)).arrows f → F.val.map f.op (↑x W) = F.val.map f.op (↑y W)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>i : ChooseBasisIndex ℤ ↥↑↑I<GOAL>(fractionalIdealLatticeBasis K I) i = (mixedEmbedding K) ((basisOfFractionalIdeal K I) i)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁴ : Category.{v', u'} D<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝³ : Category.{u_5, u_1} C₁<VAR>inst✝² : Category.{u_6, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>E₁ : Type u_3<VAR>E₂ : Type u_4<VAR>inst✝¹ : Category.{u_7, u_3} E₁<VAR>inst✝ : Category.{u_8, u_4} E₂<VAR>F₁ : C₁ ⥤ E₁<VAR>F₂ : C₂ ⥤ E₂<VAR>h₁ : W₁.IsInvertedBy F₁<VAR>h₂ : W₂.IsInvertedBy F₂<VAR>x✝¹ x✝ : C₁ × C₂<VAR>f : x✝¹ ⟶ x✝<VAR>hf : W₁.prod W₂ f<GOAL>IsIso ((F₁.prod F₂).map f)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁴ : Category.{v', u'} D<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝³ : Category.{u_5, u_1} C₁<VAR>inst✝² : Category.{u_6, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>E₁ : Type u_3<VAR>E₂ : Type u_4<VAR>inst✝¹ : Category.{u_7, u_3} E₁<VAR>inst✝ : Category.{u_8, u_4} E₂<VAR>F₁ : C₁ ⥤ E₁<VAR>F₂ : C₂ ⥤ E₂<VAR>h₁ : W₁.IsInvertedBy F₁<VAR>h₂ : W₂.IsInvertedBy F₂<VAR>x✝¹ x✝ : C₁ × C₂<VAR>f : x✝¹ ⟶ x✝<VAR>hf : W₁.prod W₂ f<GOAL>IsIso ((F₁.prod F₂).map f).1 ∧ IsIso ((F₁.prod F₂).map f).2
<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>X Y✝ Z : C<VAR>f✝ : Y✝ ⟶ X<VAR>ι : Type u_1<VAR>Y : ι → C<VAR>f : (i : ι) → Y i ⟶ X<VAR>i : ι<GOAL>∃ i_1, ∃ (h : Y i_1 = Y i), f i = eqToHom ⋯ ≫ f i_1
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : CommRing R<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsPrincipalIdealRing R<VAR>inst✝ : IsDomain R<VAR>r : R<GOAL>Associated (generator (Ideal.span {r})) r
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : CommRing R<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsPrincipalIdealRing R<VAR>inst✝ : IsDomain R<VAR>r : R<GOAL>Ideal.span {generator (Ideal.span {r})} = Ideal.span {r}
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x✝ : 𝕜<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformly f' g' l<VAR>hf : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x<VAR>hfg : ∀ (x : 𝕜), Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>x : 𝕜<GOAL>HasDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x✝ : 𝕜<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformly f' g' l<VAR>hf✝ : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x<VAR>hfg : ∀ (x : 𝕜), Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>x : 𝕜<VAR>hf : ∀ᶠ (n : ι) in l, ∀ x ∈ Set.univ, HasDerivAt (f n) (f' n x) x<GOAL>HasDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x✝ : 𝕜<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformly f' g' l<VAR>hf✝ : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x<VAR>hfg✝ : ∀ (x : 𝕜), Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>x : 𝕜<VAR>hf : ∀ᶠ (n : ι) in l, ∀ x ∈ Set.univ, HasDerivAt (f n) (f' n x) x<VAR>hfg : ∀ x ∈ Set.univ, Tendsto (fun n => f n x) l (𝓝 (g x))<GOAL>HasDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x✝ : 𝕜<VAR>inst✝ : l.NeBot<VAR>hf'✝ : TendstoUniformly f' g' l<VAR>hf✝ : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x<VAR>hfg✝ : ∀ (x : 𝕜), Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>x : 𝕜<VAR>hf : ∀ᶠ (n : ι) in l, ∀ x ∈ Set.univ, HasDerivAt (f n) (f' n x) x<VAR>hfg : ∀ x ∈ Set.univ, Tendsto (fun n => f n x) l (𝓝 (g x))<VAR>hf' : TendstoUniformlyOn f' g' l Set.univ<GOAL>HasDerivAt g (g' x) x
<VAR>m : ℕ<VAR>h : m ≠ 0<VAR>n : ℕ<GOAL>(m <<< n).size = m.size + n
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Lattice α<VAR>a b c d : α<GOAL>a ⊓ b = a ⊔ b ↔ a = b
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → β<GOAL>Bijective (map f) ↔ Bijective f
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>inst✝² : ∀ (i : ι), K.HasHomology i<VAR>inst✝¹ : ∀ (i : ι), L.HasHomology i<VAR>inst✝ : ∀ (i : ι), M.HasHomology i<VAR>hφ : QuasiIso φ<VAR>hφφ' : QuasiIso (φ ≫ φ')<GOAL>QuasiIso φ'
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>inst✝² : ∀ (i : ι), K.HasHomology i<VAR>inst✝¹ : ∀ (i : ι), L.HasHomology i<VAR>inst✝ : ∀ (i : ι), M.HasHomology i<VAR>hφ : QuasiIso φ<VAR>hφφ' : QuasiIso (φ ≫ φ')<GOAL>QuasiIso (φ ≫ φ')
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁵ : DivisionRing k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝¹ : CharZero k<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>h : s.card = n + 1<GOAL>∑ i : ι, centroidWeightsIndicator k s i = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁵ : DivisionRing k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝¹ : CharZero k<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>h : s.card = n + 1<GOAL>∑ i ∈ s, centroidWeights k s i = 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>u : Set M<VAR>hu : u ∈ 𝓝 1<GOAL>∃ V ∈ 𝓝 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
<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>u : Set M<VAR>hu : u ∈ 𝓝 1<VAR>W : Set M<VAR>W1 : W ∈ 𝓝 1<VAR>h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u<GOAL>∃ V ∈ 𝓝 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
<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>u : Set M<VAR>hu : u ∈ 𝓝 1<VAR>W : Set M<VAR>W1 : W ∈ 𝓝 1<VAR>h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u<VAR>V : Set M<VAR>V1 : V ∈ 𝓝 1<VAR>h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W<GOAL>∃ V ∈ 𝓝 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
<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>u : Set M<VAR>hu : u ∈ 𝓝 1<VAR>W : Set M<VAR>W1 : W ∈ 𝓝 1<VAR>h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u<VAR>V : Set M<VAR>V1 : V ∈ 𝓝 1<VAR>h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W<GOAL>∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
<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>u : Set M<VAR>hu : u ∈ 𝓝 1<VAR>W : Set M<VAR>W1 : W ∈ 𝓝 1<VAR>h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u<VAR>V : Set M<VAR>V1 : V ∈ 𝓝 1<VAR>h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W<VAR>v w s t : M<VAR>v_in : v ∈ V<VAR>w_in : w ∈ V<VAR>s_in : s ∈ V<VAR>t_in : t ∈ V<GOAL>v * w * s * t ∈ u
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : LinearOrderedRing α<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module α β<VAR>inst✝¹ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>inst✝ : Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f i • g (σ i) < ∑ i : ι, f i • g i ↔ ¬Monovary f (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✝¹ : Fintype ι<VAR>inst✝ : OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>hf : f ≤ 1<GOAL>∏ i : ι, f i < 1 ↔ f < 1
<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>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C<VAR>hfm : AEStronglyMeasurable f (μ.restrict s)<GOAL>‖∫ (x : X) in s, f x ∂μ‖ ≤ C * (μ s).toReal
<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>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C<VAR>hfm : AEStronglyMeasurable f (μ.restrict s)<GOAL>∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
<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>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C<VAR>hfm : AEStronglyMeasurable f (μ.restrict s)<VAR>A : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C<GOAL>∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
<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>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C<VAR>hfm : AEStronglyMeasurable f (μ.restrict s)<VAR>A : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C<VAR>B : MeasurableSet {x | ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C}<GOAL>∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
<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>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C<VAR>hfm : AEStronglyMeasurable f (μ.restrict s)<VAR>A : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C<VAR>B : MeasurableSet {x | ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C}<VAR>a✝¹ : X<VAR>h1 : f a✝¹ = AEStronglyMeasurable.mk f hfm a✝¹<VAR>a✝ : ‖AEStronglyMeasurable.mk f hfm a✝¹‖ ≤ C<GOAL>‖f a✝¹‖ ≤ C
<VAR>a b c d : ℝ≥0∞<VAR>r p q x : ℝ≥0<VAR>hx : ↑x ≠ 0<VAR>y : ℝ≥0<VAR>hy : 1 < ↑y<GOAL>∃ n, ↑x ∈ Ico (↑y ^ n) (↑y ^ (n + 1))
<VAR>a b c d : ℝ≥0∞<VAR>r p q x : ℝ≥0<VAR>hx : ↑x ≠ 0<VAR>y : ℝ≥0<VAR>hy : 1 < ↑y<VAR>A : y ≠ 0<GOAL>∃ n, ↑x ∈ Ico (↑y ^ n) (↑y ^ (n + 1))
<VAR>a b c d : ℝ≥0∞<VAR>r p q x : ℝ≥0<VAR>hx : ↑x ≠ 0<VAR>y : ℝ≥0<VAR>hy : 1 < ↑y<VAR>A : y ≠ 0<VAR>n : ℤ<VAR>hn : y ^ n ≤ x<VAR>h'n : x < y ^ (n + 1)<GOAL>∃ n, ↑x ∈ Ico (↑y ^ n) (↑y ^ (n + 1))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>H : J.OneHypercoverFamily<VAR>inst✝ : H.IsGenerating<VAR>P : Cᵒᵖ ⥤ A<VAR>hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))<VAR>X : C<VAR>S : Sieve X<VAR>E : J.OneHypercover X<VAR>hE : H E<VAR>le : E.sieve₀ ≤ S<VAR>F : Multifork (Cover.index ⟨S, ⋯⟩ P)<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<GOAL>lift hP hE le F ≫ P.map f.op = F.ι { Y := Y, f := f, hf := hf }
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>H : J.OneHypercoverFamily<VAR>inst✝ : H.IsGenerating<VAR>P : Cᵒᵖ ⥤ A<VAR>hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))<VAR>X : C<VAR>S : Sieve X<VAR>E : J.OneHypercover X<VAR>hE : H E<VAR>le : E.sieve₀ ≤ S<VAR>F : Multifork (Cover.index ⟨S, ⋯⟩ P)<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<GOAL>∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), (Sieve.pullback f E.sieve₀).arrows f_1 → (lift hP hE le F ≫ P.map f.op) ≫ P.map f_1.op = F.ι { Y := Y, f := f, hf := hf } ≫ P.map f_1.op
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>H : J.OneHypercoverFamily<VAR>inst✝ : H.IsGenerating<VAR>P : Cᵒᵖ ⥤ A<VAR>hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))<VAR>X : C<VAR>S : Sieve X<VAR>E : J.OneHypercover X<VAR>hE : H E<VAR>le : E.sieve₀ ≤ S<VAR>F : Multifork (Cover.index ⟨S, ⋯⟩ P)<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<VAR>Z : C<VAR>g : Z ⟶ Y<VAR>i : E.I₀<VAR>a : Z ⟶ E.X i<VAR>fac : a ≫ E.f i = g ≫ f<GOAL>(lift hP hE le F ≫ P.map f.op) ≫ P.map g.op = F.ι { Y := Y, f := f, hf := hf } ≫ P.map g.op
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>H : J.OneHypercoverFamily<VAR>inst✝ : H.IsGenerating<VAR>P : Cᵒᵖ ⥤ A<VAR>hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))<VAR>X : C<VAR>S : Sieve X<VAR>E : J.OneHypercover X<VAR>hE : H E<VAR>le : E.sieve₀ ≤ S<VAR>F : Multifork (Cover.index ⟨S, ⋯⟩ P)<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<VAR>Z : C<VAR>g : Z ⟶ Y<VAR>i : E.I₀<VAR>a : Z ⟶ E.X i<VAR>fac : a ≫ E.f i = g ≫ f<GOAL>F.ι { Y := E.X i, f := E.f i, hf := ⋯ } ≫ P.map a.op = F.ι { Y := Y, f := f, hf := hf } ≫ P.map g.op
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_3<VAR>D₂ : Type u_4<VAR>inst✝⁷ : Category.{u_8, u_1} C₁<VAR>inst✝⁶ : Category.{u_7, u_2} C₂<VAR>inst✝⁵ : Category.{u_6, u_3} D₁<VAR>inst✝⁴ : Category.{u_5, u_4} D₂<VAR>G : C₁ ⥤ C₂<VAR>F : C₂ ⥤ C₁<VAR>adj : G ⊣ F<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>G' : D₁ ⥤ D₂<VAR>F' : D₂ ⥤ D₁<VAR>inst✝¹ : CatCommSq G L₁ L₂ G'<VAR>inst✝ : CatCommSq F L₂ L₁ F'<VAR>X₂ : C₂<VAR>this : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := { iso' := CatCommSq.iso'.symm }<GOAL>(η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) = G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫ (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ k<VAR>ζ' : M<VAR>k' : ℕ<VAR>hζ : IsPrimitiveRoot ζ k<VAR>hζ' : IsPrimitiveRoot ζ' k'<VAR>hk : k ≠ 0<VAR>hk' : k' ≠ 0<GOAL>IsPrimitiveRoot (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k')) (k.lcm k')
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ k<VAR>ζ' : M<VAR>k' : ℕ<VAR>hζ : IsPrimitiveRoot ζ k<VAR>hζ' : IsPrimitiveRoot ζ' k'<VAR>hk : k ≠ 0<VAR>hk' : k' ≠ 0<GOAL>k.lcm k' = orderOf (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k'))
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ k<VAR>ζ' : M<VAR>k' : ℕ<VAR>hζ : IsPrimitiveRoot ζ k<VAR>hζ' : IsPrimitiveRoot ζ' k'<VAR>hk : k ≠ 0<VAR>hk' : k' ≠ 0<GOAL>k = orderOf ζ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ k<VAR>ζ' : M<VAR>k' : ℕ<VAR>hζ : IsPrimitiveRoot ζ k<VAR>hζ' : IsPrimitiveRoot ζ' k'<VAR>hk : k ≠ 0<VAR>hk' : k' ≠ 0<GOAL>k' = orderOf ζ'
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ k<VAR>ζ' : M<VAR>k' : ℕ<VAR>hζ : IsPrimitiveRoot ζ k<VAR>hζ' : IsPrimitiveRoot ζ' k'<VAR>hk : k ≠ 0<VAR>hk' : k' ≠ 0<GOAL>ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k') = ζ ^ (orderOf ζ / (orderOf ζ).factorizationLCMLeft (orderOf ζ')) * ζ' ^ (orderOf ζ' / (orderOf ζ).factorizationLCMRight (orderOf ζ'))
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ Ioo a b ↔ a < x ∧ x < b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>x : B<GOAL>(aeval x) (minpoly A pb.gen) = 0 ↔ (Equiv.refl B) x ∈ (minpoly A pb.gen).aroots B
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>x : B<GOAL>(aeval x) (minpoly A pb.gen) = 0 ↔ (aeval x) (map (algebraMap A B) (minpoly A pb.gen)) = 0