ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeasSubgroup F m p μ)<GOAL>StronglyMeasurable (-↑↑(lpMeasSubgroupToLpTrim F p μ hm f))
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeasSubgroup F m p μ)<GOAL>↑↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) =ᶠ[ae μ] -↑↑(lpMeasSubgroupToLpTrim F p μ hm f)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeasSubgroup F m p μ)<GOAL>↑↑↑(-f) =ᶠ[ae μ] -↑↑(lpMeasSubgroupToLpTrim F p μ hm f)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeasSubgroup F m p μ)<GOAL>↑↑↑(-f) =ᶠ[ae μ] fun x => -↑↑↑f x
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeasSubgroup F m p μ)<GOAL>-↑↑↑f =ᶠ[ae μ] fun x => -↑↑↑f x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>U R (-n - 2) = -U R n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>j4n : j ≤ 4 * n<VAR>h : xn a1 j ≡ xn a1 i [MOD xn a1 n]<GOAL>i ≤ 2 * n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>j4n : j ≤ 4 * n<VAR>h : xn a1 j ≡ xn a1 i [MOD xn a1 n]<GOAL>n ≤ 2 * n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>j4n : j ≤ 4 * n<VAR>h : xn a1 j ≡ xn a1 i [MOD xn a1 n]<GOAL>n ≤ n + n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>j4n : j ≤ 4 * n<VAR>h : xn a1 j ≡ xn a1 i [MOD xn a1 n]<VAR>i2n : i ≤ 2 * n<VAR>j2n : 2 * n < j<VAR>this : i = 4 * n - j<GOAL>j + i = 4 * n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>j4n : j ≤ 4 * n<VAR>h : xn a1 j ≡ xn a1 i [MOD xn a1 n]<VAR>i2n : i ≤ 2 * n<VAR>j2n : 2 * n < j<GOAL>4 * n - j + ?m.167070 i2n j2n ≤ 2 * n + ?m.167070 i2n j2n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>j4n : j ≤ 4 * n<VAR>h : xn a1 j ≡ xn a1 i [MOD xn a1 n]<VAR>i2n : i ≤ 2 * n<VAR>j2n : 2 * n < j<GOAL>2 * n + 2 * n ≤ 2 * n + j
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>j4n : j ≤ 4 * n<VAR>h : xn a1 j ≡ xn a1 i [MOD xn a1 n]<VAR>i2n : i ≤ 2 * n<VAR>j2n : 2 * n < j<VAR>j42n : 4 * n - j ≤ 2 * n<GOAL>xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>i j n : ℕ<VAR>ipos : 0 < i<VAR>hin : i ≤ n<VAR>j4n : j ≤ 4 * n<VAR>h : xn a1 j ≡ xn a1 i [MOD xn a1 n]<VAR>i2n : i ≤ 2 * n<VAR>j2n : 2 * n < j<VAR>j42n : 4 * n - j ≤ 2 * n<VAR>t : xn a1 (4 * n - (4 * n - j)) ≡ xn a1 (4 * n - j) [MOD xn a1 n] := xn_modEq_x4n_sub a1 j42n<GOAL>xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f✝ : X → ℝ<VAR>s✝ : Set X<VAR>f : X → ℝ<VAR>f_int : Integrable f μ<VAR>f_nonneg : 0 ≤ᶠ[ae μ] f<VAR>s : Set X<VAR>hs : ∀ x ∈ s, 1 ≤ f x<GOAL>μ s ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f✝ : X → ℝ<VAR>s✝ : Set X<VAR>f : X → ℝ<VAR>f_int : Integrable f μ<VAR>f_nonneg : 0 ≤ᶠ[ae μ] f<VAR>s : Set X<VAR>hs : ∀ x ∈ s, 1 ≤ f x<GOAL>μ s ≤ ∫⁻ (x : X), ENNReal.ofReal (f x) ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f✝ : X → ℝ<VAR>s✝ : Set X<VAR>f : X → ℝ<VAR>f_int : Integrable f μ<VAR>f_nonneg : 0 ≤ᶠ[ae μ] f<VAR>s : Set X<VAR>hs : ∀ x ∈ s, 1 ≤ f x<GOAL>AEMeasurable (fun a => ENNReal.ofReal (f a)) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f✝ : X → ℝ<VAR>s✝ : Set X<VAR>f : X → ℝ<VAR>f_int : Integrable f μ<VAR>f_nonneg : 0 ≤ᶠ[ae μ] f<VAR>s : Set X<VAR>hs : ∀ x ∈ s, 1 ≤ f x<GOAL>∀ x ∈ s, 1 ≤ ENNReal.ofReal (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>p q : α<VAR>h : p ~ᵤ q<VAR>hp : Prime p<VAR>u : αˣ<VAR>hu : p * ↑u = q<VAR>x✝ : IsUnit q<VAR>v : αˣ<VAR>hv : ↑v = q<GOAL>↑(v * u⁻¹) = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>p q : α<VAR>h : p ~ᵤ q<VAR>hp : Prime p<VAR>u : αˣ<VAR>hu : p * ↑u = q<GOAL>∀ (a b : α), p * ↑u ∣ a * b → p * ↑u ∣ a ∨ p * ↑u ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>p q : α<VAR>h : p ~ᵤ q<VAR>hp : Prime p<VAR>u : αˣ<VAR>hu : p * ↑u = q<GOAL>∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>p q : α<VAR>h : p ~ᵤ q<VAR>hp : Prime p<VAR>u : αˣ<VAR>hu : p * ↑u = q<VAR>a b : α<GOAL>p ∣ a * b → p ∣ a ∨ p ∣ b
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<VAR>H : Set.range ⇑g.base ⊆ Set.range ⇑f.base<GOAL>IsIso (pullback.snd f g)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<VAR>H : Set.range ⇑g.base ⊆ Set.range ⇑f.base<VAR>this : IsIso (pullback.snd f.base g.base)<GOAL>IsIso (pullback.snd f g)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<VAR>H : Set.range ⇑g.base ⊆ Set.range ⇑f.base<VAR>this✝ : IsIso (pullback.snd f.base g.base)<VAR>this : IsIso (pullback.snd f g).base<GOAL>IsIso (pullback.snd f g)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>inst✝ : DecidableEq α<VAR>p : Finset α → Prop<VAR>h0 : p ∅<VAR>step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)<VAR>s : Finset α<VAR>ihs : ∀ t ⊂ s, p t<GOAL>p s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>x : α<VAR>inst✝ : DecidableEq α<VAR>p : Finset α → Prop<VAR>h0 : p ∅<VAR>step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)<VAR>ihs : ∀ t ⊂ ∅, p t<GOAL>p ∅
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>inst✝ : DecidableEq α<VAR>p : Finset α → Prop<VAR>h0 : p ∅<VAR>step : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)<VAR>s : Finset α<VAR>ihs : ∀ t ⊂ s, p t<VAR>hne : s.Nonempty<GOAL>p s
<VAR>x✝ y x : ℝ<VAR>hx : 0 ≤ x<GOAL>1 + x + x ^ 2 / 2 = ∑ i ∈ range 3, x ^ i / ↑i !
<VAR>x✝ y x : ℝ<VAR>hx : 0 ≤ x<GOAL>1 + x + x ^ 2 / 2 = 1 / (↑0 + 1) + x / (↑0 + 1) + x ^ 2 / (↑0 + 1 + 1)
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>f : α → α<VAR>n : ℕ<VAR>hf : Involutive f<VAR>hne : f ≠ id<VAR>H : f^[n] = id<VAR>hn : Odd n<GOAL>f = id
<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>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' x✝ : D<GOAL>adj.unit.app (G.obj x✝) ≫ G.map (adj.counit.app x✝) = 𝟙 (G.obj x✝)
<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>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' x✝ : D<GOAL>adj.counit.app x✝ = F.map (𝟙 (G.obj x✝)) ≫ adj.counit.app x✝
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : Nontrivial R<GOAL>W.polynomial.degree = 2
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : Nontrivial R<GOAL>{ a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly, d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly.degree = 2
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>s : Set R<GOAL>↑(closure s) = ↑(AddSubmonoid.closure ↑(Submonoid.closure s))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<GOAL>∑ s : Finset α, ↑(card α) / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<GOAL>∑ i ∈ range (univ.card + 1), ∑ x ∈ powersetCard i univ, ↑(card α) / ((↑(card α) - ↑x.card) * ↑((card α).choose x.card)) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>this : ∀ {x : ℕ}, ∀ s ∈ powersetCard x univ, ↑(card α) / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))<GOAL>∑ i ∈ range (univ.card + 1), ∑ x ∈ powersetCard i univ, ↑(card α) / ((↑(card α) - ↑x.card) * ↑((card α).choose x.card)) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>this : ∀ {x : ℕ}, ∀ s ∈ powersetCard x univ, ↑(card α) / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))<GOAL>∑ x ∈ range (card α + 1), ↑(card α) * (↑((card α).choose x) / ((↑(card α) - ↑x) * ↑((card α).choose x))) = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>this : ∀ {x : ℕ}, ∀ s ∈ powersetCard x univ, ↑(card α) / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))<GOAL>↑(card α) * ∑ i ∈ range (card α + 1), ↑((card α).choose i) / ((↑(card α) - ↑i) * ↑((card α).choose i)) = ↑(card α) * ∑ x ∈ range (card α).succ, (↑x)⁻¹
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>this✝ : ∀ {x : ℕ}, ∀ s ∈ powersetCard x univ, ↑(card α) / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))<VAR>this : ∀ n ∈ range (card α + 1), ↑((card α).choose n) / ((↑(card α) - ↑n) * ↑((card α).choose n)) = (↑(card α) - ↑n)⁻¹<GOAL>↑(card α) * ∑ i ∈ range (card α + 1), ↑((card α).choose i) / ((↑(card α) - ↑i) * ↑((card α).choose i)) = ↑(card α) * ∑ x ∈ range (card α).succ, (↑x)⁻¹
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>this✝ : ∀ {x : ℕ}, ∀ s ∈ powersetCard x univ, ↑(card α) / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))<VAR>this : ∀ n ∈ range (card α + 1), ↑((card α).choose n) / ((↑(card α) - ↑n) * ↑((card α).choose n)) = (↑(card α) - ↑n)⁻¹<GOAL>∑ x ∈ range (card α + 1), (↑(card α) - ↑x)⁻¹ = ∑ x ∈ range (card α).succ, (↑x)⁻¹ ∨ card α = 0
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>this✝ : ∀ {x : ℕ}, ∀ s ∈ powersetCard x univ, ↑(card α) / ((↑(card α) - ↑s.card) * ↑((card α).choose s.card)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))<VAR>this : ∀ n ∈ range (card α + 1), ↑((card α).choose n) / ((↑(card α) - ↑n) * ↑((card α).choose n)) = (↑(card α) - ↑n)⁻¹<VAR>a : ℕ<VAR>ha : a ∈ range (card α + 1)<GOAL>(↑(card α) - ↑a)⁻¹ = (↑(card α + 1 - 1 - a))⁻¹
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsIso g<GOAL>OpenEmbedding ((forget TopCat).map f ≫ (forget TopCat).map g) ↔ OpenEmbedding ⇑f
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsIso g<GOAL>OpenEmbedding ((forget TopCat).map (f ≫ g)) ↔ OpenEmbedding ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : BooleanRing α<VAR>a b : α<GOAL>a - b = a + b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : 0 < c<GOAL>(fun x => c * x) ⁻¹' Ioc a b = Ioc (a / c) (b / c)
<VAR>x✝ y✝ z : ℝ<VAR>n : ℕ<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 < y<GOAL>x ^ y < 1 ↔ x < 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<VAR>h : IsUnit (Q m)<GOAL>IsUnit ((ι Q) m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<VAR>h : IsUnit (Q m)<VAR>val✝ : Invertible (Q m)<GOAL>IsUnit ((ι Q) m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<VAR>h : IsUnit (Q m)<VAR>val✝ : Invertible (Q m)<VAR>this : Invertible ((ι Q) m) := invertibleιOfInvertible Q m<GOAL>IsUnit ((ι Q) m)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_5, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.90392, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_4, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(ShortComplex.mk (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ⋯).Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_5, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.90392, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_4, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>ShortComplex.mk ((F.shift n₁).map T.invRotate.mor₁) ((F.shift n₁).map T.invRotate.mor₂) ⋯ ≅ ShortComplex.mk (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_5, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.90392, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_4, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(-(F.shiftIso (-1) n₁ n₀ ⋯).hom.app T.obj₃) ≫ F.homologySequenceδ T n₀ n₁ h = (F.shift n₁).map (-(shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁) ≫ 𝟙 ((F.shift n₁).obj T.obj₁)
<VAR>x y z : ZFSet<VAR>hx : x.IsTransitive<VAR>hy : y.IsTransitive<GOAL>(x ∪ y).IsTransitive
<VAR>x y z : ZFSet<VAR>hx : x.IsTransitive<VAR>hy : y.IsTransitive<GOAL>(⋃₀ {x, y}).IsTransitive
<VAR>x y z : ZFSet<VAR>hx : x.IsTransitive<VAR>hy : y.IsTransitive<GOAL>∀ z ∈ {x, y}, z.IsTransitive
<VAR>x y z : ZFSet<VAR>hx : x.IsTransitive<VAR>hy : y.IsTransitive<VAR>z✝ : ZFSet<GOAL>z✝ ∈ {x, y} → z✝.IsTransitive
<VAR>x y z : ZFSet<VAR>hx : x.IsTransitive<VAR>hy : y.IsTransitive<VAR>z✝ : ZFSet<GOAL>z✝ = x ∨ z✝ = y → z✝.IsTransitive
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.75295, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>i j : ℕ<VAR>x✝ : (ComplexShape.down ℕ).Rel i j<GOAL>((s.cofan (op [i])).inj (IndexSet.id (op [i])) ≫ PInfty.f i) ≫ K[X].d i j = ((s.cofan (op [i])).inj (IndexSet.id (op [i])) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op [j]))) ≫ (s.cofan (op [j])).inj (IndexSet.id (op [j])) ≫ PInfty.f j
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.75295, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>n : ℕ<GOAL>(s.cofan (op [n])).inj (IndexSet.id (op [n])) ≫ PInfty.f n = 𝟙 (s.N n) ≫ ((s.cofan (op [n])).inj (IndexSet.id (op [n])) ≫ PInfty.f n) ≫ PInfty.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.75295, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>i j : ℕ<VAR>x✝ : (ComplexShape.down ℕ).Rel i j<GOAL>s.πSummand (IndexSet.id (op [i])) ≫ (s.cofan (op [i])).inj (IndexSet.id (op [i])) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op [j])) = K[X].d i j ≫ s.πSummand (IndexSet.id (op [j]))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.75295, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>i j : ℕ<VAR>x✝ : (ComplexShape.down ℕ).Rel i j<GOAL>s.πSummand (IndexSet.id (op [i])) ≫ (s.cofan (op [i])).inj (IndexSet.id (op [i])) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op [j])) = (𝟙 (K[X].X i) ≫ K[X].d i j) ≫ s.πSummand (IndexSet.id (op [j]))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.75295, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>i j : ℕ<VAR>x✝ : (ComplexShape.down ℕ).Rel i j<GOAL>s.πSummand (IndexSet.id (op [i])) ≫ (s.cofan (op [i])).inj (IndexSet.id (op [i])) ≫ K[X].d i j ≫ s.πSummand (IndexSet.id (op [j])) = ((∑ A : IndexSet (op [i]), s.πSummand A ≫ (s.cofan (op [i])).inj A) ≫ K[X].d i j) ≫ s.πSummand (IndexSet.id (op [j]))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.75295, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>i j : ℕ<VAR>x✝ : (ComplexShape.down ℕ).Rel i j<GOAL>∀ b ∈ Finset.univ, b ≠ IndexSet.id (op [i]) → ((s.πSummand b ≫ (s.cofan (op [i])).inj b) ≫ K[X].d i j) ≫ s.πSummand (IndexSet.id (op [j])) = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.75295, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>i j : ℕ<VAR>x✝ : (ComplexShape.down ℕ).Rel i j<GOAL>IndexSet.id (op [i]) ∉ Finset.univ → ((s.πSummand (IndexSet.id (op [i])) ≫ (s.cofan (op [i])).inj (IndexSet.id (op [i]))) ≫ K[X].d i j) ≫ s.πSummand (IndexSet.id (op [j])) = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.75295, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>n : ℕ<GOAL>s.πSummand (IndexSet.id (op [n])) = PInfty.f n ≫ s.πSummand (IndexSet.id (op [n])) ≫ 𝟙 (s.N n)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.75295, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>n : ℕ<GOAL>({ f := { f := fun n => (s.cofan (op [n])).inj (IndexSet.id (op [n])) ≫ PInfty.f n, comm' := ⋯ }, comm := ⋯ } ≫ { f := { f := fun n => s.πSummand (IndexSet.id (op [n])), comm' := ⋯ }, comm := ⋯ }).f.f n = (𝟙 ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex)).f.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.75295, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>n : ℕ<GOAL>𝟙 (summand s.N (op [n]) (IndexSet.id (op [n]))) = (𝟙 ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex)).f.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.75295, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : Preadditive C<VAR>n : ℕ<GOAL>({ f := { f := fun n => s.πSummand (IndexSet.id (op [n])), comm' := ⋯ }, comm := ⋯ } ≫ { f := { f := fun n => (s.cofan (op [n])).inj (IndexSet.id (op [n])) ≫ PInfty.f n, comm' := ⋯ }, comm := ⋯ }).f.f n = (𝟙 (N₁.obj X)).f.f n
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : ℕ × ℕ<VAR>ha : a ∈ filter (fun a => a.1 < k) (antidiagonal k)<VAR>f : Finset σ × σ → MvPolynomial σ R<GOAL>∑ t ∈ filter (fun t => t.1.card = a.1) (MvPolynomial.NewtonIdentities.pairs σ k), f t = ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, f (A, j)
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : ℕ × ℕ<VAR>ha : a ∈ filter (fun a => a.1 < k) (antidiagonal k)<VAR>f : Finset σ × σ → MvPolynomial σ R<GOAL>∀ (p : Finset σ × σ), p ∈ filter (fun t => t.1.card = a.1) (MvPolynomial.NewtonIdentities.pairs σ k) ↔ p.1 ∈ powersetCard a.1 univ ∧ p.2 ∈ univ
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : ℕ × ℕ<VAR>ha : a ∈ filter (fun a => a.1 < k) (antidiagonal k)<VAR>f : Finset σ × σ → MvPolynomial σ R<GOAL>∀ (p : Finset σ × σ), p.1.card = a.1 → p ∈ MvPolynomial.NewtonIdentities.pairs σ k
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : ℕ × ℕ<VAR>ha : a ∈ filter (fun a => a.1 < k) (antidiagonal k)<VAR>f : Finset σ × σ → MvPolynomial σ R<VAR>p : Finset σ × σ<VAR>hp : p.1.card = a.1<GOAL>p ∈ MvPolynomial.NewtonIdentities.pairs σ k
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<VAR>a : ℕ × ℕ<VAR>ha : a ∈ filter (fun a => a.1 < k) (antidiagonal k)<VAR>f : Finset σ × σ → MvPolynomial σ R<VAR>p : Finset σ × σ<VAR>hp : p.1.card = a.1<VAR>this : p.1.card ≤ k<GOAL>p ∈ MvPolynomial.NewtonIdentities.pairs σ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>inst✝ : Countable ι'<VAR>x : ι' → Set α<GOAL>(⨅ i, 𝓟 (x i)).IsCountablyGenerated
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>inst✝ : Countable ι'<VAR>x : ι' → Set α<GOAL>⨅ i, 𝓟 (x i) = generate (range x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>a b : ℝ<VAR>h : a ≤ b<GOAL>Metric.diam (Ico a b) = b - a