ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a✝ : P<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a✝)<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : P<VAR>h : (s.smulAntidiagonal t a).Infinite<VAR>h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>isrfl : IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>istrns : IsTrans (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)<VAR>g : ℕ ↪o ℕ<VAR>hg : ∀ (m n : ℕ), m ≤ n → (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g m)) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g n))<VAR>m n : ℕ<VAR>mn : m < n<VAR>h2' : (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g m)) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g n))<GOAL>(Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g m) = (Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g n)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I✝ : Ideal α<VAR>a b : α<VAR>I J : Ideal α<GOAL>I < J → J = ⊤ ↔ ∀ (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I✝ : Ideal α<VAR>a b : α<VAR>I J : Ideal α<GOAL>I ≤ J ∧ ¬J ≤ I → J = ⊤ ↔ ∀ (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>b ∈ Icc a b ↔ a ≤ b
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>ht : t ∈ 𝓝 x<GOAL>mfderivWithin I I' f (s ∩ t) x = mfderivWithin I I' f s x
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SymmetricRel V → (s ∩ ball x V).Nonempty
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ✝ γ₁ γ₂ : Cochain K L n✝<VAR>n' a : ℤ<VAR>γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<VAR>x : Rˣ<GOAL>(x • γ).rightUnshift n hn = x • γ.rightUnshift n hn
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<VAR>a0 : a = 0<GOAL>a % a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<VAR>a0 : ¬a = 0<GOAL>a % a = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>a✝ : Nontrivial R<GOAL>W.polynomial.Monic
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<GOAL>Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<GOAL>Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
<VAR>a : ℤ<GOAL>(↑a)⁻¹.den = if a = 0 then 1 else a.natAbs
<VAR>a : ℤ<GOAL>↑(↑a)⁻¹.den = ↑(if a = 0 then 1 else a.natAbs)
<VAR>a : ℤ<VAR>lt : a < 0<GOAL>↑(↑a)⁻¹.den = ↑(if a = 0 then 1 else a.natAbs)
<GOAL>↑(↑0)⁻¹.den = ↑(if 0 = 0 then 1 else Int.natAbs 0)
<VAR>a : ℤ<VAR>gt : 0 < a<GOAL>↑(↑a)⁻¹.den = ↑(if a = 0 then 1 else a.natAbs)
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x y : E<GOAL>∀ a ∈ closedBall 0 1, 0 ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>s : Finset α<VAR>t : Finset β<VAR>a a' : α<VAR>b b' : β<VAR>inst✝² : DecidablePred (r a)<VAR>inst✝¹ : (a : α) → Decidable (r a b)<VAR>m n : ℕ<VAR>inst✝ : (a : α) → (b : β) → Decidable (r a b)<GOAL>∑ a ∈ s, (bipartiteAbove r t a).card = ∑ b ∈ t, (bipartiteBelow r s b).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>s : Finset α<VAR>t : Finset β<VAR>a a' : α<VAR>b b' : β<VAR>inst✝² : DecidablePred (r a)<VAR>inst✝¹ : (a : α) → Decidable (r a b)<VAR>m n : ℕ<VAR>inst✝ : (a : α) → (b : β) → Decidable (r a b)<GOAL>(∑ x ∈ s, ∑ a ∈ t, if r x a then 1 else 0) = ∑ x ∈ t, ∑ a ∈ s, if r a x then 1 else 0
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝² : Category.{u, v} C<VAR>A : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasColimits C<VAR>𝓕 : Presheaf C X<VAR>c : C<VAR>f : 𝓕.stalk p₀ ⟶ c<VAR>U : (OpenNhds p₀)ᵒᵖ<GOAL>colimit.ι (((whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).obj 𝓕) U ≫ fromStalk p₀ (toSkyscraperPresheaf p₀ f) = colimit.ι (((whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).obj 𝓕) U ≫ f
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝² : Category.{u, v} C<VAR>A : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasColimits C<VAR>𝓕 : Presheaf C X<VAR>c : C<VAR>f : 𝓕.stalk p₀ ⟶ c<VAR>U : (OpenNhds p₀)ᵒᵖ<GOAL>{ pt := c, ι := { app := fun U => (toSkyscraperPresheaf p₀ f).app (op (unop U).obj) ≫ eqToHom ⋯, naturality := ⋯ } }.ι.app U = colimit.ι (((whiskeringLeft (OpenNhds p₀)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion p₀).op).obj 𝓕) U ≫ f
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝² : Category.{u, v} C<VAR>A : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasColimits C<VAR>𝓕 : Presheaf C X<VAR>c : C<VAR>f : 𝓕.stalk p₀ ⟶ c<VAR>U : (OpenNhds p₀)ᵒᵖ<GOAL>(if h : p₀ ∈ (unop U).obj then 𝓕.germ ⟨p₀, h⟩ ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj (op (unop U).obj))) ≫ eqToHom ⋯ = colimit.ι ((OpenNhds.inclusion p₀).op ⋙ 𝓕) U ≫ f
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝² : Category.{u, v} C<VAR>A : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasColimits C<VAR>𝓕 : Presheaf C X<VAR>c : C<VAR>f : 𝓕.stalk p₀ ⟶ c<VAR>U : (OpenNhds p₀)ᵒᵖ<GOAL>(𝓕.germ ⟨p₀, ⋯⟩ ≫ f ≫ eqToHom ⋯) ≫ eqToHom ⋯ = colimit.ι ((OpenNhds.inclusion p₀).op ⋙ 𝓕) U ≫ f
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝² : Category.{u, v} C<VAR>A : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasColimits C<VAR>𝓕 : Presheaf C X<VAR>c : C<VAR>f : 𝓕.stalk p₀ ⟶ c<VAR>U : (OpenNhds p₀)ᵒᵖ<GOAL>colimit.ι ((OpenNhds.inclusion ↑⟨p₀, ⋯⟩).op ⋙ 𝓕) (op { obj := (unop U).obj, property := ⋯ }) ≫ f = colimit.ι ((OpenNhds.inclusion p₀).op ⋙ 𝓕) U ≫ f
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<GOAL>((continuousMultilinearCurryFin1 𝕜 ((i : ι) → E i) F) (f.toFormalMultilinearSeries.changeOrigin x 1)) y = (f.linearDeriv x) y
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<GOAL>(∑' (n : ℕ), (f.toFormalMultilinearSeries.changeOriginSeries 1 n) fun x_1 => x) (Fin.snoc 0 y) = ∑ i : ι, f (Function.update x i (y i))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : IsEmpty ι<GOAL>(∑' (n : ℕ), (f.toFormalMultilinearSeries.changeOriginSeries 1 n) fun x_1 => x) (Fin.snoc 0 y) = ∑ i : ι, f (Function.update x i (y i))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<GOAL>(∑' (n : ℕ), (f.toFormalMultilinearSeries.changeOriginSeries 1 n) fun x_1 => x) (Fin.snoc 0 y) = ∑ i : ι, f (Function.update x i (y i))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<GOAL>((∑ s : { s // s.card = Fintype.card ι - 1 }, f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑s ⋯) fun x_1 => x) (Fin.snoc 0 y) = ∑ i : ι, f (Function.update x i (y i))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<GOAL>∀ (b' : ℕ), b' ≠ Fintype.card ι - 1 → ((f.toFormalMultilinearSeries.changeOriginSeries 1 b') fun x_1 => x) = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<GOAL>(∑ a : { s // s.card = Fintype.card ι - 1 }, ((f.toFormalMultilinearSeries.changeOriginSeriesTerm 1 (Fintype.card ι - 1) ↑a ⋯) fun x_1 => x) fun x => y) = ∑ i : ι, f (Function.update x i (y i))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<GOAL>∑ x_1 : { s // s.card = Fintype.card ι - 1 }, (f.toFormalMultilinearSeries (1 + (Fintype.card ι - 1))) ((↑x_1).piecewise (fun x_2 => x) fun x => y) = ∑ i : ι, f (Function.update x i (y i))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<GOAL>Fin (Nat.succ 0 + (Fintype.card ι - Nat.succ 0)) → { s // s.card = Fintype.card ι - 1 }
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<GOAL>Function.Bijective ?h.inr.refine_1
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<VAR>i : ι<GOAL>f (Function.update x i (y i)) = (f.toFormalMultilinearSeries (1 + (Fintype.card ι - 1))) ((↑((?h.inr.refine_1 ∘ ⇑(Fintype.equivFinOfCardEq ⋯)) i)).piecewise (fun x_1 => x) fun x => y)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<VAR>i : ι<GOAL>f (Function.update x i (y i)) = (f.toFormalMultilinearSeries (1 + (Fintype.card ι - 1))) ((↑(((fun x => ⟨{x}ᶜ, ⋯⟩) ∘ ⇑(Fintype.equivFinOfCardEq ⋯)) i)).piecewise (fun x_1 => x) fun x => y)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<VAR>i : ι<GOAL>f (Function.update x i (y i)) = (domDomCongr (Fintype.equivFinOfCardEq ⋯) (f.compContinuousLinearMap ContinuousLinearMap.proj)) (Function.update (fun x_1 => x) ((Fintype.equivFinOfCardEq ⋯) i) y)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<VAR>i : ι<GOAL>f (Function.update x i (y i)) = f fun i_1 => if i_1 = i then y i_1 else x i_1
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<VAR>i j : ι<GOAL>Function.update x i (y i) j = if j = i then y j else x j
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<VAR>j : ι<GOAL>Function.update x j (y j) j = if j = j then y j else x j
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<VAR>inst✝ : DecidableEq ι<VAR>y : (i : ι) → E i<VAR>h✝ : Nonempty ι<VAR>i j : ι<VAR>hj : j ≠ i<GOAL>Function.update x i (y i) j = if j = i then y j else x j
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁹ : RCLike 𝕂<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : (i : m) → Fintype (n' i)<VAR>inst✝³ : (i : m) → DecidableEq (n' i)<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → Matrix m m 𝔸<VAR>h : (↑s).Pairwise fun i j => Commute (f i) (f j)<VAR>this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing<VAR>this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing<VAR>this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra<GOAL>exp 𝕂 (∑ i ∈ s, f i) = s.noncommProd (fun i => exp 𝕂 (f i)) ⋯
<VAR>J : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝ : Category.{v₂, u₂} K<VAR>h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j'<VAR>α✝ : Type u₁<VAR>F : J ⥤ Discrete α✝<VAR>j₁✝ j₂✝ : J<VAR>f : j₁✝ ⟶ j₂✝<GOAL>(F.obj j₁✝).as = (F.obj j₂✝).as
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>h : l.NodupKeys<GOAL>(lookupAll a l).length ≤ 1
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>h : l.NodupKeys<VAR>this : (map Sigma.fst (map (Sigma.mk a) (lookupAll a l))).Nodup<GOAL>(lookupAll a l).length ≤ 1
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<VAR>h : l.NodupKeys<VAR>this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup<GOAL>(lookupAll a l).length ≤ 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>n : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f g : 𝕜 → F<VAR>hfg : Set.EqOn f g s<GOAL>Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) s
<VAR>p : ℕ<GOAL>Nat.rec (unpair p).1 (fun y IH => IH + 1) (unpair p).2 = (unpair p).1 + (unpair p).2
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x✝ : ⨂[𝕜] (i : ι), E i<GOAL>((liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i)) (tprodL 𝕜)) x✝ = (ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)) x✝
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a✝ a b : R<VAR>dvd : a ∣ b<GOAL>torsionBy R M a ≤ torsionBy R M b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a✝ a b : R<VAR>dvd : a ∣ b<GOAL>torsionBySet R M ↑(span R {a}) ≤ torsionBySet R M {b}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a✝ a b : R<VAR>dvd : a ∣ b<GOAL>{b} ⊆ ↑(span R {a})
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a✝ a c : R<VAR>dvd : a ∣ c<GOAL>c ∈ ↑(span R {a})
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x<VAR>f : ι' → ι<VAR>hf : Injective f<VAR>p q : MvPolynomial ι' R<GOAL>(aeval (x ∘ f)) p = (aeval (x ∘ f)) q → p = q
<VAR>z : ℍ<VAR>k : ℝ<VAR>hk : 2 < k<GOAL>Summable fun x => ‖x‖ ^ (-k)
<VAR>z : ℍ<VAR>k : ℝ<VAR>hk : 2 < k<GOAL>(∀ (j : ℕ), Summable fun i => ((fun x => ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm) ↑i) ∧ Summable fun j => ∑' (i : ↑fun i => i ∈ (box j).val), ((fun x => ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm) ↑i
<VAR>z : ℍ<VAR>k : ℝ<VAR>hk : 2 < k<GOAL>0 ≤ (fun x => ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<GOAL>(f.extend I).target = ↑I.symm ⁻¹' f.target ∩ range ↑I
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<GOAL>[IsCoprime I J, Codisjoint I J, I + J = 1, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<GOAL>[IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J].TFAE
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : T1Space α<VAR>inst✝ : Countable α<GOAL>borel α = ⊤