mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.inclLeftCompOpEquivInverse_hom_app_op : ∀ (C : Type u₁) {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (d : D),
  (CategoryTheory.Join.inclLeftCompOpEquivInverse C D).hom.app (Opposite.op d) =
    CategoryTheory.CategoryStruct.id (Opposite.op (CategoryTheory.Join.right d))
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.induction_on_adjoin_fg : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  (P : IntermediateField F E → Prop),
  P ⊥ →
    (∀ (K : IntermediateField F E) (x : E), P K → P (IntermediateField.restrictScalars F (↥K)⟮x⟯)) →
      ∀ (K : IntermediateField F E), K.FG → P K
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- If a measure `μ` is the sum of a countable family `mₙ`, and a set `t` has finite measure for
each `mₙ`, then its measurable superset `toMeasurable μ t` (which has the same measure as `t`)
satisfies, for any measurable set `s`, the equality `μ (toMeasurable μ t ∩ s) = μ (t ∩ s)`.  -/
MeasureTheory.Measure.measure_toMeasurable_inter_of_sum : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s →
    ∀ {t : Set α} {m : ℕ → MeasureTheory.Measure α},
      (∀ (n : ℕ), (m n) t ≠ ⊤) → μ = MeasureTheory.Measure.sum m → μ (MeasureTheory.toMeasurable μ t ∩ s) = μ (t ∩ s)
-- Mathlib.RepresentationTheory.Basic
Representation.asModuleEquiv_symm_map_smul : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (r : k) (x : V),
  ρ.asModuleEquiv.symm (r • x) = (algebraMap k (MonoidAlgebra k G)) r • ρ.asModuleEquiv.symm x
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts₁.eq_def : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (x : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.stmts₁ x =
    match x with
    | Q@h:(Turing.TM2.Stmt.push k a q) => insert Q (Turing.TM2.stmts₁ q)
    | Q@h:(Turing.TM2.Stmt.peek k a q) => insert Q (Turing.TM2.stmts₁ q)
    | Q@h:(Turing.TM2.Stmt.pop k a q) => insert Q (Turing.TM2.stmts₁ q)
    | Q@h:(Turing.TM2.Stmt.load a q) => insert Q (Turing.TM2.stmts₁ q)
    | Q@h:(Turing.TM2.Stmt.branch a q₁ q₂) => insert Q (Turing.TM2.stmts₁ q₁ ∪ Turing.TM2.stmts₁ q₂)
    | Q@h:(Turing.TM2.Stmt.goto a) => {Q}
    | Q@h:Turing.TM2.Stmt.halt => {Q}
-- Mathlib.Algebra.Order.Group.CompleteLattice
ciInf_div : ∀ {ι : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
  [MulRightMono G], BddBelow (Set.range f) → ∀ (a : G), (⨅ i, f i) / a = ⨅ i, f i / a
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The colimits of `F : J ⥤ C` and `G : J ⥤ C` are isomorphic,
if the functors are naturally isomorphic.
 -/
CategoryTheory.Limits.HasColimit.isoOfNatIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F G : CategoryTheory.Functor J C} →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            [inst_3 : CategoryTheory.Limits.HasColimit G] →
              (F ≅ G) → (CategoryTheory.Limits.colimit F ≅ CategoryTheory.Limits.colimit G)
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_summable_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸],
  ∀ x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius, Summable fun n => (NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.CommShift₂Setup.int_z : ∀ {D : Type u_5} [inst : CategoryTheory.Category.{v_5, u_5} D] [inst_1 : CategoryTheory.Preadditive D]
  [inst_2 : CategoryTheory.HasShift D ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] (m n : ℤ × ℤ),
  CategoryTheory.CommShift₂Setup.int.z m n = (-1) ^ (m.1 * n.2)
-- Mathlib.AlgebraicGeometry.SpreadingOut
AlgebraicGeometry.instIsGermInjectiveOfIsIntegral : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X], X.IsGermInjective
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Bundle.Pretrivialization.continuousOn_continuousAlternatingMapCoordChange : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] {B : Type u_3} [inst_1 : TopologicalSpace B]
  {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_5}
  [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜 (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₁ x)] [inst_13 : FiberBundle F₁ E₁]
  [inst_14 : (x : B) → TopologicalSpace (E₂ x)] [inst_15 : FiberBundle F₂ E₂]
  {e₁ e₁' : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ e₂' : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [Finite ι] [inst_17 : VectorBundle 𝕜 F₁ E₁] [inst_18 : VectorBundle 𝕜 F₂ E₂] [inst_19 : MemTrivializationAtlas e₁]
  [inst_20 : MemTrivializationAtlas e₁'] [inst_21 : MemTrivializationAtlas e₂] [inst_22 : MemTrivializationAtlas e₂'],
  ContinuousOn (Bundle.Pretrivialization.continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.toMonoidHom.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N), f.toMonoidHom = { toFun := f.toFun, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.GroupTheory.Torsion
/-- A module with a finite ring of scalars is torsion.  -/
IsAddTorsion.module_of_finite : ∀ (R : Type u_3) (M : Type u_4) [inst : AddCommMonoid M] [inst_1 : Ring R] [Finite R] [Module R M], IsAddTorsion M
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.isSome_succMany?_of_lt_size_toArray : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {i : ℕ}, i < r.toArray.size → (Std.PRange.succMany? i r.lower).isSome = true
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- A finite affine combination of covariant derivatives is a covariant derivative.  -/
IsCovariantDerivativeOn.finite_affine_combination : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] {ι : Type u_7} {s : Finset ι} {u : Set M}
  {cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x},
  (∀ (i : ι), IsCovariantDerivativeOn F (cov i) u) →
    ∀ {f : ι → M → 𝕜}, ∑ i ∈ s, f i = 1 → IsCovariantDerivativeOn F (fun σ x => ∑ i ∈ s, f i x • cov i σ x) u
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_maxKey?_of_isSome_maxKey?_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, (Std.DTreeMap.Internal.Impl.erase! k t).maxKey?.isSome = true → t.maxKey?.isSome = true
-- Mathlib.Analysis.Convolution
MeasureTheory.convolution_integrand_bound_right_of_le_of_subset : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : AddGroup G] [inst_8 : TopologicalSpace G] {C : ℝ},
  (∀ (i : G), ‖g i‖ ≤ C) →
    ∀ {x t : G} {s u : Set G},
      x ∈ s → -tsupport g + s ⊆ u → ‖(L (f t)) (g (x - t))‖ ≤ u.indicator (fun t => ‖L‖ * ‖f t‖ * C) t
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_toArray_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, (k, v) ∈ m.toArray ↔ m.getKey? k = some k ∧ m[k]? = some v
-- Mathlib.Order.Filter.Extr
IsMaxFilter.add : ∀ {α : Type u} {β : Type v} [inst : AddCommMonoid β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f g : α → β}
  {a : α} {l : Filter α}, IsMaxFilter f l a → IsMaxFilter g l a → IsMaxFilter (fun x => f x + g x) l a
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Relation.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} [inst_1 : SizeOf C] {fst snd : S.Arrow} (r : fst.Relation snd),
  sizeOf { fst := fst, snd := snd, r := r } = 1 + sizeOf fst + sizeOf snd + sizeOf r
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
ConditionallyCompleteLinearOrder.toOrd : {α : Type u_5} → [self : ConditionallyCompleteLinearOrder α] → Ord α
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- Let `t i` be a countable covering of a set `T` by measurable sets. Let `f i : t i → β` be a
family of functions that agree on the intersections `t i ∩ t j`. Then the function
`Set.iUnionLift t f _ _ : T → β`, defined as `f i ⟨x, hx⟩` for `hx : x ∈ t i`, is measurable.  -/
measurable_iUnionLift : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort uι} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι]
  {t : ι → Set α} {f : (i : ι) → ↑(t i) → β}
  (htf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) {T : Set α}
  (hT : T ⊆ ⋃ i, t i),
  (∀ (i : ι), MeasurableSet (t i)) → (∀ (i : ι), Measurable (f i)) → Measurable (Set.iUnionLift t f htf T hT)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
/-- Extract a single bit in position `start` in `target` and extend it to have width `w` -/
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendBit : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget aig w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instCommSemigroup : {M : Type u_1} →
  [inst : TopologicalSpace M] → [inst_1 : CommSemigroup M] → [ContinuousMul M] → CommSemigroup (SeparationQuotient M)
-- Std.Sync.Broadcast
/-- Creates a new `Bounded` channel.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.new : {α : Type} → (capacity : optParam ℕ 16) → autoParam (capacity > 0) Std.Bounded.new._auto_1✝ → BaseIO (Std.Bounded✝ α)
-- Mathlib.Topology.Defs.Induced
Topology.isInducing_iff : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y),
  Topology.IsInducing f ↔ tX = TopologicalSpace.induced f tY
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.Core.mk.injEq : ∀ {α : Type u} (uniformity : Filter (α × α)) (refl : Filter.principal SetRel.id ≤ uniformity)
  (symm : Filter.Tendsto Prod.swap uniformity uniformity)
  (comp : (uniformity.lift' fun s => SetRel.comp s s) ≤ uniformity) (uniformity_1 : Filter (α × α))
  (refl_1 : Filter.principal SetRel.id ≤ uniformity_1) (symm_1 : Filter.Tendsto Prod.swap uniformity_1 uniformity_1)
  (comp_1 : (uniformity_1.lift' fun s => SetRel.comp s s) ≤ uniformity_1),
  ({ uniformity := uniformity, refl := refl, symm := symm, comp := comp } =
      { uniformity := uniformity_1, refl := refl_1, symm := symm_1, comp := comp_1 }) =
    (uniformity = uniformity_1)
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Precomposition of functions into a topological semiring by a continuous map is an algebra
homomorphism.  -/
ContinuousMap.compRightAlgHom : (R : Type u_2) →
  [inst : CommSemiring R] →
    (A : Type u_3) →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : Semiring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : IsTopologicalSemiring A] →
              {α : Type u_5} →
                {β : Type u_6} →
                  [inst_5 : TopologicalSpace α] → [inst_6 : TopologicalSpace β] → C(α, β) → C(β, A) →ₐ[R] C(α, A)
-- Init.PropLemmas
exists_true_left : ∀ {p : True → Prop}, Exists p ↔ p True.intro
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_le_size_insert : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, m.size ≤ (m.insert k).size
-- Std.Data.DTreeMap.Internal.Operations
/-- Returns the tree `l ++ ⟨k, v⟩ ++ r`, with the smallest element chopped off.  -/
Std.DTreeMap.Internal.Impl.minView : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        (l r : Std.DTreeMap.Internal.Impl α β) →
          l.Balanced →
            r.Balanced →
              Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size →
                Std.DTreeMap.Internal.Impl.View α β (l.size + r.size)
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- If we interchange the roles of `M` and `N`, we still have a root pairing.  -/
RootPairing.flip : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → RootPairing ι R N M
-- Init.Data.Slice.List.Lemmas
ListSlice.toList_mkSlice_roi_eq_toList_mkSlice_rco : ∀ {α : Type u_1} {xs : ListSlice α} {lo : ℕ},
  Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) =
    Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs (lo + 1)...Std.Slice.size xs)
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.instLinearComp : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Linear R F] {E : Type u_4}
  [inst_8 : CategoryTheory.Category.{v_3, u_4} E] [inst_9 : CategoryTheory.Preadditive E]
  [inst_10 : CategoryTheory.Linear R E] (G : CategoryTheory.Functor D E) [CategoryTheory.Functor.Linear R G],
  CategoryTheory.Functor.Linear R (F.comp G)
-- Init.Data.Nat.Gcd
Nat.gcd_self_sub_right : ∀ {m n : ℕ}, n ≤ m → m.gcd (m - n) = m.gcd n
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_ofClass : ∀ {S : Type u_3} {G : Type u_4} [inst : Group G] [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] (s : S),
  ↑(Subgroup.ofClass s) = ↑s
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.brecOn.go : {L : FirstOrder.Language} →
  {α : Type u'} →
    {motive : (a : ℕ) → L.BoundedFormula α a → Sort u_1} →
      {a : ℕ} →
        (t : L.BoundedFormula α a) →
          ((a : ℕ) → (t : L.BoundedFormula α a) → FirstOrder.Language.BoundedFormula.below t → motive a t) →
            motive a t ×' FirstOrder.Language.BoundedFormula.below t
-- Lean.Elab.MutualInductive
/-- The constructors produced by `InductiveElabStep1`.  -/
Lean.Elab.Command.InductiveElabStep2.ctors : Lean.Elab.Command.InductiveElabStep2 → List Lean.Constructor
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.instInitiallySmallOfHasInitial : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasInitial J],
  CategoryTheory.InitiallySmall J
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.aestronglyMeasurable_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {b : β}, MeasureTheory.AEStronglyMeasurable (fun x => b) μ
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_eq_fun : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] [MeasurableEq β] {f g : α → β},
  Measurable f → Measurable g → MeasurableSet {x | f x = g x}
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ModuleHierarchy.mk.injEq : ∀ (item : Lean.Lsp.LeanImport) (children : Array Lean.Lsp.Ipc.ModuleHierarchy) (item_1 : Lean.Lsp.LeanImport)
  (children_1 : Array Lean.Lsp.Ipc.ModuleHierarchy),
  ({ item := item, children := children } = { item := item_1, children := children_1 }) =
    (item = item_1 ∧ children = children_1)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_mul : ∀ (S : Type u) [inst : Semiring S] (n m : ℕ),
  ascPochhammer S n * (ascPochhammer S m).comp (Polynomial.X + ↑n) = ascPochhammer S (n + m)
-- Init.Prelude
String.Pos.Raw.mk : ℕ → String.Pos.Raw
-- Lean.Meta.Match.CaseArraySizes
Lean.Meta.CaseArraySizesSubgoal.subst : Lean.Meta.CaseArraySizesSubgoal → Lean.Meta.FVarSubst
-- Mathlib.Tactic.ReduceModChar
Tactic.ReduceModChar.instInhabitedTypeToCharPResult : {u : Lean.Level} → {α : Q(Type u)} → Inhabited (Tactic.ReduceModChar.TypeToCharPResult α)
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.norm_map_cons_le : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) (x : Ei 0)
  (m : (i : Fin n) → Ei i.succ), ‖f (Fin.cons x m)‖ ≤ ‖f‖ * ‖x‖ * ∏ i, ‖m i‖
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.homologyπ_singleObjHomologySelfIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).homologyπ j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).hom h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).hom h
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Colorable.cliqueFree : ∀ {V : Type u} {G : SimpleGraph V} {n m : ℕ}, G.Colorable n → n < m → G.CliqueFree m
-- Mathlib.Topology.Order.IntermediateValue
isConnected_Ico : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α}, a < b → IsConnected (Set.Ico a b)
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.degree_quadratic : ∀ {R : Type u} {a b c : R} [inst : Semiring R],
  a ≠ 0 → (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree = 2
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- The composition of Lipschitz functions is Lipschitz.  -/
LipschitzWith.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {Kf Kg : NNReal} {f : β → γ} {g : α → β},
  LipschitzWith Kf f → LipschitzWith Kg g → LipschitzWith (Kf * Kg) (f ∘ g)
-- Init.Data.Range.Polymorphic.Nat
Std.instLawfulRcoIntersectionNat_1 : Std.Roc.LawfulRcoIntersection ℕ
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIic_of_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {b x : α} (hx : x ∈ Set.Iic b), Set.projIic b x = ⟨x, hx⟩
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_bitVecToNat : ∀ (n : BitVec 8), UInt8.ofNatLT n.toNat ⋯ = { toBitVec := n }
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- The composition in the opposite direction is equal to the identity if and only if `F` preserves
the biproduct, see `preservesBinaryBiproduct_of_monoBiprodComparison`.  -/
CategoryTheory.Functor.biprodComparison'_comp_biprodComparison_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] {Z : D}
  (h : F.obj X ⊞ F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.biprodComparison' X Y)
      (CategoryTheory.CategoryStruct.comp (F.biprodComparison X Y) h) =
    h
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isBot.inj : ∀ {idx idx_1 : ℕ}, Mathlib.Tactic.Order.AtomicFact.isBot idx = Mathlib.Tactic.Order.AtomicFact.isBot idx_1 → idx = idx_1
-- Mathlib.RingTheory.IsTensorProduct
/-- If `N` is the base change `M` to `S`, then `O` is the base change of `M` to `T` if and
only if `O` is the base change of `N` to `T`.  -/
IsBaseChange.comp_iff : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {T : Type u_4} {O : Type u_5} [inst_9 : CommSemiring T]
  [inst_10 : Algebra R T] [inst_11 : Algebra S T] [IsScalarTower R S T] [inst_13 : AddCommMonoid O]
  [inst_14 : Module R O] [inst_15 : Module S O] [inst_16 : Module T O] [inst_17 : IsScalarTower S T O]
  [inst_18 : IsScalarTower R S O] [inst_19 : IsScalarTower R T O] {f : M →ₗ[R] N},
  IsBaseChange S f → ∀ {h : N →ₗ[S] O}, IsBaseChange T (↑R h ∘ₗ f) ↔ IsBaseChange T h
-- Lean.Server.Completion.EligibleHeaderDecls
Lean.Server.Completion.EligibleDecl.mk.injEq : ∀ (info : Lean.ConstantInfo) (kind : Lean.MetaM Lean.Lsp.CompletionItemKind)
  (tags : Lean.MetaM (Array Lean.Lsp.CompletionItemTag)) (info_1 : Lean.ConstantInfo)
  (kind_1 : Lean.MetaM Lean.Lsp.CompletionItemKind) (tags_1 : Lean.MetaM (Array Lean.Lsp.CompletionItemTag)),
  ({ info := info, kind := kind, tags := tags } = { info := info_1, kind := kind_1, tags := tags_1 }) =
    (info = info_1 ∧ kind = kind_1 ∧ tags = tags_1)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mk_surjective : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {S : T} (X : CategoryTheory.Over S),
  ∃ Y f, CategoryTheory.Over.mk f = X
-- Lean.MonadEnv
Lean.setEnv : {m : Type → Type} → [Lean.MonadEnv m] → Lean.Environment → m Unit
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
Homeomorph.toOpenPartialHomeomorphOfImageEq_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X)
  (hs : IsOpen s) (t : Set Y) (h : ⇑e '' s = t), (e.toOpenPartialHomeomorphOfImageEq s hs t h).source = s
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.lift'_add : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M''] [inst_3 : Module R M] [inst_4 : Module R M''] (g : M →ₗ[R] M'')
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (x y : LocalizedModule S M),
  LocalizedModule.lift' S g h (x + y) = LocalizedModule.lift' S g h x + LocalizedModule.lift' S g h y
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.faceι_ι : ∀ {n : ℕ} (i j : Fin (n + 1)) (hij : j ≠ i),
  CategoryTheory.CategoryStruct.comp (SSet.horn.faceι i j hij) (SSet.horn n i).ι = (SSet.stdSimplex.face {j}ᶜ).ι
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.any_eq_anyTR.go : ∀ (m n : ℕ) (f : (i : ℕ) → i < m + n → Bool),
  (m + n).any f = ((n.any fun i h => f i ⋯) || Nat.anyTR.loop✝ (m + n) f m ⋯)