ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>π : ι → Set (Set Ω)<VAR>m✝ : ι → MeasurableSpace Ω<VAR>x✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>S : Finset ι<VAR>s : ι → Set Ω<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<GOAL>iIndep m μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f i)) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>π : ι → Set (Set Ω)<VAR>m✝ : ι → MeasurableSpace Ω<VAR>x✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>S : Finset ι<VAR>s : ι → Set Ω<VAR>m : ι → MeasurableSpace Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<GOAL>(∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ {s | MeasurableSet s}) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)) ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f i)) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
<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>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<GOAL>(increment hP G ε).parts.card = stepBound P.parts.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>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hPα' : stepBound P.parts.card ≤ Fintype.card α<GOAL>(increment hP G ε).parts.card = stepBound P.parts.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>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hPα' : stepBound P.parts.card ≤ Fintype.card α<VAR>hPpos : 0 < stepBound P.parts.card<GOAL>(increment hP G ε).parts.card = stepBound P.parts.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>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hPα' : stepBound P.parts.card ≤ Fintype.card α<VAR>hPpos : 0 < stepBound P.parts.card<GOAL>∑ A ∈ P.parts.attach, (chunk hP G ε ⋯).parts.card = stepBound P.parts.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>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hPα' : stepBound P.parts.card ≤ Fintype.card α<VAR>hPpos : 0 < stepBound P.parts.card<GOAL>∑ x ∈ (filter (fun x => (↑x).card = m * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card)) P.parts.attach).attach, (equitabilise ⋯).parts.card + ∑ x ∈ (filter (fun x => ¬(↑x).card = m * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card)) P.parts.attach).attach, (equitabilise ⋯).parts.card = stepBound P.parts.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>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hPα' : stepBound P.parts.card ≤ Fintype.card α<VAR>hPpos : 0 < stepBound P.parts.card<GOAL>(filter (fun x => (↑x).card = m * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card)) P.parts.attach).card * ?m.16076 + (filter (fun x => ¬(↑x).card = m * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card)) P.parts.attach).card * ?m.16115 = stepBound P.parts.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>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hPα' : stepBound P.parts.card ≤ Fintype.card α<VAR>hPpos : 0 < stepBound P.parts.card<GOAL>∀ x ∈ (filter (fun x => ¬(↑x).card = m * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card)) P.parts.attach).attach, (equitabilise ⋯).parts.card = ?m.16115
<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>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hPα' : stepBound P.parts.card ≤ Fintype.card α<VAR>hPpos : 0 < stepBound P.parts.card<GOAL>ℕ
<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>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hPα' : stepBound P.parts.card ≤ Fintype.card α<VAR>hPpos : 0 < stepBound P.parts.card<GOAL>∀ x ∈ (filter (fun x => (↑x).card = m * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card)) P.parts.attach).attach, (equitabilise ⋯).parts.card = ?m.16076
<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>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hPα' : stepBound P.parts.card ≤ Fintype.card α<VAR>hPpos : 0 < stepBound P.parts.card<GOAL>(filter (fun x => (↑x).card = m * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card)) P.parts.attach).card * (4 ^ P.parts.card - (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card) + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card)) + (filter (fun x => ¬(↑x).card = m * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card)) P.parts.attach).card * (4 ^ P.parts.card - (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card + 1) + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card + 1)) = stepBound P.parts.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>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hPα' : stepBound P.parts.card ≤ Fintype.card α<VAR>hPpos : 0 < stepBound P.parts.card<GOAL>((filter (fun x => (↑x).card = m * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card)) P.parts.attach).card + (filter (fun x => ¬(↑x).card = m * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card)) P.parts.attach).card) * 4 ^ P.parts.card = stepBound P.parts.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>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPG : ¬P.IsUniform G ε<VAR>hPα' : stepBound P.parts.card ≤ Fintype.card α<VAR>hPpos : 0 < stepBound P.parts.card<GOAL>(filter (fun x => (↑x).card = m * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card)) P.parts.attach).card + (filter (fun x => ¬(↑x).card = m * 4 ^ P.parts.card + (Fintype.card α / P.parts.card - m * 4 ^ P.parts.card)) P.parts.attach).card = P.parts.card
<VAR>θ : Angle<GOAL>θ.toReal = 0 ↔ θ = 0
<VAR>θ : Angle<GOAL>θ.toReal = toReal 0 ↔ θ = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>Xs Ys : ι → Set α<VAR>h : ∀ (i : ι), M.closure (Xs i) = M.closure (Ys i)<GOAL>M.closure (⋃ i, Xs i) = M.closure (⋃ i, Ys i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>x : α<VAR>hx : x ∈ closure (Set.range e)<GOAL>Tendsto (fun N => ↑(nearestPt e N) x) atTop (𝓝 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>x : α<VAR>hx : x ∈ closure (Set.range e)<VAR>ε : ℝ≥0∞<VAR>hε : 0 < ε<GOAL>∃ ia, True ∧ ∀ x_1 ∈ Set.Ici ia, ↑(nearestPt e x_1) x ∈ ball x ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>x : α<VAR>hx : x ∈ closure (Set.range e)<VAR>ε : ℝ≥0∞<VAR>hε : 0 < ε<VAR>N : ℕ<VAR>hN : edist x (e N) < ε<GOAL>∃ ia, True ∧ ∀ x_1 ∈ Set.Ici ia, ↑(nearestPt e x_1) x ∈ ball x ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>x : α<VAR>hx : x ∈ closure (Set.range e)<VAR>ε : ℝ≥0∞<VAR>hε : 0 < ε<VAR>N : ℕ<VAR>hN : edist (e N) x < ε<GOAL>∃ ia, True ∧ ∀ x_1 ∈ Set.Ici ia, ↑(nearestPt e x_1) x ∈ ball x ε
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>eval 0 (descPochhammer R n) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>μ (s ∆ t) = μ (s \ t) + μ (t \ s)
<VAR>R : Type u_1<VAR>inst✝⁹ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι'<VAR>inst✝¹ : DecidableEq ι'<VAR>inst✝ : IsEmpty ι<VAR>b : Basis ι R M<GOAL>b.det = AlternatingMap.constLinearEquivOfIsEmpty 1
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Nonempty α<VAR>s : Set α<VAR>h : ∀ (a : α), ∃ b ∈ s, a < b<VAR>inhabited_h : Inhabited α<VAR>f : ℕ → α := fun n => Nat.recOn n ⋯.choose fun x a => ⋯.choose<GOAL>s.Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Nonempty α<VAR>s : Set α<VAR>h : ∀ (a : α), ∃ b ∈ s, a < b<VAR>inhabited_h : Inhabited α<VAR>f : ℕ → α := fun n => Nat.recOn n ⋯.choose fun x a => ⋯.choose<VAR>hf : ∀ (n : ℕ), f n ∈ s<GOAL>s.Infinite
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>s : Set (Set A)<GOAL>zeroLocus 𝒜 (⋃ s' ∈ s, s') = ⋂ s' ∈ s, zeroLocus 𝒜 s'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p₁ p₂ : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>h₁ : HasFPowerSeriesAt f p₁ x<VAR>h₂ : HasFPowerSeriesAt f p₂ x<GOAL>HasFPowerSeriesAt 0 (p₁ - p₂) ?m.1179749
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<GOAL>IsCoprime I J ↔ Codisjoint I J
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<GOAL>(∃ a b, a * I + b * J = 1) ↔ I ⊔ J = ⊤
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>r : ℝ≥0∞<GOAL>infEdist x s < r ↔ ∃ y ∈ s, edist x y < r
<VAR>x y : ℝ*<VAR>hx : x.Infinitesimal<VAR>hy : y.Infinitesimal<GOAL>(x + y).Infinitesimal
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : Algebra F K<VAR>E : Type u_3<VAR>inst✝² : Ring E<VAR>inst✝¹ : Algebra F E<VAR>e : K ≃ₐ[F] E<VAR>inst✝ : Algebra.IsSeparable F K<VAR>x✝ : E<GOAL>IsSeparable F x✝
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : Algebra F K<VAR>E : Type u_3<VAR>inst✝² : Ring E<VAR>inst✝¹ : Algebra F E<VAR>e : K ≃ₐ[F] E<VAR>inst✝ : Algebra.IsSeparable F K<VAR>x✝ : E<GOAL>(minpoly F (e.symm x✝)).Separable
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hf : TendstoLocallyUniformlyOn F f φ U<VAR>hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∃ δ > 0, cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ✝ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hf : TendstoLocallyUniformlyOn F f φ U<VAR>hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>hKδ : cthickening δ K ⊆ U<GOAL>∃ δ > 0, cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ : α<VAR>l : List α<VAR>h : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.prev (l.next x hx) ⋯ = x
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>n : ℕ<VAR>hn : n < l.length<VAR>hx : l.nthLe n hn ∈ l<GOAL>l.prev (l.next (l.nthLe n hn) hx) ⋯ = l.nthLe n hn
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>n : ℕ<VAR>hn : n < l.length<VAR>hx : l.nthLe n hn ∈ l<GOAL>l.nthLe ((n + 1 + (l.length - 1)) % l.length) ⋯ = l.nthLe n hn
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝²⁰ : CommSemiring R<VAR>inst✝¹⁹ : CommSemiring S<VAR>inst✝¹⁸ : Algebra R S<VAR>inst✝¹⁷ : Semiring A<VAR>inst✝¹⁶ : Algebra R A<VAR>inst✝¹⁵ : Algebra S A<VAR>inst✝¹⁴ : IsScalarTower R S A<VAR>inst✝¹³ : Semiring B<VAR>inst✝¹² : Algebra R B<VAR>inst✝¹¹ : Algebra S B<VAR>inst✝¹⁰ : IsScalarTower R S B<VAR>inst✝⁹ : Semiring C<VAR>inst✝⁸ : Algebra R C<VAR>inst✝⁷ : Algebra S C<VAR>inst✝⁶ : IsScalarTower R S C<VAR>inst✝⁵ : Semiring D<VAR>inst✝⁴ : Algebra R D<VAR>inst✝³ : Semiring E<VAR>inst✝² : Algebra R E<VAR>inst✝¹ : Semiring F<VAR>inst✝ : Algebra R F<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<GOAL>(map f g).range = (includeLeft.comp f).range ⊔ (includeRight.comp g).range
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝²⁰ : CommSemiring R<VAR>inst✝¹⁹ : CommSemiring S<VAR>inst✝¹⁸ : Algebra R S<VAR>inst✝¹⁷ : Semiring A<VAR>inst✝¹⁶ : Algebra R A<VAR>inst✝¹⁵ : Algebra S A<VAR>inst✝¹⁴ : IsScalarTower R S A<VAR>inst✝¹³ : Semiring B<VAR>inst✝¹² : Algebra R B<VAR>inst✝¹¹ : Algebra S B<VAR>inst✝¹⁰ : IsScalarTower R S B<VAR>inst✝⁹ : Semiring C<VAR>inst✝⁸ : Algebra R C<VAR>inst✝⁷ : Algebra S C<VAR>inst✝⁶ : IsScalarTower R S C<VAR>inst✝⁵ : Semiring D<VAR>inst✝⁴ : Algebra R D<VAR>inst✝³ : Semiring E<VAR>inst✝² : Algebra R E<VAR>inst✝¹ : Semiring F<VAR>inst✝ : Algebra R F<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<GOAL>(map f g).range ≤ (includeLeft.comp f).range ⊔ (includeRight.comp g).range
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝²⁰ : CommSemiring R<VAR>inst✝¹⁹ : CommSemiring S<VAR>inst✝¹⁸ : Algebra R S<VAR>inst✝¹⁷ : Semiring A<VAR>inst✝¹⁶ : Algebra R A<VAR>inst✝¹⁵ : Algebra S A<VAR>inst✝¹⁴ : IsScalarTower R S A<VAR>inst✝¹³ : Semiring B<VAR>inst✝¹² : Algebra R B<VAR>inst✝¹¹ : Algebra S B<VAR>inst✝¹⁰ : IsScalarTower R S B<VAR>inst✝⁹ : Semiring C<VAR>inst✝⁸ : Algebra R C<VAR>inst✝⁷ : Algebra S C<VAR>inst✝⁶ : IsScalarTower R S C<VAR>inst✝⁵ : Semiring D<VAR>inst✝⁴ : Algebra R D<VAR>inst✝³ : Semiring E<VAR>inst✝² : Algebra R E<VAR>inst✝¹ : Semiring F<VAR>inst✝ : Algebra R F<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<GOAL>(includeLeft.comp f).range ⊔ (includeRight.comp g).range ≤ (map f g).range
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<VAR>n : ℕ<GOAL>⌊a - ↑n⌋ = ⌊a⌋ - ↑n
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>inst✝ : S.HasHomology<GOAL>S.cycles ≅ S.homology
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>inst✝ : S.HasHomology<VAR>this : IsIso S.homologyπ<GOAL>S.cycles ≅ S.homology
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>m : Multiset α<VAR>s : Finset α<GOAL>m.toFinset ⊆ s → m.prod = ∏ i ∈ s, i ^ Multiset.count i m
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>m : Multiset α<VAR>s : Finset α<VAR>l : List α<GOAL>Multiset.toFinset (Quot.mk Setoid.r l) ⊆ s → Multiset.prod (Quot.mk Setoid.r l) = ∏ i ∈ s, i ^ Multiset.count i (Quot.mk Setoid.r l)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommMonoid α<VAR>m : Multiset α<VAR>s : Finset α<VAR>l : List α<GOAL>(↑l).toFinset ⊆ s → l.prod = ∏ x ∈ s, x ^ List.count x l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>inst✝ : NoMaxOrder α<VAR>a b x : α<GOAL>Ioc a b ∈ 𝓝 x ↔ x ∈ Ioo a b
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝⁶ : PseudoEMetricSpace X<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MulAction G X<VAR>inst✝³ : IsometricSMul G X<VAR>inst✝² : PseudoEMetricSpace G<VAR>inst✝¹ : IsometricSMul G G<VAR>inst✝ : IsometricSMul Gᵐᵒᵖ G<VAR>a b c : G<GOAL>edist (a / b) (a / c) = edist b c
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : Generators R S<VAR>x y : S<GOAL>P.σ x • y = x * y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>inst✝ : DecidableEq α<VAR>a x✝ y✝ : α<VAR>h : a ∈ s(x✝, y✝)<GOAL>s(a, Mem.other' h) = s(x✝, y✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>inst✝ : DecidableEq α<VAR>a x✝ y✝ : α<VAR>h : a ∈ s(x✝, y✝)<VAR>h' : a = x✝ ∨ a = y✝<GOAL>s(a, Mem.other' h) = s(x✝, y✝)
<VAR>K : Type u_1<VAR>inst✝ : DivisionSemiring K<VAR>q : ℚ≥0<VAR>z : ℤ<VAR>hq : ↑q.num ≠ 0<GOAL>↑(q ^ z) = ↑q ^ z
<VAR>K : Type u_1<VAR>inst✝ : DivisionSemiring K<VAR>q : ℚ≥0<VAR>hq : ↑q.num ≠ 0<VAR>n : ℕ<GOAL>↑(q ^ ↑n) = ↑q ^ ↑n
<VAR>K : Type u_1<VAR>inst✝ : DivisionSemiring K<VAR>q : ℚ≥0<VAR>hq : ↑q.num ≠ 0<VAR>n : ℕ<GOAL>↑(q ^ (-↑n)) = ↑q ^ (-↑n)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E✝ B I✝ X R J I E : Set α<GOAL>uniqueBaseOn (I ∩ E) E = uniqueBaseOn I E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E✝ B I✝ X R J I E : Set α<GOAL>∀ I_1 ⊆ E, I_1 ⊆ I ∧ I_1 ⊆ E ↔ I_1 ⊆ I
<VAR>o : Ordinal.{u_1}<GOAL>ℵ₀ ≤ aleph' o ↔ ω ≤ o
<VAR>α : Type u_1<VAR>t t₁ t₂ : TopologicalSpace α<VAR>s : Set α<VAR>inst✝ : TopologicalSpace α<GOAL>DiscreteTopology α ↔ ∀ (x : α), {x} ∈ 𝓝 x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<VAR>h : f.Disjoint g<GOAL>(f * g).cycleFactorsFinset = f.cycleFactorsFinset ∪ g.cycleFactorsFinset
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<VAR>h : f.Disjoint g<GOAL>(∀ f_1 ∈ f.cycleFactorsFinset ∪ g.cycleFactorsFinset, f_1.IsCycle) ∧ ∃ (h : (↑(f.cycleFactorsFinset ∪ g.cycleFactorsFinset)).Pairwise Disjoint), (f.cycleFactorsFinset ∪ g.cycleFactorsFinset).noncommProd id ⋯ = f * g
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>ifp_succ_n : IntFractPair K<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<GOAL>1 ≤ ifp_succ_n.b
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>ifp_n : IntFractPair K<VAR>nth_stream_eq : IntFractPair.stream v n = some ifp_n<VAR>stream_nth_fr_ne_zero : ifp_n.fr ≠ 0<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)<GOAL>1 ≤ (IntFractPair.of ifp_n.fr⁻¹).b
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>ifp_n : IntFractPair K<VAR>nth_stream_eq : IntFractPair.stream v n = some ifp_n<VAR>stream_nth_fr_ne_zero : ifp_n.fr ≠ 0<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)<GOAL>1 ≤ ifp_n.fr⁻¹
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>ifp_n : IntFractPair K<VAR>nth_stream_eq : IntFractPair.stream v n = some ifp_n<VAR>stream_nth_fr_ne_zero : ifp_n.fr ≠ 0<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)<GOAL>ifp_n.fr ≤ 1
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a b p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<GOAL>p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a b p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<GOAL>p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a b p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>ha0 : p.count a.factors = 0<GOAL>p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a b p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>ha : ¬a = 0<VAR>hb : ¬b = 0<VAR>hb0 : p.count b.factors = 0<GOAL>p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors
<VAR>f : ℕ → ℕ<VAR>hf : Nat.Primrec f<GOAL>Partrec ↑f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : MulActionWithZero 𝕜 E<VAR>x y : E<GOAL>1 • x + 0 • y = x