mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- A finprod of meromorphic functions in normal form is in normal form if at most one of the factors
vanishes.
 -/
meromorphicNFAt_finprod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_3} {f : ι → 𝕜 → 𝕜},
  (∀ (i : ι), MeromorphicNFAt (f i) x) → {σ | f σ x = 0}.Subsingleton → MeromorphicNFAt (∏ᶠ (i : ι), f i) x
-- Mathlib.Data.Nat.Sqrt
Nat.lt_succ_sqrt' : ∀ (n : ℕ), n < n.sqrt.succ ^ 2
-- Init.Data.Array.Lemmas
Array.foldlM_reverse : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {xs : Array α} {f : β → α → m β} {b : β},
  Array.foldlM f b xs.reverse = Array.foldrM (fun x y => f y x) b xs
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.setIntegral_dirac : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [hE : CompleteSpace E]
  [inst_2 : MeasurableSpace α] [MeasurableSingletonClass α] (f : α → E) (a : α) (s : Set α)
  [inst_4 : Decidable (a ∈ s)], ∫ (x : α) in s, f x ∂MeasureTheory.Measure.dirac a = if a ∈ s then f a else 0
-- Std.Do.WP.SimpLemmas
Std.Do.WP.read_MonadReaderOf : ∀ {m : Type u → Type v} {ρ : Type u} {n : Type u → Type u_1} {ps : Std.Do.PostShape} {Q : Std.Do.PostCond ρ ps}
  [inst : MonadReaderOf ρ m] [inst_1 : MonadLift m n] [inst_2 : Std.Do.WP n ps],
  (Std.Do.wp MonadReaderOf.read).apply Q = (Std.Do.wp (MonadLift.monadLift read)).apply Q
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_inf : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L M : BooleanSubalgebra α} {a : α}, a ∈ L ⊓ M ↔ a ∈ L ∧ a ∈ M
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.D₂_D₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' i₁₂'' : I₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂' i₁₂'') h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.mem_compl_zeroLocus_iff_notMem : ∀ {R : Type u} [inst : CommSemiring R] {f : R} {I : PrimeSpectrum R}, I ∈ (PrimeSpectrum.zeroLocus {f})ᶜ ↔ f ∉ I.asIdeal
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.symm_trans : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h₁ : ContinuousMap.HomotopyEquiv X Y) (h₂ : ContinuousMap.HomotopyEquiv Y Z),
  (h₁.trans h₂).symm = h₂.symm.trans h₁.symm
-- Mathlib.Order.Filter.Lift
Filter.comap_lift'_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {h : Set α → Set β} {m : γ → β},
  Filter.comap m (f.lift' h) = f.lift' (Set.preimage m ∘ h)
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₀_unitIso_hom_app : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] (eA : A ≌ A')
  (e' : A' ≌ B') (X : A),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₀ eA e').unitIso.hom.app X =
    CategoryTheory.CategoryStruct.comp (eA.unitIso.hom.app X) (eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)))
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.nhdsWithin_source_inter : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X}, x ∈ e.source → ∀ (s : Set X), nhdsWithin x (e.source ∩ s) = nhdsWithin x s
-- Mathlib.CategoryTheory.Preadditive.LiftToFinset
CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_π_app_eq_sum : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteProducts C] {α : Type w} [inst_3 : DecidableEq α] (f : α → C)
  [inst_4 : CategoryTheory.Limits.HasProduct f] (S : (Finset (CategoryTheory.Discrete α))ᵒᵖ),
  (CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone f).π.app S =
    ∑ a ∈ (Opposite.unop S).attach,
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f (↑a).as)
        (CategoryTheory.Limits.Pi.ι (fun a => f (↑a).as) a)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- For all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the
pair `(μ m n₁, μ m n₂)` obtained from `(n₁, n₂)` by acting upon it by `m`, then, the relation
`r` also holds for the pair `(n₁, n₂)`.  -/
ContravariantClass.elim : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [self : ContravariantClass M N μ r],
  Contravariant M N μ r
-- Mathlib.Topology.Order
le_nhdsAdjoint_iff' : ∀ {α : Type u} {a : α} {f : Filter α} {t : TopologicalSpace α},
  t ≤ nhdsAdjoint a f ↔ nhds a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → nhds b = pure b
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.inter_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.inter m₂ = m₁ ∩ m₂
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.top_left : ∀ (R : Type u_1) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M], Module.Finite (↥⊤) M
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.dfinsuppFamily_add : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : Semiring R]
  [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)]
  [inst_5 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_6 : (p : (i : ι) → κ i) → Module R (N p)]
  (f g : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)),
  MultilinearMap.dfinsuppFamily (f + g) = MultilinearMap.dfinsuppFamily f + MultilinearMap.dfinsuppFamily g
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
/-- A square matrix `A` over a commutative semiring `R` is called nonsingular if it is
only determinant balanced with respect to equal elements.

See also See also `Matrix.Nondegenerate`.  -/
Matrix.Nonsingular : {n : Type u_1} → {R : Type u_3} → [Fintype n] → [DecidableEq n] → [CommSemiring R] → Matrix n n R → Prop
-- Lean.HeadIndex
Lean.instReprHeadIndex.repr : Lean.HeadIndex → ℕ → Std.Format
-- Mathlib.Order.CompleteLattice.Basic
iInf_le_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α} [Nonempty ι], ⨅ i, f i ≤ ⨆ i, f i
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Pos.find?_bool_eq_none_iff : ∀ {p : Char → Bool} {s : String} {pos : s.Pos},
  pos.find? p = none ↔ ∀ (pos' : s.Pos), pos ≤ pos' → ∀ (h : pos' ≠ s.endPos), p (pos'.get h) = false
-- Mathlib.RingTheory.Ideal.Maps
/-- Synonym for `RingHom.ker_coe_equiv`, but given an algebra equivalence.  -/
AlgHom.ker_coe_equiv : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (e : A ≃ₐ[R] B), RingHom.ker ↑e = ⊥
-- Init.Data.SInt.Lemmas
Int8.toInt8_toUInt8 : ∀ (x : Int8), x.toUInt8.toInt8 = x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  (self : CategoryTheory.Limits.ChosenPullback f₁ f₂) {Z : C} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.p₁ (CategoryTheory.CategoryStruct.comp f₁ h) =
    CategoryTheory.CategoryStruct.comp self.p₂ (CategoryTheory.CategoryStruct.comp f₂ h)
-- Mathlib.Topology.Separation.LinearUpperLowerSetTopology
instCompletelyNormalSpaceProp : CompletelyNormalSpace Prop
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.uniformContinuous_coe : ∀ {α : Type u_1} [inst : UniformSpace α], UniformContinuous SetLike.coe
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} {φ φ' : D₁ ⟶ D₂},
  (∀ (i : ι), φ.hom i = φ'.hom i) → φ = φ'
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.map_comp : ∀ {A B C σ τ ψ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A]
  [inst_3 : CommRing B] [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] [inst_6 : CommRing C]
  [inst_7 : SetLike ψ C] [inst_8 : AddSubgroupClass ψ C] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} {𝒞 : ℕ → ψ} [inst_9 : GradedRing 𝒜]
  [inst_10 : GradedRing ℬ] [inst_11 : GradedRing 𝒞] (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒞)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  (hg : HomogeneousIdeal.irrelevant 𝒞 ≤ HomogeneousIdeal.map g (HomogeneousIdeal.irrelevant ℬ)),
  AlgebraicGeometry.Proj.map (g.comp f) ⋯ =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.map g hg) (AlgebraicGeometry.Proj.map f hf)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.mem_toArray_iff_mem : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {a : α}, a ∈ r.toArray ↔ a ∈ r
-- Mathlib.Algebra.Lie.Ideal
LieHom.isIdealMorphism_of_surjective : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L'), Function.Surjective ⇑f → f.IsIdealMorphism
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- If `g` is continuous alternating and `f` is a continuous linear map, then `g (f m₁, ..., f mₙ)`
is again a continuous alternating map, that we call `g.compContinuousLinearMap f`.  -/
ContinuousAlternatingMap.compContinuousLinearMap : {R : Type u_1} →
  {M : Type u_2} →
    {M' : Type u_3} →
      {N : Type u_4} →
        {ι : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : Module R M] →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : AddCommMonoid M'] →
                    [inst_5 : Module R M'] →
                      [inst_6 : TopologicalSpace M'] →
                        [inst_7 : AddCommMonoid N] →
                          [inst_8 : Module R N] →
                            [inst_9 : TopologicalSpace N] → M [⋀^ι]→L[R] N → (M' →L[R] M) → M' [⋀^ι]→L[R] N
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion : AlgebraicGeometry.IsOpenImmersion.HasPullbacks
-- Init.Data.SInt.Lemmas
Int64.toInt_minValue : Int64.minValue.toInt = -2 ^ 63
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDerivWithin_congr' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f f₁ : E → F} {s : Set E}
  {x v : E}, Set.EqOn f₁ f s → x ∈ s → lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_comp_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct Z W] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y W]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X W],
  CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id W))
      (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id W))