mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Relation
Relation.ReflTransGen.swap : ∀ {α : Type u_1} {r : α → α → Prop}, Function.swap (Relation.ReflTransGen r) ≤ Relation.ReflTransGen (Function.swap r)
-- Lean.Data.Lsp.Client
Lean.Lsp.instToJsonRegistration.toJson : Lean.Lsp.Registration → Lean.Json
-- Init.Data.Nat.Lemmas
Nat.min_self : ∀ (a : ℕ), min a a = a
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.lcm_zero_right : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (x : R), EuclideanDomain.lcm x 0 = 0
-- Lean.Expr
Lean.Expr.isStringLit : Lean.Expr → Bool
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- We say that a valuative relation on a ring is *nontrivial* if the
value group-with-zero is nontrivial, meaning that it has an element
which is different from 0 and 1.  -/
ValuativeRel.IsNontrivial : (R : Type u_1) → [inst : Semiring R] → [ValuativeRel R] → Prop
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_indicator_comm' : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι] [inst_2 : Zero β] {s : Set Ω},
  MeasureTheory.stoppedProcess (fun i => s.indicator (u i)) τ = fun i =>
    s.indicator (MeasureTheory.stoppedProcess u τ i)
-- Batteries.Data.Random.MersenneTwister
Batteries.Random.MersenneTwister.Config.zero_lt_wordSize : ∀ (cfg : Batteries.Random.MersenneTwister.Config), 0 < cfg.wordSize
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- Given two restricted products of rings `Πʳ (i : ι₁), [R₁ i, B₁ i]_[𝓕₁]` and
`Πʳ (j : ι₂), [R₂ j, B₂ j]_[𝓕₂]`, `RestrictedProduct.mapAlongRingHom` gives a
ring homomorphism between them. The data needed is a
function `f : ι₂ → ι₁` such that `𝓕₂` tends to `𝓕₁` along `f`, and ring homomorphisms
`φ j : R₁ (f j) → R₂ j` sending `B₁ (f j)` into `B₂ j` for an `𝓕₂`-large set of `j`'s.
 -/
RestrictedProduct.mapAlongRingHom : {ι₁ : Type u_3} →
  {ι₂ : Type u_4} →
    (R₁ : ι₁ → Type u_5) →
      (R₂ : ι₂ → Type u_6) →
        {𝓕₁ : Filter ι₁} →
          {𝓕₂ : Filter ι₂} →
            {S₁ : ι₁ → Type u_7} →
              {S₂ : ι₂ → Type u_8} →
                [inst : (i : ι₁) → SetLike (S₁ i) (R₁ i)] →
                  [inst_1 : (j : ι₂) → SetLike (S₂ j) (R₂ j)] →
                    {B₁ : (i : ι₁) → S₁ i} →
                      {B₂ : (j : ι₂) → S₂ j} →
                        (f : ι₂ → ι₁) →
                          Filter.Tendsto f 𝓕₂ 𝓕₁ →
                            [inst_2 : (i : ι₁) → Ring (R₁ i)] →
                              [inst_3 : (i : ι₂) → Ring (R₂ i)] →
                                [inst_4 : ∀ (i : ι₁), SubringClass (S₁ i) (R₁ i)] →
                                  [inst_5 : ∀ (i : ι₂), SubringClass (S₂ i) (R₂ i)] →
                                    (φ : (j : ι₂) → R₁ (f j) →+* R₂ j) →
                                      (∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)) →
                                        RestrictedProduct (fun i => R₁ i) (fun i => ↑(B₁ i)) 𝓕₁ →+*
                                          RestrictedProduct (fun j => R₂ j) (fun j => ↑(B₂ j)) 𝓕₂
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.eq_iso_inv : ∀ {A : Type u} {x y : CategoryTheory.Codiscrete A} (f : x ⟶ y), f = (y.iso x).inv
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instCommMonoid.eq_1 : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : CommMonoid R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R],
  BoundedContinuousFunction.instCommMonoid = { toMonoid := BoundedContinuousFunction.instMonoid, mul_comm := ⋯ }
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.num.injEq : ∀ (v v_1 : ℕ), (Nat.Internal.Linear.Expr.num v = Nat.Internal.Linear.Expr.num v_1) = (v = v_1)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.comp_right_assoc : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y Z : CategoryTheory.Arrow T} (g : Z ⟶ Y) (f : Y ⟶ X)
  {Z_1 : T} (h : X.right ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right (CategoryTheory.CategoryStruct.comp g f)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right f) h)
-- Init.Grind.AC
Lean.Grind.AC.Seq.erase0_k : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.ofColimitCocone_pt : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C}
  {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t),
  (CategoryTheory.Limits.Bicone.ofColimitCocone ht).pt = t.pt
-- Mathlib.CategoryTheory.IsConnected
/-- If `J` is connected, then given any function `F` such that the presence of a
morphism `j₁ ⟶ j₂` implies `F j₁ = F j₂`, we have that `F` is constant.
This can be thought of as a local-to-global property.

The converse is shown in `IsConnected.of_constant_of_preserves_morphisms`
 -/
CategoryTheory.constant_of_preserves_morphisms : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected J] {α : Type u₂} (F : J → α),
  (∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
-- Mathlib.Data.ENat.Basic
ENat.map_top : ∀ {α : Type u_1} (f : ℕ → α), ENat.map f ⊤ = ⊤
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_right_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w : Fin (n + 1) → R},
  ∑ j, w j = 1 →
    ∀ {i : Fin (n + 1)},
      (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide
          ((Finset.affineCombination R Finset.univ s.points) w) (s.points i) ↔
        0 < w i
-- Mathlib.Data.Num.Lemmas
PosNum.one_sub' : ∀ (a : PosNum), PosNum.sub' 1 a = a.pred'.toZNumNeg
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieAlgebra.IsKilling.lieIdealOrderIso_right_inv : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : FiniteDimensional K L] [inst_5 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L]
  (q : ↥(LieAlgebra.IsKilling.rootSystem H).invtRootSubmodule)
  (hq :
    optParam
      (∀ (α : ↥LieSubalgebra.root), ↑q ∈ Module.End.invtSubmodule ↑((LieAlgebra.IsKilling.rootSystem H).reflection α))
      ⋯),
  (LieAlgebra.IsKilling.invtSubmoduleToLieIdeal (↑q) hq).toInvtRootSubmodule = q
-- Mathlib.Topology.Order.Basic
/-- On a `Set.OrdConnected` subset of a linear order, the order topology for the restriction of the
order is the same as the restriction to the subset of the order topology.  -/
orderTopology_of_ordConnected : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {t : Set α} [ht : t.OrdConnected],
  OrderTopology ↑t
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Node.id.injEq : ∀ (a a_1 : Mathlib.Tactic.Widget.StringDiagram.IdNode),
  (Mathlib.Tactic.Widget.StringDiagram.Node.id a = Mathlib.Tactic.Widget.StringDiagram.Node.id a_1) = (a = a_1)
-- Mathlib.NumberTheory.Padics.PadicVal.Defs
padicValNat_eq_emultiplicity_of_ne_one : ∀ {p : ℕ}, p ≠ 1 → ∀ {n : ℕ}, n ≠ 0 → ↑(padicValNat p n) = emultiplicity p n
-- Mathlib.Topology.Compactness.Lindelof
/-- A singleton set is a Lindelof set.  -/
isLindelof_singleton : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X}, IsLindelof {x}
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f : A.toFunctor ⟶ F₂), CategoryTheory.Subfunctor.equalizer f f = A
-- Mathlib.Condensed.Light.Epi
LightCondensed.instPreservesEpimorphismsFunctorDiscreteNatLightCondModLim : ∀ {R : Type u} [inst : Ring R], CategoryTheory.Limits.lim.PreservesEpimorphisms
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
ModuleCat.shortComplexOfConj_shortExact : ∀ {R : Type u} [inst : Ring R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type v}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {L : Type v} [inst_5 : AddCommGroup L] [inst_6 : Module R L]
  {M' : Type u_1} {N' : Type u_2} {L' : Type u_3} [inst_7 : AddCommGroup M'] [inst_8 : AddCommGroup N']
  [inst_9 : AddCommGroup L'] [inst_10 : Module R M'] [inst_11 : Module R N'] [inst_12 : Module R L'] (eM : M ≃ₗ[R] M')
  (eN : N ≃ₗ[R] N') (eL : L ≃ₗ[R] L') (f : M' →ₗ[R] N') (g : N' →ₗ[R] L') (exact : Function.Exact ⇑f ⇑g),
  Function.Injective ⇑f → Function.Surjective ⇑g → (ModuleCat.shortComplexOfConj eM eN eL f g ⋯).ShortExact
-- Batteries.Data.List.Perm
List.erase_subperm : ∀ {α : Type u_1} [inst : BEq α] (a : α) (l : List α), (l.erase a).Subperm l
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.set.injEq : ∀ (x : Lean.IR.VarId) (i : ℕ) (y : Lean.IR.Arg) (b : Lean.IR.FnBody) (x_1 : Lean.IR.VarId) (i_1 : ℕ) (y_1 : Lean.IR.Arg)
  (b_1 : Lean.IR.FnBody),
  (Lean.IR.FnBody.set x i y b = Lean.IR.FnBody.set x_1 i_1 y_1 b_1) = (x = x_1 ∧ i = i_1 ∧ y = y_1 ∧ b = b_1)
-- Mathlib.Order.Cover
WithTop.coe_wcovBy_coe : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, ↑a ⩿ ↑b ↔ a ⩿ b
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.MkTableKey.State.mctx : Lean.Meta.SynthInstance.MkTableKey.State → Lean.MetavarContext
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app : ∀ {X : AlgebraicGeometry.LocallyRingedSpace} {R : Type u} [inst : CommRing R]
  (f : AlgebraicGeometry.LocallyRingedSpace.Γ.rightOp.obj X ⟶ Opposite.op (CommRingCat.of R))
  (U :
    (TopologicalSpace.Opens
        ↑↑(AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom
        (algebraMap R
          ((AlgebraicGeometry.structureSheafInType ↑(Opposite.unop (Opposite.op (CommRingCat.of R)))
                  ↑(Opposite.unop (Opposite.op (CommRingCat.of R)))).obj.obj
            U)))
      (((AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X (Opposite.op (CommRingCat.of R))) f).c.app U) =
    CategoryTheory.CategoryStruct.comp f.unop (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)
-- Lean.Compiler.LCNF.Types
Lean.Compiler.LCNF.joinTypes : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Given an adjunction `adj : F ⊣ G`, `a, b` in `A` and commutation isomorphisms
between shifts by `a` (resp. `b`) and `F` and `G`, if these commutation isomorphisms are
compatible with the unit of `adj`, then so are the commutation isomorphisms between shifts
by `a + b` and `F` and `G` constructed by `Functor.CommShift.isoAdd`.
 -/
CategoryTheory.Adjunction.CommShift.compatibilityUnit_isoAdd : ∀ {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}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] {a b : A}
  (e₁ : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
  (f₁ : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b))
  (e₂ : (CategoryTheory.shiftFunctor D a).comp G ≅ G.comp (CategoryTheory.shiftFunctor C a))
  (f₂ : (CategoryTheory.shiftFunctor D b).comp G ≅ G.comp (CategoryTheory.shiftFunctor C b)),
  CategoryTheory.Adjunction.CommShift.CompatibilityUnit adj e₁ e₂ →
    CategoryTheory.Adjunction.CommShift.CompatibilityUnit adj f₁ f₂ →
      CategoryTheory.Adjunction.CommShift.CompatibilityUnit adj (CategoryTheory.Functor.CommShift.isoAdd e₁ f₁)
        (CategoryTheory.Functor.CommShift.isoAdd e₂ f₂)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_eq_of_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α]
  [inst_3 : Inhabited α], m.WF → ∀ {k : α}, k ∈ m → m.getKey! k = k
-- Mathlib.RingTheory.LaurentSeries
RatFunc.valuation_eq_LaurentSeries_valuation : ∀ (K : Type u_2) [inst : Field K] (P : RatFunc K),
  (RatFunc.polynomialValuationX K) P =
    (IsDedekindDomain.HeightOneSpectrum.valuation (LaurentSeries K) (PowerSeries.idealX K))
      ((algebraMap (RatFunc K) (LaurentSeries K)) P)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.toAffineEquiv_refl : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P],
  (AffineIsometryEquiv.refl 𝕜 P).toAffineEquiv = AffineEquiv.refl 𝕜 P
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.Q.ind : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] {β : Lean.Grind.IntModule.OfNatModule.Q α → Prop},
  (∀ (a : α × α), β (Lean.Grind.IntModule.OfNatModule.Q.mk a)) → ∀ (q : Lean.Grind.IntModule.OfNatModule.Q α), β q
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.addWeightOfEPs_nil : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : AddMonoid R] (w : V → V → R) (a : V),
  Quiver.Path.addWeightOfEPs w Quiver.Path.nil = 0
-- Mathlib.Topology.Bornology.Absorbs
absorbent_iff_inv_smul : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α]
  {s : Set α}, Absorbent G₀ s ↔ ∀ (x : α), ∀ᶠ (c : G₀) in Bornology.cobounded G₀, c⁻¹ • x ∈ s
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.whiskerRight_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : CategoryTheory.AddGrp C) {H I : CategoryTheory.AddGrp C} (f : H ⟶ I),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G f).hom.hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft G.X f.hom.hom
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {f : β k → β k},
  (t.modify k f).getKey? k' = if cmp k k' = Ordering.eq then if k ∈ t then some k else none else t.getKey? k'
-- Lean.Server.References
/-- Combines the `usages` of `a` and `b` and prefers the `definition?` of `b` over that of `a`.  -/
Lean.Lsp.RefInfo.merge : Lean.Lsp.RefInfo → Lean.Lsp.RefInfo → Lean.Lsp.RefInfo
-- Lean.Parser.Types
Lean.Parser.ParserCacheKey.parserName : Lean.Parser.ParserCacheKey → Lean.Name
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.glue : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) r o₂ →
      Ordnode.BalancedSz l.size r.size → Ordnode.Valid' o₁ (l.glue r) o₂ ∧ (l.glue r).size = l.size + r.size
-- Init.Data.String.Basic
ByteArray.utf8Decode?.go.eq_def : ∀ (b : ByteArray) (i : ℕ) (acc : Array Char) (hi : i ≤ b.size),
  ByteArray.utf8Decode?.go b i acc hi =
    if i < b.size then
      match h : b.utf8DecodeChar? i with
      | none => none
      | some c => ByteArray.utf8Decode?.go b (i + c.utf8Size) (acc.push c) ⋯
    else some acc
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.TFAE : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R],
  [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      Std.Total fun x1 x2 => x1 ∣ x2, Std.Total fun x1 x2 => x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.insert_infty_range_coe : ∀ {X : Type u_1}, insert OnePoint.infty (Set.range OnePoint.some) = Set.univ
-- Mathlib.Topology.Separation.Basic
isEmbedding_iff_isInducing : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T0Space X] {f : X → Y},
  Topology.IsEmbedding f ↔ Topology.IsInducing f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPullback.hasPullback_biprod_fst_biprod_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.HasPullback CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.exists_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W),
  autoParam (CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
      CategoryTheory.Limits.pushout.exists_desc._auto_1 →
    ∃ l,
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) l = h ∧
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) l = k
-- Mathlib.LinearAlgebra.Projection
LinearMap.linearProjOfIsCompl.eq_1 : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (q : Submodule R E)
  {F : Type u_7} [inst_3 : AddCommGroup F] [inst_4 : Module R F] (i : F →ₗ[R] E) (hi : Function.Injective ⇑i)
  (h : IsCompl i.range q),
  LinearMap.linearProjOfIsCompl q i hi h = ↑(LinearEquiv.ofInjective i hi).symm ∘ₗ i.range.projectionOnto q h
-- Lean.Parser.Do
Lean.Parser.Term.doLetElse.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Complex.Exponential
Real.exp.eq_1 : ∀ (x : ℝ), Real.exp x = (Complex.exp ↑x).re
-- Mathlib.Control.Fix
Part.fixAux.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)) {p : ℕ → Prop} (i : Nat.Upto p)
  (g : (j : Nat.Upto p) → i < j → (a : α) → Part (β a)),
  Part.fixAux f i g = f fun x => Part.assert (¬p ↑i) fun h => g (i.succ h) ⋯ x
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.Measure.MutuallySingular.withDensity : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f : α → ENNReal},
  μ.MutuallySingular ν → (μ.withDensity f).MutuallySingular ν
-- Mathlib.Tactic.NormNum.Core
Mathlib.Meta.NormNum.NormNums.mk : Lean.Meta.DiscrTree Mathlib.Meta.NormNum.NormNumExt → Lean.PHashSet Lean.Name → Mathlib.Meta.NormNum.NormNums
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.instIteratorLoop.loop.wf.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α] {n : Type u → Type w}
  [inst_5 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxo.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (upperBound : α) (acc : γ)
  (next : α) (h : LargeEnough next)
  (f : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n { s // Pl out c s }),
  Std.Rxo.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc next h f =
    if hu : next < upperBound then do
      let __do_lift ← f next h hu acc
      match __do_lift with
        | ⟨ForInStep.yield acc', property⟩ =>
          match hs : Std.PRange.succ? next with
          | some next' => Std.Rxo.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc' next' ⋯ f
          | none => pure acc'
        | ⟨ForInStep.done acc', property⟩ => pure acc'
    else pure acc
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.opIso_inv_inr_op : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv CategoryTheory.Limits.biprod.inr.op =
    CategoryTheory.Limits.biprod.snd
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Embedding.equivRange_toEquiv_apply : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N) (a : M),
  f.equivRange.toEquiv a = (FirstOrder.Language.Embedding.codRestrict f.toHom.range f ⋯) a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.minKey!_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).isEmpty = false →
        ((Std.DTreeMap.Raw.Const.alter t k f).minKey! = k ↔
          (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true)
-- Mathlib.LinearAlgebra.StdBasis
Pi.basis.eq_1 : ∀ {R : Type u_2} {η : Type u_4} {ιs : η → Type u_5} {Ms : η → Type u_6} [inst : Semiring R]
  [inst_1 : (i : η) → AddCommMonoid (Ms i)] [inst_2 : (i : η) → Module R (Ms i)] [inst_3 : Fintype η]
  (s : (j : η) → Module.Basis (ιs j) R (Ms j)),
  Pi.basis s =
    { repr := (LinearEquiv.piCongrRight fun j => (s j).repr) ≪≫ₗ (Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm }
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.mul_ineq_cert : Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.Topology.Homeomorph.Lemmas
Topology.IsEmbedding.toHomeomorphOfSurjective_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : Topology.IsEmbedding f) (hsurj : Function.Surjective f) (a : X), (hf.toHomeomorphOfSurjective hsurj) a = f a
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
_private.Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification.0.NumberField.InfinitePlace.mapsTo_embeddingConjugateIte : ∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K),
  Set.MapsTo (NumberField.InfinitePlace.embeddingConjugateIte✝ v) (NumberField.InfinitePlace.unramifiedPlacesOver L v)
    (NumberField.ComplexEmbedding.unmixedEmbeddingsOver L v.embedding)
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.ofEquiv_F : ∀ {α : Type u_1} {τ : Type u_4} [inst : TopologicalSpace α] (F : Ctop.Realizer α) (E : F.σ ≃ τ) (s : τ),
  (F.ofEquiv E).F.f s = F.F.f (E.symm s)
-- Mathlib.CategoryTheory.Quotient
instInhabitedHomRel : (C : Type u_1) → [inst : Quiver C] → Inhabited (HomRel C)
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- If a module has a finite dimension, all bases are indexed by a finite type.  -/
Module.Basis.nonempty_fintype_index_of_rank_lt_aleph0 : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type u_1} (b : Module.Basis ι R M), Module.rank R M < Cardinal.aleph0 → Nonempty (Fintype ι)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushout.ι_desc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → B ⟶ objs j) [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C} (f : B ⟶ X)
  (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.ι arrows j)
      (CategoryTheory.Limits.WidePushout.desc f fs w) =
    fs j
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.instForInTotalOfIteratorLoopOfMonadLiftTOfMonadOfFinite : {m : Type w → Type w'} →
  {n : Type w → Type w''} →
    {α β : Type w} →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m n] →
          [MonadLiftT m n] → [Monad n] → [Std.Iterators.Finite α m] → ForIn n (Std.IterM.Total m β) β