ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↥(pbo f)<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra<GOAL>IsLocalization ((toSpec 𝒜 f).val.base x).asIdeal.primeCompl (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>h₀ : ¬R = 0<GOAL>CircleIntegrable f c R ↔ IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>h₀ : ¬R = 0<VAR>h : IntervalIntegrable (fun θ => deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π)<GOAL>CircleIntegrable f c R
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>h₀ : ¬R = 0<VAR>h : IntegrableOn (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume<GOAL>IntegrableOn (fun θ => f (circleMap c R θ)) (Ι 0 (2 * π)) volume
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>h₀ : ¬R = 0<VAR>h : IntegrableOn (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume<GOAL>AEStronglyMeasurable (fun θ => f (circleMap c R θ)) (volume.restrict (Ι 0 (2 * π)))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>h₀ : ¬R = 0<VAR>h : IntegrableOn (fun θ => (circleMap 0 R θ * I) • f (circleMap c R θ)) (Ι 0 (2 * π)) volume<GOAL>∀ᵐ (a : ℝ) ∂volume.restrict (Ι 0 (2 * π)), ‖f (circleMap c R a)‖ ≤ |R|⁻¹ * ‖(circleMap 0 R a * I) • f (circleMap c R a)‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : min c d < b<GOAL>Iic b ∪ Ioc c d = Iic (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hcd : c ≤ d<VAR>h : c < b<GOAL>Iic b ∪ Ioc c d = Iic (max b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>hcd : d ≤ c<VAR>h : d < b<GOAL>Iic b ∪ Ioc c d = Iic (max b d)
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>hf : LSeriesSummable f s<VAR>hg : LSeriesSummable g s<GOAL>LSeries (f - g) s = LSeries f s - LSeries g s
<VAR>f g : ℝ → ℝ<VAR>f' g' x y p : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hg : HasDerivWithinAt g g' s x<VAR>h : 0 < f x<GOAL>HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) s x
<VAR>f g : ℝ → ℝ<VAR>f' g' x y p : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hg : HasDerivWithinAt g g' s x<VAR>h : 0 < f x<GOAL>f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) = ((g x * f x ^ (g x - 1)) • ContinuousLinearMap.smulRight 1 f' + (f x ^ g x * Real.log (f x)) • ContinuousLinearMap.smulRight 1 g') 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)<GOAL>∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : BorelSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>f : δ → α<VAR>hf : ∀ (x : α), MeasurableSet (f ⁻¹' Iic x)<GOAL>∀ (x : α), MeasurableSet (f ⁻¹' Iic x)
<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>f : α →ₛ E<VAR>hfi : Memℒp (↑f) p μ<GOAL>↑(toSimpleFunc (toLp f hfi)) =ᶠ[ae μ] ↑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>f : α →ₛ E<VAR>hfi : Memℒp (↑f) p μ<GOAL>AEEqFun.mk ↑(toSimpleFunc (toLp f hfi)) ?m.235803 = AEEqFun.mk ↑f ?m.235804
<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>f : α →ₛ E<VAR>hfi : Memℒp (↑f) p μ<GOAL>AEStronglyMeasurable (↑(toSimpleFunc (toLp f hfi))) μ
<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>f : α →ₛ E<VAR>hfi : Memℒp (↑f) p μ<GOAL>AEStronglyMeasurable (↑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PredOrder α<VAR>a b : α<VAR>inst✝ : NoMinOrder α<VAR>h : a < b<GOAL>Ioo (pred a) b = insert a (Ioo a b)
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>r : R → R → Prop<VAR>inst✝ : StarRing R<VAR>hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)<VAR>a b : R<VAR>h : Rel r a b<GOAL>Rel r (Star.star a) (Star.star b)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R r : ℝ<VAR>hr : r < R<VAR>z : ℂ<GOAL>ContinuousOn (fun w => (circleMap z R w.2 - w.1)⁻¹ ^ 2) (closedBall z r ×ˢ univ)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R r : ℝ<VAR>hr : r < R<VAR>z : ℂ<GOAL>ContinuousOn (fun w => (1 / (circleMap z R w.2 - w.1)) ^ 2) (closedBall z r ×ˢ univ)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R r : ℝ<VAR>hr : r < R<VAR>z : ℂ<GOAL>ContinuousOn (fun x => circleMap z R x.2 - x.1) (closedBall z r ×ˢ univ)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R r : ℝ<VAR>hr : r < R<VAR>z : ℂ<GOAL>∀ x ∈ closedBall z r ×ˢ univ, circleMap z R x.2 - x.1 ≠ 0
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M✝ : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>R : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>M : Matrix n' n R<GOAL>M * (toMatrix₂' R) B = (toMatrix₂' R) (B ∘ₗ toLin' Mᵀ)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>p : β → Prop<VAR>μ : Measure α<GOAL>(∀ᵐ (x : β) ∂Measure.map f μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p (f x)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.dblY P = (P x ^ 2) ^ 3
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Ring R<VAR>toFinsupp✝ : R[ℕ]<GOAL>(-{ toFinsupp := toFinsupp✝ }).support = { toFinsupp := toFinsupp✝ }.support
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Ring R<VAR>toFinsupp✝ : R[ℕ]<GOAL>(match { toFinsupp := -toFinsupp✝ } with | { toFinsupp := p } => p.support) = match { toFinsupp := toFinsupp✝ } with | { toFinsupp := p } => p.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>R✝ : Type u_3<VAR>S✝ : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommRing S<VAR>abv : AbsoluteValue R S<VAR>a b : R<GOAL>abv b - abv a ≤ abv (a - b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>R✝ : Type u_3<VAR>S✝ : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommRing S<VAR>abv : AbsoluteValue R S<VAR>a b : R<GOAL>abv b - abv a ≤ abv (b - a)
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Group M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<VAR>x : R<VAR>h : x ∈ a • S<GOAL>a⁻¹ • x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Group M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<VAR>x : R<VAR>h : a⁻¹ • x ∈ S<GOAL>x ∈ a • S
<VAR>n : ℤ<VAR>z τ : ℂ<GOAL>‖jacobiTheta₂_term n z τ‖ = rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)
<VAR>n : ℤ<VAR>z τ : ℂ<GOAL>rexp (-(π * (2 * ↑n) * z.im) + -(π * ↑n ^ 2 * τ.im)) = rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝³ : Ring R₂<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : p ≤ ker f<GOAL>range (p.liftQ f h) = range f
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q : ℝ≥0<VAR>p : ℝ≥0∞<VAR>inst✝ : Fact (1 ≤ p)<GOAL>p = ⊤ ∨ 0 < p.toReal ∧ 1 ≤ p.toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>this : (f * g - 0).LimZero<VAR>hlz : (f * g).LimZero<VAR>hf' : ¬f.LimZero<VAR>hg' : ¬g.LimZero<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>this : (f * g - 0).LimZero<VAR>hlz : (f * g).LimZero<VAR>hf' : ¬f.LimZero<VAR>hg' : ¬g.LimZero<VAR>a1 : α<VAR>ha1 : a1 > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>this : (f * g - 0).LimZero<VAR>hlz : (f * g).LimZero<VAR>hf' : ¬f.LimZero<VAR>hg' : ¬g.LimZero<VAR>a1 : α<VAR>ha1 : a1 > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)<VAR>a2 : α<VAR>ha2 : a2 > 0<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>this✝ : (f * g - 0).LimZero<VAR>hlz : (f * g).LimZero<VAR>hf' : ¬f.LimZero<VAR>hg' : ¬g.LimZero<VAR>a1 : α<VAR>ha1 : a1 > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)<VAR>a2 : α<VAR>ha2 : a2 > 0<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)<VAR>this : 0 < a1 * a2<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, abv (↑(f * g) j) < a1 * a2<VAR>i : ℕ := max N (max N1 N2)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>this✝ : (f * g - 0).LimZero<VAR>hlz : (f * g).LimZero<VAR>hf' : ¬f.LimZero<VAR>hg' : ¬g.LimZero<VAR>a1 : α<VAR>ha1 : a1 > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)<VAR>a2 : α<VAR>ha2 : a2 > 0<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)<VAR>this : 0 < a1 * a2<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, abv (↑(f * g) j) < a1 * a2<VAR>i : ℕ := max N (max N1 N2)<VAR>hN' : abv (↑(f * g) i) < a1 * a2<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>this✝ : (f * g - 0).LimZero<VAR>hlz : (f * g).LimZero<VAR>hf' : ¬f.LimZero<VAR>hg' : ¬g.LimZero<VAR>a1 : α<VAR>ha1 : a1 > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)<VAR>a2 : α<VAR>ha2 : a2 > 0<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)<VAR>this : 0 < a1 * a2<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, abv (↑(f * g) j) < a1 * a2<VAR>i : ℕ := max N (max N1 N2)<VAR>hN' : abv (↑(f * g) i) < a1 * a2<VAR>hN1' : a1 ≤ abv (↑f i)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>this✝ : (f * g - 0).LimZero<VAR>hlz : (f * g).LimZero<VAR>hf' : ¬f.LimZero<VAR>hg' : ¬g.LimZero<VAR>a1 : α<VAR>ha1 : a1 > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)<VAR>a2 : α<VAR>ha2 : a2 > 0<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)<VAR>this : 0 < a1 * a2<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, abv (↑(f * g) j) < a1 * a2<VAR>i : ℕ := max N (max N1 N2)<VAR>hN' : abv (↑(f * g) i) < a1 * a2<VAR>hN1'✝ : a1 ≤ abv (↑f i)<VAR>hN1' : a2 ≤ abv (↑g i)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>this✝ : (f * g - 0).LimZero<VAR>hlz : (f * g).LimZero<VAR>hf' : ¬f.LimZero<VAR>hg' : ¬g.LimZero<VAR>a1 : α<VAR>ha1 : a1 > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)<VAR>a2 : α<VAR>ha2 : a2 > 0<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)<VAR>this : 0 < a1 * a2<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, abv (↑(f * g) j) < a1 * a2<VAR>i : ℕ := max N (max N1 N2)<VAR>hN' : abv (↑(f * g) i) < a1 * a2<VAR>hN1'✝ : a1 ≤ abv (↑f i)<VAR>hN1' : a2 ≤ abv (↑g i)<GOAL>a1 * a2 ≤ abv (↑(f * g) i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>this✝ : (f * g - 0).LimZero<VAR>hlz : (f * g).LimZero<VAR>hf' : ¬f.LimZero<VAR>hg' : ¬g.LimZero<VAR>a1 : α<VAR>ha1 : a1 > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)<VAR>a2 : α<VAR>ha2 : a2 > 0<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)<VAR>this : 0 < a1 * a2<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, abv (↑(f * g) j) < a1 * a2<VAR>i : ℕ := max N (max N1 N2)<VAR>hN' : abv (↑(f * g) i) < a1 * a2<VAR>hN1'✝ : a1 ≤ abv (↑f i)<VAR>hN1' : a2 ≤ abv (↑g i)<GOAL>a1 * a2 ≤ abv (↑f i * ↑g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>this✝ : (f * g - 0).LimZero<VAR>hlz : (f * g).LimZero<VAR>hf' : ¬f.LimZero<VAR>hg' : ¬g.LimZero<VAR>a1 : α<VAR>ha1 : a1 > 0<VAR>N1 : ℕ<VAR>hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)<VAR>a2 : α<VAR>ha2 : a2 > 0<VAR>N2 : ℕ<VAR>hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)<VAR>this : 0 < a1 * a2<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, abv (↑(f * g) j) < a1 * a2<VAR>i : ℕ := max N (max N1 N2)<VAR>hN' : abv (↑(f * g) i) < a1 * a2<VAR>hN1'✝ : a1 ≤ abv (↑f i)<VAR>hN1' : a2 ≤ abv (↑g i)<GOAL>a1 * a2 ≤ abv (↑f i) * abv (↑g i)
<VAR>m n✝ : ℕ<VAR>i : Fin (n✝ + 1 + 1)<GOAL>(finRotate (n✝ + 1 + 1)) i = i + 1
<VAR>m n✝ : ℕ<GOAL>(finRotate (n✝ + 1 + 1)) (Fin.last (n✝ + 1)) = Fin.last (n✝ + 1) + 1
<VAR>m n✝ : ℕ<VAR>i : Fin (n✝ + 1 + 1)<VAR>h : i < Fin.last (n✝ + 1)<GOAL>(finRotate (n✝ + 1 + 1)) i = i + 1
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>x y : P<GOAL>spanSingleton S x * spanSingleton S y = spanSingleton S (x * y)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>x y : P<GOAL>(fun I => ↑I) (spanSingleton S x * spanSingleton S y) = (fun I => ↑I) (spanSingleton S (x * y))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>b : ι<GOAL>∀ a < b, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>b : ι<GOAL>∀ (x : ι), (∀ y < x, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0) → ∀ a < x, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>b✝ b : ι<VAR>ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0<VAR>a : ι<VAR>h₀ : a < b<GOAL>⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>b✝ b : ι<VAR>ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0<VAR>a : ι<VAR>h₀ : a < b<GOAL>⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 - ∑ x ∈ Iio b, ⟪gramSchmidt 𝕜 f x, f b⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f x‖ ^ 2) * ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>b✝ b : ι<VAR>ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0<VAR>a : ι<VAR>h₀ : a < b<GOAL>⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 - ⟪gramSchmidt 𝕜 f a, f b⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f a‖ ^ 2) * ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f a⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>b✝ b : ι<VAR>ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0<VAR>a : ι<VAR>h₀ : a < b<GOAL>∀ b_1 ∈ Iio b, b_1 ≠ a → ⟪gramSchmidt 𝕜 f b_1, f b⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f b_1‖ ^ 2) * ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b_1⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>b✝ b : ι<VAR>ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0<VAR>a : ι<VAR>h₀ : a < b<VAR>i : ι<VAR>hi : i ∈ Iio b<VAR>hia : i ≠ a<GOAL>⟪gramSchmidt 𝕜 f i, f b⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f i‖ ^ 2) * ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>b✝ b : ι<VAR>ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0<VAR>a : ι<VAR>h₀ : a < b<VAR>i : ι<VAR>hi : i ∈ Iio b<VAR>hia : i ≠ a<GOAL>(⟪gramSchmidt 𝕜 f i, f b⟫_𝕜 = 0 ∨ ↑(‖gramSchmidt 𝕜 f i‖ ^ 2) = 0) ∨ ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>b✝ b : ι<VAR>ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0<VAR>a : ι<VAR>h₀ : a < b<VAR>i : ι<VAR>hi : i ∈ Iio b<VAR>hia : i ≠ a<GOAL>⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>b✝ b : ι<VAR>ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0<VAR>a : ι<VAR>h₀ : a < b<VAR>i : ι<VAR>hi : i ∈ Iio b<VAR>hia : i ≠ a<VAR>hia₁ : i < a<GOAL>⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>b✝ b : ι<VAR>ih : ∀ y < b, ∀ a < y, ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f y⟫_𝕜 = 0<VAR>a : ι<VAR>h₀ : a < b<VAR>i : ι<VAR>hi : i ∈ Iio b<VAR>hia : i ≠ a<VAR>hia₂ : a < i<GOAL>⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f i⟫_𝕜 = 0
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>S : Ideal R<VAR>inst✝ : IsPrincipal S<VAR>x a : R<GOAL>x = a • generator S ↔ x = generator S * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<GOAL>x = yᶜ ↔ y = xᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<GOAL>∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ⊤
<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>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>s ×ˢ t = ⋃ b ∈ t, (fun a => (a, b)) '' s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>hs : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<GOAL>0 < gauge s x ↔ x ≠ 0
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<VAR>l : Dual R M<VAR>i : ι<GOAL>b.dualBasis.equivFun l i = l (b i)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B I✝ J✝ X✝ Y✝ : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<VAR>hY : autoParam (Y ⊆ M.E) _auto✝<VAR>J : Set α<VAR>hJ : M.Basis J Y<VAR>I : Set α<VAR>hI : M.Basis I (X ∪ Y) ∧ I ∩ Y = J<GOAL>M.Basis (I ∩ Y) Y
<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>c x y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hy : y ≠ c<GOAL>inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c ∧ x ≠ c