ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<VAR>hf' : f.natDegree ≠ 0<VAR>hg' : g.natDegree ≠ 0<VAR>H₁ : f.comp g ≠ 0<VAR>H₂ : ¬IsUnit (f.comp g)<GOAL>Irreducible (f.comp g)
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<VAR>hf' : f.natDegree ≠ 0<VAR>hg' : g.natDegree ≠ 0<VAR>H₁ : f.comp g ≠ 0<VAR>H₂ : ¬IsUnit (f.comp g)<VAR>p : K[X]<VAR>hp₁ : Irreducible p<VAR>hp₂ : p ∣ f.comp g<GOAL>Irreducible (f.comp g)
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<VAR>hf' : f.natDegree ≠ 0<VAR>hg' : g.natDegree ≠ 0<VAR>H₁ : f.comp g ≠ 0<VAR>H₂ : ¬IsUnit (f.comp g)<VAR>p : K[X]<VAR>hp₁ : Irreducible p<VAR>hp₂ : p ∣ f.comp g<GOAL>p.natDegree = f.natDegree * g.natDegree
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<VAR>hf' : f.natDegree ≠ 0<VAR>hg' : g.natDegree ≠ 0<VAR>H₁ : f.comp g ≠ 0<VAR>H₂ : ¬IsUnit (f.comp g)<VAR>p : K[X]<VAR>hp₁ : Irreducible p<VAR>hp₂ : p ∣ f.comp g<VAR>this : Fact (Irreducible p)<VAR>Kx : Type u := AdjoinRoot p<GOAL>p.natDegree = f.natDegree * g.natDegree
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<VAR>hf' : f.natDegree ≠ 0<VAR>hg' : g.natDegree ≠ 0<VAR>H₁ : f.comp g ≠ 0<VAR>H₂ : ¬IsUnit (f.comp g)<VAR>p : K[X]<VAR>hp₁ : Irreducible p<VAR>hp₂ : p ∣ f.comp g<VAR>this✝ : Fact (Irreducible p)<VAR>Kx : Type u := AdjoinRoot p<VAR>this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))<GOAL>p.natDegree = f.natDegree * g.natDegree
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<VAR>hf' : f.natDegree ≠ 0<VAR>hg' : g.natDegree ≠ 0<VAR>H₁ : f.comp g ≠ 0<VAR>H₂ : ¬IsUnit (f.comp g)<VAR>p : K[X]<VAR>hp₁ : Irreducible p<VAR>hp₂ : p ∣ f.comp g<VAR>this✝ : Fact (Irreducible p)<VAR>Kx : Type u := AdjoinRoot p<VAR>this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))<VAR>key₁ : f = minpoly K ((aeval (root p)) g)<GOAL>p.natDegree = f.natDegree * g.natDegree
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<VAR>hf' : f.natDegree ≠ 0<VAR>hg' : g.natDegree ≠ 0<VAR>H₁ : f.comp g ≠ 0<VAR>H₂ : ¬IsUnit (f.comp g)<VAR>p : K[X]<VAR>hp₁ : Irreducible p<VAR>hp₂ : p ∣ f.comp g<VAR>this✝ : Fact (Irreducible p)<VAR>Kx : Type u := AdjoinRoot p<VAR>this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))<VAR>key₁ : f = minpoly K ((aeval (root p)) g)<VAR>key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree<GOAL>p.natDegree = f.natDegree * g.natDegree
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<VAR>hf' : f.natDegree ≠ 0<VAR>hg' : g.natDegree ≠ 0<VAR>H₁ : f.comp g ≠ 0<VAR>H₂ : ¬IsUnit (f.comp g)<VAR>p : K[X]<VAR>hp₁ : Irreducible p<VAR>hp₂ : p ∣ f.comp g<VAR>this✝ : Fact (Irreducible p)<VAR>Kx : Type u := AdjoinRoot p<VAR>this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))<VAR>key₁ : f = minpoly K ((aeval (root p)) g)<VAR>key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree<VAR>key₂ : Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g - C (AdjoinSimple.gen K ((aeval (root p)) g)) = minpoly (↥K⟮(aeval (root p)) g⟯) (root p)<GOAL>p.natDegree = f.natDegree * g.natDegree
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<VAR>hf' : f.natDegree ≠ 0<VAR>hg' : g.natDegree ≠ 0<VAR>H₁ : f.comp g ≠ 0<VAR>H₂ : ¬IsUnit (f.comp g)<VAR>p : K[X]<VAR>hp₁ : Irreducible p<VAR>hp₂ : p ∣ f.comp g<VAR>this✝ : Fact (Irreducible p)<VAR>Kx : Type u := AdjoinRoot p<VAR>this : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))<VAR>key₁ : f = minpoly K ((aeval (root p)) g)<VAR>key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree<VAR>key₂ : Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g - C (AdjoinSimple.gen K ((aeval (root p)) g)) = minpoly (↥K⟮(aeval (root p)) g⟯) (root p)<VAR>key₂' : finrank (↥K⟮(aeval (root p)) g⟯) Kx = g.natDegree<GOAL>p.natDegree = f.natDegree * g.natDegree
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : K[X]<VAR>hfm : f.Monic<VAR>hgm : g.Monic<VAR>hf : Irreducible f<VAR>hg : ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E), minpoly K x = f → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) g - C (AdjoinSimple.gen K x))<VAR>hf' : f.natDegree ≠ 0<VAR>hg' : g.natDegree ≠ 0<VAR>H₁ : f.comp g ≠ 0<VAR>H₂ : ¬IsUnit (f.comp g)<VAR>p : K[X]<VAR>hp₁ : Irreducible p<VAR>hp₂ : p ∣ f.comp g<VAR>this✝¹ : Fact (Irreducible p)<VAR>Kx : Type u := AdjoinRoot p<VAR>this✝ : Module.Finite K (AdjoinRoot p) := PowerBasis.finite (powerBasis (Irreducible.ne_zero hp₁))<VAR>key₁ : f = minpoly K ((aeval (root p)) g)<VAR>key₁' : finrank K ↥K⟮(aeval (root p)) g⟯ = f.natDegree<VAR>key₂ : Polynomial.map (algebraMap K ↥K⟮(aeval (root p)) g⟯) g - C (AdjoinSimple.gen K ((aeval (root p)) g)) = minpoly (↥K⟮(aeval (root p)) g⟯) (root p)<VAR>key₂' : finrank (↥K⟮(aeval (root p)) g⟯) Kx = g.natDegree<VAR>this : finrank K ↥K⟮(aeval (root p)) g⟯ * finrank (↥K⟮(aeval (root p)) g⟯) Kx = finrank K Kx<GOAL>p.natDegree = f.natDegree * g.natDegree
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : I → Type v₁<VAR>g : I → Type v₂<VAR>h : I → Type v₃<VAR>x✝ y : (i : I) → f i<VAR>i✝ : I<VAR>inst✝³ : DecidableEq I<VAR>inst✝² : (i : I) → One (f i)<VAR>inst✝¹ : (i : I) → One (g i)<VAR>inst✝ : (i : I) → One (h i)<VAR>f' : (i : I) → f i → g i<VAR>hf' : ∀ (i : I), f' i 1 = 1<VAR>i : I<VAR>x : f i<VAR>j : I<GOAL>f' j (mulSingle i x j) = mulSingle i (f' i x) j
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>Gc : G.Preconnected<VAR>hK : K.Nonempty<GOAL>∀ (C : G.ComponentCompl K), ∃ ck, ck.1 ∈ C ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>Gc : G.Preconnected<VAR>hK : K.Nonempty<VAR>v : V<VAR>vnK : v ∉ K<GOAL>∃ ck, ck.1 ∈ G.componentComplMk vnK ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>Gc : G.Preconnected<VAR>hK : K.Nonempty<VAR>v : V<VAR>vnK : v ∉ K<VAR>C : G.ComponentCompl K := G.componentComplMk vnK<GOAL>∃ ck, ck.1 ∈ G.componentComplMk vnK ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>Gc : G.Preconnected<VAR>hK : K.Nonempty<VAR>v : V<VAR>vnK : v ∉ K<VAR>C : G.ComponentCompl K := G.componentComplMk vnK<VAR>dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)<GOAL>∃ ck, ck.1 ∈ G.componentComplMk vnK ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>Gc : G.Preconnected<VAR>hK : K.Nonempty<VAR>v : V<VAR>vnK : v ∉ K<VAR>C : G.ComponentCompl K := G.componentComplMk vnK<VAR>dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)<VAR>h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2<GOAL>False
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>Gc : G.Preconnected<VAR>hK : K.Nonempty<VAR>v : V<VAR>vnK : v ∉ K<VAR>C : G.ComponentCompl K := G.componentComplMk vnK<VAR>dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)<VAR>h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2<GOAL>Set.univ = ↑C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>Gc : G.Preconnected<VAR>hK : K.Nonempty<VAR>v : V<VAR>vnK : v ∉ K<VAR>C : G.ComponentCompl K := G.componentComplMk vnK<VAR>dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)<VAR>h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2<GOAL>↑C = Set.univ
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>Gc : G.Preconnected<VAR>hK : K.Nonempty<VAR>v : V<VAR>vnK : v ∉ K<VAR>C : G.ComponentCompl K := G.componentComplMk vnK<VAR>dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)<VAR>h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2<GOAL>∀ (x : V), x ∈ ↑C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>Gc : G.Preconnected<VAR>hK : K.Nonempty<VAR>v : V<VAR>vnK : v ∉ K<VAR>C : G.ComponentCompl K := G.componentComplMk vnK<VAR>dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)<VAR>h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2<VAR>u : V<GOAL>u ∈ ↑C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>Gc : G.Preconnected<VAR>hK : K.Nonempty<VAR>v : V<VAR>vnK : v ∉ K<VAR>C : G.ComponentCompl K := G.componentComplMk vnK<VAR>dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)<VAR>h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2<VAR>u : V<VAR>unC : u ∉ ↑C<GOAL>False
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>Gc : G.Preconnected<VAR>hK : K.Nonempty<VAR>v : V<VAR>vnK : v ∉ K<VAR>C : G.ComponentCompl K := G.componentComplMk vnK<VAR>dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)<VAR>h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2<VAR>u : V<VAR>unC : u ∉ ↑C<VAR>p : G.Walk v u<GOAL>False
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>Gc : G.Preconnected<VAR>hK : K.Nonempty<VAR>v : V<VAR>vnK : v ∉ K<VAR>C : G.ComponentCompl K := G.componentComplMk vnK<VAR>dis : K ∩ ↑C ⊆ ∅ := Set.disjoint_iff.mp (ComponentCompl.disjoint_right C)<VAR>h : ∀ (ck : V × V), ck.1 ∈ G.componentComplMk vnK → ck.2 ∈ K → ¬G.Adj ck.1 ck.2<VAR>u : V<VAR>unC : u ∉ ↑C<VAR>p : G.Walk v u<VAR>x y : V<VAR>xy : G.Adj (x, y).1 (x, y).2<VAR>xC : { toProd := (x, y), adj := xy }.toProd.1 ∈ ↑C<VAR>ynC : { toProd := (x, y), adj := xy }.toProd.2 ∉ ↑C<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>n : ℕ<VAR>s₁ s₂ : Stream' α<GOAL>(s₁ ⋈ s₂).get (2 * n).succ.succ = s₁.get n.succ
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>n : ℕ<VAR>s₁ s₂ : Stream' α<GOAL>(s₁.tail ⋈ s₂.tail).get (2 * n) = s₁.get n.succ
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y + o.oangle y x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>s t : Set E<VAR>x✝ : E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>h : DiffContOnCl 𝕜 f (ball x r)<GOAL>ContinuousOn f (closedBall x r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>s t : Set E<VAR>x✝ : E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>h : DiffContOnCl 𝕜 f (ball x 0)<GOAL>ContinuousOn f (closedBall x 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>s t : Set E<VAR>x✝ : E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>h : DiffContOnCl 𝕜 f (ball x r)<VAR>hr : r ≠ 0<GOAL>ContinuousOn f (closedBall x r)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R : Sieve X<VAR>J : GrothendieckTopology C<VAR>S : Sieve X<GOAL>S ∈ J.sieves X ↔ J.Covers S (𝟙 X)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.coeff n ≠ 0<GOAL>↑n ≤ p.degree
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommMonoid M<VAR>ψ : AddChar R M<VAR>x✝ : R<GOAL>(ψ.mulShift 1) x✝ = ψ x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : LinearOrderedField R<VAR>inst✝¹ : OrderTopology R<VAR>inst✝ : FloorRing R<GOAL>Tendsto (fun x => ↑⌊x⌋₊ / x) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝² : ConditionallyCompleteLattice α<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>l u : α → β → γ<VAR>l₁ u₁ : β → γ → α<VAR>l₂ u₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddAbove s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddAbove t<GOAL>sSup (image2 l s t) = l (sSup s) (sSup t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝² : ConditionallyCompleteLattice α<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>l u : α → β → γ<VAR>l₁ u₁ : β → γ → α<VAR>l₂ u₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddAbove s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddAbove t<VAR>c : γ<GOAL>sSup (image2 l s t) ≤ c ↔ l (sSup s) (sSup t) ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝² : ConditionallyCompleteLattice α<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>l u : α → β → γ<VAR>l₁ u₁ : β → γ → α<VAR>l₂ u₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddAbove s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddAbove t<VAR>c : γ<GOAL>(∀ i₂ ∈ t, ∀ i₁ ∈ s, l i₁ i₂ ≤ c) ↔ ∀ b ∈ t, b ≤ u₂ (sSup s) c
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>X : Set R<VAR>x✝ : R<VAR>a✝ : ↑X<GOAL>((↑↑{ toFun := fun p => p.toContinuousMapOn X, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }).toFun ((algebraMap R R[X]) x✝)) a✝ = ((algebraMap R C(↑X, R)) x✝) a✝
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>P : R → R → Prop<VAR>a b : R<VAR>H0 : ∀ (x : R), P 0 x<VAR>H1 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b<VAR>a0 : a = 0<GOAL>P a b
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = 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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₃ p₁ p₂).sign = 1<GOAL>dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = dist p₁ p₃
<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>h : ∏ x ∈ s, f x ≠ 1<GOAL>∃ a ∈ s, f a ≠ 1
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝ : StrongRankCondition R<GOAL>Module.rank R R = 1
<VAR>x y✝ z✝ : ZFSet<VAR>h : x.IsTransitive<VAR>y : ZFSet<VAR>hy : y ∈ x.powerset<VAR>z : ZFSet<VAR>hz : z ∈ y<GOAL>z ∈ x.powerset
<VAR>x y✝ z✝ : ZFSet<VAR>h : x.IsTransitive<VAR>y : ZFSet<VAR>hy : y ⊆ x<VAR>z : ZFSet<VAR>hz : z ∈ y<GOAL>z ⊆ x
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : AddCommGroup S<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>inst✝¹ : Module R Q<VAR>inst✝ : Module R S<VAR>f g : N →ₗ[R] P<GOAL>rTensor M (f - g) = rTensor M f - rTensor M g
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : AddCommGroup S<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>inst✝¹ : Module R Q<VAR>inst✝ : Module R S<VAR>f g : N →ₗ[R] P<GOAL>(rTensorHom M) (f - g) = (rTensorHom M) f - (rTensorHom M) g
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>hf : S.f = 0<GOAL>IsIso h.π
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K<VAR>hφ : Cofork.π (CokernelCofork.ofπ h.π ⋯) ≫ φ = 𝟙 h.K<GOAL>IsIso h.π
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>φ : (CokernelCofork.ofπ h.π ⋯).pt ⟶ h.K<VAR>hφ : h.π ≫ φ = 𝟙 h.K<GOAL>IsIso h.π
<VAR>n k : ℕ<GOAL>(hermite (n + 1)).coeff (k + 1) = (hermite n).coeff k - (↑k + 2) * (hermite n).coeff (k + 2)
<VAR>n k : ℕ<GOAL>(hermite n).coeff k - (↑(k + 1) + 1) * (hermite n).coeff (k + 1 + 1) = (hermite n).coeff k - (↑k + 2) * (hermite n).coeff (k + 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>b0 : b = 0<GOAL>b * (a / b) ≤ a
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c : ℝ<VAR>hf : Integrable I l (c • f) vol<VAR>hc : c ≠ 0<GOAL>Integrable I l f vol
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m✝ n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q✝ r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>p q : R[X]<VAR>h : map f p = map f q<VAR>m : ℕ<GOAL>f (p.coeff m) = f (q.coeff m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>m n : ℤ<GOAL>a ^ (m * n) = (a ^ n) ^ m
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<GOAL>coborder s = univ ↔ IsClosed s
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : MetricSpace β<VAR>inst✝ : CompleteSpace β<VAR>f : α → β<VAR>K : ℝ≥0<VAR>h : LipschitzWith K f<VAR>x y : Completion α<GOAL>∀ (a b : α), dist (Completion.extension f (↑α a)) (Completion.extension f (↑α b)) ≤ ↑K * dist (↑α a) (↑α b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : _root_.RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>ι'' : Type u_6<VAR>E' : Type u_7<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : InnerProductSpace 𝕜 E'<VAR>E'' : Type u_8<VAR>inst✝¹ : NormedAddCommGroup E''<VAR>inst✝ : InnerProductSpace 𝕜 E''<VAR>v : ι → E<VAR>f : E →ₗᵢ[𝕜] E'<GOAL>Orthonormal 𝕜 (⇑f ∘ v) ↔ Orthonormal 𝕜 v
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝² : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Finset ι<VAR>t : Finset β<VAR>f : ι → Finset α<VAR>a✝ : α × β<GOAL>a✝ ∈ interedges r (s.biUnion f) t ↔ a✝ ∈ s.biUnion fun a => interedges r (f a) t
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>i j : A<GOAL>(shiftFunctorAdd' C i j (i + j) ⋯).hom = (shiftFunctorAdd C i j).hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>x : ℝ<GOAL>Summable fun n => x ^ n / ↑n !
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>x : ℝ<VAR>A : 0 < ↑⌊‖x‖⌋₊ + 1<GOAL>Summable fun n => x ^ n / ↑n !
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>x : ℝ<VAR>A : 0 < ↑⌊‖x‖⌋₊ + 1<VAR>B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1<GOAL>Summable fun n => x ^ n / ↑n !
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>x : ℝ<VAR>A : 0 < ↑⌊‖x‖⌋₊ + 1<VAR>B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1<GOAL>∀ n ≥ ⌊‖x‖⌋₊, ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖