ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>s : ↥S<VAR>p : LocalizedModule S M<VAR>m : M<VAR>t : ↥S<GOAL>(divBy s) (((algebraMap R (Module.End R (LocalizedModule S M))) ↑s) (mk m t)) = mk m t
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>s : ↥S<VAR>p : LocalizedModule S M<VAR>m : M<VAR>t : ↥S<GOAL>(↑s • mk m t).liftOn (fun p => mk p.1 (p.2 * s)) ⋯ = mk m t
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>s : ↥S<VAR>p : LocalizedModule S M<VAR>m : M<VAR>t : ↥S<GOAL>(mk ((IsLocalization.sec S (↑(algebraMap R (Localization S)).toMonoidWithZeroHom ↑s)).1 • m) ((IsLocalization.sec S (↑(algebraMap R (Localization S)).toMonoidWithZeroHom ↑s)).2 * t)).liftOn (fun p => mk p.1 (p.2 * s)) ⋯ = mk m t
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>s : ↥S<VAR>p : LocalizedModule S M<VAR>m : M<VAR>t : ↥S<GOAL>↑(algebraMap R (Localization S)).toMonoidWithZeroHom ↑s • mk m (t * s) = mk m t
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>s : ↥S<VAR>p : LocalizedModule S M<VAR>m : M<VAR>t : ↥S<GOAL>mk (↑s • m) (t * s) = mk m t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a : α<VAR>h : a ∉ s<VAR>hs : autoParam s.Finite _auto✝<GOAL>(insert a s).ncard = s.ncard + 1
<VAR>x✝ : ℕ<GOAL>1 x✝ = δ x✝
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x p : P<VAR>hx : x ∉ s<VAR>hp : p ∈ s<VAR>y : P<GOAL>y ∈ {y | s.SOppSide x y} ↔ y ∈ Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) ↑s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x p : P<VAR>hx : x ∉ s<VAR>hp : p ∈ s<VAR>y : P<GOAL>s.SOppSide x y ↔ ∃ a < 0, ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(simpleFunc E p μ) → Prop<VAR>h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (indicatorConst p hs ⋯ c)<VAR>h_add : ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p μ) (hg : Memℒp (↑g) p μ), Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)<VAR>f : ↥(simpleFunc E p μ)<GOAL>P f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(simpleFunc E p μ) → Prop<VAR>h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (indicatorConst p hs ⋯ c)<VAR>h_add : ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p μ) (hg : Memℒp (↑g) p μ), Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)<VAR>f : ↥(simpleFunc E p μ)<GOAL>∀ (f : α →ₛ E) (hf : Memℒp (↑f) p μ), P (toLp f hf)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(simpleFunc E p μ) → Prop<VAR>h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (indicatorConst p hs ⋯ c)<VAR>h_add : ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p μ) (hg : Memℒp (↑g) p μ), Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)<GOAL>∀ (f : α →ₛ E) (hf : Memℒp (↑f) p μ), P (toLp f hf)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(simpleFunc E p μ) → Prop<VAR>h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (indicatorConst p hs ⋯ c)<VAR>h_add : ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p μ) (hg : Memℒp (↑g) p μ), Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)<GOAL>∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hf : Memℒp (↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ), P (toLp (SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) hf)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(simpleFunc E p μ) → Prop<VAR>h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (indicatorConst p hs ⋯ c)<VAR>h_add : ∀ ⦃f g : α →ₛ E⦄ (hf : Memℒp (↑f) p μ) (hg : Memℒp (↑g) p μ), Disjoint (support ↑f) (support ↑g) → P (toLp f hf) → P (toLp g hg) → P (toLp f hf + toLp g hg)<GOAL>∀ ⦃f g : α →ₛ E⦄, Disjoint (support ↑f) (support ↑g) → (∀ (hf : Memℒp (↑f) p μ), P (toLp f hf)) → (∀ (hf : Memℒp (↑g) p μ), P (toLp g hf)) → ∀ (hf : Memℒp (↑(f + g)) p μ), P (toLp (f + g) hf)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝² : DecidablePred p<VAR>inst✝¹ : DecidablePred q<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<GOAL>filter p s = filter p t ↔ ∀ ⦃a : α⦄, p a → (a ∈ s ↔ a ∈ t)
<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 : t ∈ 𝓝 x<GOAL>HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝¹⁰ : Ring K<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : Module K V₁<VAR>inst✝⁵ : AddCommGroup V'<VAR>inst✝⁴ : Module K V'<VAR>inst✝³ : AddCommGroup V''<VAR>inst✝² : Module K V''<VAR>inst✝¹ : AddCommGroup V'₁<VAR>inst✝ : Module K V'₁<VAR>g : V →ₗ[K] V'<VAR>f : V' →ₗ[K] V'₁<GOAL>(f ∘ₗ g).rank ≤ g.rank
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : Embedding ⇑g<GOAL>Embedding ⇑(pullback.fst f g)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : Embedding ⇑g<GOAL>⇑(pullback.fst f g) = ⇑(homeoOfIso (asIso (pullback.fst f (𝟙 S)))) ∘ ⇑(pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) ⋯ ⋯)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : Embedding ⇑g<GOAL>⇑(pullback.fst f g) = ⇑(pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) ⋯ ⋯ ≫ (asIso (pullback.fst f (𝟙 S))).hom)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m₁ m₂ : ℝ≥0∞ → ℝ≥0∞<VAR>hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂<GOAL>mkMetric m₁ ≤ mkMetric m₂
<VAR>a : EReal<VAR>h : a ≤ 0<GOAL>a⁻¹ ≤ 0
<VAR>x y : ℝ≥0<VAR>h : ∀ a < 1, a * x ≤ y<VAR>a : ℝ≥0<VAR>ha : a < x<GOAL>a ≤ y
<VAR>x y : ℝ≥0<VAR>h : ∀ a < 1, a * x ≤ y<VAR>a : ℝ≥0<VAR>ha : a < x<VAR>hx : x ≠ 0<GOAL>a ≤ y
<VAR>x y : ℝ≥0<VAR>h : ∀ a < 1, a * x ≤ y<VAR>a : ℝ≥0<VAR>ha : a < x<VAR>hx : x ≠ 0<VAR>hx' : x⁻¹ ≠ 0<GOAL>a ≤ y
<VAR>x y : ℝ≥0<VAR>h : ∀ a < 1, a * x ≤ y<VAR>a : ℝ≥0<VAR>ha : a < x<VAR>hx : x ≠ 0<VAR>hx' : x⁻¹ ≠ 0<VAR>this : a * x⁻¹ < 1<GOAL>a ≤ y
<VAR>x y : ℝ≥0<VAR>h : ∀ a < 1, a * x ≤ y<VAR>a : ℝ≥0<VAR>ha : a < x<VAR>hx : x ≠ 0<VAR>hx' : x⁻¹ ≠ 0<VAR>this✝ : a * x⁻¹ < 1<VAR>this : a * x⁻¹ * x ≤ y<GOAL>a ≤ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : AddCommMonoid L<VAR>inst✝⁷ : TopologicalSpace L<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : TopologicalSpace N<VAR>v✝ : VectorMeasure α M<VAR>w✝ : VectorMeasure α N<VAR>R : Type u_6<VAR>inst✝² : Semiring R<VAR>inst✝¹ : DistribMulAction R M<VAR>inst✝ : ContinuousConstSMul R M<VAR>r : R<VAR>v : VectorMeasure α M<VAR>w : VectorMeasure α N<VAR>h : v ≪ᵥ w<VAR>s : Set α<VAR>hs : ↑w s = 0<GOAL>↑(r • v) s = 0
<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>c : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s : Set α<VAR>f : α → E<GOAL>eLpNorm (s.indicator f) p μ ≤ eLpNorm f 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>c : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s : Set α<VAR>f : α → E<VAR>x : α<GOAL>‖s.indicator f x‖ ≤ ‖f x‖
<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>c : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s : Set α<VAR>f : α → E<VAR>x : α<GOAL>‖s.indicator f x‖₊ ≤ ‖f x‖₊
<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>c : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s : Set α<VAR>f : α → E<VAR>x : α<GOAL>s.indicator (fun a => ‖f a‖₊) x ≤ ‖f x‖₊
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α<GOAL>s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α<GOAL>(s ⊆ t ∧ ∃ a ∈ t, a ∉ s) ↔ ∃ a ∉ s, a ∈ t ∧ s ⊆ t
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>k : 𝓞 K<VAR>hk : S.a + ↑η ^ 2 * S.b = λ ^ 2 * k<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>k : 𝓞 K<VAR>hk : S.a + ↑η ^ 2 * S.b = λ ^ 2 * k<VAR>k' : 𝓞 K<VAR>hk' : S.a + S.b = λ ^ 2 * k'<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>k : 𝓞 K<VAR>hk : S.a + ↑η ^ 2 * S.b = λ ^ 2 * k<VAR>k' : 𝓞 K<VAR>hk' : S.a + S.b = λ ^ 2 * k'<GOAL>S.b = λ * ((k - k') * -↑η)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>k k' : 𝓞 K<VAR>hk : λ * (S.b * (↑η + 1) + λ * k') = λ * (λ * k)<VAR>hk' : S.a + S.b = λ ^ 2 * k'<GOAL>S.b = λ * ((k - k') * -↑η)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>k k' : 𝓞 K<VAR>hk' : S.a + S.b = λ ^ 2 * k'<VAR>hk : S.b * (↑η + 1) + λ * k' = λ * k<GOAL>S.b = λ * ((k - k') * -↑η)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>k k' : 𝓞 K<VAR>hk' : S.a + S.b = λ ^ 2 * k'<VAR>hk : (S.b * (↑η + 1) + λ * k') * -↑η = λ * k * -↑η<GOAL>S.b = λ * ((k - k') * -↑η)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>k k' : 𝓞 K<VAR>hk' : S.a + S.b = λ ^ 2 * k'<VAR>hk : S.b = λ * k * -↑η + ↑η * λ * k'<GOAL>S.b = λ * ((k - k') * -↑η)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : C(Y, Z)<VAR>g : C(X, Y)<VAR>y : Z<VAR>hy : f.Homotopic (const Y y)<GOAL>(f.comp g).Nullhomotopic
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : C(Y, Z)<VAR>g : C(X, Y)<VAR>y : Z<VAR>hy : f.Homotopic (const Y y)<GOAL>(f.comp g).Homotopic (const X y)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>inst✝ : Fintype α<GOAL>𝒜.Shatters univ ↔ 𝒜 = univ
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>inst✝ : Fintype α<GOAL>image (fun t => univ ∩ t) 𝒜 = univ ↔ 𝒜 = univ
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n✝ n : ℕ+<VAR>hn : Fintype.card ↥(rootsOfUnity n L) = ↑n<VAR>g : L ≃+* L<VAR>t : Lˣ<VAR>ht : t ∈ rootsOfUnity n L<GOAL>g ↑t = ↑t ^ (↑((ModularCyclotomicCharacter L hn) g)).val
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n✝ n : ℕ+<VAR>hn : Fintype.card ↥(rootsOfUnity n L) = ↑n<VAR>g : L ≃+* L<VAR>t : Lˣ<VAR>ht : t ∈ rootsOfUnity n L<GOAL>↑t ^ (toFun n g).val = ↑t ^ (↑((ModularCyclotomicCharacter L hn) g)).val
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n✝ n : ℕ+<VAR>hn : Fintype.card ↥(rootsOfUnity n L) = ↑n<VAR>g : L ≃+* L<VAR>t : Lˣ<VAR>ht : t ∈ rootsOfUnity n L<GOAL>(toFun n g).val = (↑((ModularCyclotomicCharacter L hn) g)).val
<VAR>α : Type u_1<VAR>d : DynkinSystem α<GOAL>d.Has univ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X✝ : SimplicialObject C<VAR>q n : ℕ<VAR>X Y : SimplicialObject C<VAR>f : X ⟶ Y<VAR>hnm : c.Rel (n + 1) n<GOAL>f.app (op [n]) ≫ hσ' q n (n + 1) hnm = hσ' q n (n + 1) hnm ≫ f.app (op [n + 1])
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X✝ : SimplicialObject C<VAR>q n : ℕ<VAR>X Y : SimplicialObject C<VAR>f : X ⟶ Y<VAR>hnm : c.Rel (n + 1) n<GOAL>f.app (op [n]) ≫ hσ q n = hσ q n ≫ f.app (op [n + 1])
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : α → M × N<GOAL>mulSupport f = (mulSupport fun x => (f x).1) ∪ mulSupport fun x => (f x).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a b d y : α<VAR>x : WithBot α<GOAL>unbot' d x = y ↔ x = ↑y ∨ x = ⊥ ∧ y = d
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a b : α<VAR>l l₁ l₂ : List α<VAR>e : (a :: b :: l).split = (l₁, l₂)<GOAL>mergeSort r (a :: b :: l) ~ a :: b :: l
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a b : α<VAR>l l₁ l₂ : List α<VAR>e : (a :: b :: l).split = (l₁, l₂)<VAR>h₁ : l₁.length < (a :: b :: l).length<VAR>h₂ : l₂.length < (a :: b :: l).length<GOAL>mergeSort r (a :: b :: l) ~ a :: b :: l
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a b : α<VAR>l l₁ l₂ : List α<VAR>e : (a :: b :: l).split = (l₁, l₂)<VAR>h₁ : l₁.length < (a :: b :: l).length<VAR>h₂ : l₂.length < (a :: b :: l).length<GOAL>merge (fun x x_1 => decide (r x x_1)) (mergeSort r l₁) (mergeSort r l₂) ~ a :: b :: l
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>a b : α<VAR>l l₁ l₂ : List α<VAR>e : (a :: b :: l).split = (l₁, l₂)<VAR>h₁ : l₁.length < (a :: b :: l).length<VAR>h₂ : l₂.length < (a :: b :: l).length<GOAL>mergeSort r l₁ ++ mergeSort r l₂ ~ a :: b :: l
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>f : Filter ι<VAR>x₀ : α<VAR>p : α × ι → Prop<GOAL>(∀ᶠ (x : α × ι) in 𝓝 x₀ ×ˢ f, p x) ↔ ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (x, i)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>f : Filter ι<VAR>x₀ : α<VAR>p : α × ι → Prop<GOAL>(∃ i, (0 < i.1 ∧ i.2 ∈ f) ∧ ∀ ⦃x : α × ι⦄, x ∈ ball x₀ i.1 ×ˢ id i.2 → p x) ↔ ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (x, i)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>f : Filter ι<VAR>x₀ : α<VAR>p : α × ι → Prop<GOAL>(∃ a, 0 < a ∧ ∃ x ∈ f, ∀ (x_1 : α), dist x_1 x₀ < a → ∀ y ∈ x, p (x_1, y)) ↔ ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (x, i)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H✝ K H : Subgroup G<GOAL>Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H✝ K H : Subgroup G<GOAL>(∃ y, ∃ (_ : y ∈ H), y ≠ ↑1) ↔ ∃ x ∈ H, x ≠ 1
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b : α<VAR>x✝ : Invertible b<GOAL>a * ⅟b * b = a
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : TopologicalSpace F<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F TotalSpace.proj<VAR>x : TotalSpace F E<VAR>b✝ : B<VAR>y : E b✝<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : Module R F<VAR>inst✝³ : (x : B) → AddCommMonoid (E x)<VAR>inst✝² : (x : B) → Module R (E x)<VAR>e e' : Trivialization F TotalSpace.proj<VAR>inst✝¹ : Trivialization.IsLinear R e<VAR>inst✝ : Trivialization.IsLinear R e'<VAR>b : B<VAR>hb : b ∈ e.baseSet ∩ e'.baseSet<VAR>v : F<GOAL>↑e' (↑e.symm (b, v)) = (b, (coordChangeL R e e' b) v)
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>hx : 1 ≤ x<VAR>n : ℕ<GOAL>1 ≤ x ^ (n + 1)
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>hx : 1 ≤ x<VAR>n : ℕ<GOAL>1 ≤ x ^ n * x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℤ<VAR>hn : n ≠ -1<VAR>c w : ℂ<VAR>R : ℝ<VAR>H : w ∈ sphere c |R| → -1 ≤ n<VAR>hd : ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z => (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z<GOAL>(∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>n : ℤ<VAR>hn : n ≠ -1<VAR>c w : ℂ<VAR>R : ℝ<VAR>H : w ∈ sphere c |R| → -1 ≤ n<VAR>hd : ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z => (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z<VAR>z : ℂ<VAR>hz : z ∈ sphere c |R|<GOAL>z ≠ w ∨ -1 ≤ n
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>d s : Set (α × α)<VAR>hd : d ∈ 𝓤 α<VAR>cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}<VAR>t : (p : α × α) → p ∈ s → Set (α × α)<VAR>ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen (t p a) ∧ p ∈ t p a<GOAL>∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>p : R<VAR>hp : Irreducible p<VAR>I : Ideal R<VAR>hI : span R {p} < I<GOAL>I = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>p : R<VAR>hp : Irreducible p<VAR>a : R<VAR>hI : span R {p} < span R {a}<GOAL>span R {a} = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>p : R<VAR>hp : Irreducible p<VAR>a : R<VAR>hI : span R {p} < span R {a}<GOAL>IsUnit a
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>a b : R<VAR>hp : Irreducible (a * b)<VAR>hI : span R {a * b} < span R {a}<GOAL>IsUnit a
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>a b : R<VAR>hp : Irreducible (a * b)<VAR>hI : span R {a * b} < span R {a}<VAR>hb : IsUnit b<GOAL>span R {a} ≤ span R {a * b}
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : (i : ι) → Zero (α i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>r : ι → ι → Prop<VAR>inst✝ : IsStrictOrder ι r<VAR>x y : Π₀ (i : ι), α i<VAR>hlt : x < y<GOAL>Pi.Lex r (fun {i} x x_1 => x < x_1) ⇑x ⇑y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : (i : ι) → Zero (α i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>r : ι → ι → Prop<VAR>inst✝ : IsStrictOrder ι r<VAR>x y : Π₀ (i : ι), α i<VAR>hlt : x < y<GOAL>∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
<VAR>β : Type w<VAR>α✝ : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>f : α✝ → C<VAR>g : β → C<VAR>inst✝ : HasCoproduct f<VAR>e : β ≃ α✝<VAR>iso : (j : β) → g j ≅ f (e j)<VAR>this : HasColimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f)<VAR>α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f<GOAL>HasCoproduct g
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x✝ : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>x₀ : α<VAR>x : Fin n → α<GOAL>Injective (cons x₀ x) ↔ x₀ ∉ Set.range x ∧ Injective x
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x✝ : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>x₀ : α<VAR>x : Fin n → α<VAR>h : Injective (cons x₀ x)<GOAL>x₀ ∉ Set.range x
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x✝ : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>x₀ : α<VAR>x : Fin n → α<VAR>h : Injective (cons x₀ x)<GOAL>Injective x
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>inst✝ : Preorder β<VAR>f g : α → β<GOAL>↑f < ↑g ↔ ∀* (x : α), f x < g x