ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<VAR>h : S.RightHomologyData<GOAL>(S.rightHomologyIso.symm ≪≫ h.rightHomologyIso).hom ≫ h.rightHomologyIso.inv = S.rightHomologyIso.inv
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>w : Word G<VAR>i : ι<VAR>h : H<VAR>hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i<VAR>hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → g ∈ d.set j<GOAL>h = 1
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>w : Word G<VAR>i : ι<VAR>h : H<VAR>hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g<VAR>hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g<GOAL>h = 1
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>w : Word G<VAR>i : ι<VAR>h : H<VAR>hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g<VAR>hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g<VAR>hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head<GOAL>h = 1
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>w : Word G<VAR>i : ι<VAR>h : H<VAR>hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g<VAR>hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g<VAR>hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head<VAR>hh1 : ¬h = 1<GOAL>False
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Sigma β<VAR>tail✝ : List (Sigma β)<VAR>l : List (Sigma β)<GOAL>(kerase a (s :: tail✝)).kunion (kerase a l) = kerase a ((s :: tail✝).kunion l)
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 0<GOAL>#↑s = #E
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 0<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<GOAL>#↑s = #E
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 0<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>cn_ne : ∀ (n : ℕ), c ^ n ≠ 0<GOAL>#↑s = #E
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 0<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>cn_ne : ∀ (n : ℕ), c ^ n ≠ 0<VAR>A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s<GOAL>#↑s = #E
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 0<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>cn_ne : ∀ (n : ℕ), c ^ n ≠ 0<VAR>A : ∀ (x : E), ∀ᶠ (n : ℕ) in atTop, x ∈ c ^ n • s<VAR>B : ∀ (n : ℕ), #↑(c ^ n • s) = #↑s<GOAL>#↑s = #E
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P Q R : Prop<VAR>inst✝¹ : Decidable P<VAR>inst✝ : Decidable Q<VAR>a b c : α<VAR>A : P → α<VAR>B✝ : ¬P → α<VAR>B : Q → α<VAR>C : ¬P → ¬Q → α<VAR>h : P → ¬Q<VAR>p : P<GOAL>A p = if q : Q then B q else if p : P then A p else C p q
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P Q R : Prop<VAR>inst✝¹ : Decidable P<VAR>inst✝ : Decidable Q<VAR>a b c : α<VAR>A : P → α<VAR>B✝ : ¬P → α<VAR>B : Q → α<VAR>C : ¬P → ¬Q → α<VAR>h : P → ¬Q<VAR>np : ¬P<GOAL>(fun q => C np q) = fun q => if p : P then A p else C p q
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P Q R : Prop<VAR>inst✝¹ : Decidable P<VAR>inst✝ : Decidable Q<VAR>a b c : α<VAR>A : P → α<VAR>B✝ : ¬P → α<VAR>B : Q → α<VAR>C : ¬P → ¬Q → α<VAR>h : P → ¬Q<VAR>np : ¬P<VAR>x✝ : ¬Q<GOAL>C np x✝ = if p : P then A p else C p x✝
<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 : J ≤ I<GOAL>(single I J h).IsPartition ↔ J = I
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : M →ₗ[R] N<VAR>hf : Injective ⇑f<GOAL>finrank R ↥(range f) = finrank R M
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : CommSemiring R<VAR>p : R[X]<VAR>t : Multiset ι<VAR>f : ι → R[X]<GOAL>(∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : CommSemiring R<VAR>p : R[X]<VAR>t : Multiset ι<VAR>f : ι → R[X]<GOAL>(∀ i ∈ 0, (f i).Monic) → (Multiset.map f 0).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) 0).sum
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : CommSemiring R<VAR>p : R[X]<VAR>t✝ : Multiset ι<VAR>f : ι → R[X]<VAR>a : ι<VAR>t : Multiset ι<VAR>ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) t).sum<VAR>ht : ∀ i ∈ a ::ₘ t, (f i).Monic<GOAL>(Multiset.map f (a ::ₘ t)).prod.nextCoeff = (Multiset.map (fun i => (f i).nextCoeff) (a ::ₘ t)).sum
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>K : Multicofork I<VAR>a : I.L<GOAL>K.ι.app (WalkingMultispan.left a) = I.fst a ≫ K.π (I.fstFrom a)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>K : Multicofork I<VAR>a : I.L<GOAL>I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (I.fstFrom a)) = I.fst a ≫ K.π (I.fstFrom a)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r₁ r₂ : ℕ → ℝ<VAR>hr : Tendsto r₁ atTop (𝓝[>] 0)<VAR>hMr : ∀ᶠ (i : ℕ) in atTop, M * r₁ i ≤ r₂ i<VAR>R₁ : ℕ → ℝ := fun i => max 0 (r₁ i)<VAR>R₂ : ℕ → ℝ := fun i => max 0 (r₂ i)<GOAL>blimsup (fun i => cthickening (r₁ i) (s i)) atTop p ≤ᶠ[ae μ] blimsup (fun i => cthickening (r₂ i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r₁ r₂ : ℕ → ℝ<VAR>hr : Tendsto r₁ atTop (𝓝[>] 0)<VAR>hMr : ∀ᶠ (i : ℕ) in atTop, M * r₁ i ≤ r₂ i<VAR>R₁ : ℕ → ℝ := fun i => max 0 (r₁ i)<VAR>R₂ : ℕ → ℝ := fun i => max 0 (r₂ i)<VAR>hRp : 0 ≤ R₁<GOAL>blimsup (fun i => cthickening (r₁ i) (s i)) atTop p ≤ᶠ[ae μ] blimsup (fun i => cthickening (r₂ i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r₁ r₂ : ℕ → ℝ<VAR>hr : Tendsto r₁ atTop (𝓝[>] 0)<VAR>R₁ : ℕ → ℝ := fun i => max 0 (r₁ i)<VAR>R₂ : ℕ → ℝ := fun i => max 0 (r₂ i)<VAR>hRp : 0 ≤ R₁<VAR>hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i<GOAL>blimsup (fun i => cthickening (r₁ i) (s i)) atTop p ≤ᶠ[ae μ] blimsup (fun i => cthickening (r₂ i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r₁ r₂ : ℕ → ℝ<VAR>hr : Tendsto r₁ atTop (𝓝[>] 0)<VAR>R₁ : ℕ → ℝ := fun i => max 0 (r₁ i)<VAR>R₂ : ℕ → ℝ := fun i => max 0 (r₂ i)<VAR>hRp : 0 ≤ R₁<VAR>hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i<GOAL>blimsup (fun i => cthickening (max 0 (r₁ i)) (s i)) atTop p ≤ᶠ[ae μ] blimsup (fun i => cthickening (max 0 (r₂ i)) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r₁ r₂ : ℕ → ℝ<VAR>hr : Tendsto r₁ atTop (𝓝[>] 0)<VAR>R₁ : ℕ → ℝ := fun i => max 0 (r₁ i)<VAR>R₂ : ℕ → ℝ := fun i => max 0 (r₂ i)<VAR>hRp : 0 ≤ R₁<VAR>hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i<VAR>hM' : 1 ≤ M<GOAL>blimsup (fun i => cthickening (max 0 (r₁ i)) (s i)) atTop p ≤ᶠ[ae μ] blimsup (fun i => cthickening (max 0 (r₂ i)) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r₁ r₂ : ℕ → ℝ<VAR>hr : Tendsto r₁ atTop (𝓝[>] 0)<VAR>R₁ : ℕ → ℝ := fun i => max 0 (r₁ i)<VAR>R₂ : ℕ → ℝ := fun i => max 0 (r₂ i)<VAR>hRp : 0 ≤ R₁<VAR>hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i<VAR>hM' : M < 1<GOAL>blimsup (fun i => cthickening (max 0 (r₁ i)) (s i)) atTop p ≤ᶠ[ae μ] blimsup (fun i => cthickening (max 0 (r₂ i)) (s i)) atTop p
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<GOAL>xn a1 n ∣ Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h1 : Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (Pell.d a1 * yn a1 n * yn a1 n + 1) * xn a1 j<GOAL>xn a1 n ∣ Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h1 : Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (Pell.d a1 * yn a1 n * yn a1 n + 1) * xn a1 j<VAR>h2 : Pell.d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n<GOAL>xn a1 n ∣ Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h1 : Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j<VAR>h2 : Pell.d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n<GOAL>xn a1 n ∣ Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<VAR>h1 : Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j<VAR>h2 : Pell.d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n<GOAL>xn a1 n ∣ xn a1 n * (xn a1 n * xn a1 j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<VAR>inst✝ : Star α<GOAL>∀ (v : Fin 0 → α), (circulant v)ᴴ = circulant (star fun i => v (-i))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ<VAR>hg : AEStronglyMeasurable g μ<VAR>l : Filter ι<VAR>hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)<GOAL>TendstoInMeasure μ f l g
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ<VAR>hg : AEStronglyMeasurable g μ<VAR>l : Filter ι<VAR>hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)<GOAL>TendstoInMeasure μ (fun i => AEStronglyMeasurable.mk (f i) ⋯) l (AEStronglyMeasurable.mk g hg)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ<VAR>hg : AEStronglyMeasurable g μ<VAR>l : Filter ι<VAR>hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)<GOAL>Tendsto (fun n => eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) l (𝓝 0)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : ι → α → E<VAR>g : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ<VAR>hg : AEStronglyMeasurable g μ<VAR>l : Filter ι<VAR>hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)<VAR>this : (fun n => eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) = fun n => eLpNorm (f n - g) p μ<GOAL>Tendsto (fun n => eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) l (𝓝 0)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>p✝ : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : AddCommGroup P<VAR>inst✝³ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>inst✝² : Module.Finite R M<VAR>p : Ideal R<VAR>inst✝¹ : p.IsPrime<VAR>inst✝ : Subsingleton (LocalizedModule p.primeCompl M)<GOAL>∃ f ∉ p, Subsingleton (LocalizedModule (Submonoid.powers f) M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>p✝ : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : AddCommGroup P<VAR>inst✝³ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>inst✝² : Module.Finite R M<VAR>p : Ideal R<VAR>inst✝¹ : p.IsPrime<VAR>inst✝ : Subsingleton (LocalizedModule p.primeCompl M)<VAR>this : { asIdeal := p, isPrime := ⋯ } ∈ (Module.support R M)ᶜ<GOAL>∃ f ∉ p, Subsingleton (LocalizedModule (Submonoid.powers f) M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>p✝ : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : AddCommGroup P<VAR>inst✝³ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>inst✝² : Module.Finite R M<VAR>p : Ideal R<VAR>inst✝¹ : p.IsPrime<VAR>inst✝ : Subsingleton (LocalizedModule p.primeCompl M)<VAR>this : ∃ i, ∃ (_ : i ∈ ↑(Module.annihilator R M)), { asIdeal := p, isPrime := ⋯ } ∈ (PrimeSpectrum.zeroLocus {i})ᶜ<GOAL>∃ f ∉ p, Subsingleton (LocalizedModule (Submonoid.powers f) M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>p✝ : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : AddCommGroup P<VAR>inst✝³ : Module R P<VAR>f✝ : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>inst✝² : Module.Finite R M<VAR>p : Ideal R<VAR>inst✝¹ : p.IsPrime<VAR>inst✝ : Subsingleton (LocalizedModule p.primeCompl M)<VAR>f : R<VAR>hf : f ∈ ↑(Module.annihilator R M)<VAR>hf' : { asIdeal := p, isPrime := ⋯ } ∈ (PrimeSpectrum.zeroLocus {f})ᶜ<GOAL>∃ f ∉ p, Subsingleton (LocalizedModule (Submonoid.powers f) M)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>E : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : β → E<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>hf : StronglyMeasurable f<GOAL>∫ (x : β), f x ∂(deterministic g hg) a = f (g a)
<VAR>z✝ w✝ : ℍ<VAR>r✝ R : ℝ<VAR>z w : ℍ<VAR>r : ℝ<VAR>this : MetricSpace ℍ := metricSpaceAux<GOAL>cmp (dist z w) r = cmp (dist ↑z ↑(w.center r)) (w.im * Real.sinh r)
<VAR>z✝ w✝ : ℍ<VAR>r✝ R : ℝ<VAR>z w : ℍ<VAR>r : ℝ<VAR>this : MetricSpace ℍ := metricSpaceAux<VAR>hr₀ : r < 0<GOAL>cmp (dist z w) r = cmp (dist ↑z ↑(w.center r)) (w.im * Real.sinh r)
<VAR>z✝ w✝ : ℍ<VAR>r✝ R : ℝ<VAR>z w : ℍ<VAR>r : ℝ<VAR>this : MetricSpace ℍ := metricSpaceAux<VAR>hr₀ : 0 ≤ r<GOAL>cmp (dist z w) r = cmp (dist ↑z ↑(w.center r)) (w.im * Real.sinh r)
<VAR>z✝ w✝ : ℍ<VAR>r✝ R : ℝ<VAR>z w : ℍ<VAR>r : ℝ<VAR>this : MetricSpace ℍ := metricSpaceAux<VAR>hr₀ : 0 ≤ r<VAR>hr₀' : 0 ≤ w.im * Real.sinh r<VAR>hzw₀ : 0 < 2 * z.im * w.im<GOAL>cmp (dist z w) r = cmp (dist ↑z ↑(w.center r)) (w.im * Real.sinh r)
<VAR>z✝ w✝ : ℍ<VAR>r✝ R : ℝ<VAR>z w : ℍ<VAR>r : ℝ<VAR>this : MetricSpace ℍ := metricSpaceAux<VAR>hr₀ : 0 ≤ r<VAR>hr₀' : 0 ≤ w.im * Real.sinh r<VAR>hzw₀ : 0 < 2 * z.im * w.im<GOAL>cmp (Real.cosh (dist z w)) (Real.cosh r) = cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2) ((w.im * Real.sinh r) ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : Ordinal.{u_4} → Ordinal.{u_5}<VAR>H : IsNormal f<VAR>a b : Ordinal.{u_4}<GOAL>f a = f b ↔ a = b
<VAR>q : ℚ<VAR>x y : ℝ<VAR>m : ℤ<VAR>h : Irrational (↑m + x)<GOAL>Irrational x
<VAR>q : ℚ<VAR>x y : ℝ<VAR>m : ℤ<VAR>h : Irrational (↑↑m + x)<GOAL>Irrational x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Iio y) y<GOAL>slope f x y < f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Iio y) y<VAR>u : ℝ<VAR>hxu : x < u<VAR>huy : u < y<GOAL>slope f x y < f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Iio y) y<VAR>u : ℝ<VAR>hxu : x < u<VAR>huy : u < y<VAR>hu : u ∈ S<GOAL>slope f x y < f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Iio y) y<VAR>u : ℝ<VAR>hxu : x < u<VAR>huy : u < y<VAR>hu : u ∈ S<VAR>this : (f x - f y) / (x - y) < (f u - f y) / (u - y)<GOAL>slope f x y < f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Iio y) y<VAR>u : ℝ<VAR>hxu : x < u<VAR>huy : u < y<VAR>hu : u ∈ S<VAR>this : slope f x y < slope f u y<GOAL>slope f x y < f'
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<GOAL>(refl X ≪≫ α).hom = α.hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝⁴ : NonUnitalSemiring α<VAR>inst✝³ : StarRing α<VAR>inst✝² : NonUnitalSemiring β<VAR>inst✝¹ : StarRing β<VAR>inst✝ : Fintype m<VAR>A : Matrix m n α<GOAL>(Aᴴ * A).IsHermitian
<VAR>z✝ w : ℍ<VAR>r R : ℝ<VAR>z : ℍ<GOAL>(z.center 0).im = z.im
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<GOAL>S.Exact ↔ LinearMap.ker S.g ≤ LinearMap.range S.f
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<GOAL>(∀ (x₂ : ↑S.X₂), S.g x₂ = 0 → ∃ x₁, S.f x₁ = x₂) ↔ LinearMap.ker S.g ≤ LinearMap.range S.f
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℕ<GOAL>(A ^ ↑n)ᵀ = Aᵀ ^ ↑n
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>n : ℕ<GOAL>(A ^ -[n+1])ᵀ = Aᵀ ^ -[n+1]
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>w✝¹ : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p e w✝¹<VAR>w✝ : ℝ≥0∞<VAR>hg : HasFPowerSeriesOnBall g q e w✝<GOAL>HasFPowerSeriesAt (fun x => (f x, g x)) (p.prod q) e
<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>hs : IsCompact s<VAR>t : Set Y<VAR>ht : IsCompact t<VAR>n : Set (X × Y)<VAR>hn : IsOpen n<VAR>hp : s ×ˢ t ⊆ n<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
<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>hs : IsCompact s<VAR>t : Set Y<VAR>ht : IsCompact t<VAR>n : Set (X × Y)<VAR>hn : IsOpen n<VAR>hp : ∃ i, ((IsOpen i.1 ∧ s ⊆ i.1) ∧ IsOpen i.2 ∧ t ⊆ i.2) ∧ i.1 ×ˢ i.2 ⊆ n<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>δ : α → Sort u_2<VAR>m✝ : Multiset α<VAR>a✝ a a' : α<VAR>b : δ a<VAR>b' : δ a'<VAR>m : Multiset α<VAR>f : (a : α) → a ∈ m → δ a<VAR>h : a ≠ a'<GOAL>HEq (cons (a' ::ₘ m) a b (cons m a' b' f)) (cons (a ::ₘ m) a' b' (cons m a b f))
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>δ : α → Sort u_2<VAR>m✝ : Multiset α<VAR>a✝ a a' : α<VAR>b : δ a<VAR>b' : δ a'<VAR>m : Multiset α<VAR>f : (a : α) → a ∈ m → δ a<VAR>h : a ≠ a'<GOAL>∀ (a_1 a'_1 : α), HEq a_1 a'_1 → HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a_1) (cons (a ::ₘ m) a' b' (cons m a b f) a'_1)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>δ : α → Sort u_2<VAR>m✝ : Multiset α<VAR>a✝ a a' : α<VAR>b : δ a<VAR>b' : δ a'<VAR>m : Multiset α<VAR>f : (a : α) → a ∈ m → δ a<VAR>h : a ≠ a'<GOAL>∀ (a_1 a'_1 : α), a_1 = a'_1 → HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a_1) (cons (a ::ₘ m) a' b' (cons m a b f) a'_1)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>δ : α → Sort u_2<VAR>m✝ : Multiset α<VAR>a✝ a a' : α<VAR>b : δ a<VAR>b' : δ a'<VAR>m : Multiset α<VAR>f : (a : α) → a ∈ m → δ a<VAR>h : a ≠ a'<VAR>a'' : α<GOAL>HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'') (cons (a ::ₘ m) a' b' (cons m a b f) a'')
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>δ : α → Sort u_2<VAR>m✝ : Multiset α<VAR>a✝ a a' : α<VAR>b : δ a<VAR>b' : δ a'<VAR>m : Multiset α<VAR>f : (a : α) → a ∈ m → δ a<VAR>h : a ≠ a'<VAR>a'' : α<VAR>ha₁ : a'' ∈ a ::ₘ a' ::ₘ m<VAR>ha₂ : a'' ∈ a' ::ₘ a ::ₘ m<VAR>x✝ : HEq ha₁ ha₂<GOAL>HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>δ : α → Sort u_2<VAR>m✝ : Multiset α<VAR>a✝ a a' : α<VAR>b : δ a<VAR>b' : δ a'<VAR>m : Multiset α<VAR>f : (a : α) → a ∈ m → δ a<VAR>h : a ≠ a'<VAR>a'' : α<VAR>ha₁ : a'' ∈ a ::ₘ a' ::ₘ m<VAR>ha₂ : a'' ∈ a' ::ₘ a ::ₘ m<VAR>x✝ : HEq ha₁ ha₂<VAR>h₁ : a'' ≠ a<GOAL>HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>δ : α → Sort u_2<VAR>m✝ : Multiset α<VAR>a a' : α<VAR>b' : δ a'<VAR>m : Multiset α<VAR>f : (a : α) → a ∈ m → δ a<VAR>a'' : α<VAR>b : δ a''<VAR>h : a'' ≠ a'<VAR>ha₁ : a'' ∈ a'' ::ₘ a' ::ₘ m<VAR>ha₂ : a'' ∈ a' ::ₘ a'' ::ₘ m<VAR>x✝ : HEq ha₁ ha₂<GOAL>HEq (cons (a' ::ₘ m) a'' b (cons m a' b' f) a'' ha₁) (cons (a'' ::ₘ m) a' b' (cons m a'' b f) a'' ha₂)