ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : OrderedRing R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module R V<VAR>inst✝⁴ : AddTorsor V P<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module R V'<VAR>inst✝¹ : AddTorsor V' P'<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>x y z : P<VAR>h : Wbtw R x y z<GOAL>Wbtw R x z y ↔ y = z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s✝ t✝ : Multiset α<VAR>a : α<VAR>f : α → γ<VAR>g : β → γ<VAR>s : Multiset α<VAR>t : Multiset β<VAR>hs : s.Nodup<VAR>ht : t.Nodup<VAR>i : (a : α) → a ∈ s → β<VAR>hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t<VAR>i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂<VAR>i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b<VAR>h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)<VAR>this : t = map (fun x => i ↑x ⋯) s.attach<GOAL>map f s = map g t
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : IsUnifLocDoublingMeasure μ<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>K : ℝ<VAR>x : α<VAR>ι : Type u_2<VAR>l : Filter ι<VAR>w : ι → α<VAR>δ : ι → ℝ<VAR>δlim : Tendsto δ l (𝓝[>] 0)<VAR>xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)<GOAL>Tendsto (fun j => closedBall (w j) (δ j)) l ((vitaliFamily μ K).filterAt x)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : IsUnifLocDoublingMeasure μ<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>K : ℝ<VAR>x : α<VAR>ι : Type u_2<VAR>l : Filter ι<VAR>w : ι → α<VAR>δ : ι → ℝ<VAR>δlim : Tendsto δ l (𝓝[>] 0)<VAR>xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)<GOAL>∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ∈ (vitaliFamily μ K).setsAt x
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : IsUnifLocDoublingMeasure μ<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>K : ℝ<VAR>x : α<VAR>ι : Type u_2<VAR>l : Filter ι<VAR>w : ι → α<VAR>δ : ι → ℝ<VAR>δlim : Tendsto δ l (𝓝[>] 0)<VAR>xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : OrderedAddCommGroup H<VAR>f : G → H<VAR>h₁ : ∀ (x : G), f (-x) = -f x<VAR>h₂ : MonotoneOn f (Ici 0)<GOAL>Monotone f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : OrderedAddCommGroup H<VAR>f : G → H<VAR>h₁ : ∀ (x : G), f (-x) = -f x<VAR>h₂ : MonotoneOn f (Ici 0)<VAR>x : G<VAR>hx : x ∈ Iic 0<VAR>y : G<VAR>hy : y ∈ Iic 0<VAR>hxy : x ≤ y<GOAL>-f y ≤ -f x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : OrderedAddCommGroup H<VAR>f : G → H<VAR>h₁ : ∀ (x : G), f (-x) = -f x<VAR>h₂ : MonotoneOn f (Ici 0)<VAR>x : G<VAR>hx : x ∈ Iic 0<VAR>y : G<VAR>hy : y ∈ Iic 0<VAR>hxy : x ≤ y<GOAL>f (-y) ≤ f (-x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>ι✝ : Type u_4<VAR>π : ι✝ → Type u_5<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x : E<VAR>ι : Sort u_6<VAR>inst✝ : Nonempty ι<VAR>F : ι → Set E<VAR>hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)<VAR>i : ι<GOAL>IsExtreme 𝕜 A (⋂ i, F i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>ι✝ : Type u_4<VAR>π : ι✝ → Type u_5<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x✝ : E<VAR>ι : Sort u_6<VAR>inst✝ : Nonempty ι<VAR>F : ι → Set E<VAR>hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)<VAR>i : ι<VAR>x₁ : E<VAR>hx₁A : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂A : x₂ ∈ A<VAR>x : E<VAR>hxF : x ∈ ⋂ i, F i<VAR>hx : x ∈ openSegment 𝕜 x₁ x₂<GOAL>x₁ ∈ ⋂ i, F i ∧ x₂ ∈ ⋂ i, F i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>ι✝ : Type u_4<VAR>π : ι✝ → Type u_5<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x✝ : E<VAR>ι : Sort u_6<VAR>inst✝ : Nonempty ι<VAR>F : ι → Set E<VAR>hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)<VAR>i : ι<VAR>x₁ : E<VAR>hx₁A : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂A : x₂ ∈ A<VAR>x : E<VAR>hx : x ∈ openSegment 𝕜 x₁ x₂<VAR>hxF : ∀ (i : ι), x ∈ F i<GOAL>(∀ (i : ι), x₁ ∈ F i) ∧ ∀ (i : ι), x₂ ∈ F i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>ι✝ : Type u_4<VAR>π : ι✝ → Type u_5<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : SMul 𝕜 E<VAR>A B C : Set E<VAR>x✝ : E<VAR>ι : Sort u_6<VAR>inst✝ : Nonempty ι<VAR>F : ι → Set E<VAR>hAF : ∀ (i : ι), IsExtreme 𝕜 A (F i)<VAR>i : ι<VAR>x₁ : E<VAR>hx₁A : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂A : x₂ ∈ A<VAR>x : E<VAR>hx : x ∈ openSegment 𝕜 x₁ x₂<VAR>hxF : ∀ (i : ι), x ∈ F i<VAR>h : ∀ (i : ι), x₁ ∈ F i ∧ x₂ ∈ F i<GOAL>(∀ (i : ι), x₁ ∈ F i) ∧ ∀ (i : ι), x₂ ∈ F i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>L : List (List α)<VAR>s : List α<VAR>hs : s ∈ L<GOAL>s <+ L.join
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a : α<GOAL>(↑s).EquitableOn f ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / s.card ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / s.card + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a : α<GOAL>(∃ b, ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1) ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / s.card ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / s.card + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a : α<VAR>b : ℕ<VAR>hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1<VAR>x : α<VAR>hx₁ : x ∈ s<VAR>hx₂ : f x ≠ b + 1<GOAL>(∑ i ∈ s, f i) / s.card = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a : α<VAR>b : ℕ<VAR>hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1<VAR>x : α<VAR>hx₁ : x ∈ s<VAR>hx₂ : f x ≠ b + 1<GOAL>∑ i ∈ s, (b + 1) ≤ (b + 1) * s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a : α<VAR>b : ℕ<VAR>hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1<VAR>x : α<VAR>hx₁ : x ∈ s<VAR>hx₂ : f x ≠ b + 1<GOAL>∀ x ∈ s, b + 1 = b + 1
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝² : MulZeroClass α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PosMulMono α<VAR>ha : 0 ≤ a<VAR>hb : b ≤ 0<GOAL>a * b ≤ 0
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : ∀ (u : Set ι), u.Countable ∧ (s ∩ ⋂ i ∈ u, t i).Nonempty<GOAL>(s ∩ ⋂ i, t i).Nonempty
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<GOAL>∃ u, u.Countable → s ∩ ⋂ i ∈ u, t i = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hs : IsLindelof s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<VAR>u : Set ι<VAR>left✝ : u.Countable<VAR>husub : s ∩ ⋂ i ∈ u, t i = ∅<GOAL>∃ u, u.Countable → s ∩ ⋂ i ∈ u, t i = ∅
<VAR>n k : ℕ<GOAL>(n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)
<VAR>n k : ℕ<VAR>this : n + (k + 1) < n + 1 + (k + 1)<GOAL>(n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)
<VAR>n k : ℕ<VAR>this✝ : n + (k + 1) < n + 1 + (k + 1)<VAR>this : n + 1 + k < n + 1 + (k + 1)<GOAL>(n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)
<VAR>n k : ℕ<VAR>this✝ : n + (k + 1) < n + 1 + (k + 1)<VAR>this : n + 1 + k < n + 1 + (k + 1)<GOAL>(n + 1).multichoose k + n.multichoose (k + 1) = (n + k).choose k + (n + k).choose k.succ
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I : MulticospanIndex C<VAR>K : Multifork I<VAR>hK : IsLimit K<VAR>T : C<VAR>f g : T ⟶ K.pt<VAR>h : ∀ (a : I.L), f ≫ K.ι a = g ≫ K.ι a<GOAL>f = g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I : MulticospanIndex C<VAR>K : Multifork I<VAR>hK : IsLimit K<VAR>T : C<VAR>f g : T ⟶ K.pt<VAR>h : ∀ (a : I.L), f ≫ K.ι a = g ≫ K.ι a<GOAL>∀ (j : WalkingMulticospan I.fstTo I.sndTo), f ≫ K.π.app j = g ≫ K.π.app j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>l : List α<VAR>f : α → β<GOAL>image (fun i => f l[↑i]) univ = (List.map f l).toFinset
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderBot α<VAR>a b x : α<VAR>h : IsAtom a<GOAL>x ≤ a ↔ x = ⊥ ∨ x = a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : Associates α<VAR>h : a.factors = b.factors<VAR>this : a.factors.prod = b.factors.prod<GOAL>a = b
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>g : S →+* T<VAR>u : Set S<VAR>x : S<VAR>hx : x ∈ Subring.closure u<GOAL>g x ∈ Subring.closure (⇑g '' u)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>g : S →+* T<VAR>u : Set S<VAR>x : S<VAR>hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1<GOAL>∀ (S_1 : Subring T), ⇑g '' u ⊆ ↑S_1 → g x ∈ S_1
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>g : S →+* T<VAR>u : Set S<VAR>x : S<VAR>hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1<VAR>T₁ : Subring T<VAR>h₁ : ⇑g '' u ⊆ ↑T₁<GOAL>g x ∈ T₁
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>g : S →+* T<VAR>u : Set S<VAR>x : S<VAR>hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1<VAR>T₁ : Subring T<VAR>h₁ : ⇑g '' u ⊆ ↑T₁<GOAL>x ∈ Subring.comap g T₁
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>g : S →+* T<VAR>u : Set S<VAR>x : S<VAR>hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1<VAR>T₁ : Subring T<VAR>h₁ : ⇑g '' u ⊆ ↑T₁<GOAL>u ⊆ ↑(Subring.comap g T₁)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>g : S →+* T<VAR>u : Set S<VAR>x : S<VAR>hx : ∀ (S_1 : Subring S), u ⊆ ↑S_1 → x ∈ S_1<VAR>T₁ : Subring T<VAR>h₁ : ⇑g '' u ⊆ ↑T₁<GOAL>⇑g '' u ⊆ ↑T₁
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>A : ι → Type u_3<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GMonoid A<VAR>n : ℕ<VAR>f : Fin n → GradedMonoid A<GOAL>(List.ofFn f).prod = mk ((List.finRange n).dProdIndex fun i => (f i).fst) ((List.finRange n).dProd (fun i => (f i).fst) fun i => (f i).snd)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x✝ y z : V<VAR>x : ↑(ofVectorSpaceIndex K V)<GOAL>(extend ⋯) x = ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>H : Nat.Primrec fun n => encode (decode n)<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → σ × β → σ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<VAR>this : Primcodable (List β) := prim H<VAR>G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)<GOAL>Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>H : Nat.Primrec fun n => encode (decode n)<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → σ × β → σ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<VAR>this : Primcodable (List β) := prim H<VAR>G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)<VAR>hG : Primrec₂ G<GOAL>Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>H : Nat.Primrec fun n => encode (decode n)<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → σ × β → σ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<VAR>this : Primcodable (List β) := prim H<VAR>G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)<VAR>hG : Primrec₂ G<VAR>F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)<GOAL>Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>H : Nat.Primrec fun n => encode (decode n)<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → σ × β → σ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<VAR>this : Primcodable (List β) := prim H<VAR>G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)<VAR>hG : Primrec₂ G<VAR>F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)<VAR>hF : Primrec fun a => (F a (encode (f a))).1<GOAL>Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>H : Nat.Primrec fun n => encode (decode n)<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → σ × β → σ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<VAR>this : Primcodable (List β) := prim H<VAR>G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)<VAR>hG : Primrec₂ G<VAR>F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)<VAR>hF : Primrec fun a => (F a (encode (f a))).1<GOAL>∀ (a : α) (n : ℕ), F a n = (List.foldl (fun s b => h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>H : Nat.Primrec fun n => encode (decode n)<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → σ × β → σ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<VAR>this : Primcodable (List β) := prim H<VAR>G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)<VAR>hG : Primrec₂ G<VAR>F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)<VAR>hF : Primrec fun a => (F a (encode (f a))).1<VAR>a : α<VAR>n : ℕ<VAR>IH : ∀ (l : List β) (x : σ), (G a)^[n] (x, l) = (List.foldl (fun s b => h a (s, b)) x (List.take n l), List.drop n l)<VAR>l : List β<VAR>x : σ<GOAL>(G a)^[n + 1] (x, l) = (List.foldl (fun s b => h a (s, b)) x (List.take (n + 1) l), List.drop (n + 1) l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>H : Nat.Primrec fun n => encode (decode n)<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → σ × β → σ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<VAR>this : Primcodable (List β) := prim H<VAR>G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)<VAR>hG : Primrec₂ G<VAR>F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)<VAR>hF : Primrec fun a => (F a (encode (f a))).1<VAR>a : α<VAR>n : ℕ<VAR>IH : ∀ (l : List β) (x : σ), (G a)^[n] (x, l) = (List.foldl (fun s b => h a (s, b)) x (List.take n l), List.drop n l)<VAR>l : List β<VAR>x : σ<GOAL>(G a)^[n] (G a (x, l)) = (List.foldl (fun s b => h a (s, b)) x (List.take (n + 1) l), List.drop (n + 1) l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s t : Set α<VAR>h : s ∈ 𝓝[t] a<GOAL>𝓝[s ∩ t] a = 𝓝[t] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s t : Set α<VAR>h : s ∈ 𝓝[t] a<GOAL>𝓝[t] a ≤ 𝓝[s] a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalRing R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf✝ : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>hf : autoParam (ContinuousOn f ((fun x => -x) '' spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => f (-x)) a = cfc f (-a)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in cofinite, p x) ↔ {x | p x}.Infinite
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>point✝¹ : PointClass F<VAR>a✝¹ : Fin 3 → F<VAR>hP : W.NonsingularLift (Quot.mk Setoid.r a✝¹)<VAR>point✝ : PointClass F<VAR>a✝ : Fin 3 → F<VAR>hQ : W.NonsingularLift (Quot.mk Setoid.r a✝)<GOAL>(mk hP + mk hQ).toAffineLift = (mk hP).toAffineLift + (mk hQ).toAffineLift
<VAR>M : ℝ<VAR>hM : M ≤ 1<VAR>z : ℂ<GOAL>z ∈ stolzSet M ↔ z ∈ ∅
<VAR>M : ℝ<VAR>hM : M ≤ 1<VAR>z : ℂ<GOAL>0 < 1 - ‖z‖ → M * (1 - ‖z‖) ≤ ‖1 - z‖
<VAR>M : ℝ<VAR>hM : M ≤ 1<VAR>z : ℂ<VAR>zn : 0 < 1 - ‖z‖<GOAL>M * (1 - ‖z‖) ≤ ‖1 - z‖
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<GOAL>∫ (x : Fin (n + 1) → ℝ) in Box.Icc I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<GOAL>∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ x : Fin (n + 1), ((∫ (x_1 : Fin n → ℝ) in ↑(I.face x), f (x.insertNth (I.upper x) x_1) x) - ∫ (x_1 : Fin n → ℝ) in ↑(I.face x), f (x.insertNth (I.lower x) x_1) x)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>A : HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) volume.toBoxAdditive.toSMul (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), (f' x) (e i) i ∂volume)<GOAL>∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ x : Fin (n + 1), ((∫ (x_1 : Fin n → ℝ) in ↑(I.face x), f (x.insertNth (I.upper x) x_1) x) - ∫ (x_1 : Fin n → ℝ) in ↑(I.face x), f (x.insertNth (I.lower x) x_1) x)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>A : HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) volume.toBoxAdditive.toSMul (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), (f' x) (e i) i ∂volume)<VAR>B : HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) BoxAdditiveMap.volume (∑ i : Fin (n + 1), (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.upper i) x) i) BoxAdditiveMap.volume - BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume))<GOAL>∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ x : Fin (n + 1), ((∫ (x_1 : Fin n → ℝ) in ↑(I.face x), f (x.insertNth (I.upper x) x_1) x) - ∫ (x_1 : Fin n → ℝ) in ↑(I.face x), f (x.insertNth (I.lower x) x_1) x)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>A : HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) volume.toBoxAdditive.toSMul (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), (f' x) (e i) i ∂volume)<VAR>B : HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) BoxAdditiveMap.volume (∑ i : Fin (n + 1), (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.upper i) x) i) BoxAdditiveMap.volume - BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume))<GOAL>∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), (f' x) (e i) i = ∑ x : Fin (n + 1), ((∫ (x_1 : Fin n → ℝ) in ↑(I.face x), f (x.insertNth (I.upper x) x_1) x) - ∫ (x_1 : Fin n → ℝ) in ↑(I.face x), f (x.insertNth (I.lower x) x_1) x)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℕ<VAR>I : Box (Fin (n + 1))<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hc : ∀ (i : Fin (n + 1)), ContinuousOn (fun y => f y i) (Box.Icc I)<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>Hi : IntegrableOn (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) (Box.Icc I) volume<VAR>A : HasIntegral I ⊥ (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) volume.toBoxAdditive.toSMul (∫ (x : Fin (n + 1) → ℝ) in ↑I, ∑ i : Fin (n + 1), (f' x) (e i) i ∂volume)<VAR>B : HasIntegral I IntegrationParams.GP (fun x => ∑ i : Fin (n + 1), (f' x) (e i) i) BoxAdditiveMap.volume (∑ i : Fin (n + 1), (BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.upper i) x) i) BoxAdditiveMap.volume - BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume))<VAR>i : Fin (n + 1)<VAR>x✝ : i ∈ Finset.univ<GOAL>BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.upper i) x) i) BoxAdditiveMap.volume - BoxIntegral.integral (I.face i) IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume = (∫ (x : Fin n → ℝ) in ↑(I.face i), f (i.insertNth (I.upper i) x) i) - ∫ (x : Fin n → ℝ) in ↑(I.face i), f (i.insertNth (I.lower i) x) i
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x y : R<VAR>hx : x ∈ I<VAR>hy : y ∈ I<GOAL>x + y ∈ I
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hf : TendstoLocallyUniformlyOn F f φ U<VAR>hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U<VAR>hU : IsOpen U<GOAL>TendstoLocallyUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ U