ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m₁ m₂ m₃ : M<VAR>X : C<GOAL>inv ((F.μ (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X ≫ (F.μIso m₁ (m₂ ⊗ m₃)).inv.app X ≫ (F.μIso m₂ m₃).inv.app ((F.obj m₁).obj X)) = (F.μ m₂ m₃).app ((F.obj m₁).obj X) ≫ (F.μ m₁ (m₂ ⊗ m₃)).app X ≫ (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (F.μIso (m₁ ⊗ m₂) m₃).inv.app X
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>n : ℕ<VAR>h : Module.rank R M ≤ ↑n<GOAL>finrank R M ≤ n
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>n : ℕ<VAR>h : Module.rank R M ≤ ↑n<GOAL>Module.rank R M < ℵ₀
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>n : ℕ<VAR>h : Module.rank R M ≤ ↑n<GOAL>↑n < ℵ₀
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LocalRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : LocalRing S<VAR>inst✝¹ : CommRing T<VAR>inst✝ : LocalRing T<VAR>f : R ≃+* S<VAR>x : ResidueField R<GOAL>(map ↑f.symm) ((map ↑f) x) = x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LocalRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : LocalRing S<VAR>inst✝¹ : CommRing T<VAR>inst✝ : LocalRing T<VAR>f : R ≃+* S<VAR>x : ResidueField S<GOAL>(map ↑f) ((map ↑f.symm) x) = x
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝² : CommGroup G<VAR>g g' : G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>f : ℤ → G<VAR>hf₁ : HasProd (fun n => f ↑n) g<VAR>hf₂ : HasProd (fun n => f (-↑n)) g'<GOAL>HasProd f (g * g' / f 0)
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝² : CommGroup G<VAR>g g' : G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>f : ℤ → G<VAR>hf₁ : HasProd (fun n => f ↑n) g<VAR>hf₂ : HasProd (fun n => f (-↑n)) g'<GOAL>HasProd (fun n => f (-(↑n + 1))) (g' / f 0)
<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 : O<VAR>hx : IsUnit ((algebraMap O R) x)<VAR>hvx : v ((algebraMap O R) x) = 1<VAR>u : Rˣ<VAR>hu : ↑u = (algebraMap O R) x<VAR>h1 : v ↑u ≤ 1<GOAL>v ↑u⁻¹ ≤ 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 : O<VAR>hx : IsUnit ((algebraMap O R) x)<VAR>hvx : v ((algebraMap O R) x) = 1<VAR>u : Rˣ<VAR>hu : ↑u = (algebraMap O R) x<VAR>h1 : v ↑u ≤ 1<VAR>h2 : v ↑u⁻¹ ≤ 1<VAR>r1 : O<VAR>hr1 : (algebraMap O R) r1 = ↑u<VAR>r2 : O<VAR>hr2 : (algebraMap O R) r2 = ↑u⁻¹<GOAL>(algebraMap O R) (r1 * r2) = (algebraMap O R) 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 : O<VAR>hx : IsUnit ((algebraMap O R) x)<VAR>hvx : v ((algebraMap O R) x) = 1<VAR>u : Rˣ<VAR>hu : ↑u = (algebraMap O R) x<VAR>h1 : v ↑u ≤ 1<VAR>h2 : v ↑u⁻¹ ≤ 1<VAR>r1 : O<VAR>hr1 : (algebraMap O R) r1 = ↑u<VAR>r2 : O<VAR>hr2 : (algebraMap O R) r2 = ↑u⁻¹<GOAL>(algebraMap O R) (r2 * r1) = (algebraMap O R) 1
<VAR>B : Type u_1<VAR>inst✝⁶ : TopologicalSpace B<VAR>F₁ : Type u_2<VAR>inst✝⁵ : TopologicalSpace F₁<VAR>E₁ : B → Type u_3<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_4<VAR>inst✝³ : TopologicalSpace F₂<VAR>E₂ : B → Type u_5<VAR>inst✝² : TopologicalSpace (TotalSpace F₂ E₂)<VAR>e₁ : Trivialization F₁ TotalSpace.proj<VAR>e₂ : Trivialization F₂ TotalSpace.proj<VAR>inst✝¹ : (x : B) → Zero (E₁ x)<VAR>inst✝ : (x : B) → Zero (E₂ x)<VAR>x : B<VAR>w₁ : F₁<VAR>w₂ : F₂<VAR>h₁ : x ∈ e₁.baseSet<VAR>h₂ : x ∈ e₂.baseSet<GOAL>toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>h_zero : ¬a + b = 0<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>h_zero : ¬a + b = 0<VAR>h_nonzero : ¬(a = 0 ∧ b = 0)<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>h_zero : ¬a + b = 0<VAR>h_nonzero : ¬(a = 0 ∧ b = 0)<VAR>h_add : a / (a + b) + b / (a + b) = 1<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>h_zero : ¬a + b = 0<VAR>h_nonzero : ¬(a = 0 ∧ b = 0)<VAR>h_add : a / (a + b) + b / (a + b) = 1<VAR>h : (a / (a + b)) ^ p + (b / (a + b)) ^ p ≤ 1<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>h_zero : ¬a + b = 0<VAR>h_nonzero : ¬(a = 0 ∧ b = 0)<VAR>h_add : a / (a + b) + b / (a + b) = 1<VAR>h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>h_zero : ¬a + b = 0<VAR>h_nonzero : ¬(a = 0 ∧ b = 0)<VAR>h_add : a / (a + b) + b / (a + b) = 1<VAR>h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1<VAR>hab_0 : (a + b) ^ p ≠ 0<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>h_zero : ¬a + b = 0<VAR>h_nonzero : ¬(a = 0 ∧ b = 0)<VAR>h_add : a / (a + b) + b / (a + b) = 1<VAR>h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1<VAR>hab_0 : (a + b) ^ p ≠ 0<VAR>hab_0' : 0 < (a + b) ^ p<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>h_zero : ¬a + b = 0<VAR>h_nonzero : ¬(a = 0 ∧ b = 0)<VAR>h_add : a / (a + b) + b / (a + b) = 1<VAR>h : a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p ≤ 1<VAR>hab_0 : (a + b) ^ p ≠ 0<VAR>hab_0' : 0 < (a + b) ^ p<VAR>h_mul : (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | i ≤ τ ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>this : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ<GOAL>MeasurableSet {ω | i ≤ τ ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>this : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ<GOAL>MeasurableSet {ω | τ ω < i}ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>c : 𝕜<VAR>f : ↥(Lp F' 1 μ)<GOAL>(condexpL1CLM F' hm μ) (c • f) = c • (condexpL1CLM F' hm μ) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>c : 𝕜<VAR>f : ↥(Lp F' 1 μ)<GOAL>∀ (c : 𝕜) (s : Set α) (x : F'), (condexpInd F' hm μ s) (c • x) = c • (condexpInd F' hm μ s) x
<VAR>α β : Type u<VAR>ι : Sort u_1<VAR>f : ι → Cardinal.{v}<GOAL>lift.{u, v} (sInf (range f)) = sInf (range fun i => lift.{u, v} (f i))
<VAR>α β : Type u<VAR>ι : Sort u_1<VAR>f : ι → Cardinal.{v}<GOAL>(range fun i => lift.{u, v} (f i)) = lift.{u, v} '' range f
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<VAR>motive : (m : ℕ) → m ≤ n + 1 → Sort u_1<VAR>of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯<VAR>self : motive (n + 1) ⋯<VAR>mn : m ≤ n<VAR>msn : m ≤ n + 1<GOAL>leRec (motive := fun {n} mn => {motive : (m : ℕ) → m ≤ n → Sort u_1} → ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn) (fun {motive} of_succ self => self) (fun ⦃k⦄ h ih {motive} of_succ self => ih (fun i hi => of_succ i ⋯) (of_succ k ⋯ self)) msn of_succ self = leRec (motive := fun {n} mn => {motive : (m : ℕ) → m ≤ n → Sort u_1} → ((k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → motive n ⋯ → motive m mn) (fun {motive} of_succ self => self) (fun ⦃k⦄ h ih {motive} of_succ self => ih (fun i hi => of_succ i ⋯) (of_succ k ⋯ self)) mn (fun i hi => of_succ i ⋯) (of_succ n ⋯ self)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>a✝¹ : α<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>((κ.withDensity 1) a✝¹) s✝ = (κ a✝¹) s✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>a✝¹ : α<VAR>s✝ : Set β<VAR>a✝ : MeasurableSet s✝<GOAL>((κ a✝¹).withDensity (1 a✝¹)) s✝ = (κ a✝¹) s✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>a : α<VAR>b : β<VAR>ca : Computation α<VAR>cb : Computation β<VAR>ma : a ∈ ca<VAR>mb : b ∈ cb<VAR>ab : R a b<VAR>a' : α<VAR>ma' : a' ∈ ca<GOAL>∃ b, b ∈ cb ∧ R a' b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>a : α<VAR>b : β<VAR>ca : Computation α<VAR>cb : Computation β<VAR>ma : a ∈ ca<VAR>mb : b ∈ cb<VAR>ab : R a b<VAR>a' : α<VAR>ma' : a' ∈ ca<GOAL>∃ b, b ∈ cb ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>a : α<VAR>b : β<VAR>ca : Computation α<VAR>cb : Computation β<VAR>ma : a ∈ ca<VAR>mb : b ∈ cb<VAR>ab : R a b<VAR>b' : β<VAR>mb' : b' ∈ cb<GOAL>∃ a, a ∈ ca ∧ R a b'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>a : α<VAR>b : β<VAR>ca : Computation α<VAR>cb : Computation β<VAR>ma : a ∈ ca<VAR>mb : b ∈ cb<VAR>ab : R a b<VAR>b' : β<VAR>mb' : b' ∈ cb<GOAL>∃ a, a ∈ ca ∧ R a b
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>inst✝¹ : CommMonoid R<VAR>inst✝ : CommMonoidWithZero R'<VAR>g : Rˣ<VAR>hg : ∀ (x : Rˣ), x ∈ Subgroup.zpowers g<VAR>χ₁ χ₂ : MulChar R R'<GOAL>χ₁ = χ₂ ↔ χ₁ ↑g = χ₂ ↑g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>b c d : α<VAR>n : ℤ<VAR>b0 : 0 ≤ b<VAR>a0 : 0 ≤ -b<GOAL>-b = b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>b c d : α<VAR>n : ℤ<VAR>b0 : 0 ≤ b<VAR>a0 : 0 ≤ -b<VAR>this : b = 0<GOAL>-b = b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>a✝ b✝ : A<VAR>r : R<VAR>inst✝³ : OrderedCommRing R<VAR>inst✝² : OrderedRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : OrderedSMul R A<VAR>a b : R<VAR>h : a ≤ b<GOAL>(algebraMap R A) a ≤ (algebraMap R A) b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>a✝ b✝ : A<VAR>r : R<VAR>inst✝³ : OrderedCommRing R<VAR>inst✝² : OrderedRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : OrderedSMul R A<VAR>a b : R<VAR>h : a ≤ b<GOAL>0 ≤ (b - a) • 1
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>δ i.castSucc ≫ σ i = 𝟙 [n]
<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>h : ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i<VAR>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : CountableInterFilter f<GOAL>f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt 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>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : CountableInterFilter f<VAR>h : f ≤ 𝓟 s ∧ ∀ x ∈ s, ¬ClusterPt x f<GOAL>∃ ι U, (∀ (i : ι), IsOpen (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Set ι), t.Countable → ¬s ⊆ ⋃ i ∈ t, U i
<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>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : CountableInterFilter f<VAR>h : f ≤ 𝓟 s ∧ ∀ (x : ↑s), ∃ i, (↑x ∈ i ∧ IsOpen i) ∧ iᶜ ∈ f<GOAL>∃ ι U, (∀ (i : ι), IsOpen (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Set ι), t.Countable → ¬s ⊆ ⋃ i ∈ t, U i
<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>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : CountableInterFilter f<VAR>fsub : f ≤ 𝓟 s<VAR>U : ↑s → Set X<VAR>hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)<VAR>hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f<GOAL>∃ ι U, (∀ (i : ι), IsOpen (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Set ι), t.Countable → ¬s ⊆ ⋃ i ∈ t, U i
<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>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : CountableInterFilter f<VAR>fsub : f ≤ 𝓟 s<VAR>U : ↑s → Set X<VAR>hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)<VAR>hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f<GOAL>∀ (t : Set ↑s), t.Countable → ¬s ⊆ ⋃ i ∈ t, U i
<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>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : CountableInterFilter f<VAR>fsub : f ≤ 𝓟 s<VAR>U : ↑s → Set X<VAR>hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)<VAR>hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f<VAR>t : Set ↑s<VAR>ht : t.Countable<VAR>h : s ⊆ ⋃ i ∈ t, U i<GOAL>False
<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>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : CountableInterFilter f<VAR>fsub : f ≤ 𝓟 s<VAR>U : ↑s → Set X<VAR>hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)<VAR>hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f<VAR>t : Set ↑s<VAR>ht : t.Countable<VAR>h : s ⊆ ⋃ i ∈ t, U i<VAR>uinf : ⋃ i ∈ t, U i ∈ f.sets<GOAL>False
<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>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : CountableInterFilter f<VAR>fsub : f ≤ 𝓟 s<VAR>U : ↑s → Set X<VAR>hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)<VAR>hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f<VAR>t : Set ↑s<VAR>ht : t.Countable<VAR>h : s ⊆ ⋃ i ∈ t, U i<VAR>uinf : ⋃ i ∈ t, U i ∈ f.sets<VAR>uninf : ⋂ i ∈ t, (U i)ᶜ ∈ f<GOAL>False
<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>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : CountableInterFilter f<VAR>fsub : f ≤ 𝓟 s<VAR>U : ↑s → Set X<VAR>hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)<VAR>hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f<VAR>t : Set ↑s<VAR>ht : t.Countable<VAR>h : s ⊆ ⋃ i ∈ t, U i<VAR>uinf : ⋃ i ∈ t, U i ∈ f.sets<VAR>uninf : (⋃ i ∈ t, U i)ᶜ ∈ f<GOAL>False
<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>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : CountableInterFilter f<VAR>fsub : f ≤ 𝓟 s<VAR>U : ↑s → Set X<VAR>hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)<VAR>hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f<VAR>t : Set ↑s<VAR>ht : t.Countable<VAR>h : s ⊆ ⋃ i ∈ t, U i<VAR>uinf : ⋃ i ∈ t, U i ∈ f.sets<VAR>uninf✝ : (⋃ i ∈ t, U i)ᶜ ∈ f<VAR>uninf : (⋃ i ∈ t, U i)ᶜᶜ ∉ f<GOAL>False
<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>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : CountableInterFilter f<VAR>fsub : f ≤ 𝓟 s<VAR>U : ↑s → Set X<VAR>hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)<VAR>hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f<VAR>t : Set ↑s<VAR>ht : t.Countable<VAR>h : s ⊆ ⋃ i ∈ t, U i<VAR>uinf : ⋃ i ∈ t, U i ∈ f.sets<VAR>uninf✝ : (⋃ i ∈ t, U i)ᶜ ∈ f<VAR>uninf : ⋃ i ∈ t, U i ∉ f<GOAL>False
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>X : Augmented C<VAR>F : Arrow C<VAR>G : Augmented.toArrow.obj X ⟶ F<VAR>x : SimplexCategoryᵒᵖ<VAR>i : Fin ((Opposite.unop x).len + 1)<GOAL>(X.left.map ((SimplexCategory.mk 0).const (Opposite.unop x) i).op ≫ G.left) ≫ F.hom = X.hom.app x ≫ G.right
<VAR>α : Type u_1<VAR>l l₁ r₁ l₂ r₂ : List α<GOAL>l₂ ++ l₁ ++ l ++ (r₁ ++ r₂) = l₂ ++ (l₁ ++ l ++ r₁) ++ r₂
<VAR>n : ℕ<VAR>c : Char<VAR>l : List Char<GOAL>(replicate (n - { data := l }.length) c).IsPrefix (leftpad n c { data := l })
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<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>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiff I I' n f<VAR>hmn : 1 ≤ n<GOAL>Continuous (tangentMap I I' f)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<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>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f univ<VAR>hmn : 1 ≤ n<GOAL>Continuous (tangentMap I I' f)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<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>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f univ<VAR>hmn : 1 ≤ n<GOAL>ContinuousOn (tangentMap I I' f) univ
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<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>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f univ<VAR>hmn : 1 ≤ n<GOAL>tangentMap I I' f = tangentMapWithin I I' f univ