ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>f : G →g G'<VAR>hinj : Injective ⇑f<VAR>u v : V<VAR>p : G.Walk u v<VAR>hp : p.IsPath<VAR>p' : G.Walk u v<VAR>hp' : p'.IsPath<VAR>h : Path.map f hinj ⟨p, hp⟩ = Path.map f hinj ⟨p', hp'⟩<GOAL>⟨p, hp⟩ = ⟨p', hp'⟩
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>f : G →g G'<VAR>hinj : Injective ⇑f<VAR>u v : V<VAR>p : G.Walk u v<VAR>hp : p.IsPath<VAR>p' : G.Walk u v<VAR>hp' : p'.IsPath<VAR>h : Walk.map f p = Walk.map f p'<GOAL>⟨p, hp⟩ = ⟨p', hp'⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>s : Stream' α<GOAL>↑(a :: s) = cons a ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>s : Stream' α<GOAL>↑↑(a :: s) = ↑(cons a ↑s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>s : Stream' α<GOAL>Stream'.map some (a :: s) = some a :: Stream'.map some s
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<GOAL>a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<VAR>B₁ : BilinMap R M R<VAR>Q : QuadraticMap R M N<VAR>B : BilinMap R M R<VAR>x y : M<GOAL>(((associatedHom S) B.toQuadraticMap) x) y = ⅟2 • ((B x) y + (B y) x)
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<VAR>B₁ : BilinMap R M R<VAR>Q : QuadraticMap R M N<VAR>B : BilinMap R M R<VAR>x y : M<GOAL>⅟2 * ((B x) x + (B y) x + ((B x) y + (B y) y) - (B x) x - (B y) y) = ⅟2 * ((B x) y + (B y) x)
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>a b c : α<VAR>h : ContinuousOn f (Icc a b)<VAR>hc : c ∈ Icc a b<GOAL>f c ≤ sSup (f '' Icc a b)
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>a b c : α<VAR>h : ContinuousOn f (Icc a b)<VAR>hc : c ∈ Icc a b<VAR>this : f c ∈ f '' Icc a b<GOAL>f c ≤ sSup (f '' Icc a b)
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>a b c : α<VAR>h : ContinuousOn f (Icc a b)<VAR>hc : c ∈ Icc a b<VAR>this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))<GOAL>f c ≤ sSup (f '' Icc a b)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>r : Rel Y X<VAR>l : Filter Y<VAR>x : X<GOAL>RTendsto' r l (𝓝 x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → r.preimage s ∈ l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>r : Rel Y X<VAR>l : Filter Y<VAR>x : X<GOAL>(∀ s ∈ 𝓝 x, r.preimage s ∈ l) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → r.preimage s ∈ l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>r : Rel Y X<VAR>l : Filter Y<VAR>x : X<GOAL>∀ (s t : Set X), s ⊆ t → r.preimage s ⊆ r.preimage t
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>n k : ℕ<VAR>hk : 0 < k<VAR>hn : k ≤ n<GOAL>n < 2 * k * (n / k)
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>n k : ℕ<VAR>hk : 0 < k<VAR>hn : k ≤ n<GOAL>n % k < k * (n / k)
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>n k : ℕ<VAR>hk : 0 < k<VAR>hn : k ≤ n<GOAL>k ≤ k * (n / k)
<VAR>n : ℕ<GOAL>(2 * (n + 1) + 1)‼ = ∏ i ∈ Finset.range (n + 1), (2 * (i + 1) + 1)
<VAR>n : ℕ<GOAL>(2 * n + 1 + 2)‼ = (2 * n + 1 + 2) * (2 * n + 1)‼
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>ι : Type u_6<VAR>l : Filter ι<VAR>F : ι → C(X, Y)<VAR>f : C(X, Y)<GOAL>Tendsto F l (𝓝 f) ↔ ∀ (K : Set X), IsCompact K → Tendsto (fun i => restrict K (F i)) l (𝓝 (restrict K f))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν✝ : Measure α<VAR>mb : MeasurableSpace β<VAR>ν : Measure β<VAR>g : α → β<VAR>hg : MeasurePreserving g μ ν<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>f : β → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>a : α<VAR>P Q : Finpartition a<VAR>h : P ≤ Q<GOAL>Q.parts.card ≤ P.parts.card
<VAR>a✝ b✝ m n p a b : ℕ<GOAL>(∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p) ↔ a ∣ b
<VAR>a✝ b✝ m n p a b : ℕ<VAR>h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p<GOAL>a ∣ b
<VAR>a✝ b m n p a : ℕ<VAR>h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p<GOAL>a ∣ 0
<VAR>a✝ b✝ m n p a b : ℕ<VAR>h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p<VAR>hb0 : b ≠ 0<GOAL>a ∣ b
<VAR>a✝ b✝ m n p a b : ℕ<VAR>h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p<VAR>hb0 : b ≠ 0<VAR>pa : Prime a<VAR>pb : Prime b<GOAL>a ∣ b
<VAR>a✝ b✝ m n p a b : ℕ<VAR>h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p<VAR>hb0 : b ≠ 0<VAR>pa : Prime a<VAR>pb : Prime b<GOAL>a = b
<VAR>a✝ b✝ m n p a b : ℕ<VAR>h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p<VAR>hb0 : b ≠ 0<VAR>pa : Prime a<VAR>pb : Prime b<VAR>hab : ¬a = b<GOAL>False
<VAR>a✝ b✝ m n p a b : ℕ<VAR>h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p<VAR>hb0 : b ≠ 0<VAR>pa : Prime a<VAR>pb : Prime b<VAR>hab : ¬a = b<GOAL>a = 1
<VAR>a✝ b✝ m n p a b : ℕ<VAR>h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p<VAR>hb0 : b ≠ 0<VAR>pa : Prime a<VAR>pb : Prime b<VAR>hab : ¬a = b<GOAL>b * a ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht✝ ht : Independent t<GOAL>SetIndependent (range t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht✝ ht : Independent t<GOAL>Independent Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht✝ : Independent t<VAR>ht : Independent (Subtype.val ∘ rangeFactorization t)<GOAL>Independent Subtype.val
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : FrechetUrysohnSpace Y<VAR>f : X → Y<VAR>hf : Inducing f<VAR>s : Set X<VAR>x : X<VAR>hx : x ∈ closure s<GOAL>x ∈ seqClosure s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : FrechetUrysohnSpace Y<VAR>f : X → Y<VAR>hf : Inducing f<VAR>s : Set X<VAR>x : X<VAR>hx : ∃ x_1, (∀ (n : ℕ), x_1 n ∈ f '' s) ∧ Tendsto x_1 atTop (𝓝 (f x))<GOAL>x ∈ seqClosure s
<VAR>J : Type u<VAR>inst✝¹ : Category.{?u.24358, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j k : J<VAR>s : Set (F.obj i✝)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>i : J<GOAL>{ obj := fun j => ↑(F.eventualRange j), map := fun {X Y} f => MapsTo.restrict (F.map f) (F.eventualRange X) (F.eventualRange Y) ⋯ }.map (𝟙 i) = 𝟙 ({ obj := fun j => ↑(F.eventualRange j), map := fun {X Y} f => MapsTo.restrict (F.map f) (F.eventualRange X) (F.eventualRange Y) ⋯ }.obj i)
<VAR>J : Type u<VAR>inst✝¹ : Category.{?u.24358, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j k : J<VAR>s : Set (F.obj i✝)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>i : J<GOAL>(fun x => ⟨𝟙 (F.obj i) ↑x, ⋯⟩) = 𝟙 ↑(F.eventualRange i)
<VAR>J : Type u<VAR>inst✝¹ : Category.{?u.24358, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>X✝ Y✝ Z✝ : J<VAR>x✝¹ : X✝ ⟶ Y✝<VAR>x✝ : Y✝ ⟶ Z✝<GOAL>{ obj := fun j => ↑(F.eventualRange j), map := fun {X Y} f => MapsTo.restrict (F.map f) (F.eventualRange X) (F.eventualRange Y) ⋯ }.map (x✝¹ ≫ x✝) = { obj := fun j => ↑(F.eventualRange j), map := fun {X Y} f => MapsTo.restrict (F.map f) (F.eventualRange X) (F.eventualRange Y) ⋯ }.map x✝¹ ≫ { obj := fun j => ↑(F.eventualRange j), map := fun {X Y} f => MapsTo.restrict (F.map f) (F.eventualRange X) (F.eventualRange Y) ⋯ }.map x✝
<VAR>J : Type u<VAR>inst✝¹ : Category.{?u.24358, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>X✝ Y✝ Z✝ : J<VAR>x✝¹ : X✝ ⟶ Y✝<VAR>x✝ : Y✝ ⟶ Z✝<GOAL>(fun x => ⟨(F.map x✝¹ ≫ F.map x✝) ↑x, ⋯⟩) = (fun x => ⟨F.map x✝¹ ↑x, ⋯⟩) ≫ fun x => ⟨F.map x✝ ↑x, ⋯⟩
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset ι<VAR>f : ι → ℕ<VAR>a : β<VAR>x✝³ : ι<VAR>x✝² : Finset ι<VAR>x✝¹ : x✝³ ∉ x✝²<VAR>x✝ : ∏ i ∈ x✝², a ^ f i = a ^ ∑ i ∈ x✝², f i<GOAL>∏ i ∈ cons x✝³ x✝² x✝¹, a ^ f i = a ^ ∑ i ∈ cons x✝³ x✝² x✝¹, f i
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s : Multiset α<VAR>l : List α<VAR>H : ∀ (x : α), x ∉ Quot.mk Setoid.r l<GOAL>Quot.mk Setoid.r l = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s : Multiset α<VAR>l : List α<VAR>H : ∀ (x : α), x ∉ Quot.mk Setoid.r l<GOAL>Quot.mk Setoid.r [] = 0
<VAR>x y : ℝ<GOAL>√x ≠ 0 ↔ 0 < x
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Add R<VAR>inst✝⁴ : Mul R<VAR>inst✝³ : Neg R<VAR>inst✝² : One R<VAR>inst✝¹ : Zero R<VAR>inst✝ : CompatibleRing R<VAR>x y : ring.Term α<VAR>v : α → R<GOAL>Term.realize v (x + y) = Term.realize v x + Term.realize v y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LeftCancelMonoid G<VAR>x y a : G<VAR>m✝ n✝ : ℕ<VAR>h : orderOf x = 0<VAR>n m : ℕ<GOAL>x ^ n = x ^ m ↔ n = m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S✝ T : α → α → Prop<VAR>a : α<VAR>l✝ l : List α<VAR>hl : Pairwise R l<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>h : ∀ (x : α), x ∈ l → p x<VAR>S : β → β → Prop<VAR>hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)<GOAL>Pairwise S (List.pmap f l h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S✝ T : α → α → Prop<VAR>a : α<VAR>l✝ l : List α<VAR>hl : Pairwise R l<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>h : ∀ (x : α), x ∈ l → p x<VAR>S : β → β → Prop<VAR>hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)<GOAL>∀ {a b : α}, a ∈ l → b ∈ l → R a b → ∀ (h₁ : p a) (h₂ : p b), S (f a h₁) (f b h₂)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulOneClass P<VAR>S✝ : Submonoid M<VAR>A : Type u_4<VAR>inst✝ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>S : Submonoid M<GOAL>S = ⊥ ∨ Nontrivial ↥S
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝² : CommGroup G<VAR>g g' : G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>f : ℕ → G<VAR>k : ℕ<GOAL>HasProd (fun n => f (n + k)) g ↔ HasProd f (g * ∏ i ∈ range k, f i)
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝² : CommGroup G<VAR>g g' : G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>f : ℕ → G<VAR>k : ℕ<GOAL>HasProd (fun n => f (n + k)) g ↔ HasProd (fun x => f ↑x) g
<VAR>M : Type u_1<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : MeasurableSpace M<VAR>inst✝³ : MeasurableMul₂ M<VAR>μ ν ρ : Measure M<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite ρ<GOAL>map (fun x => x.1 * x.2) (μ.prod (ν + ρ)) = map (fun x => x.1 * x.2) (μ.prod ν) + map (fun x => x.1 * x.2) (μ.prod ρ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<GOAL>s ∩ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s ∩ t i j
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ (last n)<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.castSucc<VAR>i : Fin n<VAR>y : α✝ i.castSucc<VAR>z : α✝ (last n)<VAR>α : Type u_1<VAR>as : Fin n → α<VAR>bs : Fin m → α<VAR>b : α<GOAL>append as (snoc bs b) = snoc (append as bs) b
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ (last n)<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.castSucc<VAR>i✝ : Fin n<VAR>y : α✝ i✝.castSucc<VAR>z : α✝ (last n)<VAR>α : Type u_1<VAR>as : Fin n → α<VAR>bs : Fin m → α<VAR>b : α<VAR>i : Fin (n + (m + 1))<GOAL>append as (snoc bs b) i = snoc (append as bs) b i
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ (last n)<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.castSucc<VAR>i✝ : Fin n<VAR>y : α✝ i✝.castSucc<VAR>z : α✝ (last n)<VAR>α : Type u_1<VAR>as : Fin n → α<VAR>bs : Fin m → α<VAR>b : α<VAR>i : ℕ<VAR>isLt : i < n + (m + 1)<GOAL>append as (snoc bs b) ⟨i, isLt⟩ = snoc (append as bs) b ⟨i, isLt⟩
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ (last n)<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.castSucc<VAR>i✝ : Fin n<VAR>y : α✝ i✝.castSucc<VAR>z : α✝ (last n)<VAR>α : Type u_1<VAR>as : Fin n → α<VAR>bs : Fin m → α<VAR>b : α<VAR>i : ℕ<VAR>isLt : i < n + (m + 1)<GOAL>(if h : i < n then as ⟨i, ⋯⟩ else if h_1 : i - n < m then bs ⟨i - n, ⋯⟩ else b) = if h : i < n + m then if h_1 : i < n then as ⟨i, ⋯⟩ else bs ⟨i - n, ⋯⟩ else b
<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✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d✝ : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (x / c - d) = c • ∫ (x : ℝ) in a / c - d..b / c - d, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Integrable (fun x => κ.density ν a x s) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Memℒp (fun x => κ.density ν a x s) 1 (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => κ.density ν a x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>eLpNorm (fun x => κ.density ν a x s) 1 (ν a) < ⊤
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>c : ℂ<VAR>f : ℂ → F<VAR>R : ℝ≥0<VAR>hR : 0 < ↑R<VAR>hf : DiffContOnCl ℂ f (ball c ↑R)<GOAL>deriv f c = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - c) ^ (-2) • f z
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : CompleteSpace F<VAR>c : ℂ<VAR>f : ℂ → F<VAR>R : ℝ≥0<VAR>hR : 0 < ↑R<VAR>hf : DiffContOnCl ℂ f (ball c ↑R)<GOAL>((cauchyPowerSeries f c (↑R) 1) fun x => 1) = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - c) ^ (-2) • f z
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g✝ : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<VAR>C₁ C₂ C₃ : ℝ<VAR>h : C₃ = C₂ * C₁<VAR>hg : ‖g‖ ≤ C₂<VAR>hf : ‖f‖ ≤ C₁<GOAL>‖g.comp f‖ ≤ C₂ * C₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s t : Set α<VAR>x : α<VAR>h : t ∈ 𝓝 x<GOAL>ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x
<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>S : Type u_1<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<GOAL>(map W' f).toJacobian.polynomialY = (MvPolynomial.map f) W'.polynomialY
<VAR>n✝ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>n : ℕ+<VAR>inst✝ : IsDomain B<VAR>ζ : B<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>adjoin A ((cyclotomic (↑n) A).rootSet B) = adjoin A {ζ}
<VAR>n✝ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>n : ℕ+<VAR>inst✝ : IsDomain B<VAR>ζ : B<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>x : B<VAR>hx : x ∈ (cyclotomic (↑n) A).rootSet B<GOAL>x ∈ ↑(adjoin A {ζ})
<VAR>n✝ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>n : ℕ+<VAR>inst✝ : IsDomain B<VAR>ζ : B<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>x : B<VAR>hx : x ∈ {ζ}<GOAL>x ∈ (cyclotomic (↑n) A).rootSet B
<VAR>n m : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ last n<GOAL>i.castPred hi ≤ j ↔ i ≤ j.castSucc
<VAR>b : ℕ<GOAL>Monotone (log b)
<VAR>b n : ℕ<GOAL>log b n ≤ log b (n + 1)
<VAR>b n : ℕ<VAR>hb : b ≤ 1<GOAL>log b n ≤ log b (n + 1)
<VAR>b n : ℕ<VAR>hb : 1 < b<GOAL>log b n ≤ log b (n + 1)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : Finite m<VAR>inst✝⁵ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁴ : AddCommMonoid M₁<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>inst✝ : DecidableEq M₁<VAR>f : M₁ →ₗ[R] M₂<VAR>k : m<VAR>i : n<GOAL>(toMatrix v₁.reindexRange v₂.reindexRange) f ⟨v₂ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (toMatrix v₁ v₂) f k i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>a ⊔ b ⇨ a ⇔ b = a ⇔ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b
<VAR>X Y Z : Type u<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<VAR>w : f ≫ g = f ≫ h<VAR>t : IsLimit (Fork.ofι f w)<VAR>y : Y<VAR>hy : g y = h y<VAR>y' : PUnit.{u + 1} ⟶ Y := fun x => y<GOAL>∃! x, f x = y
<VAR>X Y Z : Type u<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<VAR>w : f ≫ g = f ≫ h<VAR>t : IsLimit (Fork.ofι f w)<VAR>y : Y<VAR>hy : g y = h y<VAR>y' : PUnit.{u + 1} ⟶ Y := fun x => y<VAR>hy' : y' ≫ g = y' ≫ h<GOAL>∃! x, f x = y
<VAR>X Y Z : Type u<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<VAR>w : f ≫ g = f ≫ h<VAR>t : IsLimit (Fork.ofι f w)<VAR>y : Y<VAR>hy : g y = h y<VAR>y' : PUnit.{u + 1} ⟶ Y := fun x => y<VAR>hy' : y' ≫ g = y' ≫ h<GOAL>∀ (y_1 : X), (fun x => f x = y) y_1 → y_1 = ↑(Fork.IsLimit.lift' t y' hy') PUnit.unit
<VAR>X Y Z : Type u<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<VAR>w : f ≫ g = f ≫ h<VAR>t : IsLimit (Fork.ofι f w)<VAR>y : Y<VAR>hy : g y = h y<VAR>y' : PUnit.{u + 1} ⟶ Y := fun x => y<VAR>hy' : y' ≫ g = y' ≫ h<VAR>x' : X<VAR>hx' : f x' = y<GOAL>(fun x => x') = ↑(Fork.IsLimit.lift' t y' hy')
<VAR>X Y Z : Type u<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<VAR>w : f ≫ g = f ≫ h<VAR>t : IsLimit (Fork.ofι f w)<VAR>y : Y<VAR>hy : g y = h y<VAR>y' : PUnit.{u + 1} ⟶ Y := fun x => y<VAR>hy' : y' ≫ g = y' ≫ h<VAR>x' : X<VAR>hx' : f x' = y<GOAL>(fun x => x') ≫ (Fork.ofι f w).ι = ↑(Fork.IsLimit.lift' t y' hy') ≫ (Fork.ofι f w).ι
<VAR>X Y Z : Type u<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<VAR>w : f ≫ g = f ≫ h<VAR>t : IsLimit (Fork.ofι f w)<VAR>y : Y<VAR>hy : g y = h y<VAR>y' : PUnit.{u + 1} ⟶ Y := fun x => y<VAR>hy' : y' ≫ g = y' ≫ h<VAR>x' : X<VAR>hx' : f x' = y<GOAL>((fun x => x') ≫ (Fork.ofι f w).ι) PUnit.unit = (↑(Fork.IsLimit.lift' t y' hy') ≫ (Fork.ofι f w).ι) PUnit.unit
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<GOAL>0 * x + 1 * 1 = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : Ring k<VAR>inst✝ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>h : i ≠ j<GOAL>(b.coord i) (b j) = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : Zero α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f g : ι →₀ α<GOAL>(Ioo f g).card = ∏ i ∈ f.support ∪ g.support, (Icc (f i) (g i)).card - 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>b c d : α<VAR>hc : AddLECancellable c<VAR>h : b - c + c < b<GOAL>False
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>F : C ⥤ D<VAR>inst✝² : HasBinaryBiproducts C<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : PreservesBinaryBiproducts F<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>F.map (f + g) = F.map f + F.map g
<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✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c✝ d✝ : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c⁻¹ • ∫ (x : ℝ) in a..b, f (d + x / c) = ∫ (x : ℝ) in d + a / c..d + b / c, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>f g : α → β<VAR>m m' : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>hf : StronglyMeasurable f<VAR>h_mono : m' ≤ m<GOAL>StronglyMeasurable f