mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.visitType : Lean.Expr → Lean.Meta.LetToHave.M✝ Lean.Meta.LetToHave.Result✝
-- Mathlib.Logic.UnivLE
univLE_max : UnivLE.{u, max u v}
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_inter!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β k},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.inter! m₂).getD k fallback = fallback
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
/-- The fppf topology on the category of schemes is topology generated by the fppf precoverage.  -/
AlgebraicGeometry.Scheme.fppfTopology : CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_add_mul_left_right : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x (y + x * z) → IsCoprime x y
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Interval averages for zero radii equal values at the center point.  -/
Real.circleAverage_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} [CompleteSpace E],
  Real.circleAverage f c 0 = f c
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_linearMap_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B],
  Function.Injective fun x => ↑x
-- Lean.Elab.PreDefinition.WF.PackMutual
/-- Pass the first `n` arguments of `e` to the continuation, and apply the result to the
remaining arguments. If `e` does not have enough arguments, it is eta-expanded as needed.

Unlike `Meta.etaExpand` does not use `withDefault`.
 -/
Lean.Elab.WF.withAppN : ℕ → Lean.Expr → (Array Lean.Expr → Lean.MetaM Lean.Expr) → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piCongrRight_apply : ∀ {ι : Type u_7} {R : ι → Type u_8} {S : ι → Type u_9} [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)]
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (S i)] (e : (i : ι) → R i ≃+* S i) (x : (i : ι) → R i) (j : ι),
  (RingEquiv.piCongrRight e) x j = (e j) (x j)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The morphism `H^{n₀}(f₃) ⟶ Z^{n₁}(f₁, f₂)` induced by `δ`
when `f₁`, `f₂`, `f₃` are composable morphisms and `n₀ + 1 = n₁`.  -/
CategoryTheory.Abelian.SpectralObject.δToCycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (n₀ n₁ : ℤ) →
                      autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δToCycles._auto_1 →
                        ((X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f₃) ⟶ X.cycles f₁ f₂ n₁)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops_ground_eq : ∀ {α : Type u_1} (M : Matroid α), M.removeLoops.E = {e | M.IsNonloop e}
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullbackIsoProdSubtype_inv_snd_assoc : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) {Z_1 : TopCat} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (TopCat.pullbackIsoProdSubtype f g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) =
    CategoryTheory.CategoryStruct.comp (TopCat.pullbackSnd f g) h
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.GenerateHas.basic : ∀ {α : Type u_3} {s : Set (Set α)}, ∀ t ∈ s, MeasurableSpace.DynkinSystem.GenerateHas s t
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.State.mk.inj : ∀ {levelNames : List Lean.Name} {syntheticMVars : Lean.MVarIdMap Lean.Elab.Term.SyntheticMVarDecl}
  {pendingMVars : List Lean.MVarId} {mvarErrorInfos : List Lean.Elab.Term.MVarErrorInfo}
  {levelMVarErrorInfos : List Lean.Elab.Term.LevelMVarErrorInfo} {mvarArgNames : Lean.MVarIdMap Lean.Name}
  {letRecsToLift : List Lean.Elab.Term.LetRecToLift} {levelNames_1 : List Lean.Name}
  {syntheticMVars_1 : Lean.MVarIdMap Lean.Elab.Term.SyntheticMVarDecl} {pendingMVars_1 : List Lean.MVarId}
  {mvarErrorInfos_1 : List Lean.Elab.Term.MVarErrorInfo}
  {levelMVarErrorInfos_1 : List Lean.Elab.Term.LevelMVarErrorInfo} {mvarArgNames_1 : Lean.MVarIdMap Lean.Name}
  {letRecsToLift_1 : List Lean.Elab.Term.LetRecToLift},
  { levelNames := levelNames, syntheticMVars := syntheticMVars, pendingMVars := pendingMVars,
        mvarErrorInfos := mvarErrorInfos, levelMVarErrorInfos := levelMVarErrorInfos, mvarArgNames := mvarArgNames,
        letRecsToLift := letRecsToLift } =
      { levelNames := levelNames_1, syntheticMVars := syntheticMVars_1, pendingMVars := pendingMVars_1,
        mvarErrorInfos := mvarErrorInfos_1, levelMVarErrorInfos := levelMVarErrorInfos_1,
        mvarArgNames := mvarArgNames_1, letRecsToLift := letRecsToLift_1 } →
    levelNames = levelNames_1 ∧
      syntheticMVars = syntheticMVars_1 ∧
        pendingMVars = pendingMVars_1 ∧
          mvarErrorInfos = mvarErrorInfos_1 ∧
            levelMVarErrorInfos = levelMVarErrorInfos_1 ∧
              mvarArgNames = mvarArgNames_1 ∧ letRecsToLift = letRecsToLift_1
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.coe_subtype : ∀ {M : Type u_4} [inst : AddZeroClass M] (S : AddSubmonoid M), ⇑S.subtype = Subtype.val
-- Aesop.RuleSet
Aesop.GlobalRuleSet.mk : Aesop.BaseRuleSet → Lean.Meta.SimpTheorems → Lean.Meta.Simprocs → Aesop.GlobalRuleSet
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_biUnion_finset_congr : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Finset ι} {t : ι → Set α},
  μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.mem_range_embedding : ∀ {n : ℕ} (c : Composition n) (j : Fin n), j ∈ Set.range ⇑(c.embedding (c.index j))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Grp.Hom.hom_pow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} [inst_3 : CategoryTheory.IsCommMonObj H.X]
  (f : G ⟶ H) (n : ℕ), (f ^ n).hom = f.hom ^ n
-- Mathlib.Data.List.Sigma
List.NodupKeys.kunion : ∀ {α : Type u} {β : α → Type v} {l₁ l₂ : List (Sigma β)} [inst : DecidableEq α],
  l₁.NodupKeys → l₂.NodupKeys → (l₁.kunion l₂).NodupKeys
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.instInhabitedLazyEntry : Inhabited Lean.Meta.RefinedDiscrTree.LazyEntry
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneEquivalenceOpCoconeOp.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  CategoryTheory.Limits.coneEquivalenceOpCoconeOp F =
    CategoryTheory.Equivalence.mk''
      { obj := fun c => Opposite.op c.op, map := fun {Y X} f => Quiver.Hom.op { hom := f.hom.op, w := ⋯ }, map_id := ⋯,
        map_comp := ⋯ }
      { obj := fun c => (Opposite.unop c).unop, map := fun {Y X} f => { hom := f.unop.hom.unop, w := ⋯ }, map_id := ⋯,
        map_comp := ⋯ }
      (CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)))
      (CategoryTheory.Iso.refl
        ({ obj := fun c => (Opposite.unop c).unop, map := fun {Y X} f => { hom := f.unop.hom.unop, w := ⋯ },
              map_id := ⋯, map_comp := ⋯ }.comp
          { obj := fun c => Opposite.op c.op, map := fun {Y X} f => Quiver.Hom.op { hom := f.hom.op, w := ⋯ },
            map_id := ⋯, map_comp := ⋯ }))
      ⋯
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.map_comp_id : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) {X X' X'' : C} (Y : D) (f : X ⟶ X') (f' : X' ⟶ X''),
  P.map (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.id Y) =
    CategoryTheory.CategoryStruct.comp (P.map f (CategoryTheory.CategoryStruct.id Y))
      (P.map f' (CategoryTheory.CategoryStruct.id Y))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getLT!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  t₁.Equiv t₂ → t₁.getLT! k = t₂.getLT! k
-- Mathlib.Topology.Order.Basic
tendsto_nhds_top_mono' : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace β] [inst_1 : Preorder β] [inst_2 : OrderTop β] [OrderTopology β]
  {l : Filter α} {f g : α → β}, Filter.Tendsto f l (nhds ⊤) → f ≤ g → Filter.Tendsto g l (nhds ⊤)
-- Mathlib.Analysis.Real.Sqrt
/-- The real square root is less than the natural square root plus one  -/
Real.real_sqrt_lt_nat_sqrt_succ : ∀ {a : ℕ}, √↑a < ↑a.sqrt + 1
-- Mathlib.Algebra.Group.Pi.Basic
Subsingleton.pi_mulSingle_eq : ∀ {I : Type u} {α : Type u_4} [inst : DecidableEq I] [Subsingleton I] [inst_2 : One α] (i : I) (x : α),
  Pi.mulSingle i x = fun x_1 => x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.δ_single : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ L.X q) (n m : ℤ),
  n + 1 = m →
    ∀ (p' q' : ℤ),
      p' + 1 = p →
        q + 1 = q' →
          CochainComplex.HomComplex.δ n m (CochainComplex.HomComplex.Cochain.single f n) =
            CochainComplex.HomComplex.Cochain.single (CategoryTheory.CategoryStruct.comp f (L.d q q')) m +
              m.negOnePow • CochainComplex.HomComplex.Cochain.single (CategoryTheory.CategoryStruct.comp (K.d p' p) f) m
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : e.BoundaryGE i),
  HomologicalComplex.restrictionToTruncGE'.f K e i =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi').hom
      (CategoryTheory.CategoryStruct.comp (K.pOpcycles i') (K.truncGE'XIsoOpcycles e hi' hi).inv)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Set.smul_mem_centralizer : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} (r : R) {a : A}, a ∈ s.centralizer → r • a ∈ s.centralizer
-- Init.Data.Iterators.Combinators.Monadic.Take
/-- Given an iterator `it` and a natural number `n`, `it.take n` is an iterator that outputs
up to the first `n` of `it`'s values in order and then terminates.

**Marble diagram:**

```text
it          ---a----b---c--d-e--⊥
it.take 3   ---a----b---c⊥

it          ---a--⊥
it.take 3   ---a--⊥
```

**Termination properties:**

* `Finite` instance: only if `it` is productive
* `Productive` instance: only if `it` is productive

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it`.
 -/
Std.IterM.take : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → [inst : Std.Iterator α m β] → ℕ → Std.IterM m β → Std.IterM m β
-- Mathlib.Data.Set.Finite.Lattice
Set.Finite.sInter : ∀ {α : Type u_1} {s : Set (Set α)} {t : Set α}, t ∈ s → t.Finite → (⋂₀ s).Finite
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.isNonZero.eq_1 : Nat.Internal.Linear.Poly.isNonZero [] = false
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∪ t₂).getKey? k = t₁.getKey? k
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Argument is relevant for E-matching.  -/
Lean.Meta.Grind.NormalizePattern.PatternArgKind.relevant : Lean.Meta.Grind.NormalizePattern.PatternArgKind
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Restricting a partial equivalence to `e.source ∩ s`  -/
PartialEquiv.restr : {α : Type u_1} → {β : Type u_2} → PartialEquiv α β → Set α → PartialEquiv α β
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- A constant `Q₃` that satisfies `Q₃ * Φ = θ`.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₃ : {K : Type u_1} → [inst : Field K] → {E : IntermediateField K (RatFunc K)} → E ≠ ⊥ → K
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instFaithfulForget : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.AddGrp.forget C).Faithful
-- Mathlib.Analysis.Normed.Group.Defs
NormedGroup.toMetricSpace : {E : Type u_8} → [self : NormedGroup E] → MetricSpace E
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_ratCast_mul : ∀ (q : ℚ) {x : ℝ}, Irrational (↑q * x) → Irrational x
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_left_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (Y : T) (X : D)
  (Y_1 : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)),
  ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y_1).left.as = PUnit.unit
-- Mathlib.Probability.Distributions.Gaussian.Real
MeasurableEmbedding.gaussianReal_comap_apply : ∀ {μ : ℝ} {v : NNReal},
  v ≠ 0 →
    ∀ {f : ℝ → ℝ},
      MeasurableEmbedding f →
        ∀ {f' : ℝ → ℝ},
          (∀ (x : ℝ), HasDerivAt f (f' x) x) →
            ∀ {s : Set ℝ},
              MeasurableSet s →
                (MeasureTheory.Measure.comap f (ProbabilityTheory.gaussianReal μ v)) s =
                  ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * ProbabilityTheory.gaussianPDFReal μ v (f x))
-- Mathlib.Topology.UniformSpace.Equiv
/-- `Equiv.piCongr` as a uniform isomorphism: this is the natural isomorphism
`Π i₁, β₁ i ≃ᵤ Π i₂, β₂ i₂` obtained from a bijection `ι₁ ≃ ι₂` and isomorphisms
`β₁ i₁ ≃ᵤ β₂ (e i₁)` for each `i₁ : ι₁`.  -/
UniformEquiv.piCongr : {ι₁ : Type u_4} →
  {ι₂ : Type u_5} →
    {β₁ : ι₁ → Type u_6} →
      {β₂ : ι₂ → Type u_7} →
        [inst : (i₁ : ι₁) → UniformSpace (β₁ i₁)] →
          [inst_1 : (i₂ : ι₂) → UniformSpace (β₂ i₂)] →
            (e : ι₁ ≃ ι₂) → ((i₁ : ι₁) → β₁ i₁ ≃ᵤ β₂ (e i₁)) → ((i₁ : ι₁) → β₁ i₁) ≃ᵤ ((i₂ : ι₂) → β₂ i₂)
-- Init.Core
Iff.refl : ∀ (a : Prop), a ↔ a
-- Mathlib.Data.Seq.Computation
Computation.LiftRel.equiv : ∀ {α : Type u} (R : α → α → Prop), Equivalence R → Equivalence (Computation.LiftRel R)
-- Init.Control.Basic
ToBool.toBool : {α : Type u} → [self : ToBool α] → α → Bool
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainNonUnitalRingHom.eq_1 : ∀ (R : Type u_3) {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Add M] [inst_2 : Add N] (f : M →ₙ+ N),
  AddMonoidAlgebra.mapDomainNonUnitalRingHom R f =
    { toFun := AddMonoidAlgebra.mapDomain ⇑f, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupContent : Type
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₃.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.v₁₂.τ₁ (CategoryTheory.CategoryStruct.comp S.v₂₃.τ₁ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Order.SuccPred.Basic
Order.pred_succ_of_not_isMax : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : SuccOrder α] {a : α},
  ¬IsMax a → Order.pred (Order.succ a) = a
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  -/
TensorProduct.«term_⊗[_]_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Convex.Quasiconvex
QuasilinearOn.isPreconnected_preimage_subtype : ∀ {E : Type u_4} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E] {β : Type u_5} [inst_5 : Preorder β] {f : E → β} {s : Set E} {t : β},
  QuasilinearOn ℝ s f → IsPreconnected (Subtype.val ⁻¹' f ⁻¹' Set.Iic t)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.toSubgroup_comap : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (f : G →* H) (K : FiniteIndexNormalSubgroup H),
  (FiniteIndexNormalSubgroup.comap f K).toSubgroup = Subgroup.comap f K.toSubgroup
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
ContinuousWithinAt.log : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {s : Set α} {a : α},
  ContinuousWithinAt f s a → f a ≠ 0 → ContinuousWithinAt (fun x => Real.log (f x)) s a
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzOnWith.ediam_image2_le : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] (f : α → β → γ) {K₁ K₂ : NNReal} (s : Set α) (t : Set β),
  (∀ b ∈ t, LipschitzOnWith K₁ (fun x => f x b) s) →
    (∀ a ∈ s, LipschitzOnWith K₂ (f a) t) →
      Metric.ediam (Set.image2 f s t) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t
-- Mathlib.Order.Interval.Finset.Defs
Finset.Iio_toDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α),
  Finset.Iio (OrderDual.toDual a) = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioi a)
-- Mathlib.Dynamics.BirkhoffSum.Basic
birkhoffSum_add' : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : α → α) (g g' : α → M) (n : ℕ) (x : α),
  birkhoffSum f (g + g') n x = birkhoffSum f g n x + birkhoffSum f g' n x
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- A choice of a left fraction deduced from a right fraction for a morphism property `W`
when `W` has left calculus of fractions.  -/
CategoryTheory.MorphismProperty.RightFraction.leftFraction : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      [W.HasLeftCalculusOfFractions] → {X Y : C} → W.RightFraction X Y → W.LeftFraction X Y
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.CostructuredArrow.toOver_obj : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] (P : CategoryTheory.MorphismProperty D)
  (F : CategoryTheory.Functor C D) (X : D) (A : P.CostructuredArrow ⊤ F X),
  (CategoryTheory.MorphismProperty.CostructuredArrow.toOver P F X).obj A =
    CategoryTheory.MorphismProperty.Over.mk ⊤ A.hom ⋯
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.MatchUnifyResult.us : Lean.Meta.Sym.MatchUnifyResult → List Lean.Level
-- Mathlib.CategoryTheory.Sites.SheafHom
CategoryTheory.PresheafHom.IsSheafFor.exists_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {F G : CategoryTheory.Functor Cᵒᵖ A} {X : C} {S : CategoryTheory.Sieve X}
  (hG :
    ⦃Y : C⦄ →
      (f : Y ⟶ X) → CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Sieve.pullback f S).arrows.cocone.op))
  (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.presheafHom F G) S.arrows) {Y : C},
  x.Compatible →
    ∀ (g : Y ⟶ X),
      ∃ φ,
        ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (CategoryTheory.CategoryStruct.comp p g)),
          CategoryTheory.CategoryStruct.comp φ (G.map p.op) =
            CategoryTheory.CategoryStruct.comp (F.map p.op)
              ((x (CategoryTheory.CategoryStruct.comp p g) hp).app
                (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id Z))))
-- Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
CategoryTheory.Preadditive.DoldKan.equivalence_unitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Preadditive.DoldKan.equivalence.unitIso = AlgebraicTopology.DoldKan.Γ₂N₂
-- Mathlib.Data.Finset.Card
/-- **Alias** of the reverse direction of `Finset.card_sdiff_eq_card_sdiff_iff`. -/
Finset.card_sdiff_comm : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], s.card = t.card → (s \ t).card = (t \ s).card
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_whiskerRight_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.LaxFunctor B C} (x_3 x_4 : x ⟶ x_1) (Γ : x_3 ⟶ x_4) (ι : x_1 ⟶ x_2) (a : B),
  (CategoryTheory.Bicategory.whiskerRight Γ ι).as.app a = CategoryTheory.Bicategory.whiskerRight (Γ.as.app a) (ι.app a)
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_top_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E),
  A.relrank ⊤ = Module.rank (↥A) E
-- Mathlib.Data.Sum.Interval
_private.Mathlib.Data.Sum.Interval.0.Finset.sumLift₂.match_1.eq_4 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (motive : α₁ ⊕ α₂ → β₁ ⊕ β₂ → Sort u_5) (a : α₂)
  (b : β₂) (h_1 : (a : α₁) → (b : β₁) → motive (Sum.inl a) (Sum.inl b))
  (h_2 : (val : α₁) → (val_1 : β₂) → motive (Sum.inl val) (Sum.inr val_1))
  (h_3 : (val : α₂) → (val_1 : β₁) → motive (Sum.inr val) (Sum.inl val_1))
  (h_4 : (a : α₂) → (b : β₂) → motive (Sum.inr a) (Sum.inr b)),
  (match Sum.inr a, Sum.inr b with
    | Sum.inl a, Sum.inl b => h_1 a b
    | Sum.inl val, Sum.inr val_1 => h_2 val val_1
    | Sum.inr val, Sum.inl val_1 => h_3 val val_1
    | Sum.inr a, Sum.inr b => h_4 a b) =
    h_4 a b
-- Init.Data.SInt.Basic
instXorOpInt16 : XorOp Int16
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.isProbabilityMeasure_iff_real : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  MeasureTheory.IsProbabilityMeasure μ ↔ μ.real Set.univ = 1
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.hom_ofHom : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : CommRing X] [inst_2 : HopfAlgebra R X] [inst_3 : CommRing Y]
  [inst_4 : HopfAlgebra R Y] (f : X →ₐc[R] Y), CommHopfAlgCat.Hom.hom (CommHopfAlgCat.ofHom f) = f
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.add_assoc : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a b c : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel.below ⋯
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (Y : T) (X : D)
  (Y_1 : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)),
  ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y_1).right.hom = Y_1.hom
-- Mathlib.LinearAlgebra.Determinant
/-- If a linear map has determinant different from `1`, then the space is finite-dimensional.  -/
LinearMap.finite_of_det_ne_one : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : M →ₗ[R] M},
  LinearMap.det f ≠ 1 → Module.Finite R M
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.completedCosZeta_neg : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedCosZeta (-a) s = HurwitzZeta.completedCosZeta a s