ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 ∈ Finset.univ, f i < 1
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.69351, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.69358, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.69365, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.72492, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : Aᵒᵖ<VAR>f : X ⟶ Y<VAR>U : Dᵒᵖ<VAR>x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.72492)).obj ℱ).obj X).obj U<GOAL>f.unop ≫ appHom (homOver α (unop X)) (unop U) x = appHom (homOver α (unop Y)) (unop U) (f.unop ≫ x)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.69351, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.69358, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.69365, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.72492, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : Aᵒᵖ<VAR>f : X ⟶ Y<VAR>U : Dᵒᵖ<VAR>x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.72492)).obj ℱ).obj X).obj U<GOAL>Sieve.coverByImage G (unop U) ∈ K.sieves (unop U)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.69351, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.69358, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.69365, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.72492, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : Aᵒᵖ<VAR>f : X ⟶ Y<VAR>U : Dᵒᵖ<VAR>x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.72492)).obj ℱ).obj X).obj U<GOAL>(pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x)).Compatible
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.69351, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.69358, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.69365, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.72492, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : Aᵒᵖ<VAR>f : X ⟶ Y<VAR>U : Dᵒᵖ<VAR>x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type ?u.72492)).obj ℱ).obj X).obj U<GOAL>(pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x)).IsAmalgamation (f.unop ≫ appHom (homOver α (unop X)) (unop U) x)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.69351, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.69358, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.69365, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.72492, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : Aᵒᵖ<VAR>f : X ⟶ Y<VAR>U : Dᵒᵖ<VAR>Y' : D<VAR>f' : Y' ⟶ unop U<VAR>hf' : (Sieve.coverByImage G (unop U)).arrows f'<VAR>x : unop X ⟶ ℱ.obj (op (unop U))<GOAL>(f.unop ≫ appHom (homOver α (unop X)) (unop U) x) ≫ ℱ'.val.map f'.op = (((f.unop ≫ x) ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1)) ≫ ℱ'.val.map (Nonempty.some hf').lift.op
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.69351, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.69358, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.69365, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.72492, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : Aᵒᵖ<VAR>f : X ⟶ Y<VAR>U : Dᵒᵖ<VAR>Y' : D<VAR>f' : Y' ⟶ unop U<VAR>hf' : (Sieve.coverByImage G (unop U)).arrows f'<VAR>x : unop X ⟶ ℱ.obj (op (unop U))<GOAL>f.unop ≫ appHom (homOver α (unop X)) (unop U) x ≫ ℱ'.val.map f'.op = f.unop ≫ x ≫ ℱ.map (Nonempty.some hf').map.op ≫ α.app (op (Nonempty.some hf').1) ≫ ℱ'.val.map (Nonempty.some hf').lift.op
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.69351, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.69358, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.69365, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.72492, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : Aᵒᵖ<VAR>f : X ⟶ Y<VAR>U : Dᵒᵖ<VAR>Y' : D<VAR>f' : Y' ⟶ unop U<VAR>hf' : (Sieve.coverByImage G (unop U)).arrows f'<VAR>x : unop X ⟶ ℱ.obj (op (unop U))<GOAL>appHom (homOver α (unop X)) (unop U) x ≫ ℱ'.val.map f'.op = x ≫ ℱ.map (Nonempty.some hf').map.op ≫ α.app (op (Nonempty.some hf').1) ≫ ℱ'.val.map (Nonempty.some hf').lift.op
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.69351, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.69358, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.69365, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.72492, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : Aᵒᵖ<VAR>f : X ⟶ Y<VAR>U : Dᵒᵖ<VAR>Y' : D<VAR>f' : Y' ⟶ unop U<VAR>hf' : (Sieve.coverByImage G (unop U)).arrows f'<VAR>x : unop X ⟶ ℱ.obj (op (unop U))<GOAL>appHom (homOver α (unop X)) (unop U) x ≫ ℱ'.val.map ((Nonempty.some hf').lift ≫ (Nonempty.some hf').map).op = x ≫ ℱ.map (Nonempty.some hf').map.op ≫ α.app (op (Nonempty.some hf').1) ≫ ℱ'.val.map (Nonempty.some hf').lift.op
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.69351, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.69358, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.69365, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.72492, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : Aᵒᵖ<VAR>f : X ⟶ Y<VAR>U : Dᵒᵖ<VAR>Y' : D<VAR>f' : Y' ⟶ unop U<VAR>hf' : (Sieve.coverByImage G (unop U)).arrows f'<VAR>x : unop X ⟶ ℱ.obj (op (unop U))<GOAL>(appHom (homOver α (unop X)) (unop U) x ≫ ℱ'.val.map (Nonempty.some hf').map.op) ≫ ℱ'.val.map (Nonempty.some hf').lift.op = ((x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1)) ≫ ℱ'.val.map (Nonempty.some hf').lift.op
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.69351, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.69358, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.69365, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.72492, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : Aᵒᵖ<VAR>f : X ⟶ Y<VAR>U : Dᵒᵖ<VAR>Y' : D<VAR>f' : Y' ⟶ unop U<VAR>hf' : (Sieve.coverByImage G (unop U)).arrows f'<VAR>x : unop X ⟶ ℱ.obj (op (unop U))<GOAL>appHom (homOver α (unop X)) (unop U) x ≫ ℱ'.val.map (Nonempty.some hf').map.op = (x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>↑(yn a1 (n + 2)) + ↑(yn a1 n) = ↑(2 * a) * ↑(yn a1 (n + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : BooleanRing α<VAR>inst✝¹ : BooleanRing β<VAR>inst✝ : BooleanRing γ<VAR>a b : AsBoolAlg α<GOAL>ofBoolAlg (a ∆ b) = ofBoolAlg a + ofBoolAlg b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : BooleanRing α<VAR>inst✝¹ : BooleanRing β<VAR>inst✝ : BooleanRing γ<VAR>a b : AsBoolAlg α<GOAL>ofBoolAlg ((a ⊔ b) \ (a ⊓ b)) = ofBoolAlg a + ofBoolAlg b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m✝ n : ℕ<VAR>h : IsPeriodicPt f n x<VAR>m : ℕ<GOAL>f^[m % n] x = f^[m] x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>inst✝ : Field k<VAR>φ ψ : MvPowerSeries σ k<VAR>h : (constantCoeff σ k) ψ ≠ 0<GOAL>ψ⁻¹ = φ ↔ φ * ψ = 1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>s : Set (α → β)<VAR>hc : ∀ f ∈ s, Continuous' f<GOAL>Continuous' (sSup s)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>s : Set (α →o β)<VAR>hc : ∀ f ∈ DFunLike.coe '' s, Continuous' f<GOAL>Continuous' (sSup (DFunLike.coe '' s))
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>s : Set (α →o β)<VAR>hc : ∀ ⦃x : α →o β⦄, x ∈ s → Continuous x<GOAL>Continuous' (sSup (DFunLike.coe '' s))
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>s : Set (α →o β)<VAR>hc : ∀ ⦃x : α →o β⦄, x ∈ s → Continuous x<GOAL>Continuous' (⨆ a ∈ s, ⇑a)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : CompleteLattice β<VAR>s : Set (α →o β)<VAR>hc : ∀ ⦃x : α →o β⦄, x ∈ s → Continuous x<GOAL>Continuous (⨆ i ∈ s, i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>Ms : ι → Type u_3<VAR>inst✝⁷ : (i : ι) → AddCommGroup (Ms i)<VAR>inst✝⁶ : (i : ι) → Module R (Ms i)<VAR>N : Type u_4<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>Ns : ι → Type u_5<VAR>inst✝³ : (i : ι) → AddCommGroup (Ns i)<VAR>inst✝² : (i : ι) → Module R (Ns i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>q : Submodule R N<VAR>f : (i : ι) → Ms i →ₗ[R] N<VAR>hf : ∀ (i : ι), p i ≤ comap (f i) q<VAR>x : (i : ι) → Ms i<GOAL>((piQuotientLift p q f hf) fun i => Quotient.mk (x i)) = Quotient.mk (((lsum R Ms R) f) x)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>Ms : ι → Type u_3<VAR>inst✝⁷ : (i : ι) → AddCommGroup (Ms i)<VAR>inst✝⁶ : (i : ι) → Module R (Ms i)<VAR>N : Type u_4<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>Ns : ι → Type u_5<VAR>inst✝³ : (i : ι) → AddCommGroup (Ns i)<VAR>inst✝² : (i : ι) → Module R (Ns i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>q : Submodule R N<VAR>f : (i : ι) → Ms i →ₗ[R] N<VAR>hf : ∀ (i : ι), p i ≤ comap (f i) q<VAR>x : (i : ι) → Ms i<GOAL>(∑ d : ι, ((p d).mapQ q (f d) ⋯ ∘ₗ proj d) fun i => Quotient.mk (x i)) = ∑ x_1 : ι, q.mkQ ((f x_1 ∘ₗ proj x_1) x)
<VAR>n : ℕ<GOAL>n.succ.primesBelow = if Prime n then insert n n.primesBelow else n.primesBelow
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set R<VAR>x : PrimeSpectrum R<GOAL>x ∈ zeroLocus ↑(Ideal.span s) ↔ x ∈ zeroLocus s
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a b c g h✝ x : G₀<VAR>h : x ≠ 0<VAR>y y' : G₀<VAR>w : (fun y => y * x) y = (fun y => y * x) y'<GOAL>y = y'
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝ : LocallyConnectedSpace α<VAR>F : Set α<VAR>x : α<VAR>h : F ∈ 𝓝 x<GOAL>connectedComponentIn F x ∈ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝ : LocallyConnectedSpace α<VAR>F : Set α<VAR>x : α<VAR>h : ∃ i, (IsOpen i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ F<GOAL>connectedComponentIn F x ∈ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : LocallyConnectedSpace α<VAR>F : Set α<VAR>x : α<VAR>s : Set α<VAR>hsF : id s ⊆ F<VAR>h1s : IsOpen s<VAR>hxs : x ∈ s<VAR>h2s : IsConnected s<GOAL>connectedComponentIn F x ∈ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>f : α ≃. β<VAR>x✝ : α<VAR>a✝ : β<GOAL>a✝ ∈ f x✝ ↔ a✝ ∈ f x✝
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : ModuleCat R<GOAL>(α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : ModuleCat R<GOAL>∀ (x : ↑X) (y : ↑Y) (z : ↑Z), ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : Filter X<GOAL>Disjoint (cocompact X) f ↔ ∃ K ∈ f, IsCompact K
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : Filter X<GOAL>(∃ i, IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedAddCommGroup E'<VAR>inst✝¹² : NormedAddCommGroup E''<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>inst✝⁷ : NormedSpace 𝕜 E''<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : MeasurableNeg G<VAR>inst✝² : μ.IsAddLeftInvariant<VAR>inst✝¹ : MeasurableAdd₂ G<VAR>inst✝ : SFinite μ<VAR>x₀ : G<VAR>s : Set G<VAR>hbg : BddAbove ((fun i => ‖g i‖) '' ((fun t => x₀ - t) ⁻¹' s))<VAR>hs : MeasurableSet s<VAR>h2s : (support fun t => (L (f t)) (g (x₀ - t))) ⊆ s<VAR>hf : IntegrableOn f s μ<VAR>hmg : AEStronglyMeasurable g μ<GOAL>ConvolutionExistsAt f g x₀ L μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedAddCommGroup E'<VAR>inst✝¹² : NormedAddCommGroup E''<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>inst✝⁷ : NormedSpace 𝕜 E''<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : MeasurableNeg G<VAR>inst✝² : μ.IsAddLeftInvariant<VAR>inst✝¹ : MeasurableAdd₂ G<VAR>inst✝ : SFinite μ<VAR>x₀ : G<VAR>s : Set G<VAR>hbg : BddAbove ((fun i => ‖g i‖) '' ((fun t => x₀ - t) ⁻¹' s))<VAR>hs : MeasurableSet s<VAR>h2s : (support fun t => (L (f t)) (g (x₀ - t))) ⊆ s<VAR>hf : IntegrableOn f s μ<VAR>hmg : AEStronglyMeasurable g μ<GOAL>BddAbove ((fun i => ‖g i‖) '' ((fun t => -t + x₀) ⁻¹' s))
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedAddCommGroup E'<VAR>inst✝¹² : NormedAddCommGroup E''<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>inst✝⁷ : NormedSpace 𝕜 E''<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : MeasurableNeg G<VAR>inst✝² : μ.IsAddLeftInvariant<VAR>inst✝¹ : MeasurableAdd₂ G<VAR>inst✝ : SFinite μ<VAR>x₀ : G<VAR>s : Set G<VAR>hbg : BddAbove ((fun i => ‖g i‖) '' ((fun t => x₀ - t) ⁻¹' s))<VAR>hs : MeasurableSet s<VAR>h2s : (support fun t => (L (f t)) (g (x₀ - t))) ⊆ s<VAR>hf : IntegrableOn f s μ<VAR>hmg : AEStronglyMeasurable g μ<GOAL>AEStronglyMeasurable g (Measure.map (fun t => x₀ - t) (μ.restrict s))
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<VAR>s : Set α<GOAL>Metric.diam (f '' s) = Metric.diam s
<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>p₁ p₂ : P<VAR>h : p₁ ≠ p₂<GOAL>AffineIndependent k ![p₁, p₂]
<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>p₁ p₂ : P<VAR>h : p₁ ≠ p₂<GOAL>LinearIndependent k fun i => ![p₁, p₂] ↑i -ᵥ ![p₁, p₂] 0
<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>p₁ p₂ : P<VAR>h : p₁ ≠ p₂<VAR>i₁ : { x // x ≠ 0 } := ⟨1, ⋯⟩<VAR>he' : ∀ (i : { x // x ≠ 0 }), i = i₁<VAR>this : Unique { x // x ≠ 0 }<GOAL>![p₁, p₂] ↑i₁ -ᵥ ![p₁, p₂] 0 ≠ 0
<VAR>x : PartENat<GOAL>x ≠ ⊤ ↔ ∃ n, x = ↑n
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>I J K L : Ideal R<VAR>inst✝ : IsDomain R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>I * span {x} = J * span {x} ↔ I = J
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y L : R<GOAL>C (eval (C L * (X - C x) + C y) (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆))) = (Y - C (C L * (X - C x) + C y)) * (-Y - C (C W.a₁ * X + C W.a₃) - C (C L * (X - C x) + C y)) + (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y L : R<GOAL>C ((C L * (X - C x) + C y) ^ 2 + (C W.a₁ * X + C W.a₃) * (C L * (X - C x) + C y) - (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) = (Y - C (C L * (X - C x) + C y)) * (-Y - C (C W.a₁ * X + C W.a₃) - C (C L * (X - C x) + C y)) + (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y L : R<GOAL>(C (C L) * (C X - C (C x)) + C (C y)) ^ 2 + (C (C W.a₁) * C X + C (C W.a₃)) * (C (C L) * (C X - C (C x)) + C (C y)) - (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆)) = (Y - (C (C L) * (C X - C (C x)) + C (C y))) * (-Y - (C (C W.a₁) * C X + C (C W.a₃)) - (C (C L) * (C X - C (C x)) + C (C y))) + (Y ^ 2 + (C (C W.a₁) * C X + C (C W.a₃)) * Y - (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆)))
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>x : E<GOAL>(𝓝 x).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y / x‖ < ε}
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>x : E<GOAL>(𝓝 x).HasBasis (fun ε => 0 < ε) fun ε => ball x ε
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{u_1, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{u_2, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>W : D<VAR>h : F.obj Z ⟶ W<GOAL>F.map (f ≫ g) ≫ h = F.map f ≫ F.map g ≫ h
<VAR>β : Type v<VAR>inst✝ : NormedField β<VAR>f : CauSeq β norm<GOAL>CauchySeq ↑f
<VAR>β : Type v<VAR>inst✝ : NormedField β<VAR>f : CauSeq β norm<VAR>s : Set (β × β)<VAR>hs : s ∈ uniformity β<GOAL>∃ t ∈ map (↑f) atTop, t ×ˢ t ⊆ s
<VAR>β : Type v<VAR>inst✝ : NormedField β<VAR>f : CauSeq β norm<VAR>s : Set (β × β)<VAR>hs : s ∈ uniformity β<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s<GOAL>∃ t ∈ map (↑f) atTop, t ×ˢ t ⊆ s
<VAR>β : Type v<VAR>inst✝ : NormedField β<VAR>f : CauSeq β norm<VAR>s : Set (β × β)<VAR>hs : s ∈ uniformity β<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε<GOAL>∃ t ∈ map (↑f) atTop, t ×ˢ t ⊆ s
<VAR>β : Type v<VAR>inst✝ : NormedField β<VAR>f : CauSeq β norm<VAR>s : Set (β × β)<VAR>hs : s ∈ uniformity β<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε<GOAL>↑f '' {n | n ≥ N} ∈ map (↑f) atTop ∧ (↑f '' {n | n ≥ N}) ×ˢ (↑f '' {n | n ≥ N}) ⊆ s
<VAR>β : Type v<VAR>inst✝ : NormedField β<VAR>f : CauSeq β norm<VAR>s : Set (β × β)<VAR>hs : s ∈ uniformity β<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε<GOAL>(∃ a, ∀ b ≥ a, b ∈ ↑f ⁻¹' (↑f '' {n | n ≥ N})) ∧ (↑f '' {n | n ≥ N}) ×ˢ (↑f '' {n | n ≥ N}) ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : NormedDivisionRing α<VAR>inst✝² : SeminormedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : BoundedSMul α β<VAR>s : α<VAR>x y : β<GOAL>dist (s • x) (s • y) = ‖s‖ * dist x y
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>V : Type u_3<VAR>inst✝⁴ : Fintype K<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Fintype V<VAR>b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex K V } K V := IsNoetherian.finsetBasis K V<GOAL>Fintype.card V = q ^ FiniteDimensional.finrank K V
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIocDiv hp a (m • p + b) = m + toIocDiv hp a b
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some '' Ioc a b = Ioc ↑a ↑b
<VAR>y z : ℤ<VAR>h : PythagoreanTriple 0 y z<VAR>hc : Nat.gcd 0 y.natAbs = 1<GOAL>h.IsPrimitiveClassified
<VAR>y z : ℤ<VAR>h : PythagoreanTriple 0 y z<VAR>hc : y.natAbs = 1<GOAL>h.IsPrimitiveClassified
<VAR>y z : ℤ<VAR>h : PythagoreanTriple 0 y z<VAR>hc : y.natAbs = 1<VAR>hy : y = ↑y.natAbs<GOAL>h.IsPrimitiveClassified
<VAR>y z : ℤ<VAR>h : PythagoreanTriple 0 y z<VAR>hc : y.natAbs = 1<VAR>hy : y = -↑y.natAbs<GOAL>h.IsPrimitiveClassified
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hn : n ≠ 0<VAR>h : m % n = m<GOAL>m % n < n
<VAR>R : Type u<VAR>S : Type u_1<VAR>A : Type v<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Ring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S A<VAR>inst✝² : IsScalarTower R S A<VAR>B : Type u_2<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>a : A<VAR>h : IsAlgebraic R a<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>ha : (aeval a) p = 0<GOAL>(aeval (f a)) p = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)<VAR>inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)<VAR>inst✝⁴ : AddCommMonoid P<VAR>inst✝³ : (i : ι) → Module R (Mᵢ i)<VAR>inst✝² : (i : ι) → Module R (Nᵢ i)<VAR>inst✝¹ : Module R P<VAR>inst✝ : Fintype ι<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<VAR>h : (pi Q).Anisotropic<GOAL>∀ (i : ι), (Q i).Anisotropic
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (Mᵢ i)<VAR>inst✝⁵ : (i : ι) → AddCommMonoid (Nᵢ i)<VAR>inst✝⁴ : AddCommMonoid P<VAR>inst✝³ : (i : ι) → Module R (Mᵢ i)<VAR>inst✝² : (i : ι) → Module R (Nᵢ i)<VAR>inst✝¹ : Module R P<VAR>inst✝ : Fintype ι<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<VAR>h : ∀ (x : (i : ι) → Mᵢ i), ∑ i : ι, (Q i) (x i) = 0 → ∀ (a : ι), x a = 0<GOAL>∀ (i : ι), (Q i).Anisotropic