ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<GOAL>IsIntegralClosure (CyclotomicRing (p ^ 1) ℤ ℚ) ℤ (CyclotomicField (p ^ 1) ℚ)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Module A M<VAR>κ : Type u_6<VAR>inst✝ : Fintype κ<VAR>b : Basis ι A M<VAR>f : M →ₗ[A] M<GOAL>(detAux (Trunc.mk b)) f = ((toMatrix b b) f).det
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Module A M<VAR>κ : Type u_6<VAR>inst✝ : Fintype κ<VAR>b : Basis ι A M<VAR>f : M →ₗ[A] M<GOAL>(Trunc.lift (fun b => detMonoidHom.comp ↑(toMatrixAlgEquiv b)) ⋯ (Trunc.mk b)) f = ((toMatrix b b) f).det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>x : γ<VAR>s : (i : ι) → κ i → Set γ<GOAL>x ∈ ⋃ i, ⋃ j, s i j ↔ ∃ i j, x ∈ s i j
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁✝ s₂✝ t✝ t₁ t₂ u t s₁ s₂ s₁' s₂' : Set α<VAR>x : α<GOAL>x ∈ t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') ↔ x ∈ t.ite s₁ s₁' ∩ t.ite s₂ s₂'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁✝ s₂✝ t✝ t₁ t₂ u t s₁ s₂ s₁' s₂' : Set α<VAR>x : α<GOAL>(x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ x ∉ t ↔ (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ x ∉ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ x ∉ t)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : TopologicalGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : OrderedCommGroup H<VAR>inst✝ : ContinuousInv H<VAR>a : H<GOAL>Tendsto Inv.inv (𝓝[≥] a⁻¹) (𝓝[≤] a)
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a * b⁻¹ * b ≤ c * b ↔ a ≤ c * b
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>frontier s = closure s ∩ closure sᶜ
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : AddGroup α<VAR>a b : α<VAR>n : ℕ<VAR>x✝ : α<GOAL>(Equiv.addLeft a ^ n) x✝ = (Equiv.addLeft (n • a)) x✝
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End R M<VAR>h : IsNilpotent φ<GOAL>LinearMap.charpoly φ = X ^ finrank R M
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End R M<VAR>h : IsNilpotent φ<GOAL>LinearMap.charpoly φ - X ^ finrank R M = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End R M<VAR>h : IsNilpotent φ<GOAL>IsNilpotent (LinearMap.charpoly φ - X ^ finrank R M)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End R M<VAR>h : IsNilpotent φ<GOAL>IsNilpotent (LinearMap.charpoly φ - X ^ Fintype.card (ChooseBasisIndex R M))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End R M<VAR>h : IsNilpotent φ<GOAL>IsNilpotent ((LinearMap.toMatrix (chooseBasis R M) (chooseBasis R M)) φ)
<VAR>X : Scheme<GOAL>Opens.IsBasis X.affineOpens
<VAR>X : Scheme<GOAL>∀ {U : Opens ↑↑X.toPresheafedSpace} {x : ↑↑X.toPresheafedSpace}, x ∈ U → ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
<VAR>X : Scheme<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>x : ↑↑X.toPresheafedSpace<VAR>hU : x ∈ ↑U<GOAL>∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
<VAR>X : Scheme<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>x : ↑↑X.toPresheafedSpace<VAR>hU : x ∈ ↑U<VAR>S : Set ↑↑X.toPresheafedSpace<VAR>hS : S ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.map a).val.base}<VAR>hxS : x ∈ S<VAR>hSU : S ⊆ ↑U<GOAL>∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
<VAR>X : Scheme<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>x : ↑↑X.toPresheafedSpace<VAR>hU : x ∈ ↑U<VAR>S : Set ↑↑X.toPresheafedSpace<VAR>hS : S ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.map a).val.base}<VAR>hxS : x ∈ S<VAR>hSU : S ⊆ ↑U<GOAL>{ carrier := S, is_open' := ⋯ } ∈ X.affineOpens
<VAR>X : Scheme<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>x : ↑↑X.toPresheafedSpace<VAR>hU : x ∈ ↑U<VAR>i : X.affineBasisCover.J<VAR>hxS : x ∈ Set.range ⇑(X.affineBasisCover.map i).val.base<VAR>hSU : Set.range ⇑(X.affineBasisCover.map i).val.base ⊆ ↑U<GOAL>{ carrier := Set.range ⇑(X.affineBasisCover.map i).val.base, is_open' := ⋯ } ∈ X.affineOpens
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>x✝ : 𝕜<VAR>h : HasFPowerSeriesAt 0 p x✝<VAR>n : ℕ<VAR>x : Fin n → 𝕜<GOAL>(p n) x = (0 n) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>x✝ : 𝕜<VAR>h : HasFPowerSeriesAt 0 p x✝<VAR>n : ℕ<VAR>x : Fin n → 𝕜<GOAL>(ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((p n) fun x => 1)) x = (0 n) x
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : s.Nonempty<GOAL>x ∈ closure s ↔ infDist x s = 0
<VAR>I : Type u_1<VAR>inst✝³ : DecidableEq I<VAR>Z : I → Type u_2<VAR>inst✝² : (i : I) → CommMonoid (Z i)<VAR>inst✝¹ : Finite I<VAR>G : Type u_3<VAR>inst✝ : CommMonoid G<VAR>g h : ((i : I) → Z i) →* G<VAR>H : ∀ (i : I) (x : Z i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)<GOAL>g = h
<VAR>I : Type u_1<VAR>inst✝³ : DecidableEq I<VAR>Z : I → Type u_2<VAR>inst✝² : (i : I) → CommMonoid (Z i)<VAR>inst✝¹ : Finite I<VAR>G : Type u_3<VAR>inst✝ : CommMonoid G<VAR>g h : ((i : I) → Z i) →* G<VAR>H : ∀ (i : I) (x : Z i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)<VAR>val✝ : Fintype I<GOAL>g = h
<VAR>I : Type u_1<VAR>inst✝³ : DecidableEq I<VAR>Z : I → Type u_2<VAR>inst✝² : (i : I) → CommMonoid (Z i)<VAR>inst✝¹ : Finite I<VAR>G : Type u_3<VAR>inst✝ : CommMonoid G<VAR>g h : ((i : I) → Z i) →* G<VAR>H : ∀ (i : I) (x : Z i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)<VAR>val✝ : Fintype I<VAR>k : (i : I) → Z i<GOAL>g k = h k
<VAR>I : Type u_1<VAR>inst✝³ : DecidableEq I<VAR>Z : I → Type u_2<VAR>inst✝² : (i : I) → CommMonoid (Z i)<VAR>inst✝¹ : Finite I<VAR>G : Type u_3<VAR>inst✝ : CommMonoid G<VAR>g h : ((i : I) → Z i) →* G<VAR>H : ∀ (i : I) (x : Z i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)<VAR>val✝ : Fintype I<VAR>k : (i : I) → Z i<GOAL>∏ x : I, g (Pi.mulSingle x (k x)) = ∏ x : I, h (Pi.mulSingle x (k x))
<VAR>θ : ℝ<GOAL>2 • ↑(θ / 2) = ↑θ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.61158, u_1} C<VAR>inst✝² : Category.{?u.61162, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁✝ S₂✝ S₃ : ShortComplex C<VAR>inst✝ : HasZeroMorphisms D<VAR>S₁ S₂ : ShortComplex Cᵒᵖ<VAR>φ : S₁ ⟶ S₂<GOAL>φ.τ₃.unop ≫ S₁.g.unop = S₂.g.unop ≫ φ.τ₂.unop
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.61158, u_1} C<VAR>inst✝² : Category.{?u.61162, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁✝ S₂✝ S₃ : ShortComplex C<VAR>inst✝ : HasZeroMorphisms D<VAR>S₁ S₂ : ShortComplex Cᵒᵖ<VAR>φ : S₁ ⟶ S₂<GOAL>φ.τ₂.unop ≫ S₁.f.unop = S₂.f.unop ≫ φ.τ₁.unop
<VAR>n : ℕ<VAR>hzero : ¬n = 0<GOAL>map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧ (cyclotomic n ℤ).degree = (cyclotomic' n ℂ).degree ∧ (cyclotomic n ℤ).Monic
<VAR>n : ℕ<VAR>hzero : ¬n = 0<GOAL>map (Int.castRingHom ℂ) ⋯.choose = cyclotomic' n ℂ ∧ ⋯.choose.degree = (cyclotomic' n ℂ).degree ∧ ⋯.choose.Monic
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Star R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : StarAddMonoid A<VAR>inst✝² : Monoid R<VAR>inst✝¹ : DistribMulAction R A<VAR>inst✝ : StarModule R A<VAR>r : R<VAR>x : A<VAR>h : x ∈ skewAdjoint A<GOAL>r • x ∈ skewAdjoint A
<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>n : ℕ<VAR>f : ℕ → ℕ → M<GOAL>∏ m ∈ range n, ∏ k ∈ range (m + 1), f k (m - k) = ∏ m ∈ range n, ∏ k ∈ range (n - m), f m k
<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>n : ℕ<VAR>f : ℕ → ℕ → M<GOAL>∏ x ∈ (range n).sigma fun m => range (m + 1), f x.snd (x.fst - x.snd) = ∏ x ∈ (range n).sigma fun m => range (n - m), f x.fst x.snd
<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>n : ℕ<VAR>f : ℕ → ℕ → M<GOAL>∀ (a b : ℕ), a < n → b ≤ a → b < n
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹³ : SeminormedCommRing S<VAR>inst✝¹² : SeminormedRing R<VAR>inst✝¹¹ : SeminormedAddCommGroup M<VAR>inst✝¹⁰ : Algebra S R<VAR>inst✝⁹ : Module S M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module Rᵐᵒᵖ M<VAR>inst✝⁶ : BoundedSMul S R<VAR>inst✝⁵ : BoundedSMul S M<VAR>inst✝⁴ : BoundedSMul R M<VAR>inst✝³ : BoundedSMul Rᵐᵒᵖ M<VAR>inst✝² : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹ : IsScalarTower S R M<VAR>inst✝ : IsScalarTower S Rᵐᵒᵖ M<VAR>r : R<GOAL>‖inl r‖ = ‖r‖
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>G : C ⥤ D<VAR>F : D ⥤ C<VAR>A B : C<VAR>X Y : D<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>u : A ⟶ F.obj X<VAR>v : B ⟶ F.obj Y<VAR>sq : CommSq u i (F.map p) v<VAR>adj : G ⊣ F<GOAL>(adj.homEquiv A X).symm u ≫ p = G.map i ≫ (adj.homEquiv B Y).symm v
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>G : C ⥤ D<VAR>F : D ⥤ C<VAR>A B : C<VAR>X Y : D<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>u : A ⟶ F.obj X<VAR>v : B ⟶ F.obj Y<VAR>sq : CommSq u i (F.map p) v<VAR>adj : G ⊣ F<GOAL>G.map u ≫ adj.counit.app X ≫ p = G.map (u ≫ F.map p) ≫ adj.counit.app Y
<VAR>n : ℕ<VAR>s : ℝ<GOAL>0 ≤ term n s
<VAR>n : ℕ<VAR>s : ℝ<GOAL>0 ≤ ∫ (x : ℝ) in Ioc (↑n) (↑n + 1), (x - ↑n) / x ^ (s + 1) ∂volume
<VAR>n : ℕ<VAR>s x : ℝ<VAR>hx : x ∈ Ioc (↑n) (↑n + 1)<GOAL>0 ≤ (x - ↑n) / x ^ (s + 1)
<VAR>n : ℕ<VAR>s x : ℝ<VAR>hx : x ∈ Ioc (↑n) (↑n + 1)<GOAL>0 ≤ x - ↑n
<VAR>n : ℕ<VAR>s x : ℝ<VAR>hx : x ∈ Ioc (↑n) (↑n + 1)<GOAL>0 ≤ x
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : IsPiSystem C<VAR>hD : IsPiSystem D<VAR>s₁ : Set α<VAR>hs₁ : s₁ ∈ C<VAR>t₁ : Set β<VAR>ht₁ : t₁ ∈ D<VAR>s₂ : Set α<VAR>hs₂ : s₂ ∈ C<VAR>t₂ : Set β<VAR>ht₂ : t₂ ∈ D<VAR>hst : ((fun x x_1 => x ×ˢ x_1) s₁ t₁ ∩ (fun x x_1 => x ×ˢ x_1) s₂ t₂).Nonempty<GOAL>(fun x x_1 => x ×ˢ x_1) s₁ t₁ ∩ (fun x x_1 => x ×ˢ x_1) s₂ t₂ ∈ image2 (fun x x_1 => x ×ˢ x_1) C D
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : IsPiSystem C<VAR>hD : IsPiSystem D<VAR>s₁ : Set α<VAR>hs₁ : s₁ ∈ C<VAR>t₁ : Set β<VAR>ht₁ : t₁ ∈ D<VAR>s₂ : Set α<VAR>hs₂ : s₂ ∈ C<VAR>t₂ : Set β<VAR>ht₂ : t₂ ∈ D<VAR>hst : ((s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)).Nonempty<GOAL>(s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) ∈ image2 (fun x x_1 => x ×ˢ x_1) C D
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : IsPiSystem C<VAR>hD : IsPiSystem D<VAR>s₁ : Set α<VAR>hs₁ : s₁ ∈ C<VAR>t₁ : Set β<VAR>ht₁ : t₁ ∈ D<VAR>s₂ : Set α<VAR>hs₂ : s₂ ∈ C<VAR>t₂ : Set β<VAR>ht₂ : t₂ ∈ D<VAR>hst : (s₁ ∩ s₂).Nonempty ∧ (t₁ ∩ t₂).Nonempty<GOAL>(s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) ∈ image2 (fun x x_1 => x ×ˢ x_1) C D
<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>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<GOAL>map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite α<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<GOAL>∃ x₀, ∀ (x : α), f x ≤ f x₀
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite α<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>val✝ : Fintype α<GOAL>∃ x₀, ∀ (x : α), f x ≤ f x₀
<VAR>α : Type u_1<GOAL>↑(-0) = -↑0
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x y z : X<VAR>r s : ℝ<GOAL>closedBall x r = closedBall y r ∨ Disjoint (closedBall x r) (closedBall y r)
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x y z : X<VAR>r s : ℝ<VAR>h : (closedBall x r ∩ closedBall y r).Nonempty<GOAL>closedBall x r = closedBall y r
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x y z : X<VAR>r s : ℝ<VAR>h : (closedBall x r ∩ closedBall y r).Nonempty<VAR>h₁ : closedBall x r = closedBall h.some r<GOAL>closedBall x r = closedBall y r
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x y z : X<VAR>r s : ℝ<VAR>h : (closedBall x r ∩ closedBall y r).Nonempty<VAR>h₁ : closedBall x r = closedBall h.some r<VAR>h₂ : closedBall y r = closedBall h.some r<GOAL>closedBall x r = closedBall y r
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>U : X.Opens<GOAL>(f ≫ inv f) ⁻¹ᵁ U = U
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>U : X.Opens<GOAL>𝟙 X ⁻¹ᵁ U = U
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>U : X.Opens<GOAL>Hom.app (inv f) U = X.presheaf.map (eqToHom ⋯).op ≫ inv (Hom.app f (inv f ⁻¹ᵁ U))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>P : Type u → Prop<VAR>of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β<VAR>h_empty : P PEmpty.{u + 1}<VAR>h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)<VAR>α : Type u<VAR>inst✝ : Finite α<GOAL>P α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>P : Type u → Prop<VAR>of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β<VAR>h_empty : P PEmpty.{u + 1}<VAR>h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)<VAR>α : Type u<VAR>inst✝ : Finite α<VAR>val✝ : Fintype α<GOAL>P α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>P : Type u → Prop<VAR>of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β<VAR>h_empty : P PEmpty.{u + 1}<VAR>h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)<VAR>α : Type u<VAR>inst✝ : Finite α<VAR>val✝ : Fintype α<GOAL>∀ (α β : Type u) [inst : Fintype β], α ≃ β → P α → P β
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>P : Type u → Prop<VAR>of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β<VAR>h_empty : P PEmpty.{u + 1}<VAR>h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)<VAR>α : Type u<VAR>inst✝ : Finite α<VAR>val✝ : Fintype α<GOAL>P PEmpty.{u + 1}
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>P : Type u → Prop<VAR>of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β<VAR>h_empty : P PEmpty.{u + 1}<VAR>h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)<VAR>α : Type u<VAR>inst✝ : Finite α<VAR>val✝ : Fintype α<GOAL>∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
<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>_mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_10<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>h : iIndepFun m f μ<GOAL>μ univ = 1
<VAR>E : Type u_1<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : T2Space E<VAR>inst✝² : ContinuousSMul ℝ E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>inst✝ : Nontrivial E<VAR>r : ℝ<VAR>F : Type u_1 := E<GOAL>μ {x | g x ≤ r} = μ {x | g x < r}
<VAR>E : Type u_1<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : T2Space E<VAR>inst✝² : ContinuousSMul ℝ E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>inst✝ : Nontrivial E<VAR>r : ℝ<VAR>F : Type u_1 := E<VAR>this : NormedAddCommGroup F := NormedAddCommGroup.mk ⋯<GOAL>μ {x | g x ≤ r} = μ {x | g x < r}
<VAR>E : Type u_1<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : T2Space E<VAR>inst✝² : ContinuousSMul ℝ E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>inst✝ : Nontrivial E<VAR>r : ℝ<VAR>F : Type u_1 := E<VAR>this✝³ : NormedAddCommGroup F := NormedAddCommGroup.mk ⋯<VAR>this✝² : NormedSpace ℝ F := NormedSpace.mk ⋯<VAR>this✝¹ : TopologicalSpace F := UniformSpace.toTopologicalSpace<VAR>this✝ : MeasurableSpace F := borel F<VAR>this : BorelSpace F<VAR>φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv<VAR>ν : Measure F := map (⇑φ) μ<GOAL>μ {x | g x ≤ r} = μ {x | g x < r}
<VAR>E : Type u_1<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : T2Space E<VAR>inst✝² : ContinuousSMul ℝ E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>inst✝ : Nontrivial E<VAR>r : ℝ<VAR>F : Type u_1 := E<VAR>this✝⁴ : NormedAddCommGroup F := NormedAddCommGroup.mk ⋯<VAR>this✝³ : NormedSpace ℝ F := NormedSpace.mk ⋯<VAR>this✝² : TopologicalSpace F := UniformSpace.toTopologicalSpace<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv<VAR>ν : Measure F := map (⇑φ) μ<VAR>this : ν.IsAddHaarMeasure<GOAL>μ {x | g x ≤ r} = μ {x | g x < r}
<VAR>E : Type u_1<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : T2Space E<VAR>inst✝² : ContinuousSMul ℝ E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>inst✝ : Nontrivial E<VAR>r : ℝ<VAR>F : Type u_1 := E<VAR>this✝⁴ : NormedAddCommGroup F := NormedAddCommGroup.mk ⋯<VAR>this✝³ : NormedSpace ℝ F := NormedSpace.mk ⋯<VAR>this✝² : TopologicalSpace F := UniformSpace.toTopologicalSpace<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv<VAR>ν : Measure F := map (⇑φ) μ<VAR>this : ν.IsAddHaarMeasure<GOAL>μ {x | g x ≤ r} = ν (Metric.closedBall 0 r)
<VAR>E : Type u_1<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : T2Space E<VAR>inst✝² : ContinuousSMul ℝ E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>inst✝ : Nontrivial E<VAR>r : ℝ<VAR>F : Type u_1 := E<VAR>this✝⁴ : NormedAddCommGroup F := NormedAddCommGroup.mk ⋯<VAR>this✝³ : NormedSpace ℝ F := NormedSpace.mk ⋯<VAR>this✝² : TopologicalSpace F := UniformSpace.toTopologicalSpace<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv<VAR>ν : Measure F := map (⇑φ) μ<VAR>this : ν.IsAddHaarMeasure<GOAL>μ {x | g x < r} = ν (Metric.ball 0 r)
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>α : Type u_3<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Preorder α<VAR>f : ι → α<VAR>i j : ι<VAR>h₁ : i ≤ j<VAR>h₂ : f j < f i<GOAL>(fun x x_1 x_2 => x_1 < x_2) i (toLex (f ∘ ⇑(Equiv.swap i j)) i) (toLex f i)
<VAR>k✝ p✝ n✝ : ℕ<VAR>h✝ : 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0<VAR>ih1✝ : go (k✝ + 1 + 1) p✝ (n✝ / p✝) = go (k✝ + 1) p✝ (n✝ / p✝) + 1<GOAL>go (k✝ + 1) p✝ n✝ = go k✝ p✝ n✝ + 1
<VAR>k✝ p✝ n✝ : ℕ<VAR>h✝ : ¬(1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0)<GOAL>go (k✝ + 1) p✝ n✝ = go k✝ p✝ n✝ + 1
<VAR>y : ℝ<GOAL>WithBot.some ∘ WithTop.some ⁻¹' Iic ↑↑y = Iic y
<VAR>y : ℝ<GOAL>WithTop.some ⁻¹' (WithBot.some ⁻¹' Iic ↑↑y) = Iic y
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Fintype α<VAR>f : Perm α<GOAL>|↑(sign f)| = 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>f g : ℕ → α<VAR>inst✝¹ : T3Space α<VAR>inst✝ : TopologicalSemiring α<VAR>h : Summable fun x => f x.1 * g x.2<GOAL>Summable fun n => ∑ k ∈ range (n + 1), f k * g (n - k)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>f g : ℕ → α<VAR>inst✝¹ : T3Space α<VAR>inst✝ : TopologicalSemiring α<VAR>h : Summable fun x => f x.1 * g x.2<GOAL>Summable fun n => ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a b : R<GOAL>(if a0 : a = 0 then b else let_fun x := ⋯; gcd (b % a) a) = gcd (b % a) a
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>x : α<VAR>h : p x = true<GOAL>rtakeWhile p (l ++ [x]) = rtakeWhile p l ++ [x]