mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_insert_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.isEmpty = true → (t.insert k).min? = some k
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.path_concat : ∀ {V : Type u_1} {G : SimpleGraph V},
  G.IsAcyclic →
    ∀ {u v w : V} {p : G.Walk u v} {q : G.Walk u w},
      p.IsPath → q.IsPath → ∀ (hadj : G.Adj v w), v ∈ q.support → q = p.concat hadj
-- Mathlib.Data.Int.Init
Int.dvd_div_of_mul_dvd : ∀ {a b c : ℤ}, a * b ∣ c → b ∣ c / a
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
addRothNumber.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α],
  addRothNumber =
    { toFun := fun s => Nat.findGreatest (fun m => ∃ t ⊆ s, t.card = m ∧ ThreeAPFree ↑t) s.card, monotone' := ⋯ }
-- Mathlib.Order.SaddlePoint
isSaddlePointOn_iff : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} {X : Set E} {Y : Set F} {f : E → F → β} [inst : CompleteLinearOrder β]
  {a : E}, a ∈ X → ∀ {b : F}, b ∈ Y → (IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b)
-- Mathlib.Analysis.Convex.Gauge
gauge_norm_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : RCLike 𝕜]
  [inst_3 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E], Balanced 𝕜 s → ∀ (r : 𝕜) (x : E), gauge s (‖r‖ • x) = gauge s (r • x)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.le_iff_le : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {x y : R}, v₁ x ≤ v₁ y ↔ v₂ x ≤ v₂ y
-- Mathlib.MeasureTheory.Integral.CircleIntegral
cauchyPowerSeries.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ),
  cauchyPowerSeries f c R n =
    ContinuousMultilinearMap.mkPiRing ℂ (Fin n)
      ((2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)
-- Lean.Parser.Basic
Lean.Parser.nodeFn : Lean.SyntaxNodeKind → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.measurableSet_preimage : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β},
  MeasurableEmbedding f → ∀ {s : Set β}, MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ Set.range f)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ →
    ∀ {k : α} {v : β k} {fallback : α}, (cmp (t.maxKeyD fallback) ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
-- Mathlib.Logic.Basic
ne_of_eq_of_ne : ∀ {α : Sort u_1} {a b c : α}, a = b → b ≠ c → a ≠ c
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.QuasiCompact f] (𝒰 : X.OpenCover)
  (U : ↑Y.affineOpens),
  ⨅ i, (AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)).ideal U = f.ker.ideal U
-- Mathlib.CategoryTheory.Limits.Cones
/-- Given a cone morphism whose object part is an isomorphism, produce an
isomorphism of cones.
 -/
CategoryTheory.Limits.Cone.cone_iso_of_hom_iso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {K : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone K} (f : c ⟶ d) [i : CategoryTheory.IsIso f.hom],
  CategoryTheory.IsIso f
-- Mathlib.Data.Sym.Sym2
Sym2.map.injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → Function.Injective (Sym2.map f)
-- Batteries.Data.PairingHeap
/-- `O(n)`. The number of elements in the heap.  -/
Batteries.PairingHeap.size : {α : Type u} → {le : α → α → Bool} → Batteries.PairingHeap α le → ℕ
-- Std.Time.DateTime
Std.Time.DateTime.instHSubOffset_6 : HSub Std.Time.DateTime Std.Time.Nanosecond.Offset Std.Time.DateTime
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `antitoneOn_dual_iff`. -/
AntitoneOn.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  AntitoneOn f s → AntitoneOn (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) s
-- Std.Time.DateTime.Timestamp
Std.Time.instReprTimestamp.repr : Std.Time.Timestamp → ℕ → Std.Format
-- Mathlib.Topology.Constructions.SumProd
isOpen_prod_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set (X × Y)},
  IsOpen s ↔ ∀ (a : X) (b : Y), (a, b) ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s
-- Mathlib.LinearAlgebra.Dimension.Finrank
Module.rank_eq_one_iff_finrank_eq_one : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.rank R M = 1 ↔ Module.finrank R M = 1
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {G H : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (θ : G ⟶ H) {a b c : B} {a' : CategoryTheory.Cat} (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) (X : ↑a'),
  CategoryTheory.CategoryStruct.comp
      ((θ.naturality (CategoryTheory.CategoryStruct.comp g h)).hom.toNatTrans.app (f.toFunctor.obj X))
      ((H.mapComp g h).hom.toNatTrans.app ((θ.app a).toFunctor.obj (f.toFunctor.obj X))) =
    CategoryTheory.CategoryStruct.comp
      ((θ.app c).toFunctor.map ((G.mapComp g h).hom.toNatTrans.app (f.toFunctor.obj X)))
      (CategoryTheory.CategoryStruct.comp
        ((θ.naturality h).hom.toNatTrans.app ((G.map g).toFunctor.obj (f.toFunctor.obj X)))
        ((H.map h).toFunctor.map ((θ.naturality g).hom.toNatTrans.app (f.toFunctor.obj X))))
-- Mathlib.Logic.Basic
Decidable.eq_or_ne : ∀ {α : Sort u_1} (x y : α) [Decidable (x = y)], x = y ∨ x ≠ y
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.sin_mul_sum_cos : ∀ (n : ℕ) (a b : ℂ),
  Complex.sin (a / 2) * ∑ i ∈ Finset.range n, Complex.cos (a * ↑i + b) =
    Complex.sin (↑n * a / 2) * Complex.cos ((↑n - 1) * a / 2 + b)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
IsAddRightRegular.withTop : ∀ {α : Type u} [inst : Add α] {a : α}, IsAddRightRegular a → IsAddRightRegular ↑a
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.toContinuousLinearMap_mapIsometry : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] F) (g : G →ₗᵢ[𝕜] H),
  (TensorProduct.mapIsometry f g).toContinuousLinearMap =
    TensorProduct.mapL f.toContinuousLinearMap g.toContinuousLinearMap
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_insert_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, t.isEmpty = true → (t.insert k v).minKey? = some k
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- A colimit cokernel cofork is mapped to a colimit cokernel cofork by a functor `G`
when this functor preserves the corresponding colimit.  -/
CategoryTheory.Limits.CokernelCofork.mapIsColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {X Y : C} →
              {f : X ⟶ Y} →
                (c : CategoryTheory.Limits.CokernelCofork f) →
                  CategoryTheory.Limits.IsColimit c →
                    (G : CategoryTheory.Functor C D) →
                      [inst_4 : G.PreservesZeroMorphisms] →
                        [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G] →
                          CategoryTheory.Limits.IsColimit (c.map G)
-- Init.Data.List.Basic
List.any_nil : ∀ {α : Type u_1} {f : α → Bool}, [].any f = false
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmuller_eq_teichmuller₀_toMonoidHom : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R], Perfection.teichmuller p I = ↑(Perfection.teichmuller₀ p I)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.mon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (self : CategoryTheory.CommMon C) → CategoryTheory.MonObj self.X
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- Given a point `x` corresponding to a homogeneous prime ideal, there is a (dependent) function
such that, for any `f` in the homogeneous localization at `x`, it returns the obvious section in the
basic open set `D(f.den)`.  -/
AlgebraicGeometry.sectionInBasicOpen : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (x : ↑(ProjectiveSpectrum.top 𝒜)) →
                (f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl) →
                  ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj
                      (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 ↑f.den)))
-- Mathlib.Topology.Compactness.Lindelof
/-- To show that a Lindelöf set intersects the intersection of a family of closed sets,
it is sufficient to show that it intersects every countable subfamily.  -/
IsLindelof.inter_iInter_nonempty : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
  IsLindelof s →
    ∀ (t : ι → Set X),
      (∀ (i : ι), IsClosed (t i)) → (∀ (u : Set ι), u.Countable ∧ (s ∩ ⋂ i ∈ u, t i).Nonempty) → (s ∩ ⋂ i, t i).Nonempty
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.uliftFunctor_obj : ∀ (X : CommGrpCat), CommGrpCat.uliftFunctor.obj X = CommGrpCat.of (ULift.{u, v} ↑X)
-- Mathlib.AlgebraicGeometry.Sites.BigZariski
/-- The Zariski pretopology on the category of schemes.  -/
AlgebraicGeometry.Scheme.zariskiPretopology : CategoryTheory.Pretopology AlgebraicGeometry.Scheme
-- Mathlib.Data.Set.Sigma
Set.fst_image_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {t : (i : ι) → Set (α i)} (s : Set ι),
  (∀ (i : ι), (t i).Nonempty) → Sigma.fst '' s.sigma t = s
-- Init.Omega.LinearCombo
_private.Init.Omega.LinearCombo.0.Lean.Omega.instReprInt : Repr ℤ
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.map_id_apply : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal]
  (h : optParam (N ≤ AddSubgroup.comap (AddMonoidHom.id G) N) ⋯) (x : G ⧸ N),
  (QuotientAddGroup.map N N (AddMonoidHom.id G) h) x = x
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X : C} {F : CategoryTheory.Sheaf J (Type (max v v'))}
  (f : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj X ⟶ F),
  J.uliftYonedaEquiv f =
    (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op X))) { down := CategoryTheory.CategoryStruct.id X }
-- Mathlib.NumberTheory.AbelSummation
_private.Mathlib.NumberTheory.AbelSummation.0.abelSummationProof.integralmulsum : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} {a b : ℝ},
  (∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) →
    MeasureTheory.IntegrableOn (deriv f) (Set.Icc a b) MeasureTheory.volume →
      ∀ (t₁ t₂ : ℝ) (n : ℕ),
        t₁ ≤ t₂ →
          ↑n ≤ t₁ →
            t₂ ≤ ↑n + 1 →
              a ≤ t₁ →
                t₂ ≤ b →
                  ∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k =
                    (f t₂ - f t₁) * ∑ k ∈ Finset.Icc 0 n, c k
-- Mathlib.Algebra.Group.Defs
/-- A `Monoid` is a `Semigroup` with an element `1` such that `1 * a = a * 1 = a`.  -/
Monoid : Type u → Type u
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Complex.sin` is complex analytic.  -/
Complex.analyticOnNhd_sin : ∀ {s : Set ℂ}, AnalyticOnNhd ℂ Complex.sin s
-- Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Complex.ofReal_arctan : ∀ (x : ℝ), ↑(Real.arctan x) = (↑x).arctan
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.isReflection_of_mem_leftInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) {t : W},
  t ∈ cs.leftInvSeq ω → cs.IsReflection t
-- Mathlib.Probability.Process.Predictable
/-- Sets of the form `(i, j] × A` for any `A ∈ 𝓕 i` are measurable with respect to the predictable
σ-algebra.  -/
MeasureTheory.measurableSet_predictable_Ioc_prod : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : LinearOrder ι] [inst_1 : OrderBot ι]
  {𝓕 : MeasureTheory.Filtration ι m} (i j : ι) {s : Set Ω}, MeasurableSet s → MeasurableSet (Set.Ioc i j ×ˢ s)
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.instIsMulCommutative_iSup : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Type u_4} [Nonempty ι] [inst_2 : Preorder ι] [IsDirectedOrder ι]
  {S : ι →o Submonoid M} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
/-- An additive action of an additive monoid `α` on a type `β` gives an additive action
of `Finset α` on `Finset β`  -/
Finset.addAction : {α : Type u_2} →
  {β : Type u_3} →
    [DecidableEq β] →
      [inst : DecidableEq α] → [inst_1 : AddMonoid α] → [AddAction α β] → AddAction (Finset α) (Finset β)
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.exact₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ), (X.sc₂ f g fg h n₀).Exact
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The composition of the adjunction gives the original functor.  -/
CategoryTheory.Cokleisli.Adjunction.toCokleisliCompFromCokleisliIsoSelf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (U : CategoryTheory.Comonad C) →
      (CategoryTheory.Cokleisli.Adjunction.toCokleisli U).comp (CategoryTheory.Cokleisli.Adjunction.fromCokleisli U) ≅
        U.toFunctor
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.typeParameter : Lean.Lsp.SemanticTokenType
-- Lean.Meta.Match.MatcherApp.Transform
_private.Lean.Meta.Match.MatcherApp.Transform.0.Lean.Meta.MatcherApp.withUserNamesImpl : {α : Type} → Array Lean.Expr → Array Lean.Name → Lean.MetaM α → Lean.MetaM α
-- Mathlib.Data.Holor
Holor.mul_left_distrib : ∀ {α : Type} {ds₁ ds₂ : List ℕ} [inst : Distrib α] (x : Holor α ds₁) (y z : Holor α ds₂),
  x.mul (y + z) = x.mul y + x.mul z
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryGED_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} {fallback : α × β},
          Std.DTreeMap.Internal.Impl.Const.getEntryGED k t₁ fallback =
            Std.DTreeMap.Internal.Impl.Const.getEntryGED k t₂ fallback
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.comp_comparison_hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J D)
  (R : CategoryTheory.Functor D C) [inst_3 : CategoryTheory.MonadicRightAdjoint R]
  [CategoryTheory.Limits.HasLimit (F.comp R)],
  CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Monad.comparison (CategoryTheory.monadicAdjunction R)))
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₁_hom : ∀ {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),
  ModuleCat.Hom.hom (groupHomology.mapCycles₁ f φ) = (ModuleCat.Hom.hom (groupHomology.chainsMap₁ f φ)).restrict ⋯
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.transcendental_of_ne_C : ∀ {K : Type u_1} [inst : Field K] (f : RatFunc K), (¬∃ c, f = RatFunc.C c) → Transcendental K f
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.mcasesPat_ : Lean.ParserDescr
-- Std.Internal.UV.System
/-- Generates cryptographically secure random bytes.
 -/
Std.Internal.UV.System.random : UInt64 → IO (IO.Promise (Except IO.Error ByteArray))
-- Mathlib.CategoryTheory.Shift.Basic
/-- Given a family of endomorphisms of `C` which are intertwined by a fully faithful `F : C ⥤ D`
with shift functors on `D`, we can promote that family to shift functors on `C`.  -/
CategoryTheory.Functor.FullyFaithful.hasShift : {C : Type u} →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {D : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} D] →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              {F : CategoryTheory.Functor C D} →
                F.FullyFaithful →
                  (s : A → CategoryTheory.Functor C C) →
                    ((i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)) → CategoryTheory.HasShift C A
-- Mathlib.Algebra.Homology.AlternatingConst
HomologicalComplex.alternatingConstScIsoEven.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0)
  (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [inst_2 : DecidableRel c.Rel]
  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) {i j k : ℕ} (hij : c.Rel i j) (hjk : c.Rel j k) (h : Even j),
  HomologicalComplex.alternatingConstScIsoEven A hOdd hEven hc hij hjk h =
    CategoryTheory.ShortComplex.isoMk
      (CategoryTheory.Iso.refl ((HomologicalComplex.alternatingConst A hOdd hEven hc).sc' i j k).X₁)
      (CategoryTheory.Iso.refl ((HomologicalComplex.alternatingConst A hOdd hEven hc).sc' i j k).X₂)
      (CategoryTheory.Iso.refl ((HomologicalComplex.alternatingConst A hOdd hEven hc).sc' i j k).X₃) ⋯ ⋯
-- Lean.Meta.SynthInstance
/-- `getSubgoals lctx localInsts xs inst` creates the subgoals for the instance `inst`.
The subgoals are in the context of the free variables `xs`, and
`(lctx, localInsts)` is the local context and instances before we added the free variables to it.

This extra complication is required because
  1- We want all metavariables created by `synthInstance` to share the same local context.
  2- We want to ensure that applications such as `mvar xs` are higher order patterns.

The method `getGoals` create a new metavariable for each parameter of `inst`.
For example, suppose the type of `inst` is `forall (x_1 : A_1) ... (x_n : A_n), B x_1 ... x_n`.
Then, we create the metavariables `?m_i : forall xs, A_i`, and return the subset of these
metavariables that are instance implicit arguments, and the expressions:
  - `inst (?m_1 xs) ... (?m_n xs)` (aka `instVal`)
  - `B (?m_1 xs) ... (?m_n xs)`  -/
Lean.Meta.SynthInstance.getSubgoals : Lean.LocalContext →
  Lean.LocalInstances →
    Array Lean.Expr → Lean.Meta.SynthInstance.Instance → Lean.MetaM Lean.Meta.SynthInstance.SubgoalsResult
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, t.isEmpty = true → ∀ {fallback : α}, (t.insert k v).minKeyD fallback = k
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.id.eq_1 : ∀ (M : Type u_2) {X : Type u_5} [inst : VAdd M X], AddActionHom.id M = { toFun := fun x => x, map_vadd' := ⋯ }
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.comp_continuousAt_iff' : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h : X ≃ₜ Y) (f : Y → Z) (x : X), ContinuousAt (f ∘ ⇑h) x ↔ ContinuousAt f (h x)
-- Mathlib.Order.Interval.Finset.Defs
LocallyFiniteOrderBot.ofIic'.eq_1 : ∀ (α : Type u_1) [inst : Preorder α] [inst_1 : DecidableLE α] (finsetIci : α → Finset α)
  (mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ x ≤ a),
  LocallyFiniteOrderBot.ofIic' α finsetIci mem_Ici =
    { finsetIio := fun a => {x ∈ finsetIci a | ¬a ≤ x}, finsetIic := finsetIci, finset_mem_Iic := mem_Ici,
      finset_mem_Iio := ⋯ }
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.comap.eq_1 : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I),
  CategoryTheory.Pi.comap C h =
    { obj := fun f i => f (h i), map := fun {X Y} α i => α (h i), map_id := ⋯, map_comp := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionHomRight`, the action of morphism in `D` on `C`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.«term_⊴ᵣ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Ring.Canonical
CanonicallyOrderedAdd.toMulLeftMono : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] [inst_1 : LE R] [CanonicallyOrderedAdd R], MulLeftMono R
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.rcoIterator.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (lowerBound upperBound : α),
  Std.DTreeMap.Internal.rcoIterator t lowerBound upperBound =
    {
      internalState :=
        { iter := Std.DTreeMap.Internal.Zipper.prependMapGE t lowerBound Std.DTreeMap.Internal.Zipper.done,
          upper := upperBound } }
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsSymm.eq : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : R →+* R}
  {B : M →ₛₗ[I] M →ₗ[R] R}, B.IsSymm → ∀ (x y : M), I ((B x) y) = (B y) x
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing A] [inst_4 : Algebra R A] (s : S) (a : A),
  (KaehlerDifferential.tensorKaehlerEquiv R S A (TensorProduct R S A)).symm
      ((KaehlerDifferential.D S (TensorProduct R S A)) (s ⊗ₜ[R] a)) =
    (algebraMap S (TensorProduct R S A)) s ⊗ₜ[A] (KaehlerDifferential.D R A) a
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.instIsMulLeftInvariantCount : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G],
  MeasureTheory.Measure.count.IsMulLeftInvariant
-- Init.Data.List.Lemmas
List.set_eq_nil_iff : ∀ {α : Type u_1} {l : List α} (i : ℕ) (a : α), l.set i a = [] ↔ l = []
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.rel₂_of_right : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  [inst_2 : Std.Iterators.Productive α₁ m] [inst_3 : Std.Iterators.Finite α₂ m] {it' it : Std.IterM m (β₁ × β₂)},
  it'.internalState.right.finitelyManySteps.Rel it.internalState.right.finitelyManySteps →
    Std.Iterators.Types.Zip.Rel₂ m it' it
-- Init.WF
PSigma.lex : {α : Sort u} →
  {β : α → Sort v} → WellFoundedRelation α → ((a : α) → WellFoundedRelation (β a)) → WellFoundedRelation (PSigma β)
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.det_vandermonde_sub : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v : Fin n → R) (a : R),
  (Matrix.vandermonde fun i => v i - a).det = (Matrix.vandermonde v).det