ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : MultilinearMap 𝕜 E G<VAR>hf : Continuous ⇑f<VAR>h✝ : Nonempty ι<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>this : 0 < (‖c‖ / ε) ^ Fintype.card ι<GOAL>∀ (m : (i : ι) → E i), ‖f m‖ ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : MultilinearMap 𝕜 E G<VAR>hf : Continuous ⇑f<VAR>h✝ : Nonempty ι<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>this : 0 < (‖c‖ / ε) ^ Fintype.card ι<VAR>m : (i : ι) → E i<VAR>hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖<VAR>hm : ∀ (i : ι), ‖m i‖ < ε<GOAL>‖f m‖ ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : MultilinearMap 𝕜 E G<VAR>hf : Continuous ⇑f<VAR>h✝ : Nonempty ι<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>this : 0 < (‖c‖ / ε) ^ Fintype.card ι<VAR>m : (i : ι) → E i<VAR>hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖<VAR>hm : ∀ (i : ι), ‖m i‖ < ε<GOAL>1 ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : MultilinearMap 𝕜 E G<VAR>hf : Continuous ⇑f<VAR>h✝ : Nonempty ι<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>this : 0 < (‖c‖ / ε) ^ Fintype.card ι<VAR>m : (i : ι) → E i<VAR>hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖<VAR>hm : ∀ (i : ι), ‖m i‖ < ε<GOAL>∏ _x : ι, ε / ‖c‖ ≤ ∏ i : ι, ‖m i‖
<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>inst✝² : SemilatticeSup α<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : atTop.IsCountablyGenerated<GOAL>∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
<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>inst✝² : SemilatticeSup α<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>ys : ℕ → α<VAR>h : Tendsto ys atTop atTop<GOAL>∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
<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>inst✝² : SemilatticeSup α<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>ys : ℕ → α<VAR>h : Tendsto ys atTop atTop<VAR>xs : ℕ → α := fun n => (Finset.range (n + 1)).sup' ⋯ ys<GOAL>∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
<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>inst✝² : SemilatticeSup α<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>ys : ℕ → α<VAR>h : Tendsto ys atTop atTop<VAR>xs : ℕ → α := fun n => (Finset.range (n + 1)).sup' ⋯ ys<VAR>h_mono : Monotone xs<GOAL>∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
<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>inst✝² : SemilatticeSup α<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>ys : ℕ → α<VAR>h : Tendsto ys atTop atTop<VAR>xs : ℕ → α := fun n => (Finset.range (n + 1)).sup' ⋯ ys<VAR>h_mono : Monotone xs<VAR>n : ℕ<GOAL>n ∈ Finset.range (n + 1)
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : IsSepClosed k<VAR>x : k<VAR>n : ℕ<VAR>hn : NeZero ↑n<GOAL>∃ z, z ^ n = x
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : IsSepClosed k<VAR>x : k<VAR>n : ℕ<VAR>hn : NeZero ↑n<VAR>hn' : 0 < n<GOAL>∃ z, z ^ n = x
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : IsSepClosed k<VAR>x : k<VAR>n : ℕ<VAR>hn : NeZero ↑n<VAR>hn' : 0 < n<VAR>this : (X ^ n - C x).degree ≠ 0<GOAL>∃ z, z ^ n = x
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : Fintype ι<VAR>z : M₂<GOAL>MultilinearMap.mkPiRing R ι z = 0 ↔ z = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>⋃ a ∈ s, f a '' t = image2 f s t
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>↑n = ↑n.pred' + 1
<VAR>u v : PrimeMultiset<VAR>n : ℕ+ := u.prod<VAR>m : ℕ+ := v.prod<GOAL>(u ⊔ v).prod = n.lcm m
<VAR>u v : PrimeMultiset<VAR>n : ℕ+ := u.prod<VAR>m : ℕ+ := v.prod<VAR>this : u = n.factorMultiset<GOAL>(u ⊔ v).prod = n.lcm m
<VAR>u v : PrimeMultiset<VAR>n : ℕ+ := u.prod<VAR>m : ℕ+ := v.prod<VAR>this : u = n.factorMultiset<GOAL>(n.factorMultiset ⊔ v).prod = n.lcm m
<VAR>u v : PrimeMultiset<VAR>n : ℕ+ := u.prod<VAR>m : ℕ+ := v.prod<VAR>this✝ : u = n.factorMultiset<VAR>this : v = m.factorMultiset<GOAL>(n.factorMultiset ⊔ v).prod = n.lcm m
<VAR>u v : PrimeMultiset<VAR>n : ℕ+ := u.prod<VAR>m : ℕ+ := v.prod<VAR>this✝ : u = n.factorMultiset<VAR>this : v = m.factorMultiset<GOAL>(n.factorMultiset ⊔ m.factorMultiset).prod = n.lcm m
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Fintype α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : LocallyFiniteOrderTop α<VAR>inst✝¹ : LocallyFiniteOrderBot α<VAR>inst✝ : CommMonoid M<VAR>f : α → α → M<GOAL>∏ i : α, ∏ j ∈ Ioi i, f j i * f i j = ∏ i : α, ∏ j ∈ {i}ᶜ, f j i
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Fintype α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : LocallyFiniteOrderTop α<VAR>inst✝¹ : LocallyFiniteOrderBot α<VAR>inst✝ : CommMonoid M<VAR>f : α → α → M<GOAL>(∏ x : α, ∏ x_1 ∈ Ioi x, f x_1 x) * ∏ x : α, ∏ x_1 ∈ Ioi x, f x x_1 = (∏ x : α, ∏ x_1 ∈ Ioi x, f x_1 x) * ∏ x : α, ∏ x_1 ∈ Iio x, f x_1 x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Fintype α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : LocallyFiniteOrderTop α<VAR>inst✝¹ : LocallyFiniteOrderBot α<VAR>inst✝ : CommMonoid M<VAR>f : α → α → M<GOAL>∏ x : α, ∏ x_1 ∈ Ioi x, f x x_1 = ∏ x : α, ∏ x_1 ∈ Iio x, f x_1 x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Fintype α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : LocallyFiniteOrderTop α<VAR>inst✝¹ : LocallyFiniteOrderBot α<VAR>inst✝ : CommMonoid M<VAR>f : α → α → M<GOAL>∏ x ∈ univ.sigma Ioi, f x.fst x.snd = ∏ x ∈ univ.sigma Iio, f x.snd x.fst
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<GOAL>(trinomial k m n u v w).coeff m = v
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>arctan x = arccos (√(1 + x ^ 2))⁻¹
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>arcsin (x / √(1 + x ^ 2)) = arcsin √(1 - (√(1 + x ^ 2))⁻¹ ^ 2)
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>0 ≤ (√(1 + x ^ 2))⁻¹
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>x / √(1 + x ^ 2) = √(1 - (√(1 + x ^ 2))⁻¹ ^ 2)
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>0 ≤ x ^ 2
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>1 + x ^ 2 ≠ 0
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>0 ≤ (1 + x ^ 2)⁻¹
<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<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>inst✝ : Infinite ι<VAR>κ : Type w<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<GOAL>#κ = #ι
<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<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>inst✝ : Infinite ι<VAR>κ : Type w<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<GOAL>#κ ≤ #ι
<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<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>inst✝ : Infinite ι<VAR>κ : Type w<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<GOAL>#ι ≤ #κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}<GOAL>o.bsup f = 0 ↔ ∀ (i : Ordinal.{u_4}) (hi : i < o), f i hi = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}<VAR>h : o.bsup f = 0<VAR>i : Ordinal.{u_4}<VAR>hi : i < o<GOAL>f i hi = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}<VAR>h : o.bsup f = 0<VAR>i : Ordinal.{u_4}<VAR>hi : i < o<GOAL>f i hi ≤ o.bsup f
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>A B✝ X X' Y Y' Z : C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : Exponentiable A<VAR>I B : C<VAR>t : IsInitial I<VAR>inst✝ : CartesianClosed C<VAR>Z✝ : C<VAR>g h : Z✝ ⟶ I<VAR>x✝ : g ≫ t.to B = h ≫ t.to B<GOAL>g = h
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>A B✝ X X' Y Y' Z : C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : Exponentiable A<VAR>I B : C<VAR>t : IsInitial I<VAR>inst✝ : CartesianClosed C<VAR>Z✝ : C<VAR>g h : Z✝ ⟶ I<VAR>x✝ : g ≫ t.to B = h ≫ t.to B<VAR>this : IsIso g<GOAL>g = h
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>A B✝ X X' Y Y' Z : C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : Exponentiable A<VAR>I B : C<VAR>t : IsInitial I<VAR>inst✝ : CartesianClosed C<VAR>Z✝ : C<VAR>g h : Z✝ ⟶ I<VAR>x✝ : g ≫ t.to B = h ≫ t.to B<VAR>this✝ : IsIso g<VAR>this : IsIso h<GOAL>g = h
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : Nontrivial A<VAR>a : A<GOAL>(spectrum ℂ a).Nonempty
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : Nontrivial A<VAR>a : A<VAR>h : spectrum ℂ a = ∅<GOAL>False
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : Nontrivial A<VAR>a : A<VAR>h : spectrum ℂ a = ∅<VAR>H₀ : resolventSet ℂ a = Set.univ<GOAL>False
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : Nontrivial A<VAR>a : A<VAR>h : spectrum ℂ a = ∅<VAR>H₀ : resolventSet ℂ a = Set.univ<VAR>H₁ : Differentiable ℂ fun z => resolvent a z<GOAL>False
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedRing A<VAR>inst✝² : NormedAlgebra ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>inst✝ : Nontrivial A<VAR>a : A<VAR>h : spectrum ℂ a = ∅<VAR>H₀ : resolventSet ℂ a = Set.univ<VAR>H₁ : Differentiable ℂ fun z => resolvent a z<VAR>H₃ : resolvent a 0 = 0<GOAL>False
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{?u.37143, u_1} C<VAR>inst✝⁶ : Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>inst✝⁵ : TotalComplexShape c₁ c₂ c<VAR>inst✝⁴ : TotalComplexShape c₂ c₁ c<VAR>inst✝³ : TotalComplexShapeSymmetry c₁ c₂ c<VAR>inst✝² : K.HasTotal c<VAR>inst✝¹ : K.flip.HasTotal c<VAR>inst✝ : DecidableEq J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>j : J<VAR>h : c₂.π c₁ c (i₂, i₁) = j<GOAL>c₁.π c₂ c (i₁, i₂) = j
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x' : Dual 𝕜 E<VAR>hx' : x' ∈ polar 𝕜 (ball 0 r)<GOAL>x' ∈ closedBall 0 (‖c‖ / r)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x' : Dual 𝕜 E<VAR>hx' : ∀ z ∈ ball 0 r, ‖x' z‖ ≤ 1<GOAL>x' ∈ closedBall 0 (‖c‖ / r)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x' : Dual 𝕜 E<VAR>hx' : ∀ (z : E), ‖z‖ < r → ‖x' z‖ ≤ 1<GOAL>‖x'‖ ≤ ‖c‖ / r
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x' : Dual 𝕜 E<VAR>hx' : ∀ (z : E), ‖z‖ < r → ‖x' z‖ ≤ 1<VAR>hcr : 0 < ‖c‖ / r<GOAL>‖x'‖ ≤ ‖c‖ / r
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x' : Dual 𝕜 E<VAR>hx' : ∀ (z : E), ‖z‖ < r → ‖x' z‖ ≤ 1<VAR>hcr : 0 < ‖c‖ / r<VAR>x : E<VAR>h₁ : r / ‖c‖ ≤ ‖x‖<VAR>h₂ : ‖x‖ < r<GOAL>‖x' x‖ ≤ ‖c‖ / r * ‖x‖
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>l : List α<VAR>l' : List β<VAR>n : ℕ<VAR>h : l.length = l'.length<GOAL>(zipWith f l l').rotate n = zipWith f (l.rotate n) (l'.rotate n)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>l : List α<VAR>l' : List β<VAR>n : ℕ<VAR>h : l.length = l'.length<GOAL>(drop (n % l'.length) l).length = (drop (n % l'.length) l').length
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x✝ y : R<VAR>inst✝⁴ : MonoidWithZero R<VAR>inst✝³ : MonoidWithZero S<VAR>F : Type u_3<VAR>inst✝² : FunLike F R S<VAR>inst✝¹ : MonoidWithZeroHomClass F R S<VAR>f : F<VAR>hf : Injective ⇑f<VAR>inst✝ : IsReduced S<VAR>x : R<VAR>hx : IsNilpotent x<GOAL>f x = f 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x✝ y : R<VAR>inst✝⁴ : MonoidWithZero R<VAR>inst✝³ : MonoidWithZero S<VAR>F : Type u_3<VAR>inst✝² : FunLike F R S<VAR>inst✝¹ : MonoidWithZeroHomClass F R S<VAR>f : F<VAR>hf : Injective ⇑f<VAR>inst✝ : IsReduced S<VAR>x : R<VAR>hx : IsNilpotent x<GOAL>f x = 0
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n : ℕ<GOAL>(ascPochhammer ℕ (n + 1)).smeval (-↑n) = 0
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<GOAL>𝓤 α ≤ Prod.swap <$> 𝓤 α
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<GOAL>𝓤 α ≤ comap Prod.swap (𝓤 α)
<VAR>α : Type u_1<VAR>inst✝⁵ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedAddCommMonoid γ<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : OrderTopology γ<VAR>inst✝ : ContinuousAdd γ<VAR>f : ι → α → γ<VAR>a : Finset ι<VAR>ha : ∀ i ∈ a, LowerSemicontinuousAt (f i) x<GOAL>LowerSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x
<VAR>α : Type u_1<VAR>inst✝⁵ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedAddCommMonoid γ<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : OrderTopology γ<VAR>inst✝ : ContinuousAdd γ<VAR>f : ι → α → γ<VAR>a : Finset ι<VAR>ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) univ x<GOAL>LowerSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) univ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv γ δ<GOAL>(e.prod e').symm = e.symm.prod e'.symm
<VAR>a b m n✝ p✝ n p : ℕ<VAR>pp : Prime p<VAR>hn : n ≠ 0<VAR>x✝ : ℕ<GOAL>x✝ ∈ {i | i ≠ 0 ∧ p ^ i ∣ n} ↔ x✝ ∈ Set.Icc 1 (n.factorization p)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>g : G<VAR>s t : Set α<VAR>hs : EventuallyConst s (ae μ)<GOAL>aestabilizer G μ s = ⊤
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>x✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>g✝ : G<VAR>s t : Set α<VAR>hs : EventuallyConst s (ae μ)<VAR>g : G<VAR>x✝ : g ∈ ⊤<GOAL>g ∈ aestabilizer G μ s
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : m < n + 1<GOAL>yn a1 m < yn a1 (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : m < n + 1<VAR>this : yn a1 m ≤ yn a1 n<GOAL>yn a1 m < yn a1 (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : m < n + 1<VAR>this : yn a1 m ≤ yn a1 n<GOAL>yn a1 m < xn a1 n + yn a1 n * a
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : m < n + 1<VAR>this : yn a1 m ≤ yn a1 n<GOAL>yn a1 m ≤ yn a1 n * a
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : m < n + 1<VAR>this : yn a1 m ≤ yn a1 n<GOAL>yn a1 m * 1 ≤ yn a1 n * a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>U : Opens ↑Y<VAR>S : Sieve U<VAR>hS : S ∈ (Opens.grothendieckTopology ↑Y).sieves U<VAR>x : ↑X<VAR>hx : x ∈ (Opens.map f).obj U<VAR>V : Opens ↑Y<VAR>i : V ⟶ U<VAR>hi : S.arrows i<VAR>hxV : f x ∈ V<GOAL>∃ U_1 f_1, (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>cofinite ⊓ 𝓟 sᶜ = cofinite
<VAR>R : Type<VAR>inst✝ : Ring R<VAR>d : ℤ<VAR>f g : ℤ√d →+* R<VAR>h : f sqrtd = g sqrtd<VAR>x_re x_im : ℤ<GOAL>f { re := x_re, im := x_im } = g { re := x_re, im := x_im }
<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>q : ℝ≥0∞<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>q_zero : q ≠ 0<VAR>q_top : q ≠ ⊤<GOAL>Memℒp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ ↔ Memℒp f p μ
<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>q : ℝ≥0∞<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>q_zero : q ≠ 0<VAR>q_top : q ≠ ⊤<VAR>h : Memℒp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ<GOAL>Memℒp f p μ
<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>q : ℝ≥0∞<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>q_zero : q ≠ 0<VAR>q_top : q ≠ ⊤<VAR>h : Memℒp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ<GOAL>Memℒp (fun x => ‖f x‖) p μ
<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>q : ℝ≥0∞<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>q_zero : q ≠ 0<VAR>q_top : q ≠ ⊤<VAR>h : Memℒp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ<GOAL>(fun x => ‖f x‖) = fun x => ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.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>q : ℝ≥0∞<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>q_zero : q ≠ 0<VAR>q_top : q ≠ ⊤<VAR>h : Memℒp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ<GOAL>p = p / q / q⁻¹
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ 0<GOAL>predAbove 0 i = i.pred hi
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<VAR>y : Fin n<VAR>hi : y.succ ≠ 0<GOAL>predAbove 0 y.succ = y.succ.pred hi
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p✝ : Type u_5<VAR>q✝ : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Zero α<VAR>d : m → α<VAR>p q : m → Prop<VAR>hpq : Disjoint p q<VAR>i : m<VAR>hi : p i<VAR>j : m<VAR>hj : q j<GOAL>(diagonal d).toBlock p q ⟨i, hi⟩ ⟨j, hj⟩ = 0 ⟨i, hi⟩ ⟨j, hj⟩
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p✝ : Type u_5<VAR>q✝ : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Zero α<VAR>d : m → α<VAR>p q : m → Prop<VAR>hpq : Disjoint p q<VAR>i : m<VAR>hi : p i<VAR>j : m<VAR>hj : q j<VAR>this : i ≠ j<GOAL>(diagonal d).toBlock p q ⟨i, hi⟩ ⟨j, hj⟩ = 0 ⟨i, hi⟩ ⟨j, hj⟩
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>hs : IsClosed s<GOAL>a ∈ s ↔ ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ sup f = a
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.WSameSide x y<VAR>ho : s.SOppSide x y<GOAL>False
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.WSameSide x y<VAR>ho : s.SOppSide x y<VAR>hxy : x ∈ s ∨ y ∈ s<GOAL>False
<VAR>a x✝ z x : ℂ<VAR>hx_re : x.re < 0<VAR>hx_im : x.im < 0<GOAL>x.arg = Real.arcsin ((-x).im / abs x) - π
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>b : β<GOAL>a⁻¹ • b ∈ s ↔ b ∈ a • s