mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)) {X' : C}
  (f' :
    ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).obj
        (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U))) ⟶
      X'),
  CategoryTheory.CategoryStruct.comp (D.opensImagePreimageMap i j U)
      (CategoryTheory.CategoryStruct.comp
        ((D.f j k).c.app (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U)))) f') =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k))
              (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).c.app
        (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
          (CategoryTheory.Limits.pullback.snd (D.f j i) (D.f j k))
          (Opposite.unop
            (Opposite.op
              ((TopologicalSpace.Opens.map
                    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k))
                        (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base).1
                (Opposite.unop (Opposite.op U))))))
        (CategoryTheory.CategoryStruct.comp ((D.V (j, k)).presheaf.map (CategoryTheory.eqToHom ⋯)) f'))
-- Mathlib.RingTheory.PrincipalIdealDomain
Ideal.exists_normalized_span_of_isPrincipal : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : NormalizationMonoid R] (I : Ideal R) [Submodule.IsPrincipal I],
  ∃ x, normalize x = x ∧ I = Ideal.span {x}
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- The sum of a locally finite collection of sections is differentiable at `x`
if each section is.  -/
MDifferentiableAt.sum_section_of_locallyFinite : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {x₀ : B} {ι : Type u_9}
  {t : ι → (x : B) → E x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) →
    (∀ (i : ι), MDiffAt (T% t) x₀) → (MDiffAt fun x => ⟨x, ∑' (i : ι), t i x⟩) x₀
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.alter!.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (f : Option β → Option β) (sz : ℕ) (k' : α) (v' : β)
  (l' r' : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.alter! k f (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.balance! k' v' (Std.DTreeMap.Internal.Impl.Const.alter! k f l') r'
    | Ordering.gt => Std.DTreeMap.Internal.Impl.balance! k' v' l' (Std.DTreeMap.Internal.Impl.Const.alter! k f r')
    | Ordering.eq =>
      match f (some v') with
      | none => l'.glue! r'
      | some v => Std.DTreeMap.Internal.Impl.inner sz k v l' r'
-- Std.Sync.Semaphore
_private.Std.Sync.Semaphore.0.Std.Semaphore.mk.injEq : ∀ (lock lock_1 : Std.Mutex Std.SemaphoreState✝), ({ lock := lock } = { lock := lock_1 }) = (lock = lock_1)
-- Mathlib.Algebra.Group.Action.Basic
smul_left_cancel_iff : ∀ {α : Type u_5} {β : Type u_6} [inst : Group α] [inst_1 : MulAction α β] (g : α) {x y : β}, g • x = g • y ↔ x = y
-- Batteries.Tactic.GeneralizeProofs
/-- State for the `MGen` monad.  -/
Batteries.Tactic.GeneralizeProofs.GState : Type
-- Init.Data.UInt.Lemmas
UInt16.add_assoc : ∀ (a b c : UInt16), a + b + c = a + (b + c)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_multiset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {g : ι → E → 𝔸'} [inst_5 : DecidableEq ι] {u : Multiset ι} {x : E},
  (∀ i ∈ u, DifferentiableAt 𝕜 (fun x => g i x) x) →
    fderiv 𝕜 (fun x => (Multiset.map (fun x_1 => g x_1 x) u).prod) x =
      (Multiset.map (fun i => (Multiset.map (fun x_1 => g x_1 x) (u.erase i)).prod • fderiv 𝕜 (g i) x) u).sum
-- Lean.ExtraModUses
Lean.ExtraModUse.mk.sizeOf_spec : ∀ (module : Lean.Name) (isExported isMeta : Bool),
  sizeOf { module := module, isExported := isExported, isMeta := isMeta } =
    1 + sizeOf module + sizeOf isExported + sizeOf isMeta
-- Lean.Structure
Lean.mergeStructureResolutionOrders : {m : Type → Type} →
  [Monad m] → [Lean.MonadEnv m] → Lean.Name → Array Lean.Name → Bool → m Lean.StructureResolutionOrderResult
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  m ≤ m₀ →
    ∀ [MeasureTheory.IsFiniteMeasure μ],
      MeasureTheory.MemLp X 2 μ → ProbabilityTheory.condVar m X μ =ᵐ[μ] μ[X ^ 2 | m] - μ[X | m] ^ 2
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_ofFin : ∀ (n : Fin USize.size) (h : System.Platform.numBits = 32), (USize.ofFin n).toBitVec32 h = { toFin := h ▸ n }
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.isAddRightInvariant : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → AddGroup (α i)] [∀ (i : ι), MeasurableAdd (α i)] [∀ (i : ι), (μ i).IsAddRightInvariant],
  (MeasureTheory.Measure.pi μ).IsAddRightInvariant
-- Mathlib.Topology.Baire.BaireMeasurable
BaireMeasurableSet.union : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α},
  BaireMeasurableSet s → BaireMeasurableSet t → BaireMeasurableSet (s ∪ t)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.snd_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C × D} (f : X ⟶ Y), (CategoryTheory.Prod.snd C D).map f = f.2
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.piEquivalenceFunctorDiscrete_functor_obj : ∀ (J : Type u₂) (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (F : J → C),
  (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.obj F = CategoryTheory.Discrete.functor F
-- Mathlib.CategoryTheory.Products.Basic
/-- The constant functor followed by the evaluation functor is just the identity.  -/
CategoryTheory.Functor.constCompEvaluationObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (X : C) →
          (CategoryTheory.Functor.const C).comp ((CategoryTheory.evaluation C D).obj X) ≅ CategoryTheory.Functor.id D
-- Mathlib.Topology.Algebra.Group.Basic
IsClosed.left_addCoset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {U : Set G},
  IsClosed U → ∀ (x : G), IsClosed (x +ᵥ U)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.least?_eq_none_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α]
  [Std.PRange.LawfulUpwardEnumerableLeast? α], Std.PRange.least? = none ↔ ¬Nonempty α
-- Mathlib.LinearAlgebra.Span.Defs
/-- A submodule is equal to the supremum of the spans of the submodule's nonzero elements.  -/
Submodule.submodule_eq_sSup_le_nonzero_spans : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Submodule R M), p = sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.exists_rightFraction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [W.HasRightCalculusOfFractions] {X Y : C} (φ : W.LeftFraction X Y),
  ∃ ψ, CategoryTheory.CategoryStruct.comp ψ.s φ.f = CategoryTheory.CategoryStruct.comp ψ.f φ.s
-- Mathlib.Order.BooleanAlgebra.Set
Set.union_eq_sdiff_union_sdiff_union_inter : ∀ {α : Type u_1} (s t : Set α), s ∪ t = s \ t ∪ t \ s ∪ s ∩ t
-- Lean.Meta.DiscrTree.Basic
_private.Lean.Meta.DiscrTree.Basic.0.Lean.Meta.DiscrTree.createNodes : {α : Type} → Array Lean.Meta.DiscrTree.Key → α → ℕ → Lean.Meta.DiscrTree.Trie α
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.mk.congr_simp : ∀ (z z_1 : ℂ) (e_z : z = z_1) (hz : ‖z‖ < 1), Complex.UnitDisc.mk z hz = Complex.UnitDisc.mk z_1 ⋯
-- Mathlib.Data.Complex.Basic
/-- The preimage under `equivRealProd` of `s ×ˢ t` is `s ×ℂ t`.  -/
Complex.preimage_equivRealProd_prod : ∀ (s t : Set ℝ), ⇑Complex.equivRealProd ⁻¹' s ×ˢ t = s ×ℂ t
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.TransvectionStruct.toSpecialLinearGroup_mk : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F] {i j : ι}
  (hij : i ≠ j) (c : F),
  { i := i, j := j, hij := hij, c := c }.toSpecialLinearGroup = Matrix.SpecialLinearGroup.transvection hij c
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsStableUnderUnitor.rightUnitor_hom_mem : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  (P : CategoryTheory.MorphismProperty C) [self : P.IsStableUnderUnitor] (c : C),
  P (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).hom
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.P_is_eventually_constant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {q n : ℕ},
  n ≤ q → (AlgebraicTopology.DoldKan.P (q + 1)).f n = (AlgebraicTopology.DoldKan.P q).f n
-- Mathlib.Order.Minimal
minimal_subtype : ∀ {α : Type u_2} {P Q : α → Prop} [inst : LE α] {x : Subtype Q}, Minimal (fun x => P ↑x) x ↔ Minimal (P ⊓ Q) ↑x
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.normalizedGcdMonoid : {R : Type u_1} → [inst : CommRing R] → [NormalizedGCDMonoid R] → NormalizedGCDMonoid (Polynomial R)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.fold_push_mk : ∀ {α : Type u} {β : Type v} {l : Std.DHashMap.Raw α fun x => β} {acc : Array (α × β)},
  Std.DHashMap.Raw.fold (fun acc k v => acc.push (k, v)) acc l =
    acc ++
      (List.map
          (fun x =>
            match x with
            | ⟨k, v⟩ => (k, v))
          (Std.DHashMap.Internal.toListModel l.buckets)).toArray
-- Mathlib.CategoryTheory.Sites.Point.Conservative
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.ObjectProperty J.Point},
  (CategoryTheory.JointlyReflectIsomorphisms fun Φ => Φ.obj.sheafFiber) → P.IsConservativeFamilyOfPoints
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_insertManyIfNewUnit_empty_list : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α] {l : List α} {k : α},
  Std.DTreeMap.Internal.Impl.contains k
      ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty l ⋯) =
    l.contains k
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.head.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (x : ι) (x_3 : M x) (a : x_3 ≠ 1),
  (Monoid.CoprodI.NeWord.singleton x_3 a).head = x_3
-- Mathlib.Data.Nat.Bitwise
Nat.lor_bit : ∀ (a : Bool) (m : ℕ) (b : Bool) (n : ℕ), Nat.bit a m ||| Nat.bit b n = Nat.bit (a || b) (m ||| n)
-- Mathlib.Algebra.Algebra.Equiv
ULift.algEquiv_symm_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (down : A),
  ULift.algEquiv.{u, v, w}.symm down = { down := down }
-- Mathlib.AlgebraicTopology.SingularHomology.Basic
/-- The `n`-th singular homology functor with coefficients in `C`.  -/
AlgebraicTopology.singularHomologyFunctor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        ℕ → [CategoryTheory.CategoryWithHomology C] → CategoryTheory.Functor C (CategoryTheory.Functor TopCat C)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.Pos.revSkipWhile_char_eq_self_iff_get : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  pos.revSkipWhile c = pos ↔ ∀ (h : pos ≠ s.startPos), (pos.prev h).get ⋯ ≠ c
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesOnBall.hasFiniteFPowerSeriesAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n : ℕ},
  HasFiniteFPowerSeriesOnBall f p x n r → HasFiniteFPowerSeriesAt f p x n
-- Mathlib.NumberTheory.Padics.PadicNorm
padicNorm.of_nat : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ), padicNorm p ↑m ≤ 1
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.instIsMulCommutative_iSup : ∀ {R : Type u} [inst : NonAssocRing R] {ι : Type u_1} [Nonempty ι] [inst_2 : Preorder ι] [IsDirectedOrder ι]
  {S : ι →o Subring R} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.Analysis.CStarAlgebra.Hom
IsSelfAdjoint.map_spectrum_real : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CStarAlgebra A] [inst_1 : CStarAlgebra B]
  [inst_2 : FunLike F A B] [AlgHomClass F ℂ A B] [StarHomClass F A B] {a : A},
  IsSelfAdjoint a → ∀ (φ : F), Function.Injective ⇑φ → spectrum ℝ (φ a) = spectrum ℝ a
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.CountablySeparated.countably_separated : ∀ {α : Type u_3} {inst : MeasurableSpace α} [self : MeasurableSpace.CountablySeparated α],
  HasCountableSeparatingOn α MeasurableSet Set.univ
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_mul₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Mul β]
  [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.Kernel.IndepFun (f i * f j) (f k * f l) κ μ
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Finset.ProveEmptyOrConsResult.cons.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(Finset «$α»)} {a : Q(«$α»)} {s' : Q(Finset «$α»)} {h : Q(«$a» ∉ «$s'»)}
  {pf : Q(«$s» = Finset.cons «$a» «$s'» «$h»)} {a_1 : Q(«$α»)} {s'_1 : Q(Finset «$α»)} {h_1 : Q(«$a_1» ∉ «$s'_1»)}
  {pf_1 : Q(«$s» = Finset.cons «$a_1» «$s'_1» «$h_1»)},
  Mathlib.Meta.Finset.ProveEmptyOrConsResult.cons a s' h pf =
      Mathlib.Meta.Finset.ProveEmptyOrConsResult.cons a_1 s'_1 h_1 pf_1 →
    a = a_1 ∧ s' = s'_1 ∧ h = h_1 ∧ pf = pf_1
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainBialgHomEquiv_apply : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : AddGroup G]
  [inst_3 : AddGroup H] (f : G →+ H), AddMonoidAlgebra.mapDomainBialgHomEquiv f = AddMonoidAlgebra.mapDomainBialgHom R f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpOptions.retriggerCharacters? : Lean.Lsp.SignatureHelpOptions → Option (Array String)
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSES_mor₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact),
  (DerivedCategory.triangleOfSES hS).mor₂ = DerivedCategory.Q.map S.g
-- Std.Data.TreeMap.Iterator
/-- Returns a finite iterator over the entries of a tree map.
The iterator yields the elements of the map in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.TreeMap.iter : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Std.Iter (α × β)
-- Lean.AuxRecursor
Lean.NoConfusionInfo.perCtor.sizeOf_spec : ∀ (arity fields : ℕ), sizeOf (Lean.NoConfusionInfo.perCtor arity fields) = 1 + sizeOf arity + sizeOf fields
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromCols.eq_1 : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R),
  B₁.fromCols B₂ = Matrix.of fun i => Sum.elim (B₁ i) (B₂ i)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂).get k h_mem = m₁.get k ⋯
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The right homology of a short complex,
given by the `H` field of a chosen right homology data.  -/
CategoryTheory.ShortComplex.rightHomology : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (S : CategoryTheory.ShortComplex C) → [S.HasRightHomology] → C
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.coe_eq_algebraMap : ∀ {K : Type u_1} [inst : Field K] (x : NumberField.RingOfIntegers K),
  ↑x = (algebraMap (NumberField.RingOfIntegers K) K) x
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.map_adj₂_counit_app_leftToRight_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful]
  (X : C),
  CategoryTheory.CategoryStruct.comp (F.map (t.adj₂.counit.app X)) (t.leftToRight.app X) = t.adj₁.counit.app (H.obj X)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.modular_T_zpow_smul : ∀ (z : UpperHalfPlane) (n : ℤ), ModularGroup.T ^ n • z = ↑n +ᵥ z
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Ico_iff_integrableOn_Ioo' : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {a b : α},
  μ {a} ≠ ⊤ →
    autoParam (‖f a‖ₑ ≠ ⊤) integrableOn_Ico_iff_integrableOn_Ioo'._auto_1 →
      (MeasureTheory.IntegrableOn f (Set.Ico a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.ker_map : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {f : Polynomial R}
  (self : IsAdjoinRoot S f), RingHom.ker self.map = Ideal.span {f}
-- Mathlib.CategoryTheory.MorphismProperty.IsSmall
CategoryTheory.MorphismProperty.IsSmall.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C},
  Small.{w, max u v} ↑W.toSet → CategoryTheory.MorphismProperty.IsSmall.{w, v, u} W
-- Mathlib.Tactic.LinearCombination
/-- The `(exp := n)` syntax for `linear_combination` says to take the goal to the `n`th power before
subtracting the given combination of hypotheses.
 -/
Mathlib.Tactic.LinearCombination.expStx : Lean.ParserDescr
-- Mathlib.Order.Interval.Finset.Basic
Finset.filter_le_lt_eq_Ico : ∀ {α : Type u_2} (a b : α) [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : Fintype α]
  [inst_3 : DecidablePred fun j => a ≤ j ∧ j < b], {j | a ≤ j ∧ j < b} = Finset.Ico a b
-- Mathlib.Data.Set.Sigma
Set.sigma_univ : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι}, (s.sigma fun x => Set.univ) = Sigma.fst ⁻¹' s
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.algebraMap_apply : ∀ (K : Type u_2) [inst : Field K] (a : K), (algebraMap K (LaurentSeries K)) a = HahnSeries.C a
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- The Frobenius automorphism of `k` induces an endomorphism of `K`. For notation purposes.
Notation `φ(p, k)` in the `Isocrystal` namespace.  -/
Isocrystal.«termφ(_,_)» : Lean.ParserDescr
-- Std.Data.Internal.List.Associative
Std.Internal.List.minEntry?_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.minEntry? (Std.Internal.List.insertEntryIfNew k v l) =
      some
        (match Std.Internal.List.minEntry? l with
        | none => ⟨k, v⟩
        | some e => if compare k e.fst = Ordering.lt then ⟨k, v⟩ else e)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.pow_monotone : ∀ (n : ℕ), Monotone fun f => f ^ n
-- Mathlib.Tactic.ITauto
/-- Convert a value-with-success to an optional value.  -/
Mathlib.Tactic.ITauto.isOk : (Bool × Mathlib.Tactic.ITauto.Proof) × ℕ → Option (Mathlib.Tactic.ITauto.Proof × ℕ)
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.dual_rTensor_conj_homEquiv : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] (A' : Type u_1) [inst_2 : AddCommGroup A']
  {B : Type uB} [inst_3 : AddCommGroup B] [inst_4 : Module R A] [inst_5 : Module R A'] [inst_6 : Module R B]
  (f : A →ₗ[R] A'),
  ↑CharacterModule.homEquiv.symm ∘ₗ CharacterModule.dual (LinearMap.rTensor B f) ∘ₗ ↑CharacterModule.homEquiv =
    LinearMap.lcomp R (CharacterModule B) f
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.tendsto_atTop_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] {u v : α → β}
  {l : Filter α} [OrderTopology β],
  Asymptotics.IsEquivalent l u v → (Filter.Tendsto u l Filter.atTop ↔ Filter.Tendsto v l Filter.atTop)
-- Mathlib.Analysis.Normed.Group.Quotient
/-- Given `f : NormedAddGroupHom M N` such that `f s = 0` for all `s ∈ S`, where,
`S : AddSubgroup M` is closed, the induced morphism `NormedAddGroupHom (M ⧸ S) N`.  -/
NormedAddGroupHom.lift : {M : Type u_1} →
  [inst : SeminormedAddCommGroup M] →
    {N : Type u_3} →
      [inst_1 : SeminormedAddCommGroup N] →
        (S : AddSubgroup M) → (f : NormedAddGroupHom M N) → (∀ s ∈ S, f s = 0) → NormedAddGroupHom (M ⧸ S) N
-- Batteries.Data.List.Lemmas
List.countPBefore_cons_succ_of_pos : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} {i : ℕ} {a : α},
  p a = true → List.countPBefore p (a :: xs) (i + 1) = List.countPBefore p xs i + 1
-- Mathlib.Probability.Distributions.Gaussian.Fernique
/-- Eta-expanded form of `ProbabilityTheory.IsGaussian.memLp_two_id` -/
ProbabilityTheory.IsGaussian.memLp_two_fun_id : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E],
  MeasureTheory.MemLp (fun x => x) 2 μ
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.mk : ∀ {R : Type u_1} {S : Type v₃} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {R' : Type u_6}
  {S' : Type u_7} [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'],
  IsBaseChange S (IsScalarTower.toAlgHom R R' S').toLinearMap → Algebra.IsPushout R S R' S'