ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : DivisionRing K<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : AddCommGroup V'<VAR>inst✝⁶ : Module K V'<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module K V₁<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : AddCommGroup V₃<VAR>inst✝ : Module K V₃<VAR>db : V₂ →ₗ[K] V<VAR>eb : V₃ →ₗ[K] V<VAR>cd : V₁ →ₗ[K] V₂<VAR>ce : V₁ →ₗ[K] V₃<VAR>hde : ⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb<VAR>hgd : ker cd = ⊥<VAR>eq : db ∘ₗ cd = eb ∘ₗ ce<VAR>eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e<GOAL>Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : DivisionRing K<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : AddCommGroup V'<VAR>inst✝⁶ : Module K V'<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module K V₁<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : AddCommGroup V₃<VAR>inst✝ : Module K V₃<VAR>db : V₂ →ₗ[K] V<VAR>eb : V₃ →ₗ[K] V<VAR>cd : V₁ →ₗ[K] V₂<VAR>ce : V₁ →ₗ[K] V₃<VAR>hde : ⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb<VAR>hgd : ker cd = ⊥<VAR>eq : db ∘ₗ cd = eb ∘ₗ ce<VAR>eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e<VAR>hf : Surjective ⇑(db.coprod eb)<GOAL>Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : DivisionRing K<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : AddCommGroup V'<VAR>inst✝⁶ : Module K V'<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module K V₁<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : AddCommGroup V₃<VAR>inst✝ : Module K V₃<VAR>db : V₂ →ₗ[K] V<VAR>eb : V₃ →ₗ[K] V<VAR>cd : V₁ →ₗ[K] V₂<VAR>ce : V₁ →ₗ[K] V₃<VAR>hde : ⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb<VAR>hgd : ker cd = ⊥<VAR>eq : db ∘ₗ cd = eb ∘ₗ ce<VAR>eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e<VAR>hf : Surjective ⇑(db.coprod eb)<GOAL>Module.rank K V + Module.rank K V₁ = Module.rank K V + Module.rank K ↥(ker (db.coprod eb))
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : DivisionRing K<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : AddCommGroup V'<VAR>inst✝⁶ : Module K V'<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module K V₁<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : AddCommGroup V₃<VAR>inst✝ : Module K V₃<VAR>db : V₂ →ₗ[K] V<VAR>eb : V₃ →ₗ[K] V<VAR>cd : V₁ →ₗ[K] V₂<VAR>ce : V₁ →ₗ[K] V₃<VAR>hde : ⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb<VAR>hgd : ker cd = ⊥<VAR>eq : db ∘ₗ cd = eb ∘ₗ ce<VAR>eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e<VAR>hf : Surjective ⇑(db.coprod eb)<GOAL>Module.rank K V₁ = Module.rank K ↥(ker (db.coprod eb))
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : DivisionRing K<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : AddCommGroup V'<VAR>inst✝⁶ : Module K V'<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module K V₁<VAR>inst✝³ : AddCommGroup V₂<VAR>inst✝² : Module K V₂<VAR>inst✝¹ : AddCommGroup V₃<VAR>inst✝ : Module K V₃<VAR>db : V₂ →ₗ[K] V<VAR>eb : V₃ →ₗ[K] V<VAR>cd : V₁ →ₗ[K] V₂<VAR>ce : V₁ →ₗ[K] V₃<VAR>hde : ⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb<VAR>hgd : ker cd = ⊥<VAR>eq : db ∘ₗ cd = eb ∘ₗ ce<VAR>eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e<VAR>hf : Surjective ⇑(db.coprod eb)<GOAL>V₁ ≃ₗ[K] ↥(ker (db.coprod eb))
<VAR>a b c b' c' : ℕ<VAR>h1 : a.pow b' = c'<VAR>hb : 2 * b' = b<VAR>hc : c' * c' = c<GOAL>(Int.negOfNat a).pow b = Int.ofNat c
<VAR>a b c b' c' : ℕ<VAR>h1 : a.pow b' = c'<VAR>hb : 2 * b' = b<VAR>hc : c' * c' = c<GOAL>Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat (a.pow b' * a.pow b')
<VAR>m n✝ : ℕ<VAR>C : ℕ → Sort u<VAR>H₁ H₂ : (b : Bool) → (n : ℕ) → C (bit b n)<VAR>h : (fun H n => n.bitCasesOn H) H₁ = (fun H n => n.bitCasesOn H) H₂<VAR>b : Bool<VAR>n : ℕ<GOAL>H₁ b n = H₂ b n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>Disjoint {a} s ↔ a ∉ s
<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<VAR>h0 : p₃ ≠ p₂<GOAL>∠ p₂ p₃ p₁ = Real.arctan (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<VAR>h0 : p₃ ≠ p₂<GOAL>∠ p₂ p₃ p₁ = Real.arctan (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<VAR>h0 : p₂ -ᵥ p₃ ≠ 0<GOAL>∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type v<VAR>X✝ Y✝ : C<VAR>S✝ : Sieve X✝<VAR>R : Presieve X✝<VAR>J✝ J₂ : GrothendieckTopology C<VAR>Ps : Set (Cᵒᵖ ⥤ Type v)<VAR>J : GrothendieckTopology C<VAR>hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P<VAR>X : C<VAR>S : Sieve X<VAR>hS : S ∈ J.sieves X<VAR>P : Cᵒᵖ ⥤ Type v<VAR>hP : P ∈ Ps<VAR>Y : C<VAR>f : Y ⟶ X<GOAL>Presieve.IsSheafFor P (Sieve.pullback f S).arrows
<VAR>x y : ℝ<GOAL>tan (-x) = -tan x
<VAR>r : ℝ<GOAL>abs ↑r = |r|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>dec : DecidableEq α<VAR>a b : α<VAR>g : β → γ<VAR>f : α → β<VAR>R S : RegularExpression α<GOAL>map g (map f (R + S)) = map (g ∘ f) (R + S)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>dec : DecidableEq α<VAR>a b : α<VAR>g : β → γ<VAR>f : α → β<VAR>R S : RegularExpression α<GOAL>map g (map f (R.comp S)) = map (g ∘ f) (R.comp S)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>dec : DecidableEq α<VAR>a b : α<VAR>g : β → γ<VAR>f : α → β<VAR>R : RegularExpression α<GOAL>map g (map f R.star) = map (g ∘ f) R.star
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁✝ a₂✝ : α<VAR>b✝ b₁ b₂ : β<VAR>γ : Type u_3<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Preorder β<VAR>inst✝⁴ : Zero γ<VAR>inst✝³ : Preorder γ<VAR>inst✝² : SMul α β<VAR>inst✝¹ : SMul α γ<VAR>f : β → γ<VAR>inst✝ : SMulPosReflectLE α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<VAR>zero : f 0 = 0<VAR>b : β<VAR>hb : 0 < b<VAR>a₁ a₂ : α<VAR>h : a₁ • b ≤ a₂ • b<GOAL>a₁ ≤ a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁✝ a₂✝ : α<VAR>b✝ b₁ b₂ : β<VAR>γ : Type u_3<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Preorder β<VAR>inst✝⁴ : Zero γ<VAR>inst✝³ : Preorder γ<VAR>inst✝² : SMul α β<VAR>inst✝¹ : SMul α γ<VAR>f : β → γ<VAR>inst✝ : SMulPosReflectLE α γ<VAR>b : β<VAR>a₁ a₂ : α<VAR>hf : ∀ {b₁ b₂ : β}, True<VAR>smul : α → β → True<VAR>zero : True<VAR>hb : 0 < f b<VAR>h : a₁ • f b ≤ a₂ • f b<GOAL>a₁ ≤ a₂
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>(w * cs.simple i * w⁻¹)⁻¹ = w * cs.simple i * w⁻¹
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r : R → R → Prop<VAR>f g : RingQuot r →+* T<VAR>w : f.comp (mkRingHom r) = g.comp (mkRingHom r)<VAR>x : RingQuot r<GOAL>f x = g x
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r✝ : R → R → Prop<VAR>inst✝ : Semiring T<VAR>r : R → R → Prop<VAR>f g : RingQuot r →+* T<VAR>w : f.comp (mkRingHom r) = g.comp (mkRingHom r)<VAR>x : R<GOAL>f ((mkRingHom r) x) = g ((mkRingHom r) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : Prop<VAR>o : Part α<VAR>h : p → o.Dom<VAR>a : α<GOAL>a ∈ restrict p o h ↔ p ∧ a ∈ o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : Prop<VAR>o : Part α<VAR>h : p → o.Dom<VAR>a : α<GOAL>(∃ (h_1 : p), o.get ⋯ = a) ↔ p ∧ ∃ (h : o.Dom), o.get h = a
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cone F<VAR>X : C<VAR>h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones<VAR>s : Cone F<GOAL>{ pt := s.pt, π := h.hom.app (op s.pt) { down := (h.inv.app (op s.pt) s.π).down } } = s
<VAR>a b c d m n✝ : ℤ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>m.toNat < n ↔ m < ↑n
<VAR>a b c d m n✝ : ℤ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>0 < ↑n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>p δ : ℝ≥0∞<VAR>hδ : δ ≠ 0<GOAL>∃ η, 0 < η ∧ ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>p δ : ℝ≥0∞<VAR>hδ : δ ≠ 0<VAR>this : Tendsto (fun η => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 (LpAddConst p * (0 + 0)))<GOAL>∃ η, 0 < η ∧ ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>p δ : ℝ≥0∞<VAR>hδ : δ ≠ 0<VAR>this : Tendsto (fun η => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 0)<GOAL>∃ η, 0 < η ∧ ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>p δ : ℝ≥0∞<VAR>hδ : δ ≠ 0<VAR>this : Tendsto (fun η => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 0)<VAR>η : ℝ≥0∞<VAR>hη : LpAddConst p * (η + η) < δ<VAR>ηpos : 0 < η<GOAL>∃ η, 0 < η ∧ ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g✝ : α → E<VAR>p δ : ℝ≥0∞<VAR>hδ : δ ≠ 0<VAR>this : Tendsto (fun η => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 0)<VAR>η : ℝ≥0∞<VAR>hη : LpAddConst p * (η + η) < δ<VAR>ηpos : 0 < η<VAR>f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>Hf : eLpNorm f p μ ≤ η<VAR>Hg : eLpNorm g p μ ≤ η<GOAL>eLpNorm (f + g) p μ < δ
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ inst✝⁴ : CommSemiring R✝<VAR>inst✝³ : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝¹ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>F✝ G✝ : MvPolynomial σ R<VAR>n✝ : ℕ<VAR>inst✝ : Infinite R<VAR>F G : MvPolynomial σ R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>hG : G.IsHomogeneous n<VAR>h : ∀ (r : σ → R), (eval r) F = (eval r) G<GOAL>F = G
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ inst✝⁴ : CommSemiring R✝<VAR>inst✝³ : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝¹ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>F✝ G✝ : MvPolynomial σ R<VAR>n✝ : ℕ<VAR>inst✝ : Infinite R<VAR>F G : MvPolynomial σ R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>hG : G.IsHomogeneous n<VAR>h : ∀ (r : σ → R), (eval r) F = (eval r) G<GOAL>↑n ≤ #R
<VAR>this : Fact (0 < 2 * π)<GOAL>IsLocalHomeomorph ⇑expMapCircle
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 3)<VAR>H : i.castSucc < j<VAR>hj : j = 0<GOAL>False
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 3)<VAR>H : i.castSucc < j<GOAL>δ i ≫ δ j = δ (j.pred ⋯) ≫ δ i.castSucc
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 3)<VAR>H : i.castSucc < j<GOAL>δ i ≫ δ j = δ i ≫ δ (j.pred ⋯).succ
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 3)<VAR>H : i.castSucc < j<GOAL>i ≤ j.pred ⋯
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝¹ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsOpenImmersion f<VAR>H : P g<GOAL>P (f ≫ g)
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝¹ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsOpenImmersion f<VAR>H : ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U), Q (Scheme.Hom.appLE g (↑U) (↑V) e)<GOAL>∀ (U : ↑Z.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U), Q (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e)
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝¹ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsOpenImmersion f<VAR>H : ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U), Q (Scheme.Hom.appLE g (↑U) (↑V) e)<VAR>U : ↑Z.affineOpens<VAR>V : ↑X.affineOpens<VAR>e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U<GOAL>Q (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e)
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝¹ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsOpenImmersion f<VAR>H : ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U), Q (Scheme.Hom.appLE g (↑U) (↑V) e)<VAR>U : ↑Z.affineOpens<VAR>V : ↑X.affineOpens<VAR>e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U<VAR>this : IsIso (Scheme.Hom.appLE f (f ''ᵁ ↑V) ↑V ⋯)<GOAL>Q (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e)
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝¹ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsOpenImmersion f<VAR>H : ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U), Q (Scheme.Hom.appLE g (↑U) (↑V) e)<VAR>U : ↑Z.affineOpens<VAR>V : ↑X.affineOpens<VAR>e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U<VAR>this : IsIso (Scheme.Hom.appLE f (f ''ᵁ ↑V) ↑V ⋯)<GOAL>Q (Scheme.Hom.appLE g (↑U) (f ''ᵁ ↑V) ⋯)
<VAR>α : Type u_1<VAR>s : Cycle α<VAR>x y : α<VAR>hxy : x ≠ y<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>2 ≤ s.length
<VAR>α : Type u_1<VAR>x y : α<VAR>hxy : x ≠ y<VAR>l : List α<VAR>hx : x ∈ Quot.mk Setoid.r l<VAR>hy : y ∈ Quot.mk Setoid.r l<GOAL>2 ≤ length (Quot.mk Setoid.r l)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<GOAL>𝓝ˢ univ = ⊤
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>x : E<GOAL>1 + ‖x‖ ≤ √2 * √(1 + ‖x‖ ^ 2)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>x : E<GOAL>1 + ‖x‖ ≤ √(2 * (1 + ‖x‖ ^ 2))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>x : E<VAR>this : 0 ≤ (‖x‖ - 1) ^ 2<GOAL>1 + ‖x‖ ≤ √(2 * (1 + ‖x‖ ^ 2))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>x : E<VAR>this : 0 ≤ (‖x‖ - 1) ^ 2<GOAL>(1 + ‖x‖) ^ 2 ≤ 2 * (1 + ‖x‖ ^ 2)
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<GOAL>↑(upperClosure (s * t)) = ↑(upperClosure s * upperClosure t)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁶ : NontriviallyNormedField 𝕂<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedRing 𝔹<VAR>inst✝³ : NormedAlgebra 𝕂 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔹<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x y : 𝔸<VAR>hxy : Commute x y<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 y
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁶ : NontriviallyNormedField 𝕂<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedRing 𝔹<VAR>inst✝³ : NormedAlgebra 𝕂 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔹<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x y : 𝔸<VAR>hxy : Commute x y<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>(fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (x + y) = ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁶ : NontriviallyNormedField 𝕂<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedRing 𝔹<VAR>inst✝³ : NormedAlgebra 𝕂 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔹<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x y : 𝔸<VAR>hxy : Commute x y<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>∑' (n : ℕ), (↑n !)⁻¹ • (x + y) ^ n = ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁶ : NontriviallyNormedField 𝕂<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedRing 𝔹<VAR>inst✝³ : NormedAlgebra 𝕂 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔹<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x y : 𝔸<VAR>hxy : Commute x y<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>∑' (x_1 : ℕ), ∑ x_2 ∈ Finset.antidiagonal x_1, (↑x_1 !)⁻¹ • x_1.choose x_2.1 • (x ^ x_2.1 * y ^ x_2.2) = ∑' (n : ℕ), ∑ kl ∈ Finset.antidiagonal n, (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁶ : NontriviallyNormedField 𝕂<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedRing 𝔹<VAR>inst✝³ : NormedAlgebra 𝕂 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔹<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x y : 𝔸<VAR>hxy : Commute x y<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>n : ℕ<VAR>kl : ℕ × ℕ<VAR>hkl : kl ∈ Finset.antidiagonal n<GOAL>(↑n !)⁻¹ • n.choose kl.1 • (x ^ kl.1 * y ^ kl.2) = (↑kl.1!)⁻¹ • x ^ kl.1 * (↑kl.2!)⁻¹ • y ^ kl.2
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁶ : NontriviallyNormedField 𝕂<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedRing 𝔹<VAR>inst✝³ : NormedAlgebra 𝕂 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔹<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x y : 𝔸<VAR>hxy : Commute x y<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>n : ℕ<VAR>kl : ℕ × ℕ<VAR>hkl : kl ∈ Finset.antidiagonal n<GOAL>((↑n !)⁻¹ * (↑n ! / (↑kl.1! * ↑kl.2!))) • (x ^ kl.1 * y ^ kl.2) = ((↑kl.1!)⁻¹ * (↑kl.2!)⁻¹) • (x ^ kl.1 * y ^ kl.2)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁶ : NontriviallyNormedField 𝕂<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedRing 𝔹<VAR>inst✝³ : NormedAlgebra 𝕂 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔹<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x y : 𝔸<VAR>hxy : Commute x y<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>n : ℕ<VAR>kl : ℕ × ℕ<VAR>hkl : kl ∈ Finset.antidiagonal n<GOAL>(↑n !)⁻¹ * (↑n ! / (↑kl.1! * ↑kl.2!)) = (↑kl.1!)⁻¹ * (↑kl.2!)⁻¹
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁶ : NontriviallyNormedField 𝕂<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedRing 𝔹<VAR>inst✝³ : NormedAlgebra 𝕂 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔹<VAR>inst✝¹ : CompleteSpace 𝔸<VAR>inst✝ : CharZero 𝕂<VAR>x y : 𝔸<VAR>hxy : Commute x y<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>hy : y ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>n : ℕ<VAR>kl : ℕ × ℕ<VAR>hkl : kl ∈ Finset.antidiagonal n<VAR>this : ↑n ! ≠ 0<GOAL>(↑n !)⁻¹ * (↑n ! / (↑kl.1! * ↑kl.2!)) = (↑kl.1!)⁻¹ * (↑kl.2!)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteBooleanAlgebra α<VAR>f : Filter β<VAR>u : β → α<VAR>inst✝ : f.NeBot<VAR>a : α<GOAL>liminf u f \ a = liminf (fun b => u b \ a) f
<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>h : ∀ s ∈ S, n ∣ s<VAR>hS : S.Nonempty<GOAL>IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B
<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>h : ∀ s ∈ S, n ∣ s<VAR>hS : S.Nonempty<VAR>H : IsCyclotomicExtension (S ∪ {n}) A B<VAR>s : ℕ+<VAR>hs : s ∈ S<GOAL>∃ r, IsPrimitiveRoot r ↑s
<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>h : ∀ s ∈ S, n ∣ s<VAR>hS : S.Nonempty<VAR>H : IsCyclotomicExtension (S ∪ {n}) A B<GOAL>adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1} = ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p✝ : Perm α<VAR>x✝ : α<VAR>p : Perm α<VAR>x : α<VAR>k : ℕ<GOAL>p.toList ((p ^ k) x) = (p.toList x).rotate k
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p✝ : Perm α<VAR>x✝ : α<VAR>p : Perm α<VAR>x : α<VAR>k : ℕ<GOAL>(p.toList ((p ^ k) x)).length = ((p.toList x).rotate k).length
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p✝ : Perm α<VAR>x✝ : α<VAR>p : Perm α<VAR>x : α<VAR>k : ℕ<GOAL>∀ (n : ℕ) (h₁ : n < (p.toList ((p ^ k) x)).length) (h₂ : n < ((p.toList x).rotate k).length), (p.toList ((p ^ k) x)).nthLe n h₁ = ((p.toList x).rotate k).nthLe n h₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a b c d : G<VAR>h : b = c / a<GOAL>a * b = c
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f✝ : X → Y<VAR>s t : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>f : X → Y<VAR>hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s<GOAL>dimH (range f) ≤ dimH univ
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f✝ : X → Y<VAR>s t : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>f : X → Y<VAR>hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s<GOAL>dimH (f '' univ) ≤ dimH univ
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f✝ : X → Y<VAR>s t : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>f : X → Y<VAR>hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s<VAR>x : X<VAR>x✝ : x ∈ univ<GOAL>∃ C, ∃ t ∈ 𝓝[univ] x, LipschitzOnWith C f t
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q p : R[X]<VAR>x : R<GOAL>0 < rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>hdvd : p ^ n ∣ Nat.card G<GOAL>p ^ n ∣ Nat.card ↥↑P
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>hdvd : p ^ n ∣ (↑P).index * Nat.card ↥↑P<GOAL>p ^ n ∣ Nat.card ↥↑P
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂✝ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>s₂ : Finset ι<VAR>h : s₂ ⊆ s<VAR>w : ι → k<VAR>p : ι → P<GOAL>(affineCombination k (s \ s₂) p) w -ᵥ (affineCombination k s₂ p) (-w) = (s.weightedVSub p) w