ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype o<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype m<VAR>inst✝ : StrongRankCondition R<VAR>A : Matrix m n R<VAR>this✝ : Module.Finite R (m → R)<VAR>this : Module.Free R (m → R)<GOAL>A.rank ≤ Fintype.card m
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w✝ : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>w : InfinitePlace K<VAR>H : IsUnramified k w<VAR>v : InfinitePlace K<VAR>hv : v.comap (algebraMap k K) = w.comap (algebraMap k K)<GOAL>IsUnramified k v
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ✝ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>v : InfinitePlace K<VAR>σ : K ≃ₐ[k] K<VAR>H : IsUnramified k (σ • v)<VAR>hv : v.comap (algebraMap k K) = (σ • v).comap (algebraMap k K)<GOAL>IsUnramified k v
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>r : R<GOAL>choose r 1 = r ^ 1
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>this : 0 < p<GOAL>∑ i ∈ s, w i * z i ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>this : 0 < p<GOAL>(∑ i ∈ s, w i * z i) ^ p ≤ ∑ i ∈ s, w i * z i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>this : 0 < p<GOAL>0 ≤ ∑ i ∈ s, w i * z i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>this : 0 < p<GOAL>0 ≤ ∑ i ∈ s, w i * z i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>this : 0 < p<GOAL>0 ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>n m : ℕ<VAR>s : Stream' α<VAR>n✝ : ℕ<GOAL>(drop n (drop m s)).get n✝ = (drop (n + m) s).get n✝
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>S : B<VAR>s : Submonoid M<VAR>l : List ↥s<GOAL>(List.map Subtype.val l).prod ∈ s
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : SetLike B M<VAR>inst✝ : SubmonoidClass B M<VAR>S : B<VAR>s : Submonoid M<VAR>l : List ↥s<GOAL>↑l.prod ∈ s
<VAR>G : Type u<VAR>inst✝ : Group G<GOAL>Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) = Nat.card ↥(_root_.commutator G)
<VAR>G : Type u<VAR>inst✝ : Group G<GOAL>Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) = Nat.card ↥(map (closureCommutatorRepresentatives G).subtype (_root_.commutator ↥(closureCommutatorRepresentatives G)))
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>f : α → β<GOAL>(∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f x = ∏ x ∈ s, f x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>f : α → β<VAR>x✝ : α<VAR>a✝ : x✝ ∈ s<GOAL>f = t.piecewise f f
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>a b : G<GOAL>a * b * a⁻¹ = b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace α<VAR>π : ι → Set (Set α)<VAR>h : ∀ (n : ι), generateFrom (π n) ≤ m<VAR>S : Set ι<GOAL>generateFrom (piiUnionInter π S) ≤ m
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace α<VAR>π : ι → Set (Set α)<VAR>h : ∀ (n : ι), generateFrom (π n) ≤ m<VAR>S : Set ι<GOAL>∀ t ∈ piiUnionInter π S, MeasurableSet t
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace α<VAR>π : ι → Set (Set α)<VAR>h : ∀ (n : ι), generateFrom (π n) ≤ m<VAR>S : Set ι<VAR>ht_p : Finset ι<VAR>w✝ : ↑ht_p ⊆ S<VAR>ft : ι → Set α<VAR>hft_mem_pi : ∀ x ∈ ht_p, ft x ∈ π x<GOAL>MeasurableSet (⋂ x ∈ ht_p, ft x)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace α<VAR>π : ι → Set (Set α)<VAR>h : ∀ (n : ι), generateFrom (π n) ≤ m<VAR>S : Set ι<VAR>ht_p : Finset ι<VAR>w✝ : ↑ht_p ⊆ S<VAR>ft : ι → Set α<VAR>hft_mem_pi : ∀ x ∈ ht_p, ft x ∈ π x<VAR>x : ι<VAR>hx_mem : x ∈ ht_p<GOAL>MeasurableSet (ft x)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a✝ : α<VAR>g f✝ : α → M<VAR>a b : ℕ<VAR>hab : a ≤ b<VAR>f : ℕ → M<GOAL>∏ k ∈ Ioc a (b + 1), f k = (∏ k ∈ Ioc a b, f k) * f (b + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>n : ℤ<GOAL>‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>n : ℤ<GOAL>‖↑x‖ ≤ ↑p ^ n ↔ ‖↑x‖ < ↑p ^ (n + 1)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f✝¹ : X → Y<VAR>s✝ : Set X<VAR>x : X<VAR>y : Y<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>f✝ : α → X<VAR>g : X → Y<VAR>f : α → X<VAR>s : Set X<VAR>hf : DenseRange f<VAR>hs : IsOpen s<GOAL>s ⊆ closure (f '' (f ⁻¹' s))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f✝¹ : X → Y<VAR>s✝ : Set X<VAR>x : X<VAR>y : Y<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>f✝ : α → X<VAR>g : X → Y<VAR>f : α → X<VAR>s : Set X<VAR>hf : DenseRange f<VAR>hs : IsOpen s<GOAL>s ⊆ closure (s ∩ range f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>inst✝⁷ : InnerProductSpace 𝕜 F<VAR>inst✝⁶ : InnerProductSpace 𝕜 G<VAR>H : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : InnerProductSpace 𝕜 H<VAR>inst✝³ : CompleteSpace H<VAR>K : Type u_6<VAR>inst✝² : NormedAddCommGroup K<VAR>inst✝¹ : InnerProductSpace 𝕜 K<VAR>inst✝ : CompleteSpace K<VAR>e : H ≃ₗᵢ[𝕜] K<VAR>e' : H →L[𝕜] K := ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }<GOAL>adjoint e' = (adjoint e').comp (e'.comp ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>inst✝⁷ : InnerProductSpace 𝕜 F<VAR>inst✝⁶ : InnerProductSpace 𝕜 G<VAR>H : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : InnerProductSpace 𝕜 H<VAR>inst✝³ : CompleteSpace H<VAR>K : Type u_6<VAR>inst✝² : NormedAddCommGroup K<VAR>inst✝¹ : InnerProductSpace 𝕜 K<VAR>inst✝ : CompleteSpace K<VAR>e : H ≃ₗᵢ[𝕜] K<VAR>e' : H →L[𝕜] K := ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }<GOAL>e'.comp ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = id 𝕜 K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>inst✝⁷ : InnerProductSpace 𝕜 F<VAR>inst✝⁶ : InnerProductSpace 𝕜 G<VAR>H : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : InnerProductSpace 𝕜 H<VAR>inst✝³ : CompleteSpace H<VAR>K : Type u_6<VAR>inst✝² : NormedAddCommGroup K<VAR>inst✝¹ : InnerProductSpace 𝕜 K<VAR>inst✝ : CompleteSpace K<VAR>e : H ≃ₗᵢ[𝕜] K<VAR>e' : H →L[𝕜] K := ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }<GOAL>(adjoint e').comp (e'.comp ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) = ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>inst✝⁷ : InnerProductSpace 𝕜 F<VAR>inst✝⁶ : InnerProductSpace 𝕜 G<VAR>H : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : InnerProductSpace 𝕜 H<VAR>inst✝³ : CompleteSpace H<VAR>K : Type u_6<VAR>inst✝² : NormedAddCommGroup K<VAR>inst✝¹ : InnerProductSpace 𝕜 K<VAR>inst✝ : CompleteSpace K<VAR>e : H ≃ₗᵢ[𝕜] K<VAR>e' : H →L[𝕜] K := ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }<GOAL>comp 1 ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁷ : MonoidWithZero R<VAR>inst✝⁶ : MonoidWithZero R'<VAR>inst✝⁵ : Zero M<VAR>inst✝⁴ : MulActionWithZero R M<VAR>inst✝³ : Zero M'<VAR>inst✝² : SMul R M'<VAR>p : Prop<VAR>inst✝¹ : Decidable p<VAR>ι : Type u_5<VAR>inst✝ : DecidableEq ι<VAR>x : M<VAR>i j : ι<GOAL>single i 1 j • x = single i x j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>u : R<VAR>freq_le : ∃ᶠ (x : R) in F, x ≤ u<VAR>ev : ∀ᶠ (x : S) in map f F, ¬(fun y => y ≤ f u) x<GOAL>∀ᶠ (x : R) in F, ¬(fun x => x ≤ u) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>u : R<VAR>freq_le : ∃ᶠ (x : R) in F, x ≤ u<VAR>ev : ∀ᶠ (x : S) in map f F, f u < x<GOAL>∀ᶠ (x : R) in F, u < x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>u : R<VAR>freq_le : ∃ᶠ (x : R) in F, x ≤ u<VAR>ev : ∀ᶠ (x : S) in map f F, f u < x<VAR>z : R<VAR>hz : z ∈ f ⁻¹' {x | f u < x}<GOAL>u < z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : LinearOrder S<VAR>f : R → S<VAR>f_incr : Monotone f<VAR>u : R<VAR>freq_le : ∃ᶠ (x : R) in F, x ≤ u<VAR>ev : ∀ᶠ (x : S) in map f F, f u < x<VAR>z : R<VAR>hz : z ∈ f ⁻¹' {x | f u < x}<VAR>con : ¬u < z<GOAL>False
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>compare a b = Ordering.gt ↔ a > b
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>(if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.gt ↔ a > b
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h✝¹ : ¬a < b<VAR>h✝ : ¬a = b<GOAL>True ↔ a > b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>x y : G<VAR>h : ¬IsOfFinOrder x<VAR>n m : ℤ<VAR>hnm : (fun n => x ^ n) n = (fun n => x ^ n) m<GOAL>n = m
<VAR>b x : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hx : x ≠ 0<VAR>t : Ordinal.{u_1} := sInf {o | x < b ^ o}<GOAL>succ (log b x) = sInf {o | x < b ^ o}
<VAR>b x : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hx : x ≠ 0<VAR>t : Ordinal.{u_1} := sInf {o | x < b ^ o}<VAR>this : x < b ^ t<GOAL>succ (log b x) = sInf {o | x < b ^ o}
<VAR>b x : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hx : x ≠ 0<VAR>t : Ordinal.{u_1} := sInf {o | x < b ^ o}<VAR>this : x < b ^ t<VAR>h : t = 0<GOAL>succ (log b x) = sInf {o | x < b ^ o}
<VAR>b x : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hx : x ≠ 0<VAR>t : Ordinal.{u_1} := sInf {o | x < b ^ o}<VAR>this : x < b ^ t<VAR>h : ∃ a, t = succ a<GOAL>succ (log b x) = sInf {o | x < b ^ o}
<VAR>b x : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>hx : x ≠ 0<VAR>t : Ordinal.{u_1} := sInf {o | x < b ^ o}<VAR>this : x < b ^ t<VAR>h : t.IsLimit<GOAL>succ (log b x) = sInf {o | x < b ^ o}
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>x : ℝ<GOAL>↑x < 0 ↔ x < 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>x : ↑(F.obj X)<GOAL>∃ Y i y, F.map i y = x ∧ IsConnected Y ∧ Mono i
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>x : ↑(F.obj X)<VAR>ι : Type<VAR>f : ι → C<VAR>g : (i : ι) → f i ⟶ X<VAR>hl : IsColimit (Cofan.mk X g)<VAR>hc : ∀ (i : ι), IsConnected (f i)<VAR>he : Finite ι<GOAL>∃ Y i y, F.map i y = x ∧ IsConnected Y ∧ Mono i
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>x : ↑(F.obj X)<VAR>ι : Type<VAR>f : ι → C<VAR>g : (i : ι) → f i ⟶ X<VAR>hl : IsColimit (Cofan.mk X g)<VAR>hc : ∀ (i : ι), IsConnected (f i)<VAR>he : Finite ι<VAR>this : Fintype ι<VAR>s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)<VAR>s' : IsColimit s := isColimitOfPreserves F hl<GOAL>∃ Y i y, F.map i y = x ∧ IsConnected Y ∧ Mono i
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>x : ↑(F.obj X)<VAR>ι : Type<VAR>f : ι → C<VAR>g : (i : ι) → f i ⟶ X<VAR>hl : IsColimit (Cofan.mk X g)<VAR>hc : ∀ (i : ι), IsConnected (f i)<VAR>he : Finite ι<VAR>this : Fintype ι<VAR>s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)<VAR>s' : IsColimit s := isColimitOfPreserves F hl<VAR>j : ι<VAR>z : (forget FintypeCat).obj ((Discrete.functor f ⋙ F).obj { as := j })<VAR>h : (s.ι.app { as := j }) z = x<GOAL>∃ Y i y, F.map i y = x ∧ IsConnected Y ∧ Mono i
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>x : ↑(F.obj X)<VAR>ι : Type<VAR>f : ι → C<VAR>g : (i : ι) → f i ⟶ X<VAR>hl : IsColimit (Cofan.mk X g)<VAR>hc : ∀ (i : ι), IsConnected (f i)<VAR>he : Finite ι<VAR>this : Fintype ι<VAR>s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)<VAR>s' : IsColimit s := isColimitOfPreserves F hl<VAR>j : ι<VAR>z : (forget FintypeCat).obj ((Discrete.functor f ⋙ F).obj { as := j })<VAR>h : (s.ι.app { as := j }) z = x<GOAL>F.map (g j) z = x
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderTop α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>(ndinsert a s).inf = a ⊓ s.inf
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderTop α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f✝ g : α → β<VAR>a : α<VAR>f : ℕ → ℕ<VAR>hf : StrictMono f<VAR>m n : ℕ<GOAL>m + f n ≤ f (m + n)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f✝ g : α → β<VAR>a : α<VAR>f : ℕ → ℕ<VAR>hf : StrictMono f<VAR>m n : ℕ<GOAL>f n + m ≤ f (n + m)
<VAR>f : ℝ → ℝ<VAR>x f' : ℝ<VAR>s : Set ℝ<VAR>hf : HasStrictDerivAt f f' x<VAR>hx : f x ≠ 0<GOAL>HasStrictDerivAt (fun y => Real.log (f y)) (f' / f x) x
<VAR>f : ℝ → ℝ<VAR>x f' : ℝ<VAR>s : Set ℝ<VAR>hf : HasStrictDerivAt f f' x<VAR>hx : f x ≠ 0<GOAL>HasStrictDerivAt (fun y => Real.log (f y)) ((f x)⁻¹ * f') x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>f f' : Fan Z<VAR>c : Cofan fun x => op (Z x)<VAR>hf : IsLimit f<VAR>hf' : IsLimit f'<VAR>hc : IsColimit c<GOAL>(opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>f f' : Fan Z<VAR>c : Cofan fun x => op (Z x)<VAR>hf : IsLimit f<VAR>hf' : IsLimit f'<VAR>hc : IsColimit c<GOAL>((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop = (hf.conePointUniqueUpToIso hf').op.inv.unop
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>f f' : Fan Z<VAR>c : Cofan fun x => op (Z x)<VAR>hf : IsLimit f<VAR>hf' : IsLimit f'<VAR>hc : IsColimit c<GOAL>∀ (j : Discrete α), ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop ≫ f.π.app j = (hf.conePointUniqueUpToIso hf').op.inv.unop ≫ f.π.app j
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>f f' : Fan Z<VAR>c : Cofan fun x => op (Z x)<VAR>hf : IsLimit f<VAR>hf' : IsLimit f'<VAR>hc : IsColimit c<VAR>j : α<GOAL>((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop ≫ f.proj j = (hf.conePointUniqueUpToIso hf').op.inv.unop ≫ f.π.app { as := j }
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>f f' : Fan Z<VAR>c : Cofan fun x => op (Z x)<VAR>hf : IsLimit f<VAR>hf' : IsLimit f'<VAR>hc : IsColimit c<VAR>j : α<GOAL>(opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j = f'.π.app { as := j }
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>f f' : Fan Z<VAR>c : Cofan fun x => op (Z x)<VAR>hf : IsLimit f<VAR>hf' : IsLimit f'<VAR>hc : IsColimit c<VAR>j : α<GOAL>((opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j).op = (f'.π.app { as := j }).op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>f f' : Fan Z<VAR>c : Cofan fun x => op (Z x)<VAR>hf : IsLimit f<VAR>hf' : IsLimit f'<VAR>hc : IsColimit c<VAR>j : α<GOAL>c.inj j ≫ (opProductIsoCoproduct' hf' hc).inv = (f'.π.app { as := j }).op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>f f' : Fan Z<VAR>c : Cofan fun x => op (Z x)<VAR>hf : IsLimit f<VAR>hf' : IsLimit f'<VAR>hc : IsColimit c<VAR>j : α<GOAL>((f'.proj j).op ≫ (opProductIsoCoproduct' hf' hc).hom) ≫ (opProductIsoCoproduct' hf' hc).inv = (f'.π.app { as := j }).op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>f f' : Fan Z<VAR>c : Cofan fun x => op (Z x)<VAR>hf : IsLimit f<VAR>hf' : IsLimit f'<VAR>hc : IsColimit c<VAR>j : α<GOAL>(f'.proj j).op = (f'.π.app { as := j }).op
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : (i : ι) → DecidableEq (α i)<VAR>inst✝² : (i : ι) → PartialOrder (α i)<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>inst✝ : (i : ι) → LocallyFiniteOrder (α i)<VAR>f g : Π₀ (i : ι), α i<GOAL>(Ico f g).card = ∏ i ∈ f.support ∪ g.support, (Icc (f i) (g i)).card - 1
<VAR>x y : ℂ<GOAL>SameRay ℝ x y ↔ (x / y).arg = 0
<VAR>x y : ℂ<GOAL>x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0
<VAR>x y : ℂ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type w<VAR>inst✝¹ : Category.{z, w} D<VAR>inst✝ : Abelian D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(cokernel.π (kernel.ι (α.app X)) ≫ coimageImageComparison (α.app X)) ≫ kernel.ι (cokernel.π (α.app X)) = (cokernel.π (kernel.ι (α.app X)) ≫ (cokernel.desc (kernel.ι (α.app X)) (𝟙 (F.obj X) ≫ cokernel.π ((kernel.ι α).app X)) ⋯ ≫ (PreservesCokernel.iso ((evaluation C D).obj X) (kernel.ι α)).inv) ≫ (coimageImageComparison α).app X ≫ (PreservesKernel.iso ((evaluation C D).obj X) (cokernel.π α)).hom ≫ kernel.map ((cokernel.π α).app X) (cokernel.π (α.app X)) (𝟙 (G.obj X)) (PreservesCokernel.iso ((evaluation C D).obj X) α).hom ⋯) ≫ kernel.ι (cokernel.π (α.app X))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type w<VAR>inst✝¹ : Category.{z, w} D<VAR>inst✝ : Abelian D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>α.app X = cokernel.π ((kernel.ι α).app X) ≫ cokernelComparison (kernel.ι α) ((evaluation C D).obj X) ≫ (coimageImageComparison α).app X ≫ kernelComparison (cokernel.π α) ((evaluation C D).obj X) ≫ kernel.ι ((cokernel.π α).app X)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type w<VAR>inst✝¹ : Category.{z, w} D<VAR>inst✝ : Abelian D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>α.app X = ((evaluation C D).obj X).map (cokernel.π (kernel.ι α)) ≫ (coimageImageComparison α).app X ≫ ((evaluation C D).obj X).map (kernel.ι (cokernel.π α))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type w<VAR>inst✝¹ : Category.{z, w} D<VAR>inst✝ : Abelian D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(coimage.π α ≫ coimageImageComparison α ≫ image.ι α).app X = ((evaluation C D).obj X).map (cokernel.π (kernel.ι α)) ≫ (coimageImageComparison α).app X ≫ ((evaluation C D).obj X).map (kernel.ι (cokernel.π α))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>Tendsto (fun m => ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<GOAL>Tendsto (fun m => ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<GOAL>Tendsto (fun m => ((κ a) (univ ×ˢ seq m)).toReal) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<VAR>this : IsFiniteKernel κ<GOAL>Tendsto (fun m => ((κ a) (univ ×ˢ seq m)).toReal) atTop (𝓝 (ENNReal.toReal 0))