ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<VAR>n : ℕ<VAR>c : R<VAR>hc : c * g = h ^ (n + 1)<VAR>basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h<VAR>i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V<GOAL>∀ x ∈ PrimeSpectrum.basicOpen (h ^ (n + 1)), g ∈ x.asIdeal.primeCompl
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<VAR>n : ℕ<VAR>c : R<VAR>hc : c * g = h ^ (n + 1)<VAR>basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h<VAR>i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V<GOAL>const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1))) ⋯ = const R f g (PrimeSpectrum.basicOpen (h ^ (n + 1))) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<VAR>n : ℕ<VAR>c : R<VAR>hc : c * g = h ^ (n + 1)<VAR>basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h<VAR>i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V<GOAL>f * c * g = f * h ^ (n + 1)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_sub : w ○ w ⊆ s<GOAL>∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_sub : w ○ w ⊆ s<GOAL>symmetrizeRel w ○ symmetrizeRel w ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_sub : w ○ w ⊆ s<VAR>this : symmetrizeRel w ⊆ w<GOAL>symmetrizeRel w ○ symmetrizeRel w ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>x y z : α<VAR>t : Set α<VAR>xs : x ∈ s<VAR>yt : y ∈ t<GOAL>diam (s ∪ t) ≤ diam s + dist x y + diam t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>x y z : α<VAR>t : Set α<VAR>xs : x ∈ s<VAR>yt : y ∈ t<GOAL>(EMetric.diam (s ∪ t)).toReal ≤ (EMetric.diam s).toReal + (edist x y).toReal + (EMetric.diam t).toReal
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>x y z : α<VAR>t : Set α<VAR>xs : x ∈ s<VAR>yt : y ∈ t<GOAL>EMetric.diam s + edist x y = ⊤ → EMetric.diam (s ∪ t) = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>x y z : α<VAR>t : Set α<VAR>xs : x ∈ s<VAR>yt : y ∈ t<GOAL>EMetric.diam t = ⊤ → EMetric.diam (s ∪ t) = ⊤
<VAR>α : Type u_1<VAR>a' a : α<VAR>l : List α<VAR>p : α → Option α<VAR>h : p a = some a'<GOAL>replaceF p (a :: l) = a' :: l
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<GOAL>Function.Bijective ((forget C).map f)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<GOAL>IsIso ((forget C).map f)
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>𝕜 : Type u_5<VAR>R : Type u_6<VAR>M : Type u_7<VAR>N : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : Invertible 2<VAR>inst✝³ : Lattice β<VAR>inst✝² : AddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : β<GOAL>x ⊓ y = ⅟2 • (x + y - |y - x|)
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → CommRing (G i)<VAR>f✝ : (i j : ι) → i ≤ j → G i → G j<VAR>f'✝ : (i j : ι) → i ≤ j → G i →+* G j<VAR>P : Type u₁<VAR>inst✝⁴ : CommRing P<VAR>g : (i : ι) → G i →+* P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f✝ i j hij x) = (g i) x<VAR>f : (i j : ι) → i ≤ j → G i →+* G j<VAR>G' : ι → Type v'<VAR>inst✝³ : (i : ι) → CommRing (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →+* G' j<VAR>G'' : ι → Type v''<VAR>inst✝² : (i : ι) → CommRing (G'' i)<VAR>f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>g₁ : (i : ι) → G i →+* G' i<VAR>g₂ : (i : ι) → G' i →+* G'' i<VAR>hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)<VAR>hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)<VAR>i j : ι<VAR>h : i ≤ j<GOAL>((fun i => (g₂ i).comp (g₁ i)) j).comp (f i j h) = (f'' i j h).comp ((fun i => (g₂ i).comp (g₁ i)) i)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>ι : Sort u_5<VAR>p : ι → Subgroup G<GOAL>⨆ i, p i = closure (⋃ i, ↑(p i))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : SemilatticeInf β<VAR>f : α ≃o β<VAR>x y : α<GOAL>f (x ⊓ y) = f x ⊓ f y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : SemilatticeInf β<VAR>f : α ≃o β<VAR>x y : α<GOAL>f.toOrderEmbedding x ⊓ f.toOrderEmbedding y ≤ f.toOrderEmbedding (x ⊓ y)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : SemilatticeInf β<VAR>f : α ≃o β<VAR>x y : α<GOAL>f.symm (f.toOrderEmbedding x ⊓ f.toOrderEmbedding y) ≤ f.symm (f.toOrderEmbedding (x ⊓ y))
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a b c : α<VAR>hc : c ≠ 0<VAR>d : α<GOAL>b * c = a * c * d ↔ b = a * d
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M✝ M N : Mon_ C<VAR>f : M.X ≅ N.X<VAR>one_f : autoParam (M.one ≫ f.hom = N.one) _auto✝<VAR>mul_f : autoParam (M.mul ≫ f.hom = (f.hom ⊗ f.hom) ≫ N.mul) _auto✝<GOAL>N.mul ≫ f.inv = (f.inv ⊗ f.inv) ≫ M.mul
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M✝ M N : Mon_ C<VAR>f : M.X ≅ N.X<VAR>one_f : autoParam (M.one ≫ f.hom = N.one) _auto✝<VAR>mul_f : autoParam (M.mul ≫ f.hom = (f.hom ⊗ f.hom) ≫ N.mul) _auto✝<GOAL>(N.mul ≫ f.inv) ≫ f.hom = ((f.inv ⊗ f.inv) ≫ M.mul) ≫ f.hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M✝ M N : Mon_ C<VAR>f : M.X ≅ N.X<VAR>one_f : autoParam (M.one ≫ f.hom = N.one) _auto✝<VAR>mul_f : autoParam (M.mul ≫ f.hom = (f.hom ⊗ f.hom) ≫ N.mul) _auto✝<GOAL>(N.mul ≫ f.inv) ≫ f.hom = (f.inv ⊗ f.inv) ≫ (f.hom ⊗ f.hom) ≫ N.mul
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ : Filter α<VAR>k✝ f g g' : α → β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : CommSemiring β<VAR>l : Filter α<VAR>k : α → β<VAR>z : ℕ<GOAL>Tendsto (fun a => k a ^ z * 0 a) l (𝓝 0)
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>ξ : 𝕊<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ T / ↑(n + 1)
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>ξ : 𝕊<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>volume univ ≤ (n + 1) • volume (closedBall 0 (T / ↑(n + 1) / 2))
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b c : α<VAR>n : ℤ<VAR>a : α<GOAL>toIcoMod hp a a = a
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b c : α<VAR>n : ℤ<VAR>a : α<GOAL>a < a + p ∧ ∃ z, a = a + z • p
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Cardinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : lift.{v, u} #ι < c<GOAL>lift.{v, u} #ι < c.ord.cof
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>(fun x => a + x) '' Icc b c = Icc (a + b) (a + c)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : CompactSpace M<GOAL>∃ n e, Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧ ClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
<VAR>ι✝ : Type uι<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : CompactSpace M<VAR>ι : Type uM<VAR>f : SmoothBumpCovering ι I M<GOAL>∃ n e, Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧ ClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
<VAR>ι✝ : Type uι<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : CompactSpace M<VAR>ι : Type uM<VAR>f : SmoothBumpCovering ι I M<VAR>this : Fintype ι<GOAL>∃ n e, Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧ ClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
<VAR>ι✝ : Type uι<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : CompactSpace M<VAR>ι : Type uM<VAR>f : SmoothBumpCovering ι I M<VAR>this : Fintype ι<VAR>n : ℕ<VAR>e : M → EuclideanSpace ℝ (Fin n)<VAR>hsmooth : Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e<VAR>hinj : Injective e<VAR>hinj_mfderiv : ∀ (x : M), Injective ⇑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)<GOAL>∃ n e, Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧ ClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>H : Valid' o₁ (Ordnode.node s l x r) o₂<GOAL>Valid' o₁ (l.node' x r).eraseMax ↑(findMax' x r) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>H : Valid' o₁ (Ordnode.node s l x r) o₂<VAR>this : Ordnode.node s l x r = l.node' x r<GOAL>Valid' o₁ (l.node' x r).eraseMax ↑(findMax' x r) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>s : ℕ<VAR>o₂ : WithTop α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>l_ih✝ : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rl) o₂ → Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1<VAR>IHrr : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rr) o₂ → Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>H : Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)) o₂<GOAL>Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)).eraseMax ↑(findMax' x (Ordnode.node rs rl rx rr)) ∧ (l.node' x (Ordnode.node rs rl rx rr)).size = (l.node' x (Ordnode.node rs rl rx rr)).eraseMax.size + 1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>s : ℕ<VAR>o₂ : WithTop α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>l_ih✝ : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rl) o₂ → Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1<VAR>IHrr : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rr) o₂ → Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>H : Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)) o₂<VAR>this : Ordnode.node rs rl rx rr = rl.node' rx rr<GOAL>Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)).eraseMax ↑(findMax' x (Ordnode.node rs rl rx rr)) ∧ (l.node' x (Ordnode.node rs rl rx rr)).size = (l.node' x (Ordnode.node rs rl rx rr)).eraseMax.size + 1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>s : ℕ<VAR>o₂ : WithTop α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>l_ih✝ : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rl) o₂ → Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1<VAR>IHrr : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rr) o₂ → Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂<VAR>this : Ordnode.node rs rl rx rr = rl.node' rx rr<GOAL>Valid' o₁ (l.node' x (rl.node' rx rr)).eraseMax ↑(findMax' x (rl.node' rx rr)) ∧ (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>s : ℕ<VAR>o₂ : WithTop α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>l_ih✝ : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rl) o₂ → Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1<VAR>IHrr : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rr) o₂ → Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂<VAR>this : Ordnode.node rs rl rx rr = rl.node' rx rr<VAR>h : Valid' (↑x) (rl.node' rx rr).eraseMax ↑(findMax' rx rr)<VAR>e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1<GOAL>Valid' o₁ (l.node' x (rl.node' rx rr)).eraseMax ↑(findMax' x (rl.node' rx rr)) ∧ (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>s : ℕ<VAR>o₂ : WithTop α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>l_ih✝ : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rl) o₂ → Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1<VAR>IHrr : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rr) o₂ → Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂<VAR>this : Ordnode.node rs rl rx rr = rl.node' rx rr<VAR>h : Valid' (↑x) (rl.node' rx rr).eraseMax ↑(findMax' rx rr)<VAR>e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1<GOAL>(l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>s : ℕ<VAR>o₂ : WithTop α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>l_ih✝ : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rl) o₂ → Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1<VAR>IHrr : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rr) o₂ → Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂<VAR>this : Ordnode.node rs rl rx rr = rl.node' rx rr<VAR>h : Valid' (↑x) (rl.node' rx rr).eraseMax ↑(findMax' rx rr)<VAR>e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1<GOAL>(l.node' x (rl.node' rx rr)).size = l.size + (rl.node' rx rr).eraseMax.size + 1 + 1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>s : ℕ<VAR>o₂ : WithTop α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr : Ordnode α<VAR>l_ih✝ : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rl) o₂ → Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1<VAR>IHrr : ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α}, Valid' o₁ (l.node' x rr) o₂ → Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1<VAR>l : Ordnode α<VAR>x : α<VAR>o₁ : WithBot α<VAR>H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂<VAR>this : Ordnode.node rs rl rx rr = rl.node' rx rr<VAR>h : Valid' (↑x) (rl.node' rx rr).eraseMax ↑(findMax' rx rr)<VAR>e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1<GOAL>l.size + ((rl.node' rx rr).eraseMax.size + 1) + 1 = l.size + (rl.node' rx rr).eraseMax.size + 1 + 1
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>hv : n = 0<GOAL>m + n = m
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>hv : n = 0<GOAL>append u v = u ∘ cast ⋯
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>hv : n = 0<VAR>l : Fin m<GOAL>append u v (castAdd n l) = (u ∘ cast ⋯) (castAdd n l)
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>hv : n = 0<VAR>r : Fin n<GOAL>append u v (natAdd m r) = (u ∘ cast ⋯) (natAdd m r)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : NonUnitalSemiring α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype o<VAR>v : o → α<VAR>M : Matrix m n α<VAR>N : Matrix n o α<VAR>x✝ : m<GOAL>((M * N) *ᵥ v) x✝ = (M *ᵥ N *ᵥ v) x✝
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>i : ι × κ<VAR>r : R<GOAL>(finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>i : ι × κ<VAR>r : R<GOAL>(finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i (r * 1)) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<GOAL>𝒜.card ≤ (Fintype.card α).choose r
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<GOAL>𝒜.card ≤ (powersetCard r univ).card
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n✝ : A<VAR>n : ℕ<GOAL>map (↑(opLinearEquiv R)) (M ^ n) = map (↑(opLinearEquiv R)) M ^ n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.map' 0 2 ⋯ ⋯ = 0<VAR>hR₂' : Mono (R₂.map' 0 1 ⋯ ⋯)<VAR>h₀ : Epi (app' φ 1 ⋯)<VAR>h₁ : Mono (app' φ 2 ⋯)<GOAL>Epi (app' φ 0 ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.map' 0 2 ⋯ ⋯ = 0<VAR>hR₂' : Mono (R₂.map' 0 1 ⋯ ⋯)<VAR>h₀ : Epi (app' φ 1 ⋯)<VAR>h₁ : Mono (app' φ 2 ⋯)<VAR>ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) := homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 ⋯)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯<GOAL>Epi (app' φ 0 ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.map' 0 2 ⋯ ⋯ = 0<VAR>hR₂' : Mono (R₂.map' 0 1 ⋯ ⋯)<VAR>h₀ : Epi (app' φ 1 ⋯)<VAR>h₁ : Mono (app' φ 2 ⋯)<VAR>ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) := homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 ⋯)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯<GOAL>(ShortComplex.mk ((mk₂ ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯) ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯) ((mk₂ ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯) ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯) ⋯).Exact
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.map' 0 2 ⋯ ⋯ = 0<VAR>hR₂' : Mono (R₂.map' 0 1 ⋯ ⋯)<VAR>h₀ : Epi (app' φ 1 ⋯)<VAR>h₁ : Mono (app' φ 2 ⋯)<VAR>ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) := homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 ⋯)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯<GOAL>(mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 3 ⋯ ⋯ = 0
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>C : ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>h_nonneg : ∀ (n : ℕ), 0 ≤ f n<VAR>hu : Monotone u<VAR>h_succ_diff : SuccDiffBounded C u<VAR>n : ℕ<GOAL>∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k) ≤ (u 1 - u 0) • f (u 0) + C • ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k