ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>c : Chain (Part α)<VAR>a b : α<VAR>i : ℕ<VAR>ha : c i = some a<VAR>j : ℕ<VAR>hb : some b = c j<GOAL>a = b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>c : Chain (Part α)<VAR>a b : α<VAR>i : ℕ<VAR>ha : c i = some a<VAR>j : ℕ<VAR>hb : c j = some b<GOAL>a = b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>c : Chain (Part α)<VAR>a b : α<VAR>i : ℕ<VAR>ha : a ∈ c i<VAR>j : ℕ<VAR>hb : b ∈ c j<GOAL>a = b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>c : Chain (Part α)<VAR>a b : α<VAR>i : ℕ<VAR>ha : a ∈ c i<VAR>j : ℕ<VAR>hb : b ∈ c j<VAR>hij : i ≤ j<GOAL>a = b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>c : Chain (Part α)<VAR>a b : α<VAR>i : ℕ<VAR>ha : a ∈ c i<VAR>j : ℕ<VAR>hb : b ∈ c j<VAR>hji : j ≤ i<GOAL>a = b
<VAR>ι : Type u<VAR>X : Type v<VAR>Y : Type w<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ParacompactSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>u : ι → Set X<VAR>uo : ∀ (i : ι), IsOpen (u i)<VAR>us : s ⊆ ⋃ i, u i<VAR>uc : ⋃ i, Option.elim' sᶜ u i = univ<GOAL>∃ v, (∀ (i : ι), IsOpen (v i)) ∧ s ⊆ ⋃ i, v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
<VAR>ι : Type u<VAR>X : Type v<VAR>Y : Type w<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ParacompactSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>u : ι → Set X<VAR>uo : ∀ (i : ι), IsOpen (u i)<VAR>us : s ⊆ ⋃ i, u i<VAR>uc : ⋃ i, Option.elim' sᶜ u i = univ<VAR>v : Option ι → Set X<VAR>vo : ∀ (a : Option ι), IsOpen (v a)<VAR>vc : ⋃ i, v i = univ<VAR>vf : LocallyFinite v<VAR>vu : ∀ (a : Option ι), v a ⊆ Option.elim' sᶜ u a<GOAL>∃ v, (∀ (i : ι), IsOpen (v i)) ∧ s ⊆ ⋃ i, v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
<VAR>ι : Type u<VAR>X : Type v<VAR>Y : Type w<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : ParacompactSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>u : ι → Set X<VAR>uo : ∀ (i : ι), IsOpen (u i)<VAR>us : s ⊆ ⋃ i, u i<VAR>uc : ⋃ i, Option.elim' sᶜ u i = univ<VAR>v : Option ι → Set X<VAR>vo : ∀ (a : Option ι), IsOpen (v a)<VAR>vc : ⋃ i, v i = univ<VAR>vf : LocallyFinite v<VAR>vu : ∀ (a : Option ι), v a ⊆ Option.elim' sᶜ u a<GOAL>s ⊆ ⋃ i, (v ∘ some) i
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>z : S<GOAL>∃ r m, z = r • ↑((toInvSubmonoid M S) m)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>z : S<VAR>r : R<VAR>m : ↥M<VAR>e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r<GOAL>∃ r m, z = r • ↑((toInvSubmonoid M S) m)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>z : S<VAR>r : R<VAR>m : ↥M<VAR>e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r<GOAL>z = r • ↑((toInvSubmonoid M S) m)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>z : S<VAR>r : R<VAR>m : ↥M<VAR>e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r<GOAL>z = z * ((algebraMap R S) ↑(r, m).2 * ↑((toInvSubmonoid M S) m))
<VAR>n i : ℕ<VAR>h : i ≤ n<VAR>l₁ : ↑i + 1 ≠ 0<VAR>l₂ : ↑n - ↑i + 1 ≠ 0<GOAL>gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i = ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
<VAR>n i : ℕ<VAR>h : i ≤ n<VAR>l₁ : ↑i + 1 ≠ 0<VAR>l₂ : ↑n - ↑i + 1 ≠ 0<VAR>h₁ : ↑(i + 1).centralBinom = (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1)<GOAL>gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i = ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
<VAR>n i : ℕ<VAR>h : i ≤ n<VAR>l₁ : ↑i + 1 ≠ 0<VAR>l₂ : ↑n - ↑i + 1 ≠ 0<VAR>h₁ : ↑(i + 1).centralBinom = (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1)<VAR>h₂ : ↑(n - i + 1).centralBinom = (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom / (↑n - ↑i + 1)<GOAL>gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i = ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
<VAR>n i : ℕ<VAR>h : i ≤ n<VAR>l₁ : ↑i + 1 ≠ 0<VAR>l₂ : ↑n - ↑i + 1 ≠ 0<VAR>h₁ : ↑(i + 1).centralBinom = (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1)<VAR>h₂ : ↑(n - i + 1).centralBinom = (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom / (↑n - ↑i + 1)<VAR>h₃ : (↑i + 1) * ↑(i + 1).centralBinom = 2 * (2 * ↑i + 1) * ↑i.centralBinom<GOAL>gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i = ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
<VAR>n i : ℕ<VAR>h : i ≤ n<VAR>l₁ : ↑i + 1 ≠ 0<VAR>l₂ : ↑n - ↑i + 1 ≠ 0<VAR>h₁ : ↑(i + 1).centralBinom = (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1)<VAR>h₂ : ↑(n - i + 1).centralBinom = (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom / (↑n - ↑i + 1)<VAR>h₃ : (↑i + 1) * ↑(i + 1).centralBinom = 2 * (2 * ↑i + 1) * ↑i.centralBinom<VAR>h₄ : (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom = 2 * (2 * (↑n - ↑i) + 1) * ↑(n - i).centralBinom<GOAL>gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i = ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
<VAR>n i : ℕ<VAR>h : i ≤ n<VAR>l₁ : ↑i + 1 ≠ 0<VAR>l₂ : ↑n - ↑i + 1 ≠ 0<VAR>h₁ : ↑(i + 1).centralBinom = (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1)<VAR>h₂ : ↑(n - i + 1).centralBinom = (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom / (↑n - ↑i + 1)<VAR>h₃ : (↑i + 1) * ↑(i + 1).centralBinom = 2 * (2 * ↑i + 1) * ↑i.centralBinom<VAR>h₄ : (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom = 2 * (2 * (↑n - ↑i) + 1) * ↑(n - i).centralBinom<GOAL>↑(i + 1).centralBinom * ↑(n - i).centralBinom * (2 * (↑i + 1) - (↑n + 1)) / (2 * (↑n + 1) * (↑n + 1 + 1)) - ↑i.centralBinom * ↑(n + 1 - i).centralBinom * (2 * ↑i - (↑n + 1)) / (2 * (↑n + 1) * (↑n + 1 + 1)) = ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
<VAR>n i : ℕ<VAR>h : i ≤ n<VAR>l₁ : ↑i + 1 ≠ 0<VAR>l₂ : ↑n - ↑i + 1 ≠ 0<VAR>h₁ : ↑(i + 1).centralBinom = (↑i + 1) * ↑(i + 1).centralBinom / (↑i + 1)<VAR>h₂ : ↑(n - i + 1).centralBinom = (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom / (↑n - ↑i + 1)<VAR>h₃ : (↑i + 1) * ↑(i + 1).centralBinom = 2 * (2 * ↑i + 1) * ↑i.centralBinom<VAR>h₄ : (↑n - ↑i + 1) * ↑(n - i + 1).centralBinom = 2 * (2 * (↑n - ↑i) + 1) * ↑(n - i).centralBinom<GOAL>↑(i + 1).centralBinom * ↑(n - i).centralBinom * (2 * (↑i + 1) - (↑n + 1)) / (2 * (↑n + 1) * (↑n + 1 + 1)) - ↑i.centralBinom * ↑(n - i + 1).centralBinom * (2 * ↑i - (↑n + 1)) / (2 * (↑n + 1) * (↑n + 1 + 1)) = ↑i.centralBinom / (↑i + 1) * ↑(n - i).centralBinom / (↑n - ↑i + 1)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a : α<VAR>l : List α<VAR>f : α → β<VAR>g : α → List β<GOAL>map f l ++ l.bind g ~ l.bind fun x => f x :: g x
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C₁<VAR>inst✝⁵ : Category.{v₂, u₂} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>D₁ : Type u_1<VAR>D₂ : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} D₁<VAR>inst✝³ : Category.{u_3, u_2} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₁.IsLocalization W₁<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>F : D₁ ⥤ D₂<VAR>inst✝ : Φ.HasRightResolutions<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F<GOAL>Φ.IsRightDerivabilityStructure ↔ TwoSquare.GuitartExact e.hom
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C₁<VAR>inst✝⁵ : Category.{v₂, u₂} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>D₁ : Type u_1<VAR>D₂ : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} D₁<VAR>inst✝³ : Category.{u_3, u_2} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₁.IsLocalization W₁<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>F : D₁ ⥤ D₂<VAR>inst✝ : Φ.HasRightResolutions<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F<VAR>this : Φ.IsRightDerivabilityStructure ↔ TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom<GOAL>Φ.IsRightDerivabilityStructure ↔ TwoSquare.GuitartExact e.hom
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C₁<VAR>inst✝⁵ : Category.{v₂, u₂} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>D₁ : Type u_1<VAR>D₂ : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} D₁<VAR>inst✝³ : Category.{u_3, u_2} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₁.IsLocalization W₁<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>F : D₁ ⥤ D₂<VAR>inst✝ : Φ.HasRightResolutions<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F<VAR>this : Φ.IsRightDerivabilityStructure ↔ TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom<VAR>e' : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)<VAR>E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁<VAR>E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂<VAR>e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁<VAR>e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂<VAR>e'' : (Φ.functor ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F := Φ.functor.associator W₂.Q E₂.functor ≪≫ isoWhiskerLeft Φ.functor e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F<VAR>e''' : Φ.localizedFunctor W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F := liftNatIso W₁.Q W₁ ((Φ.functor ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F) (Φ.localizedFunctor W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''<GOAL>TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom ↔ TwoSquare.GuitartExact e.hom
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C₁<VAR>inst✝⁵ : Category.{v₂, u₂} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>D₁ : Type u_1<VAR>D₂ : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} D₁<VAR>inst✝³ : Category.{u_3, u_2} D₂<VAR>L₁ : C₁ ⥤ D₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₁.IsLocalization W₁<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>F : D₁ ⥤ D₂<VAR>inst✝ : Φ.HasRightResolutions<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F<VAR>this✝ : Φ.IsRightDerivabilityStructure ↔ TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom<VAR>e' : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)<VAR>E₁ : W₁.Localization ≌ D₁ := uniq W₁.Q L₁ W₁<VAR>E₂ : W₂.Localization ≌ D₂ := uniq W₂.Q L₂ W₂<VAR>e₁ : W₁.Q ⋙ E₁.functor ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁<VAR>e₂ : W₂.Q ⋙ E₂.functor ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂<VAR>e'' : (Φ.functor ⋙ W₂.Q) ⋙ E₂.functor ≅ (W₁.Q ⋙ E₁.functor) ⋙ F := Φ.functor.associator W₂.Q E₂.functor ≪≫ isoWhiskerLeft Φ.functor e₂ ≪≫ e ≪≫ isoWhiskerRight e₁.symm F<VAR>e''' : Φ.localizedFunctor W₁.Q W₂.Q ⋙ E₂.functor ≅ E₁.functor ⋙ F := liftNatIso W₁.Q W₁ ((Φ.functor ⋙ W₂.Q) ⋙ E₂.functor) ((W₁.Q ⋙ E₁.functor) ⋙ F) (Φ.localizedFunctor W₁.Q W₂.Q ⋙ E₂.functor) (E₁.functor ⋙ F) e''<VAR>this : TwoSquare.vComp' e'.hom e'''.hom e₁ e₂ = e.hom<GOAL>TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom ↔ TwoSquare.GuitartExact e.hom
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>s : Set α<VAR>f : α →ᵤ[singleton '' s] E<GOAL>LowerSemicontinuousAt (fun f => eVariationOn f s) f
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>s : Set α<VAR>f : α →ᵤ[singleton '' s] E<GOAL>∀ x ∈ s, Tendsto (fun i => id i x) (𝓝 f) (𝓝 (f x))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>x : M<GOAL>x ∈ torsionBySet R M s ↔ ∀ (a : ↑s), ↑a • x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>x : M<VAR>h : ∀ (a : ↑s), ↑a • x = 0<GOAL>∀ p ∈ torsionBy R M '' s, x ∈ p
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<GOAL>mk f = 0 ↔ f.LimZero
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>this : mk f = 0 ↔ (f - 0).LimZero<GOAL>mk f = 0 ↔ f.LimZero
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>ι : Type u_5<VAR>ι₁ : Type u_6<VAR>ι₂ : Type u_7<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₁<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R M₁<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι₁<VAR>inst✝³ : Fintype ι₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableEq ι₁<VAR>inst✝ : DecidableEq ι₂<VAR>b : Basis ι R M<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>ij : ι₂ × ι₁<GOAL>(b₁.linearMap b₂) ij = (toLin b₁ b₂) ((Matrix.stdBasis R ι₂ ι₁) ij)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : Balanced C<VAR>𝒢 : Set C<VAR>h𝒢 : IsSeparating 𝒢<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h<GOAL>IsIso f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : Balanced C<VAR>𝒢 : Set C<VAR>h𝒢 : IsSeparating 𝒢<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h<VAR>Z✝ : C<VAR>g h : Z✝ ⟶ X<VAR>hgh : g ≫ f = h ≫ f<VAR>G : C<VAR>hG : G ∈ 𝒢<VAR>i : G ⟶ Z✝<GOAL>i ≫ g = i ≫ h
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : Balanced C<VAR>𝒢 : Set C<VAR>h𝒢 : IsSeparating 𝒢<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h<VAR>Z✝ : C<VAR>g h : Y ⟶ Z✝<VAR>hgh : f ≫ g = f ≫ h<GOAL>g = h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>U : Set X<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>closure K ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>U : Set X<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>∀ i ∈ K, {y | Inseparable i y} ⊆ U
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝⁵ : Category.{v₁, u₁} 𝒮<VAR>inst✝⁴ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ✝ : a ⟶ b<VAR>inst✝³ : p.IsStronglyCartesian f φ✝<VAR>φ : a ⟶ b<VAR>inst✝² : p.IsStronglyCartesian f φ<VAR>R' : 𝒮<VAR>a' : 𝒳<VAR>g : R' ⟶ R<VAR>ψ ψ' : a' ⟶ a<VAR>inst✝¹ : p.IsHomLift g ψ<VAR>inst✝ : p.IsHomLift g ψ'<VAR>h : ψ ≫ φ = ψ' ≫ φ<GOAL>ψ = ψ'
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c✝ d x✝ y z : P<VAR>r R✝ : ℝ<VAR>c x : P<VAR>R : ℝ<GOAL>dist (inversion c R x) c = R ^ 2 / dist x c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d x✝ y z : P<VAR>r R✝ : ℝ<VAR>x : P<VAR>R : ℝ<GOAL>dist (inversion x R x) x = R ^ 2 / dist x x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c✝ d x✝ y z : P<VAR>r R✝ : ℝ<VAR>c x : P<VAR>R : ℝ<VAR>hx : x ≠ c<GOAL>dist (inversion c R x) c = R ^ 2 / dist x c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c✝ d x✝ y z : P<VAR>r R✝ : ℝ<VAR>c x : P<VAR>R : ℝ<VAR>hx : x ≠ c<VAR>this : dist x c ≠ 0<GOAL>dist (inversion c R x) c = R ^ 2 / dist x c
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>E : Set α<GOAL>cthickening (max 0 δ) E = cthickening δ E
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : ¬p = 0<GOAL>(X - C a) ^ rootMultiplicity a p ∣ p
<VAR>x✝ y x : ℝ≥0<GOAL>sqrt x * sqrt x = x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Simplex ℝ P 0<VAR>i : Fin 1<GOAL>s.circumcenter = s.points i
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Simplex ℝ P 0<VAR>i : Fin 1<VAR>h : s.circumcenter ∈ affineSpan ℝ (Set.range s.points)<GOAL>s.circumcenter = s.points i
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Simplex ℝ P 0<VAR>i : Fin 1<VAR>h : s.circumcenter ∈ affineSpan ℝ (Set.range s.points)<VAR>this : Unique (Fin 1)<GOAL>s.circumcenter = s.points i
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Simplex ℝ P 0<VAR>i : Fin 1<VAR>this : Unique (Fin 1)<VAR>h : s.circumcenter = s.points default<GOAL>s.circumcenter = s.points i
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Simplex ℝ P 0<VAR>i : Fin 1<VAR>this : Unique (Fin 1)<VAR>h : s.circumcenter = s.points default<GOAL>default = i
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : DecidableEq m<VAR>a : α<GOAL>a • 1 = diagonal fun x => a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedCommSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>z : E<VAR>c : 𝕜<GOAL>Convex 𝕜 ((fun x => z + c • x) '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>c₁ c₂ : Computation α<VAR>h : c₁ ~ c₂<GOAL>c₁.Terminates ↔ c₂.Terminates
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n<GOAL>N.LinearDisjoint M
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n<GOAL>Function.Injective ⇑(M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M))
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>ιM' : Type u_8<VAR>inst✝¹ : Fintype ιM'<VAR>inst✝ : DecidableEq ιM'<VAR>bₘ' : Basis ιM' R M<VAR>f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (aeval X).toRingHom<GOAL>φ.polyCharpolyAux b bₘ = φ.polyCharpolyAux b bₘ'
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>ιM' : Type u_8<VAR>inst✝¹ : Fintype ιM'<VAR>inst✝ : DecidableEq ιM'<VAR>bₘ' : Basis ιM' R M<VAR>f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (aeval X).toRingHom<VAR>hf : Function.Injective f<GOAL>φ.polyCharpolyAux b bₘ = φ.polyCharpolyAux b bₘ'
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>ιM' : Type u_8<VAR>inst✝¹ : Fintype ιM'<VAR>inst✝ : DecidableEq ιM'<VAR>bₘ' : Basis ιM' R M<VAR>f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (aeval X).toRingHom<VAR>hf : Function.Injective f<GOAL>f (φ.polyCharpolyAux b bₘ) = f (φ.polyCharpolyAux b bₘ')
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>ιM' : Type u_8<VAR>inst✝¹ : Fintype ιM'<VAR>inst✝ : DecidableEq ιM'<VAR>bₘ' : Basis ιM' R M<VAR>f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (aeval X).toRingHom<VAR>hf : Function.Injective f<VAR>_h1 : Module.Finite (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) := Module.Finite.of_basis (basis (MvPolynomial ι R) bₘ)<GOAL>f (φ.polyCharpolyAux b bₘ) = f (φ.polyCharpolyAux b bₘ')
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>ιM' : Type u_8<VAR>inst✝¹ : Fintype ιM'<VAR>inst✝ : DecidableEq ιM'<VAR>bₘ' : Basis ιM' R M<VAR>f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) := Polynomial.map (aeval X).toRingHom<VAR>hf : Function.Injective f<VAR>_h1 : Module.Finite (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) := Module.Finite.of_basis (basis (MvPolynomial ι R) bₘ)<VAR>_h2 : Module.Free (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) := Module.Free.of_basis (basis (MvPolynomial ι R) bₘ)<GOAL>f (φ.polyCharpolyAux b bₘ) = f (φ.polyCharpolyAux b bₘ')
<VAR>x : ℝ<GOAL>abs (cexp ↑x) = Real.exp x
<VAR>x : ℝ<GOAL>abs ↑(Real.exp x) = Real.exp x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<GOAL>1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : b < 0<GOAL>1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a c d : α<VAR>n : ℤ<GOAL>1 < a / 0 ↔ 0 < 0 ∧ 0 < a ∨ 0 < 0 ∧ a < 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : 0 < b<GOAL>1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b