ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>inst✝¹ : Fintype F<VAR>inst✝ : Field F<VAR>hF : ringChar F ≠ 2<VAR>hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0<VAR>n : ℕ+<VAR>hp : Nat.Prime (ringChar F)<VAR>hc : Fintype.card F = ringChar F ^ ↑n<VAR>FF : Type u_1 := CyclotomicField 8 F<VAR>hchar : ringChar F = ringChar FF<VAR>FFp : Nat.Prime (ringChar FF)<VAR>this : Fact (Nat.Prime (ringChar FF))<VAR>hFF : ringChar FF ≠ 2<VAR>hu : IsUnit ↑(ringChar FF)<VAR>ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯<VAR>ψ₈char : AddChar (ZMod 8) FF := ψ₈.char<VAR>τ : FF := ψ₈char 1<VAR>τ_spec : τ ^ 4 = -1<VAR>χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)<VAR>hχ : χ (-1) = 1<VAR>hq : χ.IsQuadratic<VAR>h₁ : (fun a => ↑(χ₈ a) * τ ^ ↑a) = fun a => χ a * ψ₈char a<VAR>hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)<VAR>hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))<VAR>h : ↑8 ^ (Fintype.card F / 2) = χ ↑(Fintype.card F)<GOAL>(algebraMap F FF) (8 ^ (Fintype.card F / 2)) = (algebraMap F FF) ↑(χ₈ ↑(Fintype.card F))
<VAR>p : ℕ<VAR>q : ℚ<VAR>hp : p ≠ 1<VAR>hq : q ≠ 0<GOAL>(multiplicity p q.den).Dom
<VAR>p : ℕ<VAR>q : ℚ<VAR>hp : p ≠ 1<VAR>hq : q ≠ 0<GOAL>p ≠ 1 ∧ 0 < q.den
<VAR>p : ℕ<VAR>q : ℚ<VAR>hp : p ≠ 1<VAR>hq : q ≠ 0<GOAL>padicValRat p q = ↑((multiplicity (↑p) q.num).get ⋯) - ↑((multiplicity p q.den).get ⋯)
<VAR>p : ℕ<VAR>q : ℚ<VAR>hp : p ≠ 1<VAR>hq : q ≠ 0<GOAL>q.num ≠ 0
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b✝ c✝ u a : αˣ<VAR>b c : α<VAR>h : b * ↑a = c * ↑a<GOAL>b = c
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>β : Type u_3<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : l.NeBot<VAR>f : α → β<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>hfm : ∀ (i : ι), AEStronglyMeasurable f (μ.restrict (φ i))<GOAL>AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>β : Type u_3<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : l.NeBot<VAR>f : α → β<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>hfm : ∀ (i : ι), AEStronglyMeasurable f (μ.restrict (φ i))<VAR>u : ℕ → ι<VAR>hu : Tendsto u atTop l<GOAL>AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>β : Type u_3<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : l.NeBot<VAR>f : α → β<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>hfm : ∀ (i : ι), AEStronglyMeasurable f (μ.restrict (φ i))<VAR>u : ℕ → ι<VAR>hu : Tendsto u atTop l<VAR>this : AEStronglyMeasurable f (μ.restrict (⋃ i, φ (u i)))<GOAL>AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>β : Type u_3<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : l.NeBot<VAR>f : α → β<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>hfm : ∀ (i : ι), AEStronglyMeasurable f (μ.restrict (φ i))<VAR>u : ℕ → ι<VAR>hu : Tendsto u atTop l<VAR>this : AEStronglyMeasurable f (μ.restrict (⋃ i, φ (u i)))<GOAL>∀ᵐ (x : α) ∂μ, x ∈ ⋃ i, φ (u i)
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>inhabited_h✝ : Inhabited X<VAR>inhabited_h : Inhabited Y<VAR>A : ∀ (p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)), ⟦p⟧ = toGHSpace X → ⟦q⟧ = toGHSpace Y → hausdorffDist ↑p ↑q < diam univ + 1 + diam univ → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q<VAR>B : ∀ (p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)), ⟦p⟧ = toGHSpace X → ⟦q⟧ = toGHSpace Y → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q<GOAL>hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>inhabited_h✝ : Inhabited X<VAR>inhabited_h : Inhabited Y<VAR>A : ∀ (p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)), ⟦p⟧ = toGHSpace X → ⟦q⟧ = toGHSpace Y → hausdorffDist ↑p ↑q < diam univ + 1 + diam univ → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q<VAR>B : ∀ (p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)), ⟦p⟧ = toGHSpace X → ⟦q⟧ = toGHSpace Y → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q<GOAL>hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ ghDist X Y
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>inhabited_h✝ : Inhabited X<VAR>inhabited_h : Inhabited Y<VAR>A : ∀ (p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)), ⟦p⟧ = toGHSpace X → ⟦q⟧ = toGHSpace Y → hausdorffDist ↑p ↑q < diam univ + 1 + diam univ → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q<VAR>B : ∀ (p q : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)), ⟦p⟧ = toGHSpace X → ⟦q⟧ = toGHSpace Y → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q<GOAL>ghDist X Y ≤ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>f : α →₀ ℕ<VAR>a : α<GOAL>((fun s => { support := s.toFinset, toFun := fun a => count a s, mem_support_toFun := ⋯ }) ((fun f => Finsupp.toMultiset f) f)) a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>f : α →₀ ℕ<VAR>a : α<GOAL>f a = 0 → 0 = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<GOAL>(fun f => Finsupp.toMultiset f) ((fun s => { support := s.toFinset, toFun := fun a => count a s, mem_support_toFun := ⋯ }) s) = s
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K : ℝ<VAR>hK : 0 < K<GOAL>∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x r) ≤ ↑(scalingConstantOf μ K⁻¹) * μ (closedBall x (K * r))
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>K : ℝ<VAR>hK : 0 < K<VAR>x✝ : ℝ<VAR>a✝ : α<GOAL>x✝ = K⁻¹ * (K * x✝)
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x✝ : α (last n)<VAR>q : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.castSucc<VAR>i : Fin n<VAR>y : α i.castSucc<VAR>z : α (last n)<VAR>P : ((i : Fin (n + 1)) → α i) → Sort u_1<VAR>h : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → P (snoc x x₀)<VAR>x : (i : Fin n) → init α i<VAR>x₀ : α (last n)<GOAL>snocCases h (snoc x x₀) = h x x₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : ↥(Lp β 1 μ)<GOAL>Integrable (↑↑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : ↥(Lp β 1 μ)<GOAL>Memℒp (↑↑f) 1 μ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<GOAL>IsTotallyDisconnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<GOAL>(∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1) ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
<VAR>A : Type u_1<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>n k l : A<VAR>h : (k, l) ∈ antidiagonal n<GOAL>(fun x => ⟨x.1 + x.2, ⟨x, ⋯⟩⟩) ((fun x => ↑x.snd) ⟨n, ⟨(k, l), h⟩⟩) = ⟨n, ⟨(k, l), h⟩⟩
<VAR>A : Type u_1<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>n k l : A<VAR>h✝ : (k, l) ∈ antidiagonal n<VAR>h : (k, l).1 + (k, l).2 = n<GOAL>(fun x => ⟨x.1 + x.2, ⟨x, ⋯⟩⟩) ((fun x => ↑x.snd) ⟨n, ⟨(k, l), h✝⟩⟩) = ⟨n, ⟨(k, l), h✝⟩⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : OrderedCommMonoid α<VAR>s t : Multiset α<VAR>a : α<VAR>h : ∀ x ∈ s, a ≤ x<GOAL>a ^ card s ≤ s.prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : OrderedCommMonoid α<VAR>s t : Multiset α<VAR>a : α<VAR>h : ∀ x ∈ s, a ≤ x<GOAL>(map (Function.const α a) s).prod ≤ s.prod
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<GOAL>‖f‖ = ⨆ x, ‖f x‖
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a + x) ⁻¹' Ico b c = Ico (b - a) (c - a)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : Decidable (IsField A)<GOAL>⊤ᵛ = if IsField A then ⊤ else ⊥
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : Decidable (IsField A)<GOAL>IsField A ↔ restrictScalars A (LinearMap.range (Algebra.trace K L)) ≤ 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : Decidable (IsField A)<GOAL>⊤ ≤ (algebraMap A K).range ↔ restrictScalars A ⊤ ≤ 1
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁴ : Preorder α✝<VAR>inst✝³ : Preorder β✝<VAR>inst✝² : Preorder γ<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝¹ : Unique α<VAR>inst✝ : Preorder β<GOAL>∀ {a b : α → β}, (Equiv.funUnique α β) a ≤ (Equiv.funUnique α β) b ↔ a ≤ b
<VAR>m n : ℤ<GOAL>Odd (m + n) ↔ (Odd n ↔ Even m)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<VAR>h₁ : ¬a ∈ l₁<GOAL>l₁.erase a ~ l₂.erase a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<VAR>h₁ : ¬a ∈ l₁<VAR>h₂ : ¬a ∈ l₂<GOAL>l₁.erase a ~ l₂.erase a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<VAR>h₁ : ¬a ∈ l₁<VAR>h₂ : ¬a ∈ l₂<GOAL>l₁ ~ l₂
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Finite α<VAR>l : List (Perm α)<VAR>h1 : ∀ σ ∈ l, σ.IsCycle<VAR>h2 : List.Pairwise Disjoint l<VAR>σ : Perm α<GOAL>σ ∈ l ↔ σ.IsCycle ∧ ∀ (a : α), σ a ≠ a → σ a = l.prod a
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Finite α<VAR>l : List (Perm α)<VAR>h1 : ∀ σ ∈ l, σ.IsCycle<VAR>h2 : List.Pairwise Disjoint l<VAR>σ : Perm α<GOAL>σ.IsCycle → (σ ∈ l ↔ ∀ (a : α), σ a ≠ a → σ a = l.prod a)
<VAR>V : Type u_1<VAR>inst✝¹ : Category.{?u.8253, u_1} V<VAR>inst✝ : Abelian V<VAR>X Y Z : Vᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>w : f ≫ g = 0<GOAL>g.unop ≫ f.unop = 0
<VAR>V : Type u_1<VAR>inst✝¹ : Category.{?u.8253, u_1} V<VAR>inst✝ : Abelian V<VAR>X Y Z : Vᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>w : f ≫ g = 0<GOAL>f ≫ factorThruImage g = 0
<VAR>V : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} V<VAR>inst✝ : Abelian V<VAR>X Y Z : Vᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>w : f ≫ g = 0<GOAL>imageToKernel g.unop f.unop ⋯ ≫ (kernelSubobject f.unop).arrow = ((imageSubobjectIso g.unop ≪≫ (imageUnopOp g).unop.symm).hom ≫ (cokernel.desc f (factorThruImage g) ⋯).unop ≫ (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f).inv) ≫ (kernelSubobject f.unop).arrow
<VAR>R✝ : Type u<VAR>ι : Type u_1<VAR>inst✝² : CommSemiring R✝<VAR>I✝ J✝ K L : Ideal R✝<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>I J : Ideal R<VAR>h : I = ⊥ ∨ J = ⊥<GOAL>I * J = ⊥
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : TotalComplexShape c₁ c₂ c₁₂<VAR>I : Type u_4<VAR>inst✝¹ : AddMonoid I<VAR>c : ComplexShape I<VAR>inst✝ : c.TensorSigns<VAR>i₁✝ i₁'✝ i₂✝ i₂'✝ : I<VAR>h : c.Rel i₁✝ i₁'✝<VAR>x✝ : c.Rel i₂✝ i₂'✝<GOAL>c.ε i₁✝ * 1 = -1 * c.ε i₁'✝
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝³ : SMul R ℝ≥0<VAR>inst✝² : SMul R ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>μ ν : FiniteMeasure Ω<GOAL>⇑(μ + ν) = ⇑μ + ⇑ν
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝³ : SMul R ℝ≥0<VAR>inst✝² : SMul R ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>μ ν : FiniteMeasure Ω<VAR>x✝ : Set Ω<GOAL>(μ + ν) x✝ = (⇑μ + ⇑ν) x✝
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝³ : SMul R ℝ≥0<VAR>inst✝² : SMul R ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>μ ν : FiniteMeasure Ω<VAR>x✝ : Set Ω<GOAL>↑(μ + ν) x✝ = ↑μ x✝ + ↑ν x✝
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>p : FreeAddMonoid (R × ((i : ι) → s i))<GOAL>↑p = (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum
<VAR>α : Type u<VAR>β : Type u_1<VAR>n : ℕ<VAR>x : α<VAR>inst✝ : StrictOrderedRing α<VAR>hx : x + 1 < 0<VAR>hn : 1 < n<GOAL>if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>n : ℕ<VAR>x : α<VAR>inst✝ : StrictOrderedRing α<VAR>hx : x + 1 < 0<VAR>hn : 1 < n<VAR>hx0 : x < 0<GOAL>if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>n : ℕ<VAR>x : α<VAR>inst✝ : StrictOrderedRing α<VAR>hx : x + 1 < 0<VAR>hn : 1 < n<VAR>hx0 : x < 0<GOAL>if Even 2 then ∑ i ∈ range 2, x ^ i < 0 else 1 < ∑ i ∈ range 2, x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>n : ℕ<VAR>x : α<VAR>inst✝ : StrictOrderedRing α<VAR>hx : x + 1 < 0<VAR>hn : 1 < n<VAR>hx0 : x < 0<GOAL>∀ (n : ℕ), 2 ≤ n → (if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i) → if Even (n + 1) then ∑ i ∈ range (n + 1), x ^ i < 0 else 1 < ∑ i ∈ range (n + 1), x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>n✝ : ℕ<VAR>x : α<VAR>inst✝ : StrictOrderedRing α<VAR>hx : x + 1 < 0<VAR>hx0 : x < 0<VAR>n : ℕ<VAR>hmn✝ : 2 ≤ n<VAR>ihn : if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i<GOAL>if Even (n + 1) then ∑ i ∈ range (n + 1), x ^ i < 0 else 1 < ∑ i ∈ range (n + 1), x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>n✝ : ℕ<VAR>x : α<VAR>inst✝ : StrictOrderedRing α<VAR>hx : x + 1 < 0<VAR>hx0 : x < 0<VAR>n : ℕ<VAR>hmn✝ : 2 ≤ n<VAR>ihn : if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i<GOAL>if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 < 0 else 1 < x * ∑ i ∈ range n, x ^ i + 1
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<GOAL>a + 1 ≤ 4 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>h : 1 ≤ 4 ^ P.parts.card<GOAL>a + 1 ≤ 4 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>h : 1 ≤ 4 ^ P.parts.card<GOAL>Fintype.card α / P.parts.card - Fintype.card α / P.parts.card / 4 ^ P.parts.card * 4 ^ P.parts.card + 1 ≤ 4 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>h : 1 ≤ 4 ^ P.parts.card<GOAL>Fintype.card α / P.parts.card - Fintype.card α / P.parts.card / 4 ^ P.parts.card * 4 ^ P.parts.card + 1 ≤ 4 ^ P.parts.card - 1 + 1
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>h : 1 ≤ 4 ^ P.parts.card<GOAL>Fintype.card α / P.parts.card ≤ Fintype.card α / P.parts.card / 4 ^ P.parts.card * 4 ^ P.parts.card + 4 ^ P.parts.card - 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>0 < asympBound g a b n
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>1 - 2⁻¹ = 2⁻¹
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ x✝ y : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<VAR>x : V<VAR>hx : x ∈ (p.dropUntil u h).support<GOAL>x ∈ p.support
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ x✝ y : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<VAR>x : V<VAR>hx : x ∈ (p.dropUntil u h).support<GOAL>x ∈ (p.takeUntil u h).support ∨ x ∈ (p.dropUntil u h).support
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>x : G<VAR>n✝ : ℕ<VAR>a : G<VAR>n : ℕ<GOAL>a ^ (n % card G) = a ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MulOneClass α<VAR>inst✝¹ : LE α<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a * b ≤ b<GOAL>a * b ≤ 1 * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<GOAL>∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<VAR>this : IsFiniteKernel κ<GOAL>∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>this : IsFiniteKernel κ<VAR>S : Finset (Set γ)<VAR>hS_subset : ↑S ⊆ countablePartition γ n<VAR>hA : MeasurableSet (⋃₀ ↑S)<GOAL>∫ (x : γ) in ⋃₀ ↑S, κ.densityProcess ν n a x s ∂ν a = ((κ a) (⋃₀ ↑S ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>this : IsFiniteKernel κ<VAR>S : Finset (Set γ)<VAR>hS_subset : ↑S ⊆ countablePartition γ n<VAR>hA : MeasurableSet (⋃₀ ↑S)<GOAL>∫ (x : γ) in ⋃ i, ↑i, κ.densityProcess ν n a x s ∂ν a = ((κ a) ((⋃ i, ↑i) ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>this : IsFiniteKernel κ<VAR>S : Finset (Set γ)<VAR>hS_subset : ↑S ⊆ countablePartition γ n<VAR>hA : MeasurableSet (⋃₀ ↑S)<VAR>h_disj : Pairwise (Disjoint on fun i => ↑i)<GOAL>∫ (x : γ) in ⋃ i, ↑i, κ.densityProcess ν n a x s ∂ν a = ((κ a) ((⋃ i, ↑i) ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>this : IsFiniteKernel κ<VAR>S : Finset (Set γ)<VAR>hS_subset : ↑S ⊆ countablePartition γ n<VAR>hA : MeasurableSet (⋃₀ ↑S)<VAR>h_disj : Pairwise (Disjoint on fun i => ↑i)<GOAL>∑' (n_1 : ↑↑S), ∫ (x : γ) in ↑n_1, κ.densityProcess ν n a x s ∂ν a = ∑' (a_1 : ↑↑S), ((κ a) (↑a_1 ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>this : IsFiniteKernel κ<VAR>S : Finset (Set γ)<VAR>hS_subset : ↑S ⊆ countablePartition γ n<VAR>hA : MeasurableSet (⋃₀ ↑S)<VAR>h_disj : Pairwise (Disjoint on fun i => ↑i)<GOAL>Pairwise (Disjoint on fun i => ↑i ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>this : IsFiniteKernel κ<VAR>S : Finset (Set γ)<VAR>hS_subset : ↑S ⊆ countablePartition γ n<VAR>hA : MeasurableSet (⋃₀ ↑S)<VAR>h_disj : Pairwise (Disjoint on fun i => ↑i)<GOAL>∀ (i : ↑↑S), MeasurableSet (↑i ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>this : IsFiniteKernel κ<VAR>S : Finset (Set γ)<VAR>hS_subset : ↑S ⊆ countablePartition γ n<VAR>hA : MeasurableSet (⋃₀ ↑S)<VAR>h_disj : Pairwise (Disjoint on fun i => ↑i)<GOAL>∀ (i : ↑↑S), MeasurableSet ↑i