ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : PosMulMono α<VAR>ha : 0 ≤ a<VAR>n : ℕ<GOAL>0 ≤ a ^ (-↑(n + 1))
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : PosMulMono α<VAR>ha : 0 ≤ a<VAR>n : ℕ<GOAL>0 ≤ a ^ (n + 1)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : AddCommMonoid M<VAR>s : Finset α<VAR>f : α → β →₀ M<GOAL>(s.sum f).support ⊆ s.biUnion fun x => (f x).support
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : AddCommMonoid M<VAR>s : Finset α<VAR>f : α → β →₀ M<GOAL>(s.sum f).support ⊆ s.sup fun x => (f x).support
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : AddCommMonoid M<VAR>f : α → β →₀ M<GOAL>(∅.sum f).support ⊆ ∅.sup fun x => (f x).support
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s✝ : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : AddCommMonoid M<VAR>f : α → β →₀ M<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>ih : (s.sum f).support ⊆ s.sup fun x => (f x).support<GOAL>((Finset.cons a s ha).sum f).support ⊆ (Finset.cons a s ha).sup fun x => (f x).support
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Semigroup M<VAR>a b : M<VAR>h : ⊤ ≤ S.centralizer<VAR>x✝¹ : M<VAR>hx : x✝¹ ∈ S<VAR>x✝ : M<GOAL>x✝ * x✝¹ = x✝¹ * x✝
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : ℕ<GOAL>c.sizeUpTo i ≤ n
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : ℕ<GOAL>c.sizeUpTo i ≤ (take i c.blocks).sum + (drop i c.blocks).sum
<VAR>ι : Sort u_1<VAR>f✝ : ι → ℕ<VAR>s✝ : Set ℕ<VAR>f : ι → ℕ∞<VAR>s : Set ℕ∞<GOAL>sInf s = 0 ↔ 0 ∈ s
<VAR>ι : Sort u_1<VAR>f✝ : ι → ℕ<VAR>s✝ : Set ℕ<VAR>f : ι → ℕ∞<VAR>s : Set ℕ∞<GOAL>sInf s < 1 ↔ 0 ∈ s
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>a : σ → K<VAR>a✝ : Nontrivial K<GOAL>(eval a) (indicator a) = 1
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>a : σ → K<VAR>a✝ : Nontrivial K<VAR>this : 0 < Fintype.card K - 1<GOAL>(eval a) (indicator a) = 1
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>N : ι → Type u_3<VAR>inst✝ : (i : ι) → Monoid (N i)<VAR>ϕ : (i : ι) → N i →* M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>f g : (i : ι) → N i<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>mrange (noncommPiCoprod ϕ hcomm) = ⨆ i, mrange (ϕ i)
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>N : ι → Type u_3<VAR>inst✝ : (i : ι) → Monoid (N i)<VAR>ϕ : (i : ι) → N i →* M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>f g : (i : ι) → N i<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>mrange (noncommPiCoprod ϕ hcomm) ≤ ⨆ i, mrange (ϕ i)
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>N : ι → Type u_3<VAR>inst✝ : (i : ι) → Monoid (N i)<VAR>ϕ : (i : ι) → N i →* M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>f g : (i : ι) → N i<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>⨆ i, mrange (ϕ i) ≤ mrange (noncommPiCoprod ϕ hcomm)
<VAR>A B A' B' : CommRingCat<VAR>f : A ⟶ B<VAR>f' : A' ⟶ B'<VAR>g : A ⟶ A'<VAR>g' : B ⟶ B'<VAR>fac : g ≫ f' = f ≫ g'<VAR>b : ↑B<VAR>this✝³ : Algebra ↑A ↑B := RingHom.toAlgebra f<VAR>this✝² : Algebra ↑A' ↑B' := RingHom.toAlgebra f'<VAR>this✝¹ : Algebra ↑A ↑A' := RingHom.toAlgebra g<VAR>this✝ : Algebra ↑B ↑B' := RingHom.toAlgebra g'<VAR>this : Algebra ↑A ↑B' := (RingHom.comp f' g).toAlgebra<GOAL>(map fac) (d b) = d (g' b)
<VAR>A B A' B' : CommRingCat<VAR>f : A ⟶ B<VAR>f' : A' ⟶ B'<VAR>g : A ⟶ A'<VAR>g' : B ⟶ B'<VAR>fac : g ≫ f' = f ≫ g'<VAR>b : ↑B<VAR>this✝⁴ : Algebra ↑A ↑B := RingHom.toAlgebra f<VAR>this✝³ : Algebra ↑A' ↑B' := RingHom.toAlgebra f'<VAR>this✝² : Algebra ↑A ↑A' := RingHom.toAlgebra g<VAR>this✝¹ : Algebra ↑B ↑B' := RingHom.toAlgebra g'<VAR>this✝ : Algebra ↑A ↑B' := (RingHom.comp f' g).toAlgebra<VAR>this : IsScalarTower ↑A ↑A' ↑B'<GOAL>(map fac) (d b) = d (g' b)
<VAR>A B A' B' : CommRingCat<VAR>f : A ⟶ B<VAR>f' : A' ⟶ B'<VAR>g : A ⟶ A'<VAR>g' : B ⟶ B'<VAR>fac : g ≫ f' = f ≫ g'<VAR>b : ↑B<VAR>this✝⁵ : Algebra ↑A ↑B := RingHom.toAlgebra f<VAR>this✝⁴ : Algebra ↑A' ↑B' := RingHom.toAlgebra f'<VAR>this✝³ : Algebra ↑A ↑A' := RingHom.toAlgebra g<VAR>this✝² : Algebra ↑B ↑B' := RingHom.toAlgebra g'<VAR>this✝¹ : Algebra ↑A ↑B' := (RingHom.comp f' g).toAlgebra<VAR>this✝ : IsScalarTower ↑A ↑A' ↑B'<VAR>this : IsScalarTower ↑A ↑B ↑B'<GOAL>(map fac) (d b) = d (g' b)
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n<GOAL>eval 1 (cyclotomic n R) = 1
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ 0<GOAL>eval 1 (cyclotomic 0 R) = 1
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n<VAR>hn' : n > 0<GOAL>eval 1 (cyclotomic n R) = 1
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n<VAR>hn' : n > 0<VAR>hn : 1 < n<GOAL>eval 1 (cyclotomic n R) = 1
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n<VAR>hn' : n > 0<VAR>hn : 1 < n<GOAL>eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n<VAR>hn' : n > 0<VAR>hn : 1 < n<GOAL>∀ (p : ℕ), Nat.Prime p → ¬p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n<VAR>hn' : n > 0<VAR>hn : 1 < n<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs<VAR>this : Fact (Nat.Prime p)<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n<VAR>hn' : n > 0<VAR>hn : 1 < n<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs<VAR>this✝ : Fact (Nat.Prime p)<VAR>this : ∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ = ∑ i ∈ range n, X ^ i<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n<VAR>hn' : n > 0<VAR>hn : 1 < n<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs<VAR>this✝ : Fact (Nat.Prime p)<VAR>this : eval 1 (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) = eval 1 (∑ i ∈ range n, X ^ i)<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n<VAR>hn' : n > 0<VAR>hn : 1 < n<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs<VAR>this✝ : Fact (Nat.Prime p)<VAR>this : ↑n = (∏ x ∈ n.divisors.erase 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)) * ∏ x ∈ range (padicValNat p n), eval 1 (cyclotomic (p ^ (x + 1)) ℤ)<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n<VAR>hn' : n > 0<VAR>hn : 1 < n<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs<VAR>this✝ : Fact (Nat.Prime p)<VAR>this : ↑n = (∏ x ∈ n.divisors.erase 1 \ image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)) * ∏ x ∈ image (fun t => p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)<GOAL>∀ x ∈ range (padicValNat p n), ∀ y ∈ range (padicValNat p n), p ^ (x + 1) = p ^ (y + 1) → x = y
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x r y : ℝ<GOAL>y ∈ ball x r ↔ y ∈ Ioo (x - r) (x + r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f g : α → β<VAR>h : f =ᶠ[l] g<GOAL>EventuallyConst f l ↔ EventuallyConst g l
<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>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<GOAL>s ∥ ⊥ ↔ s = ⊥
<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>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>h : s ∥ ⊥<GOAL>s = ⊥
<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>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>v : V<VAR>h : ⊥ = map (↑(constVAdd k P v)) s<GOAL>s = ⊥
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<GOAL>content 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a : ℕ<VAR>b : ℤ<GOAL>multiplicity a b.natAbs = multiplicity (↑a) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a : ℕ<VAR>b : ℤ<VAR>h : b = ↑b.natAbs<GOAL>multiplicity a b.natAbs = multiplicity ↑a ↑b.natAbs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a : ℕ<VAR>b : ℤ<VAR>h : b = -↑b.natAbs<GOAL>multiplicity a b.natAbs = multiplicity (↑a) (-↑b.natAbs)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>inst✝¹⁶ : NormedField 𝕜₁<VAR>inst✝¹⁵ : NormedField 𝕜₂<VAR>inst✝¹⁴ : NormedField 𝕜₃<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>τ : 𝕜₂ →+* 𝕜₃<VAR>ρ : 𝕜₁ →+* 𝕜₃<VAR>inst✝¹³ : RingHomCompTriple σ τ ρ<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜₁ E<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜₃ G<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalAddGroup G<VAR>inst✝² : ContinuousConstSMul 𝕜₃ G<VAR>inst✝¹ : RingHomSurjective σ<VAR>inst✝ : RingHomIsometric σ<VAR>L : E →SL[σ] F<VAR>this : UniformSpace G := TopologicalAddGroup.toUniformSpace G<GOAL>Continuous { toFun := fun f => f.comp L, map_add' := ⋯, map_smul' := ⋯ }.toFun
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>inst✝¹⁶ : NormedField 𝕜₁<VAR>inst✝¹⁵ : NormedField 𝕜₂<VAR>inst✝¹⁴ : NormedField 𝕜₃<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>τ : 𝕜₂ →+* 𝕜₃<VAR>ρ : 𝕜₁ →+* 𝕜₃<VAR>inst✝¹³ : RingHomCompTriple σ τ ρ<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜₁ E<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜₃ G<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalAddGroup G<VAR>inst✝² : ContinuousConstSMul 𝕜₃ G<VAR>inst✝¹ : RingHomSurjective σ<VAR>inst✝ : RingHomIsometric σ<VAR>L : E →SL[σ] F<VAR>this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G<VAR>this : UniformAddGroup G<GOAL>Continuous { toFun := fun f => f.comp L, map_add' := ⋯, map_smul' := ⋯ }.toFun
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>inst✝¹⁶ : NormedField 𝕜₁<VAR>inst✝¹⁵ : NormedField 𝕜₂<VAR>inst✝¹⁴ : NormedField 𝕜₃<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>τ : 𝕜₂ →+* 𝕜₃<VAR>ρ : 𝕜₁ →+* 𝕜₃<VAR>inst✝¹³ : RingHomCompTriple σ τ ρ<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜₁ E<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜₃ G<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalAddGroup G<VAR>inst✝² : ContinuousConstSMul 𝕜₃ G<VAR>inst✝¹ : RingHomSurjective σ<VAR>inst✝ : RingHomIsometric σ<VAR>L : E →SL[σ] F<VAR>this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G<VAR>this : UniformAddGroup G<GOAL>Continuous ((⇑(UniformOnFun.ofFun {S | Bornology.IsVonNBounded 𝕜₁ S}) ∘ DFunLike.coe) ∘ { toFun := fun f => f.comp L, map_add' := ⋯, map_smul' := ⋯ }.toFun)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>inst✝¹⁶ : NormedField 𝕜₁<VAR>inst✝¹⁵ : NormedField 𝕜₂<VAR>inst✝¹⁴ : NormedField 𝕜₃<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>τ : 𝕜₂ →+* 𝕜₃<VAR>ρ : 𝕜₁ →+* 𝕜₃<VAR>inst✝¹³ : RingHomCompTriple σ τ ρ<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜₁ E<VAR>inst✝¹⁰ : AddCommGroup F<VAR>inst✝⁹ : Module 𝕜₂ F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜₃ G<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalAddGroup G<VAR>inst✝² : ContinuousConstSMul 𝕜₃ G<VAR>inst✝¹ : RingHomSurjective σ<VAR>inst✝ : RingHomIsometric σ<VAR>L : E →SL[σ] F<VAR>this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G<VAR>this : UniformAddGroup G<GOAL>Continuous ((fun f => (UniformOnFun.ofFun {S | Bornology.IsVonNBounded 𝕜₁ S}) (f ∘ ⇑L)) ∘ DFunLike.coe)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>f : Filter (OnePoint X)<GOAL>f ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed s → IsCompact s → some '' sᶜ ∪ {∞} ∈ f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hnot : ¬x ^ p ^ n = 1<VAR>hfin : x ^ p ^ (n + 1) = 1<GOAL>orderOf x = p ^ (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ✝ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ✝<VAR>ρ : Measure (α × ℝ)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<GOAL>∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ✝ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ✝<VAR>ρ : Measure (α × ℝ)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ<GOAL>∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ✝ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ✝<VAR>ρ : Measure (α × ℝ)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ<GOAL>∀ᵐ (x : α) ∂ρ.fst, ∀ ⦃t : Set ℝ⦄, MeasurableSet t → (κ x) t = (ρ.condKernel x) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ✝ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ✝<VAR>ρ : Measure (α × ℝ)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ<GOAL>∀ᵐ (x : α) ∂ρ.fst, (κ x) ∅ = (ρ.condKernel x) ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ✝ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ✝<VAR>ρ : Measure (α × ℝ)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ<GOAL>∀ᵐ (x : α) ∂ρ.fst, ∀ t ∈ ⋃ a, {Iic ↑a}, (κ x) t = (ρ.condKernel x) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ✝ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ✝<VAR>ρ : Measure (α × ℝ)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ<GOAL>∀ᵐ (x : α) ∂ρ.fst, ∀ (t : Set ℝ), MeasurableSet t → (κ x) t = (ρ.condKernel x) t → (κ x) tᶜ = (ρ.condKernel x) tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ✝ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ✝<VAR>ρ : Measure (α × ℝ)<VAR>inst✝¹ : IsFiniteMeasure ρ<VAR>κ : Kernel α ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ = ρ.fst ⊗ₘ κ<VAR>huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ<GOAL>∀ᵐ (x : α) ∂ρ.fst, ∀ (f : ℕ → Set ℝ), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), (κ x) (f i) = (ρ.condKernel x) (f i)) → (κ x) (⋃ i, f i) = (ρ.condKernel x) (⋃ i, f i)
<VAR>a : ℤ<GOAL>|a|.natAbs = a.natAbs
<VAR>a : ℤ<GOAL>(↑a.natAbs).natAbs = a.natAbs
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>φ : MvPowerSeries σ R<VAR>u : Rˣ<GOAL>(constantCoeff σ R) (φ.invOfUnit u) = ↑u⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LT α<VAR>a b : αᵒᵈ<GOAL>lt.Compares (ofDual a) (ofDual b) ↔ lt.Compares b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LT α<VAR>a b : αᵒᵈ<GOAL>eq.Compares (ofDual a) (ofDual b) ↔ eq.Compares b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LT α<VAR>a b : αᵒᵈ<GOAL>gt.Compares (ofDual a) (ofDual b) ↔ gt.Compares b a
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : CategoryWithHomology C<VAR>n a a' : ℤ<VAR>ha' : n + a = a'<VAR>K : CochainComplex C ℤ<GOAL>((𝟙 (homology K a') ≫ ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').inv.app K)) ≫ 𝟙 ((shortComplexFunctor C (up ℤ) a).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K)).homology) ≫ 𝟙 (((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K).homology a) = ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').inv.app K)
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f : α → α<VAR>x y : ℕ → α<VAR>hf : Monotone f<VAR>h₀ : x 0 ≤ y 0<VAR>n : ℕ<VAR>ihn : 0 < n → (∀ (k : ℕ), k < n → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n < y n<VAR>hn : 0 < n + 1<VAR>hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)<VAR>hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)<GOAL>x (n + 1) < y (n + 1)
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f : α → α<VAR>x y : ℕ → α<VAR>hf : Monotone f<VAR>h₀ : x 0 ≤ y 0<VAR>n : ℕ<VAR>ihn : 0 < n → (∀ (k : ℕ), k < n → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n < y n<VAR>hn : 0 < n + 1<VAR>hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)<VAR>hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)<GOAL>x n ≤ y n
<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n)) n
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<GOAL>IsUnit ↑r.den
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<GOAL>‖↑r.den‖ = 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<GOAL>1 ≤ ‖↑↑r.den‖
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<GOAL>¬‖↑r.den‖ < 1
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>norm_denom_lt : ‖↑r.den‖ < 1<GOAL>False
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>norm_denom_lt : ‖↑r.den‖ < 1<VAR>hr : ‖↑r * ↑r.den‖ = ‖↑r.num‖<GOAL>False
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>norm_denom_lt : ‖↑r.den‖ < 1<VAR>hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖<GOAL>False
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>norm_denom_lt : ‖↑r.den‖ < 1<VAR>hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖<VAR>key : ‖↑r.num‖ < 1<GOAL>False
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>norm_denom_lt : ‖↑r.den‖ < 1<VAR>hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖<VAR>key : ‖↑r.num‖ < 1<VAR>this : ↑p ∣ r.num ∧ ↑p ∣ ↑r.den<GOAL>False
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r✝ r : ℚ<VAR>h : ‖↑r‖ ≤ 1<VAR>norm_denom_lt : ‖↑r.den‖ < 1<VAR>hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖<VAR>key : ‖↑r.num‖ < 1<VAR>this : ↑p ∣ r.num ∧ ↑p ∣ ↑r.den<GOAL>p ∣ 1
<VAR>m n a b c d : ℕ<VAR>hm : 0 < m<VAR>h : a * c ≡ b * c [MOD m]<GOAL>a ≡ b [MOD m / m.gcd c]
<VAR>m n a b c d : ℕ<VAR>hm : 0 < m<VAR>h : a * c ≡ b * c [MOD m]<GOAL>c * a ≡ c * b [MOD m]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure β<VAR>x : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((Kernel.sum fun n => const α (μ n)) x) s = ((const α (Measure.sum μ)) x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>inst✝ : Countable ι<VAR>μ : ι → Measure β<VAR>x : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∑' (n : ι), ((const α (μ n)) x) s = ∑' (i : ι), (μ i) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f✝ : ℕ → α<VAR>a : α<VAR>f : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), 0 ≤ f n<GOAL>Summable f ↔ ¬Tendsto (fun n => ∑ i ∈ range n, f i) atTop atTop
<VAR>x y : ℝ<GOAL>sin x * sin x ≤ 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : Inducing (g ∘ f)<GOAL>inst✝² ≤ induced f inst✝¹
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : Inducing (g ∘ f)<GOAL>induced f inst✝¹ ≤ inst✝²
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : Inducing (g ∘ f)<GOAL>induced f inst✝¹ ≤ induced f (induced g inst✝)
<GOAL>Tendsto sin (𝓝[>] (-(π / 2))) (𝓝 (-1))