ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype ι'<VAR>F' : ι → Type u_5<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)<GOAL>HasFTaylorSeriesUpToOn n Φ P' s ↔ ∀ (i : ι), HasFTaylorSeriesUpToOn n (fun x => Φ x i) (fun x m => (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x m)) s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype ι'<VAR>F' : ι → Type u_5<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)<VAR>x✝¹ : E<VAR>x✝ : ℕ<GOAL>P' x✝¹ x✝ = ContinuousMultilinearMap.pi fun i => (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x✝¹ x✝)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>pn : xz a1 n * xz a1 n - ↑(Pell.d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n<GOAL>↑(xn a1 n * xn a1 n) - ↑(Pell.d a1 * yn a1 n * yn a1 n) = 1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>pn : xz a1 n * xz a1 n - ↑(Pell.d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n<VAR>h : ↑(xn a1 n * xn a1 n) - ↑(Pell.d a1 * yn a1 n * yn a1 n) = 1<VAR>hl : Pell.d a1 * yn a1 n * yn a1 n ≤ xn a1 n * xn a1 n<GOAL>↑(xn a1 n * xn a1 n - Pell.d a1 * yn a1 n * yn a1 n) = ↑1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>pn : xz a1 n * xz a1 n - ↑(Pell.d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n<VAR>h : ↑(xn a1 n * xn a1 n) - ↑(Pell.d a1 * yn a1 n * yn a1 n) = 1<VAR>hl : Pell.d a1 * yn a1 n * yn a1 n ≤ xn a1 n * xn a1 n<GOAL>↑(xn a1 n * xn a1 n) - ↑(Pell.d a1 * yn a1 n * yn a1 n) = ↑1
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<GOAL>S.disconnect ≤ S
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<GOAL>∀ {c d : C}, S.disconnect.arrows c d ⊆ S.arrows c d
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : CompleteSpace (α × β)<VAR>h : Nonempty α<VAR>f✝ : Filter β<VAR>hf : Cauchy f✝<VAR>x a : α<VAR>b : β<VAR>hab : pure x ×ˢ f✝ ≤ 𝓝 (a, b)<GOAL>f✝ ≤ 𝓝 b
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c a : G₀<GOAL>a / (a * a) = a⁻¹⁻¹ * a⁻¹ * a⁻¹
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommRing P<VAR>a c : R<VAR>b d : ↥M<GOAL>mk a b - mk c d = mk (↑d * a - ↑b * c) (b * d)
<VAR>q : ℚ<VAR>x y : ℝ<VAR>n : ℕ<VAR>h : Irrational (x ^ ↑n)<GOAL>Irrational x
<VAR>q : ℚ<VAR>x y : ℝ<VAR>n : ℕ<VAR>h : Irrational (x ^ n)<GOAL>Irrational x
<VAR>q : ℚ<VAR>x y : ℝ<VAR>n : ℕ<VAR>h : Irrational (x ^ -[n+1])<GOAL>Irrational x
<VAR>q : ℚ<VAR>x y : ℝ<VAR>n : ℕ<VAR>h : Irrational (x ^ (n + 1))⁻¹<GOAL>Irrational x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ✝ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ✝<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : α<GOAL>ρ.condKernel a = (const Unit ρ).condKernelUnitBorel ((), a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁵ : CountablyGenerated γ<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ✝ : Measure (α × Ω)<VAR>inst✝¹ : IsFiniteMeasure ρ✝<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>a : α<GOAL>((const Unit ρ).condKernelUnitBorel.comap (fun a => ((), a)) ⋯) a = (const Unit ρ).condKernelUnitBorel ((), a)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>inst✝ : DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a : Sigma α<VAR>b : Sigma β<VAR>x : Sigma γ<VAR>h : a.fst ≠ x.fst<GOAL>x ∉ sigmaLift f a b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>inst✝ : DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a : Sigma α<VAR>b : Sigma β<VAR>x : Sigma γ<VAR>h : a.fst ≠ x.fst<GOAL>¬∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<GOAL>(s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<GOAL>(∃ x, ∃ a ∈ s, x ∈ t a) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<GOAL>(∃ y x, y ∈ s ∧ x ∈ t y) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x
<VAR>s : ℝ<VAR>hs : -1 ≤ s<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>1 + p * s ≤ (1 + s) ^ p
<VAR>s : ℝ<VAR>hs : -1 ≤ s<VAR>hp : 1 ≤ 1<GOAL>1 + 1 * s ≤ (1 + s) ^ 1
<VAR>s : ℝ<VAR>hs : -1 ≤ s<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<GOAL>1 + p * s ≤ (1 + s) ^ p
<VAR>s : ℝ<VAR>hs : -1 ≤ s<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>hs' : ¬s = 0<GOAL>1 + p * s ≤ (1 + s) ^ p
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>x : ι → ℝ<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)<VAR>h₁ : π₁.IsHenstock<VAR>h₂ : π₂.IsHenstock<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>(π₁.disjUnion π₂ h).IsHenstock
<VAR>ι : Type u_1<VAR>I J✝ : Box ι<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>x : ι → ℝ<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)<VAR>h₁ : π₁.IsHenstock<VAR>h₂ : π₂.IsHenstock<VAR>h : Disjoint π₁.iUnion π₂.iUnion<VAR>J : Box ι<VAR>hJ✝ : J ∈ π₁.disjUnion π₂ h<VAR>hJ : J ∈ π₁.boxes<GOAL>(π₁.disjUnion π₂ h).tag J ∈ Box.Icc J
<VAR>ι : Type u_1<VAR>I J✝ : Box ι<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>x : ι → ℝ<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)<VAR>h₁ : π₁.IsHenstock<VAR>h₂ : π₂.IsHenstock<VAR>h : Disjoint π₁.iUnion π₂.iUnion<VAR>J : Box ι<VAR>hJ✝ : J ∈ π₁.disjUnion π₂ h<VAR>hJ : J ∈ π₂.boxes<GOAL>(π₁.disjUnion π₂ h).tag J ∈ Box.Icc J
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t✝ u✝ : Set E<VAR>x y : E<VAR>s t u : Set E<GOAL>convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 s (convexJoin 𝕜 t u)
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t✝ u✝ : Set E<VAR>x y : E<VAR>s t u : Set E<GOAL>convexJoin 𝕜 s (convexJoin 𝕜 t u) ⊆ convexJoin 𝕜 (convexJoin 𝕜 s t) u
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t✝ u✝ : Set E<VAR>x y : E<VAR>s t u : Set E<GOAL>convexJoin 𝕜 (convexJoin 𝕜 u t) s ⊆ convexJoin 𝕜 u (convexJoin 𝕜 t s)
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n✝ : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<VAR>n : ℕ<GOAL>f x ≤ f 1 + x * log (↑n + 1) - x * log ↑n + logGammaSeq x n
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n✝ : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<VAR>n : ℕ<GOAL>f (↑(n + 1) + x) ≤ f 1 + x * log (↑n + 1) - x * log ↑n + (x * log ↑n + log ↑n !)
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n✝ : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<VAR>n : ℕ<GOAL>f ↑(n + 1) + x * log ↑(n + 1) = f 1 + x * log (↑n + 1) - x * log ↑n + (x * log ↑n + log ↑n !)
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n✝ : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<VAR>n : ℕ<GOAL>f 1 + log ↑n ! + x * log (↑n + 1) = f 1 + x * log (↑n + 1) - x * log ↑n + (x * log ↑n + log ↑n !)
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v : Valuation R Γ₀<VAR>x✝ y✝ z x y : R<GOAL>v (x + y) ≤ v x ∨ v (x + y) ≤ v y
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v : Valuation R Γ₀<VAR>x✝ y✝ z x y : R<GOAL>max (v x) (v y) ≥ v (x + y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : Ordinal.{u} → Ordinal.{max u v}<VAR>x✝ : (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o<VAR>h₁ : ∀ (a : Ordinal.{u}), f a < f (succ a)<VAR>h₂ : ∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>a : Ordinal.{max u v}<GOAL>(o.bsup fun x x_1 => f x) ≤ a ↔ ∀ b < o, f b ≤ a
<VAR>X✝ X Y : LocallyRingedSpace<VAR>e : X ≅ Y<GOAL>e.inv.val.base ≫ e.hom.val.base = 𝟙 ↑Y.toPresheafedSpace
<VAR>X✝ X Y : LocallyRingedSpace<VAR>e : X ≅ Y<GOAL>(e.inv ≫ e.hom).val.base = 𝟙 ↑Y.toPresheafedSpace
<VAR>M₀ : Type u_1<VAR>inst✝⁷ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁶ : MonoidWithZero M<VAR>inst✝⁵ : MonoidWithZero M'<VAR>inst✝⁴ : CommMonoidWithZero M₁<VAR>inst✝³ : Ring R<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : FunLike F M M'<VAR>inst✝ : Finite R<VAR>a : R<GOAL>IsUnit a ↔ a ∈ R⁰
<VAR>M₀ : Type u_1<VAR>inst✝⁷ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁶ : MonoidWithZero M<VAR>inst✝⁵ : MonoidWithZero M'<VAR>inst✝⁴ : CommMonoidWithZero M₁<VAR>inst✝³ : Ring R<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : FunLike F M M'<VAR>inst✝ : Finite R<VAR>a : R<VAR>ha : a ∈ R⁰<GOAL>IsUnit a
<VAR>M₀ : Type u_1<VAR>inst✝⁷ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁶ : MonoidWithZero M<VAR>inst✝⁵ : MonoidWithZero M'<VAR>inst✝⁴ : CommMonoidWithZero M₁<VAR>inst✝³ : Ring R<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : FunLike F M M'<VAR>inst✝ : Finite R<VAR>a : R<VAR>ha : a ∈ R⁰<GOAL>Function.Injective fun x => x * a
<VAR>M₀ : Type u_1<VAR>inst✝⁷ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁶ : MonoidWithZero M<VAR>inst✝⁵ : MonoidWithZero M'<VAR>inst✝⁴ : CommMonoidWithZero M₁<VAR>inst✝³ : Ring R<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : FunLike F M M'<VAR>inst✝ : Finite R<VAR>a : R<VAR>ha : a ∈ R⁰<VAR>b c : R<VAR>hbc : (fun x => x * a) b = (fun x => x * a) c<GOAL>b = c
<VAR>M₀ : Type u_1<VAR>inst✝⁷ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁶ : MonoidWithZero M<VAR>inst✝⁵ : MonoidWithZero M'<VAR>inst✝⁴ : CommMonoidWithZero M₁<VAR>inst✝³ : Ring R<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : FunLike F M M'<VAR>inst✝ : Finite R<VAR>a : R<VAR>ha : a ∈ R⁰<VAR>b c : R<VAR>hbc : (b - c) * a = 0<GOAL>b = c
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>a b : ℕ<VAR>hb : ↑b ≠ 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c }<VAR>e : divNat a b = ⟨{ num := n, den := d, den_nz := h, reduced := c }, hn⟩<GOAL>↑⟨{ num := n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>a b : ℕ<VAR>hb : ↑b ≠ 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>hn✝ : 0 ≤ { num := n, den := d, den_nz := h, reduced := c }<VAR>hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c }.num<VAR>e : divNat a b = ⟨{ num := n, den := d, den_nz := h, reduced := c }, hn✝⟩<GOAL>↑⟨{ num := n, den := d, den_nz := h, reduced := c }, hn✝⟩ = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>a b : ℕ<VAR>hb : ↑b ≠ 0<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>n : ℕ<VAR>c : (↑n).natAbs.Coprime d<VAR>hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }<VAR>e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩<GOAL>↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>a b : ℕ<VAR>hb : ↑b ≠ 0<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>n : ℕ<VAR>c : (↑n).natAbs.Coprime d<VAR>hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }<VAR>e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩<VAR>hd : ↑d ≠ 0<GOAL>↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>a b : ℕ<VAR>hb : ↑b ≠ 0<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>n : ℕ<VAR>c : (↑n).natAbs.Coprime d<VAR>hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }<VAR>e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩<VAR>hd : ↑d ≠ 0<VAR>hb' : b ≠ 0<GOAL>↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>a b : ℕ<VAR>hb : ↑b ≠ 0<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>n : ℕ<VAR>c : (↑n).natAbs.Coprime d<VAR>hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }<VAR>e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩<VAR>hd : ↑d ≠ 0<VAR>hb' : b ≠ 0<VAR>hd' : d ≠ 0<GOAL>↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>a b : ℕ<VAR>hb : ↑b ≠ 0<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>n : ℕ<VAR>c : (↑n).natAbs.Coprime d<VAR>hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }<VAR>hd : ↑d ≠ 0<VAR>hb' : b ≠ 0<VAR>hd' : d ≠ 0<VAR>e : a * d = n * b<GOAL>↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>a b : ℕ<VAR>hb : ↑b ≠ 0<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>n : ℕ<VAR>c : (↑n).natAbs.Coprime d<VAR>hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }<VAR>hd : ↑d ≠ 0<VAR>hb' : b ≠ 0<VAR>hd' : d ≠ 0<VAR>e : a * d = n * b<GOAL>↑(num ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩) / ↑(den ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩) = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>a b : ℕ<VAR>hb : ↑b ≠ 0<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>n : ℕ<VAR>c : (↑n).natAbs.Coprime d<VAR>hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }<VAR>hd : ↑d ≠ 0<VAR>hb' : b ≠ 0<VAR>hd' : d ≠ 0<VAR>e : a * d = n * b<GOAL>↑n / ↑d = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>a b : ℕ<VAR>hb : ↑b ≠ 0<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>n : ℕ<VAR>c : (↑n).natAbs.Coprime d<VAR>hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }<VAR>hd : ↑d ≠ 0<VAR>hb' : b ≠ 0<VAR>hd' : d ≠ 0<VAR>e : a * d = n * b<GOAL>↑n * ↑b = ↑a * ↑d
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>a b : ℕ<VAR>hb : ↑b ≠ 0<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>n : ℕ<VAR>c : (↑n).natAbs.Coprime d<VAR>hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }<VAR>hd : ↑d ≠ 0<VAR>hb' : b ≠ 0<VAR>hd' : d ≠ 0<VAR>e : a * d = n * b<GOAL>Commute ↑d ↑b
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m p : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<GOAL>Prime ↑(d ⟨p, ⋯⟩)
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m p : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<GOAL>Irreducible ↑(d ⟨p, ⋯⟩)
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m p : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<GOAL>↑(d ⟨p, ⋯⟩) ≠ ⊥
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : UniqueFactorizationMonoid N<VAR>inst✝ : UniqueFactorizationMonoid M<VAR>m p : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>hp : p ∈ normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>b : Associates N<VAR>hb : b < ↑(d ⟨p, ⋯⟩)<GOAL>b = ⊥
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>hs : Convex ℝ s<VAR>δ : ℝ<GOAL>Convex ℝ (Metric.thickening δ s)
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>hs : Convex ℝ s<VAR>δ : ℝ<GOAL>Convex ℝ (s + ball 0 δ)
<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<GOAL>(lift fe) (inl a) = (↑fe).1 a
<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>i : ι<VAR>x : M<GOAL>(b.dualBasis i) x = (b.coord i) x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n✝ : σ →₀ ℕ<VAR>φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R<VAR>n : σ →₀ ℕ<GOAL>(coeff R n) ((φ₁ + φ₂) * φ₃) = (coeff R n) (φ₁ * φ₃ + φ₂ * φ₃)
<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>s \ frontier s = interior s
<VAR>r : ℝ<GOAL>r.toNNReal = 0 ↔ r ≤ 0
<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>c : F<GOAL>fderiv 𝕜 (fun y => c + f y) x = fderiv 𝕜 f x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N : LieSubmodule R L M<GOAL>comap N.incl N = ⊤
<VAR>x✝ : ℂ<GOAL>logTaylor 0 x✝ = 0
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<GOAL>IsCoveringMap f ↔ IsCoveringMapOn f Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<VAR>μ' : Measure α := ν.withDensity (μ.rnDeriv ν)<GOAL>μ.rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun x => (f x)⁻¹ * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<VAR>μ' : Measure α := ν.withDensity (μ.rnDeriv ν)<VAR>h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)<GOAL>μ.rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun x => (f x)⁻¹ * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<VAR>μ' : Measure α := ν.withDensity (μ.rnDeriv ν)<VAR>h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)<VAR>h₂ : μ.rnDeriv ν =ᶠ[ae ν] μ'.rnDeriv ν<GOAL>μ.rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun x => (f x)⁻¹ * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<VAR>μ' : Measure α := ν.withDensity (μ.rnDeriv ν)<VAR>h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)<VAR>h₂ : μ.rnDeriv ν =ᶠ[ae ν] μ'.rnDeriv ν<VAR>this : SigmaFinite μ'<GOAL>μ.rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun x => (f x)⁻¹ * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hf : AEMeasurable f ν<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ⊤<VAR>μ' : Measure α := ν.withDensity (μ.rnDeriv ν)<VAR>h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)<VAR>h₂ : μ.rnDeriv ν =ᶠ[ae ν] μ'.rnDeriv ν<VAR>this : SigmaFinite μ'<VAR>hμ' : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun x => (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x<GOAL>μ.rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun x => (f x)⁻¹ * μ.rnDeriv ν x