ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝ : Finite ι<VAR>e : Basis ι R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>(Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x
<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✝ : Finite ι<VAR>e : Basis ι R M<VAR>f : M ≃ₗ[R] M<VAR>val✝ : Fintype ι<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>g : M [⋀^ι]→ₗ[R] R<VAR>hg : g ≠ 0<GOAL>(Orientation.map ι f) (rayOfNeZero R g hg) = (LinearEquiv.det f)⁻¹ • rayOfNeZero R g hg
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : M →* N<VAR>hf : ∀ (y : ↥S), IsUnit (f ↑y)<VAR>y z : ↥S<VAR>h : ((IsUnit.liftRight (f.restrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.restrict S) hf) z)⁻¹<GOAL>f ↑y = f ↑z
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : M →* N<VAR>hf : ∀ (y : ↥S), IsUnit (f ↑y)<VAR>y z : ↥S<VAR>h : ((IsUnit.liftRight (f.restrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.restrict S) hf) z)⁻¹<GOAL>f ↑z * ↑((IsUnit.liftRight (f.restrict S) hf) z)⁻¹ = 1
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x < y ^ (1 / z) ↔ x ^ z < y
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ 1 < y ^ (1 / z) ↔ x ^ z < y
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ (z * z⁻¹) < y ^ (1 / z) ↔ x ^ z < y
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedRing A<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : IntervalIntegrable f volume a b<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => f (x - c)) volume (a + c) (b + c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>g : β → γ<VAR>s t : Set α<VAR>h : Semiconj f fa fb<VAR>ha : Surjective fa<GOAL>SurjOn fb (range f) (range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>g : β → γ<VAR>s t : Set α<VAR>h : Semiconj f fa fb<VAR>ha : Surjective fa<GOAL>SurjOn fb (f '' univ) (f '' univ)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>h : Directed (fun x x_1 => x ≤ x_1) f<GOAL>(⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℚ<GOAL>⨅ r, ρ (s ×ˢ Iic ↑↑r) = ρ (s ×ˢ Iic ↑t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℚ<GOAL>ρ (⋂ i, s ×ˢ Iic ↑↑i) = ρ (s ×ˢ Iic ↑t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℚ<GOAL>∀ (i : { r' // t < r' }), MeasurableSet (s ×ˢ Iic ↑↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℚ<GOAL>Directed (fun x x_1 => x ⊇ x_1) fun r => s ×ˢ Iic ↑↑r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℚ<GOAL>∃ i, ρ (s ×ˢ Iic ↑↑i) ≠ ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Ring S<VAR>inst✝⁹ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : IsDomain B<VAR>inst✝⁵ : Algebra A B<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>S' : Type u_7<VAR>inst✝³ : CommRing S'<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : Algebra A S<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>e : S ≃ₐ[A] S'<VAR>h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0<VAR>h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0<VAR>x : S<GOAL>(pb.equivOfRoot (pb.map e) h₁ h₂) x = e x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Ring S<VAR>inst✝⁹ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : IsDomain B<VAR>inst✝⁵ : Algebra A B<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>S' : Type u_7<VAR>inst✝³ : CommRing S'<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : Algebra A S<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>e : S ≃ₐ[A] S'<VAR>h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0<VAR>h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0<VAR>f : A[X]<GOAL>(pb.equivOfRoot (pb.map e) h₁ h₂) ((aeval pb.gen) f) = e ((aeval pb.gen) f)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>i : E →ₐ[F] K<VAR>x : E<GOAL>i x ∈ separableClosure F K ↔ x ∈ separableClosure F E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Finset α<VAR>a b : α<VAR>m : Multiset α<VAR>hm : m.Nodup<GOAL>{ val := m, nodup := hm }.Nonempty ↔ m ≠ 0
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>z : N<GOAL>g ↑(f.sec z).2 * (f.lift hg) z = g (f.sec z).1
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝⁴ : Semiring R<VAR>φ : ι → Type u_1<VAR>inst✝³ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝² : (i : ι) → Module R (φ i)<VAR>I : Set ι<VAR>p q : (i : ι) → Submodule R (φ i)<VAR>x : (i : ι) → φ i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι<GOAL>⨆ i, map (single i) (p i) = pi Set.univ p
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝⁴ : Semiring R<VAR>φ : ι → Type u_1<VAR>inst✝³ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝² : (i : ι) → Module R (φ i)<VAR>I : Set ι<VAR>p q : (i : ι) → Submodule R (φ i)<VAR>x : (i : ι) → φ i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<GOAL>⨆ i, map (single i) (p i) = pi Set.univ p
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝⁴ : Semiring R<VAR>φ : ι → Type u_1<VAR>inst✝³ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝² : (i : ι) → Module R (φ i)<VAR>I : Set ι<VAR>p q : (i : ι) → Submodule R (φ i)<VAR>x : (i : ι) → φ i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<VAR>i : ι<GOAL>map (single i) (p i) ≤ pi Set.univ p
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝⁴ : Semiring R<VAR>φ : ι → Type u_1<VAR>inst✝³ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝² : (i : ι) → Module R (φ i)<VAR>I : Set ι<VAR>p q : (i : ι) → Submodule R (φ i)<VAR>x : (i : ι) → φ i<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<GOAL>pi Set.univ p ≤ ⨆ i, map (single i) (p i)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x y : E<VAR>r : ℝ<GOAL>y ∈ p.closedBall 0 r ↔ p y ≤ r
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>h : M.IsMatching<VAR>x y : V<VAR>he : s(x, y) ∈ M.edgeSet<GOAL>∃ a, h.toEdge a = ⟨s(x, y), he⟩
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Ring R<VAR>p q r : R[X]<VAR>S : Type u_1<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>x : S<GOAL>eval₂ f x (-p) = -eval₂ f x p
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>ContinuousAt (fun p => p.1 * p.2) (⊤, ⊤)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), ↑x < a.1 * a.2
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>x : ℝ<GOAL>∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), ↑x < a.1 * a.2
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>x : ℝ<GOAL>∃ t, (∀ y ∈ t, ↑x < y.1 * y.2) ∧ IsOpen t ∧ (⊤, ⊤) ∈ t
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>x : ℝ<GOAL>(∀ y ∈ Ioi (max (↑x) 0) ×ˢ Ioi 1, ↑x < y.1 * y.2) ∧ IsOpen (Ioi (max (↑x) 0) ×ˢ Ioi 1) ∧ (⊤, ⊤) ∈ Ioi (max (↑x) 0) ×ˢ Ioi 1
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i j : n<GOAL>Aᵀ.cramer (A i) j = Pi.single i A.det j
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i j : n<GOAL>(Aᵀ.updateColumn j (A i)).det = if j = i then A.det else 0
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>h : ¬G.IsUniform ε s t<GOAL>↑s.card * ε ≤ ↑(G.nonuniformWitnesses ε s t).1.card
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>h : ¬G.IsUniform ε s t<GOAL>↑s.card * ε ≤ ↑(⋯.choose, ⋯.choose).1.card
<VAR>α : Type u_1<VAR>l✝ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l : List α<GOAL>count a (b :: l) = count a l + if a = b then 1 else 0
<VAR>α : Type u_1<VAR>l✝ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l : List α<GOAL>(if b = a then 1 else 0) = if a = b then 1 else 0
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>boxes : Finset (WithBot (Box ι))<VAR>le_of_mem : ∀ J ∈ boxes, J ≤ ↑I<VAR>pairwise_disjoint : (↑boxes).Pairwise Disjoint<VAR>H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J'<GOAL>ofWithBot boxes le_of_mem pairwise_disjoint ≤ π
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>boxes : Finset (WithBot (Box ι))<VAR>le_of_mem : ∀ J ∈ boxes, J ≤ ↑I<VAR>pairwise_disjoint : (↑boxes).Pairwise Disjoint<VAR>H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J'<VAR>this : ∀ (J : Box ι), ↑J ∈ boxes → ∃ J' ∈ π, J ≤ J'<GOAL>ofWithBot boxes le_of_mem pairwise_disjoint ≤ π
<VAR>f : ℕ → ℂ<VAR>c s : ℂ<VAR>hf : LSeriesSummable f s<GOAL>LSeriesSummable (c • f) s
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n : ℕ<GOAL>predictablePart f ℱ μ 0 = 0
<VAR>α : Type u_2<VAR>f : Type u_1<VAR>n : α → f → α<VAR>l : α<GOAL>scanl n l = scanlTR n l
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s✝ t : Set α<VAR>a b x y : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>m n : ℕ<GOAL>(f ^ m) a = (f ^ n) a ↔ m ≡ n [MOD s.card]
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s✝ t : Set α<VAR>a b x y : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>m n : ℕ<GOAL>(f ^ m) a = (f ^ n) a ↔ (f ^ (↑n - ↑m)) a = a
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : G → CoeSort.coe A<GOAL>f ∈ oneCocycles A ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ coequalizer.desc P.actRight ⋯ ≫ (ρ_ P.X).inv ≫ P.X ◁ S.one ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) = coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ 𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>((P.actRight ≫ (ρ_ P.X).inv) ≫ P.X ◁ S.one) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) = coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ 𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(((ρ_ (P.X ⊗ S.X)).inv ≫ P.actRight ▷ 𝟙_ C) ≫ P.X ◁ S.one) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) = coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ 𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(ρ_ (P.X ⊗ S.X)).inv ≫ ((P.X ⊗ S.X) ◁ S.one ≫ P.actRight ▷ S.X) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) = coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ 𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(ρ_ (P.X ⊗ S.X)).inv ≫ (P.X ⊗ S.X) ◁ S.one ≫ ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) = coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ 𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(ρ_ (P.X ⊗ S.X)).inv ≫ (((α_ P.X S.X (𝟙_ C)).hom ≫ P.X ◁ S.X ◁ S.one) ≫ P.X ◁ S.mul) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) = coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ 𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(ρ_ (P.X ⊗ S.X)).inv ≫ (α_ P.X S.X (𝟙_ C)).hom ≫ P.X ◁ (ρ_ S.X).hom ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) = coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ 𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝ : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>(ρ_ (P.X ⊗ S.X)).inv ≫ (α_ P.X S.X (𝟙_ C)).hom ≫ P.X ◁ (ρ_ S.X).hom ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) = coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂✝ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>s₁ s₂ : Finset ι<VAR>h : s₁ ⊆ s₂<GOAL>(affineCombination k s₁ p) w = (affineCombination k s₂ p) ((↑s₁).indicator w)
<VAR>c : Code<VAR>k : Cont'<GOAL>trStmts₁ (trNormal c k) ⊆ codeSupp' c k
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>zero : p 0<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>smul : ∀ (r : R) (x : ↥(adjoin R s)), p x → p (r • x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>p ⟨b, hb⟩
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>zero : p 0<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>smul : ∀ (r : R) (x : ↥(adjoin R s)), p x → p (r • x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>∃ (x : b ∈ adjoin R s), p ⟨b, x⟩
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>zero : p 0<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>smul : ∀ (r : R) (x : ↥(adjoin R s)), p x → p (r • x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>∀ x ∈ s, ∃ (x_1 : x ∈ adjoin R s), p ⟨x, x_1⟩
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>zero : p 0<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>smul : ∀ (r : R) (x : ↥(adjoin R s)), p x → p (r • x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>∀ (x y : A), (∃ (x_1 : x ∈ adjoin R s), p ⟨x, x_1⟩) → (∃ (x : y ∈ adjoin R s), p ⟨y, x⟩) → ∃ (x_1 : x + y ∈ adjoin R s), p ⟨x + y, x_1⟩
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>zero : p 0<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>smul : ∀ (r : R) (x : ↥(adjoin R s)), p x → p (r • x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>∃ (x : 0 ∈ adjoin R s), p ⟨0, x⟩
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>zero : p 0<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>smul : ∀ (r : R) (x : ↥(adjoin R s)), p x → p (r • x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>∀ (x y : A), (∃ (x_1 : x ∈ adjoin R s), p ⟨x, x_1⟩) → (∃ (x : y ∈ adjoin R s), p ⟨y, x⟩) → ∃ (x_1 : x * y ∈ adjoin R s), p ⟨x * y, x_1⟩
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>s : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>a : ↥(adjoin R s)<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>zero : p 0<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>smul : ∀ (r : R) (x : ↥(adjoin R s)), p x → p (r • x)<VAR>b : A<VAR>hb : b ∈ adjoin R s<GOAL>∀ (r : R) (x : A), (∃ (x_1 : x ∈ adjoin R s), p ⟨x, x_1⟩) → ∃ (x_1 : r • x ∈ adjoin R s), p ⟨r • x, x_1⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f : Filter α<VAR>g : Filter β<VAR>φ : α → β<VAR>ψ : β → α<VAR>eq : φ ∘ ψ = id<VAR>hφ : Tendsto φ f g<VAR>hψ : Tendsto ψ g f<GOAL>map φ f = g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f : Filter α<VAR>g : Filter β<VAR>φ : α → β<VAR>ψ : β → α<VAR>eq : φ ∘ ψ = id<VAR>hφ : Tendsto φ f g<VAR>hψ : Tendsto ψ g f<GOAL>g ≤ map φ (map ψ g)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : Nonempty α<VAR>r : α → β → Prop<GOAL>(∃ b, ∀ᶠ (a : α) in atTop, r a b) ↔ ∀ᶠ (a₀ : α) in atTop, ∃ b, ∀ a ≥ a₀, r a b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : Nonempty α<VAR>r : α → β → Prop<GOAL>(∃ x y, ∀ b ≥ x, r b y) ↔ ∃ a, ∀ b ≥ a, ∃ b_1, ∀ a ≥ b, r a b_1
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ C<VAR>c : Cone F<VAR>hc : IsLimit c<VAR>s : Cocone F.rightOp<VAR>m : (coconeRightOpOfCone c).pt ⟶ s.pt<VAR>w : ∀ (j : J), (coconeRightOpOfCone c).ι.app j ≫ m = s.ι.app j<GOAL>m = (fun s => (hc.lift (coneOfCoconeRightOp s)).op) s