mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- **Alias** of `FunLike.coe_coeAddMonoidHom`. -/
ContDiffMapSupportedIn.coe_coeHom : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β], ⇑(FunLike.coeAddMonoidHom F α β) = DFunLike.coe
-- Batteries.Data.AssocList
List.toList_toAssocList : ∀ {α : Type u_1} {β : Type u_2} (l : List (α × β)), l.toAssocList.toList = l
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restrictionCyclesIso_inv_iCycles : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (j k : ι) (hk : c.next j = k) {j' k' : ι'}
  (hj' : e.f j = j') (hk' : e.f k = k') (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j']
  [inst_4 : (K.restriction e).HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').inv ((K.restriction e).iCycles j) =
    CategoryTheory.CategoryStruct.comp (K.iCycles j') (K.restrictionXIso e hj').inv
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.mapAddEquiv_trans`. -/
MonoidAlgebra.mapRangeAddEquiv_trans : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] [inst_3 : Mul M] (e₁ : R ≃+ S) (e₂ : S ≃+ T),
  MonoidAlgebra.mapAddEquiv M (e₁.trans e₂) = (MonoidAlgebra.mapAddEquiv M e₁).trans (MonoidAlgebra.mapAddEquiv M e₂)
-- Mathlib.Algebra.Algebra.Unitization
/-- The coercion from a non-unital `R`-algebra `A` to its unitization `Unitization R A`
realized as a non-unital star algebra homomorphism.  -/
Unitization.inrNonUnitalStarAlgHom : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : StarAddMonoid R] →
        [inst_2 : NonUnitalSemiring A] → [inst_3 : Star A] → [inst_4 : Module R A] → A →⋆ₙₐ[R] Unitization R A
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.TransitionRule.mk.injEq : ∀ (spec : Std.Time.TimeZone.TransitionSpec) (time : Std.Time.Second.Offset) (spec_1 : Std.Time.TimeZone.TransitionSpec)
  (time_1 : Std.Time.Second.Offset),
  ({ spec := spec, time := time } = { spec := spec_1, time := time_1 }) = (spec = spec_1 ∧ time = time_1)
-- Init.Data.String.Basic
String.prev : String → String.Pos.Raw → String.Pos.Raw
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationHints.partialFixpoint? : Lean.Elab.TerminationHints → Option Lean.Elab.PartialFixpoint
-- Mathlib.Data.List.Shortlex
List.Shortlex.append_right : ∀ {α : Type u_1} {r : α → α → Prop} {s₁ s₂ : List α} (t : List α), List.Shortlex r s₁ s₂ → List.Shortlex r s₁ (s₂ ++ t)
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- On a scheme `X`, the preimage of the zero locus of the prime spectrum
of `Γ(X, ⊤)` under `X.toSpecΓ : X ⟶ Spec Γ(X, ⊤)` agrees with the associated zero locus on `X`.  -/
AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus : ∀ (X : AlgebraicGeometry.Scheme) (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))),
  ⇑X.toSpecΓ ⁻¹' PrimeSpectrum.zeroLocus s = X.zeroLocus s
-- Lean.Meta.Tactic.Simp.Rewrite
/-- Helper type for implementing `discharge?'`
 -/
Lean.Meta.Simp.DischargeResult : Type
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.weightedVSubVSubWeights_apply_right : ∀ (k : Type u_1) [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] {i j : ι},
  i ≠ j → Finset.weightedVSubVSubWeights k i j j = -1
-- Mathlib.Order.Filter.CountablyGenerated
Filter.HasAntitoneBasis.mem_iff : ∀ {α : Type u_1} {ι : Type u_4} [inst : Preorder ι] {l : Filter α} {s : ι → Set α},
  l.HasAntitoneBasis s → ∀ {t : Set α}, t ∈ l ↔ ∃ i, s i ⊆ t
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
CommMonCat.FilteredColimits.colimitCocone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J CommMonCat),
  CommMonCat.FilteredColimits.colimitCocone F =
    { pt := CommMonCat.FilteredColimits.colimit F,
      ι :=
        {
          app := fun j =>
            CommMonCat.ofHom
              (MonCat.Hom.hom
                ((MonCat.FilteredColimits.colimitCocone (F.comp (CategoryTheory.forget₂ CommMonCat MonCat))).ι.app j)),
          naturality := ⋯ } }
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_of_mul_const : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {l : Filter α}
  {f : α → M} (C : M), Filter.Tendsto (fun x => f x * C) l Filter.atBot → Filter.Tendsto f l Filter.atBot
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
_private.Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple.0.RootPairing.GeckConstruction.instIsIrreducible_aux₀ : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field K] [inst_1 : CharZero K]
  [inst_2 : DecidableEq ι] [inst_3 : Fintype ι] [inst_4 : AddCommGroup M] [inst_5 : Module K M]
  [inst_6 : AddCommGroup N] [inst_7 : Module K N] {P : RootPairing ι K M N} [P.IsRootSystem]
  [inst_9 : P.IsCrystallographic] {b : P.Base}
  {U : LieSubmodule K (↥(RootPairing.GeckConstruction.cartanSubalgebra' b)) (↥b.support ⊕ ι → K)}
  (χ : ↥(RootPairing.GeckConstruction.cartanSubalgebra' b) → K),
  χ ≠ 0 →
    LieModule.genWeightSpace (↥U) χ ≠ ⊥ →
      ∃ i, RootPairing.GeckConstruction.v b i ∈ LieSubmodule.map U.incl (LieModule.genWeightSpace (↥U) χ)
-- Init.Data.String.Substring
/-- Removes the specified number of characters (Unicode code points) from the beginning of a substring
by advancing its start position.

If the substring's end position is reached, the start position is not advanced past it.
 -/
Substring.Raw.drop : Substring.Raw → ℕ → Substring.Raw
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage f U).hom
      ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U).ι =
    CategoryTheory.CategoryStruct.comp U.ι f
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- Interpret a bundled continuous map as an element of `α →ᵤ[{K | IsCompact K}] β`.

We use this map to induce the `UniformSpace` structure on `C(α, β)`.  -/
ContinuousMap.toUniformOnFunIsCompact : {α : Type u₁} →
  {β : Type u₂} → [inst : TopologicalSpace α] → [inst_1 : UniformSpace β] → C(α, β) → UniformOnFun α β {K | IsCompact K}
-- Mathlib.Data.Nat.Sqrt
Nat.succ_le_succ_sqrt' : ∀ (n : ℕ), n + 1 ≤ (n.sqrt + 1) ^ 2
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instFstScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsImmersion g],
  AlgebraicGeometry.IsImmersion (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.instCoeTCOfMulDistribMulActionSemiHomClassCoeMonoidHom.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  {F : Type u_10} [inst_6 : FunLike F A B] [inst_7 : MulDistribMulActionSemiHomClass F (⇑φ) A B],
  MulDistribMulActionHom.instCoeTCOfMulDistribMulActionSemiHomClassCoeMonoidHom =
    { coe := MulDistribMulActionSemiHomClass.toMulDistribMulActionHom }
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.inertiaDeg_pos : ∀ {S : Type u_1} [inst : CommRing S] (q : Ideal S) (R : Type u_2) [inst_1 : CommRing R] [inst_2 : Algebra R S]
  [hq : q.IsPrime] [Module.Finite R S], 0 < q.inertiaDeg R
-- Mathlib.Order.Filter.Defs
Filter.sSup_lowerBounds : ∀ {α : Type u_1} (s : Set (Filter α)), sSup (lowerBounds s) = sInf s
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.support.eq_1 : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] (x : HahnSeries Γ R),
  x.support = Function.support x.coeff
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.nonCommSemiring : ℕ → Lean.Meta.Sym.Arith.ClassifyResult
-- Std.Time.Format
/-- Parses a date string in the Lean format (`uuuu-MM-dd`) and returns a `PlainDate`.
 -/
Std.Time.PlainDate.fromLeanDateString : String → Except String Std.Time.PlainDate
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.isRat_pow : ∀ {α : Type u_1} [inst : Ring α] {f : α → ℕ → α} {a : α} {an cn : ℤ} {ad b b' cd : ℕ},
  f = HPow.hPow →
    Mathlib.Meta.NormNum.IsRat a an ad →
      Mathlib.Meta.NormNum.IsNat b b' → an.pow b' = cn → ad.pow b' = cd → Mathlib.Meta.NormNum.IsRat (f a b) cn cd
-- Mathlib.NumberTheory.Height.Basic
Finsupp.logHeight_eq_log_mulHeight : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {α : Type u_4} (x : α →₀ K),
  Height.logHeight ⇑x = Real.log (Height.mulHeight ⇑x)
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.neg_add_cancel_right : ∀ {α : Type u} [inst : SubtractionMonoid α] {b : α}, IsAddUnit b → ∀ (a : α), a + -b + b = a
-- Init.Data.SInt.Basic
instMulInt64 : Mul Int64
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.Forall.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (x : α) → motive [x])
  (h_3 : (x : α) → (l : List α) → motive (x :: l)),
  (match [] with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: l => h_3 x l) =
    h_1 ()
-- Mathlib.Combinatorics.Matroid.Dual
/-- **Alias** of `Matroid.setOfPred_dual_isBase_eq`. -/
Matroid.setOf_dual_isBase_eq : ∀ {α : Type u_1} {M : Matroid α}, {B | M✶.IsBase B} = (fun X => M.E \ X) '' {B | M.IsBase B}
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.forM_eq_forM_toList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {m' : Type w → Type w'}
  [inst_2 : Monad m'] [LawfulMonad m'], m.WF → ∀ {f : (a : α) × β a → m' PUnit.{w + 1}}, forM m f = m.toList.forM f
-- Batteries.Data.Array.Lemmas
Array.extract_append_of_stop_le_size_left : ∀ {α : Type u_1} {j i : ℕ} {a b : Array α}, j ≤ a.size → (a ++ b).extract i j = a.extract i j
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mulPow.induct_unfolding : ∀ (pw : Lean.Grind.CommRing.Power) (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Prop),
  motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit) →
    (∀ (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
        pw.varLt p = true →
          motive (Lean.Grind.CommRing.Mon.mult p m)
            (Lean.Grind.CommRing.Mon.mult pw (Lean.Grind.CommRing.Mon.mult p m))) →
      (∀ (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
          pw.varLt p = false →
            p.varLt pw = true →
              motive m (Lean.Grind.CommRing.Mon.mulPow pw m) →
                motive (Lean.Grind.CommRing.Mon.mult p m)
                  (Lean.Grind.CommRing.Mon.mult p (Lean.Grind.CommRing.Mon.mulPow pw m))) →
        (∀ (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
            pw.varLt p = false →
              p.varLt pw = false →
                motive (Lean.Grind.CommRing.Mon.mult p m)
                  (Lean.Grind.CommRing.Mon.mult { x := pw.x, k := pw.k + p.k } m)) →
          ∀ (m : Lean.Grind.CommRing.Mon), motive m (Lean.Grind.CommRing.Mon.mulPow pw m)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.tendsto_cofinite_cofinite : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f]
  [AlgebraicGeometry.QuasiCompact f], Filter.Tendsto (⇑f) Filter.cofinite Filter.cofinite
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.pi : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {ι : Type u_3} [Finite α] {f : ι → α → M},
  (∀ (a : α), Function.HasFiniteMulSupport fun x => f x a) → Function.HasFiniteMulSupport f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ]
  {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β × γ},
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => (f x).2) μ
-- Std.Time.Zoned.RecurringRule
/-- Rule for the start of DST, if any.
 -/
Std.Time.TimeZone.DaylightSavingRule.start : Std.Time.TimeZone.DaylightSavingRule → Option Std.Time.TimeZone.TransitionRule
-- Mathlib.Data.Set.Restrict
Set.domRestrict_extend_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) (g' : β → γ),
  (Set.range f).domRestrict (Function.extend f g g') = fun x => g (Exists.choose ⋯)
-- Mathlib.Data.Set.Image
Set.preimage_inr_range_inl : ∀ {α : Type u_1} {β : Type u_2}, Sum.inr ⁻¹' Set.range Sum.inl = ∅
-- Std.Data.TreeMap.Slice
Std.TreeMap.toList_rio : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.toList_rio._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap α β cmp} {bound : α},
  Std.Slice.toList (Std.Rio.Sliceable.mkSlice t *...bound) = List.filter (fun e => (cmp e.1 bound).isLT) t.toList
-- Mathlib.GroupTheory.Exponent
AddMonoid.one_lt_exponent : ∀ {G : Type u} [inst : AddLeftCancelMonoid G] [Finite G] [Nontrivial G], 1 < AddMonoid.exponent G
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.norm_single : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (i : ι) (a : 𝕜),
  ‖EuclideanSpace.single i a‖ = ‖a‖
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- As a complex of `k`-modules, the standard resolution of the trivial `G`-representation `k` is
homotopy equivalent to the complex which is `k` at 0 and 0 elsewhere.  -/
Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv : (k G : Type u) →
  [inst : CommRing k] →
    [inst_1 : Monoid G] →
      HomotopyEquiv (Rep.standardComplex.forget₂ToModuleCat k G)
        ((ChainComplex.single₀ (ModuleCat k)).obj
          ((CategoryTheory.forget₂ (Rep.{u, u, u} k G) (ModuleCat k)).obj (Rep.trivial k G k)))
-- Mathlib.Logic.Equiv.Prod
Equiv.prodPProd_symm_apply : ∀ {α₂ : Sort u_3} {β₂ : Sort u_6} {α₁ : Type u_9} {β₁ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (a : α₂ ×' β₂),
  (ea.prodPProd eb).symm a = (ea.symm a.fst, eb.symm a.snd)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insertMany_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h : t.WF) {l : List (α × β)} {k k' : α} {v : β},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
      (k, v) ∈ l → Std.DTreeMap.Internal.Impl.Const.get! (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k' = v
-- Mathlib.Analysis.Convex.Cone.Dual
/-- The **double dual of a proper cone** is itself.  -/
ProperCone.dual_flip_dual : ∀ {E : Type u_1} {F : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [IsTopologicalAddGroup E]
  [inst_3 : TopologicalSpace F] [inst_4 : AddCommGroup F] [inst_5 : Module ℝ E] [ContinuousSMul ℝ E]
  [LocallyConvexSpace ℝ E] [inst_8 : Module ℝ F] (p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [inst_9 : p.IsContPerfPair]
  (C : ProperCone ℝ E), ProperCone.dual p.flip ↑(ProperCone.dual p ↑C) = C
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_ulift : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r],
  Ordinal.type (ULift.down ⁻¹'o r) = Ordinal.lift.{v, u} (Ordinal.type r)
-- Init.Data.Char.Lemmas
Char.toNat_val : ∀ {c : Char}, c.val.toNat = c.toNat
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.rootMultiplicity_mul' : ∀ {R : Type u} [inst : CommRing R] {p q : Polynomial R} {x : R},
  Polynomial.eval x (p /ₘ (Polynomial.X - Polynomial.C x) ^ Polynomial.rootMultiplicity x p) *
        Polynomial.eval x (q /ₘ (Polynomial.X - Polynomial.C x) ^ Polynomial.rootMultiplicity x q) ≠
      0 →
    Polynomial.rootMultiplicity x (p * q) = Polynomial.rootMultiplicity x p + Polynomial.rootMultiplicity x q
-- Lean.Meta.Basic
/-- Executes `x` using the given metavariable `LocalContext` and `LocalInstances`.
The type class resolution cache is flushed when executing `x` if its `LocalInstances` are
different from the current ones.  -/
Lean.MVarId.withContext : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Lean.MVarId → n α → n α
-- Mathlib.LinearAlgebra.TensorAlgebra.Basis
/-- `TensorAlgebra R M` is free when `M` is.  -/
TensorAlgebra.instModuleFree : ∀ {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M], Module.Free R (TensorAlgebra R M)
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Capture the `MetaM` state including local context.  -/
Lean.Elab.WF.GuessLex.SavedLocalContext.create : Lean.MetaM Lean.Elab.WF.GuessLex.SavedLocalContext
-- Mathlib.Algebra.Group.Defs
inv_mul_cancel : ∀ {G : Type u_1} [inst : Group G] (a : G), a⁻¹ * a = 1
-- Mathlib.Lean.Meta.Basic
/-- `mkRel n lhs rhs` is `mkAppM n #[lhs, rhs]`, but with optimizations for `Eq` and `Iff`.  -/
Lean.Meta.mkRel : Lean.Name → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `L` is an algebraic extension of a normed field `K` and `y : L` then the spectral norm
`spectralNorm K y : ℝ` of `y` (written `|y|_sp` in the textbooks) is the spectral value of the
minimal polynomial of `y` over `K`.  -/
spectralNorm : (K : Type u_2) → [inst : NormedField K] → (L : Type u_3) → [inst_1 : Field L] → [Algebra K L] → L → ℝ
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
/-- `F` satisfies the (strong) sheaf condition for the pre-`1`-hypercover `E`, then
the multiequalizer diagram attached to `E` is limiting.  -/
CategoryTheory.PreOneHypercover.IsStronglySheafFor.isLimitMultifork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : C} →
      {E : CategoryTheory.PreOneHypercover X} →
        {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} →
          E.IsStronglySheafFor F → CategoryTheory.Limits.IsLimit (E.multifork F)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.forget₂Mon.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Grp.forget₂Mon C = CategoryTheory.inducedFunctor CategoryTheory.Grp.toMon
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_maxView : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced}
  {hr : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size},
  (Std.DTreeMap.Internal.Impl.maxView k v l r hl hr hlr).tree.impl.toListModel ++
      [⟨(Std.DTreeMap.Internal.Impl.maxView k v l r hl hr hlr).k,
          (Std.DTreeMap.Internal.Impl.maxView k v l r hl hr hlr).v⟩] =
    l.toListModel ++ ⟨k, v⟩ :: r.toListModel
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.lift_openEmbedding_toFun : ∀ {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace X']
  [inst_2 : TopologicalSpace Z] [inst_3 : Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z)
  (hf : Topology.IsOpenEmbedding f), ↑(e.lift_openEmbedding hf) = Function.extend f ↑e fun x => Classical.arbitrary Z
-- Mathlib.Computability.StateTransition
StateTransition.EvalsToInTime.mk : {σ : Type u_1} →
  {f : σ → Option σ} →
    {a : σ} →
      {b : Option σ} →
        {m : ℕ} →
          (toEvalsTo : StateTransition.EvalsTo f a b) → toEvalsTo.steps ≤ m → StateTransition.EvalsToInTime f a b m
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_ofReal_re : ∀ (x : ℝ), (Complex.log ↑x).re = Real.log x
-- Mathlib.Order.CompleteLattice.Lemmas
ULift.up_sSup : ∀ {α : Type u_1} [inst : SupSet α] (s : Set α), { down := sSup s } = sSup (ULift.down ⁻¹' s)
-- Mathlib.Order.Notation
_private.Mathlib.Order.Notation.0.Mathlib.Meta.linearOrderToMin : (u : Lean.Level) →
  have a := Mathlib.Meta.linearOrderExpr✝ u;
  Q((a : Type u) → «$a» a → Min a)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Real.nnnorm_rpow_of_nonneg : ∀ {x y : ℝ}, 0 ≤ x → ‖x ^ y‖₊ = ‖x‖₊ ^ y
-- Lean.Util.SCC
Lean.SCC.State : (α : Type) → [BEq α] → [Hashable α] → Type
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- If `c` is a cofork, then `c.op.unop` is isomorphic to `c`.  -/
CategoryTheory.Limits.Cofork.opUnopIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f g : X ⟶ Y} → (c : CategoryTheory.Limits.Cofork f g) → c.op.unop ≅ c
-- Mathlib.Logic.Relation
Equivalence.comap : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop}, Equivalence r → ∀ (f : α → β), Equivalence (Function.onFun r f)
-- Mathlib.Order.BoundedOrder.Basic
eq_bot_mono : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, b ≤ a → a = ⊥ → b = ⊥
-- Mathlib.Data.Set.Pairwise.Lattice
/-- If the suprema of columns are pairwise disjoint and suprema of rows as well, then everything is
pairwise disjoint. Not to be confused with `Set.PairwiseDisjoint.prod`.  -/
Set.PairwiseDisjoint.prod_left : ∀ {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : CompleteLattice α] {s : Set ι} {t : Set ι'} {f : ι × ι' → α},
  (s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')) →
    (t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')) → (s ×ˢ t).PairwiseDisjoint f
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.coindToInd.congr_simp : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G} (A : Rep.{w, u, v} k ↥S)
  [inst_2 : S.FiniteIndex], A.coindToInd = A.coindToInd
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- Only finitely many maximal ideals of `R` divide a given nonzero ideal.  -/
Ideal.finite_factors : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] {I : Ideal R}, I ≠ 0 → {v | v.asIdeal ∣ I}.Finite
-- Lean.CoreM
Lean.Core.Cache.mk.inj : ∀ {instLevelType instLevelValue instLevelType_1 instLevelValue_1 : Lean.Core.InstantiateLevelCache},
  { instLevelType := instLevelType, instLevelValue := instLevelValue } =
      { instLevelType := instLevelType_1, instLevelValue := instLevelValue_1 } →
    instLevelType = instLevelType_1 ∧ instLevelValue = instLevelValue_1
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctorStruct.mk.inj : ∀ {B : Type u₁} {inst : Quiver B} {inst_1 : (a b : B) → Quiver (a ⟶ b)} {C : Type u₂} {inst_2 : Quiver C}
  {inst_3 : (a b : C) → Quiver (a ⟶ b)} {toPrefunctor : B ⥤q C}
  {map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (toPrefunctor.map f ⟶ toPrefunctor.map g)} {toPrefunctor_1 : B ⥤q C}
  {map₂_1 : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (toPrefunctor_1.map f ⟶ toPrefunctor_1.map g)},
  { toPrefunctor := toPrefunctor, map₂ := map₂ } = { toPrefunctor := toPrefunctor_1, map₂ := map₂_1 } →
    toPrefunctor = toPrefunctor_1 ∧ map₂ ≍ map₂_1
-- Std.Http.Data.URI.Encoding
ByteArray.empty.eq_1 : ByteArray.empty = ByteArray.emptyWithCapacity 0
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_symm_toAffineEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), ⇑e.symm = ⇑e.symm
-- Mathlib.Data.Finsupp.SMul
Finsupp.sum_smul_index : ∀ {α : Type u_1} {M : Type u_3} {R : Type u_6} [inst : MulZeroClass R] [inst_1 : AddCommMonoid M] {g : α →₀ R} {b : R}
  {h : α → R → M}, (∀ (i : α), h i 0 = 0) → (b • g).sum h = g.sum fun i a => h i (b * a)