ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜₁ : Type u_1<VAR>inst✝²² : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝²¹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝²⁰ : NormedAddCommGroup F₁<VAR>inst✝¹⁹ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁸ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁷ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹⁵ : NormedAddCommGroup F₂<VAR>inst✝¹⁴ : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹³ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹² : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝¹⁰ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁹ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁸ : FiberBundle F₁ E₁<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁶ : FiberBundle F₂ E₂<VAR>inst✝⁵ : VectorBundle 𝕜₁ F₁ E₁<VAR>inst✝⁴ : VectorBundle 𝕜₂ F₂ E₂<VAR>inst✝³ : MemTrivializationAtlas e₁<VAR>inst✝² : MemTrivializationAtlas e₁'<VAR>inst✝¹ : MemTrivializationAtlas e₂<VAR>inst✝ : MemTrivializationAtlas e₂'<VAR>h₁ : Continuous ⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂))<VAR>h₂ : Continuous ⇑(compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ).flip<VAR>h₃ : ContinuousOn (fun b => ↑(Trivialization.coordChangeL 𝕜₁ e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)<VAR>h₄ : ContinuousOn (fun b => ↑(Trivialization.coordChangeL 𝕜₂ e₂ e₂' b)) (e₂.baseSet ∩ e₂'.baseSet)<GOAL>ContinuousOn (continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
<VAR>𝕜₁ : Type u_1<VAR>inst✝²² : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝²¹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝²⁰ : NormedAddCommGroup F₁<VAR>inst✝¹⁹ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁸ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁷ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹⁵ : NormedAddCommGroup F₂<VAR>inst✝¹⁴ : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹³ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹² : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝¹⁰ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁹ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁸ : FiberBundle F₁ E₁<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁶ : FiberBundle F₂ E₂<VAR>inst✝⁵ : VectorBundle 𝕜₁ F₁ E₁<VAR>inst✝⁴ : VectorBundle 𝕜₂ F₂ E₂<VAR>inst✝³ : MemTrivializationAtlas e₁<VAR>inst✝² : MemTrivializationAtlas e₁'<VAR>inst✝¹ : MemTrivializationAtlas e₂<VAR>inst✝ : MemTrivializationAtlas e₂'<VAR>h₁ : Continuous ⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂))<VAR>h₂ : Continuous ⇑(compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ).flip<VAR>h₃ : ContinuousOn (fun b => ↑(Trivialization.coordChangeL 𝕜₁ e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)<VAR>h₄ : ContinuousOn (fun b => ↑(Trivialization.coordChangeL 𝕜₂ e₂ e₂' b)) (e₂.baseSet ∩ e₂'.baseSet)<GOAL>e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
<VAR>𝕜₁ : Type u_1<VAR>inst✝²² : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝²¹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝²⁰ : NormedAddCommGroup F₁<VAR>inst✝¹⁹ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁸ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁷ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹⁵ : NormedAddCommGroup F₂<VAR>inst✝¹⁴ : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹³ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹² : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝¹⁰ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁹ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁸ : FiberBundle F₁ E₁<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁶ : FiberBundle F₂ E₂<VAR>inst✝⁵ : VectorBundle 𝕜₁ F₁ E₁<VAR>inst✝⁴ : VectorBundle 𝕜₂ F₂ E₂<VAR>inst✝³ : MemTrivializationAtlas e₁<VAR>inst✝² : MemTrivializationAtlas e₁'<VAR>inst✝¹ : MemTrivializationAtlas e₂<VAR>inst✝ : MemTrivializationAtlas e₂'<VAR>h₁ : Continuous ⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂))<VAR>h₂ : Continuous ⇑(compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ).flip<VAR>h₃ : ContinuousOn (fun b => ↑(Trivialization.coordChangeL 𝕜₁ e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)<VAR>h₄ : ContinuousOn (fun b => ↑(Trivialization.coordChangeL 𝕜₂ e₂ e₂' b)) (e₂.baseSet ∩ e₂'.baseSet)<GOAL>e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet
<VAR>𝕜₁ : Type u_1<VAR>inst✝²² : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝²¹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝²⁰ : NormedAddCommGroup F₁<VAR>inst✝¹⁹ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁸ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁷ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹⁵ : NormedAddCommGroup F₂<VAR>inst✝¹⁴ : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹³ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹² : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝¹⁰ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁹ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁸ : FiberBundle F₁ E₁<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁶ : FiberBundle F₂ E₂<VAR>inst✝⁵ : VectorBundle 𝕜₁ F₁ E₁<VAR>inst✝⁴ : VectorBundle 𝕜₂ F₂ E₂<VAR>inst✝³ : MemTrivializationAtlas e₁<VAR>inst✝² : MemTrivializationAtlas e₁'<VAR>inst✝¹ : MemTrivializationAtlas e₂<VAR>inst✝ : MemTrivializationAtlas e₂'<VAR>h₁ : Continuous ⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂))<VAR>h₂ : Continuous ⇑(compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ).flip<VAR>h₃ : ContinuousOn (fun b => ↑(Trivialization.coordChangeL 𝕜₁ e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)<VAR>h₄ : ContinuousOn (fun b => ↑(Trivialization.coordChangeL 𝕜₂ e₂ e₂' b)) (e₂.baseSet ∩ e₂'.baseSet)<GOAL>EqOn (continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂') (fun x => ((⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)) ∘ fun b => ↑(Trivialization.coordChangeL 𝕜₂ e₂ e₂' b)) x).comp ((⇑(compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ).flip ∘ fun b => ↑(Trivialization.coordChangeL 𝕜₁ e₁' e₁ b)) x)) (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y<GOAL>abscissaOfAbsConv f ≤ ↑x
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y<VAR>y : EReal<VAR>hy : y ∈ lowerBounds (Real.toEReal '' {x | LSeriesSummable f ↑x})<GOAL>y ≤ ↑x
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y<VAR>y : EReal<VAR>hy : ∀ (a : ℝ), LSeriesSummable f ↑a → y ≤ ↑a<GOAL>y ≤ ↑x
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y<VAR>y : EReal<VAR>hy : ∀ (a : ℝ), LSeriesSummable f ↑a → y ≤ ↑a<VAR>H : ∀ (a : EReal), ↑x < a → y ≤ a<GOAL>y ≤ ↑x
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>(Iic b).card = ↑b + 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>s : Finset α<GOAL>∑ x ∈ s, {x} = s.val
<VAR>q : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (x * ↑n) ↔ n ≠ 0 ∧ Irrational x
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set V<GOAL>G'.deleteVerts (s ∩ G'.verts) = G'.deleteVerts s
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some '' Ico a b = Ico ↑a ↑b
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Field A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>x✝ : minpoly A x ∣ p<VAR>q : A[X]<VAR>hq : p = minpoly A x * q<GOAL>(Polynomial.aeval x) p = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l✝ : List α<VAR>o : Option α<VAR>a m : α<VAR>l : List α<GOAL>∀ (a m : α), m ∈ foldl (argAux r) (some a) [] → m ∈ [a]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l✝ : List α<VAR>o : Option α<VAR>a✝ m✝ : α<VAR>l tl : List α<VAR>hd : α<VAR>ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl<VAR>a m : α<GOAL>m ∈ foldl (argAux r) (some a) (tl ++ [hd]) → m ∈ a :: (tl ++ [hd])
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>inst✝ : DecidableRel r<VAR>l✝ : List α<VAR>o : Option α<VAR>a✝ m✝ : α<VAR>l tl : List α<VAR>hd : α<VAR>ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl<VAR>a m : α<GOAL>m ∈ Option.rec (some hd) (fun val => if r hd val then some hd else some val) (foldl (argAux r) (some a) tl) → m ∈ a :: (tl ++ [hd])
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x₁ x₂ : M<VAR>y : ↥S<GOAL>f.mk' x₂ y * f.toMap x₁ = f.mk' (x₁ * x₂) y
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderTop α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁ ∪ s₂).inf = s₁.inf ⊓ s₂.inf
<VAR>α : Type u_1<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderTop α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>h : LineDifferentiableAt 𝕜 f x (c • v)<GOAL>LineDifferentiableAt 𝕜 f x v
<VAR>n : ℕ<GOAL>antidiagonal n = image (fun i => (n - i, i)) (range (n + 1))
<VAR>C : Type u<VAR>X Y : F C<VAR>f : X ⟶ Y<GOAL>∀ (n : NormalMonoidalObject C), inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
<VAR>C : Type u<VAR>X Y X✝ : F C<GOAL>∀ (n : NormalMonoidalObject C), inclusionObj n ◁ 𝟙 X✝ ≫ (normalizeIsoApp' C X✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)
<VAR>C : Type u<VAR>X Y X✝ Y✝ Z✝ : F C<GOAL>∀ (n : NormalMonoidalObject C), inclusionObj n ◁ (α_ X✝ Y✝ Z✝).hom ≫ (normalizeIsoApp' C (X✝ ⊗ Y✝ ⊗ Z✝) n).hom = (normalizeIsoApp' C ((X✝ ⊗ Y✝) ⊗ Z✝) n).hom ≫ inclusion.map (eqToHom ⋯)
<VAR>C : Type u<VAR>X Y X✝ Y✝ Z✝ : F C<GOAL>∀ (n : NormalMonoidalObject C), inclusionObj n ◁ (α_ X✝ Y✝ Z✝).inv ≫ (normalizeIsoApp' C ((X✝ ⊗ Y✝) ⊗ Z✝) n).hom = (normalizeIsoApp' C (X✝ ⊗ Y✝ ⊗ Z✝) n).hom ≫ inclusion.map (eqToHom ⋯)
<VAR>C : Type u<VAR>X Y X✝ : F C<GOAL>∀ (n : NormalMonoidalObject C), inclusionObj n ◁ (λ_ X✝).hom ≫ (normalizeIsoApp' C X✝ n).hom = (normalizeIsoApp' C (𝟙_ (F C) ⊗ X✝) n).hom ≫ inclusion.map (eqToHom ⋯)
<VAR>C : Type u<VAR>X Y X✝ : F C<GOAL>∀ (n : NormalMonoidalObject C), inclusionObj n ◁ (λ_ X✝).inv ≫ (normalizeIsoApp' C (𝟙_ (F C) ⊗ X✝) n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)
<VAR>C : Type u<VAR>X Y X✝ : F C<GOAL>∀ (n : NormalMonoidalObject C), inclusionObj n ◁ (ρ_ X✝).hom ≫ (normalizeIsoApp' C X✝ n).hom = (normalizeIsoApp' C (X✝ ⊗ 𝟙_ (F C)) n).hom ≫ inclusion.map (eqToHom ⋯)
<VAR>C : Type u<VAR>X Y X✝ : F C<GOAL>∀ (n : NormalMonoidalObject C), inclusionObj n ◁ (ρ_ X✝).inv ≫ (normalizeIsoApp' C (X✝ ⊗ 𝟙_ (F C)) n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)
<VAR>C : Type u<VAR>X Y X✝ Y✝ Z✝ : F C<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<VAR>a✝¹ : ∀ (n : NormalMonoidalObject C), inclusionObj n ◁ f✝ ≫ (normalizeIsoApp' C Y✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)<VAR>a✝ : ∀ (n : NormalMonoidalObject C), inclusionObj n ◁ g✝ ≫ (normalizeIsoApp' C Z✝ n).hom = (normalizeIsoApp' C Y✝ n).hom ≫ inclusion.map (eqToHom ⋯)<GOAL>∀ (n : NormalMonoidalObject C), inclusionObj n ◁ (f✝ ≫ g✝) ≫ (normalizeIsoApp' C Z✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)
<VAR>C : Type u<VAR>X Y X✝ Y✝ Z✝ : F C<VAR>f✝ : Y✝ ⟶ Z✝<VAR>a✝ : ∀ (n : NormalMonoidalObject C), inclusionObj n ◁ f✝ ≫ (normalizeIsoApp' C Z✝ n).hom = (normalizeIsoApp' C Y✝ n).hom ≫ inclusion.map (eqToHom ⋯)<GOAL>∀ (n : NormalMonoidalObject C), inclusionObj n ◁ X✝ ◁ f✝ ≫ (normalizeIsoApp' C (X✝ ⊗ Z✝) n).hom = (normalizeIsoApp' C (X✝ ⊗ Y✝) n).hom ≫ inclusion.map (eqToHom ⋯)
<VAR>C : Type u<VAR>X Y X✝ Y✝ : F C<VAR>f✝ : X✝ ⟶ Y✝<VAR>Z✝ : F C<VAR>a✝ : ∀ (n : NormalMonoidalObject C), inclusionObj n ◁ f✝ ≫ (normalizeIsoApp' C Y✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)<GOAL>∀ (n : NormalMonoidalObject C), inclusionObj n ◁ f✝ ▷ Z✝ ≫ (normalizeIsoApp' C (Y✝ ⊗ Z✝) n).hom = (normalizeIsoApp' C (X✝ ⊗ Z✝) n).hom ≫ inclusion.map (eqToHom ⋯)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>h : y ∈ sphere x ε<VAR>hε : ε ≠ 0<GOAL>x ∉ sphere x ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : LocallyCompactSpace X<VAR>x : X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>hx : x ∈ U<GOAL>∃ K, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : LocallyCompactSpace X<VAR>x : X<VAR>U : Set X<VAR>hU : IsOpen U<VAR>hx : x ∈ U<VAR>K : Set X<VAR>h1K : K ∈ 𝓝 x<VAR>h2K : K ⊆ U<VAR>h3K : IsCompact K<GOAL>∃ K, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>f : γ → β<GOAL>uniformSpace α γ 𝔖 = UniformSpace.comap (fun x => f ∘ x) (uniformSpace α β 𝔖)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>f : γ → β<GOAL>⨅ s ∈ 𝔖, UniformSpace.comap ((fun x => f ∘ x) ∘ ⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) β) = ⨅ i ∈ 𝔖, UniformSpace.comap ((⇑UniformFun.ofFun ∘ i.restrict ∘ ⇑(toFun 𝔖)) ∘ fun x => f ∘ x) (UniformFun.uniformSpace (↑i) β)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a✝ b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>a : ℕ<VAR>h_ind : multiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = multiplicity (↑p) (x - y) + ↑a<GOAL>multiplicity (↑p) (x ^ p ^ (a + 1) - y ^ p ^ (a + 1)) = multiplicity (↑p) (x - y) + ↑(a + 1)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a✝ b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>a : ℕ<VAR>h_ind : multiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = multiplicity (↑p) (x - y) + ↑a<GOAL>multiplicity (↑p) ((x ^ p ^ a) ^ p - (y ^ p ^ a) ^ p) = multiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) + 1
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a✝ b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>a : ℕ<VAR>h_ind : multiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = multiplicity (↑p) (x - y) + ↑a<GOAL>↑p ∣ x ^ p ^ a - y ^ p ^ a
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a✝ b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<VAR>a : ℕ<VAR>h_ind : multiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = multiplicity (↑p) (x - y) + ↑a<GOAL>¬↑p ∣ x ^ p ^ a
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>fst R M M₂ ⊓ snd R M M₂ = ⊥
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>fst R M M₂ ⊓ snd R M M₂ ≤ ⊥
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>x : M<VAR>y : M₂<GOAL>(x, y) ∈ fst R M M₂ ⊓ snd R M M₂ → (x, y) ∈ ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>f : α → β<VAR>g : β → α<VAR>h : LeftInverse g f<VAR>s : Set α<GOAL>f ⁻¹' (g ⁻¹' s) = s
<VAR>α : Type u_1<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>max a⁻¹ 1 = a⁻¹ * max a 1
<VAR>A : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>inst✝⁵ : Category.{v₃, u₃} T<VAR>A' : Type u_1<VAR>B' : Type u_2<VAR>T' : Type u_3<VAR>inst✝⁴ : Category.{?u.129256, u_1} A'<VAR>inst✝³ : Category.{?u.129260, u_2} B'<VAR>inst✝² : Category.{?u.129264, u_3} T'<VAR>L✝ : A ⥤ T<VAR>R✝ : B ⥤ T<VAR>C : Type u₄<VAR>inst✝¹ : Category.{v₄, u₄} C<VAR>D : Type u₅<VAR>inst✝ : Category.{v₅, u₅} D<VAR>F : C ⥤ A<VAR>L : A ⥤ T<VAR>R : B ⥤ T<VAR>X✝ Y✝ : Comma (F ⋙ L) R<VAR>f : X✝ ⟶ Y✝<GOAL>L.map (F.map f.left) ≫ ((fun X => { left := F.obj X.left, right := X.right, hom := X.hom }) Y✝).hom = ((fun X => { left := F.obj X.left, right := X.right, hom := X.hom }) X✝).hom ≫ R.map f.right
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>p : α → Prop<VAR>inst✝ : CommMonoid N<VAR>v : α →₀ M<VAR>h : α → M → N<VAR>hp : ∀ x ∈ v.support, p x<GOAL>((subtypeDomain p v).prod fun a b => h (↑a) b) = v.prod h
<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp₁ : p ≤ 1<GOAL>ConcaveOn ℝ≥0 univ fun x => x ^ p
<VAR>hp₀ : 0 ≤ 0<VAR>hp₁ : 0 ≤ 1<GOAL>ConcaveOn ℝ≥0 univ fun x => x ^ 0
<VAR>p : ℝ<VAR>hp₀✝ : 0 ≤ p<VAR>hp₁ : p ≤ 1<VAR>hp₀ : 0 < p<GOAL>ConcaveOn ℝ≥0 univ fun x => x ^ p
<VAR>hp₀✝ : 0 ≤ 1<VAR>hp₁ : 1 ≤ 1<VAR>hp₀ : 0 < 1<GOAL>ConcaveOn ℝ≥0 univ fun x => x ^ 1
<VAR>p : ℝ<VAR>hp₀✝ : 0 ≤ p<VAR>hp₁✝ : p ≤ 1<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<GOAL>ConcaveOn ℝ≥0 univ fun x => x ^ p
<VAR>R L : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : NoZeroSMulDivisors R L<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>x : L<VAR>p : { x_1 // x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0 } := Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯<GOAL>x ∈ (↑p).aroots L
<VAR>R L : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : NoZeroSMulDivisors R L<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>x : L<VAR>p : { x_1 // x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0 } := Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯<VAR>h : Polynomial.map (algebraMap R L) ↑p ≠ 0<GOAL>x ∈ (↑p).aroots L
<VAR>R L : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : NoZeroSMulDivisors R L<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>x y : L<VAR>h : (fun x => let p := Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯; ⟨↑p, ⟨x, ⋯⟩⟩) x = (fun x => let p := Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯; ⟨↑p, ⟨x, ⋯⟩⟩) y<GOAL>x = y
<VAR>R L : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : NoZeroSMulDivisors R L<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>x y : L<VAR>h : ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯) = ↑(Classical.indefiniteDescription (fun x => ¬x = 0 ∧ (Polynomial.aeval y) x = 0) ⋯) ∧ HEq ⟨x, ⋯⟩ ⟨y, ⋯⟩<GOAL>x = y
<VAR>R L : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing L<VAR>inst✝³ : IsDomain L<VAR>inst✝² : Algebra R L<VAR>inst✝¹ : NoZeroSMulDivisors R L<VAR>inst✝ : Algebra.IsAlgebraic R L<VAR>x y : L<VAR>h : ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ (Polynomial.aeval x) x_1 = 0) ⋯) = ↑(Classical.indefiniteDescription (fun x => ¬x = 0 ∧ (Polynomial.aeval y) x = 0) ⋯) ∧ HEq ⟨x, ⋯⟩ ⟨y, ⋯⟩<GOAL>∀ (x_1 : L), x_1 ∈ (↑(Classical.indefiniteDescription (fun x_2 => ¬x_2 = 0 ∧ (Polynomial.aeval x) x_2 = 0) ⋯)).aroots L ↔ x_1 ∈ (↑(Classical.indefiniteDescription (fun x => ¬x = 0 ∧ (Polynomial.aeval y) x = 0) ⋯)).aroots L
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : PrimeSpectrum R<GOAL>p ∈ support R M ↔ ∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : PrimeSpectrum R<GOAL>(¬∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0) ↔ ∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : PrimeSpectrum R<GOAL>(∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>S : Set (HeightOneSpectrum R) := {v | (fun v => ↑a v) v ∉ adicCompletionIntegers K v}<GOAL>∃ b c, a * ↑↑b = ↑c
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>S : Set (HeightOneSpectrum R) := {v | (fun v => ↑a v) v ∉ adicCompletionIntegers K v}<VAR>b : (v : HeightOneSpectrum R) → adicCompletion K v → R<VAR>hb : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), b v a ∈ R⁰<VAR>h : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), a * ↑(b v a) ∈ adicCompletionIntegers K v<GOAL>∃ b c, a * ↑↑b = ↑c
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>S : Set (HeightOneSpectrum R) := {v | (fun v => ↑a v) v ∉ adicCompletionIntegers K v}<VAR>b : (v : HeightOneSpectrum R) → adicCompletion K v → R<VAR>hb : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), b v a ∈ R⁰<VAR>h : ∀ (v : HeightOneSpectrum R) (a : adicCompletion K v), a * ↑(b v a) ∈ adicCompletionIntegers K v<VAR>p : R := ∏ᶠ (v : HeightOneSpectrum R) (_ : v ∈ S), b v ((fun v => ↑a v) v)<VAR>hp : p ∈ R⁰<GOAL>∃ b c, a * ↑↑b = ↑c