ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ : Multiset α<VAR>a✝ b a : α<VAR>s t : Multiset α<VAR>h : a ∈ t<GOAL>(s + t).erase a = s + t.erase a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>p : R[X]<VAR>m : ℕ<VAR>i j : n<GOAL>(matPolyEquiv (p • 1)).coeff m i j = (Polynomial.map (algebraMap R (Matrix n n R)) p).coeff m i j
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>p : R[X]<VAR>m : ℕ<VAR>i j : n<GOAL>(if i = j then p else 0).coeff m = if i = j then p.coeff m else 0
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℤ<GOAL>x ≠ ↑m
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℤ<GOAL>x ≠ ↑↑m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x✝ y✝ : M<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p p' : Submodule R M<VAR>x y : M<GOAL>Setoid.r x y ↔ -(x - y) ∈ p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x✝ y✝ : M<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p p' : Submodule R M<VAR>x y : M<GOAL>-x + y ∈ p.toAddSubgroup ↔ -x + y ∈ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m n : ℕ<GOAL>Fintype.card (Fin n → Fin m) = Fintype.card (Fin (m ^ n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n✝ : ℕ<VAR>ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i : Fin n, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n<VAR>f : Fin (n + 1) → Fin (n✝ + 1)<GOAL>∑ i : Fin (n + 1), ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n✝ : ℕ<VAR>ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i : Fin n, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n<VAR>f : Fin (n + 1) → Fin (n✝ + 1)<GOAL>∑ x : Fin n, ↑(f x.castSucc) * (n✝ + 1) ^ ↑x + ↑(f (Fin.last n)) * (n✝ + 1) ^ n < (n✝ + 1) ^ (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n✝ : ℕ<VAR>ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i : Fin n, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n<VAR>f : Fin (n + 1) → Fin (n✝ + 1)<GOAL>(n✝ + 1) ^ n + n✝ * (n✝ + 1) ^ n = (n✝ + 1) ^ (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m n : ℕ<VAR>ih : ∀ (a : Fin (m ^ n)), ⟨∑ i : Fin n, ↑a / m ^ ↑i % m * m ^ ↑i, ⋯⟩ = a<VAR>a : Fin (m ^ (n + 1))<GOAL>⟨∑ i : Fin (n + 1), ↑a / m ^ ↑i % m * m ^ ↑i, ⋯⟩ = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m n : ℕ<VAR>a : Fin (m ^ (n + 1))<VAR>ih : ∀ i < m ^ n, ∑ x : Fin n, i / m ^ ↑x % m * m ^ ↑x = i<GOAL>⟨∑ i : Fin (n + 1), ↑a / m ^ ↑i % m * m ^ ↑i, ⋯⟩ = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m n : ℕ<VAR>a : Fin (m ^ (n + 1))<VAR>ih : ∀ i < m ^ n, ∑ x : Fin n, i / m ^ ↑x % m * m ^ ↑x = i<GOAL>↑⟨∑ i : Fin (n + 1), ↑a / m ^ ↑i % m * m ^ ↑i, ⋯⟩ = ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m n : ℕ<VAR>a : Fin (m ^ (n + 1))<VAR>ih : ∀ i < m ^ n, ∑ x : Fin n, i / m ^ ↑x % m * m ^ ↑x = i<GOAL>↑a % m + m * ∑ i : Fin n, ↑a / m / m ^ ↑i % m * m ^ ↑i = ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m n : ℕ<VAR>a : Fin (m ^ (n + 1))<VAR>ih : ∀ i < m ^ n, ∑ x : Fin n, i / m ^ ↑x % m * m ^ ↑x = i<GOAL>↑a < m * m ^ n
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurve γ v<VAR>a : ℝ<GOAL>IsIntegralCurve (γ ∘ fun x => x * a) (a • v)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v univ<VAR>a : ℝ<GOAL>IsIntegralCurveOn (γ ∘ fun x => x * a) (a • v) univ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝¹ : T2Space X<VAR>inst✝ : SequentialSpace X<VAR>s : Set X<GOAL>IsClosed s ↔ ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝¹ : T2Space X<VAR>inst✝ : SequentialSpace X<VAR>s : Set X<VAR>h : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)<VAR>u : ℕ → X<VAR>p : X<VAR>hu : ∀ (n : ℕ), u n ∈ s<VAR>hup : Tendsto u atTop (𝓝 p)<GOAL>∀ᶠ (x : ℕ) in atTop, u x ∈ s ∩ insert p (range u)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝¹ : T2Space X<VAR>inst✝ : SequentialSpace X<VAR>s : Set X<VAR>h : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)<VAR>u : ℕ → X<VAR>p : X<VAR>hu : ∀ (n : ℕ), u n ∈ s<VAR>hup : Tendsto u atTop (𝓝 p)<GOAL>∃ a, ∀ (b : ℕ), a ≤ b → u b ∈ s
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocMod hp a b = toIocMod hp 0 (b - a) + a
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>hL : f₁ =ᶠ[𝓝 x] f<GOAL>(fderiv 𝕜 f₁ x) 1 = (fderiv 𝕜 f x) 1
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝ : Category.{u_3, u_2} D<VAR>ε : C ≌ D<VAR>h : IsIdempotentComplete C<VAR>X' : D<VAR>p : X' ⟶ X'<VAR>hp : p ≫ p = p<VAR>φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'<GOAL>∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝ : Category.{u_3, u_2} D<VAR>ε : C ≌ D<VAR>h : IsIdempotentComplete C<VAR>X' : D<VAR>p : X' ⟶ X'<VAR>hp : p ≫ p = p<VAR>φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'<GOAL>∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝ : Category.{u_3, u_2} D<VAR>ε : C ≌ D<VAR>h : IsIdempotentComplete C<VAR>X' : D<VAR>p : X' ⟶ X'<VAR>hp : p ≫ p = p<VAR>φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'<VAR>Y : C<VAR>i : Y ⟶ ε.inverse.obj X'<VAR>e : ε.inverse.obj X' ⟶ Y<VAR>h₁ : i ≫ e = 𝟙 Y<VAR>h₂ : e ≫ i = ε.inverse.map p<GOAL>∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝ : Category.{u_3, u_2} D<VAR>ε : C ≌ D<VAR>h : IsIdempotentComplete C<VAR>X' : D<VAR>p : X' ⟶ X'<VAR>hp : p ≫ p = p<VAR>φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'<VAR>Y : C<VAR>i : Y ⟶ ε.inverse.obj X'<VAR>e : ε.inverse.obj X' ⟶ Y<VAR>h₁ : i ≫ e = 𝟙 Y<VAR>h₂ : e ≫ i = ε.inverse.map p<GOAL>ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y) ∧ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g✝ : β → α<VAR>a b : α<VAR>s : Finset β<VAR>g : β → γ<VAR>hg : Injective g<GOAL>HasProd (extend g f 1) a ↔ HasProd f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g✝ : β → α<VAR>a b : α<VAR>s : Finset β<VAR>g : β → γ<VAR>hg : Injective g<GOAL>∀ x ∉ Set.range g, extend g f 1 x = 1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.25479, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>p : ℤ<GOAL>((inl φ).comp ↑(fst φ) ⋯).v p p ⋯ = (Cochain.ofHom (𝟙 F)).v p p ⋯
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<GOAL>(image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<GOAL>(image2 f ↑s ↑t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<VAR>k : ℕ<VAR>hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)<VAR>x : AdicCauchySequence I N<VAR>hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤<VAR>x✝ n : ℕ<GOAL>g (↑x (k + n)) ∈ Submodule.map g (I ^ (k + n) • ⊤)
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<VAR>k : ℕ<VAR>hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)<VAR>x : AdicCauchySequence I N<VAR>hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤<VAR>x✝ n : ℕ<GOAL>g (↑x (k + n)) ∈ I ^ (k + n) • ⊤
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<VAR>k : ℕ<VAR>hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)<VAR>x : AdicCauchySequence I N<VAR>hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤<VAR>x✝ n : ℕ<VAR>d : N<VAR>hdmem : d ∈ ↑(I ^ (k + n) • ⊤)<VAR>hd : g d = g (↑x (k + n))<GOAL>∃ d y, d ∈ I ^ (k + n) • ⊤ ∧ f y = ↑x (k + n) - d
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R N<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<VAR>k : ℕ<VAR>hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ range f = I ^ (n - k) • (I ^ k • ⊤ ⊓ range f)<VAR>x : AdicCauchySequence I N<VAR>hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤<VAR>x✝ n : ℕ<VAR>d : N<VAR>hdmem : d ∈ ↑(I ^ (k + n) • ⊤)<VAR>hd : g d = g (↑x (k + n))<VAR>y : M<VAR>hdy : f y = ↑x (k + n) - d<GOAL>∃ d y, d ∈ I ^ (k + n) • ⊤ ∧ f y = ↑x (k + n) - d
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s : Finset α<VAR>t : Finset β<GOAL>0 ≤ edgeDensity r s t
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>hr : r < 0<VAR>x✝ : E<GOAL>x✝ ∈ p.closedBall x r ↔ x✝ ∈ ∅
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>hr : r < 0<VAR>x✝ : E<GOAL>r < p (x✝ - x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<GOAL>BijOn f {a} {b} ↔ f a = b
<VAR>f : ℕ → ℝ<VAR>h_nonneg : ∀ (n : ℕ), 0 ≤ f n<VAR>h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_succ_diff : SuccDiffBounded 2 fun x => 2 ^ x<GOAL>(Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f
<VAR>f : ℕ → ℝ<VAR>h_nonneg : ∀ (n : ℕ), 0 ≤ f n<VAR>h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_succ_diff : SuccDiffBounded 2 fun x => 2 ^ x<VAR>x✝ : ℕ<GOAL>2 ^ x✝ = ↑(2 ^ (x✝ + 1)) - ↑(2 ^ x✝)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F₁ : A ⥤ C<VAR>U₁ : C ⥤ A<VAR>F₂ : B ⥤ D<VAR>U₂ : D ⥤ B<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : F₁ ⊣ U₁<VAR>adj₄ : F₂ ⊣ U₂<VAR>α : F₁ ⋙ L₂ ⟶ L₁ ⋙ F₂<VAR>d : D<GOAL>({ toFun := fun α => whiskerLeft (U₂ ⋙ R₁) adj₃.unit ≫ whiskerRight (whiskerLeft U₂ α) U₁ ≫ whiskerRight adj₄.counit (R₂ ⋙ U₁), invFun := fun β => whiskerRight adj₄.unit (R₁ ⋙ F₁) ≫ whiskerRight (whiskerLeft F₂ β) F₁ ≫ whiskerLeft (F₂ ⋙ R₂) adj₃.counit, left_inv := ⋯, right_inv := ⋯ } ({ toFun := fun α => whiskerLeft (R₁ ⋙ F₁) adj₂.unit ≫ whiskerRight (whiskerLeft R₁ α) R₂ ≫ whiskerRight adj₁.counit (F₂ ⋙ R₂), invFun := fun β => whiskerRight adj₁.unit (F₁ ⋙ L₂) ≫ whiskerRight (whiskerLeft L₁ β) L₂ ≫ whiskerLeft (L₁ ⋙ F₂) adj₂.counit, left_inv := ⋯, right_inv := ⋯ } α)).app d = ((Trans.trans (Trans.trans ((F₁ ⋙ L₂).leftUnitor.homCongr (L₁ ⋙ F₂).rightUnitor).symm { toFun := fun α => whiskerLeft ((U₂ ⋙ R₁) ⋙ 𝟭 A) { homEquiv := fun X Z => (adj₂.homEquiv (F₁.obj X) Z).trans (adj₃.homEquiv X (R₂.obj Z)), unit := adj₃.unit ≫ whiskerLeft F₁ (whiskerRight adj₂.unit U₁) ≫ (F₁.associator (L₂ ⋙ R₂) U₁).inv, counit := (R₂.associator U₁ (F₁ ⋙ L₂)).hom ≫ whiskerLeft R₂ (whiskerRight adj₃.counit L₂) ≫ adj₂.counit, homEquiv_unit := ⋯, homEquiv_counit := ⋯ }.unit ≫ whiskerRight (whiskerLeft (U₂ ⋙ R₁) α) (R₂ ⋙ U₁) ≫ whiskerRight { homEquiv := fun X Z => (adj₄.homEquiv (L₁.obj X) Z).trans (adj₁.homEquiv X (U₂.obj Z)), unit := adj₁.unit ≫ whiskerLeft L₁ (whiskerRight adj₄.unit R₁) ≫ (L₁.associator (F₂ ⋙ U₂) R₁).inv, counit := (U₂.associator R₁ (L₁ ⋙ F₂)).hom ≫ whiskerLeft U₂ (whiskerRight adj₁.counit F₂) ≫ adj₄.counit, homEquiv_unit := ⋯, homEquiv_counit := ⋯ }.counit (𝟭 D ⋙ R₂ ⋙ U₁), invFun := fun β => whiskerRight { homEquiv := fun X Z => (adj₄.homEquiv (L₁.obj X) Z).trans (adj₁.homEquiv X (U₂.obj Z)), unit := adj₁.unit ≫ whiskerLeft L₁ (whiskerRight adj₄.unit R₁) ≫ (L₁.associator (F₂ ⋙ U₂) R₁).inv, counit := (U₂.associator R₁ (L₁ ⋙ F₂)).hom ≫ whiskerLeft U₂ (whiskerRight adj₁.counit F₂) ≫ adj₄.counit, homEquiv_unit := ⋯, homEquiv_counit := ⋯ }.unit (𝟭 A ⋙ F₁ ⋙ L₂) ≫ whiskerRight (whiskerLeft (L₁ ⋙ F₂) β) (F₁ ⋙ L₂) ≫ whiskerLeft ((L₁ ⋙ F₂) ⋙ 𝟭 D) { homEquiv := fun X Z => (adj₂.homEquiv (F₁.obj X) Z).trans (adj₃.homEquiv X (R₂.obj Z)), unit := adj₃.unit ≫ whiskerLeft F₁ (whiskerRight adj₂.unit U₁) ≫ (F₁.associator (L₂ ⋙ R₂) U₁).inv, counit := (R₂.associator U₁ (F₁ ⋙ L₂)).hom ≫ whiskerLeft R₂ (whiskerRight adj₃.counit L₂) ≫ adj₂.counit, homEquiv_unit := ⋯, homEquiv_counit := ⋯ }.counit, left_inv := ⋯, right_inv := ⋯ }) ((U₂ ⋙ R₁).rightUnitor.homCongr (R₂ ⋙ U₁).leftUnitor)) α).app d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>a : α<GOAL>(s \ {a}).ncard ≤ s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>a : α<VAR>hs : s.Finite<GOAL>(s \ {a}).ncard ≤ s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>a : α<VAR>hs : s.Infinite<GOAL>(s \ {a}).ncard ≤ s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>a : α<VAR>hs : s.Infinite<GOAL>(s \ {a}).ncard = 0
<VAR>b : Bool<VAR>n : ℕ<GOAL>bit b ↑n = ↑(Nat.bit b n)
<VAR>b : Bool<VAR>n : ℕ<GOAL>(2 * ↑n + bif b then 1 else 0) = ↑(2 * n + bif b then 1 else 0)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Iic a) a<VAR>hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>hf : Tendsto f atBot (𝓝 m)<VAR>hcont : ContinuousOn f (Iic a)<GOAL>∫ (x : ℝ) in Iic a, f' x = f a - m
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Iic a) a<VAR>hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>hf : Tendsto f atBot (𝓝 m)<VAR>hcont : ContinuousOn f (Iic a)<GOAL>Tendsto (fun i => ∫ (x : ℝ) in id i..a, f' x) atBot (𝓝 (f a - m))
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Iic a) a<VAR>hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>hf : Tendsto f atBot (𝓝 m)<VAR>hcont : ContinuousOn f (Iic a)<GOAL>(fun k => f a - f k) =ᶠ[atBot] fun i => ∫ (x : ℝ) in id i..a, f' x
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Iic a) a<VAR>hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>hf : Tendsto f atBot (𝓝 m)<VAR>hcont : ContinuousOn f (Iic a)<VAR>x : ℝ<VAR>hx : x ∈ Iic a<GOAL>f a - f x = ∫ (x : ℝ) in id x..a, f' x
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Iic a) a<VAR>hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>hf : Tendsto f atBot (𝓝 m)<VAR>hcont : ContinuousOn f (Iic a)<VAR>x : ℝ<VAR>hx : x ∈ Iic a<GOAL>∫ (x : ℝ) in id x..a, f' x = f a - f x
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Iic a) a<VAR>hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>hf : Tendsto f atBot (𝓝 m)<VAR>hcont : ContinuousOn f (Iic a)<VAR>x : ℝ<VAR>hx : x ∈ Iic a<GOAL>IntervalIntegrable f' volume x a
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Iic a) a<VAR>hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>hf : Tendsto f atBot (𝓝 m)<VAR>hcont : ContinuousOn f (Iic a)<VAR>x : ℝ<VAR>hx : x ∈ Iic a<GOAL>IntegrableOn f' (Ioc x a) volume
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : Lattice β<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : BoundedOrder β<VAR>f✝ : α ≃o β<VAR>inst✝ : ComplementedLattice α<VAR>f : α ≃o β<VAR>x : β<GOAL>∃ b, IsCompl x b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : Lattice β<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : BoundedOrder β<VAR>f✝ : α ≃o β<VAR>inst✝ : ComplementedLattice α<VAR>f : α ≃o β<VAR>x : β<VAR>y : α<VAR>hy : IsCompl (f.symm x) y<GOAL>∃ b, IsCompl x b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁴ : Lattice α<VAR>inst✝³ : Lattice β<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : BoundedOrder β<VAR>f✝ : α ≃o β<VAR>inst✝ : ComplementedLattice α<VAR>f : α ≃o β<VAR>x : β<VAR>y : α<VAR>hy : IsCompl (f.symm x) (f.symm (f y))<GOAL>∃ b, IsCompl x b
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<GOAL>ClassGroup.mk (XYIdeal' ⋯) * ClassGroup.mk (XYIdeal' h) = 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<GOAL>ClassGroup.mk (XYIdeal' ⋯ * XYIdeal' h) = 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<GOAL>C ↑(p ^ (n + 1)) ∣ (bind₁ fun b => (rename fun i => (b, i)) (W_ ℤ (n + 1))) Φ - ∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>key : (bind₁ fun b => (rename fun i => (b, i)) ((expand p) (W_ ℤ n))) Φ = (bind₁ fun i => (expand p) (wittStructureInt p Φ i)) (W_ ℤ n)<GOAL>C ↑(p ^ (n + 1)) ∣ (bind₁ fun b => (rename fun i => (b, i)) (W_ ℤ (n + 1))) Φ - ∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>key : (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun b => (rename fun i => (b, i)) ((expand p) (W_ ℤ n))) Φ) = (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i => (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))<GOAL>C ↑(p ^ (n + 1)) ∣ (bind₁ fun b => (rename fun i => (b, i)) (W_ ℤ (n + 1))) Φ - ∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i)