mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.map_one_snd_of_isCocycle₂ : ∀ {G : Type u_1} {A : Type u_2} [inst : Monoid G] [inst_1 : AddCommGroup A] [inst_2 : MulAction G A] {f : G × G → A},
  groupCohomology.IsCocycle₂ f → ∀ (g : G), f (g, 1) = g • f (1, 1)
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeIdCompUliftYonedaOfPreservesColimitsOfSizeOfHasPointwiseLeftKanExtension : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  [CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
        max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
      L]
  [CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension
      (CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L)],
  L.IsLeftKanExtension (CategoryTheory.CategoryStruct.id (CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L))
-- Mathlib.Topology.Neighborhoods
/-- If two functions are equal in a neighbourhood of `x`, then for `y` sufficiently close
to `x` these functions are equal in a neighbourhood of `y`.  -/
Filter.EventuallyEq.eventuallyEq_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {f g : X → α},
  f =ᶠ[nhds x] g → ∀ᶠ (y : X) in nhds x, f =ᶠ[nhds y] g
-- Lean.Elab.PreDefinition.WF.Preprocess
Lean.Elab.WF.isWfParam? : Lean.Expr → Option Lean.Expr
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
/-- The diagonal morphism is always an immersion.  -/
AlgebraicGeometry.IsImmersion.instDiagonalScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsImmersion (CategoryTheory.Limits.pullback.diagonal f)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.InternalState.mk : Std.HashMap String (Lean.Doc.Ref✝ (Lean.Doc.Inline Lean.ElabInline)) →
  Std.HashMap String (Lean.Doc.Ref✝ String) → Array Lean.Doc.DeferredCheck → Lean.Doc.InternalState
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
/-- The canonical natural transformation
`(whiskeringRight Cᵒᵖ A B).obj F ⋙ G₂ ⟶ G₁ ⋙ sheafCompose J F`
when `F : A ⥤ B` is such that `J.HasSheafCompose F`, and that `G₁` and `G₂` are
left adjoints to the forget functors `sheafToPresheaf`.  -/
CategoryTheory.sheafComposeNatTrans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {A : Type u_1} →
        {B : Type u_2} →
          [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
            [inst_2 : CategoryTheory.Category.{v_2, u_2} B] →
              (F : CategoryTheory.Functor A B) →
                {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} →
                  (G₁ ⊣ CategoryTheory.sheafToPresheaf J A) →
                    {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} →
                      (G₂ ⊣ CategoryTheory.sheafToPresheaf J B) →
                        [inst_3 : J.HasSheafCompose F] →
                          ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp G₂ ⟶
                            G₁.comp (CategoryTheory.sheafCompose J F)
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.comap_exp_nhds_zero : Filter.comap Real.exp (nhds 0) = Filter.atBot
-- Init.Data.String.Pattern.Basic
/-- The default implementation of `ToForwardSearcher` repeatedly tries to match the pattern using
the given `ForwardPattern` instance.

It is sometimes possible to give a more efficient implementation; see `ToForwardSearcher`
for more details.
 -/
String.Slice.Pattern.ToForwardSearcher.defaultImplementation : {ρ : Type} →
  {pat : ρ} →
    [String.Slice.Pattern.ForwardPattern pat] →
      String.Slice.Pattern.ToForwardSearcher pat (String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher pat)
-- Mathlib.Order.Iterate
/-- If `f` is a monotone map and `x ≤ f x` at some point `x`, then the iterates `f^[n] x` form
a monotone sequence.  -/
Monotone.monotone_iterate_of_le_map : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x : α}, Monotone f → x ≤ f x → Monotone fun n => f^[n] x
-- Mathlib.Algebra.Polynomial.Derivation
Derivation.compAEval_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [inst_6 : IsScalarTower R A M]
  (d : Derivation R A M) (a : A) (f : Polynomial R),
  (d.compAEval a) f = (Module.AEval.of R M a) (d ((Polynomial.aeval a) f))
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.LaxRightLinear C] (d : D) (c c' : C)
  {Z : D'}
  (h :
    F.obj
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c') ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxRightLinear.μᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorObj c c'))
      (CategoryTheory.CategoryStruct.comp
        (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').hom) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
          (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c) c')
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.LaxRightLinear.μᵣ F
            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c')
          h))
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_mul_ball : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x y : E), {x} * Metric.ball y δ = Metric.ball (x * y) δ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α},
  (Std.HashMap.filterMap f m).getKey? k = (m.getKey? k).pfilter fun x_2 h' => (f x_2 m[x_2]).isSome
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.finMulAntidiag_zero_right : ∀ (d : ℕ), d.finMulAntidiag 0 = ∅
-- Mathlib.Topology.Homotopy.Product
/-- The relative product homotopy of `homotopies` between functions `f` and `g`  -/
ContinuousMap.HomotopyRel.pi : {I : Type u_1} →
  {A : Type u_2} →
    {X : I → Type u_3} →
      [inst : (i : I) → TopologicalSpace (X i)] →
        [inst_1 : TopologicalSpace A] →
          {f g : (i : I) → C(A, X i)} →
            {S : Set A} →
              ((i : I) → (f i).HomotopyRel (g i) S) → (ContinuousMap.pi f).HomotopyRel (ContinuousMap.pi g) S
-- Mathlib.Topology.Separation.Regular
T5Space.toT1Space : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T5Space X], T1Space X
-- Mathlib.Combinatorics.Derangements.Basic
derangements.Equiv.RemoveNone.fiber_none : ∀ {α : Type u_1} [inst : DecidableEq α], derangements.Equiv.RemoveNone.fiber none = ∅
-- Mathlib.Data.List.SplitBy
List.getLast_getLast_splitBy : ∀ {α : Type u_1} (r : α → α → Bool) {l : List α} (hn : l ≠ []), ((List.splitBy r l).getLast ⋯).getLast ⋯ = l.getLast hn
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.brecOn.eq : ∀ {motive_1 : Lean.Parser.Tactic.MRefinePat → Sort u} {motive_2 : List Lean.Parser.Tactic.MRefinePat → Sort u}
  (t : Lean.Parser.Tactic.MRefinePat) (F_1 : (t : Lean.Parser.Tactic.MRefinePat) → t.below → motive_1 t)
  (F_2 : (t : List Lean.Parser.Tactic.MRefinePat) → Lean.Parser.Tactic.MRefinePat.below_1 t → motive_2 t),
  t.brecOn F_1 F_2 = F_1 t (Lean.Parser.Tactic.MRefinePat.brecOn.go t F_1 F_2).2
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A B : C) {E : Type u₂} [inst_4 : CategoryTheory.Category.{v₂, u₂} E]
  [inst_5 : CategoryTheory.CartesianMonoidalCategory E] (G : CategoryTheory.Functor D E)
  [inst_6 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) (F.comp G)]
  [inst_8 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair (F.obj A) (F.obj B)) G],
  CategoryTheory.CartesianMonoidalCategory.prodComparisonIso (F.comp G) A B =
    G.mapIso (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso F A B) ≪≫
      CategoryTheory.CartesianMonoidalCategory.prodComparisonIso G (F.obj A) (F.obj B)
-- Mathlib.Order.Filter.Pointwise
Filter.inv_pure : ∀ {α : Type u_2} [inst : Inv α] {a : α}, (pure a)⁻¹ = pure a⁻¹
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.foldM_eq_foldlM_toArray : ∀ {α : Type u} {δ : Type w} {m' : Type w → Type w'} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst : Monad m'] [LawfulMonad m'] {f : δ → α → β → m' δ} {init : δ},
  Std.DHashMap.Raw.foldM f init ↑m = Array.foldlM (fun a b => f a b.1 b.2) init (Std.DHashMap.Raw.Const.toArray ↑m)
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.sumMk : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {M' : Type u_3} [inst_1 : Zero M'] {f : α → M} {g : α → M'},
  Function.HasFiniteSupport f → Function.HasFiniteSupport g → Function.HasFiniteSupport fun a => (f a, g a)
-- Mathlib.Algebra.Lie.UniversalEnveloping
instAlgebraUniversalEnvelopingAlgebra : (R : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Algebra R (UniversalEnvelopingAlgebra R L)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- Normalize the multiplicity of a prime ideal `p` in the factorization of `I`
as `multiplicity p.asIdeal I`.  -/
IsDedekindDomain.HeightOneSpectrum.count_normalizedFactors_eq_multiplicity : ∀ {R : Type u_3} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R},
  I ≠ ⊥ →
    ∀ (p : IsDedekindDomain.HeightOneSpectrum R),
      Multiset.count p.asIdeal (UniqueFactorizationMonoid.normalizedFactors I) = multiplicity p.asIdeal I
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.mul_subset_mul : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R}, ↑M * ↑N ⊆ ↑(M * N)
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.closedBallAddSubgroup.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  (c : FiniteArchimedeanClass M), c.closedBallAddSubgroup = FiniteArchimedeanClass.addSubgroup (UpperSet.Ici c)
-- Init.GetElem
List.getElem_cons_drop : ∀ {α : Type u_1} {as : List α} {i : ℕ} (h : i < as.length), as[i] :: List.drop (i + 1) as = List.drop i as
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhdsGT_zero_neBot : (nhdsWithin 0 (Set.Ioi 0)).NeBot
-- Init.Data.List.Impl
List.findSomeRev?_eq_findSome?_reverse : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → Option β}, List.findSomeRev? f l = List.findSome? f l.reverse
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofZeroDvd.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofZeroDvd c = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofZeroDvd c_1) =
    (c = c_1)
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.prop_retractClosure_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : C),
  P.retractClosure X ↔ ∃ Y, ∃ (_ : P Y), Nonempty (CategoryTheory.Retract X Y)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstField.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Calculus.Gradient.Basic
toDual_comp_gradientWithin : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {s : Set F},
  ⇑(InnerProductSpace.toDual 𝕜 F) ∘ gradientWithin f s = fderivWithin 𝕜 f s
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.proved.injEq : ∀ (newRapps newRapps_1 : Array Aesop.RappRef),
  (Aesop.SafeRulesResult.proved newRapps = Aesop.SafeRulesResult.proved newRapps_1) = (newRapps = newRapps_1)
-- Mathlib.Algebra.Polynomial.Div
Irreducible.isRoot_eq_bot_of_natDegree_ne_one : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} [IsDomain R], Irreducible p → p.natDegree ≠ 1 → p.IsRoot = ⊥
-- Init.Data.BitVec.Lemmas
/-- The number of leading zeroes is strictly less than the bitwidth iff the bitvector is nonzero.  -/
BitVec.clz_lt_iff_ne_zero : ∀ {w : ℕ} {x : BitVec w}, x.clz < ↑w ↔ x ≠ 0#w
-- Mathlib.Algebra.Group.Invertible.Basic
Commute.invOf_left : ∀ {α : Type u} [inst : Monoid α] {a b : α} [inst_1 : Invertible b], Commute b a → Commute (⅟b) a
-- Init.Data.Option.Lemmas
Option.get_congr : ∀ {α : Type u_1} {o o' : Option α} {ho : o.isSome = true} (h : o = o'), o.get ho = o'.get ⋯
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatClamp n).toUInt16 = UInt16.ofNatLT n ⋯
-- Mathlib.Lean.Expr.Rat
/-- Check if an expression is a "rational in normal form",
i.e. either an integer number in normal form,
or `n / d` where `n` is an integer in normal form, `d` is a natural number in normal form,
`d ≠ 1`, and `n` and `d` are coprime (in particular, we check that `(mkRat n d).den = d`).
If so returns the rational number.
 -/
Lean.Expr.rat? : Lean.Expr → Option ℚ
-- Mathlib.Algebra.Group.Units.Defs
Units.instDiv.eq_1 : ∀ {α : Type u} [inst : Monoid α],
  Units.instDiv = { div := fun a b => { val := ↑a * ↑b⁻¹, inv := ↑b * ↑a⁻¹, val_inv := ⋯, inv_val := ⋯ } }
-- Init.Prelude
instMonadLiftT : (m : Type u_1 → Type u_2) → MonadLiftT m m
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Structure containing the minimal axioms required to check that an order is a complete
distributive lattice. Do NOT use, except for implementing `CompleteDistribLattice` via
`CompleteDistribLattice.ofMinimalAxioms`.

This structure omits the `himp`, `compl`, `sdiff`, `hnot` fields, which can be recovered using
`CompleteDistribLattice.ofMinimalAxioms`.  -/
CompleteDistribLattice.MinimalAxioms : (α : Type u) → [CompleteLattice α] → Prop
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inr_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {d e : ℤ} (γ : CochainComplex.HomComplex.Cochain G K d) (he : 0 + d = e),
  (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp
      ((CochainComplex.mappingCone.snd φ).comp γ he) ⋯ =
    γ
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.cases.injEq : ∀ (target : Aesop.CasesTarget) (md : Lean.Meta.TransparencyMode) (isRecursiveType : Bool)
  (ctorNames : Array Aesop.CtorNames) (target_1 : Aesop.CasesTarget) (md_1 : Lean.Meta.TransparencyMode)
  (isRecursiveType_1 : Bool) (ctorNames_1 : Array Aesop.CtorNames),
  (Aesop.RuleTacDescr.cases target md isRecursiveType ctorNames =
      Aesop.RuleTacDescr.cases target_1 md_1 isRecursiveType_1 ctorNames_1) =
    (target = target_1 ∧ md = md_1 ∧ isRecursiveType = isRecursiveType_1 ∧ ctorNames = ctorNames_1)
-- Mathlib.Topology.MetricSpace.Isometry
NNReal.isometry_coe : Isometry NNReal.toReal
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.sinh_artanh : ∀ {x : ℝ}, x ∈ Set.Ioo (-1) 1 → Real.sinh (Real.artanh x) = x / √(1 - x ^ 2)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.AddConvolutionExistsAt.convolution_vadd : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} [inst : AddMonoid M] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : Module S E] [inst_5 : Module S E'] {F : Type u_10}
  [inst_6 : AddCommMonoid F] [inst_7 : Module S F] [inst_8 : TopologicalSpace F] [ContinuousConstSMul S F] [T2Space F]
  {c : S} {f : M → E} {g : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F),
  DiscreteConvolution.AddConvolutionExistsAt L f g x →
    DiscreteConvolution.addConvolution L f (c • g) x = c • DiscreteConvolution.addConvolution L f g x
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.isSetRing_supClosure : ∀ {α : Type u_1} {C : Set (Set α)}, MeasureTheory.IsSetSemiring C → MeasureTheory.IsSetRing (supClosure C)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_filterMap : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Option γ} (it : Std.IterM m β),
  (Std.IterM.filterMap f it).toListRev = (fun x => List.filterMap f x) <$> it.toListRev
-- Mathlib.RingTheory.KrullDimension.Basic
Ring.krullDimLE_one_iff : ∀ {R : Type u_1} [inst : CommSemiring R],
  Ring.KrullDimLE 1 R ↔ ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β},
  m.WF →
    Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.Const.modify m k f) k fallback =
      (Option.map f (Std.DHashMap.Raw.Const.get? m k)).getD fallback
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.induction₃ : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  {C : DirectLimit F f → DirectLimit F f → DirectLimit F f → Prop},
  (∀ (i : ι) (x y z : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ ⟦⟨i, z⟩⟧) → ∀ (x y z : DirectLimit F f), C x y z
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- An equivalence of categories `e` between `C` and `D` induces an equivalence between
`MonoOver X` and `MonoOver (e.functor.obj X)` whenever `X` is an object of `C`.  -/
CategoryTheory.MonoOver.congr : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : C) →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (e : C ≌ D) → CategoryTheory.MonoOver X ≌ CategoryTheory.MonoOver (e.functor.obj X)
-- Mathlib.Topology.Homotopy.TopCat.Path
TopCat.pathEquiv_apply_apply : ∀ {X : TopCat} {x y : ↑X} (p : X.Path x y) (a : ↑unitInterval),
  (TopCat.pathEquiv p) a = (TopCat.Hom.hom p.hom) (TopCat.I.homeomorph.symm a)
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.closure_rels_subset_ker : ∀ {α : Type u_1} {G : Type u_3} [inst : Group G] {f : α → G} {rels : Set (FreeGroup α)},
  (∀ r ∈ rels, (FreeGroup.lift f) r = 1) → Subgroup.normalClosure rels ≤ (FreeGroup.lift f).ker
-- Mathlib.Algebra.Group.ULift
ULift.group.eq_1 : ∀ {α : Type u} [inst : Group α], ULift.group = Function.Injective.group ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- An equalizer that is an epimorphism is an isomorphism.  -/
CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_epi : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {c : CategoryTheory.Limits.Fork f g}
  (h : CategoryTheory.Limits.IsLimit c) [CategoryTheory.Epi c.ι], CategoryTheory.IsIso c.ι
-- Mathlib.ModelTheory.Satisfiability
/-- A theory is maximal when it is satisfiable and contains each sentence or its negation.
Maximal theories are complete.  -/
FirstOrder.Language.Theory.IsMaximal : {L : FirstOrder.Language} → L.Theory → Prop
-- Mathlib.Order.Hom.Basic
/-- Curry/uncurry as an order isomorphism between `α × β →o γ` and `α →o β →o γ`.  -/
OrderHom.curry : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} → [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Preorder γ] → (α × β →o γ) ≃o (α →o β →o γ)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.State.diag : Lean.Meta.Simp.State → Lean.Meta.Simp.Diagnostics
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.norm_pos : ∀ (A : Type u_1) {E : Type u_2} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : Norm E] [CStarModule A E] {x : E}, x ≠ 0 → 0 < ‖x‖
-- Mathlib.Algebra.Ring.Prod
/-- `Prod.map` as a `RingHom`.  -/
RingHom.prodMap : {R : Type u_1} →
  {R' : Type u_2} →
    {S : Type u_3} →
      {S' : Type u_4} →
        [inst : NonAssocSemiring R] →
          [inst_1 : NonAssocSemiring S] →
            [inst_2 : NonAssocSemiring R'] →
              [inst_3 : NonAssocSemiring S'] → (R →+* R') → (S →+* S') → R × S →+* R' × S'
-- Mathlib.Topology.Algebra.Module.Equiv
/-- By definition, if `f` is not invertible then `inverse f = 0`.  -/
ContinuousLinearMap.inverse_of_not_isInvertible : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂}, ¬f.IsInvertible → f.inverse = 0
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.lsingle_comp_chainsMap_f_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (n : ℕ) (x : Fin n → G) {Z : ModuleCat k}
  (h : ModuleCat.of k ((Fin n → H) →₀ ↑B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle x))
      (CategoryTheory.CategoryStruct.comp ((groupHomology.chainsMap f φ).f n) h) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle (⇑f ∘ x) ∘ₗ (Rep.Hom.hom φ).toLinearMap)) h
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Continuity from above (a.e. version):
the measure of the intersection of a family of sets that is almost everywhere antitone
is equal to the infimum of the measures.  -/
MeasureTheory.measure_iInter_of_ae_antitone : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder ι]
  [IsDirectedOrder ι] [Filter.atTop.IsCountablyGenerated] {s : ι → Set α},
  (∀ᵐ (ω : α) ∂μ, Antitone fun x => ω ∈ s x) →
    (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) → (∃ i, μ (s i) ≠ ⊤) → μ (⋂ i, s i) = ⨅ i, μ (s i)
-- Init.Data.Int.Gcd
Int.gcd_mul_right_add_right : ∀ (m n k : ℤ), m.gcd (k * m + n) = m.gcd n
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫`.  -/
Orientation.inner_mul_inner_add_areaForm_mul_areaForm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (a x y : E),
  inner ℝ a x * inner ℝ a y + (o.areaForm a) x * (o.areaForm a) y = ‖a‖ ^ 2 * inner ℝ x y