ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>n : ℕ<GOAL>((Γ₀.splitting X).desc (op [n]) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op [n])).inj A) ≫ PInfty.f n = PInfty.f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>n : ℕ<GOAL>∀ (A : Splitting.IndexSet (op [n])), ((Γ₀.splitting X).cofan (op [n])).inj A ≫ ((Γ₀.splitting X).desc (op [n]) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op [n])).inj A) ≫ PInfty.f n = ((Γ₀.splitting X).cofan (op [n])).inj A ≫ PInfty.f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>n : ℕ<VAR>A : Splitting.IndexSet (op [n])<GOAL>((Γ₀.splitting X).cofan (op [n])).inj A ≫ ((Γ₀.splitting X).desc (op [n]) fun A => 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op [n])).inj A) ≫ PInfty.f n = ((Γ₀.splitting X).cofan (op [n])).inj A ≫ PInfty.f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>n : ℕ<VAR>A : Splitting.IndexSet (op [n])<GOAL>𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op [n])).inj A ≫ PInfty.f n = ((Γ₀.splitting X).cofan (op [n])).inj A ≫ PInfty.f n
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>hb : head s₁ = head s₂<VAR>ht : last s₁ = last s₂<VAR>hs₁0 : s₁.length = 0<GOAL>s₁ = s₂
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>hb : head s₁ = head s₂<VAR>ht : last s₁ = last s₂<VAR>hs₁0 : s₁.length = 0<VAR>this : ∀ (x : X), x ∈ s₁ ↔ x = last s₁<GOAL>s₁ = s₂
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>hb : head s₁ = head s₂<VAR>ht : last s₁ = last s₂<VAR>hs₁0 : s₁.length = 0<VAR>this✝ : ∀ (x : X), x ∈ s₁ ↔ x = last s₁<VAR>this : ∀ (x : X), x ∈ s₂ ↔ x = last s₂<GOAL>s₁ = s₂
<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>inst✝¹ : MeasurableSpace β<VAR>f✝ f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>hx : f x ∈ closure s<VAR>this : Nonempty ↑s<GOAL>Tendsto (fun n => ↑(approxOn f hf s y₀ h₀ n) x) atTop (𝓝 (f 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>inst✝¹ : MeasurableSpace β<VAR>f✝ f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>this : Nonempty ↑s<VAR>hx : f x ∈ closure (Subtype.val '' closure (Set.range (denseSeq ↑s)))<GOAL>Tendsto (fun n => ↑(approxOn f hf s y₀ h₀ n) x) atTop (𝓝 (f 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>inst✝¹ : MeasurableSpace β<VAR>f✝ f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>this : Nonempty ↑s<VAR>hx : f x ∈ closure (Subtype.val '' closure (Set.range (denseSeq ↑s)))<GOAL>Tendsto (fun n => (↑(nearestPt (fun k => Nat.casesOn k y₀ (Subtype.val ∘ denseSeq ↑s)) n) ∘ f) x) atTop (𝓝 (f 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>inst✝¹ : MeasurableSpace β<VAR>f✝ f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>this : Nonempty ↑s<VAR>hx : f x ∈ closure (Subtype.val '' closure (Set.range (denseSeq ↑s)))<GOAL>Subtype.val '' closure (Set.range (denseSeq ↑s)) ⊆ closure (Set.range fun k => Nat.casesOn k y₀ (Subtype.val ∘ denseSeq ↑s))
<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>inst✝¹ : MeasurableSpace β<VAR>f✝ f : β → α<VAR>hf : Measurable f<VAR>s : Set α<VAR>y₀ : α<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>this : Nonempty ↑s<VAR>hx : f x ∈ closure (Subtype.val '' closure (Set.range (denseSeq ↑s)))<GOAL>Subtype.val '' closure (Set.range (denseSeq ↑s)) ⊆ closure {y₀} ∪ closure (Subtype.val '' Set.range (denseSeq ↑s))
<VAR>c : Char<VAR>cs t : List Char<VAR>i : Nat<VAR>e : Pos<GOAL>go₁ (c :: cs ++ t) { byteIdx := i } { byteIdx := utf8Len (c :: cs) + i } e = go₂ t { byteIdx := utf8Len (c :: cs) + i } e
<VAR>c : Char<VAR>cs t : List Char<VAR>i : Nat<VAR>e : Pos<GOAL>go₁ (cs ++ t) { byteIdx := i + c.utf8Size } { byteIdx := utf8Len cs + c.utf8Size + i } e = go₂ t { byteIdx := utf8Len cs + c.utf8Size + i } e
<VAR>c : Char<VAR>cs t : List Char<VAR>i : Nat<VAR>e : Pos<GOAL>utf8Len cs + c.utf8Size + i = utf8Len cs + (i + c.utf8Size)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x✝ : Z<VAR>e' : Trivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b✝ : B<VAR>y : E b✝<VAR>e₁ e₂ : Trivialization F proj<VAR>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<VAR>x : F<GOAL>(b, e₁.coordChange e₂ b x) = ↑e₂ (↑e₁.symm (b, x))
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x✝ : Z<VAR>e' : Trivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b✝ : B<VAR>y : E b✝<VAR>e₁ e₂ : Trivialization F proj<VAR>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<VAR>x : F<GOAL>(b, e₁.coordChange e₂ b x).1 = (↑e₂ (↑e₁.symm (b, x))).1
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x✝ : Z<VAR>e' : Trivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b✝ : B<VAR>y : E b✝<VAR>e₁ e₂ : Trivialization F proj<VAR>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<VAR>x : F<GOAL>proj (↑e₁.symm (b, x)) ∈ e₁.baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x✝ : Z<VAR>e' : Trivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b✝ : B<VAR>y : E b✝<VAR>e₁ e₂ : Trivialization F proj<VAR>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<VAR>x : F<GOAL>proj (↑e₁.symm (b, x)) ∈ e₂.baseSet
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>f : γ → α<GOAL>UniformContinuous fun g => ofFun (toFun g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>f : γ → α<GOAL>∀ ib ∈ 𝓤 β, ∃ ia ∈ 𝓤 β, ∀ x ∈ UniformFun.gen α β ia, (ofFun (toFun x.1 ∘ f), ofFun (toFun x.2 ∘ f)) ∈ UniformFun.gen γ β ib
<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✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<VAR>a : α<GOAL>_root_.Disjoint a (s.sup f) ↔ ∀ ⦃i : ι⦄, i ∈ s → _root_.Disjoint a (f i)
<VAR>ι : Type u_2<VAR>α✝ : ι → Type ?u.38171<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α✝ i)<VAR>s t : Set ((i : ι) → α✝ i)<VAR>α : ι → Type u_1<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<GOAL>univ ∈ measurableCylinders α
<VAR>ι : Type u_2<VAR>α✝ : ι → Type ?u.38171<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α✝ i)<VAR>s t : Set ((i : ι) → α✝ i)<VAR>α : ι → Type u_1<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<GOAL>∅ᶜ ∈ measurableCylinders α
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : Preadditive C<VAR>J : Type<VAR>inst✝² : Fintype J<VAR>f✝ : J → C<VAR>inst✝¹ : HasBiproduct f✝<VAR>inst✝ : HasFiniteBiproducts C<VAR>f g : J → C<VAR>h : (j : J) → f j ⟶ g j<VAR>j✝¹ j✝ : J<GOAL>ι f j✝ ≫ map h ≫ π g j✝¹ = ι f j✝ ≫ (∑ j : J, π f j ≫ h j ≫ ι g j) ≫ π g j✝¹
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>g : β → α<VAR>hfg : LeftInverse g f<VAR>F : Filter α<GOAL>comap f (comap g F) = F
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>I P : Ideal R<VAR>hP : P.IsPrime<VAR>n : ℕ<VAR>h : I ^ n ≤ P<VAR>hP0 : ¬P = ⊥<GOAL>I ≤ P
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>I P : Ideal R<VAR>hP : P.IsPrime<VAR>n : ℕ<VAR>h : P ∣ I ^ n<VAR>hP0 : ¬P = ⊥<GOAL>P ∣ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<GOAL>f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>(fun x => a + x) '' Ici b = Ici (a + b)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>a✝ : Nontrivial R<VAR>h : IsField R[X]<VAR>this : Field R[X] := h.toField<GOAL>False
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁶ : Category.{max v u, w} D<VAR>inst✝⁵ : ConcreteCategory D<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<VAR>F G : Sheaf J D<VAR>f : F ⟶ G<VAR>m : Mono f.val<GOAL>Mono f
<VAR>α : Type u_1<VAR>n : ℕ<VAR>l : List α<VAR>s : Multiset α<GOAL>∀ (a : List α), ⟦a⟧ ∈ powersetCardAux n l ↔ ⟦a⟧ ≤ ↑l ∧ card ⟦a⟧ = n
<VAR>α : Type u_1<VAR>n : ℕ<VAR>l : List α<VAR>s : Multiset α<GOAL>∀ (a : List α), (∃ a_1, (a_1 <+ l ∧ a_1.length = n) ∧ a_1 ~ a) ↔ (∃ l_1, l_1 ~ a ∧ l_1 <+ l) ∧ a.length = n
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l r : List α<VAR>i : ℕ<VAR>h1 : l.length - 1 - i < (l.reverseAux r).length<VAR>h2 : i < l.length<GOAL>(l.reverseAux r).get ⟨l.length - 1 - i, h1⟩ = l.get ⟨i, h2⟩
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ι : Type u_3<VAR>p : ι → Prop<VAR>t : ι → Set X<VAR>s : Set X<VAR>inst✝ : DiscreteTopology ↑s<VAR>x : X<VAR>hb : (𝓝 x).HasBasis p t<VAR>hx : x ∈ s<GOAL>∃ i, p i ∧ t i ∩ s = {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ι : Type u_3<VAR>p : ι → Prop<VAR>t : ι → Set X<VAR>s : Set X<VAR>inst✝ : DiscreteTopology ↑s<VAR>x : X<VAR>hb : (𝓝 x).HasBasis p t<VAR>hx : x ∈ s<VAR>i : ι<VAR>hi : p i<VAR>hix : t i ∩ s ⊆ {x}<GOAL>∃ i, p i ∧ t i ∩ s = {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace ℝ E'<VAR>T S : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>hS : S.IsSymmetric<VAR>x y : E<GOAL>⟪(T + S) x, y⟫_𝕜 = ⟪x, (T + S) y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace ℝ E'<VAR>T S : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>hS : S.IsSymmetric<VAR>x y : E<GOAL>⟪x, T y + S y⟫_𝕜 = ⟪x, (T + S) y⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>h : xs ⊆ ys<GOAL>(xs ++ ys).dedup = ys.dedup
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u_1<VAR>Q : α → Prop<VAR>u v : α → Cofix F<VAR>h : ∀ (x : α), Q x → ∃ a f f', (u x).dest = abs ⟨a, f⟩ ∧ (v x).dest = abs ⟨a, f'⟩ ∧ ∀ (i : (P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'<VAR>x✝¹ : α<VAR>Qx : Q x✝¹<VAR>R : Cofix F → Cofix F → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'<VAR>x y : Cofix F<VAR>x✝ : R x y<VAR>x' : α<VAR>Qx' : Q x'<VAR>xeq : x = u x'<VAR>yeq : y = v x'<VAR>a : (P F).A<VAR>f f' : (P F).B a → Cofix F<VAR>ux'eq : (u x').dest = abs ⟨a, f⟩<VAR>vx'eq : (v x').dest = abs ⟨a, f'⟩<VAR>h' : ∀ (i : (P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'<GOAL>Liftr R x.dest y.dest
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u_1<VAR>Q : α → Prop<VAR>u v : α → Cofix F<VAR>h : ∀ (x : α), Q x → ∃ a f f', (u x).dest = abs ⟨a, f⟩ ∧ (v x).dest = abs ⟨a, f'⟩ ∧ ∀ (i : (P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'<VAR>x✝¹ : α<VAR>Qx : Q x✝¹<VAR>R : Cofix F → Cofix F → Prop := fun w z => ∃ x', Q x' ∧ w = u x' ∧ z = v x'<VAR>x y : Cofix F<VAR>x✝ : R x y<VAR>x' : α<VAR>Qx' : Q x'<VAR>xeq : x = u x'<VAR>yeq : y = v x'<VAR>a : (P F).A<VAR>f f' : (P F).B a → Cofix F<VAR>ux'eq : (u x').dest = abs ⟨a, f⟩<VAR>vx'eq : (v x').dest = abs ⟨a, f'⟩<VAR>h' : ∀ (i : (P F).B a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x'<GOAL>∃ a f₀ f₁, x.dest = abs ⟨a, f₀⟩ ∧ y.dest = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), R (f₀ i) (f₁ i)
<VAR>m : ℕ<VAR>n : ℕ∞<GOAL>↑m < ↑n ↔ ↑m < n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>T : Set α → F →L[ℝ] F'<VAR>f : α →ₛ F<GOAL>∑ x ∈ filter (fun x => x ≠ 0) f.range, (T (↑f ⁻¹' {x})) x = setToSimpleFunc T f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>T : Set α → F →L[ℝ] F'<VAR>f : α →ₛ F<VAR>x : F<VAR>x✝ : x ∈ f.range<VAR>hx0 : x = 0<GOAL>(T (↑f ⁻¹' {x})) x = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>T : Set α → F →L[ℝ] F'<VAR>f : α →ₛ F<VAR>x : F<VAR>x✝ : x ∈ f.range<VAR>hx0 : x = 0<GOAL>(T (↑f ⁻¹' {0})) 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<GOAL>∀ b ∈ {a | ∀ᶠ (n : α) in ⊤, a ≤ n}, b ≤ ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<GOAL>∀ (b : α), (∀ (x : α), b ≤ x) → b = ⊥
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : CommMonoid P<VAR>f : M →* P<VAR>g : N →* P<VAR>x : M<GOAL>((f.coprod g).comp (inl M N)) x = f x
<VAR>α : Type u_1<VAR>inst✝⁴ : UniformSpace α<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace β<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace γ<VAR>f✝ : α → β<VAR>inst✝¹ : CompleteSpace γ<VAR>inst✝ : T0Space γ<VAR>f : β → γ<VAR>g : α → β<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<VAR>a : α<GOAL>(Completion.extension f ∘ Completion.map g) (↑α a) = Completion.extension (f ∘ g) (↑α a)
<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : HasZeroMorphisms V<VAR>inst✝¹ : HasZeroObject V<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A B : V<VAR>f : A ⟶ B<GOAL>(if h : j = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) = (singleObjXSelf c j A).hom ≫ f ≫ (singleObjXSelf c j B).inv
<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : HasZeroMorphisms V<VAR>inst✝¹ : HasZeroObject V<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A B : V<VAR>f : A ⟶ B<GOAL>eqToHom ⋯ ≫ f ≫ eqToHom ⋯ = (singleObjXSelf c j A).hom ≫ f ≫ (singleObjXSelf c j B).inv
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>c : σ → K<GOAL>indicator c ∈ restrictDegree σ K (Fintype.card K - 1)
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>c : σ → K<GOAL>∀ (i : σ), Multiset.count i (∏ n : σ, (1 - (X n - C (c n)) ^ (Fintype.card K - 1))).degrees ≤ Fintype.card K - 1
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>c : σ → K<VAR>n : σ<GOAL>Multiset.count n (∏ n : σ, (1 - (X n - C (c n)) ^ (Fintype.card K - 1))).degrees ≤ Fintype.card K - 1
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>c : σ → K<VAR>n : σ<GOAL>Multiset.count n (∑ s : σ, (Fintype.card K - 1) • {s}) = Fintype.card K - 1
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>c : σ → K<VAR>n : σ<GOAL>∑ x : σ, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommGroup G<VAR>L : List G<VAR>n : ℕ<VAR>a : G<GOAL>(L.set n a).prod = L.prod * if hn : n < L.length then (L.get ⟨n, hn⟩)⁻¹ * a else 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommGroup G<VAR>L : List G<VAR>n : ℕ<VAR>a : G<GOAL>((take n L).prod * if n < L.length then a else 1) * (drop (n + 1) L).prod = L.prod * if hn : n < L.length then (L.get ⟨n, hn⟩)⁻¹ * a else 1
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n : ℕ+<VAR>g : L ≃+* L<VAR>c : ZMod (Fintype.card ↥(rootsOfUnity n L))<VAR>hc : ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ c.val)<GOAL>c = χ₀ n g
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n : ℕ+<VAR>g : L ≃+* L<VAR>c : ZMod (Fintype.card ↥(rootsOfUnity n L))<VAR>hc : ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ c.val)<VAR>ζ : ↥(rootsOfUnity n L)<GOAL>ζ ^ c.val = ζ ^ (χ₀ n g).val
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n : ℕ+<VAR>g : L ≃+* L<VAR>c : ZMod (Fintype.card ↥(rootsOfUnity n L))<VAR>ζ : ↥(rootsOfUnity n L)<VAR>hc : g ↑↑ζ = ↑(↑ζ ^ c.val)<GOAL>↑(↑ζ ^ c.val) = ↑(↑ζ ^ (χ₀ n g).val)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace α<GOAL>MeasurableSet (range Sum.inl)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace α<GOAL>MeasurableSet (Sum.inl '' univ)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroDivisors A<VAR>x : A<VAR>hx : x ≠ 0<VAR>this : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }<GOAL>Function.Injective ⇑(mulLeft R x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroDivisors A<VAR>x : A<VAR>hx : x ≠ 0<VAR>this✝ : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }<VAR>this : IsDomain A := NoZeroDivisors.to_isDomain A<GOAL>Function.Injective ⇑(mulLeft R x)
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>p₀ -ᵥ (lineMap p₀ p₁) c = c • (p₀ -ᵥ p₁)
<VAR>R✝ : Type u_1<VAR>R₂✝ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M✝ : Type u_6<VAR>M₂✝ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹⁹ : Semiring R✝<VAR>inst✝¹⁸ : Semiring R₂✝<VAR>inst✝¹⁷ : Semiring R₃<VAR>inst✝¹⁶ : AddCommMonoid M✝<VAR>inst✝¹⁵ : AddCommMonoid M₂✝<VAR>inst✝¹⁴ : AddCommMonoid M₃<VAR>σ₁₂ : R✝ →+* R₂✝<VAR>σ₂₃ : R₂✝ →+* R₃<VAR>σ₁₃ : R✝ →+* R₃<VAR>inst✝¹³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹² : Module R✝ M✝<VAR>inst✝¹¹ : Module R₂✝ M₂✝<VAR>inst✝¹⁰ : Module R₃ M₃<VAR>σ₂₁ : R₂✝ →+* R✝<VAR>τ₁₂✝ : R✝ →+* R₂✝<VAR>τ₂₃ : R₂✝ →+* R₃<VAR>τ₁₃ : R✝ →+* R₃<VAR>inst✝⁹ : RingHomCompTriple τ₁₂✝ τ₂₃ τ₁₃<VAR>F : Type u_11<VAR>inst✝⁸ : FunLike F M✝ M₂✝<VAR>inst✝⁷ : SemilinearMapClass F τ₁₂✝ M✝ M₂✝<VAR>R : Type u_12<VAR>R₂ : Type u_13<VAR>M : Type u_14<VAR>M₂ : Type u_15<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Ring R₂<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>range ((-id).comp f) = range f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝²⁰ : RCLike 𝕜<VAR>inst✝¹⁹ : NormedAddCommGroup E<VAR>inst✝¹⁸ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁷ : CompleteSpace E<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 G<VAR>inst✝⁹ : NormedAddCommGroup G'<VAR>inst✝⁸ : NormedSpace ℝ G'<VAR>inst✝⁷ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁶ : RCLike 𝕜'<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : InnerProductSpace 𝕜' E''<VAR>inst✝³ : CompleteSpace E''<VAR>inst✝² : NormedSpace ℝ E''<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>Integrable (↑↑(condexpIndSMul hm hs hμs x)) μ