ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>D : GlueData<GOAL>Sieve.generate (Presieve.ofArrows D.openCover.obj D.openCover.map) ≤ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.sieve₀
<VAR>D : GlueData<GOAL>Presieve.ofArrows D.openCover.obj D.openCover.map ≤ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.sieve₀.arrows
<VAR>D : GlueData<VAR>i₁ i₂ : { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.I₀<VAR>W : Scheme<VAR>p₁ : W ⟶ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.X i₁<VAR>p₂ : W ⟶ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.X i₂<VAR>fac : p₁ ≫ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.f i₁ = p₂ ≫ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.f i₂<GOAL>{ I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.sieve₁ p₁ p₂ ∈ zariskiTopology.sieves W
<VAR>D : GlueData<VAR>i₁ i₂ : { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.I₀<VAR>W : Scheme<VAR>p₁ : W ⟶ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.X i₁<VAR>p₂ : W ⟶ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.X i₂<VAR>fac : p₁ ≫ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.f i₁ = p₂ ≫ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.f i₂<VAR>T : Scheme<VAR>g : T ⟶ W<VAR>x✝ : ⊤.arrows g<GOAL>({ I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.sieve₁ p₁ p₂).arrows g
<VAR>D : GlueData<VAR>i₁ i₂ : { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.I₀<VAR>W : Scheme<VAR>p₁ : W ⟶ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.X i₁<VAR>p₂ : W ⟶ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.X i₂<VAR>fac : p₁ ≫ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.f i₁ = p₂ ≫ { I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.f i₂<VAR>T : Scheme<VAR>g : T ⟶ W<VAR>x✝ : ⊤.arrows g<VAR>φ : T ⟶ (D.vPullbackCone i₁ i₂).pt<VAR>h₁ : φ ≫ (D.vPullbackCone i₁ i₂).fst = g ≫ p₁<VAR>h₂ : φ ≫ (D.vPullbackCone i₁ i₂).snd = g ≫ p₂<GOAL>({ I₀ := D.J, X := D.U, f := D.ι, I₁ := fun x x => PUnit.{u + 1}, Y := fun i₁ i₂ x => D.V (i₁, i₂), p₁ := fun i₁ i₂ x => D.f i₁ i₂, p₂ := fun i₁ i₂ j => D.t i₁ i₂ ≫ D.f i₂ i₁, w := ⋯ }.sieve₁ p₁ p₂).arrows g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : LocallyFiniteOrderBot ι<VAR>inst✝² : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>h : finrank 𝕜 E = Fintype.card ι<VAR>f✝ f : ι → E<VAR>i : ι<VAR>hi : gramSchmidtNormed 𝕜 f i = 0<VAR>j : ι<GOAL>⟪(gramSchmidtOrthonormalBasis h f) i, f j⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : LocallyFiniteOrderBot ι<VAR>inst✝² : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>h : finrank 𝕜 E = Fintype.card ι<VAR>f✝ f : ι → E<VAR>i : ι<VAR>hi : gramSchmidtNormed 𝕜 f i = 0<VAR>j : ι<GOAL>f j ∈ (span 𝕜 {(gramSchmidtOrthonormalBasis h f) i})ᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : LocallyFiniteOrderBot ι<VAR>inst✝² : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>h : finrank 𝕜 E = Fintype.card ι<VAR>f✝ f : ι → E<VAR>i : ι<VAR>hi : gramSchmidtNormed 𝕜 f i = 0<VAR>j : ι<GOAL>span 𝕜 (gramSchmidtNormed 𝕜 f '' Set.Iic j) ⟂ span 𝕜 {(gramSchmidtOrthonormalBasis h f) i}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : LocallyFiniteOrderBot ι<VAR>inst✝² : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>h : finrank 𝕜 E = Fintype.card ι<VAR>f✝ f : ι → E<VAR>i : ι<VAR>hi : gramSchmidtNormed 𝕜 f i = 0<VAR>j : ι<GOAL>∀ ⦃u : E⦄, u ∈ gramSchmidtNormed 𝕜 f '' Set.Iic j → ∀ ⦃v : E⦄, v ∈ {(gramSchmidtOrthonormalBasis h f) i} → ⟪u, v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : LocallyFiniteOrderBot ι<VAR>inst✝² : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>h : finrank 𝕜 E = Fintype.card ι<VAR>f✝ f : ι → E<VAR>i : ι<VAR>hi : gramSchmidtNormed 𝕜 f i = 0<VAR>j k : ι<VAR>left✝ : k ∈ Set.Iic j<VAR>hk : ¬gramSchmidtNormed 𝕜 f k = 0<GOAL>⟪gramSchmidtNormed 𝕜 f k, (gramSchmidtOrthonormalBasis h f) i⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : LocallyFiniteOrderBot ι<VAR>inst✝² : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>h : finrank 𝕜 E = Fintype.card ι<VAR>f✝ f : ι → E<VAR>i : ι<VAR>hi : gramSchmidtNormed 𝕜 f i = 0<VAR>j k : ι<VAR>left✝ : k ∈ Set.Iic j<VAR>hk : ¬gramSchmidtNormed 𝕜 f k = 0<GOAL>⟪(gramSchmidtOrthonormalBasis h f) k, (gramSchmidtOrthonormalBasis h f) i⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝⁴ : LinearOrder ι<VAR>inst✝³ : LocallyFiniteOrderBot ι<VAR>inst✝² : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>h : finrank 𝕜 E = Fintype.card ι<VAR>f✝ f : ι → E<VAR>i : ι<VAR>hi : gramSchmidtNormed 𝕜 f i = 0<VAR>j k : ι<VAR>left✝ : k ∈ Set.Iic j<VAR>hk : ¬gramSchmidtNormed 𝕜 f k = 0<VAR>this : k ≠ i<GOAL>⟪(gramSchmidtOrthonormalBasis h f) k, (gramSchmidtOrthonormalBasis h f) i⟫_𝕜 = 0
<VAR>R : Type u_1<VAR>inst✝¹⁴ : CommSemiring R<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>inst✝¹³ : AddCommMonoid M₁<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : Module R M₁<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>f : M₁ →ₗ[R] M₂ →ₗ[R] M<VAR>N₁ : Type u_6<VAR>N₂ : Type u_7<VAR>N : Type u_8<VAR>inst✝⁵ : AddCommMonoid N₁<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N₁<VAR>inst✝¹ : Module R N₂<VAR>inst✝ : Module R N<VAR>g : N₁ →ₗ[R] N₂ →ₗ[R] N<VAR>h : IsTensorProduct f<VAR>x₁ : M₁<VAR>x₂ : M₂<GOAL>h.equiv.symm ((f x₁) x₂) = x₁ ⊗ₜ[R] x₂
<VAR>R : Type u_1<VAR>inst✝¹⁴ : CommSemiring R<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>inst✝¹³ : AddCommMonoid M₁<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : Module R M₁<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>f : M₁ →ₗ[R] M₂ →ₗ[R] M<VAR>N₁ : Type u_6<VAR>N₂ : Type u_7<VAR>N : Type u_8<VAR>inst✝⁵ : AddCommMonoid N₁<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N₁<VAR>inst✝¹ : Module R N₂<VAR>inst✝ : Module R N<VAR>g : N₁ →ₗ[R] N₂ →ₗ[R] N<VAR>h : IsTensorProduct f<VAR>x₁ : M₁<VAR>x₂ : M₂<GOAL>h.equiv (h.equiv.symm ((f x₁) x₂)) = h.equiv (x₁ ⊗ₜ[R] x₂)
<VAR>R : Type u_1<VAR>inst✝¹⁴ : CommSemiring R<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>inst✝¹³ : AddCommMonoid M₁<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : Module R M₁<VAR>inst✝⁸ : Module R M₂<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>f : M₁ →ₗ[R] M₂ →ₗ[R] M<VAR>N₁ : Type u_6<VAR>N₂ : Type u_7<VAR>N : Type u_8<VAR>inst✝⁵ : AddCommMonoid N₁<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N₁<VAR>inst✝¹ : Module R N₂<VAR>inst✝ : Module R N<VAR>g : N₁ →ₗ[R] N₂ →ₗ[R] N<VAR>h : IsTensorProduct f<VAR>x₁ : M₁<VAR>x₂ : M₂<GOAL>(f x₁) x₂ = h.equiv (x₁ ⊗ₜ[R] x₂)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<GOAL>hausdorffEdist s u ≤ hausdorffEdist s t + hausdorffEdist t u
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<GOAL>(⨆ x ∈ s, infEdist x u) ⊔ ⨆ y ∈ u, infEdist y s ≤ hausdorffEdist s t + hausdorffEdist t u
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<GOAL>(∀ i ∈ s, infEdist i u ≤ hausdorffEdist s t + hausdorffEdist t u) ∧ ∀ i ∈ u, infEdist i s ≤ hausdorffEdist s t + hausdorffEdist t u
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>A : BinaryBicone P Q<GOAL>F.map A.inl ≫ F.map A.fst = 𝟙 (F.obj P)
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>A : BinaryBicone P Q<GOAL>F.map A.inl ≫ F.map A.snd = 0
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>A : BinaryBicone P Q<GOAL>F.map A.inr ≫ F.map A.fst = 0
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>A : BinaryBicone P Q<GOAL>F.map A.inr ≫ F.map A.snd = 𝟙 (F.obj Q)
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X✝ Y✝ : BinaryBicone P Q<VAR>f : X✝ ⟶ Y✝<GOAL>F.map f.hom ≫ ((fun A => { pt := F.obj A.pt, fst := F.map A.fst, snd := F.map A.snd, inl := F.map A.inl, inr := F.map A.inr, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }) Y✝).fst = ((fun A => { pt := F.obj A.pt, fst := F.map A.fst, snd := F.map A.snd, inl := F.map A.inl, inr := F.map A.inr, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }) X✝).fst
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X✝ Y✝ : BinaryBicone P Q<VAR>f : X✝ ⟶ Y✝<GOAL>F.map f.hom ≫ ((fun A => { pt := F.obj A.pt, fst := F.map A.fst, snd := F.map A.snd, inl := F.map A.inl, inr := F.map A.inr, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }) Y✝).snd = ((fun A => { pt := F.obj A.pt, fst := F.map A.fst, snd := F.map A.snd, inl := F.map A.inl, inr := F.map A.inr, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }) X✝).snd
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X✝ Y✝ : BinaryBicone P Q<VAR>f : X✝ ⟶ Y✝<GOAL>((fun A => { pt := F.obj A.pt, fst := F.map A.fst, snd := F.map A.snd, inl := F.map A.inl, inr := F.map A.inr, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }) X✝).inl ≫ F.map f.hom = ((fun A => { pt := F.obj A.pt, fst := F.map A.fst, snd := F.map A.snd, inl := F.map A.inl, inr := F.map A.inr, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }) Y✝).inl
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q : C<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X✝ Y✝ : BinaryBicone P Q<VAR>f : X✝ ⟶ Y✝<GOAL>((fun A => { pt := F.obj A.pt, fst := F.map A.fst, snd := F.map A.snd, inl := F.map A.inl, inr := F.map A.inr, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }) X✝).inr ≫ F.map f.hom = ((fun A => { pt := F.obj A.pt, fst := F.map A.fst, snd := F.map A.snd, inl := F.map A.inl, inr := F.map A.inr, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }) Y✝).inr
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<GOAL>d + ↑s.card / ↑t.card * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑t.card
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>hscard : 0 = ↑s.card<GOAL>d + ↑s.card / ↑t.card * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑t.card
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>hscard : 0 < ↑s.card<GOAL>d + ↑s.card / ↑t.card * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑t.card
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>hscard : 0 < ↑s.card<VAR>htcard : 0 < ↑t.card<GOAL>d + ↑s.card / ↑t.card * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑t.card
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>hscard : 0 < ↑s.card<VAR>htcard : 0 < ↑t.card<VAR>h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card) ^ 2<GOAL>d + ↑s.card / ↑t.card * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑t.card
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>hscard : 0 < ↑s.card<VAR>htcard : 0 < ↑t.card<VAR>h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑t.card)) / ↑s.card) ^ 2<GOAL>d + ↑s.card / ↑t.card * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑t.card
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>hscard : 0 < ↑s.card<VAR>htcard : 0 < ↑t.card<VAR>h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑t.card)) / ↑s.card) ^ 2<GOAL>((∑ i ∈ t, f i) / ↑t.card) ^ 2 + ↑s.card / ↑t.card * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑t.card
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>hscard : 0 < ↑s.card<VAR>htcard : 0 < ↑t.card<VAR>h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑t.card)) / ↑s.card) ^ 2<GOAL>((∑ i ∈ t, f i) / ↑t.card) ^ 2 * ↑t.card + ↑s.card * x ^ 2 ≤ ∑ i ∈ t, f i ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>hscard : 0 < ↑s.card<VAR>htcard : 0 < ↑t.card<VAR>h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑t.card)) / ↑s.card) ^ 2<VAR>h₃ : ↑s.card * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑t.card) i ^ 2<GOAL>((∑ i ∈ t, f i) / ↑t.card) ^ 2 * ↑t.card + ↑s.card * x ^ 2 ≤ ∑ i ∈ t, f i ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>hscard : 0 < ↑s.card<VAR>htcard : 0 < ↑t.card<VAR>h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑t.card)) / ↑s.card) ^ 2<VAR>h₃ : ↑s.card * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑t.card) i ^ 2<GOAL>((∑ i ∈ t, f i) / ↑t.card) ^ 2 * ↑t.card + ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑t.card) i ^ 2 ≤ ∑ i ∈ t, f i ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>hscard : 0 < ↑s.card<VAR>htcard : 0 < ↑t.card<VAR>h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑t.card)) / ↑s.card) ^ 2<VAR>h₃ : ↑s.card * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑t.card) i ^ 2<GOAL>((∑ i ∈ t, f i) / ↑t.card) ^ 2 * ↑t.card + ∑ x ∈ t, ((f x * ↑t.card - ∑ i ∈ t, f i) / ↑t.card) ^ 2 ≤ ∑ i ∈ t, f i ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>hscard : 0 < ↑s.card<VAR>htcard : 0 < ↑t.card<VAR>h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑t.card)) / ↑s.card) ^ 2<VAR>h₃ : ↑s.card * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑t.card) i ^ 2<GOAL>((∑ i ∈ t, f i) / ↑t.card) ^ 2 * ↑t.card + ∑ x ∈ t, (f x * ↑t.card - ∑ i ∈ t, f i) ^ 2 / ↑t.card ^ 2 ≤ ∑ i ∈ t, f i ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>l : ℕ<VAR>ι : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : ι → ι → Prop<VAR>inst✝ : DecidableRel r<VAR>s t : Finset ι<VAR>x : 𝕜<VAR>hst : s ⊆ t<VAR>f : ι → 𝕜<VAR>d : 𝕜<VAR>hx : 0 ≤ x<VAR>hs : x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card|<VAR>ht : d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>hscard : 0 < ↑s.card<VAR>htcard : 0 < ↑t.card<VAR>h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card) ^ 2<VAR>h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑t.card)) / ↑s.card) ^ 2<VAR>h₃ : ↑s.card * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑t.card) i ^ 2<GOAL>(∑ i ∈ t, f i) ^ 2 * ↑t.card + ∑ i ∈ t, (f i * ↑t.card - ∑ i ∈ t, f i) ^ 2 ≤ (∑ i ∈ t, f i ^ 2) * ↑t.card ^ 2