ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<GOAL>map ({ toFun := fun i => (i, n - i), inj' := ⋯ }.trans { toFun := Prod.swap, inj' := ⋯ }) (range (n + 1)) = map { toFun := fun i => (n - i, i), inj' := ⋯ } (range (n + 1))
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t✝ s : Set A<VAR>t : Submodule R A<GOAL>Subalgebra.toSubmodule (adjoin R s) ≤ t ↔ ↑(Submonoid.closure s) ⊆ ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>f : α → β<VAR>x : α →₀ M<VAR>a : β<VAR>h : a ∉ Set.range f<GOAL>(mapDomain f x) a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>v v₁ v₂ : α →₀ M<VAR>f : α → β<VAR>x : α →₀ M<VAR>a : β<VAR>h : a ∉ Set.range f<GOAL>∑ a_1 ∈ x.support, (single (f a_1) (x a_1)) a = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o✝ : Orientation ℝ E (Fin 2)<VAR>w z : ℂ<VAR>o : Orientation ℝ ℂ (Fin 2) := Complex.orientation<GOAL>(Complex.orientation.areaForm w) z = ((starRingEnd ℂ) w * z).im
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o✝ : Orientation ℝ E (Fin 2)<VAR>w z : ℂ<VAR>o : Orientation ℝ ℂ (Fin 2) := Complex.orientation<GOAL>w.re * z.im - z.re * w.im = w.re * z.im + -w.im * z.re
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>(polyOfInterest p n).vars ⊆ univ ×ˢ range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>(↑p ^ (n + 1) * (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) - X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) - X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars ⊆ univ ×ˢ range (n + 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✝⁶ : Semiring R<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>a b : R<VAR>x y : M<VAR>hf : ∀ (l : ι →₀ R), (Finsupp.total ι M R v) l = 0 → l = 0<VAR>s : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<VAR>his : i ∈ s<GOAL>(Finsupp.total ι M R v) (∑ i ∈ s, Finsupp.single i (g i)) = 0
<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✝⁶ : Semiring R<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>a b : R<VAR>x y : M<VAR>hf : ∀ (l : ι →₀ R), (Finsupp.total ι M R v) l = 0 → l = 0<VAR>s : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<VAR>his : i ∈ s<VAR>h : ∑ i ∈ s, Finsupp.single i (g i) = 0<GOAL>g i = (Finsupp.lapply i) (Finsupp.single i (g i))
<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✝⁶ : Semiring R<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>a b : R<VAR>x y : M<VAR>hf : ∀ (l : ι →₀ R), (Finsupp.total ι M R v) l = 0 → l = 0<VAR>s : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<VAR>his : i ∈ s<VAR>h : ∑ i ∈ s, Finsupp.single i (g i) = 0<VAR>j : ι<VAR>_hjs : j ∈ s<VAR>hji : j ≠ i<GOAL>(Finsupp.lapply i) (Finsupp.single j (g j)) = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>Γ' : Type u_3<VAR>inst✝ : PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>x y : HahnSeries Γ R<VAR>xy : embDomain f x = embDomain f y<VAR>g : Γ<GOAL>x.coeff g = y.coeff g
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>Γ' : Type u_3<VAR>inst✝ : PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>x y : HahnSeries Γ R<VAR>xy : ∀ (a : Γ'), (embDomain f x).coeff a = (embDomain f y).coeff a<VAR>g : Γ<GOAL>x.coeff g = y.coeff g
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>Γ' : Type u_3<VAR>inst✝ : PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>x y : HahnSeries Γ R<VAR>xy : ∀ (a : Γ'), (embDomain f x).coeff a = (embDomain f y).coeff a<VAR>g : Γ<VAR>xyg : (embDomain f x).coeff (f g) = (embDomain f y).coeff (f g)<GOAL>x.coeff g = y.coeff g
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<GOAL>↑↑0 = ↑0
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>p : PosNum<GOAL>↑↑(pos p) = ↑(pos p)
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>p : PosNum<GOAL>↑↑(neg p) = ↑(neg p)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x \ (y \ z) = z ⊓ x ⊔ x \ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = ⊥
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>x y : F<GOAL>(basisDivisor x x).natDegree = 0
<VAR>a b c : Cardinal.{u_1}<VAR>h : a + b = c + b<VAR>hb : b < ℵ₀<GOAL>a = c
<VAR>a b c : Cardinal.{u_1}<VAR>h : b + a = b + c<VAR>hb : b < ℵ₀<GOAL>a = c
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower S R M<VAR>f : R[X]<VAR>g : PolynomialModule R M<VAR>n : ℕ<GOAL>(f • g) n = ∑ x ∈ Finset.antidiagonal n, f.coeff x.1 • g x.2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower S R M<VAR>g : PolynomialModule R M<VAR>n : ℕ<VAR>p q : R[X]<VAR>hp : (p • g) n = ∑ x ∈ Finset.antidiagonal n, p.coeff x.1 • g x.2<VAR>hq : (q • g) n = ∑ x ∈ Finset.antidiagonal n, q.coeff x.1 • g x.2<GOAL>((p + q) • g) n = ∑ x ∈ Finset.antidiagonal n, (p + q).coeff x.1 • g x.2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower S R M<VAR>g : PolynomialModule R M<VAR>n f_n : ℕ<VAR>f_a : R<GOAL>((monomial f_n) f_a • g) n = ∑ x ∈ Finset.antidiagonal n, ((monomial f_n) f_a).coeff x.1 • g x.2
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>s : Set α<GOAL>m.trim s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>s : Set α<GOAL>m.trim s = ⨅ t, ⨅ (_ : MeasurableSet t), ⨅ (_ : s ⊆ t), m t
<VAR>m : ℤ<VAR>n : ℕ<GOAL>dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m (Submonoid.pow 2 n)) = m • powHalf n
<VAR>m : ℤ<VAR>n : ℕ<GOAL>↑m * powHalf n = m • powHalf n
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasBinaryProducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).hom ≫ ((fun X Y => prod.braiding X Y) X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = ((fun X Y => prod.braiding X Y) X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ ((fun X Y => prod.braiding X Y) X Z).hom
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasBinaryProducts C<VAR>X Y Z : C<GOAL>prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd) ≫ prod.lift prod.snd prod.fst ≫ prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd) = prod.map (prod.lift prod.snd prod.fst) (𝟙 Z) ≫ prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd) ≫ prod.map (𝟙 Y) (prod.lift prod.snd prod.fst)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasBinaryProducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).inv ≫ ((fun X Y => prod.braiding X Y) (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ ((fun X Y => prod.braiding X Y) Y Z).hom ≫ (α_ X Z Y).inv ≫ ((fun X Y => prod.braiding X Y) X Z).hom ▷ Y
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasBinaryProducts C<VAR>X Y Z : C<GOAL>prod.lift (prod.lift prod.fst (prod.snd ≫ prod.fst)) (prod.snd ≫ prod.snd) ≫ prod.lift prod.snd prod.fst ≫ prod.lift (prod.lift prod.fst (prod.snd ≫ prod.fst)) (prod.snd ≫ prod.snd) = prod.map (𝟙 X) (prod.lift prod.snd prod.fst) ≫ prod.lift (prod.lift prod.fst (prod.snd ≫ prod.fst)) (prod.snd ≫ prod.snd) ≫ prod.map (prod.lift prod.snd prod.fst) (𝟙 Y)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>ι : Type u_1<VAR>m : Basis ι R ↥M<VAR>H : Function.Injective ⇑(mulLeftMap N ⇑m)<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>ι : Type u_1<VAR>m : Basis ι R ↥M<VAR>H : Function.Injective ⇑(M.mulMap N)<GOAL>M.LinearDisjoint N
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g✝ : W ⟶ Y<VAR>h✝ : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>g : W ≅ Y<VAR>h : X ≅ Z<VAR>p : CommSq f g.hom h.hom i<GOAL>i ≫ h.inv = g.inv ≫ f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ↥(Lp E p μ)<GOAL>f = 0 ↔ ↑↑f =ᶠ[ae μ] 0
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f✝ : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f : X ⟶ Z<GOAL>𝟙 X ≫ f = f ≫ 𝟙 Z
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs' : s ≠ 1<GOAL>DifferentiableAt ℂ (hurwitzZetaEven a) s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs' : s ≠ 1<VAR>this : DifferentiableAt ℂ (Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 ((if a = 0 then -1 else 0) / 2)) s<GOAL>DifferentiableAt ℂ (hurwitzZetaEven a) s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs' : s ≠ 1<VAR>this : DifferentiableAt ℂ (Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0)) s<GOAL>DifferentiableAt ℂ (hurwitzZetaEven a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<GOAL>∫⁻ (a : α), liminf (fun n => f n a) atTop ∂μ = ∫⁻ (a : α), ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i a ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>H : IsPreirreducible s<VAR>f : X → Y<VAR>hf : ContinuousOn f s<VAR>u v : Set Y<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x : X<VAR>hx : x ∈ s<VAR>hxu : f x ∈ u<VAR>y : X<VAR>hy : y ∈ s<VAR>hyv : f y ∈ v<GOAL>(f '' s ∩ (u ∩ v)).Nonempty
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>H : IsPreirreducible s<VAR>f : X → Y<VAR>hf : ContinuousOn f s<VAR>u v : Set Y<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x : X<VAR>hx : x ∈ s<VAR>hxu : x ∈ f ⁻¹' u<VAR>y : X<VAR>hy : y ∈ s<VAR>hyv : y ∈ f ⁻¹' v<GOAL>(f '' s ∩ (u ∩ v)).Nonempty
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>H : IsPreirreducible s<VAR>f : X → Y<VAR>hf : ContinuousOn f s<VAR>u v : Set Y<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x : X<VAR>hx : x ∈ s<VAR>hxu : x ∈ f ⁻¹' u<VAR>y : X<VAR>hy : y ∈ s<VAR>hyv : y ∈ f ⁻¹' v<VAR>u' : Set X<VAR>hu' : IsOpen u'<VAR>u'_eq : f ⁻¹' u ∩ s = u' ∩ s<GOAL>(f '' s ∩ (u ∩ v)).Nonempty
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>H : IsPreirreducible s<VAR>f : X → Y<VAR>hf : ContinuousOn f s<VAR>u v : Set Y<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x : X<VAR>hx : x ∈ s<VAR>hxu : x ∈ f ⁻¹' u<VAR>y : X<VAR>hy : y ∈ s<VAR>hyv : y ∈ f ⁻¹' v<VAR>u' : Set X<VAR>hu' : IsOpen u'<VAR>u'_eq : f ⁻¹' u ∩ s = u' ∩ s<VAR>v' : Set X<VAR>hv' : IsOpen v'<VAR>v'_eq : f ⁻¹' v ∩ s = v' ∩ s<GOAL>(f '' s ∩ (u ∩ v)).Nonempty
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>H : IsPreirreducible s<VAR>f : X → Y<VAR>hf : ContinuousOn f s<VAR>u v : Set Y<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x : X<VAR>hx : x ∈ s<VAR>hxu : x ∈ f ⁻¹' u<VAR>y : X<VAR>hy : y ∈ s<VAR>hyv : y ∈ f ⁻¹' v<VAR>u' : Set X<VAR>hu' : IsOpen u'<VAR>u'_eq : f ⁻¹' u ∩ s = u' ∩ s<VAR>v' : Set X<VAR>hv' : IsOpen v'<VAR>v'_eq : f ⁻¹' v ∩ s = v' ∩ s<VAR>this : (s ∩ u').Nonempty → (s ∩ v').Nonempty → (s ∩ (u' ∩ v')).Nonempty<GOAL>(f '' s ∩ (u ∩ v)).Nonempty
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>H : IsPreirreducible s<VAR>f : X → Y<VAR>hf : ContinuousOn f s<VAR>u v : Set Y<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x : X<VAR>hx : x ∈ s<VAR>hxu : x ∈ f ⁻¹' u<VAR>y : X<VAR>hy : y ∈ s<VAR>hyv : y ∈ f ⁻¹' v<VAR>u' : Set X<VAR>hu' : IsOpen u'<VAR>u'_eq : f ⁻¹' u ∩ s = u' ∩ s<VAR>v' : Set X<VAR>hv' : IsOpen v'<VAR>v'_eq : f ⁻¹' v ∩ s = v' ∩ s<VAR>this : (f ⁻¹' u ∩ s).Nonempty → (s ∩ v').Nonempty → (s ∩ (u' ∩ v')).Nonempty<GOAL>(f '' s ∩ (u ∩ v)).Nonempty
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>H : IsPreirreducible s<VAR>f : X → Y<VAR>hf : ContinuousOn f s<VAR>u v : Set Y<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x : X<VAR>hx : x ∈ s<VAR>hxu : x ∈ f ⁻¹' u<VAR>y : X<VAR>hy : y ∈ s<VAR>hyv : y ∈ f ⁻¹' v<VAR>u' : Set X<VAR>hu' : IsOpen u'<VAR>u'_eq : f ⁻¹' u ∩ s = u' ∩ s<VAR>v' : Set X<VAR>hv' : IsOpen v'<VAR>v'_eq : f ⁻¹' v ∩ s = v' ∩ s<VAR>this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty<GOAL>(f '' s ∩ (u ∩ v)).Nonempty
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>H : IsPreirreducible s<VAR>f : X → Y<VAR>hf : ContinuousOn f s<VAR>u v : Set Y<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x✝ : X<VAR>hx : x✝ ∈ s<VAR>hxu : x✝ ∈ f ⁻¹' u<VAR>y : X<VAR>hy : y ∈ s<VAR>hyv : y ∈ f ⁻¹' v<VAR>u' : Set X<VAR>hu' : IsOpen u'<VAR>u'_eq : f ⁻¹' u ∩ s = u' ∩ s<VAR>v' : Set X<VAR>hv' : IsOpen v'<VAR>v'_eq : f ⁻¹' v ∩ s = v' ∩ s<VAR>this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty<VAR>x : X<VAR>hxs : x ∈ s<VAR>hxu' : x ∈ u'<VAR>hxv' : x ∈ v'<GOAL>(f '' s ∩ (u ∩ v)).Nonempty
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>H : IsPreirreducible s<VAR>f : X → Y<VAR>hf : ContinuousOn f s<VAR>u v : Set Y<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x✝ : X<VAR>hx : x✝ ∈ s<VAR>hxu : x✝ ∈ f ⁻¹' u<VAR>y : X<VAR>hy : y ∈ s<VAR>hyv : y ∈ f ⁻¹' v<VAR>u' : Set X<VAR>hu' : IsOpen u'<VAR>u'_eq : f ⁻¹' u ∩ s = u' ∩ s<VAR>v' : Set X<VAR>hv' : IsOpen v'<VAR>v'_eq : f ⁻¹' v ∩ s = v' ∩ s<VAR>this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty<VAR>x : X<VAR>hxs : x ∈ s<VAR>hxu' : x ∈ u'<VAR>hxv' : x ∈ v'<GOAL>f x ∈ u
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>H : IsPreirreducible s<VAR>f : X → Y<VAR>hf : ContinuousOn f s<VAR>u v : Set Y<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x✝ : X<VAR>hx : x✝ ∈ s<VAR>hxu : x✝ ∈ f ⁻¹' u<VAR>y : X<VAR>hy : y ∈ s<VAR>hyv : y ∈ f ⁻¹' v<VAR>u' : Set X<VAR>hu' : IsOpen u'<VAR>u'_eq : f ⁻¹' u ∩ s = u' ∩ s<VAR>v' : Set X<VAR>hv' : IsOpen v'<VAR>v'_eq : f ⁻¹' v ∩ s = v' ∩ s<VAR>this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty<VAR>x : X<VAR>hxs : x ∈ s<VAR>hxu' : x ∈ u'<VAR>hxv' : x ∈ v'<GOAL>f x ∈ v
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>f : ι' ≃ ι<VAR>t : (i : ι) → Set (α i)<GOAL>(⇑(piCongrLeft α f).symm ⁻¹' univ.pi fun i' => t (f i')) = univ.pi t
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ab : a ≤ b<VAR>c : ℤ√↑d<GOAL>(c + b - (c + a)).Nonneg
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ab : a ≤ b<VAR>c : ℤ√↑d<GOAL>(b - a).Nonneg
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>a₁ : α<VAR>b : β<VAR>a₂ : α<GOAL>(G □ H).Adj (a₁, b) (a₂, b) ↔ G.Adj a₁ a₂
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<GOAL>¬Injective f ↔ ∃ a b, f a = f b ∧ a ≠ b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<GOAL>(convexHull 𝕜) (-s) = -(convexHull 𝕜) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<GOAL>(convexHull 𝕜) (Neg.neg '' s) = Neg.neg '' (convexHull 𝕜) s
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<GOAL>(condCount s) t = 0 ↔ s ∩ t = ∅
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Integrable f μ<GOAL>∫ (x : α), ⨍ (a : α), f a ∂μ - f x ∂μ = 0
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f : w.CostructuredArrowDownwards g<GOAL>R.map f.left.hom ≫ ((w.costructuredArrowRightwards X₃).obj (CostructuredArrow.mk f.hom.right)).hom = (CostructuredArrow.mk g).hom
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f₁ f₂ : w.CostructuredArrowDownwards g<VAR>φ : f₁ ⟶ f₂<GOAL>L.map φ.left.right ≫ f₂.hom.right = f₁.hom.right
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f₁ f₂ : w.CostructuredArrowDownwards g<VAR>φ : f₁ ⟶ f₂<GOAL>L.map φ.left.right ≫ f₂.hom.right = ((w.structuredArrowDownwards X₂).map φ.left ≫ f₂.hom).right
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f₁ f₂ : w.CostructuredArrowDownwards g<VAR>φ : f₁ ⟶ f₂<GOAL>(((fun f => StructuredArrow.mk (CostructuredArrow.homMk f.left.hom ⋯)) f₁).hom ≫ (w.costructuredArrowRightwards X₃).map (CostructuredArrow.homMk φ.left.right ⋯)).left = ((fun f => StructuredArrow.mk (CostructuredArrow.homMk f.left.hom ⋯)) f₂).hom.left
<VAR>b x y : ℝ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>logb b (x / y) = logb b x - logb b y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>S : WSeq (Computation α)<GOAL>map f (parallel S) = parallel (WSeq.map (map f) S)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>S : WSeq (Computation α)<GOAL>IsBisimulation fun c1 c2 => ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ij : i ≤ j<VAR>j2n : j ≤ 2 * n<VAR>h : xn a1 i ≡ xn a1 j [MOD xn a1 n]<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)<VAR>npos : ¬n = 0<VAR>ij' : i < j<VAR>jn : j = n<GOAL>False
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ij : i ≤ j<VAR>j2n : j ≤ 2 * n<VAR>h : xn a1 i ≡ xn a1 j [MOD xn a1 n]<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)<VAR>npos : ¬n = 0<VAR>ij' : i < j<VAR>jn : j = n<GOAL>xn a1 j % xn a1 n < xn a1 i % xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ij : i ≤ j<VAR>j2n : j ≤ 2 * n<VAR>h : xn a1 i ≡ xn a1 j [MOD xn a1 n]<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)<VAR>npos : ¬n = 0<VAR>ij' : i < j<VAR>jn : j = n<GOAL>0 < xn a1 i % xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ij : i ≤ j<VAR>j2n : j ≤ 2 * n<VAR>h : xn a1 i ≡ xn a1 j [MOD xn a1 n]<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)<VAR>npos : ¬n = 0<VAR>ij' : i < j<VAR>jn : j = n<VAR>x0 : 0 < xn a1 0 % xn a1 n<GOAL>0 < xn a1 i % xn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>j n : ℕ<VAR>j2n : j ≤ 2 * n<VAR>npos : ¬n = 0<VAR>jn : j = n<VAR>x0 : 0 < xn a1 0 % xn a1 n<VAR>i : ℕ<VAR>ij : i + 1 ≤ j<VAR>h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]<VAR>ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)<VAR>ij' : i + 1 < n<GOAL>0 < xn a1 (i + 1) % xn a1 n
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)<VAR>M : HomologicalComplex C c<VAR>α : K ⟶ M<VAR>β : L ⟶ M<VAR>i : ι<GOAL>biprod.inl.f i ≫ (biprod.desc α β).f i = α.f i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hp : ∀ k < n, ∀ᶠ (a : ℕ) in atTop, p (n * a + k)<GOAL>∀ᶠ (a : ℕ) in atTop, p a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hp : ∀ k < n, ∃ a, ∀ b ≥ a, p (n * b + k)<GOAL>∃ a, ∀ b ≥ a, p b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>N : ℕ → ℕ<VAR>hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)<VAR>b : ℕ<VAR>hb : b ≥ (Finset.range n).sup fun x => n * N x<GOAL>p b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>N : ℕ → ℕ<VAR>hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)<VAR>b : ℕ<VAR>hb : b ≥ (Finset.range n).sup fun x => n * N x<GOAL>p (n * (b / n) + b % n)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>N : ℕ → ℕ<VAR>hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)<VAR>b : ℕ<VAR>hb : b ≥ (Finset.range n).sup fun x => n * N x<VAR>hlt : b % n < n<GOAL>p (n * (b / n) + b % n)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>N : ℕ → ℕ<VAR>hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)<VAR>b : ℕ<VAR>hb : b ≥ (Finset.range n).sup fun x => n * N x<VAR>hlt : b % n < n<GOAL>b / n ≥ N (b % n)