ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>p : ℝ≥0∞<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α → F<VAR>c : ℝ≥0∞<GOAL>c ^ (1 / p.toReal) * eLpNorm' f p.toReal μ = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>p : ℝ≥0∞<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α → F<VAR>c : ℝ≥0∞<GOAL>1 / p.toReal = (1 / p).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>p : ℝ≥0∞<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α → F<VAR>c : ℝ≥0∞<GOAL>p.toReal⁻¹ = p⁻¹.toReal
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h : σ.IsThreeCycle<GOAL>Perm.sign σ = 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h : σ.IsThreeCycle<GOAL>(-1) ^ ({3}.sum + card {3}) = 1
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : ¬r = 0<GOAL>o.oangle (x - r • (o.rotation ↑(π / 2)) x) x = ↑(Real.arctan r)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : ¬r = 0<VAR>hx : x = r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))<GOAL>o.oangle (x - r • (o.rotation ↑(π / 2)) x) x = ↑(Real.arctan r)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : ¬r = 0<VAR>hx : x = r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))<GOAL>o.oangle (-(r • (o.rotation ↑(π / 2)) x) + x) x = ↑(Real.arctan r)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : ¬r = 0<VAR>hx : x = r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))<GOAL>o.oangle (-(r • (o.rotation ↑(π / 2)) x) + r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))) (r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))) = ↑(Real.arctan r)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : ¬r = 0<VAR>hx : x = r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))<GOAL>-(r • (o.rotation ↑(π / 2)) x) ≠ 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)<VAR>p : Set ι<VAR>x₁ x₂ x : Π₀ (i : ι), α i<VAR>i : ι<VAR>hr : ∀ (j : ι), r j i → x j = ((fun x => x.2.1.piecewise x.2.2 x.1) (p, x₁, x₂)) j<VAR>hs : s i (x i) (((fun x => x.2.1.piecewise x.2.2 x.1) (p, x₁, x₂)) i)<GOAL>∃ a', InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧ (fun x => x.2.1.piecewise x.2.2 x.1) a' = x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)<VAR>p : Set ι<VAR>x₁ x₂ x : Π₀ (i : ι), α i<VAR>i : ι<VAR>hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j<VAR>hs : s i (x i) (if i ∈ p then x₁ i else x₂ i)<GOAL>∃ a', InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧ (fun x => x.2.1.piecewise x.2.2 x.1) a' = x
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁴ : Quiver U<VAR>inst✝³ : Quiver V<VAR>inst✝² : Quiver W<VAR>V' : Type u_4<VAR>inst✝¹ : Quiver V'<VAR>inst✝ : HasReverse V'<VAR>φ : V ⥤q V'<GOAL>of ⋙q lift φ = φ
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁴ : Quiver U<VAR>inst✝³ : Quiver V<VAR>inst✝² : Quiver W<VAR>V' : Type u_4<VAR>inst✝¹ : Quiver V'<VAR>inst✝ : HasReverse V'<VAR>φ : V ⥤q V'<GOAL>∀ (X : V), (of ⋙q lift φ).obj X = φ.obj X
<VAR>U : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁴ : Quiver U<VAR>inst✝³ : Quiver V<VAR>inst✝² : Quiver W<VAR>V' : Type u_4<VAR>inst✝¹ : Quiver V'<VAR>inst✝ : HasReverse V'<VAR>φ : V ⥤q V'<GOAL>∀ (X Y : V) (f : X ⟶ Y), (of ⋙q lift φ).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : Algebra R Rₘ<VAR>inst✝⁹ : CommRing Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>M : Submonoid R<VAR>inst✝⁷ : IsLocalization M Rₘ<VAR>inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>a : S<GOAL>(trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : Algebra R Rₘ<VAR>inst✝⁹ : CommRing Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>M : Submonoid R<VAR>inst✝⁷ : IsLocalization M Rₘ<VAR>inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>a : S<VAR>h✝ : Subsingleton R<GOAL>(trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : Algebra R Rₘ<VAR>inst✝⁹ : CommRing Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>M : Submonoid R<VAR>inst✝⁷ : IsLocalization M Rₘ<VAR>inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>a : S<VAR>h✝ : Nontrivial R<GOAL>(trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : Algebra R Rₘ<VAR>inst✝⁹ : CommRing Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>M : Submonoid R<VAR>inst✝⁷ : IsLocalization M Rₘ<VAR>inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>a : S<VAR>h✝ : Nontrivial R<VAR>b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S<VAR>this : DecidableEq (Module.Free.ChooseBasisIndex R S) := Classical.decEq (Module.Free.ChooseBasisIndex R S)<GOAL>(trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : Algebra R Rₘ<VAR>inst✝⁹ : CommRing Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>M : Submonoid R<VAR>inst✝⁷ : IsLocalization M Rₘ<VAR>inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : Algebra R Sₘ<VAR>inst✝³ : IsScalarTower R Rₘ Sₘ<VAR>inst✝² : IsScalarTower R S Sₘ<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>a : S<VAR>h✝ : Nontrivial R<VAR>b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S<VAR>this : DecidableEq (Module.Free.ChooseBasisIndex R S) := Classical.decEq (Module.Free.ChooseBasisIndex R S)<GOAL>((algebraMap R Rₘ).mapMatrix ((leftMulMatrix b) a)).trace = (algebraMap R Rₘ) ((leftMulMatrix b) a).trace
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ≥0<GOAL>Integrable (NNReal.toReal ∘ ⇑f) μ
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ≥0<GOAL>HasFiniteIntegral (NNReal.toReal ∘ ⇑f) μ
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ≥0<GOAL>∫⁻ (a : X), ↑(f a) ∂μ < ⊤
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : AddMonoid A<VAR>x y : A<GOAL>y ∈ closure {x} ↔ ∃ n, n • x = y
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : AddMonoid A<VAR>x y : A<GOAL>(∃ x_1, ((multiplesHom A) x) x_1 = y) ↔ ∃ n, n • x = y
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<GOAL>μ.toFiniteMeasure ≠ 0
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<GOAL>1 ≠ 0
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>b : Set ι<VAR>c : ι → Set X<VAR>hs : IsCompact s<VAR>hc₁ : ∀ i ∈ b, IsOpen (c i)<VAR>hc₂ : s ⊆ ⋃ i ∈ b, c i<GOAL>∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>b : Set ι<VAR>c : ι → Set X<VAR>hs : IsCompact s<VAR>hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)<VAR>hc₂ : s ⊆ ⋃ x, c ↑x<GOAL>∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>b : Set ι<VAR>c : ι → Set X<VAR>hs : IsCompact s<VAR>hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)<VAR>hc₂ : s ⊆ ⋃ x, c ↑x<VAR>d : Finset ↑b<VAR>hd : s ⊆ ⋃ i ∈ d, c ↑i<GOAL>∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>b : Set ι<VAR>c : ι → Set X<VAR>hs : IsCompact s<VAR>hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)<VAR>hc₂ : s ⊆ ⋃ x, c ↑x<VAR>d : Finset ↑b<VAR>hd : s ⊆ ⋃ i ∈ d, c ↑i<GOAL>Subtype.val '' ↑d ⊆ b
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>b : Set ι<VAR>c : ι → Set X<VAR>hs : IsCompact s<VAR>hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)<VAR>hc₂ : s ⊆ ⋃ x, c ↑x<VAR>d : Finset ↑b<VAR>hd : s ⊆ ⋃ i ∈ d, c ↑i<GOAL>s ⊆ ⋃ i ∈ Subtype.val '' ↑d, c i
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<GOAL>(s.prod f).totalDegree ≤ ∑ i ∈ s, (f i).totalDegree
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<GOAL>(Multiset.map totalDegree (Multiset.map f s.val)).sum ≤ ∑ i ∈ s, (f i).totalDegree
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<GOAL>(Multiset.map (totalDegree ∘ f) s.val).sum ≤ ∑ i ∈ s, (f i).totalDegree
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroSMulDivisors R M<GOAL>Module.rank R M = 0 ↔ ∀ (x : M), x = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>(a ⊓ b) ∆ (a ∆ b) = a ⊔ b
<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✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<GOAL>‖p.changeOriginSeriesTerm k l s hs‖ = ‖p (k + l)‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra 𝕜 A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : NormOneClass A<VAR>φ : A →ₐ[𝕜] 𝕜<VAR>x✝¹ : ℝ<VAR>x✝ : x✝¹ ≥ 0<VAR>h : ∀ (x : A), ‖φ.toContinuousLinearMap x‖ ≤ x✝¹ * ‖x‖<GOAL>1 ≤ x✝¹
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Finset α<VAR>t✝ t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>s : Set α<VAR>t : Set β<VAR>hu : ↑u ⊆ image2 f s t<GOAL>∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Finset α<VAR>t✝ t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>s : Set α<VAR>t : Set β<VAR>hu : ∃ s', ↑s' ⊆ s ×ˢ t ∧ image (fun x => f x.1 x.2) s' = u<GOAL>∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Finset α<VAR>t✝ t' : Finset β<VAR>u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>s : Set α<VAR>t : Set β<VAR>u : Finset (α × β)<VAR>hu : ↑u ⊆ s ×ˢ t<GOAL>∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ image (fun x => f x.1 x.2) u ⊆ image₂ f s' t'
<VAR>R : Type u<VAR>inst✝² : NonUnitalRing R<VAR>inst✝¹ : PartialOrder R<VAR>inst✝ : StarRing R<VAR>h_add : ∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y<VAR>h_nonneg_iff : ∀ (x : R), 0 ≤ x ↔ x ∈ AddSubmonoid.closure (range fun s => star s * s)<VAR>x y : R<VAR>this : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), y = x + p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hs : s ∈ 𝓝 0<GOAL>Tendsto (gauge s) (𝓝 0) (𝓝[≥] 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hs : s ∈ 𝓝 0<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>ε : ℝ<VAR>hs : ε • s ∈ 𝓝 0<VAR>hε : 0 < ε<GOAL>∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>ε : ℝ<VAR>hs : ε • s ∈ 𝓝 0<VAR>hε : 0 < ε<VAR>x : E<VAR>hx : x ∈ ε • s<GOAL>gauge s x ∈ Icc 0 ε
<VAR>s : String<VAR>n : Nat<GOAL>(s.drop n).data = List.drop n s.data
<VAR>a x✝ z x y : ℂ<VAR>hx₀ : x ≠ 0<VAR>hy₀ : y ≠ 0<GOAL>(x * y).arg = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
<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<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : ChartedSpace H' M'<VAR>x : M<GOAL>↑(extChartAt I x).symm ⁻¹' (s ∩ t) ∩ range ↑I = ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' t
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<VAR>M : T.ModelType<VAR>v : α → ↑M<VAR>xs : Fin n → ↑M<GOAL>(φ ⇔ ∀'liftAt 1 n φ).Realize v xs
<VAR>M₀ : Type u_1<VAR>inst✝ : MonoidWithZero M₀<VAR>r : M₀<GOAL>r ∉ nonZeroDivisorsRight M₀ ↔ {s | r * s = 0 ∧ s ≠ 0}.Nonempty
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<GOAL>A.det = ∑ j : Fin n.succ, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<GOAL>∑ i : Fin n.succ, (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det = ∑ j : Fin n.succ, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>i : Fin n.succ<VAR>x✝ : i ∈ univ<GOAL>(-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det = (-1) ^ ↑i * A 0 i * (A.submatrix Fin.succ i.succAbove).det
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>A : Matrix (Fin n.succ) (Fin n.succ) R<VAR>i : Fin n.succ<VAR>x✝ : i ∈ univ<GOAL>(-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ)ᵀ.det = (-1) ^ ↑i * A 0 i * (A.submatrix Fin.succ i.succAbove).det
<VAR>n : ℕ<GOAL>(bit false n).fastFibAux = let p := n.fastFibAux; (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)
<VAR>n : ℕ<GOAL>(if false = true then ((binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).2 ^ 2 + (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).1 ^ 2, (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).2 * (2 * (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).1 + (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).2)) else ((binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).1 * (2 * (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).2 - (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).1), (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).2 ^ 2 + (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).1 ^ 2)) = let p := binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n; (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u s : Set α<GOAL>sᶜ ∪ s = univ
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M'<GOAL>(iso S f).symm m = LocalizedModule.mk ⋯.choose.1 ⋯.choose.2
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M'<GOAL>(iso S f) ((iso S f).symm m) = (iso S f) (LocalizedModule.mk ⋯.choose.1 ⋯.choose.2)
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M'<GOAL>m = (iso S f) (LocalizedModule.mk ⋯.choose.1 ⋯.choose.2)