ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x y : M<GOAL>Q.IsOrtho x y ↔ Q.IsOrtho y x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Module R M<VAR>tR : IsTorsion R<VAR>f : M<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hn : n • 1 = 0<GOAL>∃ n, 0 < n ∧ n • f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<GOAL>Nat.Subtype.toFunAux (ofNat s 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<GOAL>∀ (x : ℕ), x ∉ filter (fun x => x ∈ s) (range ↑(ofNat s 0))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>n : ℕ<VAR>hn : n ∈ filter (fun x => x ∈ s) (range ↑(ofNat s 0))<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>n : ℕ<VAR>hn : n < ↑⊥ ∧ n ∈ s<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>n : ℕ<VAR>ih : Nat.Subtype.toFunAux (ofNat s n) = n<VAR>h₁ : ↑(ofNat s n) ∉ filter (fun x => x ∈ s) (range ↑(ofNat s n))<VAR>h₂ : filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) = insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))<GOAL>Nat.Subtype.toFunAux (ofNat s (n + 1)) = n + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set ℕ<VAR>inst✝¹ : Infinite ↑s<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>n : ℕ<VAR>h₁ : ↑(ofNat s n) ∉ filter (fun x => x ∈ s) (range ↑(ofNat s n))<VAR>h₂ : filter (fun x => x ∈ s) (range ↑(succ (ofNat s n))) = insert (↑(ofNat s n)) (filter (fun x => x ∈ s) (range ↑(ofNat s n)))<VAR>ih : (filter (fun x => x ∈ s) (range ↑(ofNat s n))).card = n<GOAL>(filter (fun x => x ∈ s) (range ↑(succ (ofNat s n)))).card = n + 1
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>(↑(hC.diffFinset₀ hs hI)).PairwiseDisjoint id
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Monoid G<GOAL>(forget₂ (Rep k G) (ModuleCat k)).map ((εToSingle₀ k G).f 0) ≫ ((HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ) 0).hom.app (Rep.trivial k G k)).f 0 = (forget₂ToModuleCatHomotopyEquiv k G).hom.f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s t : Set α<VAR>f g : α → M<VAR>a : α<GOAL>s.mulIndicator f = f ↔ mulSupport f ⊆ s
<VAR>α β : Type<VAR>n : ℕ<VAR>S : Set (α ⊕ Fin2 0 → ℕ)<VAR>d : Dioph S<VAR>f : Vector3 ((α → ℕ) → ℕ) 0<VAR>x✝ : VectorAllP DiophFn f<VAR>v : α → ℕ<GOAL>v ∘ (id ⊗ elim0) ∈ S ↔ (v ⊗ fun i => f i v) ∈ S
<VAR>α β : Type<VAR>n : ℕ<VAR>S : Set (α ⊕ Fin2 0 → ℕ)<VAR>d : Dioph S<VAR>f : Vector3 ((α → ℕ) → ℕ) 0<VAR>x✝ : VectorAllP DiophFn f<VAR>v : α → ℕ<GOAL>v ∘ (id ⊗ elim0) = v ⊗ fun i => f i v
<VAR>α β : Type<VAR>n✝ n : ℕ<VAR>S : Set (α ⊕ Fin2 n.succ → ℕ)<VAR>d : Dioph S<VAR>f✝ : Vector3 ((α → ℕ) → ℕ) n.succ<VAR>f : (α → ℕ) → ℕ<VAR>fl : Vector3 ((α → ℕ) → ℕ) n<GOAL>VectorAllP DiophFn (f :: fl) → Dioph {v | (v ⊗ fun i => (f :: fl) i v) ∈ S}
<VAR>α β : Type<VAR>n✝ n : ℕ<VAR>S : Set (α ⊕ Fin2 n.succ → ℕ)<VAR>d : Dioph S<VAR>f✝ : Vector3 ((α → ℕ) → ℕ) n.succ<VAR>f : (α → ℕ) → ℕ<VAR>fl : Vector3 ((α → ℕ) → ℕ) n<GOAL>DiophFn f → VectorAllP DiophFn fl → Dioph {v | (v ⊗ fun i => (f :: fl) i v) ∈ S}
<VAR>R✝ : Type u_1<VAR>inst✝¹⁴ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝¹ : Type u_2<VAR>inst✝¹³ : AddCommGroup M✝¹<VAR>inst✝¹² : Module R✝ M✝¹<VAR>N✝ : Type u_3<VAR>inst✝¹¹ : AddCommGroup N✝<VAR>inst✝¹⁰ : Module R✝ N✝<VAR>R : Type u<VAR>inst✝⁹ : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : Module R M✝<VAR>inst✝⁶ : IsNoetherianRing R<VAR>M : Type u<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>f : M →ₗ[R] N<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Finite R N<GOAL>AlgebraTensorModule.map LinearMap.id f = ↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ map I f ∘ₗ ↑(ofTensorProductEquivOfFiniteNoetherian I M)
<VAR>R✝ : Type u_1<VAR>inst✝¹⁴ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝¹ : Type u_2<VAR>inst✝¹³ : AddCommGroup M✝¹<VAR>inst✝¹² : Module R✝ M✝¹<VAR>N✝ : Type u_3<VAR>inst✝¹¹ : AddCommGroup N✝<VAR>inst✝¹⁰ : Module R✝ N✝<VAR>R : Type u<VAR>inst✝⁹ : CommRing R<VAR>I : Ideal R<VAR>M✝ : Type u<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : Module R M✝<VAR>inst✝⁶ : IsNoetherianRing R<VAR>M : Type u<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>f : M →ₗ[R] N<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Finite R N<GOAL>AlgebraTensorModule.map LinearMap.id f = ↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f
<VAR>α : Type u_1<VAR>inst✝ : CommSemigroup α<VAR>s t : Set α<VAR>a : α<VAR>x : α × α<GOAL>x.2 ∈ s ∧ x.1 ∈ t ∧ x.2 * x.1 = a ↔ x ∈ t.mulAntidiagonal s a
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIocDiv hp a (b - m • p) = toIocDiv hp a b - m
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedRing 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p : Seminorm 𝕝 E<VAR>hp : ContinuousAt (⇑p) 0<VAR>this : UniformSpace E := TopologicalAddGroup.toUniformSpace E<GOAL>Continuous ⇑p
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedRing 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p : Seminorm 𝕝 E<VAR>hp : ContinuousAt (⇑p) 0<VAR>this✝ : UniformSpace E := TopologicalAddGroup.toUniformSpace E<VAR>this : UniformAddGroup E<GOAL>Continuous ⇑p
<VAR>ι : Type u<VAR>X : Type v<VAR>Y : Type w<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ParacompactSpace X<VAR>u : ι → Set X<VAR>uo : ∀ (a : ι), IsOpen (u a)<VAR>uc : ⋃ i, u i = univ<GOAL>∃ v, (∀ (a : ι), IsOpen (v a)) ∧ ⋃ i, v i = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
<VAR>ι : Type u<VAR>X : Type v<VAR>Y : Type w<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ParacompactSpace X<VAR>u : ι → Set X<VAR>uo : ∀ (a : ι), IsOpen (u a)<VAR>uc : ⋃ i, u i = univ<VAR>this : ∃ β t, (∀ (b : β), IsOpen (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ (fun r => ↑r) a<GOAL>∃ v, (∀ (a : ι), IsOpen (v a)) ∧ ⋃ i, v i = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
<VAR>ι : Type u<VAR>X : Type v<VAR>Y : Type w<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ParacompactSpace X<VAR>u : ι → Set X<VAR>uo : ∀ (a : ι), IsOpen (u a)<VAR>uc : ⋃ i, u i = univ<VAR>this : ∃ β t, (∀ (b : β), IsOpen (t b)) ∧ (∀ (x : X), ∃ i, x ∈ t i) ∧ LocallyFinite t ∧ ∀ (b : β), ∃ i, t b ⊆ u i<GOAL>∃ v, (∀ (a : ι), IsOpen (v a)) ∧ ⋃ i, v i = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
<VAR>b n : ℕ<GOAL>log b n = 0 ↔ n < b ∨ b ≤ 1
<VAR>b n : ℕ<GOAL>b ≤ n ∧ 1 < b → log b (n / b) + 1 = 0 ↔ n < b ∨ b ≤ 1
<VAR>F : Type u<VAR>inst✝² : Field F<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>hf : f ≠ 0<VAR>h : Splits (algebraMap F K) f<GOAL>(f.aroots K).Nodup ↔ f.Separable
<VAR>F : Type u<VAR>inst✝² : Field F<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>hf : f ≠ 0<VAR>h : Splits (RingHom.id K) (map (algebraMap F K) f)<GOAL>(f.aroots K).Nodup ↔ f.Separable
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R M<VAR>x : L<GOAL>_root_.IsNilpotent ((toEnd R L ↥↑(weightSpace M 0)) x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>n : ℕ<GOAL>Conservative f^[n + 1] μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>n : ℕ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs0 : μ s ≠ 0<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>n : ℕ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs0 : μ s ≠ 0<VAR>x : α<VAR>left✝ : x ∈ s<VAR>hx : ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>n : ℕ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs0 : μ s ≠ 0<VAR>x : α<VAR>left✝ : x ∈ s<VAR>hx : {n | f^[n] x ∈ s}.Infinite<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>n : ℕ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs0 : μ s ≠ 0<VAR>x : α<VAR>left✝ : x ∈ s<VAR>hx : {n | f^[n] x ∈ s}.Infinite<VAR>k : ℕ<VAR>hk : k ∈ {n | f^[n] x ∈ s}<VAR>l : ℕ<VAR>hl : l ∈ {n | f^[n] x ∈ s}<VAR>hkl : k < l<VAR>hn : k ≡ l [MOD n.succ]<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>n : ℕ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs0 : μ s ≠ 0<VAR>x : α<VAR>left✝ : x ∈ s<VAR>hx : {n | f^[n] x ∈ s}.Infinite<VAR>k : ℕ<VAR>hk : k ∈ {n | f^[n] x ∈ s}<VAR>l : ℕ<VAR>hl : l ∈ {n | f^[n] x ∈ s}<VAR>hkl : k < l<VAR>hn : k ≡ l [MOD n.succ]<VAR>m : ℕ := (l - k) / (n + 1)<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>n : ℕ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs0 : μ s ≠ 0<VAR>x : α<VAR>left✝ : x ∈ s<VAR>hx : {n | f^[n] x ∈ s}.Infinite<VAR>k : ℕ<VAR>hk : k ∈ {n | f^[n] x ∈ s}<VAR>l : ℕ<VAR>hl : l ∈ {n | f^[n] x ∈ s}<VAR>hkl : k < l<VAR>hn : k ≡ l [MOD n.succ]<VAR>m : ℕ := (l - k) / (n + 1)<VAR>this : (n + 1) * m = l - k<GOAL>∃ x ∈ s, ∃ m, m ≠ 0 ∧ f^[n + 1]^[m] x ∈ s
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T1Space X<VAR>inst✝ : T35Space X<VAR>a b : X<VAR>hab : stoneCechUnit a = stoneCechUnit b<GOAL>a = b
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T1Space X<VAR>inst✝ : T35Space X<VAR>a b : X<VAR>hab : ¬a = b<GOAL>¬stoneCechUnit a = stoneCechUnit b
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T1Space X<VAR>inst✝ : T35Space X<VAR>a b : X<VAR>hab : ¬a = b<VAR>f : X → ↑I<VAR>fc : f ∈ Continuous<VAR>fab : f a ≠ f b<GOAL>¬stoneCechUnit a = stoneCechUnit 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>l : Subspace η α ι<VAR>x : η → α<VAR>i : ι<VAR>a : α<VAR>e : η<VAR>η' : Type u_9<VAR>α' : Type u_10<VAR>ι' : Type u_11<VAR>eη : η ≃ η'<VAR>eα : α ≃ α'<VAR>eι : ι ≃ ι'<VAR>C : (ι' → α') → κ<GOAL>IsMono C (l.reindex eη eα eι) ↔ IsMono (fun x => C (⇑eα ∘ x ∘ ⇑eι.symm)) l
<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>l : Subspace η α ι<VAR>x : η → α<VAR>i : ι<VAR>a : α<VAR>e : η<VAR>η' : Type u_9<VAR>α' : Type u_10<VAR>ι' : Type u_11<VAR>eη : η ≃ η'<VAR>eα : α ≃ α'<VAR>eι : ι ≃ ι'<VAR>C : (ι' → α') → κ<GOAL>(∃ c, ∀ (x : η' → α'), (C fun x_1 => eα (Sum.elim id (⇑eα.symm ∘ x ∘ ⇑eη) (l.idxFun (eι.symm x_1)))) = c) ↔ ∃ c, ∀ (x : η → α), C (⇑eα ∘ ↑l x ∘ ⇑eι.symm) = c
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3<GOAL>W.dblXYZ P = W.dblU P • ![1, 1, 0]
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X₁ : ModuleCat R<VAR>X₂ : ModuleCat R<VAR>X₃ : ModuleCat R<VAR>Y₁ : ModuleCat R<VAR>Y₂ : ModuleCat R<VAR>Y₃ : ModuleCat R<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>f₃ : X₃ ⟶ Y₃<GOAL>tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom = (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>f f' : ℕ → α → β<VAR>g g' : α → β<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] f' n<VAR>hgg' : g =ᶠ[ae μ] g'<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun n => f' n x) atTop (𝓝 (g' x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>f f' : ℕ → α → β<VAR>g g' : α → β<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] f' n<VAR>hgg' : g =ᶠ[ae μ] g'<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hff'' : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), f i x = f' i x<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun n => f' n x) atTop (𝓝 (g' x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>f f' : ℕ → α → β<VAR>g g' : α → β<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] f' n<VAR>hgg' : g =ᶠ[ae μ] g'<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hff'' : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), f i x = f' i x<VAR>x : α<VAR>hff'x : ∀ (i : ℕ), f i x = f' i x<VAR>hgg'x : g x = g' x<VAR>hfgx : Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>Tendsto (fun n => f' n x) atTop (𝓝 (g' x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>f f' : ℕ → α → β<VAR>g g' : α → β<VAR>hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] f' n<VAR>hgg' : g =ᶠ[ae μ] g'<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hff'' : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), f i x = f' i x<VAR>x : α<VAR>hff'x : ∀ (i : ℕ), f i x = f' i x<VAR>hgg'x : g x = g' x<VAR>hfgx : Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>Tendsto (fun x_1 => f x_1 x) atTop (𝓝 (g' x))
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>n : ℤ<GOAL>n + 0 = n
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>n : ℤ<GOAL>((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K).f n = (XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>n : ℤ<VAR>this : IsIso (((shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n)<GOAL>((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K).f n = (XIsoOfEq K ⋯).hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>n : ℤ<VAR>this : IsIso (((shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n)<GOAL>𝟙 (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 0).obj K).X n) = (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra R B<VAR>z : ℤ<GOAL>↑z = 1 ⊗ₜ[R] ↑z
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivAt f f' x<VAR>hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖<GOAL>∀ᶠ (z : E) in 𝓝[≠] x, f z ≠ f x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : ‖a.c i‖ ≤ 2<VAR>hj : 2 < ‖a.c j‖<GOAL>1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : ‖a.c i‖ ≤ 2<VAR>hj : 2 < ‖a.c j‖<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<GOAL>1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : ‖a.c i‖ ≤ 2<VAR>hj : 2 < ‖a.c j‖<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>D : 0 ≤ 1 - δ / 4<GOAL>1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : ‖a.c i‖ ≤ 2<VAR>hj : 2 < ‖a.c j‖<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>D : 0 ≤ 1 - δ / 4<VAR>hcrj : ‖a.c j‖ ≤ a.r j + 1<GOAL>1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : ‖a.c i‖ ≤ 2<VAR>hj : 2 < ‖a.c j‖<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>D : 0 ≤ 1 - δ / 4<VAR>hcrj : ‖a.c j‖ ≤ a.r j + 1<VAR>I : a.r i ≤ 2<GOAL>1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : ‖a.c i‖ ≤ 2<VAR>hj : 2 < ‖a.c j‖<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>D : 0 ≤ 1 - δ / 4<VAR>hcrj : ‖a.c j‖ ≤ a.r j + 1<VAR>I : a.r i ≤ 2<VAR>J : (1 - δ / 4) * τ ≤ 1<GOAL>1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : ‖a.c i‖ ≤ 2<VAR>hj : 2 < ‖a.c j‖<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>D : 0 ≤ 1 - δ / 4<VAR>hcrj : ‖a.c j‖ ≤ a.r j + 1<VAR>I : a.r i ≤ 2<VAR>J : (1 - δ / 4) * τ ≤ 1<VAR>A : a.r j - δ ≤ ‖a.c i - a.c j‖<VAR>d : E := (2 / ‖a.c j‖) • a.c j<VAR>hd : d = (2 / ‖a.c j‖) • a.c j<GOAL>1 - δ ≤ ‖a.c i - d‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig E N τ<VAR>lastc : a.c (last N) = 0<VAR>lastr : a.r (last N) = 1<VAR>hτ : 1 ≤ τ<VAR>δ : ℝ<VAR>hδ1 : τ ≤ 1 + δ / 4<VAR>hδ2 : δ ≤ 1<VAR>i j : Fin N.succ<VAR>inej : i ≠ j<VAR>hi : ‖a.c i‖ ≤ 2<VAR>hj : 2 < ‖a.c j‖<VAR>ah : Pairwise fun i j => a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j<VAR>δnonneg : 0 ≤ δ<VAR>D : 0 ≤ 1 - δ / 4<VAR>hcrj : ‖a.c j‖ ≤ a.r j + 1<VAR>I : a.r i ≤ 2<VAR>J : (1 - δ / 4) * τ ≤ 1<VAR>A : a.r j - δ ≤ ‖a.c i - a.c j‖<VAR>d : E := (2 / ‖a.c j‖) • a.c j<VAR>hd : d = (2 / ‖a.c j‖) • a.c j<VAR>this : a.r j - δ ≤ ‖a.c i - d‖ + (a.r j - 1)<GOAL>1 - δ ≤ ‖a.c i - d‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<GOAL>Tendsto (fun s => s • P.Λ s) (𝓝[≠] 0) (𝓝 (-P.f₀))
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<GOAL>Tendsto (fun s => s • P.Λ₀ s - s • (1 / s) • P.f₀ - s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0) (𝓝 (0 • P.Λ₀ 0 - P.f₀ - 0))
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<GOAL>Tendsto (fun s => s • P.Λ₀ s) (𝓝 0) (𝓝 (0 • P.Λ₀ 0))
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<GOAL>Tendsto (fun s => s • (1 / s) • P.f₀) (𝓝[≠] 0) (𝓝 P.f₀)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<GOAL>Tendsto (fun s => s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0) (𝓝 0)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : Monoid G<GOAL>¬IsTorsionFree G ↔ ∃ g, g ≠ 1 ∧ IsOfFinOrder g
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set (PrimeSpectrum R)<GOAL>vanishingIdeal s = ⊤ ↔ s = ∅
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommRing P<VAR>s : Set R<GOAL>coeSubmodule S (Ideal.span s) = Submodule.span R (⇑(algebraMap R S) '' s)
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommRing P<VAR>s : Set R<GOAL>Submodule.span R (⇑(Algebra.linearMap R S) '' s) = Submodule.span R (⇑(algebraMap R S) '' s)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>h : c ≠ 0<VAR>hab : a * c ≤ b * c<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>a p : Associates α<VAR>hp : Irreducible p<VAR>inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)<VAR>n : ℕ<VAR>h : a ∣ p ^ n<GOAL>a = p ^ Nat.find ⋯