ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K✝ : Type u_3<VAR>M✝ : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M✝<VAR>inst✝¹³ : Ring R<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>a b : R<VAR>x y : M✝<VAR>K : Type u_8<VAR>M : Type u_9<VAR>L : Type u_10<VAR>inst✝⁶ : CommRing K<VAR>inst✝⁵ : Semiring M<VAR>inst✝⁴ : Algebra K M<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : NoZeroSMulDivisors K L<GOAL>Injective fun r => r • 1
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K✝ : Type u_3<VAR>M✝ : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M✝<VAR>inst✝¹³ : Ring R<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>a b : R<VAR>x y : M✝<VAR>K : Type u_8<VAR>M : Type u_9<VAR>L : Type u_10<VAR>inst✝⁶ : CommRing K<VAR>inst✝⁵ : Semiring M<VAR>inst✝⁴ : Algebra K M<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : NoZeroSMulDivisors K L<GOAL>Injective fun r => (algebraMap K L) r
<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>a : α<VAR>ha : Tendsto (seq hf U_mem) atTop (𝓝 a)<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>m : ℕ<VAR>hm : U m ⊆ s<GOAL>∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (a, y) ∈ s ∧ y ∈ t
<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>a : α<VAR>ha : Tendsto (seq hf U_mem) atTop (𝓝 a)<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>m : ℕ<VAR>hm : U m ⊆ s<VAR>n : ℕ<VAR>hn : ∀ b ≥ n, seq hf U_mem b ∈ {y | (a, y) ∈ U m}<GOAL>∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (a, y) ∈ s ∧ y ∈ t
<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>a : α<VAR>ha : Tendsto (seq hf U_mem) atTop (𝓝 a)<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>m : ℕ<VAR>hm : U m ⊆ s<VAR>n : ℕ<VAR>hn : ∀ b ≥ n, seq hf U_mem b ∈ {y | (a, y) ∈ U m}<GOAL>setSeq hf U_mem (max m n) ×ˢ setSeq hf U_mem (max m n) ⊆ s
<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>a : α<VAR>ha : Tendsto (seq hf U_mem) atTop (𝓝 a)<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>m : ℕ<VAR>hm : U m ⊆ s<VAR>n : ℕ<VAR>hn : ∀ b ≥ n, seq hf U_mem b ∈ {y | (a, y) ∈ U m}<GOAL>(a, seq hf U_mem (max m n)) ∈ s
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>hunif : ¬G.IsUniform ε U V<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<GOAL>(1 - ε / 10) * ↑(G.nonuniformWitness ε U V).card ≤ ↑((star hP G ε hU V).biUnion id).card
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>hunif : ¬G.IsUniform ε U V<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hP₁ : 0 < P.parts.card<GOAL>(1 - ε / 10) * ↑(G.nonuniformWitness ε U V).card ≤ ↑((star hP G ε hU V).biUnion id).card
<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>A : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C✝<VAR>K✝ : GrothendieckTopology D✝<VAR>L : GrothendieckTopology A<VAR>G✝ : C✝ ⥤ D✝<VAR>hG : CompatiblePreserving K✝ G✝<VAR>ℱ✝ : SheafOfTypes K✝<VAR>Z✝ : C✝<VAR>T✝ : Presieve Z✝<VAR>x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝<VAR>h : x✝.Compatible<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} D<VAR>K : GrothendieckTopology D<VAR>G : C ⥤ D<VAR>inst✝ : RepresentablyFlat G<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>c : Cone (cospan g₁ g₂ ⋙ G) := (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)<VAR>c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) := IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)<GOAL>ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
<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>A : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C✝<VAR>K✝ : GrothendieckTopology D✝<VAR>L : GrothendieckTopology A<VAR>G✝ : C✝ ⥤ D✝<VAR>hG : CompatiblePreserving K✝ G✝<VAR>ℱ✝ : SheafOfTypes K✝<VAR>Z✝ : C✝<VAR>T✝ : Presieve Z✝<VAR>x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝<VAR>h : x✝.Compatible<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} D<VAR>K : GrothendieckTopology D<VAR>G : C ⥤ D<VAR>inst✝ : RepresentablyFlat G<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>c : Cone (cospan g₁ g₂ ⋙ G) := (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)<VAR>c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) := IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)<VAR>eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom ⋯<GOAL>ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
<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>A : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C✝<VAR>K✝ : GrothendieckTopology D✝<VAR>L : GrothendieckTopology A<VAR>G✝ : C✝ ⥤ D✝<VAR>hG : CompatiblePreserving K✝ G✝<VAR>ℱ✝ : SheafOfTypes K✝<VAR>Z✝ : C✝<VAR>T✝ : Presieve Z✝<VAR>x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝<VAR>h : x✝.Compatible<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} D<VAR>K : GrothendieckTopology D<VAR>G : C ⥤ D<VAR>inst✝ : RepresentablyFlat G<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>c : Cone (cospan g₁ g₂ ⋙ G) := (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)<VAR>c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) := IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)<VAR>eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom ⋯<VAR>eq₂ : f₂ = (c'.pt.hom ≫ G.map (c'.π.app right).right) ≫ eqToHom ⋯<GOAL>ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
<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>A : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C✝<VAR>K✝ : GrothendieckTopology D✝<VAR>L : GrothendieckTopology A<VAR>G✝ : C✝ ⥤ D✝<VAR>hG : CompatiblePreserving K✝ G✝<VAR>ℱ✝ : SheafOfTypes K✝<VAR>Z✝ : C✝<VAR>T✝ : Presieve Z✝<VAR>x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝<VAR>h : x✝.Compatible<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} D<VAR>K : GrothendieckTopology D<VAR>G : C ⥤ D<VAR>inst✝ : RepresentablyFlat G<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>c : Cone (cospan g₁ g₂ ⋙ G) := (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)<VAR>c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) := IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)<VAR>eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom ⋯<VAR>eq₂ : f₂ = (c'.pt.hom ≫ G.map (c'.π.app right).right) ≫ eqToHom ⋯<GOAL>ℱ.val.map ((c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom ⋯).op (x g₁ hg₁) = ℱ.val.map ((c'.pt.hom ≫ G.map (c'.π.app right).right) ≫ eqToHom ⋯).op (x g₂ hg₂)
<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>A : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C✝<VAR>K✝ : GrothendieckTopology D✝<VAR>L : GrothendieckTopology A<VAR>G✝ : C✝ ⥤ D✝<VAR>hG : CompatiblePreserving K✝ G✝<VAR>ℱ✝ : SheafOfTypes K✝<VAR>Z✝ : C✝<VAR>T✝ : Presieve Z✝<VAR>x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝<VAR>h : x✝.Compatible<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} D<VAR>K : GrothendieckTopology D<VAR>G : C ⥤ D<VAR>inst✝ : RepresentablyFlat G<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>c : Cone (cospan g₁ g₂ ⋙ G) := (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)<VAR>c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) := IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)<VAR>eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom ⋯<VAR>eq₂ : f₂ = (c'.pt.hom ≫ G.map (c'.π.app right).right) ≫ eqToHom ⋯<GOAL>ℱ.val.map c'.pt.hom.op (ℱ.val.map (G.map (c'.π.app left).right).op (eqToHom ⋯ (x g₁ hg₁))) = ℱ.val.map c'.pt.hom.op (ℱ.val.map (G.map (c'.π.app right).right).op (eqToHom ⋯ (x g₂ hg₂)))
<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>A : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C✝<VAR>K✝ : GrothendieckTopology D✝<VAR>L : GrothendieckTopology A<VAR>G✝ : C✝ ⥤ D✝<VAR>hG : CompatiblePreserving K✝ G✝<VAR>ℱ✝ : SheafOfTypes K✝<VAR>Z✝ : C✝<VAR>T✝ : Presieve Z✝<VAR>x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝<VAR>h : x✝.Compatible<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} D<VAR>K : GrothendieckTopology D<VAR>G : C ⥤ D<VAR>inst✝ : RepresentablyFlat G<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>c : Cone (cospan g₁ g₂ ⋙ G) := (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)<VAR>c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) := IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)<VAR>eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom ⋯<VAR>eq₂ : f₂ = (c'.pt.hom ≫ G.map (c'.π.app right).right) ≫ eqToHom ⋯<GOAL>ℱ.val.map (G.map (c'.π.app left).right).op (eqToHom ⋯ (x g₁ hg₁)) = ℱ.val.map (G.map (c'.π.app right).right).op (eqToHom ⋯ (x g₂ hg₂))
<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>A : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C✝<VAR>K✝ : GrothendieckTopology D✝<VAR>L : GrothendieckTopology A<VAR>G✝ : C✝ ⥤ D✝<VAR>hG : CompatiblePreserving K✝ G✝<VAR>ℱ✝ : SheafOfTypes K✝<VAR>Z✝ : C✝<VAR>T✝ : Presieve Z✝<VAR>x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝<VAR>h : x✝.Compatible<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} D<VAR>K : GrothendieckTopology D<VAR>G : C ⥤ D<VAR>inst✝ : RepresentablyFlat G<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>c : Cone (cospan g₁ g₂ ⋙ G) := (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)<VAR>c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) := IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)<VAR>eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom ⋯<VAR>eq₂ : f₂ = (c'.pt.hom ≫ G.map (c'.π.app right).right) ≫ eqToHom ⋯<VAR>left_eq✝ : (((Functor.const WalkingCospan).obj c'.pt).map Hom.inl).left ≫ (c'.π.app one).left = (c'.π.app left).left ≫ ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inl).left<VAR>e₁ : (((Functor.const WalkingCospan).obj c'.pt).map Hom.inl).right ≫ (c'.π.app one).right = (c'.π.app left).right ≫ ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inl).right<GOAL>ℱ.val.map (G.map (c'.π.app left).right).op (eqToHom ⋯ (x g₁ hg₁)) = ℱ.val.map (G.map (c'.π.app right).right).op (eqToHom ⋯ (x g₂ hg₂))
<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>A : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} A<VAR>J : GrothendieckTopology C✝<VAR>K✝ : GrothendieckTopology D✝<VAR>L : GrothendieckTopology A<VAR>G✝ : C✝ ⥤ D✝<VAR>hG : CompatiblePreserving K✝ G✝<VAR>ℱ✝ : SheafOfTypes K✝<VAR>Z✝ : C✝<VAR>T✝ : Presieve Z✝<VAR>x✝ : FamilyOfElements (G✝.op ⋙ ℱ✝.val) T✝<VAR>h : x✝.Compatible<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} D<VAR>K : GrothendieckTopology D<VAR>G : C ⥤ D<VAR>inst✝ : RepresentablyFlat G<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>c : Cone (cospan g₁ g₂ ⋙ G) := (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)<VAR>c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) := IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)<VAR>eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom ⋯<VAR>eq₂ : f₂ = (c'.pt.hom ≫ G.map (c'.π.app right).right) ≫ eqToHom ⋯<VAR>left_eq✝¹ : (((Functor.const WalkingCospan).obj c'.pt).map Hom.inl).left ≫ (c'.π.app one).left = (c'.π.app left).left ≫ ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inl).left<VAR>e₁ : (((Functor.const WalkingCospan).obj c'.pt).map Hom.inl).right ≫ (c'.π.app one).right = (c'.π.app left).right ≫ ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inl).right<VAR>left_eq✝ : (((Functor.const WalkingCospan).obj c'.pt).map Hom.inr).left ≫ (c'.π.app one).left = (c'.π.app right).left ≫ ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inr).left<VAR>e₂ : (((Functor.const WalkingCospan).obj c'.pt).map Hom.inr).right ≫ (c'.π.app one).right = (c'.π.app right).right ≫ ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).map Hom.inr).right<GOAL>ℱ.val.map (G.map (c'.π.app left).right).op (eqToHom ⋯ (x g₁ hg₁)) = ℱ.val.map (G.map (c'.π.app right).right).op (eqToHom ⋯ (x g₂ hg₂))
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>h : ∞ ∉ s<GOAL>IsOpen s ↔ IsOpen (some ⁻¹' s)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : (i : o) → DecidableEq (m' i)<VAR>d : (i : o) → m' i → α<VAR>i : o<VAR>k : m' i<VAR>j : o<VAR>k' : m' j<GOAL>blockDiagonal' (fun k => diagonal (d k)) ⟨i, k⟩ ⟨j, k'⟩ = diagonal (fun ik => d ik.fst ik.snd) ⟨i, k⟩ ⟨j, k'⟩
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : (i : o) → DecidableEq (m' i)<VAR>d : (i : o) → m' i → α<VAR>i : o<VAR>k : m' i<VAR>j : o<VAR>k' : m' j<GOAL>(if h : i = j then of (fun i_1 j => if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) = of (fun i j => if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨j, k'⟩
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : (i : o) → DecidableEq (m' i)<VAR>d : (i : o) → m' i → α<VAR>i : o<VAR>k k' : m' i<GOAL>(if h : i = i then of (fun i_1 j => if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) = of (fun i j => if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨i, k'⟩
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : (i : o) → DecidableEq (m' i)<VAR>d : (i : o) → m' i → α<VAR>i : o<VAR>k : m' i<VAR>j : o<VAR>k' : m' j<VAR>hij : i ≠ j<GOAL>(if h : i = j then of (fun i_1 j => if i_1 = j then d i i_1 else 0) k (cast ⋯ k') else 0) = of (fun i j => if i = j then d i.fst i.snd else 0) ⟨i, k⟩ ⟨j, k'⟩
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSpace Ω'<VAR>ν : ProbabilityMeasure Ω<VAR>f : Ω → Ω'<VAR>f_aemble : AEMeasurable f ↑ν<VAR>A : Set Ω'<VAR>A_mble : MeasurableSet A<GOAL>(ν.map f_aemble) A = ν (f ⁻¹' A)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSpace Ω'<VAR>ν : ProbabilityMeasure Ω<VAR>f : Ω → Ω'<VAR>f_aemble : AEMeasurable f ↑ν<VAR>A : Set Ω'<VAR>A_mble : MeasurableSet A<VAR>this : ↑(ν.map f_aemble) A = ↑ν (f ⁻¹' A)<GOAL>(ν.map f_aemble) A = ν (f ⁻¹' A)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : f ≈ 0<GOAL>(f * g).norm = f.norm * g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : f ≈ 0<VAR>hg : f * g ≈ 0<GOAL>(f * g).norm = f.norm * g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : g ≈ 0<GOAL>(f * g).norm = f.norm * g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf✝ : ¬f ≈ 0<VAR>hg : g ≈ 0<VAR>hf : f * g ≈ 0<GOAL>(f * g).norm = f.norm * g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : ¬f * g ≈ 0<GOAL>padicNorm p (↑(f * g) (stationaryPoint hfg)) = padicNorm p (↑f (stationaryPoint hf)) * padicNorm p (↑g (stationaryPoint hg))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : ¬f * g ≈ 0<GOAL>padicNorm p (↑(f * g) (max (stationaryPoint hfg) (max ?neg.v2✝ ?neg.v3✝))) = padicNorm p (↑f (max ?neg.v1✝ (max (stationaryPoint hf) ?neg.v3✝))) * padicNorm p (↑g (max ?neg.v1✝ (max ?neg.v2✝ (stationaryPoint hg))))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : ¬f * g ≈ 0<GOAL>ℕ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>y : M<VAR>hy : y ∈ f.source<GOAL>map (↑(f.extend I).symm) (𝓝[range ↑I] ↑(f.extend I) y) = 𝓝 y
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>A B : T.Algebra<VAR>f : A ⟶ B<VAR>inst✝ : IsIso f.f<GOAL>T.map (inv f.f) ≫ A.a = B.a ≫ inv f.f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>A B : T.Algebra<VAR>f : A ⟶ B<VAR>inst✝ : IsIso f.f<GOAL>T.map (inv f.f) ≫ T.map f.f ≫ B.a = B.a
<VAR>E✝ : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E✝<VAR>inst✝⁸ : NormedSpace ℝ E✝<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E✝<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>f✝ g : E✝ → G<VAR>C : ℝ<VAR>s : Set E✝<VAR>x✝ y✝ : E✝<VAR>f' g' : E✝ → E✝ →L[𝕜] G<VAR>φ : E✝ →L[𝕜] G<VAR>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : E → G<VAR>hf : Differentiable 𝕜 f<VAR>hf' : ∀ (x : E), fderiv 𝕜 f x = 0<VAR>x y : E<VAR>A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E<GOAL>f x = f y
<VAR>x : ℝ<VAR>h : cos x = 1<VAR>n : ℤ<VAR>hn : ↑n * π = x<VAR>hn0 : n % 2 = 0<GOAL>↑(n / 2) * (2 * π) = x
<VAR>x : ℝ<VAR>h : cos x = 1<VAR>n : ℤ<VAR>hn : ↑n * π = x<VAR>hn1 : n % 2 = 1<GOAL>↑(n / 2) * (2 * π) = x
<VAR>x : ℝ<VAR>h : cos x = 1<VAR>n : ℤ<VAR>hn : ↑(n / 2) * (2 * π) + π = x<VAR>hn1 : n % 2 = 1<GOAL>↑(n / 2) * (2 * π) = x
<VAR>x : ℝ<VAR>n : ℤ<VAR>h : -1 = 1<VAR>hn : ↑(n / 2) * (2 * π) + π = x<VAR>hn1 : n % 2 = 1<GOAL>↑(n / 2) * (2 * π) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g✝ : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T2Space γ<VAR>b : β<VAR>f : α → γ<VAR>g : β → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x<VAR>hg : ContinuousAt g b<GOAL>di.extend f b = g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g✝ : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T2Space γ<VAR>b : β<VAR>f : α → γ<VAR>g : β → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x<VAR>hg : ContinuousAt g b<VAR>s : Set γ<VAR>hs : s ∈ 𝓝 (g b)<GOAL>f ⁻¹' s ∈ comap i (𝓝 b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g✝ : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T2Space γ<VAR>b : β<VAR>f : α → γ<VAR>g : β → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x<VAR>hg : ContinuousAt g b<VAR>s : Set γ<VAR>hs : s ∈ 𝓝 (g b)<GOAL>∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s