mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.ext_getVert : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v}, (∀ (k : ℕ), p.getVert k = q.getVert k) → p = q
-- Mathlib.Data.ZMod.Basic
/-- In `ZMod (p ^ d)` with `0 < d`, the prime `p` is not a unit.  -/
ZMod.prime_natCast_not_isUnit_pow : ∀ {p d : ℕ}, Nat.Prime p → 0 < d → ¬IsUnit ↑p
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- In a topological group, if the neighborhoods of zero are defined by a valuation `v` compatible
with the valuative relation, then the underlying topology is valuative.  -/
IsValuativeTopology.of_mem_nhds_zero_iff_vle : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_3 : TopologicalSpace R] (v : Valuation R Γ₀) [v.Compatible] [IsTopologicalAddGroup R],
  (∀ {s : Set R}, s ∈ nhds 0 ↔ ∃ γ, {z | v.restrict z < ↑γ} ⊆ s) → IsValuativeTopology R
-- Std.Http.Data.URI.Basic
Std.Http.URI.instBEqPath.beq : Std.Http.URI.Path → Std.Http.URI.Path → Bool
-- Mathlib.Data.Int.Bitwise
Int.div2_val : ∀ (n : ℤ), n.div2 = n / 2
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The 1-morphism `h` commutes with the left Kan lift `f₊ g`.  -/
CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : b ⟶ a) →
        (g : c ⟶ a) →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] →
            {x : B} →
              (h : x ⟶ c) →
                [inst_2 : CategoryTheory.Bicategory.LanLift.CommuteWith f g h] →
                  CategoryTheory.Bicategory.lanLift f (CategoryTheory.CategoryStruct.comp h g) ≅
                    CategoryTheory.CategoryStruct.comp h (CategoryTheory.Bicategory.lanLift f g)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- The image of `ExteriorAlgebra.ιMulti R n` is contained in the `n`th exterior power.  -/
ExteriorAlgebra.ιMulti_range : ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ),
  Set.range ⇑(ExteriorAlgebra.ιMulti R n) ⊆ ↑(⋀[R]^n M)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
StronglyMeasurable.apply_continuousLinearMap : ∀ {α : Type u_1} {𝕜 : Type u_4} [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_6} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {_m : MeasurableSpace α} {φ : α → F →L[𝕜] E},
  MeasureTheory.StronglyMeasurable φ → ∀ (v : F), MeasureTheory.StronglyMeasurable fun a => (φ a) v
-- Mathlib.Tactic.Linter.Header
/-- Return if `line` looks like a correct authors line in a copyright header.

The `offset` input is used to shift the position information of the `Syntax` that the command
produces.
`authorsLineChecks` computes a position for its warning *relative to `line`*.
The `offset` input passes on the starting position of `line` in the whole file.
 -/
_private.Mathlib.Tactic.Linter.Header.0.Mathlib.Linter.authorsLineChecks : String → String.Pos.Raw → Array (Lean.Syntax × String)
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.tactic.parenthesizer : Lean.PrettyPrinter.CategoryParenthesizer
-- Mathlib.GroupTheory.Coset.Basic
RightAddCosetEquivalence.eq_1 : ∀ {α : Type u_1} [inst : Add α] (s : Set α) (a b : α),
  RightAddCosetEquivalence s a b = (AddOpposite.op a +ᵥ s = AddOpposite.op b +ᵥ s)
-- Mathlib.Analysis.Convex.AmpleSet
/-- Let `E` be a linear subspace in a real vector space.
If `E` has codimension at least two, its complement is ample.  -/
AmpleSet.of_one_lt_codim : ∀ {F : Type u_1} [inst : AddCommGroup F] [inst_1 : Module ℝ F] [inst_2 : TopologicalSpace F] [IsTopologicalAddGroup F]
  [ContinuousSMul ℝ F] {E : Submodule ℝ F}, 1 < Module.rank ℝ (F ⧸ E) → AmpleSet (↑E)ᶜ
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.add`. -/
MeasureTheory.ProgMeasurable.add : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u v : ι → Ω → β} [inst_2 : MeasurableSpace ι] [inst_3 : Add β]
  [ContinuousAdd β],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStronglyProgressive f v → MeasureTheory.IsStronglyProgressive f fun i ω => u i ω + v i ω
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.copy_eq : ∀ {R : Type u_1} [inst : CommRing R] (P : RingPreordering R) (S : Set R) (hS : S = ↑P), ↑(P.copy S hS) = S
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
NonarchimedeanRing.is_nonarchimedean : ∀ {R : Type u_1} {inst : Ring R} {inst_1 : TopologicalSpace R} [self : NonarchimedeanRing R], ∀ U ∈ nhds 0, ∃ V, ↑V ⊆ U
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.hasIntegral_zero : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.HasIntegral I l (fun x => 0) vol 0
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.l_biInf_of_u_l_eq_self : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisInsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → α),
  (∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi) → l (⨅ i, ⨅ (hi : p i), f i hi) = ⨅ i, ⨅ (hi : p i), l (f i hi)
-- Mathlib.Order.Completion
DedekindCut.coe_principalEmbedding : ∀ {α : Type u_1} [inst : PartialOrder α], ⇑DedekindCut.principalEmbedding = DedekindCut.principal
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.instIsInducedComp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₃ : CategoryTheory.MorphismProperty C₃} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (Ψ : CategoryTheory.LocalizerMorphism W₂ W₃) [Φ.IsInduced] [Ψ.IsInduced], (Φ.comp Ψ).IsInduced
-- Mathlib.Topology.Constructions.SumProd
continuous_curry : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {g : X × Y → Z} (x : X), Continuous g → Continuous (Function.curry g x)
-- Init.Data.UInt.Bitwise
UInt16.toUInt8_shiftLeft : ∀ (a b : UInt16), b < 8 → (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Interpret an `Equiv` as a `PartialEquiv` by restricting it to `s` in the domain
and to `t` in the codomain.  -/
Equiv.toPartialEquivOfImageEq : {α : Type u_1} → {β : Type u_2} → (e : α ≃ β) → (s : Set α) → (t : Set β) → ⇑e '' s = t → PartialEquiv α β
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.toMulEquiv : {G : Type u} →
  [inst : TopologicalSpace G] →
    {H : Type v} → [inst_1 : TopologicalSpace H] → [inst_2 : Mul G] → [inst_3 : Mul H] → G ≃ₜ* H → G ≃* H
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {f : E → ContinuousMultilinearMap 𝕜 G H} {f' : E →L[𝕜] ContinuousMultilinearMap 𝕜 G H}
  {g : (i : ι) → E → F i →L[𝕜] G i} {g' : (i : ι) → E →L[𝕜] F i →L[𝕜] G i} {x : E} [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι],
  HasFDerivAt f f' x →
    (∀ (i : ι), HasFDerivAt (g i) (g' i) x) →
      HasFDerivAt (fun x => (f x).compContinuousLinearMap fun x_1 => g x_1 x)
        ((ContinuousMultilinearMap.compContinuousLinearMapL fun x_1 => g x_1 x) ∘SL f' +
          ((f x).fderivCompContinuousLinearMap fun x_1 => g x_1 x) ∘SL ContinuousLinearMap.pi g')
        x
-- Mathlib.Analysis.Convolution
MeasureTheory.AEStronglyMeasurable.convolution_integrand : ∀ {𝕜 : 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 : MeasurableSpace G] {μ ν : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] [MeasureTheory.SFinite ν],
  MeasureTheory.AEStronglyMeasurable f ν →
    MeasureTheory.AEStronglyMeasurable g μ →
      MeasureTheory.AEStronglyMeasurable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
-- Mathlib.Algebra.Group.TypeTags.Basic
isAddLeftRegular_ofMul : ∀ {α : Type u} [inst : Monoid α] {a : α}, IsAddLeftRegular (Additive.ofMul a) ↔ IsLeftRegular a
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensor_right_unitality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₁).hom
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₂).hom))
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.Quotient.addCommGroup : {G : Type u_5} → [inst : AddCommGroup G] → (N : AddSubgroup G) → AddCommGroup (G ⧸ N)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.closedBall_mem_nhds : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α) {ε : ℝ}, 0 < ε → Metric.closedBall x ε ∈ nhds x
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.pair : Nat.Partrec.Code → Nat.Partrec.Code → Nat.Partrec.Code
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.imp_1eq_certC.eq_1 : ∀ (lhs rhs : Lean.Grind.CommRing.Expr) (p₁ p₂ : Lean.Grind.CommRing.Poly) (c : ℕ),
  Lean.Grind.CommRing.Stepwise.imp_1eq_certC lhs rhs p₁ p₂ c =
    (((lhs.sub rhs).toPolyC c).beq' p₁).and' (p₂.beq' (Lean.Grind.CommRing.Poly.num 0))
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
IsIntegral.mem_intermediateField_of_minpoly_splits : ∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  IsIntegral K x → ∀ {F : IntermediateField K L}, (Polynomial.map (algebraMap K ↥F) (minpoly K x)).Splits → x ∈ F
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Mon.sharesVar.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.eq) (h_2 : Unit → motive Ordering.lt)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.gt with
    | Ordering.eq => h_1 ()
    | Ordering.lt => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_3 ()
-- Lean.Data.KVMap
Lean.DataValue.ofBool.inj : ∀ {v v_1 : Bool}, Lean.DataValue.ofBool v = Lean.DataValue.ofBool v_1 → v = v_1
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.ConeMorphism.ext_iff : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} {f g : c ⟶ c'}, f = g ↔ f.hom = g.hom
-- Std.Internal.Do.WP.Basic
/-- `ReaderT`'s `WP` interpretation: lift the base interpretation by adding a reader argument.  -/
Std.Internal.Do.ReaderT.wpInst : {m : Type u → Type z} →
  {EPred : Type u_1} →
    {α ρ : Type u} →
      {Pred : Type v} →
        [inst : Std.Internal.Do.Assertion Pred] →
          [inst_1 : Std.Internal.Do.Assertion EPred] →
            [Std.Internal.Do.WP (m α) α Pred EPred] → Std.Internal.Do.WP (ReaderT ρ m α) α (ρ → Pred) EPred
-- Mathlib.Tactic.Widget.StringDiagram
/-- Strings in a string diagram.  -/
Mathlib.Tactic.Widget.StringDiagram.Strand : Type
-- Mathlib.FieldTheory.IntermediateField.Algebraic
/-- Turn an algebraic subalgebra into an intermediate field, `Subalgebra.IsAlgebraic` version.  -/
Subalgebra.IsAlgebraic.toIntermediateField : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] → [inst_2 : Algebra K L] → {S : Subalgebra K L} → S.IsAlgebraic → IntermediateField K L
-- Mathlib.NumberTheory.FermatPsp
/-- `n` is a Fermat pseudoprime to base `b` if `n` is a probable prime to base `b` and is composite. By
this definition, all composite natural numbers are pseudoprimes to base 0 and 1. This definition
also permits `n` to be less than `b`, so that 4 is a pseudoprime to base 5, for example.
 -/
Nat.FermatPsp : ℕ → ℕ → Prop
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_sub' : ∀ {y z : ℝ}, y - z ≠ 0 → ∀ (x : NNReal), x ^ (y - z) = x ^ y / x ^ z
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.map_comap_eq : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (f : L →ₐ[K] L') (S : IntermediateField K L'),
  IntermediateField.map f (IntermediateField.comap f S) = S ⊓ f.fieldRange
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.core.sizeOf_spec : ∀ (e : Lean.Expr) (lhs rhs : Lean.Grind.CommRing.Expr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.core e lhs rhs) = 1 + sizeOf e + sizeOf lhs + sizeOf rhs
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.done.injEq : ∀ (goal goal_1 : Lean.Meta.Grind.Goal),
  (Lean.Meta.Grind.IntroResult.done✝ goal = Lean.Meta.Grind.IntroResult.done✝ goal_1) = (goal = goal_1)
-- Mathlib.Data.Fin.SuccPred
Fin.eq_castSucc_or_eq_last : ∀ {n : ℕ} (i : Fin (n + 1)), (∃ j, i = j.castSucc) ∨ i = Fin.last n
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Turn an element of a type `F` satisfying `OrderHomClass F α β` and `MonoidHomClass F α β`
into an actual `OrderMonoidHom`. This is declared as the default coercion from `F` to `α →*o β`.  -/
OrderMonoidHomClass.toOrderMonoidHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : MulOneClass α] →
            [inst_3 : MulOneClass β] →
              [inst_4 : FunLike F α β] → [OrderHomClass F α β] → [MonoidHomClass F α β] → F → α →*o β
-- Mathlib.Data.Set.Insert
/-- **Alias** of `Set.ofPred_mem_list_eq_singleton_of_nodup`. -/
Set.setOf_mem_list_eq_singleton_of_nodup : ∀ {α : Type u_1} {l : List α}, l.Nodup → ∀ {a : α}, {x | x ∈ l} = {a} ↔ l = [a]
-- Mathlib.RingTheory.Etale.Weakly
/-- [Stacks Tag 092N](https://stacks.math.columbia.edu/tag/092N) ((2)) -/
Algebra.WeaklyEtale.instOfEtale : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Algebra.Etale R S],
  Algebra.WeaklyEtale R S
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- The `n`th monomial as multivariate formal power series:
it is defined as the `R`-linear map from `R` to the semiring
of multivariate formal power series associating to each `a`
the map sending `n : σ →₀ ℕ` to the value `a`
and sending all other `x : σ →₀ ℕ` different from `n` to `0`.  -/
MvPowerSeries.monomial : {σ : Type u_1} → {R : Type u_2} → [inst : Semiring R] → (σ →₀ ℕ) → R →ₗ[R] MvPowerSeries σ R
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_hom_assoc : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.uncurry.obj F)]
  [inst_5 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] {j : J} {k : K} {Z : C}
  (h : CategoryTheory.Limits.colimit (F.comp CategoryTheory.Limits.colim) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.uncurry.obj F) (j, k))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j) h)
-- Lean.Meta.AppBuilder
/-- Returns `a op b`, where `op` has name `opName` and is implemented using the typeclass `className`.
This method assumes `a` and `b` have the same type, and typeclass `className` is heterogeneous.
Examples of supported classes: `HAdd`, `HSub`, `HMul`.
We use heterogeneous operators to ensure we have a uniform representation.
 -/
_private.Lean.Meta.AppBuilder.0.Lean.Meta.mkBinaryOp : Lean.Name → Lean.Name → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Batteries.Lean.Expr
/-- Auxiliary definition for `withAppRev'`.  -/
Lean.Expr.withAppRev'.go : {α : Sort u_1} → (Lean.Expr → Array Lean.Expr → α) → Lean.Expr → Array Lean.Expr → α
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instMulZeroOneClass : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [MulZeroOneClass Y] → MulZeroOneClass (LocallyConstant X Y)
-- Mathlib.Data.List.Lattice
List.nil_bagInter : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), [].bagInter l = []
-- Mathlib.Data.Set.Lattice.Image
Set.iInter_union_iInter : ∀ {α : Type u_1} {ι : Sort u_9} {κ : Sort u_10} (f : ι → Set α) (g : κ → Set α),
  (⋂ i, f i) ∪ ⋂ j, g j = ⋂ i, ⋂ j, f i ∪ g j
-- Mathlib.Order.CountableDenseLinearOrder
Order.instPreorderPartialIso : (α : Type u_1) → (β : Type u_2) → [inst : LinearOrder α] → [inst_1 : LinearOrder β] → Preorder (Order.PartialIso α β)
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.leCnstr? : Lean.Expr → Lean.Meta.Simp.Arith.Int.ToLinear.M (Option (Int.Internal.Linear.Expr × Int.Internal.Linear.Expr))
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.lt_iff : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {L₁ L₂ : IntermediateField.Lifts F E K},
  L₁ < L₂ ↔ ∃ (h : L₁.carrier < L₂.carrier), L₂.emb.comp (IntermediateField.inclusion ⋯) = L₁.emb
-- Mathlib.NumberTheory.Padics.PadicNumbers
AddValuation.of.congr_simp : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (f f_1 : R → Γ₀)
  (e_f : f = f_1) (h0 : f 0 = ⊤) (h1 : f 1 = 0) (hadd : ∀ (x y : R), min (f x) (f y) ≤ f (x + y))
  (hmul : ∀ (x y : R), f (x * y) = f x + f y), AddValuation.of f h0 h1 hadd hmul = AddValuation.of f_1 ⋯ ⋯ ⋯ ⋯
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_smul : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (r : R) (f : N →ₗ[R] P), LinearMap.lTensor M (r • f) = r • LinearMap.lTensor M f
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.map_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  {x : X}, x ∈ e.source → ↑e x ∈ e.target
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.insert_eq_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {p : (a : α) × β a}, insert p m = m.insert p.fst p.snd
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.extend_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A) (η : A ⟶ B) [inst_1 : CategoryTheory.IsIso η],
  (P.extend η).F = P.F
-- Mathlib.Data.NNReal.Defs
NNReal.bddAbove_coe : ∀ {s : Set NNReal}, BddAbove (NNReal.toReal '' s) ↔ BddAbove s
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.minFacHelper_0 : ∀ (n : ℕ), Nat.ble 2 n = true → 1 = n % 2 → Mathlib.Meta.NormNum.MinFacHelper n 3
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.homAddEquiv_symm_apply_hom : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (f : ↑M →ₗ[R] ↑N),
  ModuleCat.Hom.hom (ModuleCat.homAddEquiv.symm f) = f
-- Mathlib.Analysis.Normed.Module.Bases
/-- A generalized Schauder basis indexed by `β` with summation along filter `L`.

The key fields are:
* `basis`: The basis vectors `e i` for `i : β`
* `coord`: The coordinate functionals `f i` for `i : β` in the dual space
* `ortho`: Biorthogonality condition `f i (e j) = if i = j then 1 else 0`
* `expansion`: Every `x` equals `∑ i, f i x • e i`, converging along `L`

See `SchauderBasis` for the classical `ℕ`-indexed case with conditional convergence,
and `UnconditionalSchauderBasis` for the unconditional case.
 -/
GeneralSchauderBasis : (β : Type u_3) →
  (𝕜 : Type u_4) →
    (X : Type u_5) →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup X] → [NormedSpace 𝕜 X] → SummationFilter β → Type (max (max u_3 u_4) u_5)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inrHom_injective : ∀ {S : Type u_2} {R : Type u_3} {A : Type u_4} [inst : Semiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid A]
  [inst_3 : Module S R] [inst_4 : Module S A], Function.Injective ⇑(Unitization.inrHom S R A)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone.snd : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → (self : CategoryTheory.Limits.BinaryBicone P Q) → self.pt ⟶ Q
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.map_toComp_ker : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_3} {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι),
  Ideal.map (Q.toComp P).toAlgHom P.ker = RingHom.ker (Q.ofComp P).toAlgHom
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.instIsClosedUnderIsomorphismsPlus : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), t.plus.IsClosedUnderIsomorphisms