ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>H1 : ∀ x ∈ s, infDist x t ≤ r<VAR>H2 : ∀ x ∈ t, infDist x s ≤ r<VAR>h1 : ¬hausdorffEdist s t = ⊤<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>this : hausdorffEdist s t ≤ ENNReal.ofReal r<GOAL>hausdorffDist s t ≤ r
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>hp : 0 < p.radius<GOAL>0 < (p.rightInv i).radius
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>hp : 0 < p.radius<VAR>C r : ℝ<VAR>Cpos : 0 < C<VAR>rpos : 0 < r<VAR>ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<GOAL>0 < (p.rightInv i).radius
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>hp : 0 < p.radius<VAR>C r : ℝ<VAR>Cpos : 0 < C<VAR>rpos : 0 < r<VAR>ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<GOAL>0 < (p.rightInv i).radius
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>hp : 0 < p.radius<VAR>C r : ℝ<VAR>Cpos : 0 < C<VAR>rpos : 0 < r<VAR>ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<VAR>a : ℝ<VAR>apos : 0 < a<VAR>ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1<VAR>ha2 : r * (I + 1) * a ≤ 1 / 2<GOAL>0 < (p.rightInv i).radius
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>hp : 0 < p.radius<VAR>C r : ℝ<VAR>Cpos : 0 < C<VAR>rpos : 0 < r<VAR>ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<VAR>a : ℝ<VAR>apos : 0 < a<VAR>ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1<VAR>ha2 : r * (I + 1) * a ≤ 1 / 2<VAR>S : ℕ → ℝ := fun n => ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i k‖<VAR>IRec : ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a<VAR>a' : NNReal := ⟨a, ⋯⟩<GOAL>0 < (p.rightInv i).radius
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>hp : 0 < p.radius<VAR>C r : ℝ<VAR>Cpos : 0 < C<VAR>rpos : 0 < r<VAR>ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<VAR>a : ℝ<VAR>apos : 0 < a<VAR>ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1<VAR>ha2 : r * (I + 1) * a ≤ 1 / 2<VAR>S : ℕ → ℝ := fun n => ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i k‖<VAR>IRec : ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a<VAR>a' : NNReal := ⟨a, ⋯⟩<GOAL>↑a' ≤ (p.rightInv i).radius
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>hp : 0 < p.radius<VAR>C r : ℝ<VAR>Cpos : 0 < C<VAR>rpos : 0 < r<VAR>ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<VAR>I : ℝ := ‖↑i.symm‖<VAR>a : ℝ<VAR>apos : 0 < a<VAR>ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1<VAR>ha2 : r * (I + 1) * a ≤ 1 / 2<VAR>S : ℕ → ℝ := fun n => ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i k‖<VAR>IRec : ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a<VAR>a' : NNReal := ⟨a, ⋯⟩<VAR>n : ℕ<GOAL>‖p.rightInv i n‖ * ↑a' ^ n ≤ (I + 1) * a
<GOAL>2 * 0 ^ 2 - 1 = -1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q p : R[X]<VAR>hp : p.Monic<VAR>hp1 : p ≠ 1<GOAL>Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q p : R[X]<VAR>hp : p.Monic<VAR>hp1 : p ≠ 1<GOAL>(∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b c : σ<VAR>h₁ : Reaches₁ f a c<VAR>h₂ : b ∈ f a<GOAL>Reaches f b c
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b c : σ<VAR>h₁ : Reaches₁ f a c<VAR>h₂ : b ∈ f a<VAR>b' : σ<VAR>hab : b' ∈ f a<VAR>hbc : ReflTransGen (fun a b => b ∈ f a) b' c<GOAL>Reaches f b c
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b c : σ<VAR>h₁ : Reaches₁ f a c<VAR>h₂ hab : b ∈ f a<VAR>hbc : ReflTransGen (fun a b => b ∈ f a) b c<GOAL>Reaches f b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>hst : Disjoint s t<VAR>hs : (s ∩ mulSupport f).Finite<VAR>ht : (t ∩ mulSupport f).Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : LaxMonoidalFunctor C D<VAR>A : Mon_ C<GOAL>(F.ε ≫ F.map A.one) ▷ F.obj A.X ≫ F.μ A.X A.X ≫ F.map A.mul = (λ_ (F.obj A.X)).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : LaxMonoidalFunctor C D<VAR>A : Mon_ C<GOAL>F.ε ▷ F.obj A.X ≫ F.μ (𝟙_ C) A.X ≫ F.map (A.one ▷ A.X) ≫ F.map A.mul = F.ε ▷ F.obj A.X ≫ F.μ (𝟙_ C) A.X ≫ F.map (λ_ A.X).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : LaxMonoidalFunctor C D<VAR>A : Mon_ C<GOAL>F.obj A.X ◁ (F.ε ≫ F.map A.one) ≫ F.μ A.X A.X ≫ F.map A.mul = (ρ_ (F.obj A.X)).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : LaxMonoidalFunctor C D<VAR>A : Mon_ C<GOAL>F.obj A.X ◁ F.ε ≫ F.μ A.X (𝟙_ C) ≫ F.map (A.X ◁ A.one) ≫ F.map A.mul = F.obj A.X ◁ F.ε ≫ F.μ A.X (𝟙_ C) ≫ F.map (ρ_ A.X).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : LaxMonoidalFunctor C D<VAR>A : Mon_ C<GOAL>(F.μ A.X A.X ≫ F.map A.mul) ▷ F.obj A.X ≫ F.μ A.X A.X ≫ F.map A.mul = (α_ (F.obj A.X) (F.obj A.X) (F.obj A.X)).hom ≫ F.obj A.X ◁ (F.μ A.X A.X ≫ F.map A.mul) ≫ F.μ A.X A.X ≫ F.map A.mul
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : LaxMonoidalFunctor C D<VAR>A : Mon_ C<GOAL>F.μ A.X A.X ▷ F.obj A.X ≫ F.μ (A.X ⊗ A.X) A.X ≫ F.map (A.mul ▷ A.X) ≫ F.map A.mul = (α_ (F.obj A.X) (F.obj A.X) (F.obj A.X)).hom ≫ F.obj A.X ◁ F.μ A.X A.X ≫ F.μ A.X (A.X ⊗ A.X) ≫ F.map (A.X ◁ A.mul) ≫ F.map A.mul
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : LaxMonoidalFunctor C D<VAR>A : Mon_ C<GOAL>F.μ A.X A.X ▷ F.obj A.X ≫ F.μ (A.X ⊗ A.X) A.X ≫ F.map ((α_ A.X A.X A.X).hom ≫ A.X ◁ A.mul ≫ A.mul) = (α_ (F.obj A.X) (F.obj A.X) (F.obj A.X)).hom ≫ F.obj A.X ◁ F.μ A.X A.X ≫ F.μ A.X (A.X ⊗ A.X) ≫ F.map (A.X ◁ A.mul) ≫ F.map A.mul
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : LaxMonoidalFunctor C D<VAR>X✝ Y✝ : Mon_ C<VAR>f : X✝ ⟶ Y✝<GOAL>(F.ε ≫ F.map X✝.one) ≫ F.map f.hom = F.ε ≫ F.map Y✝.one
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : LaxMonoidalFunctor C D<VAR>X✝ Y✝ : Mon_ C<VAR>f : X✝ ⟶ Y✝<GOAL>(F.μ X✝.X X✝.X ≫ F.map X✝.mul) ≫ F.map f.hom = (F.map f.hom ⊗ F.map f.hom) ≫ F.μ Y✝.X Y✝.X ≫ F.map Y✝.mul
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ h : IsPrimitiveRoot ζ k<VAR>i j : ℕ<VAR>hi : i < k<VAR>hj : j < k<VAR>H : ζ ^ i = ζ ^ j<VAR>hij : i ≤ j<GOAL>i = j
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ h : IsPrimitiveRoot ζ k<VAR>i j : ℕ<VAR>hi : i < k<VAR>hj : j < k<VAR>H : ζ ^ i = ζ ^ j<VAR>hij : i ≤ j<GOAL>j ≤ i
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ h : IsPrimitiveRoot ζ k<VAR>i j : ℕ<VAR>hi : i < k<VAR>hj : j < k<VAR>H : ζ ^ i = ζ ^ j<VAR>hij : i ≤ j<GOAL>j - i = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ h : IsPrimitiveRoot ζ k<VAR>i j : ℕ<VAR>hi : i < k<VAR>hj : j < k<VAR>H : ζ ^ i = ζ ^ j<VAR>hij : i ≤ j<GOAL>k ∣ j - i
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ h : IsPrimitiveRoot ζ k<VAR>i j : ℕ<VAR>hi : i < k<VAR>hj : j < k<VAR>H : ζ ^ i = ζ ^ j<VAR>hij : i ≤ j<GOAL>ζ ^ (j - i) = 1
<VAR>K : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : Module K V₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module K V₂<VAR>inst✝³ : Fintype ι₁<VAR>inst✝² : Fintype ι₂<VAR>inst✝¹ : DecidableEq ι₁<VAR>inst✝ : DecidableEq ι₂<VAR>B₁ : Basis ι₁ K V₁<VAR>B₂ : Basis ι₂ K V₂<VAR>u : V₁ →ₗ[K] V₂<VAR>i : ι₁<VAR>j : ι₂<GOAL>(toMatrix B₂.dualBasis B₁.dualBasis) (Module.Dual.transpose u) i j = ((toMatrix B₁ B₂) u)ᵀ i j
<VAR>x y : ℝ<GOAL>√x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2
<VAR>x y : ℝ<GOAL>0 ≤ y → (√x ≤ y ↔ x ≤ y ^ 2)
<VAR>R✝ S : Type u<VAR>M✝ : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R✝<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : AddCommGroup M'✝<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R✝ M✝<VAR>inst✝⁴ : Module R✝ M'✝<VAR>inst✝³ : Module R✝ M₁<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>M' : Submodule R M<VAR>hN : M' ≤ torsion R M<VAR>a✝ : Nontrivial R<GOAL>Module.rank R M ≤ Module.rank R (M ⧸ M')
<VAR>R✝ S : Type u<VAR>M✝ : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R✝<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : AddCommGroup M'✝<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R✝ M✝<VAR>inst✝⁴ : Module R✝ M'✝<VAR>inst✝³ : Module R✝ M₁<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>M' : Submodule R M<VAR>hN : M' ≤ torsion R M<VAR>a✝ : Nontrivial R<GOAL>⨆ ι, #↑↑ι ≤ Module.rank R (M ⧸ M')
<VAR>R✝ S : Type u<VAR>M✝ : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R✝<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : AddCommGroup M'✝<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R✝ M✝<VAR>inst✝⁴ : Module R✝ M'✝<VAR>inst✝³ : Module R✝ M₁<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>M' : Submodule R M<VAR>hN : M' ≤ torsion R M<VAR>a✝ : Nontrivial R<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<GOAL>⨆ ι, #↑↑ι ≤ Module.rank R (M ⧸ M')
<VAR>R✝ S : Type u<VAR>M✝ : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R✝<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : AddCommGroup M'✝<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R✝ M✝<VAR>inst✝⁴ : Module R✝ M'✝<VAR>inst✝³ : Module R✝ M₁<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>M' : Submodule R M<VAR>hN : M' ≤ torsion R M<VAR>a✝ : Nontrivial R<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>x✝ : { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>s : Set M<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<GOAL>LinearIndependent R fun (x : ↑↑⟨s, hs⟩) => M'.mkQ ↑x
<VAR>R✝ S : Type u<VAR>M✝ : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R✝<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : AddCommGroup M'✝<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R✝ M✝<VAR>inst✝⁴ : Module R✝ M'✝<VAR>inst✝³ : Module R✝ M₁<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>M' : Submodule R M<VAR>hN : M' ≤ torsion R M<VAR>a✝ : Nontrivial R<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>x✝ : { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>s : Set M<VAR>hs✝ : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>hs : ∀ (s_1 : Finset { x // x ∈ s }) (g : { x // x ∈ s } → R), ∑ i ∈ s_1, g i • ↑i = 0 → ∀ i ∈ s_1, g i = 0<GOAL>∀ (s_1 : Finset ↑↑⟨s, hs✝⟩) (g : ↑↑⟨s, hs✝⟩ → R), ∑ i ∈ s_1, g i • M'.mkQ ↑i = 0 → ∀ i ∈ s_1, g i = 0
<VAR>R✝ S : Type u<VAR>M✝ : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R✝<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : AddCommGroup M'✝<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R✝ M✝<VAR>inst✝⁴ : Module R✝ M'✝<VAR>inst✝³ : Module R✝ M₁<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>M' : Submodule R M<VAR>hN : M' ≤ torsion R M<VAR>a✝ : Nontrivial R<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>x✝ : { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>s : Set M<VAR>hs✝ : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>hs : ∀ (s_1 : Finset { x // x ∈ s }) (g : { x // x ∈ s } → R), ∑ i ∈ s_1, g i • ↑i = 0 → ∀ i ∈ s_1, g i = 0<GOAL>∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ x ∈ s_1, g x • ↑x ∈ M' → ∀ i ∈ s_1, g i = 0
<VAR>R✝ S : Type u<VAR>M✝ : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R✝<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : AddCommGroup M'✝<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R✝ M✝<VAR>inst✝⁴ : Module R✝ M'✝<VAR>inst✝³ : Module R✝ M₁<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>M' : Submodule R M<VAR>hN : M' ≤ torsion R M<VAR>a✝ : Nontrivial R<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>x✝ : { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>s : Set M<VAR>hs✝ : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>hs : ∀ (s_1 : Finset { x // x ∈ s }) (g : { x // x ∈ s } → R), ∑ i ∈ s_1, g i • ↑i = 0 → ∀ i ∈ s_1, g i = 0<VAR>t : Finset ↑s<VAR>g : ↑s → R<VAR>hg✝ : ∑ x ∈ t, g x • ↑x ∈ M'<VAR>i : ↑s<VAR>hi : i ∈ t<VAR>r : ↥(nonZeroDivisors R)<VAR>hg : r • ∑ x ∈ t, g x • ↑x = 0<GOAL>g i = 0
<VAR>R✝ S : Type u<VAR>M✝ : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R✝<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : AddCommGroup M'✝<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R✝ M✝<VAR>inst✝⁴ : Module R✝ M'✝<VAR>inst✝³ : Module R✝ M₁<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>M' : Submodule R M<VAR>hN : M' ≤ torsion R M<VAR>a✝ : Nontrivial R<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>x✝ : { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>s : Set M<VAR>hs✝ : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>hs : ∀ (s_1 : Finset { x // x ∈ s }) (g : { x // x ∈ s } → R), ∑ i ∈ s_1, g i • ↑i = 0 → ∀ i ∈ s_1, g i = 0<VAR>t : Finset ↑s<VAR>g : ↑s → R<VAR>hg✝ : ∑ x ∈ t, g x • ↑x ∈ M'<VAR>i : ↑s<VAR>hi : i ∈ t<VAR>r : ↥(nonZeroDivisors R)<VAR>hg : ∑ x ∈ t, (↑r * g x) • ↑x = 0<GOAL>g i = 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝ : IsIrrefl α r<VAR>s : Multiset α<VAR>hs : ∀ a ∈ s, Acc (CutExpand r) {a}<GOAL>Acc (CutExpand r) s
<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>p : ι → Prop<VAR>q : ι → ι' → Prop<VAR>s : (x : ι) → (y : ι') → p x ∧ q x y → Set α<GOAL>⋂ x, ⋂ y, ⋂ (h : p x ∧ q x y), s x y h = ⋂ x, ⋂ (hx : p x), ⋂ y, ⋂ (hy : q x y), s x y ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>a * b⁻¹ = 1 ↔ a = b
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>β : Type u_1<VAR>s : Finset β<VAR>f : n → β → α<VAR>i : n<GOAL>(∑ x ∈ s, A.cramer fun j => f j x) i = A.cramer (fun j => ∑ x ∈ s, f j x) i
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>β : Type u_1<VAR>s : Finset β<VAR>f : n → β → α<VAR>i : n<GOAL>(A.updateColumn i (∑ x ∈ s, fun j => f j x)).det = (A.updateColumn i fun j => ∑ x ∈ s, f j x).det
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>β : Type u_1<VAR>s : Finset β<VAR>f : n → β → α<VAR>i j x✝ : n<GOAL>(∑ x ∈ s, fun j => f j x) j = ∑ x ∈ s, f j x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℤ<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>init n (m • x) = init n (m • init n x)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<VAR>C : VariableChange R<GOAL>{ u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 } = { u := 1, r := 0, s := 0, t := 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>I : Ideal R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower S R M<VAR>i : ℕ<VAR>f : R[X]<VAR>m : M<VAR>n : ℕ<GOAL>(f • (single R i) m) n = if i ≤ n then f.coeff (n - i) • m else 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>I : Ideal R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower S R M<VAR>i : ℕ<VAR>m : M<VAR>n : ℕ<VAR>p q : R[X]<VAR>hp : (p • (single R i) m) n = if i ≤ n then p.coeff (n - i) • m else 0<VAR>hq : (q • (single R i) m) n = if i ≤ n then q.coeff (n - i) • m else 0<GOAL>((p + q) • (single R i) m) n = if i ≤ n then (p + q).coeff (n - i) • m else 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>I : Ideal R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower S R M<VAR>i : ℕ<VAR>m : M<VAR>n n✝ : ℕ<VAR>a✝ : R<GOAL>((monomial n✝) a✝ • (single R i) m) n = if i ≤ n then ((monomial n✝) a✝).coeff (n - i) • m else 0
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>W.Φ (↑n + 1) = (X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) - W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>((X * W.preΨ' (n + 1) ^ 2 * if Even (n + 1) then W.Ψ₂Sq else 1) - W.preΨ' (n + 1 + 1) * W.preΨ' n * if Even (↑n + 1) then 1 else W.Ψ₂Sq) = (X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) - W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1
<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>β : Type u_5<VAR>inst✝ : MeasurableSpace β<VAR>μb : Measure β<VAR>g : β →ₘ[μb] E<VAR>hg : g ∈ Lp E p μb<VAR>f : α → β<VAR>hf : MeasurePreserving f μ μb<GOAL>g.compMeasurePreserving f hf ∈ Lp E 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>β : Type u_5<VAR>inst✝ : MeasurableSpace β<VAR>μb : Measure β<VAR>g : β →ₘ[μb] E<VAR>hg : eLpNorm (↑g) p μb < ⊤<VAR>f : α → β<VAR>hf : MeasurePreserving f μ μb<GOAL>eLpNorm (↑(g.compMeasurePreserving f hf)) p μ < ⊤
<VAR>x y : ℝ<GOAL>sinh (x - y) = sinh x * cosh y - cosh x * sinh y
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>c : E<VAR>hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z<VAR>hc : IsLocalMax (norm ∘ f) c<GOAL>∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>c : E<VAR>hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z<VAR>hc : IsLocalMax (norm ∘ f) c<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr : ∀ ⦃x : E⦄, x ∈ closedBall c r → DifferentiableAt ℂ f x ∧ (norm ∘ f) x ≤ (norm ∘ f) c<GOAL>∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<GOAL>a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X Y : T<VAR>f : X ⟶ Y<GOAL>map f ⋙ forget Y = forget X
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X Y : T<VAR>f : X ⟶ Y<GOAL>∀ (X_1 : Over X), (map f ⋙ forget Y).obj X_1 = (forget X).obj X_1
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X Y : T<VAR>f : X ⟶ Y<GOAL>autoParam (∀ (X_1 Y_1 : Over X) (f_1 : X_1 ⟶ Y_1), (map f ⋙ forget Y).map f_1 = eqToHom ⋯ ≫ (forget X).map f_1 ≫ eqToHom ⋯) _auto✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin b<GOAL>Icc a (pred b) = Ico a b