ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<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>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>ContMDiff I I' n f ↔ Continuous f ∧ ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<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>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>(ContinuousOn f univ ∧ ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) (univ ∩ f ⁻¹' (extChartAt I' y).source)) ↔ Continuous f ∧ ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>p : α → Prop<GOAL>(∀ x ∈ insert a s, p x) ↔ p a ∧ ∀ x ∈ s, p x
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderTop α<VAR>h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c<GOAL>IsCoatomic α
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderTop α<VAR>h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c<VAR>x : α<VAR>hx : x < ⊤<GOAL>∃ a, IsCoatom a ∧ x ≤ a
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderTop α<VAR>h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c<VAR>x : α<VAR>hx : x < ⊤<VAR>this : ∃ y ∈ Ico x ⊤, x ≤ y ∧ ∀ z ∈ Ico x ⊤, y ≤ z → z = y<GOAL>∃ a, IsCoatom a ∧ x ≤ a
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderTop α<VAR>h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c<VAR>x : α<VAR>hx : x < ⊤<VAR>y : α<VAR>hxy : x ≤ y<VAR>hy : y < ⊤<VAR>hy' : ∀ z ∈ Ico x ⊤, y ≤ z → z = y<GOAL>∃ a, IsCoatom a ∧ x ≤ a
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderTop α<VAR>h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c<VAR>x : α<VAR>hx : x < ⊤<VAR>y : α<VAR>hxy : x ≤ y<VAR>hy : y < ⊤<VAR>hy' : ∀ z ∈ Ico x ⊤, y ≤ z → z = y<VAR>z : α<VAR>hyz : y < z<VAR>hz : z < ⊤<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>n : ℕ<VAR>h : n ∈ σ.cycleType<GOAL>n ∣ orderOf σ
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>n : ℕ<VAR>h : n ∈ σ.cycleType<GOAL>n ∣ σ.cycleType.lcm
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>f : R →+* MvPolynomial σ S<VAR>g : S →+* T<VAR>φ : MvPolynomial σ R<GOAL>(map g) ((bind₂ f) φ) = (bind₂ ((map g).comp f)) φ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>f : R →+* MvPolynomial σ S<VAR>g : S →+* T<VAR>φ : MvPolynomial σ R<GOAL>eval₂ ((map g).comp f) (⇑(map g) ∘ X) φ = eval₂ ((map g).comp f) X φ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>f : R →+* MvPolynomial σ S<VAR>g : S →+* T<VAR>φ : MvPolynomial σ R<VAR>x✝ : σ<GOAL>(⇑(map g) ∘ X) x✝ = X x✝
<VAR>α✝ β✝ : Type u<VAR>a : Cardinal.{u}<VAR>b : Cardinal.{max u v}<VAR>α : Type u<VAR>β : Type (max u v)<GOAL>#β ≤ lift.{v, u} #α → ∃ a', lift.{v, u} a' = #β
<VAR>α✝ β✝ : Type u<VAR>a : Cardinal.{u}<VAR>b : Cardinal.{max u v}<VAR>α : Type u<VAR>β : Type (max u v)<GOAL>Nonempty (β ↪ α) → ∃ a', lift.{max u v, u} a' = lift.{max u v, max u v} #β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : Preorder M<VAR>inst✝⁶ : Add M<VAR>inst✝⁵ : Sub M<VAR>inst✝⁴ : OrderedSub M<VAR>inst✝³ : PartialOrder N<VAR>inst✝² : Add N<VAR>inst✝¹ : Sub N<VAR>inst✝ : OrderedSub N<VAR>e : M ≃o N<VAR>h_add : ∀ (a b : M), e (a + b) = e a + e b<VAR>a b : M<VAR>e_add : M ≃+ N := { toEquiv := e.toEquiv, map_add' := h_add }<GOAL>e (a - b) = e a - e b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : Preorder M<VAR>inst✝⁶ : Add M<VAR>inst✝⁵ : Sub M<VAR>inst✝⁴ : OrderedSub M<VAR>inst✝³ : PartialOrder N<VAR>inst✝² : Add N<VAR>inst✝¹ : Sub N<VAR>inst✝ : OrderedSub N<VAR>e : M ≃o N<VAR>h_add : ∀ (a b : M), e (a + b) = e a + e b<VAR>a b : M<VAR>e_add : M ≃+ N := { toEquiv := e.toEquiv, map_add' := h_add }<GOAL>e (a - b) ≤ e a - e b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : Preorder M<VAR>inst✝⁶ : Add M<VAR>inst✝⁵ : Sub M<VAR>inst✝⁴ : OrderedSub M<VAR>inst✝³ : PartialOrder N<VAR>inst✝² : Add N<VAR>inst✝¹ : Sub N<VAR>inst✝ : OrderedSub N<VAR>e : M ≃o N<VAR>h_add : ∀ (a b : M), e (a + b) = e a + e b<VAR>a b : M<VAR>e_add : M ≃+ N := { toEquiv := e.toEquiv, map_add' := h_add }<GOAL>e (e.symm (e a) - e.symm (e b)) ≤ e (e.symm (e a - e b))
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>a₁ : P.mp.A<VAR>f₁ : P.mp.B a₁ ⟹ α<VAR>a' : P.A<VAR>f' : (P.B a').drop ⟹ α<VAR>f₁' : (P.B a').last → P.M α<VAR>ff : P.B a' ⟹ α ::: P.M α<VAR>ef : splitFun f' f₁' = ff<VAR>e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', ff⟩<VAR>he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁<VAR>a₁' : P.last.A<VAR>g₁' : P.last.B a₁' → P.last.M<VAR>e₁' : he₁' = ⟨a₁', g₁'⟩<GOAL>∃ g₁', ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩), f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>a₁ : P.mp.A<VAR>f₁ : P.mp.B a₁ ⟹ α<VAR>a' : P.A<VAR>f' : (P.B a').drop ⟹ α<VAR>f₁' : (P.B a').last → P.M α<VAR>ff : P.B a' ⟹ α ::: P.M α<VAR>ef : splitFun f' f₁' = ff<VAR>he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁<VAR>a₁' : P.last.A<VAR>g₁' : P.last.B a₁' → P.last.M<VAR>e₁' : he₁' = ⟨a₁', g₁'⟩<VAR>e₁ : dest' P e₁' f₁ = ⟨a', ff⟩<GOAL>∃ g₁', ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩), f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>a₁ : P.mp.A<VAR>f₁ : P.mp.B a₁ ⟹ α<VAR>a' : P.A<VAR>f' : (P.B a').drop ⟹ α<VAR>f₁' : (P.B a').last → P.M α<VAR>he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁<VAR>g₁' : P.last.B a' → P.last.M<VAR>e₁' : he₁' = ⟨a', g₁'⟩<VAR>ef : splitFun f' f₁' = splitFun (pathDestLeft P e₁' f₁) fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩<GOAL>∃ g₁', ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩), f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => ⟨g₁' x, pathDestRight P e₁' f₁ x⟩
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l₁ l₂ : List Γ<VAR>l₃ : ListBlank Γ<GOAL>append (l₁ ++ l₂) l₃ = append l₁ (append l₂ l₃)
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l₁ l₂ : List Γ<VAR>l₃ : ListBlank Γ<VAR>l : List Γ<GOAL>append (l₁ ++ l₂) ⟦l⟧ = append l₁ (append l₂ ⟦l⟧)
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l₁ l₂ : List Γ<VAR>l₃ : ListBlank Γ<VAR>l : List Γ<GOAL>append (l₁ ++ l₂) (mk l) = append l₁ (append l₂ (mk l))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : DecidableEq α<VAR>i : α<GOAL>i ∈ image Prod.fst (s ×ˢ t) → i ∈ s
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J<VAR>hJ : J ∈ π<GOAL>(π.biUnion πi).restrict J = πi J
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J<VAR>hJ : J ∈ π<VAR>J₁ : Box ι<VAR>h₁ : J₁ ∈ (πi J).boxes<GOAL>J₁ ∈ ((π.biUnion πi).restrict J).boxes
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J<VAR>hJ : J ∈ π<GOAL>((π.biUnion πi).restrict J).iUnion ⊆ (πi J).iUnion
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>s✝ s₁ s₂ : Finset β<VAR>f : β → α<VAR>inst✝ : DecidableEq β<VAR>g : γ → β<VAR>s : Finset γ<GOAL>(image g s).lcm f = s.lcm (f ∘ g)
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<GOAL>S.toCycles ≫ S.moduleCatCyclesIso.hom = S.moduleCatToCycles
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<GOAL>S.f = S.moduleCatToCycles ≫ (LinearMap.ker S.g).subtype
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>α : Type u_4<VAR>l : Filter α<VAR>x : ℝ≥0<VAR>f : ℝ≥0∞ → α<GOAL>Tendsto f (𝓝 ↑x) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p r : R[X]<VAR>hp : p.Monic<VAR>u : R[X]ˣ<VAR>hq : (p * ↑u).Monic<GOAL>p = p * ↑u
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>inst✝ : DecidableRel R<VAR>a✝ b a : α<VAR>h : destutter' R a l = a :: l<GOAL>Chain' R (destutter' R a l)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>f : Filter X<VAR>inst✝ : CountableInterFilter f<VAR>hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f<GOAL>sᶜ ∈ f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>f : Filter X<VAR>inst✝ : CountableInterFilter f<VAR>hf : sᶜ ∉ f<GOAL>∃ x ∈ s, sᶜ ∉ 𝓝 x ⊓ f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsLindelof s<VAR>f : Filter X<VAR>inst✝ : CountableInterFilter f<VAR>hf : (f ⊓ 𝓟 s).NeBot<GOAL>∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : StarAddMonoid α<VAR>v : n → α<GOAL>(diagonal v)ᴴ = diagonal (star v)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : StarAddMonoid α<VAR>v : n → α<GOAL>(diagonal fun m => star (v m)) = diagonal (star v)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ≤ b ⊔ (a \ c ⊔ c \ b)
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>A✝ A : ValuationSubring K<VAR>P : Ideal ↥A<VAR>inst✝ : P.IsPrime<VAR>x : ↥A<GOAL>(A.ofPrime P).valuation ↑x = 1 ↔ x ∈ P.primeCompl
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>A✝ A : ValuationSubring K<VAR>P : Ideal ↥A<VAR>inst✝ : P.IsPrime<VAR>x : ↥A<GOAL>(A.ofPrime P).valuation ↑x = 1 ↔ (A.ofPrime P).valuation ↑((algebraMap ↥A ↥(A.ofPrime P)) x) = 1
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>x : Cauchy abv<VAR>f : CauSeq β abv<VAR>hf : ⟦f⟧ ≠ 0<GOAL>(⟦f⟧)⁻¹ * ⟦f⟧ = 1
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>x : Cauchy abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<GOAL>(⟦f⟧)⁻¹ * ⟦f⟧ = 1
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>x : Cauchy abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<GOAL>mk (f.inv ⋯ * f) = 1
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>inst✝³ : CommRing O<VAR>inst✝² : Algebra O R<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O R<VAR>hv : v.Integers O<VAR>x y : O<VAR>h : x ∣ y<VAR>z : O<VAR>hz : y = x * z<GOAL>v ((algebraMap O R) y) ≤ v ((algebraMap O R) x)
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>inst✝³ : CommRing O<VAR>inst✝² : Algebra O R<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O R<VAR>hv : v.Integers O<VAR>x y : O<VAR>h : x ∣ y<VAR>z : O<VAR>hz : y = x * z<GOAL>v ((algebraMap O R) x) * v ((algebraMap O R) z) ≤ v ((algebraMap O R) x) * 1
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>g : LocallyConstant ↑(π C fun x => ord I x < o₁) ℤ<VAR>hg : g ∈ range (π C fun x => ord I x < o₁)<GOAL>(πs C o₁) g ∈ smaller C o₂
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>g : LocallyConstant ↑(π C fun x => ord I x < o₁) ℤ<VAR>hg : g ∈ range (π C fun x => ord I x < o₁)<GOAL>∃ x ∈ range (π C fun x => ord I x < o₂), (πs C o₂) x = (πs C o₁) g
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>g : LocallyConstant ↑(π C fun x => ord I x < o₁) ℤ<VAR>hg : g ∈ range (π C fun x => ord I x < o₁)<GOAL>(πs' C h) g ∈ range (π C fun x => ord I x < o₂) ∧ (πs C o₂) ((πs' C h) g) = (πs C o₁) g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>N✝ N₁ N₂ P P₁ P₂ N : Submodule R M<GOAL>Module.annihilator R (M ⧸ N) = N.colon ⊤
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddMonoid G<VAR>p : k[G] → Prop<VAR>f : k[G]<VAR>hM : ∀ (g : G), p ((of k G) (Multiplicative.ofAdd g))<VAR>hadd : ∀ (f g : k[G]), p f → p g → p (f + g)<VAR>hsmul : ∀ (r : k) (f : k[G]), p f → p (r • f)<GOAL>p f
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddMonoid G<VAR>p : k[G] → Prop<VAR>f : k[G]<VAR>hM : ∀ (g : G), p ((of k G) (Multiplicative.ofAdd g))<VAR>hadd : ∀ (f g : k[G]), p f → p g → p (f + g)<VAR>hsmul : ∀ (r : k) (f : k[G]), p f → p (r • f)<GOAL>p 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddMonoid G<VAR>p : k[G] → Prop<VAR>f : k[G]<VAR>hM : ∀ (g : G), p ((of k G) (Multiplicative.ofAdd g))<VAR>hadd : ∀ (f g : k[G]), p f → p g → p (f + g)<VAR>hsmul : ∀ (r : k) (f : k[G]), p f → p (r • f)<VAR>g : G<VAR>r : k<GOAL>p (Finsupp.single g r)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝¹ : F.Final<VAR>inst✝ : IsFilteredOrEmpty C<VAR>X Y : D<VAR>f g : X ⟶ Y<VAR>P : StructuredArrow X F → Prop := fun h => ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂<VAR>h₀ : P (StructuredArrow.mk (f ≫ Final.homToLift F Y))<GOAL>Nonempty (P (StructuredArrow.mk (g ≫ Final.homToLift F Y)))
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝¹ : F.Final<VAR>inst✝ : IsFilteredOrEmpty C<VAR>X Y : D<VAR>f g : X ⟶ Y<VAR>P : StructuredArrow X F → Prop := fun h => ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂<VAR>h₀ : P (StructuredArrow.mk (f ≫ Final.homToLift F Y))<GOAL>∀ {j₁ j₂ : StructuredArrow X F}, (j₁ ⟶ j₂) → P j₁ → P j₂
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝¹ : F.Final<VAR>inst✝ : IsFilteredOrEmpty C<VAR>X Y : D<VAR>f g : X ⟶ Y<VAR>P : StructuredArrow X F → Prop := fun h => ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂<VAR>h₀ : P (StructuredArrow.mk (f ≫ Final.homToLift F Y))<GOAL>∀ {j₁ j₂ : StructuredArrow X F}, (j₁ ⟶ j₂) → P j₂ → P j₁
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>X Y : C<VAR>D : Type u₂<VAR>inst✝⁷ : Category.{w, u₂} D<VAR>E : Type u₃<VAR>inst✝⁶ : Category.{w', u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A A' B B' : C<VAR>inst✝⁵ : HasBinaryProduct A B<VAR>inst✝⁴ : HasBinaryProduct A' B'<VAR>inst✝³ : HasBinaryProduct (F.obj A) (F.obj B)<VAR>inst✝² : HasBinaryProduct (F.obj A') (F.obj B')<VAR>inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))<VAR>inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)<VAR>f : A ⟶ A'<VAR>g : B ⟶ B'<GOAL>F.map (prod.map f g) ≫ prodComparison F A' B' = prodComparison F A B ≫ prod.map (F.map f) (F.map g)
<VAR>α : Type u<VAR>n : ℕ<VAR>h : n ≤ [].length<GOAL>[].rotate' n = drop n [] ++ take n []
<VAR>α : Type u<VAR>l : List α<VAR>h : 0 ≤ l.length<GOAL>l.rotate' 0 = drop 0 l ++ take 0 l
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>n : ℕ<VAR>h : n + 1 ≤ (a :: l).length<GOAL>(a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>n : ℕ<VAR>h : n + 1 ≤ (a :: l).length<VAR>hnl : n ≤ l.length<GOAL>(a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>n : ℕ<VAR>h : n + 1 ≤ (a :: l).length<VAR>hnl : n ≤ l.length<VAR>hnl' : n ≤ (l ++ [a]).length<GOAL>(a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
<VAR>α : Type u<VAR>a : α<VAR>l : List α<VAR>n : ℕ<VAR>h : n + 1 ≤ (a :: l).length<VAR>hnl : n ≤ l.length<VAR>hnl' : n ≤ (l ++ [a]).length<GOAL>drop n l ++ [a] ++ take n l = drop n l ++ a :: take n l
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>x : ⨂[R] (i : ι), s i<VAR>p : FreeAddMonoid (R × ((i : ι) → s i))<GOAL>p ∈ x.lifts ↔ (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) p).sum = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel G.Adj<VAR>a b₁ b₂ x z y : α<VAR>h : G.Adj x y<VAR>w : G.Walk y z<GOAL>(Walk.boxProdRight G a (cons' x y z h w)).ofBoxProdRight = cons' x y z h w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel G.Adj<VAR>a b₁ b₂ x z y : α<VAR>h : G.Adj x y<VAR>w : G.Walk y z<GOAL>cons ⋯ (Walk.boxProdRight G a w).ofBoxProdRight = cons' x y z h w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel G.Adj<VAR>a b₁ b₂ x z y : α<VAR>h : G.Adj x y<VAR>w : G.Walk y z<GOAL>G.Adj (a, x).2 ((G.boxProdRight G a).toHom y).2 ∧ (a, x).1 = ((G.boxProdRight G a).toHom y).1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>count s = ∑' (i : ↑s), 1
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cone F✝<VAR>F : J ⥤ C<VAR>s : Cone F<VAR>G : K ⥤ C<VAR>t : Cone G<VAR>P : IsLimit s<VAR>Q : IsLimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<GOAL>Q.lift ((Cones.equivalenceOfReindexing e.symm w').functor.obj s) ≫ P.lift ((Cones.equivalenceOfReindexing e w).functor.obj t) = 𝟙 s.pt
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cone F✝<VAR>F : J ⥤ C<VAR>s : Cone F<VAR>G : K ⥤ C<VAR>t : Cone G<VAR>P : IsLimit s<VAR>Q : IsLimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<GOAL>∀ (j : J), (Q.lift ((Cones.equivalenceOfReindexing e.symm w').functor.obj s) ≫ P.lift ((Cones.equivalenceOfReindexing e w).functor.obj t)) ≫ s.π.app j = 𝟙 s.pt ≫ s.π.app j