ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝¹ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝ : LinearOrder γ<VAR>f : α → γ<GOAL>LowerSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Iic y)
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝¹ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝ : LinearOrder γ<VAR>f : α → γ<GOAL>(∀ (y : γ), IsOpen (f ⁻¹' Ioi y)) ↔ ∀ (y : γ), IsClosed (f ⁻¹' Iic y)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝ : L.IsLocalization W<VAR>X Y Z X' Y' : C<VAR>e : X ≅ X'<VAR>e' : Y ≅ Y'<GOAL>HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X' Y'
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} D'<VAR>L : C ⥤ D<VAR>inst✝ : L.IsLocalization W<VAR>X Y Z X' Y' : C<VAR>e : X ≅ X'<VAR>e' : Y ≅ Y'<GOAL>Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s t : Set α<GOAL>(s ∪ t).encard ≤ s.encard + t.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s t : Set α<GOAL>(s ∪ t).encard ≤ (s ∪ t).encard + (s ∩ t).encard
<VAR>q : ℚ<GOAL>↑q.num < (↑⌊q⌋ + 1) * ↑q.den
<VAR>q : ℚ<GOAL>↑q.num < (q - fract q + 1) * ↑q.den
<VAR>q : ℚ<GOAL>↑q.num < ↑q.num + (1 - fract q) * ↑q.den
<VAR>q : ℚ<GOAL>0 < (1 - fract q) * ↑q.den
<VAR>q : ℚ<VAR>this : 0 < 1 - fract q<GOAL>0 < (1 - fract q) * ↑q.den
<VAR>r n : ℕ<VAR>h : r < n / 2<GOAL>n.choose r ≤ n.choose (r + 1)
<VAR>r n : ℕ<VAR>h : r < n / 2<GOAL>n.choose r * (n - r) ≤ n.choose (r + 1) * (n - r)
<VAR>r n : ℕ<VAR>h : r < n / 2<GOAL>n.choose (r + 1) * (r + 1) ≤ n.choose (r + 1) * (n - r)
<VAR>r n : ℕ<VAR>h : r < n / 2<GOAL>r + 1 ≤ n - r
<VAR>r n : ℕ<VAR>h : r < n / 2<GOAL>r * 2 < n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>p : α → Prop<VAR>fs : Set (Filter α)<GOAL>(∃ᶠ (x : α) in sSup fs, p x) ↔ ∃ f ∈ fs, ∃ᶠ (x : α) in f, p x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ : α<VAR>n : ℕ<VAR>a : ℤ<GOAL>a ≤ ⌊↑n⌋ ↔ a ≤ ↑n
<VAR>R : Type u_1<VAR>inst✝⁴ : Semiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>M : Matrix m n R<VAR>M' : Matrix n m R<VAR>hMM' : M * M' = 1<VAR>hM'M : M' * M = 1<VAR>x : n → R<GOAL>(toLinearMapRight' M) ({ toFun := ⇑(toLinearMapRight' M'), map_add' := ⋯, map_smul' := ⋯ }.toFun x) = x
<VAR>R : Type u_1<VAR>inst✝⁴ : Semiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>M : Matrix m n R<VAR>M' : Matrix n m R<VAR>hMM' : M * M' = 1<VAR>hM'M : M' * M = 1<VAR>x : m → R<GOAL>(toLinearMapRight' M') ((toLinearMapRight' M) x) = x
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>hf' : LocallyIntegrable f' μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ<VAR>this : ∀ᵐ (x : M) ∂μ, (f - f') x = 0<GOAL>∀ᵐ (x : M) ∂μ, f x = f' x
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>hf' : LocallyIntegrable f' μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = ∫ (x : M), g x • f' x ∂μ<VAR>this : ∀ᵐ (x : M) ∂μ, (f - f') x = 0<VAR>x : M<VAR>hx : (f - f') x = 0<GOAL>f x = f' x
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>a b : α<VAR>u : αˣ<GOAL>↑u ∣ a
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t✝ : M → Set F<VAR>n : ℕ∞<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<GOAL>∃ f, Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t✝ : M → Set F<VAR>n : ℕ∞<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>f : M → ℝ<VAR>f_diff : Smooth I 𝓘(ℝ, ℝ) f<VAR>f_range : range f ⊆ Icc 0 1<VAR>fs : support f = sᶜ<VAR>ft : ∀ (x : M), x ∈ t ↔ f x = 1<GOAL>∃ f, Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>t✝ : M → Set F<VAR>n : ℕ∞<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>f : M → ℝ<VAR>f_diff : Smooth I 𝓘(ℝ, ℝ) f<VAR>f_range : range f ⊆ Icc 0 1<VAR>fs : support f = sᶜ<VAR>ft : ∀ (x : M), x ∈ t ↔ f x = 1<GOAL>∀ (x : M), x ∈ s ↔ f x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : ι → α<VAR>s t : Set α<GOAL>Sum.inl ⁻¹' range Sum.inr = ∅
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : SeminormedRing α✝<VAR>α : Type u_5<VAR>inst✝¹ : NormedCommRing α<VAR>inst✝ : NormOneClass α<VAR>f : ι → α<VAR>val✝ : Multiset ι<VAR>l : List ι<VAR>hl : Multiset.Nodup (Quot.mk Setoid.r l)<GOAL>‖∏ i ∈ { val := Quot.mk Setoid.r l, nodup := hl }, f i‖ ≤ ∏ i ∈ { val := Quot.mk Setoid.r l, nodup := hl }, ‖f i‖
<VAR>m n✝ a n : ℕ<GOAL>succ^[n + 1] a = a + (n + 1)
<VAR>m n✝ a n : ℕ<GOAL>(succ ∘ succ^[n]) a = (a + n).succ
<VAR>s : ℂ<GOAL>LSeriesSummable 0 s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ ⊤<GOAL>(r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite μ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ ⊤<VAR>h : (r.toNNReal • ν).rnDeriv μ =ᶠ[ae μ] r.toNNReal • ν.rnDeriv μ<GOAL>(r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<GOAL>0 ∈ σ a ↔ ¬IsUnit a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : ↥(Lp E 2 μ)<GOAL>AEEqFun.mk (fun x => ⟪↑↑f x, ↑↑g x⟫_𝕜) ⋯ ∈ Lp 𝕜 1 μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidableEq α<VAR>h : a ≤ b<GOAL>insert a (Ioc a b) = Icc a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ∆ b ⊔ a ⊓ b = a ⊔ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ⊔ b ≤ a ∆ b ⊔ a ⊓ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ≤ a \ b ⊔ b \ a ⊔ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>b ≤ a \ b ⊔ b \ a ⊔ a
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>p : α → Prop<VAR>q : β → Prop<VAR>e : α ≃ β<GOAL>∀ (a : α), ((fun a => q (e a)) a ∧ ∀ (y : α), (fun a => q (e a)) y → y = a) ↔ (fun b => q b) (e a) ∧ ∀ (y : β), (fun b => q b) y → y = e a
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>g : G<GOAL>QuasiMeasurePreserving (fun h => g / h) μ μ
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>g : G<GOAL>QuasiMeasurePreserving (fun h => g / h) μ.inv.inv μ.inv.inv
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁.ndunion s₂).sup = s₁.sup ⊔ s₂.sup
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>W X Y Z : C<VAR>h : X ⟶ Z<VAR>k : Y ⟶ Z<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>comm : f ≫ h = g ≫ k<VAR>inst✝² : PreservesColimit (span f g) G<VAR>inst✝¹ : HasPushout f g<VAR>inst✝ : HasPushout (G.map f) (G.map g)<GOAL>G.map (pushout.inl f g) ≫ (iso G f g).inv = pushout.inl (G.map f) (G.map g)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝[≥] a<GOAL>∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝[≥] a<VAR>ha : IsMax a<GOAL>∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝[≥] a<VAR>ha : ∃ b, a < b<GOAL>∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i✝ j : ι<VAR>l✝ : List ι<VAR>f✝ : (i : ι) → α i<VAR>i : ι<VAR>l : List ι<VAR>t : (i : ι) → Set (α i)<VAR>f : (i : ι) → α i<GOAL>f ∈ TProd.mk (i :: l) ⁻¹' Set.tprod (i :: l) t ↔ f ∈ {i_1 | i_1 ∈ i :: l}.pi t
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i✝ j : ι<VAR>l✝ : List ι<VAR>f✝ : (i : ι) → α i<VAR>i : ι<VAR>l : List ι<VAR>t : (i : ι) → Set (α i)<VAR>f : (i : ι) → α i<VAR>h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ i ∈ l, f i ∈ t i<GOAL>f ∈ TProd.mk (i :: l) ⁻¹' Set.tprod (i :: l) t ↔ f ∈ {i_1 | i_1 ∈ i :: l}.pi t
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i✝ j : ι<VAR>l✝ : List ι<VAR>f✝ : (i : ι) → α i<VAR>i : ι<VAR>l : List ι<VAR>t : (i : ι) → Set (α i)<VAR>f : (i : ι) → α i<VAR>h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ i ∈ l, f i ∈ t i<GOAL>f i ∈ t i ∧ TProd.mk l f ∈ Set.tprod l t ↔ ∀ i_1 ∈ {i_2 | i_2 ∈ i :: l}, f i_1 ∈ t i_1
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i✝ j : ι<VAR>l✝ : List ι<VAR>f✝ : (i : ι) → α i<VAR>i : ι<VAR>l : List ι<VAR>t : (i : ι) → Set (α i)<VAR>f : (i : ι) → α i<VAR>h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ i ∈ l, f i ∈ t i<GOAL>f i ∈ t i ∧ TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ l → f i_1 ∈ t i_1
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i✝ j : ι<VAR>l✝ : List ι<VAR>f✝ : (i : ι) → α i<VAR>i : ι<VAR>l : List ι<VAR>t : (i : ι) → Set (α i)<VAR>f : (i : ι) → α i<VAR>h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ i ∈ l, f i ∈ t i<GOAL>f i ∈ t i → (TProd.mk l f ∈ Set.tprod l t ↔ ∀ a ∈ l, f a ∈ t a)
<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>x : X<VAR>C : Set X<GOAL>AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>e₁ : T₁.obj₁ ≅ T₂.obj₁<VAR>e₂ : T₁.obj₂ ≅ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁<GOAL>T₁ ≅ T₂
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>e₁ : T₁.obj₁ ≅ T₂.obj₁<VAR>e₂ : T₁.obj₂ ≅ T₂.obj₂<VAR>comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁<VAR>h : ∃ e', e'.hom.hom₁ = (Arrow.isoMk e₁ e₂ ⋯).hom.left ∧ e'.hom.hom₂ = (Arrow.isoMk e₁ e₂ ⋯).hom.right<GOAL>T₁ ≅ T₂
<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>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
<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>∀ (i : α), ∀ᶠ (x : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑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<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)<GOAL>∀ᶠ (x : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑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<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<GOAL>∀ᶠ (x : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑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<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<GOAL>∀ᶠ (x : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑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<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<VAR>h_main_norm : (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖<GOAL>∀ᶠ (x : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑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<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<VAR>h_main_norm : (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖<VAR>h_main : (fun n => q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n => b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<GOAL>∀ᶠ (x : ℕ) in atTop, ↑(r i x) ^ p a b * (1 - ε ↑(r i x)) ≤ b i ^ p a b * ↑x ^ p a b * (1 - ε ↑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<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<VAR>h_main_norm : (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖<VAR>h_main : (fun n => q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n => b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>n : ℕ<VAR>hn : q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<GOAL>↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
<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>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<VAR>h_main_norm : (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖<VAR>h_main : (fun n => q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n => b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>n : ℕ<VAR>hn : q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>h₁ : q (b i * ↑n) + b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)<GOAL>↑(r i n) ^ p a b * (1 - ε ↑(r i n)) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
<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>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<VAR>h_main_norm : (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖<VAR>h_main : (fun n => q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n => b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>n : ℕ<VAR>hn : q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>h₁ : q (b i * ↑n) + b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)<GOAL>q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)
<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>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 - ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<VAR>h_main_norm : (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖<VAR>h_main : (fun n => q ↑(r i n) - q (b i * ↑n)) ≤ᶠ[atTop] fun n => b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>n : ℕ<VAR>hn : q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>h₁ : q (b i * ↑n) + b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 - ε ↑n)<GOAL>q ↑(r i n) - q (b i * ↑n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NoZeroDivisors α<VAR>m : ℕ<VAR>hm : FermatLastTheoremWith α m<VAR>a b c : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<VAR>k : ℕ<GOAL>a ^ (m * k) + b ^ (m * k) ≠ c ^ (m * k)
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NoZeroDivisors α<VAR>m : ℕ<VAR>hm : FermatLastTheoremWith α m<VAR>a b c : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<VAR>k : ℕ<GOAL>(a ^ k) ^ m + (b ^ k) ^ m ≠ (c ^ k) ^ m
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁹ : RCLike 𝕂<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : (i : m) → Fintype (n' i)<VAR>inst✝³ : (i : m) → DecidableEq (n' i)<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>A : Matrix m m 𝔸<VAR>this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing<VAR>this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing<VAR>this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra<GOAL>IsUnit (exp 𝕂 A)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>G : Type u_6<VAR>H : Type u_7<VAR>F : Type u_8<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : CommGroup H<VAR>f : G →* H<VAR>g h : M →* G<VAR>x✝ : M<GOAL>(f.comp (g / h)) x✝ = (f.comp g / f.comp h) x✝
<VAR>a b c : ℤ<VAR>habc : a ∣ b * c<VAR>hab : a.gcd b = 1<GOAL>a ∣ c
<VAR>a b c : ℤ<VAR>habc : a ∣ c * b<VAR>hab : a.gcd b = 1<GOAL>a ∣ c
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S<VAR>S' : Type u_1<VAR>inst✝² : CommSemiring S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R S<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>p q : PrimeSpectrum S<VAR>h : (fun x => Ideal.map (algebraMap R S) x.asIdeal) ((comap (algebraMap R S)) p) = (fun x => Ideal.map (algebraMap R S) x.asIdeal) ((comap (algebraMap R S)) q)<GOAL>p = q
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S<VAR>S' : Type u_1<VAR>inst✝² : CommSemiring S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R S<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>p q : PrimeSpectrum S<VAR>h : Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) p.asIdeal) = Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) q.asIdeal)<GOAL>p = q
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S<VAR>S' : Type u_1<VAR>inst✝² : CommSemiring S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R S<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>p q : PrimeSpectrum S<VAR>h : p.asIdeal = q.asIdeal<GOAL>p = q
<VAR>x y z✝ : ℝ<VAR>n✝ : ℕ<VAR>hx : 0 ≤ x<VAR>n : ℤ<VAR>z : ℝ<GOAL>x ^ (↑n * z) = (x ^ n) ^ z