ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>f : C(↑I, ℝ)<VAR>n : ℕ<GOAL>bernsteinApproximation n f ∈ ↑(polynomialFunctions I).toSubsemiring
<VAR>f : C(↑I, ℝ)<VAR>n : ℕ<GOAL>bernsteinApproximation n f ∈ (polynomialFunctions I).toSubsemiring
<VAR>f : C(↑I, ℝ)<VAR>n : ℕ<GOAL>∀ x ∈ Finset.univ, f (bernstein.z x) • bernstein n ↑x ∈ polynomialFunctions I
<VAR>f : C(↑I, ℝ)<VAR>n✝ : ℕ<VAR>n : Fin (n✝ + 1)<GOAL>f (bernstein.z n) • bernstein n✝ ↑n ∈ polynomialFunctions I
<VAR>f : C(↑I, ℝ)<VAR>n✝ : ℕ<VAR>n : Fin (n✝ + 1)<GOAL>bernstein n✝ ↑n ∈ polynomialFunctions I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s : Set α<GOAL>𝓝[s] a ≤ 𝓝 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s : Set α<GOAL>𝓝[s] a ≤ 𝓝[univ] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s : Set α<GOAL>univ ∈ 𝓝[s] a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>x : HahnSeries Γ R<VAR>hx : 0 < x.orderTop<GOAL>(1 - x) * (powers x hx).hsum = 1
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : LinearOrderedCancelAddCommMonoid Γ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>x : HahnSeries Γ R<VAR>hx : 0 < x.orderTop<GOAL>(powers x hx).hsum - (powers x hx - ofFinsupp (Finsupp.single 0 1)).hsum = 1
<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>(∡ p₃ p₁ p₂).tan = 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>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>(∡ p₃ p₁ p₂).tan = dist p₃ p₂ / dist p₁ p₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>p : α → Prop<VAR>f : α →₀ M<GOAL>subtypeDomain p f = 0 ↔ ∀ (x : α), p x → f x = 0
<VAR>ι : Type u_1<VAR>I J✝ J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>h✝ : π.IsPartition<VAR>hx✝ : x ∈ I<VAR>J : Box ι<VAR>h : J ∈ π<VAR>hx : x ∈ J<GOAL>∃! J, J ∈ π ∧ x ∈ J
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → β<VAR>g : β → α<VAR>h : LeftInverse f g<GOAL>map f (map g []) = []
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → β<VAR>g : β → α<VAR>h : LeftInverse f g<VAR>x : β<VAR>xs : List β<GOAL>map f (map g (x :: xs)) = x :: xs
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x✝³ x✝² : α<VAR>x✝¹ : ℤ<VAR>x✝ : ℕ<VAR>h : IsRat (x✝³ * x✝²⁻¹) x✝¹ x✝<GOAL>IsRat (x✝³ / x✝²) x✝¹ x✝
<VAR>n : ℕ<VAR>Hn : n ≠ 0<GOAL>0 < ∑ i ∈ Finset.range n, (↑(i + 1))⁻¹
<VAR>n : ℕ<VAR>Hn : (Finset.range n).Nonempty<GOAL>0 < ∑ i ∈ Finset.range n, (↑(i + 1))⁻¹
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A✝ A B : ValuationSubring K<VAR>h : A.nonunits = B.nonunits<GOAL>A = B
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p : R[X]<VAR>x✝ : S<VAR>x : ℕ<GOAL>x ∈ (normalizeScaleRoots p).support → x ∈ p.support
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p : R[X]<VAR>x✝ : S<VAR>x : ℕ<GOAL>x ∉ p.support → x ∉ (normalizeScaleRoots p).support
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p : R[X]<VAR>x✝ : S<VAR>x : ℕ<GOAL>p.coeff x = 0 → ¬p.coeff x = 0 → (if x = p.natDegree then 1 else p.coeff x * p.leadingCoeff ^ (p.natDegree - 1 - x)) = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hc : c < 0<VAR>h : b < a<GOAL>a / c < b / c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hc : c < 0<VAR>h : b < a<GOAL>a * (1 / c) < b * (1 / c)
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>f : J → C<VAR>inst✝ : HasBiproduct f<VAR>b : Bicone f<VAR>hb : b.IsBilimit<GOAL>lift b.π ≫ desc b.ι = 𝟙 b.pt
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>f : J → C<VAR>inst✝ : HasBiproduct f<VAR>b : Bicone f<VAR>hb : b.IsBilimit<GOAL>desc b.ι ≫ lift b.π = 𝟙 (⨁ f)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m✝ n : ℕ<VAR>a : M<VAR>m : ℕ<GOAL>a ^ (m * 0) = (a ^ m) ^ 0
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m✝ n✝ : ℕ<VAR>a : M<VAR>m n : ℕ<GOAL>a ^ (m * (n + 1)) = (a ^ m) ^ (n + 1)
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>n : ℕ<VAR>x : ↑I<VAR>k : Fin (n + 1)<VAR>m : k ∈ S f ε h n x<GOAL>|f k/ₙ - f x| < ε / 2
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>n : ℕ<VAR>x : ↑I<VAR>k : Fin (n + 1)<VAR>m : k ∈ S f ε h n x<GOAL>dist k/ₙ x < f.modulus (ε / 2) ⋯
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>H : Type u_4<VAR>inst✝⁵ : TopologicalSpace H<VAR>G : Type u_5<VAR>inst✝⁴ : TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>N : Type u_7<VAR>inst✝¹ : TopologicalSpace N<VAR>inst✝ : ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>s : Set M<GOAL>IsLocalDiffeomorphOn I J n f s ↔ ∀ (x : ↑s), IsLocalDiffeomorphAt I J n f ↑x
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>G : C ⥤ D<VAR>inst✝¹ : HasBinaryProducts C<VAR>inst✝ : HasPullbacks C<VAR>F : WalkingParallelPair ⥤ C<GOAL>pullbackFst F = pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left)) (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → LinearOrder (α i)<VAR>x y x' y' a : (i : ι) → α i<VAR>ha' : a ∉ univ.pi fun i => Ioo (x' i) (y' i)<VAR>hxa : x ≤ a<VAR>hay : a ≤ y<GOAL>a ∈ (⋃ i, Icc x (update y i (x' i))) ∪ ⋃ i, Icc (update x i (y' i)) y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → LinearOrder (α i)<VAR>x y x' y' a : (i : ι) → α i<VAR>hxa : x ≤ a<VAR>hay : a ≤ y<VAR>ha' : ∃ x, ¬(x' x < a x ∧ a x < y' x)<GOAL>a ∈ (⋃ i, Icc x (update y i (x' i))) ∪ ⋃ i, Icc (update x i (y' i)) y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → LinearOrder (α i)<VAR>x y x' y' a : (i : ι) → α i<VAR>hxa : x ≤ a<VAR>hay : a ≤ y<VAR>ha' : ∃ x, ¬(x' x < a x ∧ a x < y' x)<GOAL>∃ x, (True ∧ a x ≤ x' x ∧ ∀ (j : ι), j ≠ x → True) ∨ (y' x ≤ a x ∧ ∀ (j : ι), j ≠ x → True) ∧ True
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → LinearOrder (α i)<VAR>x y x' y' a : (i : ι) → α i<VAR>hxa : x ≤ a<VAR>hay : a ≤ y<VAR>w : ι<VAR>hw : ¬(x' w < a w ∧ a w < y' w)<GOAL>(True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y : NumDenSameDeg 𝒜 x<VAR>n : ℕ<GOAL>(Quotient.mk'' y ^ n).val = val (Quotient.mk'' y) ^ n
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y : NumDenSameDeg 𝒜 x<VAR>n : ℕ<GOAL>Localization.mk ↑(y ^ n).num ⟨↑(y ^ n).den, ⋯⟩ = Localization.mk (↑y.num ^ n) (⟨↑y.den, ⋯⟩ ^ n)
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i✝ j : ι<VAR>l : List ι<VAR>f : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>hnd : l.Nodup<VAR>h : ∀ (i : ι), i ∈ l<VAR>v : TProd α l<VAR>i : ι<VAR>hi : i ∈ l<GOAL>(TProd.mk l (TProd.elim' h v)).elim hi = v.elim hi
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>l✝ : List α<VAR>inst✝ : Fintype α<VAR>l l' : List α<VAR>x : α<VAR>hx : x ∈ (zipWith swap l l').prod.support<VAR>hx' : x ∈ {x | (zipWith swap l l').prod x ≠ x}<GOAL>x ∈ l.toFinset ⊔ l'.toFinset
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>A✝ B✝ : C<VAR>f✝ g✝ : A✝ ⟶ B✝<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝ : HasCoreflexiveEqualizers C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>r : B ⟶ A<VAR>fr : f ≫ r = 𝟙 A<VAR>gr : g ≫ r = 𝟙 A<GOAL>HasEqualizer f g
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>A✝ B✝ : C<VAR>f✝ g✝ : A✝ ⟶ B✝<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝ : HasCoreflexiveEqualizers C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>r : B ⟶ A<VAR>fr : f ≫ r = 𝟙 A<VAR>gr : g ≫ r = 𝟙 A<VAR>this : IsCoreflexivePair f g := IsCoreflexivePair.mk' r fr gr<GOAL>HasEqualizer f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>h's : BddBelow s<GOAL>↑(sInf s) = ⨅ a ∈ s, ↑a
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>i : ι<VAR>x : β i<VAR>h : ¬p i<GOAL>filter p (single i x) = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>g : Γ<VAR>hg : x.orderTop = ↑g<GOAL>x.coeff g ≠ 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>g : Γ<VAR>hg : x.orderTop = ↑g<VAR>h : x.orderTop ≠ ⊤<GOAL>x.coeff g ≠ 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>g : Γ<VAR>hg : x.orderTop = ↑g<VAR>h : x.orderTop ≠ ⊤<VAR>hx : x ≠ 0<GOAL>x.coeff g ≠ 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>g : Γ<VAR>h : x.orderTop ≠ ⊤<VAR>hx : x ≠ 0<VAR>hg : ⋯.min ⋯ = g<GOAL>x.coeff g ≠ 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : Zero R<VAR>a b : Γ<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>g : Γ<VAR>h : x.orderTop ≠ ⊤<VAR>hx : x ≠ 0<VAR>hg : ⋯.min ⋯ = g<GOAL>x.coeff (⋯.min ⋯) ≠ 0
<VAR>s : ℂ<GOAL>completedCosZeta 0 s = completedRiemannZeta s
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝² : PseudoEMetricSpace F<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>K✝ : Set E<VAR>comp✝ : IsCompact K✝<VAR>f✝ : E → F<VAR>D : Set E<VAR>ε✝ : ℝ≥0∞<VAR>inst✝ : PseudoEMetricSpace E<VAR>K : Set E<VAR>comp : IsCompact K<VAR>f : E → F<VAR>ε : ℝ≥0∞<VAR>hK : ∀ x ∈ K, oscillation f x < ε<GOAL>∃ δ > 0, ∀ x ∈ K, diam (f '' ball x (ENNReal.ofReal δ)) ≤ ε
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝² : PseudoEMetricSpace F<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>K✝ : Set E<VAR>comp✝ : IsCompact K✝<VAR>f✝ : E → F<VAR>D : Set E<VAR>ε✝ : ℝ≥0∞<VAR>inst✝ : PseudoEMetricSpace E<VAR>K : Set E<VAR>comp : IsCompact K<VAR>f : E → F<VAR>ε : ℝ≥0∞<VAR>hK : ∀ x ∈ K, oscillationWithin f univ x < ε<GOAL>∃ δ > 0, ∀ x ∈ K, diam (f '' ball x (ENNReal.ofReal δ)) ≤ ε
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝² : PseudoEMetricSpace F<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>K✝ : Set E<VAR>comp✝ : IsCompact K✝<VAR>f✝ : E → F<VAR>D : Set E<VAR>ε✝ : ℝ≥0∞<VAR>inst✝ : PseudoEMetricSpace E<VAR>K : Set E<VAR>comp : IsCompact K<VAR>f : E → F<VAR>ε : ℝ≥0∞<VAR>hK : ∀ x ∈ K, oscillationWithin f univ x < ε<VAR>x✝ : ℝ<VAR>a✝¹ : E<VAR>a✝ : a✝¹ ∈ K<GOAL>ball a✝¹ (ENNReal.ofReal x✝) ∩ univ = ball a✝¹ (ENNReal.ofReal x✝)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>DifferentiableWithinAt 𝕜 f t y ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => f x i) t y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>(∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => (⇑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) t y) ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => f x i) t y
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'<GOAL>Valid' o₁ (l.balanceL x r) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'<GOAL>Valid' o₁ (l.balance' x r) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'<GOAL>∃ l' r', BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f : Y ⟶ X<VAR>S R✝ : Sieve X<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>G : D ⥤ E<VAR>R : Sieve X<VAR>Y✝ : C<VAR>f✝ : Y✝ ⟶ X<GOAL>(functorPullback (𝟭 C) R).arrows f✝ ↔ R.arrows f✝
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : DecidableEq R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>hp : NeZero p<VAR>inst✝ : CharZero R<VAR>n : ℕ<GOAL>(W_ R n).vars = range (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : DecidableEq R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>hp : NeZero p<VAR>inst✝ : CharZero R<VAR>n : ℕ<VAR>this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}<GOAL>(W_ R n).vars = range (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : DecidableEq R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>hp : NeZero p<VAR>inst✝ : CharZero R<VAR>n : ℕ<VAR>this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}<GOAL>((range (n + 1)).biUnion fun i => ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars) = range (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : DecidableEq R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>hp : NeZero p<VAR>inst✝ : CharZero R<VAR>n : ℕ<VAR>this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}<GOAL>Pairwise (Disjoint on fun i => ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars)
<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>i : ι<VAR>a : α<VAR>f✝ g : ι → α<VAR>inst✝¹ : CommSemiring α<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>f : ι → α<VAR>n : ℕ<GOAL>(∑ a ∈ s, f a) ^ n = ∑ p ∈ piFinset fun _i => s, ∏ i : Fin n, f (p i)
<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>i : ι<VAR>a : α<VAR>f✝ g : ι → α<VAR>inst✝¹ : CommSemiring α<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>f : ι → α<VAR>n : ℕ<GOAL>(∑ a ∈ s, f a) ^ n = ∏ i : Fin n, ∑ j ∈ s, f j
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ f : ℂ → E<VAR>z : ℂ<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<GOAL>‖f z‖ ≤ ‖interpStrip f z‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ f : ℂ → E<VAR>z : ℂ<VAR>hz : z ∈ verticalClosedStrip 0 1<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<GOAL>z ∈ closure (verticalStrip 0 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<GOAL>(TransGen fun x x_1 => x ⩿ x_1) = ReflTransGen fun x x_1 => x ⋖ x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<GOAL>range (t.restrictPreimage f) = Subtype.val ⁻¹' range f
<VAR>m✝ n a✝ b✝ c✝ d a b c m : ℕ<VAR>hc : c ≠ 0<GOAL>c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m]
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>FermatLastTheoremForThreeGen.Solution.x S * FermatLastTheoremForThreeGen.Solution.y S * FermatLastTheoremForThreeGen.Solution.z S = ↑S.u * FermatLastTheoremForThreeGen.Solution.w S ^ 3
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>λ ^ (3 * S.multiplicity - 2) * FermatLastTheoremForThreeGen.Solution.x S * λ * FermatLastTheoremForThreeGen.Solution.y S * λ * FermatLastTheoremForThreeGen.Solution.z S = ↑S.u * λ ^ (3 * S.multiplicity) * FermatLastTheoremForThreeGen.Solution.w S ^ 3
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>(S.a + S.b) * ((S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)) = ↑S.u * (λ ^ (3 * S.multiplicity) * FermatLastTheoremForThreeGen.Solution.w S ^ 3)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>(S.a + S.b) * ((S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)) = (S.a + S.b) * (S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>s : Set V<VAR>t : Set P<VAR>hs : IsClosed s<VAR>ht : IsCompact t<GOAL>IsClosed (s +ᵥ t)
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>s : Set V<VAR>t : Set P<VAR>hs : IsClosed s<VAR>ht : IsCompact t<VAR>u : ℕ → P<VAR>p : P<VAR>husv : ∀ (n : ℕ), u n ∈ s +ᵥ t<VAR>hup : Tendsto u atTop (𝓝 p)<GOAL>p ∈ s +ᵥ t
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>s : Set V<VAR>t : Set P<VAR>hs : IsClosed s<VAR>ht : IsCompact t<VAR>u : ℕ → P<VAR>p : P<VAR>hup : Tendsto u atTop (𝓝 p)<VAR>a : ℕ → V<VAR>ha : ∀ (n : ℕ), a n ∈ s<VAR>v : ℕ → P<VAR>hv : ∀ (n : ℕ), v n ∈ t<VAR>hav : ∀ (n : ℕ), (fun x x_1 => x +ᵥ x_1) (a n) (v n) = u n<GOAL>p ∈ s +ᵥ t
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>s : Set V<VAR>t : Set P<VAR>hs : IsClosed s<VAR>ht : IsCompact t<VAR>u : ℕ → P<VAR>p : P<VAR>hup : Tendsto u atTop (𝓝 p)<VAR>a : ℕ → V<VAR>ha : ∀ (n : ℕ), a n ∈ s<VAR>v : ℕ → P<VAR>hv : ∀ (n : ℕ), v n ∈ t<VAR>hav : ∀ (n : ℕ), (fun x x_1 => x +ᵥ x_1) (a n) (v n) = u n<VAR>q : P<VAR>hqt : q ∈ t<VAR>φ : ℕ → ℕ<VAR>φ_mono : StrictMono φ<VAR>hφq : Tendsto (v ∘ φ) atTop (𝓝 q)<GOAL>p ∈ s +ᵥ t
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>s : Set V<VAR>t : Set P<VAR>hs : IsClosed s<VAR>ht : IsCompact t<VAR>u : ℕ → P<VAR>p : P<VAR>hup : Tendsto u atTop (𝓝 p)<VAR>a : ℕ → V<VAR>ha : ∀ (n : ℕ), a n ∈ s<VAR>v : ℕ → P<VAR>hv : ∀ (n : ℕ), v n ∈ t<VAR>hav : ∀ (n : ℕ), (fun x x_1 => x +ᵥ x_1) (a n) (v n) = u n<VAR>q : P<VAR>hqt : q ∈ t<VAR>φ : ℕ → ℕ<VAR>φ_mono : StrictMono φ<VAR>hφq : Tendsto (v ∘ φ) atTop (𝓝 q)<VAR>n : ℕ<GOAL>(u ∘ φ -ᵥ v ∘ φ) n ∈ s
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>s : Set V<VAR>t : Set P<VAR>hs : IsClosed s<VAR>ht : IsCompact t<VAR>u : ℕ → P<VAR>p : P<VAR>hup : Tendsto u atTop (𝓝 p)<VAR>a : ℕ → V<VAR>ha : ∀ (n : ℕ), a n ∈ s<VAR>v : ℕ → P<VAR>hv : ∀ (n : ℕ), v n ∈ t<VAR>hav : ∀ (n : ℕ), (fun x x_1 => x +ᵥ x_1) (a n) (v n) = u n<VAR>q : P<VAR>hqt : q ∈ t<VAR>φ : ℕ → ℕ<VAR>φ_mono : StrictMono φ<VAR>hφq : Tendsto (v ∘ φ) atTop (𝓝 q)<VAR>n : ℕ<GOAL>(u ∘ φ -ᵥ v ∘ φ) n = a (φ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>h : a * b⁻¹ = c<GOAL>a = c * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>h : a = c * b<GOAL>a * b⁻¹ = c
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>n : ℕ<VAR>x y : R<GOAL>(x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>ε : 𝕜<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : DecidableEq γ<VAR>inst✝ : ExplicitDisjoint t<VAR>x✝ : Finset (α ⊕ β ⊕ γ)<GOAL>x✝ ∈ ↑(map toTriangle t) → ∀ ⦃y : Finset (α ⊕ β ⊕ γ)⦄, y ∈ ↑(map toTriangle t) → x✝ ≠ y → (fun x y => (↑x ∩ ↑y).Subsingleton) x✝ y