ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s✝ : Set ℝ<VAR>l : ℝ≥0<VAR>s t : ℝ<VAR>hs : 0 ≤ s<VAR>ht : 0 ≤ t<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ (Icc 0 s)<VAR>φst : φ '' Icc 0 s = Icc 0 t<VAR>hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)<VAR>hf : HasUnitSpeedOn f (φ '' Icc 0 s)<VAR>this : φ 0 = 0<GOAL>id = fun y => y - 0 + φ 0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s✝ : Set ℝ<VAR>l : ℝ≥0<VAR>s t : ℝ<VAR>hs : 0 ≤ s<VAR>ht : 0 ≤ t<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ (Icc 0 s)<VAR>φst : φ '' Icc 0 s = Icc 0 t<VAR>hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)<VAR>hf : HasUnitSpeedOn f (φ '' Icc 0 s)<VAR>this : φ 0 = 0<GOAL>id = fun y => y
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>(deriv fun x => 1 + ε x) =ᶠ[atTop] deriv ε
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>x : ℝ<VAR>hx : 1 < x<GOAL>deriv (fun x => 1 + ε x) x = deriv ε x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>deriv ε =ᶠ[atTop] fun x => -x⁻¹ / log x ^ 2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹² : CommRing R₁<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁶ : AddCommMonoid M'✝<VAR>inst✝⁵ : AddCommMonoid M''<VAR>inst✝⁴ : Module R M'✝<VAR>inst✝³ : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>f : Module.Dual K V<VAR>v : V<GOAL>((B.toDual hB) ((B.toDual hB).symm f)) v = f v
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s₁ s₂ : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s₁<VAR>inst✝ : HasOrthogonalProjection s₁.direction<VAR>hle : s₁ ≤ s₂<VAR>p : P<VAR>hp : p ∈ s₂<GOAL>(reflection s₁) p ∈ s₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s₁ s₂ : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s₁<VAR>inst✝ : HasOrthogonalProjection s₁.direction<VAR>hle : s₁ ≤ s₂<VAR>p : P<VAR>hp : p ∈ s₂<GOAL>↑((orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑((orthogonalProjection s₁) p) ∈ s₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s₁ s₂ : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s₁<VAR>inst✝ : HasOrthogonalProjection s₁.direction<VAR>hle : s₁ ≤ s₂<VAR>p : P<VAR>hp : p ∈ s₂<VAR>ho : ↑((orthogonalProjection s₁) p) ∈ s₂<GOAL>↑((orthogonalProjection s₁) p) -ᵥ p +ᵥ ↑((orthogonalProjection s₁) p) ∈ s₂
<VAR>B : Type u<VAR>inst✝ : Quiver B<VAR>a b : B<VAR>f : Discrete (Path a b)<VAR>down✝ : f.as = f.as<GOAL>(preinclusion B).map₂ { down := { down := down✝ } } = eqToHom ⋯
<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✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>H : Subgroup G<VAR>K : Subgroup N<VAR>J : Subgroup (G × N)<GOAL>J ≤ H.prod K ↔ map (MonoidHom.fst G N) J ≤ H ∧ map (MonoidHom.snd G N) J ≤ K
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : C<VAR>Y : Over X<VAR>S : Sieve Y<VAR>Z : C<VAR>f : Z ⟶ Y.left<GOAL>((overEquiv Y) S).arrows f ↔ S.arrows (Over.homMk f ⋯)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : C<VAR>Y : Over X<VAR>Z : C<VAR>f : Z ⟶ Y.left<VAR>S : Sieve Y.left<GOAL>((overEquiv Y) ((overEquiv Y).symm S)).arrows f ↔ ((overEquiv Y).symm S).arrows (Over.homMk f ⋯)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<GOAL>frontier sᶜ = frontier s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a b x y : α<VAR>h : ∃ t, IsChain r s ∧ SuperChain r s t<GOAL>SuperChain r s (SuccChain r s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a b x y : α<VAR>h : ∃ t, IsChain r s ∧ SuperChain r s t<VAR>this : IsChain r s ∧ SuperChain r s h.choose<GOAL>SuperChain r s (SuccChain r s)
<VAR>g : SL(2, ℝ)<VAR>hc : ↑↑g 1 0 ≠ 0<GOAL>∃ u v w, (fun x => g • x) = (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x
<VAR>g : SL(2, ℝ)<VAR>hc : ↑↑g 1 0 ≠ 0<VAR>h_denom : ∀ (z : ℍ), denom (toGLPos g) z ≠ 0<GOAL>∃ u v w, (fun x => g • x) = (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x
<VAR>a b c d : ℝ<VAR>h : a * d - b * c = 1<VAR>hc : ↑↑⟨!![a, b; c, d], ⋯⟩ 1 0 ≠ 0<VAR>h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0<GOAL>∃ u v w, (fun x => ⟨!![a, b; c, d], ⋯⟩ • x) = (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x
<VAR>a b c d : ℝ<VAR>h : a * d - b * c = 1<VAR>h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0<VAR>hc : c ≠ 0<GOAL>∃ u v w, (fun x => ⟨!![a, b; c, d], ⋯⟩ • x) = (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x
<VAR>a b c d : ℝ<VAR>h : a * d - b * c = 1<VAR>h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0<VAR>hc : c ≠ 0<GOAL>(fun x => ⟨!![a, b; c, d], ⋯⟩ • x) = (fun x => a / c +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => c * d +ᵥ x) ∘ fun x => ⟨c * c, ⋯⟩ • x
<VAR>a b c d : ℝ<VAR>h : a * d - b * c = 1<VAR>h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0<VAR>hc : c ≠ 0<VAR>z : ℂ<VAR>hz : 0 < z.im<GOAL>↑(⟨!![a, b; c, d], ⋯⟩ • ⟨z, hz⟩) = ↑(((fun x => a / c +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => c * d +ᵥ x) ∘ fun x => ⟨c * c, ⋯⟩ • x) ⟨z, hz⟩)
<VAR>a b c d : ℝ<VAR>h : a * d - b * c = 1<VAR>h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0<VAR>hc : c ≠ 0<VAR>z : ℂ<VAR>hz : 0 < z.im<GOAL>(↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
<VAR>a b c d : ℝ<VAR>h : a * d - b * c = 1<VAR>z : ℂ<VAR>hz : 0 < z.im<VAR>hc : ↑c ≠ 0<VAR>h_denom : ↑c * z + ↑d ≠ 0<GOAL>(↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
<VAR>a b c d : ℝ<VAR>h : a * d - b * c = 1<VAR>z : ℂ<VAR>hz : 0 < z.im<VAR>hc : ↑c ≠ 0<VAR>h_denom : ↑c * z + ↑d ≠ 0<VAR>h_aux : ↑c * ↑d + ↑c * ↑c * z ≠ 0<GOAL>(↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
<VAR>a b c d : ℝ<VAR>z : ℂ<VAR>hz : 0 < z.im<VAR>hc : ↑c ≠ 0<VAR>h_denom : ↑c * z + ↑d ≠ 0<VAR>h_aux : ↑c * ↑d + ↑c * ↑c * z ≠ 0<VAR>h : ↑a * ↑d - ↑b * ↑c = 1<GOAL>(↑a * z + ↑b) * (↑c * (↑c * ↑d + ↑c * ↑c * z)) = (↑a * (↑c * ↑d + ↑c * ↑c * z) - ↑c) * (↑c * z + ↑d)
<VAR>z : ℂ<GOAL>(z - (starRingEnd ℂ) z).re = (↑(2 * z.im) * I).re ∧ (z - (starRingEnd ℂ) z).im = (↑(2 * z.im) * I).im
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>r : R<VAR>a b c : A<VAR>h₁ : (↑ₐ r - a) * b = 1<VAR>h₂ : c * (↑ₐ r - a) = 1<GOAL>b * (↑ₐ r - a) = 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✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : ¬IsOfFinOrder x<GOAL>orderOf x = 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>∀ᵐ (x : α) ∂μ, ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>w : Set ℝ≥0∞<VAR>w_count : w.Countable<VAR>w_dense : Dense w<VAR>left✝ : 0 ∉ w<VAR>w_top : ⊤ ∉ w<GOAL>∀ᵐ (x : α) ∂μ, ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>w : Set ℝ≥0∞<VAR>w_count : w.Countable<VAR>w_dense : Dense w<VAR>left✝ : 0 ∉ w<VAR>w_top : ⊤ ∉ w<VAR>I : ∀ x ∈ w, x ≠ ⊤<VAR>A : ∀ c ∈ w, ∀ d ∈ w, c < d → ∀ᵐ (x : α) ∂μ, ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)<GOAL>∀ᵐ (x : α) ∂μ, ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>w : Set ℝ≥0∞<VAR>w_count : w.Countable<VAR>w_dense : Dense w<VAR>left✝ : 0 ∉ w<VAR>w_top : ⊤ ∉ w<VAR>I : ∀ x ∈ w, x ≠ ⊤<VAR>A : ∀ c ∈ w, ∀ d ∈ w, c < d → ∀ᵐ (x : α) ∂μ, ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)<VAR>B : ∀ᵐ (x : α) ∂μ, ∀ c ∈ w, ∀ d ∈ w, c < d → ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)<GOAL>∀ᵐ (x : α) ∂μ, ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>w : Set ℝ≥0∞<VAR>w_count : w.Countable<VAR>w_dense : Dense w<VAR>left✝ : 0 ∉ w<VAR>w_top : ⊤ ∉ w<VAR>I : ∀ x ∈ w, x ≠ ⊤<VAR>A : ∀ c ∈ w, ∀ d ∈ w, c < d → ∀ᵐ (x : α) ∂μ, ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)<VAR>B : ∀ᵐ (x : α) ∂μ, ∀ c ∈ w, ∀ d ∈ w, c < d → ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)<GOAL>∀ (a : α), (∀ c ∈ w, ∀ d ∈ w, c < d → ¬((∃ᶠ (a : Set α) in v.filterAt a, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt a, d < ρ a / μ a)) → ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 c)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>w : Set ℝ≥0∞<VAR>w_count : w.Countable<VAR>w_dense : Dense w<VAR>left✝ : 0 ∉ w<VAR>w_top : ⊤ ∉ w<VAR>I : ∀ x ∈ w, x ≠ ⊤<VAR>A : ∀ c ∈ w, ∀ d ∈ w, c < d → ∀ᵐ (x : α) ∂μ, ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)<VAR>B : ∀ᵐ (x : α) ∂μ, ∀ c ∈ w, ∀ d ∈ w, c < d → ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)<VAR>x : α<VAR>hx : ∀ c ∈ w, ∀ d ∈ w, c < d → ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)<GOAL>∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x y : ModP K v O hv p<VAR>hxy0 : x * y ≠ 0<GOAL>preVal K v O hv p (x * y) = preVal K v O hv p x * preVal K v O hv p y
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x y : ModP K v O hv p<VAR>hxy0 : x * y ≠ 0<VAR>hx0 : x ≠ 0<GOAL>preVal K v O hv p (x * y) = preVal K v O hv p x * preVal K v O hv p y
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x y : ModP K v O hv p<VAR>hxy0 : x * y ≠ 0<VAR>hx0 : x ≠ 0<VAR>hy0 : y ≠ 0<GOAL>preVal K v O hv p (x * y) = preVal K v O hv p x * preVal K v O hv p y
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>y : ModP K v O hv p<VAR>hy0 : y ≠ 0<VAR>r : O<VAR>hxy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r * y ≠ 0<VAR>hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0<GOAL>preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) r * y) = preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) * preVal K v O hv p y
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0<VAR>s : O<VAR>hy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0<VAR>hxy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r * (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0<GOAL>preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) r * (Ideal.Quotient.mk (Ideal.span {↑p})) s) = preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) * preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) s)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0<VAR>s : O<VAR>hy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0<VAR>hxy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0<GOAL>preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) (r * s)) = preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) r) * preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) s)
<VAR>m n a b c d : ℤ<GOAL>a ≡ b [ZMOD n] ↔ n ∣ b - a
<VAR>m n a b c d : ℤ<GOAL>b % n = a % n ↔ n ∣ b - a
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>c d : C<VAR>f : c ⟶ d<VAR>γ : c ⟶ c<GOAL>(fun δ => f ≫ δ ≫ inv f) ((fun γ => inv f ≫ γ ≫ f) γ) = γ
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>c d : C<VAR>f : c ⟶ d<VAR>δ : d ⟶ d<GOAL>(fun γ => inv f ≫ γ ≫ f) ((fun δ => f ≫ δ ≫ inv f) δ) = δ
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>c d : C<VAR>f : c ⟶ d<VAR>γ₁ γ₂ : c ⟶ c<GOAL>{ toFun := fun γ => inv f ≫ γ ≫ f, invFun := fun δ => f ≫ δ ≫ inv f, left_inv := ⋯, right_inv := ⋯ }.toFun (γ₁ * γ₂) = { toFun := fun γ => inv f ≫ γ ≫ f, invFun := fun δ => f ≫ δ ≫ inv f, left_inv := ⋯, right_inv := ⋯ }.toFun γ₁ * { toFun := fun γ => inv f ≫ γ ≫ f, invFun := fun δ => f ≫ δ ≫ inv f, left_inv := ⋯, right_inv := ⋯ }.toFun γ₂
<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 α<VAR>s t : Finset α<GOAL>s ∩ filter p t = filter p (s ∩ t)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : Algebra.IsAlgebraic K L<GOAL>IsLocalization (algebraMapSubmonoid C A⁰) L
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : Algebra.IsAlgebraic K L<VAR>this : IsDomain C<GOAL>IsLocalization (algebraMapSubmonoid C A⁰) L
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : Algebra.IsAlgebraic K L<VAR>this✝ : IsDomain C<VAR>this : NoZeroSMulDivisors A L<GOAL>IsLocalization (algebraMapSubmonoid C A⁰) L
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : Algebra.IsAlgebraic K L<VAR>this✝¹ : IsDomain C<VAR>this✝ : NoZeroSMulDivisors A L<VAR>this : NoZeroSMulDivisors A C<GOAL>IsLocalization (algebraMapSubmonoid C A⁰) L
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : ∑ i ∈ s, f i ^ p ≤ 1<VAR>hg : ∑ i ∈ s, g i ^ q ≤ 1<GOAL>∑ i ∈ s, f i * g i ≤ 1
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : ∑ i ∈ s, f i ^ p ≤ 1<VAR>hg : ∑ i ∈ s, g i ^ q ≤ 1<VAR>hp_ne_zero : p.toNNReal ≠ 0<GOAL>∑ i ∈ s, f i * g i ≤ 1
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : ∑ i ∈ s, f i ^ p ≤ 1<VAR>hg : ∑ i ∈ s, g i ^ q ≤ 1<VAR>hp_ne_zero : p.toNNReal ≠ 0<VAR>hq_ne_zero : q.toNNReal ≠ 0<GOAL>∑ i ∈ s, f i * g i ≤ 1
<VAR>I : Type u<VAR>inst✝¹¹ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝¹⁰ : Category.{u_2, u_1} C<VAR>inst✝⁹ : MonoidalCategory C<VAR>inst✝⁸ : DecidableEq I<VAR>inst✝⁷ : HasInitial C<VAR>inst✝⁶ : (X₁ : C) → PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)<VAR>inst✝⁵ : (X₂ : C) → PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)<VAR>X₁ X₃ : GradedObject I C<VAR>inst✝⁴ : X₁.HasTensor X₃<VAR>inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃<VAR>inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)<VAR>inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃<VAR>inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃<GOAL>(associator X₁ tensorUnit X₃).hom ≫ tensorHom (𝟙 X₁) (leftUnitor X₃).hom = tensorHom (rightUnitor X₁).hom (𝟙 X₃)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝² : Category.{u_4, u_3} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' j' : ι'<VAR>j : ι<VAR>hj : e.f j = j'<VAR>hj' : ¬c.Rel (c.prev j) j<GOAL>(K.extend e).d i' j' = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝² : Category.{u_4, u_3} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' j' : ι'<VAR>j : ι<VAR>hj : e.f j = j'<VAR>hj' : ¬c.Rel (c.prev j) j<VAR>hi' : e.r i' = none<GOAL>(K.extend e).d i' j' = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝² : Category.{u_4, u_3} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' j' : ι'<VAR>j : ι<VAR>hj : e.f j = j'<VAR>hj' : ¬c.Rel (c.prev j) j<VAR>i : ι<VAR>hi : e.r i' = some i<GOAL>(K.extend e).d i' j' = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex ℝ t<VAR>ht₂ : IsClosed t<VAR>disj : Disjoint s t<GOAL>∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>t : Set E<VAR>x y : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>ht₁ : Convex ℝ t<VAR>ht₂ : IsClosed t<VAR>hs₁ : Convex ℝ ∅<VAR>hs₂ : IsCompact ∅<VAR>disj : Disjoint ∅ t<GOAL>∃ f u v, (∀ a ∈ ∅, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex ℝ t<VAR>ht₂ : IsClosed t<VAR>disj : Disjoint s t<VAR>hs : s.Nonempty<GOAL>∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>x y : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsCompact s<VAR>hs : s.Nonempty<VAR>ht₁ : Convex ℝ ∅<VAR>ht₂ : IsClosed ∅<VAR>disj : Disjoint s ∅<GOAL>∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ ∅, v < f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex ℝ t<VAR>ht₂ : IsClosed t<VAR>disj : Disjoint s t<VAR>hs : s.Nonempty<VAR>_ht : t.Nonempty<GOAL>∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex ℝ t<VAR>ht₂ : IsClosed t<VAR>disj : Disjoint s t<VAR>hs : s.Nonempty<VAR>_ht : t.Nonempty<VAR>U V : Set E<VAR>hU : IsOpen U<VAR>hV : IsOpen V<VAR>hU₁ : Convex ℝ U<VAR>hV₁ : Convex ℝ V<VAR>sU : s ⊆ U<VAR>tV : t ⊆ V<VAR>disj' : Disjoint U V<GOAL>∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b