mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Graph.Maps
Graph.map_inc : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {e : β} {x : α'} (f : α → α'),
  (Graph.map f G).Inc e x ↔ ∃ v, G.Inc e v ∧ x = f v
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chains₁ToCoinvariantsKer.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.chains₁ToCoinvariantsKer A =
    ModuleCat.ofHom
      (LinearMap.codRestrict (Representation.Coinvariants.ker A.ρ) (ModuleCat.Hom.hom (groupHomology.d₁₀ A)) ⋯)
-- Init.Data.SInt.Lemmas
Int32.minValue_div_neg_one : Int32.minValue / -1 = Int32.minValue
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The generating equivalence relation for elements of the free tensor algebra
that are identified in the free product  -/
LinearAlgebra.FreeProduct.rel : {I : Type u} →
  [DecidableEq I] →
    (R : Type v) →
      [inst : CommSemiring R] →
        (A : I → Type w) →
          [inst_1 : (i : I) → Semiring (A i)] →
            [inst_2 : (i : I) → Algebra R (A i)] →
              LinearAlgebra.FreeProduct.FreeTensorAlgebra R A → LinearAlgebra.FreeProduct.FreeTensorAlgebra R A → Prop
-- Lean.MetavarContext
Lean.MetavarContext.mk.injEq : ∀ (depth levelAssignDepth lmvarCounter mvarCounter : ℕ)
  (lDecls : Lean.PersistentHashMap Lean.LMVarId Lean.LevelMetavarDecl)
  (decls : Lean.PersistentHashMap Lean.MVarId Lean.MetavarDecl)
  (userNames : Lean.PersistentHashMap Lean.Name Lean.MVarId)
  (lAssignment : Lean.PersistentHashMap Lean.LMVarId Lean.Level)
  (eAssignment : Lean.PersistentHashMap Lean.MVarId Lean.Expr)
  (dAssignment : Lean.PersistentHashMap Lean.MVarId Lean.DelayedMetavarAssignment)
  (depth_1 levelAssignDepth_1 lmvarCounter_1 mvarCounter_1 : ℕ)
  (lDecls_1 : Lean.PersistentHashMap Lean.LMVarId Lean.LevelMetavarDecl)
  (decls_1 : Lean.PersistentHashMap Lean.MVarId Lean.MetavarDecl)
  (userNames_1 : Lean.PersistentHashMap Lean.Name Lean.MVarId)
  (lAssignment_1 : Lean.PersistentHashMap Lean.LMVarId Lean.Level)
  (eAssignment_1 : Lean.PersistentHashMap Lean.MVarId Lean.Expr)
  (dAssignment_1 : Lean.PersistentHashMap Lean.MVarId Lean.DelayedMetavarAssignment),
  ({ depth := depth, levelAssignDepth := levelAssignDepth, lmvarCounter := lmvarCounter, mvarCounter := mvarCounter,
        lDecls := lDecls, decls := decls, userNames := userNames, lAssignment := lAssignment,
        eAssignment := eAssignment, dAssignment := dAssignment } =
      { depth := depth_1, levelAssignDepth := levelAssignDepth_1, lmvarCounter := lmvarCounter_1,
        mvarCounter := mvarCounter_1, lDecls := lDecls_1, decls := decls_1, userNames := userNames_1,
        lAssignment := lAssignment_1, eAssignment := eAssignment_1, dAssignment := dAssignment_1 }) =
    (depth = depth_1 ∧
      levelAssignDepth = levelAssignDepth_1 ∧
        lmvarCounter = lmvarCounter_1 ∧
          mvarCounter = mvarCounter_1 ∧
            lDecls = lDecls_1 ∧
              decls = decls_1 ∧
                userNames = userNames_1 ∧
                  lAssignment = lAssignment_1 ∧ eAssignment = eAssignment_1 ∧ dAssignment = dAssignment_1)
-- Mathlib.NumberTheory.Divisors
Nat.filter_dvd_eq_divisors : ∀ {n : ℕ}, n ≠ 0 → {d ∈ Finset.range n.succ | d ∣ n} = n.divisors
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance to a set is uniformly continuous in point  -/
Metric.uniformContinuous_infDist_pt : ∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), UniformContinuous fun x => Metric.infDist x s
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.Factors.piQuotientEquiv_map : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsDedekindDomain S] (p : Ideal R) (hp : Ideal.map (algebraMap R S) p ≠ ⊥) (x : R),
  (Ideal.Factors.piQuotientEquiv p hp) ((algebraMap R (S ⧸ Ideal.map (algebraMap R S) p)) x) = fun x_1 =>
    (Ideal.Quotient.mk (↑x_1 ^ p.ramificationIdx' ↑x_1)) ((algebraMap R S) x)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.clear.inj : ∀ {p : Turing.PartrecToTM2.Γ' → Bool} {k : Turing.PartrecToTM2.K'} {q : Turing.PartrecToTM2.Λ'}
  {p_1 : Turing.PartrecToTM2.Γ' → Bool} {k_1 : Turing.PartrecToTM2.K'} {q_1 : Turing.PartrecToTM2.Λ'},
  Turing.PartrecToTM2.Λ'.clear p k q = Turing.PartrecToTM2.Λ'.clear p_1 k_1 q_1 → p = p_1 ∧ k = k_1 ∧ q = q_1
-- Mathlib.Algebra.Lie.Matrix
LieModule.toEnd_matrix : ∀ {R : Type u} [inst : CommRing R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  LieModule.toEnd R (Matrix n n R) (n → R) = lieEquivMatrix'.symm.toLieHom
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.mk_bracket : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (x y : L), LieSubmodule.Quotient.mk ⁅x, y⁆ = ⁅LieSubmodule.Quotient.mk x, LieSubmodule.Quotient.mk y⁆
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Given `Subsemiring`s `s`, `t` of semirings `R`, `S` respectively, `s.prod t` is `s × t`
as a subsemiring of `R × S`.  -/
Subsemiring.prod : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → Subsemiring R → Subsemiring S → Subsemiring (R × S)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.homMk'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.AddGrp C} (f : A.toAddMon ⟶ B.toAddMon), CategoryTheory.AddGrp.homMk' f = { hom := f }
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_restoreM_OptionT_apply_eq : ∀ {Pred : Type u} {EPred : Type u_1} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ Pred EPred} (x : m (Option α)),
  Std.Internal.Do.wp (MonadControl.restoreM x) post epost =
    Std.Internal.Do.wp x (Std.Internal.Do.EPost.Cons.pushOption post epost) epost.tail
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.mapToEqualizer.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_4)) {W X B : C}
  (f : X ⟶ B) (g₁ g₂ : W ⟶ X) (w : CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f),
  CategoryTheory.regularTopology.mapToEqualizer P f g₁ g₂ w =
    TypeCat.ofHom fun t => ⟨(CategoryTheory.ConcreteCategory.hom (P.map f.op)) t, ⋯⟩
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_erase_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k : α} {fallback : β k}, (m.erase k).getD k fallback = fallback
-- Mathlib.CategoryTheory.Sites.Continuous
/-- If a continuous functor between sites is isomorphic to the identity functor,
then the corresponding pushforward functor on sheaves identifies to the
identity functor.  -/
CategoryTheory.Functor.sheafPushforwardContinuousId' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F'' : CategoryTheory.Functor C C} →
      (F'' ≅ CategoryTheory.Functor.id C) →
        (A : Type u) →
          [inst_1 : CategoryTheory.Category.{t, u} A] →
            (J : CategoryTheory.GrothendieckTopology C) →
              [inst_2 : F''.IsContinuous J J] →
                F''.sheafPushforwardContinuous A J J ≅ CategoryTheory.Functor.id (CategoryTheory.Sheaf J A)
-- Mathlib.Algebra.Category.MonCat.Yoneda
AddCommMonCat.coyonedaType.eq_1 : AddCommMonCat.coyonedaType =
  {
    obj := fun X =>
      { obj := fun M => AddCommMonCat.of (Opposite.unop X → ↑M),
        map := fun {X_1 Y} f =>
          AddCommMonCat.ofHom
            (AddMonoidHom.pi fun i => (AddCommMonCat.Hom.hom f).comp (Pi.evalAddMonoidHom (fun a => ↑X_1) i)),
        map_id := ⋯, map_comp := ⋯ },
    map := fun {X Y} f =>
      {
        app := fun N =>
          AddCommMonCat.ofHom
            (AddMonoidHom.pi fun i =>
              Pi.evalAddMonoidHom (fun a => ↑N) ((CategoryTheory.ConcreteCategory.hom f.unop) i)),
        naturality := ⋯ },
    map_id := AddCommMonCat.coyonedaType._proof_4, map_comp := @AddCommMonCat.coyonedaType._proof_5 }
-- Mathlib.Analysis.Meromorphic.Order
/-- A function meromorphic on `U`, with meromorphic order nowhere `⊤`, is nonvanishing away from a
codiscrete subset of `U`.
 -/
MeromorphicOn.eventually_codiscreteWithin_apply_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E},
  MeromorphicOn f U → (∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤) → ∀ᶠ (x : 𝕜) in Filter.codiscreteWithin U, f x ≠ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.le_iff_exists_mono : ∀ {X : SSet} {x y : X.N},
  x ≤ y ↔ ∃ f, ∃ (_ : CategoryTheory.Mono f), (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
-- Mathlib.Order.Filter.Prod
Filter.map_fst_prod : ∀ {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) [g.NeBot], Filter.map Prod.fst (f ×ˢ g) = f
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.quasiIsoAt_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K L : CochainComplex C ℤ) [inst_2 : CategoryTheory.EnoughInjectives C] (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ →
    ∀ (i : ℤ),
      autoParam (i ≤ n₀) CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.quasiIsoAt_π._auto_1✝ →
        QuasiIsoAt (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.π✝ K L n₁) i
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.lanCompColimIso_hom_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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape C H] [inst_5 : CategoryTheory.Limits.HasColimitsOfShape D H]
  (X : CategoryTheory.Functor C H),
  L.lanCompColimIso.hom.app X = ((L.lan.obj X).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X)).hom
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- (Implementation): Auxiliary lemma for `CategoryTheory.PreOneHypercover.isoMk`.  -/
CategoryTheory.PreOneHypercover.isoMk_aux : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j))
  {i j : E.I₀} (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) (k : E.I₁ i j),
  CategoryTheory.CategoryStruct.comp (h₁ k).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (h₁ (s₁.symm ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ k).inv
      (CategoryTheory.eqToHom ⋯)
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.fixedField_le : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {H1 H2 : Subgroup Gal(E/F)},
  H1 ≤ H2 → IntermediateField.fixedField H2 ≤ IntermediateField.fixedField H1
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_iSizeToBitVec : ∀ (x : ISize), Int8.ofBitVec (BitVec.signExtend 8 x.toBitVec) = x.toInt8
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.unop_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex Cᵒᵖ), S.unop.X₂ = Opposite.unop S.X₂
-- Mathlib.Data.QPF.Univariate.Basic
QPF.mem_supp : ∀ {F : Type u → Type u} [q : QPF F] {α : Type u} (x : F α) (u : α),
  u ∈ Functor.supp x ↔ ∀ (a : (QPF.P F).A) (f : (QPF.P F).B a → α), QPF.abs ⟨a, f⟩ = x → u ∈ f '' Set.univ
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.jacobson_top : ∀ {R : Type u} [inst : Ring R], ⊤.jacobson = ⊤
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.instOfTwoCocycle : {R : Type u_1} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    (c : ↥(LieModule.Cohomology.twoCocycle R L M)) → LieAlgebra R (LieAlgebra.ofTwoCocycle c)
-- Lean.Meta.ArgsPacker
/-- If `arg` is the argument to the `fidx`th of the `argsPacker.numFuncs` in the recursive group,
then `mk` packs that argument in `PSum.inl` and `PSum.inr` constructors
to create the mutual-packed argument of type `domain`.
 -/
Lean.Meta.ArgsPacker.Mutual.pack : ℕ → Lean.Expr → ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.List.Sort
List.mem_orderedInsert : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] {a b : α} {l : List α},
  a ∈ List.orderedInsert r b l ↔ a = b ∨ a ∈ l
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorialBinarySplitting.eq_1 : ∀ (n : ℕ), n.factorialBinarySplitting = Nat.ascFactorialBinary 1 n
-- Mathlib.Algebra.Homology.Augment
ChainComplex.augmentTruncate_hom_f_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ), C.augmentTruncate.hom.f 0 = CategoryTheory.CategoryStruct.id (C.X 0)
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.instHasCoproductsOfShapeOverSchemeTopMorphismPropertyOfSmall : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {S : AlgebraicGeometry.Scheme} {ι : Type u_2} [Small.{u, u_2} ι],
  CategoryTheory.Limits.HasCoproductsOfShape ι (P.Over ⊤ S)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getKey? k' = some k
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.constVSub_symm_apply : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (p : P₁) (x : V₁), (AffineEquiv.constVSub k p).symm x = -x +ᵥ p
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleRange_of_gt : ∀ {n : ℕ} {i j : Fin n}, i < j → i.cycleRange j = j
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
/-- For `μ : VectorMeasure X ℝ≥0∞`, `preVariationFun μ s = μ s` for any `s`.  -/
MeasureTheory.VectorMeasure.preVariationFun_apply_of_ennreal : ∀ {X : Type u_1} {mX : MeasurableSpace X} (μ : MeasureTheory.VectorMeasure X ENNReal) (s : Set X),
  MeasureTheory.preVariationFun (⇑μ) s = μ s
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.sdiv_eq.match_1.eq_1 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match false, false with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_1 ()
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.maxD_le_maxD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {k fallback : α}, (cmp (t.maxD fallback) ((t.insert k).maxD fallback)).isLE = true
-- Mathlib.Logic.Equiv.Basic
/-- Augment an equivalence with a prescribed mapping `f a = b`  -/
Equiv.setValue : {α : Sort u_1} → {β : Sort u_4} → [DecidableEq α] → α ≃ β → α → β → α ≃ β
-- Mathlib.Analysis.Normed.Operator.Bilinear
Continuous.clm_comp_const : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  {σ₁₃ : 𝕜 →+* 𝕜₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃]
  [RingHomIsometric σ₁₂] {X : Type u_11} [inst_13 : TopologicalSpace X] {g : X → F →SL[σ₂₃] G},
  Continuous g → ∀ (f : E →SL[σ₁₂] F), Continuous fun x => g x ∘SL f
-- Mathlib.NumberTheory.NumberField.Basic
/-- The ring of integers (or number ring) corresponding to a number field
is the integral closure of ℤ in the number field.

This is defined as its own type, rather than a `Subalgebra`, for performance reasons:
looking for instances of the form `SMul (RingOfIntegers _) (RingOfIntegers _)` makes
much more effective use of the discrimination tree than instances of the form
`SMul (Subtype _) (Subtype _)`.
The drawback is we have to copy over instances manually.
 -/
NumberField.RingOfIntegers : (K : Type u_1) → [Field K] → Type u_1
-- Mathlib.CategoryTheory.Localization.Predicate
/-- Given a localization functor `L : C ⥤ D` for `W : MorphismProperty C`,
if `(F₁' F₂' : D ⥤ E)` are functors which lift functors `(F₁ F₂ : C ⥤ E)`,
a natural isomorphism `τ : F₁ ⟶ F₂` lifts to a natural isomorphism `F₁' ⟶ F₂'`.  -/
CategoryTheory.Localization.liftNatIso : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            {E : Type u_3} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
                [L.IsLocalization W] →
                  (F₁ F₂ : CategoryTheory.Functor C E) →
                    (F₁' F₂' : CategoryTheory.Functor D E) →
                      [h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'] →
                        [h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂'] → (F₁ ≅ F₂) → (F₁' ≅ F₂')
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
ModuleCat.extendScalars_μ : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (M₁ M₂ : ModuleCat R),
  CategoryTheory.Functor.LaxMonoidal.μ (ModuleCat.extendScalars f) M₁ M₂ =
    ModuleCat.ofHom ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R S ↑M₁ ↑M₂).symm
-- Lean.Meta.Instances
Lean.Meta.instInhabitedInstanceEntry.default : Lean.Meta.InstanceEntry
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- In an additive commutative monoid with multiplication,
`∑ i ∈ I, a i * a i` is a sum of squares.
 -/
IsSumSq.sum_mul_self : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Mul R] {ι : Type u_2} (I : Finset ι) (a : ι → R),
  IsSumSq (∑ i ∈ I, a i * a i)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
/-- A choice of finite products of `Over X` given by `Limits.pullback`.  -/
CategoryTheory.Over.cartesianMonoidalCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasPullbacks C] → (X : C) → CategoryTheory.CartesianMonoidalCategory (CategoryTheory.Over X)
-- Init.Data.Range.Polymorphic.SInt
Int8.instRxoLawfulHasSize : Std.Rxo.LawfulHasSize Int8
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_map_fun : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'}
  {μ : MeasureTheory.Measure Ω'} {Z : Ω' → Ω},
  MeasureTheory.AEStronglyMeasurable X (MeasureTheory.Measure.map Z μ) →
    MeasureTheory.AEStronglyMeasurable Y (MeasureTheory.Measure.map Z μ) →
      AEMeasurable Z μ →
        ProbabilityTheory.covariance X Y (MeasureTheory.Measure.map Z μ) =
          ProbabilityTheory.covariance (fun ω => X (Z ω)) (fun ω => Y (Z ω)) μ
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.map_id : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  Subalgebra.map (AlgHom.id R A) S = S
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyRel.symm_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {S : Set X}
  (F : f₀.HomotopyRel f₁ S) (x : ↑unitInterval × X), F.symm x = F (unitInterval.symm x.1, x.2)
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint : ∀ {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_2, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] (F : CategoryTheory.Functor C D) [F.IsLeftAdjoint],
  CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v_2, v_3, u_2, u_3} F
-- Mathlib.Data.Sym.NatCard
Sym2.instInfiniteSubtypeNotIsDiag : ∀ (α : Type u_1) [Infinite α], Infinite { a // ¬a.IsDiag }
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_of_not_sfinite : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α)
  (κ : ProbabilityTheory.Kernel α β), ¬MeasureTheory.SFinite μ → μ.compProd κ = 0
-- Mathlib.Tactic.DeriveFintype
/-- The term elaborator `derive_fintype% α` tries to synthesize a `Fintype α` instance
using all the assumptions in the local context; this can be useful, for example, if one
needs an extra `DecidableEq` instance. It works only if `α` is an inductive
type that `proxy_equiv% α` can handle. The elaborator makes use of the
expected type, so `(derive_fintype% _ : Fintype α)` works.

This uses `proxy_equiv% α`, so as a side effect it defines `proxyType` and `proxyTypeEquiv` in
the namespace associated to the inductive type `α`.
 -/
Mathlib.Deriving.Fintype.«termDerive_fintype%_» : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.EMatchTheorem.getProofWithFreshMVarLevels : Lean.Meta.Grind.EMatchTheorem → Lean.MetaM Lean.Expr
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsStronglyProgressive.neg : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : MeasurableSpace ι] [inst_3 : AddGroup β]
  [ContinuousNeg β], MeasureTheory.IsStronglyProgressive f u → MeasureTheory.IsStronglyProgressive f fun i ω => -u i ω
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.toIsoString : Std.Time.TimeZone.Offset → Std.Time.Reason✝ → Std.Time.Reason✝ → Bool → optParam Bool true → String
-- Mathlib.Condensed.TopCatAdjunction
condensedSetToTopCat_obj_carrier : ∀ (X : CondensedSet), ↑(condensedSetToTopCat.obj X) = X.obj.obj (Opposite.op (CompHaus.of PUnit.{u + 1}))
-- Mathlib.Algebra.Order.Monovary
/-- Two functions monovary iff the rearrangement inequality holds.  -/
monovaryOn_iff_mul_rearrangement : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α}
  {s : Set ι}, MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g j + f j * g i ≤ f i * g i + f j * g j
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.lt_of_floor_lt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {n : ℕ},
  ⌊a⌋₊ < n → a < ↑n
-- Mathlib.Analysis.LocallyConvex.PointwiseConvergence
PointwiseConvergenceCLM.withSeminorms : ∀ {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_7}
  {F : Type u_8} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜₂ F],
  WithSeminorms (PointwiseConvergenceCLM.seminormFamily σ E F)
-- Mathlib.Tactic.Push
/-- The `simp` configuration used in `push`.  -/
Mathlib.Tactic.Push.pushSimpConfig : Lean.Meta.Simp.Config