ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p✝ p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>l : Filter X<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>h : l.HasBasis p s<VAR>ho : ∀ (i : ι), p i → IsOpen (s i)<VAR>i : ι<VAR>hi : p i<GOAL>interior (s i) ∈ l
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>f i ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>gramSchmidt 𝕜 f i + ∑ i_1 ∈ Finset.Iio i, ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>gramSchmidt 𝕜 f i + ∑ x ∈ Finset.Iio i, (⟪gramSchmidt 𝕜 f x, f i⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f x‖ ^ 2)) • gramSchmidt 𝕜 f x ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p} ℚ K<VAR>hζ✝ : IsPrimitiveRoot ζ ↑p<VAR>hodd : p ≠ 2<VAR>this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))<GOAL>¬∃ n, ↑↑p ∣ hζ✝.toInteger - ↑n
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι✝ → Type u_3<VAR>inst✝⁴ : Fintype ι✝<VAR>m✝¹ : (i : ι✝) → OuterMeasure (α✝ i)<VAR>m✝ : (i : ι✝) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι✝) → Measure (α✝ i)<VAR>inst✝³ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>inst✝² : Fintype ι'<VAR>ι : Type u<VAR>α : ι → Type v<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : IsEmpty ι<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit<GOAL>MeasurePreserving (⇑e) (Measure.pi μ) (Measure.dirac ())
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι✝ → Type u_3<VAR>inst✝⁴ : Fintype ι✝<VAR>m✝¹ : (i : ι✝) → OuterMeasure (α✝ i)<VAR>m✝ : (i : ι✝) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι✝) → Measure (α✝ i)<VAR>inst✝³ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>inst✝² : Fintype ι'<VAR>ι : Type u<VAR>α : ι → Type v<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : IsEmpty ι<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit<GOAL>Measure.map (⇑e) (Measure.pi μ) = Measure.dirac ()
<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>hb : b ≤ 0<GOAL>a / b ≤ 0
<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>hb : b ≤ 0<GOAL>a * b⁻¹ ≤ 0
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i j : Fin n✝<VAR>n : ℕ<GOAL>Set.range succ = {0}ᶜ
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i j : Fin n✝<VAR>n : ℕ<GOAL>Set.range (succAbove 0) = {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>f : X → Y<VAR>hf : Continuous f<GOAL>comap f (coLindelof Y) ≤ coLindelof X
<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>f : X → Y<VAR>hf : Continuous f<GOAL>∀ (i' : Set X), IsLindelof i' → ∃ i, IsLindelof i ∧ f ⁻¹' iᶜ ⊆ 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>f : X → Y<VAR>hf : Continuous f<VAR>t : Set X<VAR>ht : IsLindelof t<GOAL>∃ i, IsLindelof i ∧ f ⁻¹' iᶜ ⊆ tᶜ
<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>f : X → Y<VAR>hf : Continuous f<VAR>t : Set X<VAR>ht : IsLindelof t<GOAL>f ⁻¹' (f '' t)ᶜ ⊆ tᶜ
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>t' : Finset α<VAR>s' : α → Finset γ<VAR>h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'<VAR>f : γ → α → β<GOAL>∏ x ∈ s, ∏ y ∈ t x, f x y = ∏ y ∈ t', ∏ x ∈ s' y, f x y
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>x : E<VAR>I : Type u_3<VAR>inst✝ : TopologicalSpace I<VAR>h✝ : IsEvenlyCovered f (f x) I<VAR>e : Trivialization I f := Classical.choose ⋯<VAR>h : f x ∈ (Classical.choose ⋯).baseSet := Classical.choose_spec h✝.right<VAR>he : (f x, (↑e x).2) = ↑e x := Trivialization.mk_proj_snd' e h<GOAL>(f x, (↑e x).2) ∈ e.target
<VAR>F : 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✝¹ : CompleteLattice β<VAR>inst✝ : DecidableEq α<VAR>f : γ → α<VAR>g : α → β<VAR>s : Finset γ<GOAL>⨆ x ∈ image f s, g x = ⨆ y ∈ s, g (f y)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>a✝ : Nontrivial R<GOAL>(p * q).nextCoeff = p.nextCoeff + q.nextCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>a✝ : Nontrivial R<GOAL>(p * q).reverse.coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁷ : SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>inst✝⁶ : SeminormedAddCommGroup M₁<VAR>inst✝⁵ : TopologicalSpace M₂<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : NormedSpace 𝕜₁ M₁<VAR>inst✝² : Module 𝕜₂ M₂<VAR>inst✝¹ : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝ : T2Space M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>S : Set M₁<VAR>hS : Bornology.IsBounded S<GOAL>IsVonNBounded 𝕜₁ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>m : ℕ<VAR>hm : multiplicity a b < ↑m<VAR>h : a ^ m ∣ b<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>m : ℕ<VAR>hm : ∃ (h : (multiplicity a b).Dom), (multiplicity a b).get h < m<VAR>h : a ^ m ∣ b<GOAL>False
<VAR>a b : Ordinal.{u_1}<VAR>ha : 0 < a<GOAL>a * b ≤ b ↔ a ^ ω ∣ b
<VAR>a b : Ordinal.{u_1}<VAR>ha : 0 < a<GOAL>a * b ≤ b ↔ a * b = b
<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>f✝ f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Set α<VAR>t✝ t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>f : α × β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>image2 (fun a b => f (a, b)) s t = f '' s ×ˢ t
<VAR>n p : ℕ<VAR>hp : Prime p<VAR>hp' : _root_.Prime p<GOAL>multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
<VAR>n p : ℕ<VAR>hp : Prime p<VAR>hp' : _root_.Prime p<VAR>h0 : 2 ≤ p<GOAL>multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
<VAR>n p : ℕ<VAR>hp : Prime p<VAR>hp' : _root_.Prime p<VAR>h0 : 2 ≤ p<VAR>h1 : 1 ≤ p * n + 1<GOAL>multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
<VAR>n p : ℕ<VAR>hp : Prime p<VAR>hp' : _root_.Prime p<VAR>h0 : 2 ≤ p<VAR>h1 : 1 ≤ p * n + 1<VAR>h2 : p * n + 1 ≤ p * (n + 1)<VAR>h3 : p * n + 1 ≤ p * (n + 1) + 1<GOAL>multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
<VAR>n p : ℕ<VAR>hp : Prime p<VAR>hp' : _root_.Prime p<VAR>h0 : 2 ≤ p<VAR>h1 : 1 ≤ p * n + 1<VAR>h2 : p * n + 1 ≤ p * (n + 1)<VAR>h3 : p * n + 1 ≤ p * (n + 1) + 1<VAR>hm : multiplicity p (p * n)! ≠ ⊤<GOAL>multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
<VAR>n p : ℕ<VAR>hp : Prime p<VAR>hp' : _root_.Prime p<VAR>h0 : 2 ≤ p<VAR>h1 : 1 ≤ p * n + 1<VAR>h2 : p * n + 1 ≤ p * (n + 1)<VAR>h3 : p * n + 1 ≤ p * (n + 1) + 1<GOAL>multiplicity p (p * n)! ≠ ⊤ → multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
<VAR>n p : ℕ<VAR>hp : Prime p<VAR>hp' : _root_.Prime p<VAR>h0 : 2 ≤ p<VAR>h1 : 1 ≤ p * n + 1<VAR>h2 : p * n + 1 ≤ p * (n + 1)<VAR>h3 : p * n + 1 ≤ p * (n + 1) + 1<VAR>h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), multiplicity p m = 0<GOAL>multiplicity p (p * n)! ≠ ⊤ → multiplicity p (p * (n + 1))! = multiplicity p (p * n)! + multiplicity p (n + 1) + 1
<VAR>n p : ℕ<VAR>hp : Prime p<VAR>hp' : _root_.Prime p<VAR>h0 : 2 ≤ p<VAR>h1 : 1 ≤ p * n + 1<VAR>h2 : p * n + 1 ≤ p * (n + 1)<VAR>h3 : p * n + 1 ≤ p * (n + 1) + 1<VAR>h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), multiplicity p m = 0<GOAL>∑ x ∈ Ico 1 (p * n + 1), multiplicity p x ≠ ⊤ → ∑ x ∈ Ico 1 (p * n + 1), multiplicity p x + ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), multiplicity p x = ∑ x ∈ Ico 1 (p * n + 1), multiplicity p x + (multiplicity p (n + 1) + 1)
<VAR>n p : ℕ<VAR>hp : Prime p<VAR>hp' : _root_.Prime p<VAR>h0 : 2 ≤ p<VAR>h1 : 1 ≤ p * n + 1<VAR>h2 : p * n + 1 ≤ p * (n + 1)<VAR>h3 : p * n + 1 ≤ p * (n + 1) + 1<VAR>h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), multiplicity p m = 0<VAR>h : ∑ x ∈ Ico 1 (p * n + 1), multiplicity p x ≠ ⊤<GOAL>∑ x ∈ Ico 1 (p * n + 1), multiplicity p x + ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), multiplicity p x = ∑ x ∈ Ico 1 (p * n + 1), multiplicity p x + (multiplicity p (n + 1) + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : LinearOrderedField β<VAR>a✝ a₁ a₂ : α<VAR>b : β<VAR>q : ℚ<VAR>inst✝ : Archimedean α<VAR>a : α<GOAL>BddAbove (cutMap β a)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : LinearOrderedField β<VAR>a✝ a₁ a₂ : α<VAR>b : β<VAR>q✝ : ℚ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>q : ℚ<VAR>hq : a < ↑q<GOAL>BddAbove (cutMap β a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra 𝕜 A<VAR>M : Type u_3<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module 𝕜 M<VAR>f : Module.End 𝕜 M<GOAL>Ideal.span {minpoly 𝕜 f} = Module.annihilator 𝕜[X] (Module.AEval' f)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra 𝕜 A<VAR>M : Type u_3<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module 𝕜 M<VAR>f : Module.End 𝕜 M<GOAL>annIdeal 𝕜 f = Module.annihilator 𝕜[X] (Module.AEval' f)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra 𝕜 A<VAR>M : Type u_3<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module 𝕜 M<VAR>f : Module.End 𝕜 M<VAR>x✝ : 𝕜[X]<GOAL>x✝ ∈ annIdeal 𝕜 f ↔ x✝ ∈ Module.annihilator 𝕜[X] (Module.AEval' f)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra 𝕜 A<VAR>M : Type u_3<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module 𝕜 M<VAR>f : Module.End 𝕜 M<VAR>x✝ : 𝕜[X]<GOAL>(∀ (x : M), ((aeval f) x✝) x = 0 x) ↔ ∀ (m : Module.AEval' f), x✝ • m = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q✝ : R[X]<VAR>ι : Type u_1<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>H : p.leadingCoeff = 0<GOAL>(p * q).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q✝ : R[X]<VAR>ι : Type u_1<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>H : p.leadingCoeff ≠ 0<GOAL>(p * q).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q✝ : R[X]<VAR>ι : Type u_1<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>H : p.leadingCoeff ≠ 0<GOAL>p.leadingCoeff * q.leadingCoeff ≠ 0
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>f : α → ℝ<VAR>h : Summable fun x => ↑(f x)<GOAL>Summable f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f : M → N<VAR>p : M → Prop<VAR>h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y<VAR>hp_mul : ∀ (x y : M), p x → p y → p (x * y)<VAR>g : ι → M<VAR>s : Finset ι<VAR>hs_nonempty : s.Nonempty<VAR>hs : ∀ i ∈ s, p (g i)<GOAL>f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f : M → N<VAR>p : M → Prop<VAR>h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y<VAR>hp_mul : ∀ (x y : M), p x → p y → p (x * y)<VAR>g : ι → M<VAR>s : Finset ι<VAR>hs_nonempty : s.Nonempty<VAR>hs : ∀ i ∈ s, p (g i)<GOAL>Multiset.map (fun i => g i) s.val ≠ ∅
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f : M → N<VAR>p : M → Prop<VAR>h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y<VAR>hp_mul : ∀ (x y : M), p x → p y → p (x * y)<VAR>g : ι → M<VAR>s : Finset ι<VAR>hs_nonempty : s.Nonempty<VAR>hs : ∀ i ∈ s, p (g i)<GOAL>∀ a ∈ Multiset.map (fun i => g i) s.val, p a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f : M → N<VAR>p : M → Prop<VAR>h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y<VAR>hp_mul : ∀ (x y : M), p x → p y → p (x * y)<VAR>g : ι → M<VAR>s : Finset ι<VAR>hs_nonempty : s.Nonempty<VAR>hs : ∀ i ∈ s, p (g i)<GOAL>(Multiset.map f (Multiset.map (fun i => g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f : M → N<VAR>p : M → Prop<VAR>h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y<VAR>hp_mul : ∀ (x y : M), p x → p y → p (x * y)<VAR>g : ι → M<VAR>s : Finset ι<VAR>hs_nonempty : s.Nonempty<VAR>hs : ∀ i ∈ s, p (g i)<GOAL>(Multiset.map (f ∘ fun i => g i) s.val).prod ≤ ∏ i ∈ s, f (g i)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n✝ m✝ n : ℤ<VAR>z₁ : Cochain F G n<VAR>f : G ⟶ K<VAR>m : ℤ<GOAL>δ n m (z₁.comp (Cochain.ofHom f) ⋯) = (δ n m z₁).comp (Cochain.ofHom f) ⋯
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>x : α<GOAL>‖(WithLp.equiv p (α × β)).symm (x, 0)‖₊ = ‖x‖₊
<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>s : Sphere P<VAR>p₁ p₂ p₃ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₃ : p₂ ≠ p₃<GOAL>∡ p₁ s.center p₃ = 2 • ∡ p₁ 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>s : Sphere P<VAR>p₁ p₂ p₃ : P<VAR>hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius<VAR>hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius<VAR>hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₃ : p₂ ≠ p₃<GOAL>∡ p₁ s.center p₃ = 2 • ∡ p₁ p₂ p₃
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>j : Fin (n + 1)<VAR>op : α → α → α<VAR>g : Fin (n + 1) → α<VAR>k : Fin n<VAR>hjk : ↑j ≠ ↑k<GOAL>j.contractNth op g k = g (j.succAbove k)
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>j : Fin (n + 1)<VAR>op : α → α → α<VAR>g : Fin (n + 1) → α<VAR>k : Fin n<VAR>hjk : ↑j ≠ ↑k<VAR>h : ↑k < ↑j<GOAL>j.contractNth op g k = g (j.succAbove k)
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>j : Fin (n + 1)<VAR>op : α → α → α<VAR>g : Fin (n + 1) → α<VAR>k : Fin n<VAR>hjk : ↑j ≠ ↑k<VAR>h : ↑k = ↑j<GOAL>j.contractNth op g k = g (j.succAbove k)
<VAR>m n : ℕ<VAR>α : Type u_1<VAR>j : Fin (n + 1)<VAR>op : α → α → α<VAR>g : Fin (n + 1) → α<VAR>k : Fin n<VAR>hjk : ↑j ≠ ↑k<VAR>h : ↑j < ↑k<GOAL>j.contractNth op g k = g (j.succAbove k)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>x : X × Y<GOAL>map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x) = 𝓝 x.1
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>x : X × Y<VAR>s : Set X<VAR>hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x)<GOAL>s ∈ 𝓝 x.1
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {(x, y).2}] (x, y))<GOAL>s ∈ 𝓝 (x, y).1
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>hs : ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.snd ⁻¹' {(x, y).2} → x_1 ∈ Prod.fst ⁻¹' s}<GOAL>s ∈ 𝓝 (x, y).1
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>u : Set X<VAR>hu : u ∈ 𝓝 x<VAR>v : Set Y<VAR>hv : v ∈ 𝓝 y<VAR>H : u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.snd ⁻¹' {(x, y).2} → x_1 ∈ Prod.fst ⁻¹' s}<GOAL>s ∈ 𝓝 (x, y).1
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>u : Set X<VAR>hu : u ∈ 𝓝 x<VAR>v : Set Y<VAR>hv : v ∈ 𝓝 y<VAR>H : ∀ x ∈ u, ∀ y_1 ∈ v, y_1 = y → x ∈ s<GOAL>s ∈ 𝓝 (x, y).1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedLinearOrderedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x y z : E<VAR>a b r : ℝ<VAR>h : ‖x‖ = ‖y‖<GOAL>‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<GOAL>⊤.prod g = comap Prod.snd g
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>C : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x<VAR>bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C<VAR>g : ℝ → E := fun x => f x - f a<GOAL>∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>C : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x<VAR>bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C<VAR>g : ℝ → E := fun x => f x - f a<VAR>hg : ContinuousOn g (Icc a b)<GOAL>∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>C : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x<VAR>bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C<VAR>g : ℝ → E := fun x => f x - f a<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x<GOAL>∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>C : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x<VAR>bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C<VAR>g : ℝ → E := fun x => f x - f a<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x<VAR>B : ℝ → ℝ := fun x => C * (x - a)<GOAL>∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>C : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x<VAR>bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C<VAR>g : ℝ → E := fun x => f x - f a<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x<VAR>B : ℝ → ℝ := fun x => C * (x - a)<VAR>hB : ∀ (x : ℝ), HasDerivAt B C x<GOAL>∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>C : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x<VAR>bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C<VAR>g : ℝ → E := fun x => f x - f a<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x<VAR>B : ℝ → ℝ := fun x => C * (x - a)<VAR>hB : ∀ (x : ℝ), HasDerivAt B C x<GOAL>‖g a‖ ≤ B a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>f' : ℝ → E<VAR>C : ℝ<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x<VAR>bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C<VAR>g : ℝ → E := fun x => f x - f a<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ x ∈ Ico a b, HasDerivWithinAt g (f' x) (Ici x) x<VAR>B : ℝ → ℝ := fun x => C * (x - a)<VAR>hB : ∀ (x : ℝ), HasDerivAt B C x<GOAL>‖f a - f a‖ ≤ C * (a - a)