ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))<GOAL>Finite (𝓞 K ⧸ Ideal.span {hζ✝.toInteger - 1})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : α → β<VAR>s✝ t✝ : Set α<VAR>hf : Injective f<VAR>s t : Set α<GOAL>f '' s ∆ t = (f '' s) ∆ (f '' t)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<VAR>hs : P.k < s.re<GOAL>mellin (fun x => P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<VAR>hs : P.k < s.re<VAR>h_re1 : -1 < (s - 1).re<GOAL>mellin (fun x => P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
<VAR>R : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>A : Type u_4<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }<VAR>a : A<VAR>ad : A[ε]<GOAL>(lift fe) (MulOpposite.op a • ad) = (lift fe) ad * (↑fe).1 a
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>v v' : V<VAR>p p' : P<GOAL>dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p'
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t v w : V<GOAL>(edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
<VAR>α : Type u_1<VAR>inst✝ : CommSemigroup α<VAR>a b c✝ : α<VAR>h : a ∣ b<VAR>c : α<GOAL>a ∣ c * b
<VAR>α : Type u_1<VAR>inst✝ : CommSemigroup α<VAR>a b c✝ : α<VAR>h : a ∣ b<VAR>c : α<GOAL>a ∣ b * c
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<GOAL>(↑P.parts.offDiag.attach).PairwiseDisjoint (SzemerediRegularity.distinctPairs hP G ε)
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<GOAL>(↑P.parts.offDiag.attach).Pairwise fun x y => ∀ ⦃a : Finset α × Finset α⦄, a.1 ∈ (chunk hP G ε ⋯).parts ∧ a.2 ∈ (chunk hP G ε ⋯).parts → ¬(a.1 ∈ (chunk hP G ε ⋯).parts ∧ a.2 ∈ (chunk hP G ε ⋯).parts)
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s₁ s₂ : Finset α<VAR>hs : (s₁, s₂) ∈ P.parts.offDiag<VAR>a✝¹ : ⟨(s₁, s₂), hs⟩ ∈ ↑P.parts.offDiag.attach<VAR>t₁ t₂ : Finset α<VAR>ht : (t₁, t₂) ∈ P.parts.offDiag<VAR>a✝ : ⟨(t₁, t₂), ht⟩ ∈ ↑P.parts.offDiag.attach<VAR>hst : ⟨(s₁, s₂), hs⟩ ≠ ⟨(t₁, t₂), ht⟩<VAR>u v : Finset α<VAR>huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts<VAR>huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s₁ s₂ : Finset α<VAR>hs✝ : (s₁, s₂) ∈ P.parts.offDiag<VAR>hs : (s₁, s₂).1 ∈ P.parts ∧ (s₁, s₂).2 ∈ P.parts ∧ (s₁, s₂).1 ≠ (s₁, s₂).2<VAR>a✝¹ : ⟨(s₁, s₂), hs✝⟩ ∈ ↑P.parts.offDiag.attach<VAR>t₁ t₂ : Finset α<VAR>ht✝ : (t₁, t₂) ∈ P.parts.offDiag<VAR>ht : (t₁, t₂).1 ∈ P.parts ∧ (t₁, t₂).2 ∈ P.parts ∧ (t₁, t₂).1 ≠ (t₁, t₂).2<VAR>a✝ : ⟨(t₁, t₂), ht✝⟩ ∈ ↑P.parts.offDiag.attach<VAR>hst : ⟨(s₁, s₂), hs✝⟩ ≠ ⟨(t₁, t₂), ht✝⟩<VAR>u v : Finset α<VAR>huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts<VAR>huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s₁ s₂ : Finset α<VAR>hs✝ : (s₁, s₂) ∈ P.parts.offDiag<VAR>hs : (s₁, s₂).1 ∈ P.parts ∧ (s₁, s₂).2 ∈ P.parts ∧ (s₁, s₂).1 ≠ (s₁, s₂).2<VAR>a✝¹ : ⟨(s₁, s₂), hs✝⟩ ∈ ↑P.parts.offDiag.attach<VAR>t₁ t₂ : Finset α<VAR>ht✝ : (t₁, t₂) ∈ P.parts.offDiag<VAR>ht : (t₁, t₂).1 ∈ P.parts ∧ (t₁, t₂).2 ∈ P.parts ∧ (t₁, t₂).1 ≠ (t₁, t₂).2<VAR>a✝ : ⟨(t₁, t₂), ht✝⟩ ∈ ↑P.parts.offDiag.attach<VAR>hst : ⟨(s₁, s₂), hs✝⟩ ≠ ⟨(t₁, t₂), ht✝⟩<VAR>u v : Finset α<VAR>huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts<VAR>huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts<VAR>a : α<VAR>ha : a ∈ (u, v).1<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s₁ s₂ : Finset α<VAR>hs✝ : (s₁, s₂) ∈ P.parts.offDiag<VAR>hs : (s₁, s₂).1 ∈ P.parts ∧ (s₁, s₂).2 ∈ P.parts ∧ (s₁, s₂).1 ≠ (s₁, s₂).2<VAR>a✝¹ : ⟨(s₁, s₂), hs✝⟩ ∈ ↑P.parts.offDiag.attach<VAR>t₁ t₂ : Finset α<VAR>ht✝ : (t₁, t₂) ∈ P.parts.offDiag<VAR>ht : (t₁, t₂).1 ∈ P.parts ∧ (t₁, t₂).2 ∈ P.parts ∧ (t₁, t₂).1 ≠ (t₁, t₂).2<VAR>a✝ : ⟨(t₁, t₂), ht✝⟩ ∈ ↑P.parts.offDiag.attach<VAR>hst : ⟨(s₁, s₂), hs✝⟩ ≠ ⟨(t₁, t₂), ht✝⟩<VAR>u v : Finset α<VAR>huv₁ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts<VAR>huv₂ : (u, v).1 ∈ (chunk hP G ε ⋯).parts ∧ (u, v).2 ∈ (chunk hP G ε ⋯).parts<VAR>a : α<VAR>ha : a ∈ (u, v).1<VAR>b : α<VAR>hb : b ∈ (u, v).2<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : WfDvdMonoid R<VAR>x : R<VAR>hx₀ : x ≠ 0<GOAL>Squarefree x ↔ ∀ (p : R), Irreducible p → ¬p * p ∣ x
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : WfDvdMonoid R<VAR>x : R<VAR>hx₀ : x ≠ 0<VAR>h : ∀ (p : R), Irreducible p → ¬p * p ∣ x<VAR>d : R<VAR>hd : d * d ∣ x<VAR>hdu : ¬IsUnit d<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : WfDvdMonoid R<VAR>x : R<VAR>hx₀ : x ≠ 0<VAR>h : ∀ (p : R), Irreducible p → ¬p * p ∣ x<VAR>d : R<VAR>hd : d * d ∣ x<VAR>hdu : ¬IsUnit d<VAR>hd₀ : d ≠ 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : WfDvdMonoid R<VAR>x : R<VAR>hx₀ : x ≠ 0<VAR>h : ∀ (p : R), Irreducible p → ¬p * p ∣ x<VAR>d : R<VAR>hd : d * d ∣ x<VAR>hdu : ¬IsUnit d<VAR>hd₀ : d ≠ 0<VAR>p : R<VAR>irr : Irreducible p<VAR>dvd : p ∣ d<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A✝ : Type u_5<VAR>inst✝¹³ : CommSemiring A✝<VAR>inst✝¹² : Algebra R A✝<VAR>inst✝¹¹ : Module A✝ M'<VAR>inst✝¹⁰ : IsLocalization S A✝<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A✝ M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>A : Type u_6<VAR>Aₛ : Type u_7<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : CommSemiring Aₛ<VAR>inst✝² : Algebra A Aₛ<VAR>inst✝¹ : Algebra R Aₛ<VAR>inst✝ : IsScalarTower R A Aₛ<GOAL>IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap ↔ IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A✝ : Type u_5<VAR>inst✝¹³ : CommSemiring A✝<VAR>inst✝¹² : Algebra R A✝<VAR>inst✝¹¹ : Module A✝ M'<VAR>inst✝¹⁰ : IsLocalization S A✝<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A✝ M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>A : Type u_6<VAR>Aₛ : Type u_7<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : CommSemiring Aₛ<VAR>inst✝² : Algebra A Aₛ<VAR>inst✝¹ : Algebra R Aₛ<VAR>inst✝ : IsScalarTower R A Aₛ<GOAL>((∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R Aₛ)) ↑x)) ∧ (∀ (y : Aₛ), ∃ x, x.2 • y = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x.1) ∧ ∀ {x₁ x₂ : A}, (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x₁ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x₂ → ∃ c, c • x₁ = c • x₂) ↔ (∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit ((algebraMap A Aₛ) ↑y)) ∧ (∀ (z : Aₛ), ∃ x, z * (algebraMap A Aₛ) ↑x.2 = (algebraMap A Aₛ) x.1) ∧ ∀ {x y : A}, (algebraMap A Aₛ) x = (algebraMap A Aₛ) y → ∃ c, ↑c * x = ↑c * y
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A✝ : Type u_5<VAR>inst✝¹³ : CommSemiring A✝<VAR>inst✝¹² : Algebra R A✝<VAR>inst✝¹¹ : Module A✝ M'<VAR>inst✝¹⁰ : IsLocalization S A✝<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A✝ M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>A : Type u_6<VAR>Aₛ : Type u_7<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : CommSemiring Aₛ<VAR>inst✝² : Algebra A Aₛ<VAR>inst✝¹ : Algebra R Aₛ<VAR>inst✝ : IsScalarTower R A Aₛ<GOAL>(∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R Aₛ)) ↑x)) ↔ ∀ (y : ↥(Algebra.algebraMapSubmonoid A S)), IsUnit ((algebraMap A Aₛ) ↑y)
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A✝ : Type u_5<VAR>inst✝¹³ : CommSemiring A✝<VAR>inst✝¹² : Algebra R A✝<VAR>inst✝¹¹ : Module A✝ M'<VAR>inst✝¹⁰ : IsLocalization S A✝<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A✝ M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>A : Type u_6<VAR>Aₛ : Type u_7<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : CommSemiring Aₛ<VAR>inst✝² : Algebra A Aₛ<VAR>inst✝¹ : Algebra R Aₛ<VAR>inst✝ : IsScalarTower R A Aₛ<VAR>x✝ : Aₛ<GOAL>(∃ x, x.2 • x✝ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x.1) ↔ ∃ x, x✝ * (algebraMap A Aₛ) ↑x.2 = (algebraMap A Aₛ) x.1
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : AddCommMonoid M'<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A✝ : Type u_5<VAR>inst✝¹³ : CommSemiring A✝<VAR>inst✝¹² : Algebra R A✝<VAR>inst✝¹¹ : Module A✝ M'<VAR>inst✝¹⁰ : IsLocalization S A✝<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R M'<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A✝ M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>A : Type u_6<VAR>Aₛ : Type u_7<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : CommSemiring Aₛ<VAR>inst✝² : Algebra A Aₛ<VAR>inst✝¹ : Algebra R Aₛ<VAR>inst✝ : IsScalarTower R A Aₛ<VAR>x✝¹ x✝ : A<GOAL>((IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝¹ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x✝ → ∃ c, c • x✝¹ = c • x✝) ↔ (algebraMap A Aₛ) x✝¹ = (algebraMap A Aₛ) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<GOAL>variance (fun ω => c * X ω) μ = c ^ 2 * variance X μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<GOAL>c ^ 2 * (evariance X μ).toReal = c ^ 2 * variance X μ
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>n : ℕ<VAR>ih : FP (Stream'.drop n a) ⊆ FP a<GOAL>FP (Stream'.drop (n + 1) a) ⊆ FP a
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>n : ℕ<VAR>ih : FP (Stream'.drop n a) ⊆ FP a<GOAL>FP (Stream'.drop 1 (Stream'.drop n a)) ⊆ FP a
<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✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>B : BilinMap R M N<VAR>h : IsUnit 2<VAR>Q₁ Q₂ : QuadraticMap R M N<VAR>h₁₂ : Q₁.polarBilin = Q₂.polarBilin<GOAL>Q₁ = Q₂
<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✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>B : BilinMap R M N<VAR>h : IsUnit 2<VAR>Q₁ Q₂ : QuadraticMap R M N<VAR>h₁₂ : Q₁.polarBilin = Q₂.polarBilin<GOAL>2 • Q₁ = 2 • Q₂
<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✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>B : BilinMap R M N<VAR>h : IsUnit 2<VAR>Q₁ Q₂ : QuadraticMap R M N<VAR>h₁₂ : Q₁.polarBilin = Q₂.polarBilin<GOAL>↑2 • Q₁ = ↑2 • Q₂
<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✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>B : BilinMap R M N<VAR>h : IsUnit 2<VAR>Q₁ Q₂ : QuadraticMap R M N<VAR>h₁₂ : Q₁.polarBilin = Q₂.polarBilin<GOAL>Q₁.polarBilin.toQuadraticMap = Q₂.polarBilin.toQuadraticMap
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F✝ : Type u_2<VAR>inst✝³ : NormedAddCommGroup F✝<VAR>inst✝² : NormedSpace 𝕜 F✝<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F✝<VAR>f' : F✝<VAR>s t : Set E<VAR>x v✝ : E<VAR>L : E →L[𝕜] F✝<VAR>v : E<VAR>F : 𝕜 → E := fun t => x + t • v<VAR>hf : HasFDerivWithinAt f L s (F 0)<GOAL>HasLineDerivWithinAt 𝕜 f (L v) s x v
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F✝ : Type u_2<VAR>inst✝³ : NormedAddCommGroup F✝<VAR>inst✝² : NormedSpace 𝕜 F✝<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F✝<VAR>f' : F✝<VAR>s t : Set E<VAR>x v✝ : E<VAR>L : E →L[𝕜] F✝<VAR>v : E<VAR>F : 𝕜 → E := fun t => x + t • v<VAR>hf : HasFDerivWithinAt f L s (F 0)<VAR>A : HasDerivWithinAt F (0 + 1 • v) (F ⁻¹' s) 0<GOAL>HasLineDerivWithinAt 𝕜 f (L v) s x v
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F✝ : Type u_2<VAR>inst✝³ : NormedAddCommGroup F✝<VAR>inst✝² : NormedSpace 𝕜 F✝<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F✝<VAR>f' : F✝<VAR>s t : Set E<VAR>x v✝ : E<VAR>L : E →L[𝕜] F✝<VAR>v : E<VAR>F : 𝕜 → E := fun t => x + t • v<VAR>hf : HasFDerivWithinAt f L s (F 0)<VAR>A : HasDerivWithinAt F v (F ⁻¹' s) 0<GOAL>HasLineDerivWithinAt 𝕜 f (L v) s x v
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>G : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁹ : NormedField R<VAR>inst✝⁸ : SeminormedAddCommGroup M<VAR>inst✝⁷ : SeminormedAddCommGroup N<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace R M<VAR>inst✝⁴ : NormedSpace R N<VAR>inst✝³ : NormedSpace R G<VAR>inst✝² : NormedAddCommGroup M'<VAR>inst✝¹ : NormedSpace R M'<VAR>f : M →L[R] N<VAR>g : N →L[R] G<VAR>c : R<VAR>inst✝ : Nontrivial M'<VAR>hf' : IsConformalMap 0<GOAL>False
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>G : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁹ : NormedField R<VAR>inst✝⁸ : SeminormedAddCommGroup M<VAR>inst✝⁷ : SeminormedAddCommGroup N<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace R M<VAR>inst✝⁴ : NormedSpace R N<VAR>inst✝³ : NormedSpace R G<VAR>inst✝² : NormedAddCommGroup M'<VAR>inst✝¹ : NormedSpace R M'<VAR>f : M →L[R] N<VAR>g : N →L[R] G<VAR>c : R<VAR>inst✝ : Nontrivial M'<VAR>hf' : IsConformalMap 0<VAR>a : M'<VAR>ha : a ≠ 0<GOAL>False
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>P : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), P ((_root_.algebraMap R (CliffordAlgebra Q)) r)<VAR>add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)<VAR>mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)<VAR>x : CliffordAlgebra Q<GOAL>P x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>P : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), P ((_root_.algebraMap R (CliffordAlgebra Q)) r)<VAR>add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)<VAR>mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)<VAR>x : CliffordAlgebra Q<VAR>this : x ∈ ⊤<GOAL>P x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>P : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), P ((_root_.algebraMap R (CliffordAlgebra Q)) r)<VAR>add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)<VAR>mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)<VAR>x : CliffordAlgebra Q<VAR>this : x ∈ ⨆ i, LinearMap.range (ι Q) ^ i<GOAL>P x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>x y : G<VAR>i : ℤ<GOAL>↑(orderOf x) ∣ i ↔ x ^ i = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>x y : G<VAR>i : ℕ<GOAL>↑(orderOf x) ∣ ↑i ↔ x ^ ↑i = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>x y : G<VAR>i : ℕ<GOAL>↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1
<VAR>m n k : ℕ+<VAR>h : k.Coprime m<GOAL>m.gcd (k * n) = m.gcd n
<VAR>m n k : ℕ+<VAR>h : k.Coprime m<GOAL>(k * n).gcd m = n.gcd m
<VAR>y₁ y₂ : ℕ<VAR>h : y₁ ≤ y₂<VAR>m₁ m₂ : ℤ<VAR>h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂<GOAL>↑m₁ * powHalf y₂ = ↑m₂ * powHalf y₁
<VAR>y₁ : ℕ<VAR>m₁ m₂ : ℤ<VAR>c : ℕ<VAR>h : y₁ ≤ y₁ + c<VAR>h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ (y₁ + c)<GOAL>↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁
<VAR>y₁ : ℕ<VAR>m₁ m₂ : ℤ<VAR>c : ℕ<VAR>h : y₁ ≤ y₁ + c<VAR>h₂ : m₁ = m₂ * 2 ^ c ∨ 2 ^ y₁ = 0<GOAL>↑m₁ * powHalf (y₁ + c) = ↑m₂ * powHalf y₁
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : PolishSpace α<VAR>C : Set α<VAR>hC : IsClosed C<VAR>hunc : ¬C.Countable<VAR>this : UpgradedPolishSpace α := upgradePolishSpace α<GOAL>∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : PolishSpace α<VAR>C : Set α<VAR>hC : IsClosed C<VAR>hunc : ¬C.Countable<VAR>this : UpgradedPolishSpace α := upgradePolishSpace α<VAR>D : Set α<VAR>hD : Perfect D<VAR>Dnonempty : D.Nonempty<VAR>hDC : D ⊆ C<GOAL>∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : PolishSpace α<VAR>C : Set α<VAR>hC : IsClosed C<VAR>hunc : ¬C.Countable<VAR>this : UpgradedPolishSpace α := upgradePolishSpace α<VAR>D : Set α<VAR>hD : Perfect D<VAR>Dnonempty : D.Nonempty<VAR>hDC : D ⊆ C<VAR>f : (ℕ → Bool) → α<VAR>hfD : range f ⊆ D<VAR>hf : Continuous f ∧ Function.Injective f<GOAL>∃ f, range f ⊆ C ∧ Continuous f ∧ Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>k : Nat<VAR>hk : l.length ≤ k<VAR>l' : List α<GOAL>(l ++ l').eraseIdx k = l ++ l'.eraseIdx (k - l.length)
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>k : Nat<VAR>hk : l.length ≤ k<VAR>l' : List α<GOAL>l ++ (take (k - l.length) l' ++ drop (k + 1 - l.length) l') = l ++ (take (k - l.length) l' ++ drop (k - l.length + 1) l')
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s t✝ : Set α<VAR>f : α → β<VAR>t : Set ↑s<GOAL>LipschitzOnWith K (s.restrict f) t ↔ LipschitzOnWith K f (s ∩ Subtype.val '' t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s t✝ : Set α<VAR>f : α → β<VAR>t : Set ↑s<GOAL>(∀ (a : α) (b : a ∈ s), ⟨a, b⟩ ∈ t → ∀ (a_2 : α) (b : a_2 ∈ s), ⟨a_2, b⟩ ∈ t → edist (f a) (f a_2) ≤ ↑K * edist a a_2) ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Subtype.val '' t → ∀ ⦃y : α⦄, y ∈ s ∩ Subtype.val '' t → edist (f x) (f y) ≤ ↑K * edist x y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>c : (X : C) → ClosureOperator (Sieve X)<VAR>pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)<VAR>X : C<VAR>S : Sieve X<VAR>Y : C<VAR>f : Y ⟶ X<GOAL>(c Y) (Sieve.pullback f S) = ⊤ ↔ ((c X) S).arrows f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<GOAL>AntitoneOn (fun x => x⁻¹) (Set.Iio 0)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>c : Con M<VAR>l : List ι<VAR>f g : ι → M<VAR>h : ∀ x ∈ l, c (f x) (g x)<GOAL>c (List.map f l).prod (List.map g l).prod
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>hN : IsTorsion' N ↥(Submonoid.powers p)<VAR>h' : Finite R N<GOAL>∃ d k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>hN : IsTorsion' N ↥(Submonoid.powers p)<VAR>h' : Finite R N<VAR>d : ℕ<VAR>s : Fin d → N<VAR>hs : Submodule.span R (Set.range s) = ⊤<GOAL>∃ d k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>hN : IsTorsion' N ↥(Submonoid.powers p)<VAR>h' : Finite R N<VAR>d : ℕ<VAR>s : Fin d → N<VAR>hs : Submodule.span R (Set.range s) = ⊤<GOAL>∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>inst✝ : LocallyFiniteOrderBot α<GOAL>Icc a b ⊆ Iic b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<GOAL>[x-[𝕜]y] = ⇑(AffineMap.lineMap x y) '' Icc 0 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>a✝¹ : 𝕜<VAR>a✝ : a✝¹ ∈ Icc 0 1<GOAL>(AffineMap.lineMap x y) a✝¹ = (1 - a✝¹) • x + a✝¹ • y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝³ : Ring α<VAR>a b : α<VAR>F : Type u_1<VAR>inst✝² : Ring β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RingHomClass F α β<VAR>f : F<GOAL>(map ↑f) (-1) = -1
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>x : α<VAR>f : ℕ → α → α<GOAL>(range fun n => rec x f n) = {x} ∪ range fun n => rec (f 0 x) (f ∘ succ) n
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>x : α<VAR>f : ℕ → α → α<VAR>x✝ : ℕ<GOAL>rec (f 0 x) (f ∘ succ) x✝ = ((fun n => rec x f n) ∘ succ) x✝