ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddCommMonoid (α i)<VAR>inst✝ : DecidableEq ι<VAR>f g : Π₀ (i : ι), α i<GOAL>f.support ∩ g.support = ∅ ↔ f.support ⊓ g.support = ⊥
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasWideEqualizers C<VAR>T : C<VAR>hT : ∀ (X : C), Nonempty (T ⟶ X)<VAR>endos : Type v := T ⟶ T<VAR>i : wideEqualizer id ⟶ T := wideEqualizer.ι id<VAR>this : Nonempty endos<GOAL>HasInitial C
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasWideEqualizers C<VAR>T : C<VAR>hT : ∀ (X : C), Nonempty (T ⟶ X)<VAR>endos : Type v := T ⟶ T<VAR>i : wideEqualizer id ⟶ T := wideEqualizer.ι id<VAR>this✝ : Nonempty endos<VAR>this : (X : C) → Unique (wideEqualizer id ⟶ X)<GOAL>HasInitial C
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X : C<GOAL>R.map (L.map (R.map (h.counit.app (L.obj X)))) ≫ R.map (h.counit.app (L.obj X)) = R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X : C<GOAL>R.map (L.map (R.map (h.counit.app (L.obj X))) ≫ h.counit.app (L.obj X)) = R.map (h.counit.app (L.obj (R.obj (L.obj X)))) ≫ R.map (h.counit.app (L.obj X))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X : C<GOAL>R.map (L.map (h.unit.app X)) ≫ R.map (h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X : C<GOAL>R.map (L.map (h.unit.app X) ≫ h.counit.app (L.obj X)) = 𝟙 (R.obj (L.obj X))
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>P : C → Prop<VAR>A : Type u_2<VAR>inst✝² : AddMonoid A<VAR>inst✝¹ : HasShift C A<VAR>a b c : A<VAR>h : a + b = c<VAR>inst✝ : ClosedUnderIsomorphisms P<VAR>X : C<GOAL>PredicateShift (PredicateShift P b) a X ↔ PredicateShift P c X
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b✝ c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>a : WithBot ℕ<VAR>b : ℕ<VAR>hp : p.degree ≤ a<GOAL>(p ^ b).degree ≤ ↑b * a
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝² : Semiring k<VAR>inst✝¹ : DecidableEq G<VAR>inst✝ : Mul G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>a : G<GOAL>image₂ (fun x x_1 => x * x_1) {a} f.support ⊆ image (fun x => a * x) f.support
<VAR>n : ℕ<GOAL>n ^ 0 ≤ n.ascFactorial 0
<VAR>n k : ℕ<GOAL>n ^ (k + 1) ≤ n.ascFactorial (k + 1)
<VAR>n k : ℕ<GOAL>n * n ^ k ≤ n * n.succ.ascFactorial k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : CommMonoid β<VAR>n : ℕ<VAR>c : Fin n → β<GOAL>∏ i : Fin n, c i = ∏ i ∈ range n, if h : i < n then c ⟨i, h⟩ else 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : CommMonoid β<VAR>n : ℕ<VAR>c : Fin n → β<GOAL>∀ x ∈ univ, c x = if h : ↑x < n then c ⟨↑x, h⟩ else 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : CommMonoid β<VAR>n : ℕ<VAR>c : Fin n → β<VAR>i : ℕ<VAR>hi : i < n<VAR>a✝ : ⟨i, hi⟩ ∈ univ<GOAL>c ⟨i, hi⟩ = if h : ↑⟨i, hi⟩ < n then c ⟨↑⟨i, hi⟩, h⟩ else 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : Nontrivial F<GOAL>‖snd 𝕜 E F‖ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : Nontrivial F<GOAL>1 ≤ ‖snd 𝕜 E F‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : Nontrivial F<VAR>f : F<VAR>hf : f ≠ 0<GOAL>1 ≤ ‖snd 𝕜 E F‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : Nontrivial F<VAR>f : F<VAR>hf : f ≠ 0<VAR>this : ‖f‖ ≤ ‖snd 𝕜 E F‖ * max ‖0‖ ‖f‖<GOAL>1 ≤ ‖snd 𝕜 E F‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : Nontrivial F<VAR>f : F<VAR>hf : f ≠ 0<VAR>this : ‖f‖ ≤ ‖snd 𝕜 E F‖ * ‖f‖<GOAL>1 ≤ ‖snd 𝕜 E F‖
<VAR>m n : ℕ<GOAL>(finRotate (n + 1)) ⟨n, ⋯⟩ = ⟨0, ⋯⟩
<VAR>m n : ℕ<GOAL>Fin.cast ⋯ (finAddFlip ⟨n, ⋯⟩) = 0
<VAR>m n : ℕ<GOAL>Fin.cast ⋯ ⟨n - n, ⋯⟩ = 0
<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✝¹ : PseudoEMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>x : α<VAR>N : ℕ<VAR>ihN : ↑(nearestPtInd e N) x ≤ N<GOAL>↑(nearestPtInd e (N + 1)) x ≤ N + 1
<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✝¹ : PseudoEMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>x : α<VAR>N : ℕ<VAR>ihN : ↑(nearestPtInd e N) x ≤ N<GOAL>(if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else ↑(nearestPtInd e N) x) ≤ N + 1
<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✝¹ : PseudoEMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>x : α<VAR>N : ℕ<VAR>ihN : ↑(nearestPtInd e N) x ≤ N<VAR>h✝ : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x<GOAL>N + 1 ≤ N + 1
<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✝¹ : PseudoEMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>e : ℕ → α<VAR>x : α<VAR>N : ℕ<VAR>ihN : ↑(nearestPtInd e N) x ≤ N<VAR>h✝ : ¬∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x<GOAL>↑(nearestPtInd e N) x ≤ N + 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s'✝ : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p'✝ : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>f' : α' → β'<VAR>p' : Filter ι'<VAR>s' : Set α'<VAR>h : TendstoUniformlyOn F f p s<VAR>h' : TendstoUniformlyOn F' f' p' s'<GOAL>TendstoUniformlyOn (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (s ×ˢ s')
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s'✝ : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p'✝ : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>f' : α' → β'<VAR>p' : Filter ι'<VAR>s' : Set α'<VAR>h : TendstoUniformlyOnFilter F f p (𝓟 s)<VAR>h' : TendstoUniformlyOnFilter F' f' p' (𝓟 s')<GOAL>TendstoUniformlyOnFilter (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (𝓟 (s ×ˢ s'))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>z : 𝕜<VAR>hz : z ∈ spectrum 𝕜 a<GOAL>exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>z : 𝕜<VAR>hz : z ∈ spectrum 𝕜 a<VAR>hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)<GOAL>exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>z : 𝕜<VAR>hz : z ∈ spectrum 𝕜 a<VAR>hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)<VAR>b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n<GOAL>exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>z : 𝕜<VAR>hz : z ∈ spectrum 𝕜 a<VAR>hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)<VAR>b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n<VAR>hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n<GOAL>exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>z : 𝕜<VAR>hz : z ∈ spectrum 𝕜 a<VAR>hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)<VAR>b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n<VAR>hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n<VAR>h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b<GOAL>exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>z : 𝕜<VAR>hz : z ∈ spectrum 𝕜 a<VAR>hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)<VAR>b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n<VAR>hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n<VAR>h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b<VAR>h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)<GOAL>exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>z : 𝕜<VAR>hz : z ∈ spectrum 𝕜 a<VAR>hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)<VAR>b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n<VAR>hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n<VAR>h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b<VAR>h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)<VAR>h₃ : exp 𝕜 (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b<GOAL>exp 𝕜 z ∈ spectrum 𝕜 (exp 𝕜 a)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>z : 𝕜<VAR>hz : z ∈ spectrum 𝕜 a<VAR>hexpmul : exp 𝕜 a = exp 𝕜 (a - ↑ₐ z) * ↑ₐ (exp 𝕜 z)<VAR>b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n<VAR>hb : Summable fun n => (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n<VAR>h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b<VAR>h₁ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)<VAR>h₃ : exp 𝕜 (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b<GOAL>¬((IsUnit (a - ↑ₐ z) ∧ IsUnit b) ∧ IsUnit (↑ₐ (exp 𝕜 z)))
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : a ∉ s<VAR>h₁ : f a = 1<GOAL>multinomial (insert a s) f = (s.sum f).succ * multinomial s f
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : a ∉ s<VAR>h₁ : f a = 1<GOAL>(∑ i ∈ insert a s, f i)! / ∏ i ∈ insert a s, (f i)! = (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : a ∉ s<VAR>h₁ : f a = 1<GOAL>(∑ x ∈ s, f x + 1) * (∑ x ∈ s, f x)! / (1! * ∏ x ∈ s, (f x)!) = (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : a ∉ s<VAR>h₁ : f a = 1<GOAL>(∑ x ∈ s, f x + 1) * (∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)! = (s.sum f).succ * ((∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)!)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ γ : Path x y<VAR>f : ↑I → ↑I<VAR>hfcont : Continuous f<VAR>hf₀ : f 0 = 0<VAR>hf₁ : f 1 = 1<VAR>this : range f = univ<GOAL>range (⇑γ ∘ f) = range ⇑γ
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R⟦X⟧<VAR>n : ℕ<GOAL>(trunc n f).degree < ↑n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R⟦X⟧<VAR>n : ℕ<GOAL>∀ (m : ℕ), n ≤ m → (trunc n f).coeff m = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R⟦X⟧<VAR>n m✝ : ℕ<VAR>a✝ : n ≤ m✝<GOAL>(trunc n f).coeff m✝ = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R⟦X⟧<VAR>n m✝ : ℕ<VAR>a✝ : n ≤ m✝<GOAL>(if m✝ < n then (coeff R m✝) f else 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f : F<VAR>g : G<VAR>x✝ y✝ z : α<VAR>s : Set α<VAR>x y : α<GOAL>edist x y ≤ ↑(ratio f)⁻¹ * edist (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f : F<VAR>g : G<VAR>x✝ y✝ z : α<VAR>s : Set α<VAR>x y : α<VAR>hr : ratio f ≠ 0<GOAL>edist x y ≤ ↑(ratio f)⁻¹ * edist (f x) (f y)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>h : p.last = q.head<GOAL>{ length := p.length + q.length, toFun := fun i => if H : ↑i < p.length then p.toFun ⟨↑i, ⋯⟩ else q.toFun ⟨↑i - p.length, ⋯⟩, step := ⋯ }.toFun 0 = p.toFun 0
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>h : p.last = q.head<GOAL>p.length = 0 → q.toFun 0 = p.toFun 0
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>h : p.last = q.head<VAR>H : p.length = 0<GOAL>q.toFun 0 = p.toFun 0
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>h : p.last = q.head<VAR>H : p.length = 0<GOAL>p.toFun 0 = p.last
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>f g : α → β<VAR>p : Set β → Prop<VAR>s : Set β<VAR>h' : HasCountableSeparatingOn β p s<VAR>hf : ∀ᶠ (x : α) in l, f x ∈ s<VAR>hg : ∀ᶠ (x : α) in l, g x ∈ s<VAR>h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U<GOAL>f =ᶠ[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>f g : α → β<VAR>p : Set β → Prop<VAR>s : Set β<VAR>h' : HasCountableSeparatingOn β p s<VAR>hf : ∀ᶠ (x : α) in l, f x ∈ s<VAR>hg : ∀ᶠ (x : α) in l, g x ∈ s<VAR>h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U<VAR>S : Set (Set β)<VAR>hSc : S.Countable<VAR>hSp : ∀ s ∈ S, p s<VAR>hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y<GOAL>f =ᶠ[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>f g : α → β<VAR>p : Set β → Prop<VAR>s : Set β<VAR>h' : HasCountableSeparatingOn β p s<VAR>hf : ∀ᶠ (x : α) in l, f x ∈ s<VAR>hg : ∀ᶠ (x : α) in l, g x ∈ s<VAR>h : ∀ (U : Set β), p U → ∀ᶠ (x : α) in l, f x ∈ U ↔ g x ∈ U<VAR>S : Set (Set β)<VAR>hSc : S.Countable<VAR>hSp : ∀ s ∈ S, p s<VAR>hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y<VAR>H : ∀ᶠ (x : α) in l, ∀ s ∈ S, f x ∈ s ↔ g x ∈ s<GOAL>f =ᶠ[l] g
<VAR>x✝ y x : ℝ<VAR>n : ℕ<VAR>ih : log (x ^ n) = ↑n * log x<GOAL>log (x ^ (n + 1)) = ↑(n + 1) * log x
<VAR>x y : ℝ<VAR>n : ℕ<VAR>ih : log (0 ^ n) = ↑n * log 0<GOAL>log (0 ^ (n + 1)) = ↑(n + 1) * log 0
<VAR>x✝ y x : ℝ<VAR>n : ℕ<VAR>ih : log (x ^ n) = ↑n * log x<VAR>hx : x ≠ 0<GOAL>log (x ^ (n + 1)) = ↑(n + 1) * log x
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>μ' μ ν : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : ν.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>hG : LocallyCompactSpace G<GOAL>μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>μ' μ ν : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : ν.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>hG : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<GOAL>μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>μ' μ ν : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : ν.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>hG : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>Z : ∫ (x : G), g x ∂μ' = ∫ (x : G), g x ∂μ'.haarScalarFactor μ • μ<GOAL>μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>μ' μ ν : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : ν.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>hG : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>Z : μ'.haarScalarFactor ν • ∫ (x : G), g x ∂ν = (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) • ∫ (x : G), g x ∂ν<GOAL>μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
<VAR>G : Type u_1<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalGroup G<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>μ' μ ν : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : ν.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>hG : LocallyCompactSpace G<VAR>g : G → ℝ<VAR>g_cont : Continuous g<VAR>g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }<VAR>g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }<VAR>g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0<VAR>int_g_pos : 0 < ∫ (x : G), g x ∂ν<VAR>Z : ↑(μ'.haarScalarFactor ν) * ∫ (x : G), g x ∂ν = ↑(μ'.haarScalarFactor μ * μ.haarScalarFactor ν) * ∫ (x : G), g x ∂ν<GOAL>μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₂ = ra * ↑s₃<GOAL>((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₂ = ra * ↑s₃<GOAL>((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (sa • r₂ /ₒ (sa * s₂)) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₂ = ra * ↑s₃<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * sa • r₂ = rb * ↑s₁<GOAL>((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂)) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₂ = ra * ↑s₃<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * sa • r₂ = rb * ↑s₁<VAR>hs₃rasb : ↑sb * ra * ↑s₃ ∈ S<GOAL>((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂)) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₂ = ra * ↑s₃<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * sa • r₂ = rb * ↑s₁<VAR>hs₃rasb : ↑sb * ra * ↑s₃ ∈ S<GOAL>((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂)) + ((↑sb * ra) • r₃ /ₒ ⟨↑sb * ra * ↑s₃, hs₃rasb⟩) • (r₁ /ₒ s₁)
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₂ = ra * ↑s₃<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * sa • r₂ = rb * ↑s₁<VAR>hs₃rasb : ↑sb * ra * ↑s₃ ∈ S<VAR>ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃<GOAL>((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂)) + ((↑sb * ra) • r₃ /ₒ ⟨↑sb * ra * ↑s₃, hs₃rasb⟩) • (r₁ /ₒ s₁)
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₂ = ra * ↑s₃<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * sa • r₂ = rb * ↑s₁<VAR>hs₃rasb : ↑sb * ra * ↑s₃ ∈ S<VAR>ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃<GOAL>((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂)) + ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁)
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₂ = ra * ↑s₃<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * sa • r₂ = rb * ↑s₁<VAR>hs₃rasb : ↑sb * ra * ↑s₃ ∈ S<VAR>ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * (↑sb * ra) • r₃ = rc * ↑s₁<VAR>hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))<GOAL>((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = rb • r₁ /ₒ (sb * (sa * s₂)) + rc • r₁ /ₒ (sc * (sb * sa * s₂))
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : Module R X<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : R<VAR>s₂ : ↥S<VAR>r₃ : R<VAR>s₃ : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s₂ = ra * ↑s₃<VAR>rb : R<VAR>sb : ↥S<VAR>hb : ↑sb * sa • r₂ = rb * ↑s₁<VAR>hs₃rasb : ↑sb * ra * ↑s₃ ∈ S<VAR>ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃<VAR>rc : R<VAR>sc : ↥S<VAR>hc : ↑sc * (↑sb * ra) • r₃ = rc * ↑s₁<VAR>hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))<GOAL>((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) = (sc • rb • r₁ + 1 • rc • r₁) /ₒ (sc * (sb * (sa * s₂)))