ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Ring B'<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Algebra A B'<VAR>x✝ : B<VAR>f : B →ₐ[A] B'<VAR>x : B<GOAL>(Polynomial.aeval (f x)) (minpoly A x) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Sort ?u.95493<VAR>inst✝ : _root_.Finite ι<VAR>h : FinitePresentation R M<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<VAR>hl' : (LinearMap.ker l).FG<GOAL>FinitePresentation R N
<VAR>x y : ℂ<VAR>hx₁ : -π < x.im<VAR>hx₂ : x.im ≤ π<VAR>hy₁ : -π < y.im<VAR>hy₂ : y.im ≤ π<VAR>hxy : cexp x = cexp y<GOAL>x = y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedRing α<VAR>f g : ι → α<VAR>s : Set ι<VAR>a b c d : α<GOAL>Antivary f g ↔ ∀ (i j : ι), (f j - f i) * (g j - g i) ≤ 0
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>completedCosZeta a (1 - s) = completedHurwitzZetaEven a s
<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>f : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<GOAL>IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b) μ
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<GOAL>1 = ⊤
<VAR>α β : Type u<VAR>a b : Cardinal.{u}<GOAL>ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0
<VAR>α β : Type u<VAR>a b : Cardinal.{u}<VAR>this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0<GOAL>ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0
<VAR>α β : Type u<VAR>a b : Cardinal.{u}<VAR>this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0<GOAL>b ≠ 0 ∧ ℵ₀ ≤ a ∨ a ≠ 0 ∧ ℵ₀ ≤ b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>r' : β → β → Prop<VAR>s t : Set α<VAR>a b✝ : α<VAR>hs : IsAntichain r s<VAR>φ : r ↪r r'<VAR>b : β<VAR>hb : b ∈ ⇑φ '' s<VAR>b' : β<VAR>hb' : b' ∈ ⇑φ '' s<VAR>h₁ : b ≠ b'<VAR>h₂ : r' b b'<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>r' : β → β → Prop<VAR>s t : Set α<VAR>a b✝ : α<VAR>hs : IsAntichain r s<VAR>φ : r ↪r r'<VAR>b : β<VAR>hb : ∃ x ∈ s, φ x = b<VAR>b' : β<VAR>hb' : ∃ x ∈ s, φ x = b'<VAR>h₁ : b ≠ b'<VAR>h₂ : r' b b'<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>r' : β → β → Prop<VAR>s t : Set α<VAR>a✝ b : α<VAR>hs : IsAntichain r s<VAR>φ : r ↪r r'<VAR>a : α<VAR>has : a ∈ s<VAR>a' : α<VAR>has' : a' ∈ s<VAR>h₁ : φ a ≠ φ a'<VAR>h₂ : r' (φ a) (φ a')<GOAL>False
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>S : Set (Set α)<VAR>hS : S.Countable<GOAL>μ (⋃₀ S) = 0 ↔ ∀ s ∈ S, μ s = 0
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n : ℕ<GOAL>replicate n p = (p ^ n).primeFactorsList
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n : ℕ<GOAL>replicate n p ~ (p ^ n).primeFactorsList
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n : ℕ<GOAL>∀ p_1 ∈ replicate n p, Prime p_1
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n q : ℕ<VAR>hq : q ∈ replicate n p<GOAL>Prime q
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m m₁ m₂ m₃ : OuterMeasure α<VAR>op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞<VAR>h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)<VAR>s : Set α<GOAL>m₁.trim s = op (m₂.trim s) (m₃.trim s)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m m₁ m₂ m₃ : OuterMeasure α<VAR>op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞<VAR>h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)<VAR>s t : Set α<VAR>_hst : s ⊆ t<VAR>_ht : MeasurableSet t<VAR>htm : ∀ (i : Fin (Nat.succ 0).succ.succ), (![m₁, m₂, m₃] i) t = (![m₁, m₂, m₃] i).trim s<GOAL>m₁.trim s = op (m₂.trim s) (m₃.trim s)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m m₁ m₂ m₃ : OuterMeasure α<VAR>op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞<VAR>h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)<VAR>s t : Set α<VAR>_hst : s ⊆ t<VAR>_ht : MeasurableSet t<VAR>htm : m₁ t = m₁.trim s ∧ m₂ t = m₂.trim s ∧ m₃ t = m₃.trim s ∧ ∀ (i : Fin 0), (![] i) t = (![] i).trim s<GOAL>m₁.trim s = op (m₂.trim s) (m₃.trim s)
<VAR>α : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s k : Set α<VAR>G : Type u_2<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<GOAL>μ.InnerRegularWRT (fun s => ∃ f, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) fun s => MeasurableSet s ∧ μ s ≠ ⊤
<VAR>α : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s k : Set α<VAR>G : Type u_2<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<GOAL>μ.InnerRegularWRT (fun s => ∃ f, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) fun s => IsCompact s ∧ IsClosed s
<VAR>α : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s k : Set α<VAR>G : Type u_2<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>K : Set G<VAR>K_comp : IsCompact K<VAR>K_closed : IsClosed K<VAR>r : ℝ≥0∞<VAR>hr : r < μ K<VAR>L : Set G := μ.everywherePosSubset K<GOAL>∃ K_1 ⊆ K, (fun s => ∃ f, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) K_1 ∧ r < μ K_1
<VAR>α : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s k : Set α<VAR>G : Type u_2<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>K : Set G<VAR>K_comp : IsCompact K<VAR>K_closed : IsClosed K<VAR>r : ℝ≥0∞<VAR>hr : r < μ K<VAR>L : Set G := μ.everywherePosSubset K<VAR>L_comp : IsCompact L<GOAL>∃ K_1 ⊆ K, (fun s => ∃ f, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) K_1 ∧ r < μ K_1
<VAR>α : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s k : Set α<VAR>G : Type u_2<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>K : Set G<VAR>K_comp : IsCompact K<VAR>K_closed : IsClosed K<VAR>r : ℝ≥0∞<VAR>hr : r < μ K<VAR>L : Set G := μ.everywherePosSubset K<VAR>L_comp : IsCompact L<VAR>L_closed : IsClosed L<GOAL>∃ K_1 ⊆ K, (fun s => ∃ f, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) K_1 ∧ r < μ K_1
<VAR>α : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s k : Set α<VAR>G : Type u_2<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>K : Set G<VAR>K_comp : IsCompact K<VAR>K_closed : IsClosed K<VAR>r : ℝ≥0∞<VAR>hr : r < μ K<VAR>L : Set G := μ.everywherePosSubset K<VAR>L_comp : IsCompact L<VAR>L_closed : IsClosed L<GOAL>(fun s => ∃ f, Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) L
<VAR>α : Type u_1<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s k : Set α<VAR>G : Type u_2<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : LocallyCompactSpace G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>K : Set G<VAR>K_comp : IsCompact K<VAR>K_closed : IsClosed K<VAR>r : ℝ≥0∞<VAR>hr : r < μ K<VAR>L : Set G := μ.everywherePosSubset K<VAR>L_comp : IsCompact L<VAR>L_closed : IsClosed L<GOAL>r < μ L
<VAR>R : Type u_1<VAR>N : Type u_2<VAR>M : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f i : N →ₗ[R] M<VAR>K : Submodule R N<VAR>m : ℕ<VAR>heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K<VAR>hf : Surjective ⇑f<VAR>hi : Injective ⇑i<GOAL>ker f ≤ K
<VAR>R : Type u_1<VAR>N : Type u_2<VAR>M : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f i : N →ₗ[R] M<VAR>K : Submodule R N<VAR>m : ℕ<VAR>heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K<VAR>hf : Surjective ⇑f<VAR>hi : Injective ⇑i<GOAL>ker f ≤ f.iterateMapComap i (0 + 1) K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>hd : l.Nodup<VAR>n : ℕ<GOAL>l.formPerm = (l.rotate n).formPerm
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>S : Type u_3<VAR>inst✝ : Semigroup S<VAR>a✝ b c : S<VAR>h : Commute b c<VAR>a : S<GOAL>a * b * c = a * c * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>s.toFinset.Nonempty ↔ s ≠ 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X X' : SimplicialObject C<VAR>n : ℕ<VAR>Z Z' : C<VAR>f : MorphComponents X n Z<VAR>g : X' ⟶ X<VAR>h : Z ⟶ Z'<GOAL>PInfty.f (n + 1) ≫ { a := f.a ≫ h, b := fun i => f.b i ≫ h }.a + ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ { a := f.a ≫ h, b := fun i => f.b i ≫ h }.b i.rev = (PInfty.f (n + 1) ≫ f.a + ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev) ≫ h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>a : α<VAR>inst✝ : IsSFiniteKernel κ<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(dirac a ⊗ₘ κ) s = (κ a) (Prod.mk a ⁻¹' s)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>α : E<VAR>S : Set E<VAR>hS : ∀ x ∈ S, IsAlgebraic F x<GOAL>(adjoin F S).toSubalgebra = Algebra.adjoin F S
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>α : E<VAR>S : Set E<VAR>hS : ∀ x ∈ S, IsIntegral F x<GOAL>(adjoin F S).toSubalgebra = Algebra.adjoin F S
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>α : E<VAR>S : Set E<VAR>hS : ∀ x ∈ S, IsIntegral F x<VAR>this : Algebra.IsIntegral F ↥(Algebra.adjoin F S)<GOAL>(adjoin F S).toSubalgebra = Algebra.adjoin F S
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>α : E<VAR>S : Set E<VAR>hS : ∀ x ∈ S, IsIntegral F x<VAR>this✝ : Algebra.IsIntegral F ↥(Algebra.adjoin F S)<VAR>this : IsField ↥(Algebra.adjoin F S)<GOAL>(adjoin F S).toSubalgebra = Algebra.adjoin F S
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>(mulETransformLeft e x).1.card + (mulETransformLeft e x).2.card + ((mulETransformRight e x).1.card + (mulETransformRight e x).2.card) = x.1.card + x.2.card + (x.1.card + x.2.card)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁✝ s₂✝ t t₁ t₂ u v : Finset α<VAR>a b : α<VAR>s₁ s₂ s₃ : Finset α<VAR>x✝ : α<GOAL>x✝ ∈ s₁ ∩ s₂ ∩ s₃ ↔ x✝ ∈ s₁ ∩ (s₂ ∩ s₃)
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>toFinsupp✝¹ toFinsupp✝ : R[ℕ]<GOAL>({ toFinsupp := toFinsupp✝¹ } - { toFinsupp := toFinsupp✝ }).coeff n = { toFinsupp := toFinsupp✝¹ }.coeff n - { toFinsupp := toFinsupp✝ }.coeff n
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>toFinsupp✝¹ toFinsupp✝ : R[ℕ]<GOAL>(match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝¹ - toFinsupp✝ } with | { toFinsupp := p } => ⇑p) n = (match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝¹ } with | { toFinsupp := p } => ⇑p) n - (match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝ } with | { toFinsupp := p } => ⇑p) n
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖x‖ / (o.oangle y (y - x)).tan = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle y (y - x)).sign = 1<GOAL>‖x‖ / (o.oangle y (y - x)).tan = ‖y‖
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>s : WSeq α<GOAL>(Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) ([], cons a s)).destruct = Sum.inr (List.cons a <$> Computation.corec (fun x => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) ([], s))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>s : WSeq α<GOAL>Computation.corec (fun x => match Seq.destruct x.2 with | none => Sum.inl x.1.reverse | some (none, s') => Sum.inr (x.1, s') | some (some a, s') => Sum.inr (a :: x.1, s')) ([a], s) = List.cons a <$> Computation.corec (fun x => match Seq.destruct x.2 with | none => Sum.inl x.1.reverse | some (none, s') => Sum.inr (x.1, s') | some (some a, s') => Sum.inr (a :: x.1, s')) ([], s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>s : WSeq α<GOAL>(fun x => [a].reverse ++ x) <$> s.toList = List.cons a <$> Computation.corec (fun x => match Seq.destruct x.2 with | none => Sum.inl x.1.reverse | some (none, s') => Sum.inr (x.1, s') | some (some a, s') => Sum.inr (a :: x.1, s')) ([], s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>s : WSeq α<GOAL>(fun x => a :: x) <$> s.toList = List.cons a <$> Computation.corec (fun x => match Seq.destruct x.2 with | none => Sum.inl x.1.reverse | some (none, s') => Sum.inr (x.1, s') | some (some a, s') => Sum.inr (a :: x.1, s')) ([], s)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>t : RBNode α<VAR>h : WF cmp t<GOAL>Ordered cmp t ∧ ∃ c n, t.Balanced c n
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>r : R<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<GOAL>((gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1)) x = r • x
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>r : R<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<GOAL>(gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) = DistribMulAction.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>r : R<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<VAR>ia : ι<VAR>a : 𝒜 ia<VAR>ib : ι<VAR>b : ℬ ib<GOAL>((gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1)) ((lof R ι 𝒜 ia) a ⊗ₜ[R] (lof R ι ℬ ib) b) = r • (lof R ι 𝒜 ia) a ⊗ₜ[R] (lof R ι ℬ ib) b
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>r : R<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<VAR>ia : ι<VAR>a : 𝒜 ia<VAR>ib : ι<VAR>b : ℬ ib<GOAL>(-1) ^ (0 * ia) • ((algebraMap R (DirectSum ι 𝒜)) r * (lof R ι 𝒜 ia) a) ⊗ₜ[R] ((lof R ι ℬ 0) GradedMonoid.GOne.one * (lof R ι ℬ ib) b) = r • (lof R ι 𝒜 ia) a ⊗ₜ[R] (lof R ι ℬ ib) b
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>r : R<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<VAR>ia : ι<VAR>a : 𝒜 ia<VAR>ib : ι<VAR>b : ℬ ib<GOAL>((algebraMap R (DirectSum ι 𝒜)) r * (lof R ι 𝒜 ia) a) ⊗ₜ[R] ((lof R ι ℬ 0) GradedMonoid.GOne.one * (lof R ι ℬ ib) b) = (r • (lof R ι 𝒜 ia) a) ⊗ₜ[R] (lof R ι ℬ ib) b
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<GOAL>logb b x ≤ 0 ↔ x ≤ 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p : ℕ<VAR>hn : Fact (Nat.Prime p)<GOAL>eval 1 (cyclotomic p R) = ↑p
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f g : a ⟶ b<VAR>η : f ≅ g<VAR>h : b ⟶ c<GOAL>η.hom ▷ h ≫ η.inv ▷ h = 𝟙 (f ≫ h)
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<GOAL>logb b x ≤ 0 ↔ 1 ≤ x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<GOAL>card σ.cycleType = 0 ↔ σ = 1
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : SMulCommClass S R M<VAR>inst✝¹ : SMul R S<VAR>inst✝ : IsScalarTower R S M<VAR>x : R<VAR>h : IsUnit ((algebraMap R (End S M)) x)<VAR>m m' : M<VAR>H : m = x • m'<GOAL>m' = ↑h.unit⁻¹ (x • m')
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : SMulCommClass S R M<VAR>inst✝¹ : SMul R S<VAR>inst✝ : IsScalarTower R S M<VAR>x : R<VAR>h : IsUnit ((algebraMap R (End S M)) x)<VAR>m m' : M<VAR>H : m = x • m'<GOAL>↑h.unit m' = ↑h.unit (↑h.unit⁻¹ (x • m'))
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : SMulCommClass S R M<VAR>inst✝¹ : SMul R S<VAR>inst✝ : IsScalarTower R S M<VAR>x : R<VAR>h : IsUnit ((algebraMap R (End S M)) x)<VAR>m m' : M<VAR>H : m = x • m'<GOAL>↑h.unit m' = x • m'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : s ⊆ t<GOAL>(t \ s).card = t.card - s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : s ⊆ t<GOAL>(t \ s).card = (t \ s ∪ s).card - s.card
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cocone F✝<VAR>F : J ⥤ C<VAR>s : Cocone F<VAR>G : K ⥤ C<VAR>t : Cocone G<VAR>P : IsColimit s<VAR>Q : IsColimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<GOAL>P.desc ((Cocones.equivalenceOfReindexing e w).functor.obj t) ≫ Q.desc ((Cocones.equivalenceOfReindexing e.symm w').functor.obj s) = 𝟙 s.pt
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cocone F✝<VAR>F : J ⥤ C<VAR>s : Cocone F<VAR>G : K ⥤ C<VAR>t : Cocone G<VAR>P : IsColimit s<VAR>Q : IsColimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<GOAL>∀ (j : J), s.ι.app j ≫ P.desc ((Cocones.equivalenceOfReindexing e w).functor.obj t) ≫ Q.desc ((Cocones.equivalenceOfReindexing e.symm w').functor.obj s) = s.ι.app j ≫ 𝟙 s.pt
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cocone F✝<VAR>F : J ⥤ C<VAR>s : Cocone F<VAR>G : K ⥤ C<VAR>t : Cocone G<VAR>P : IsColimit s<VAR>Q : IsColimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<VAR>j : J<GOAL>s.ι.app j ≫ P.desc ((Cocones.precompose w.inv).obj (Cocone.whisker e.functor t)) ≫ Q.desc ((Cocones.precompose ((e.invFunIdAssoc G).inv ≫ whiskerLeft e.inverse w.hom)).obj (Cocone.whisker e.inverse s)) = s.ι.app j ≫ 𝟙 s.pt
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cocone F✝<VAR>F : J ⥤ C<VAR>s : Cocone F<VAR>G : K ⥤ C<VAR>t : Cocone G<VAR>P : IsColimit s<VAR>Q : IsColimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<VAR>j : J<GOAL>w.inv.app j ≫ G.map (e.counitInv.app (e.functor.obj j)) ≫ w.hom.app (e.inverse.obj (e.functor.obj j)) ≫ s.ι.app (e.inverse.obj (e.functor.obj j)) = s.ι.app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cocone F✝<VAR>F : J ⥤ C<VAR>s : Cocone F<VAR>G : K ⥤ C<VAR>t : Cocone G<VAR>P : IsColimit s<VAR>Q : IsColimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<VAR>j : J<GOAL>F.map (e.unit.app j) ≫ w.inv.app ((e.functor ⋙ e.inverse).obj j) ≫ w.hom.app (e.inverse.obj (e.functor.obj j)) ≫ s.ι.app (e.inverse.obj (e.functor.obj j)) = s.ι.app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cocone F✝<VAR>F : J ⥤ C<VAR>s : Cocone F<VAR>G : K ⥤ C<VAR>t : Cocone G<VAR>P : IsColimit s<VAR>Q : IsColimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<GOAL>Q.desc ((Cocones.equivalenceOfReindexing e.symm w').functor.obj s) ≫ P.desc ((Cocones.equivalenceOfReindexing e w).functor.obj t) = 𝟙 t.pt