mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.WithTerminal.Cone
instHasColimitsOfSizeUnder : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C)
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₁, u₁} C],
  CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₁, max u₁ v₁} (CategoryTheory.Under X)
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.restrictRestrictAlgEquivMapHom_injective : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K L : IntermediateField F E)
  [inst_3 : Normal F ↥K],
  K ⊔ L = ⊤ → Function.Injective ⇑(IntermediateField.restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.instFullIncl : FintypeCat.incl.Full
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_lt_top : ∀ {r : ENNReal}, ⌊r⌋ₑ < ⊤ ↔ r < ⊤
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.adjoin_rank_le_of_isAlgebraic_left : ∀ {F : Type u_1} [inst : Field F] (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] (L : IntermediateField F K)
  [halg : Algebra.IsAlgebraic F E], Module.rank E ↥(IntermediateField.adjoin E ↑L) ≤ Module.rank F ↥L
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
GenContFract.IntFractPair.exists_succ_nth_stream_of_fr_zero : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K} {n : ℕ}
  {ifp_succ_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n →
    ifp_succ_n.fr = 0 → ∃ ifp_n, GenContFract.IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.ExprWithHoles.getHoles : Lean.Elab.Term.ExprWithHoles✝ → Lean.Elab.TermElabM (Array Lean.MVarId)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.compAlongOrderFinpartition_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n)
  (f : F [×c.length]→L[𝕜] G) (p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F) (v : Fin n → E),
  (c.compAlongOrderedFinpartition f p) v = f (c.applyOrderedFinpartition p v)
-- Mathlib.Order.Antichain
IsAntichain.greatest_iff : ∀ {α : Type u_1} {s : Set α} {a : α} [inst : Preorder α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → (IsGreatest s a ↔ s = {a})
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.ext_iff : ∀ {d : ℤ} {x y : ℤ√d}, x = y ↔ x.re = y.re ∧ x.im = y.im
-- Mathlib.Data.FinEnum
FinEnum.nodup_toList : ∀ {α : Type u} [inst : FinEnum α], (FinEnum.toList α).Nodup
-- Mathlib.Data.Nat.NthRoot.Defs
/-- `Nat.nthRoot n a = ⌊(a : ℝ) ^ (1 / n : ℝ)⌋₊` defined in terms of natural numbers.

We use Newton's method to find a root of $x^n = a$,
so it converges superexponentially fast.  -/
Nat.nthRoot : ℕ → ℕ → ℕ
-- Init.Data.Nat.Basic
Nat.one_ne_zero : 1 ≠ 0
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.over_def : ∀ {X : AlgebraicGeometry.Scheme} (x : ↥X), AlgebraicGeometry.Spec (X.residueField x) ↘ X = X.fromSpecResidueField x
-- Aesop.Forward.State
_private.Aesop.Forward.State.0.Aesop.VariableMap.findMatches.prevSlotMatches : Aesop.VariableMap → Aesop.Slot → Aesop.Substitution → Aesop.PremiseIndex → Aesop.BaseM (Lean.PHashSet Aesop.Match)
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.mk : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : outParam ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop)},
  (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q) →
    (P = AlgebraicGeometry.affineLocally fun {R S} [CommRing R] [CommRing S] => Q) →
      AlgebraicGeometry.HasRingHomProperty P Q
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a limit for `F.rightOp : J ⥤ Cᵒᵖ` into a colimit for `F : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.isColimitOfConeRightOpOfCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ C) →
          {c : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneRightOpOfCocone c) →
              CategoryTheory.Limits.IsColimit c
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.homCategory.ext_iff : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} {α β : F ⟶ G},
  α = β ↔ α.toNatTrans = β.toNatTrans
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadInfo.mk.injEq : ∀ (check : Lean.Elab.Term.Quotation.HeadCheck)
  (onMatch : Lean.Elab.Term.Quotation.HeadCheck → Lean.Elab.Term.Quotation.MatchResult)
  (doMatch :
    (List Lean.Term → Lean.Elab.TermElabM Lean.Term) → Lean.Elab.TermElabM Lean.Term → Lean.Elab.TermElabM Lean.Term)
  (check_1 : Lean.Elab.Term.Quotation.HeadCheck)
  (onMatch_1 : Lean.Elab.Term.Quotation.HeadCheck → Lean.Elab.Term.Quotation.MatchResult)
  (doMatch_1 :
    (List Lean.Term → Lean.Elab.TermElabM Lean.Term) → Lean.Elab.TermElabM Lean.Term → Lean.Elab.TermElabM Lean.Term),
  ({ check := check, onMatch := onMatch, doMatch := doMatch } =
      { check := check_1, onMatch := onMatch_1, doMatch := doMatch_1 }) =
    (check = check_1 ∧ onMatch = onMatch_1 ∧ doMatch = doMatch_1)
-- Mathlib.Data.Int.Order.Basic
/-- **Alias** of the reverse direction of `Int.ofNat_le`. -/
Int.ofNat_le_ofNat_of_le : ∀ {m n : ℕ}, m ≤ n → ↑m ≤ ↑n
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.map_infty : ∀ {X : Type u_1} {Y : Type u_2} (f : X → Y), OnePoint.map f OnePoint.infty = OnePoint.infty
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.mk : {A : Type u_9} →
  {B : Type u_10} →
    [inst : Add A] →
      [inst_1 : Add B] →
        (toEquiv : A ≃ B) → (∀ (x y : A), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y) → A ≃+ B
-- Mathlib.MeasureTheory.Group.Measure
/-- A nonzero left-invariant inner regular measure gives positive mass to any open set.  -/
MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_innerRegular : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] [μ.InnerRegular] [NeZero μ], μ.IsOpenPosMeasure
-- Mathlib.Algebra.Group.Action.Defs
/-- Given a tower of scalar actions `M → α → β`, if we use `SMul.comp`
to pull back both of `M`'s actions by a map `g : N → M`, then we obtain a new
tower of scalar actions `N → α → β`.

This cannot be an instance because it can cause infinite loops whenever the `SMul` arguments
are still metavariables.  -/
SMul.comp.isScalarTower : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : SMul M α] [inst_1 : SMul M β] [inst_2 : SMul α β]
  [IsScalarTower M α β] (g : N → M), IsScalarTower N α β
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.convexCombPair.congr_simp : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] (s s_1 : R) (e_s : s = s_1) (t t_1 : R) (e_t : t = t_1) (hs : 0 ≤ s) (ht : 0 ≤ t)
  (hst : s + t = 1) (x x_1 : M),
  x = x_1 →
    ∀ (y y_1 : M), y = y_1 → Convexity.convexCombPair s t hs ht hst x y = Convexity.convexCombPair s_1 t_1 ⋯ ⋯ ⋯ x_1 y_1
-- Lean.Compiler.ExternAttr
_private.Lean.Compiler.ExternAttr.0.Lean.syntaxToExternAttrData : Lean.Syntax → Lean.AttrM Lean.ExternAttrData
-- Mathlib.Order.CountableSupClosed
/-- A set `s` is closed under countable infimum if for every nonempty countable subset of `s`, any
greatest lower bound of that subset is in `s`.  -/
CountableInfClosed : {α : Type u_2} → [LE α] → Set α → Prop
-- Lean.Server.References
/-- Replaces the worker references in `self` with the `refs` of the worker managing the module `name`
if `version` is newer than the current version managed in `refs`.
 -/
Lean.Server.References.finalizeWorkerRefs : Lean.Server.References →
  Lean.Name → Lean.Lsp.DocumentUri → ℕ → Lean.Lsp.ModuleRefs → Lean.Lsp.Decls → IO Lean.Server.References
-- Mathlib.Analysis.Complex.JensenFormula
/-- **Jensen's Formula**: If `f : ℂ → ℂ` is meromorphic on the closed ball with center `c` and radius
`R`, then the `circleAverage (log ‖f ·‖) c R` equals `log ‖meromorphicTrailingCoeffAt f c‖` plus a
correction term that accounts for the zeros and poles of `f` within the ball.

See `Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const` for a
reformulation in terms of the logarithmic counting function of Value Distribution Theory.
 -/
MeromorphicOn.circleAverage_log_norm : ∀ {c : ℂ} {R : ℝ} {f : ℂ → ℂ},
  R ≠ 0 →
    MeromorphicOn f (Metric.closedBall c |R|) →
      Real.circleAverage (fun x => Real.log ‖f x‖) c R =
        ∑ᶠ (u : ℂ), ↑((MeromorphicOn.divisor f (Metric.closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) +
            ↑((MeromorphicOn.divisor f (Metric.closedBall c |R|)) c) * Real.log R +
          Real.log ‖meromorphicTrailingCoeffAt f c‖
-- Mathlib.Algebra.Module.Pi
Pi.module' : {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {r : (i : I) → Semiring (f i)} →
        {m : (i : I) → AddCommMonoid (g i)} → [(i : I) → Module (f i) (g i)] → Module ((i : I) → f i) ((i : I) → g i)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.coe_toHomeomorph_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (f : M ≃ₜ* N), (↑f).symm = ↑f.symm
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.sigmaFixedByEquivOrbitsProdGroup.eq_1 : ∀ (G : Type u) (X : Type v) [inst : Group G] [inst_1 : MulAction G X],
  MulAction.sigmaFixedByEquivOrbitsProdGroup G X =
    Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans
            (Trans.trans
              (Trans.trans
                (Trans.trans
                  (Trans.trans (Equiv.subtypeProdEquivSigmaSubtype fun g => Membership.mem (MulAction.fixedBy X g)).symm
                    ((Equiv.prodComm G X).subtypeEquiv ⋯))
                  (Equiv.subtypeProdEquivSigmaSubtype fun b a => a ∈ MulAction.stabilizer G b))
                (MulAction.selfEquivSigmaOrbits G X).sigmaCongrLeft')
              (Equiv.sigmaAssoc fun ω b => ↥(MulAction.stabilizer G ↑b)))
            (Equiv.sigmaCongrRight fun x =>
              Equiv.sigmaCongrRight fun x_1 =>
                match x_1 with
                | ⟨val, hb⟩ => (MulAction.stabilizerEquivStabilizerOfOrbitRel hb).toEquiv))
          (Equiv.sigmaCongrRight fun x =>
            Equiv.sigmaEquivProd ↑(MulAction.orbit G x.out) ↥(MulAction.stabilizer G x.out)))
        (Equiv.sigmaCongrRight fun ω => MulAction.orbitProdStabilizerEquivGroup G ω.out))
      (Equiv.sigmaEquivProd (Quotient (MulAction.orbitRel G X)) G)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_coe_eq_self_sub_two_pi_iff : ∀ {θ : ℝ}, (↑θ).toReal = θ - 2 * Real.pi ↔ θ ∈ Set.Ioc Real.pi (3 * Real.pi)
-- Mathlib.Order.Atoms
sSup_atoms_eq_top : ∀ {α : Type u_4} [inst : CompleteLattice α] [IsAtomistic α], sSup {a | IsAtom a} = ⊤
-- Aesop.Search.Queue
Aesop.BestFirstQueue.ActiveGoal.addedInIteration : Aesop.BestFirstQueue.ActiveGoal → Aesop.Iteration
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_bound : ∀ {x : ℝ}, |x| ≤ 1 → |Real.sin x - (x - x ^ 3 / 6)| ≤ |x| ^ 5 / 100
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.elim.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.elim c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.elim c_1) = (c = c_1)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.measure_sdiff'`. -/
MeasureTheory.measure_diff' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasureTheory.NullMeasurableSet t μ → μ t ≠ ⊤ → μ (s \ t) = μ (s ∪ t) - μ t
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.MeasurePreserving.mul_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G)
  [μ.IsMulRightInvariant] (g : G) {X : Type u_3} [inst_4 : MeasurableSpace X] {μ' : MeasureTheory.Measure X}
  {f : X → G}, MeasureTheory.MeasurePreserving f μ' μ → MeasureTheory.MeasurePreserving (fun x => f x * g) μ' μ
-- Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Nat.Partition.card_odds_eq_card_distincts : ∀ (n : ℕ), (Nat.Partition.odds n).card = (Nat.Partition.distincts n).card
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.mem_mapSubmodule_symm_apply : ∀ (R : Type u_1) {A : Type u_3} (M : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] {q : Submodule (Polynomial R) (Module.AEval R M a)} {m : M},
  m ∈ ↑((Module.AEval.mapSubmodule R M a).symm q) ↔ (Module.AEval.of R M a) m ∈ q
-- Mathlib.Topology.Compactness.Lindelof
/-- A set `s` is Lindelöf if every nontrivial filter `f` with the countable intersection
property that contains `s`, has a cluster point in `s`. The filter-free definition is given by
`isLindelof_iff_countable_subcover`.  -/
IsLindelof : {X : Type u} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure_monotone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {Q : CategoryTheory.ObjectProperty C},
  P ≤ Q → P.colimitsClosure J ≤ Q.colimitsClosure J
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.map.eq_1 : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L),
  LieIdeal.map f I = LieSubmodule.lieSpan R L' ↑(Submodule.map (↑f) (LieIdeal.toLieSubalgebra R L I).toSubmodule)
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.opLaxMonoidalPi'_δ : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : (i : I) → CategoryTheory.Functor D (C i)) [inst_4 : (i : I) → (F i).OplaxMonoidal] (X Y : D) (i : I),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Functor.pi' F) X Y i =
    CategoryTheory.Functor.OplaxMonoidal.δ (F i) X Y
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_dite_left : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} (P : Prop)
  [inst_2 : Decidable P] (x : β → P → α),
  (∏'[L] (b : β), if h : P then x b h else 1) = if h : P then ∏'[L] (b : β), x b h else 1
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.mk : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {σ' : S →+* R} →
            [inst_2 : RingHomInvPair σ σ'] →
              [inst_3 : RingHomInvPair σ' σ] →
                {M : Type u_3} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : AddCommMonoid M] →
                      {M₂ : Type u_4} →
                        [inst_6 : TopologicalSpace M₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R M] →
                              [inst_9 : Module S M₂] →
                                (toLinearEquiv : M ≃ₛₗ[σ] M₂) →
                                  autoParam (Continuous (↑toLinearEquiv).toFun)
                                      ContinuousLinearEquiv.continuous_toFun._autoParam →
                                    autoParam (Continuous toLinearEquiv.invFun)
                                        ContinuousLinearEquiv.continuous_invFun._autoParam →
                                      M ≃SL[σ] M₂
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Arrow.preservesColimitsOfShape_leftFunc : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  [CategoryTheory.Limits.HasColimitsOfShape J T],
  CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.Arrow.leftFunc
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] [inst_2 : Inhabited β] (h : t.WF) {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    Std.DTreeMap.Internal.Impl.Const.get! (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)) k =
      Std.DTreeMap.Internal.Impl.Const.get! t k
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `Bundle.Trivialization.localFrameCoeff_apply_of_mem_baseSet`. -/
Bundle.Trivialization.localFrame_coeff_apply_of_mem_baseSet : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V] {ι : Type u_7}
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_14 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F)
  [inst_15 : ContMDiffVectorBundle 1 F V I] {x : M} (hx : x ∈ e.baseSet) (s : (x : M) → V x) (i : ι),
  (Bundle.Trivialization.localFrameCoeff I e b i x) (s x) = ((e.basisAt b hx).repr (s x)) i
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiable.mfderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  MDiffAt f x → UniqueMDiffAt[s] x → mfderiv[s] f x = mfderiv% f x
-- Mathlib.Order.Antichain
IsMaxAntichain.symm : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsMaxAntichain r s → IsMaxAntichain (flip r) s
-- Mathlib.CategoryTheory.Action.Basic
/-- The functor from `Action V H` to `Action V G` induced by a monoid homomorphism
`f : G →* H` is faithful.  -/
Action.instFaithfulRes : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [inst_1 : Monoid G]
  [inst_2 : Monoid H] (f : G →* H), (Action.res V f).Faithful
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.ext' : ∀ {α : Type u_1} [T : TopologicalSpace α] {σ : Type u_5} {F : Ctop α σ},
  (∀ (a : α) (s : Set α), s ∈ nhds a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s) → F.toTopsp = T
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.toDualMap_apply_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, ((InnerProductSpace.toDualMap 𝕜 E) x) y = inner 𝕜 x y
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncateFun_intCast : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (m : ℤ),
  WittVector.truncateFun n ↑m = ↑m
-- Init.Data.SInt.Lemmas
Int64.toBitVec_zero : Int64.toBitVec 0 = 0#64
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasurableEmbedding.absolutelyContinuous_map : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β}
  {μ ν : MeasureTheory.Measure α},
  MeasurableEmbedding f →
    μ.AbsolutelyContinuous ν → (MeasureTheory.Measure.map f μ).AbsolutelyContinuous (MeasureTheory.Measure.map f ν)
-- Mathlib.Data.List.Basic
Function.Surjective.list_map : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Surjective f → Function.Surjective (List.map f)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_homothety : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1) (r : k),
  ⇑(AffineMap.homothety c r) = fun p => r • (p -ᵥ c) +ᵥ c
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.AbelNF.Config.toConfig : Mathlib.Tactic.Abel.AbelNF.Config → Mathlib.Tactic.AtomM.Recurse.Config
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Slow.instDecidableMem : {α : Type u_1} → {cmp : α → α → Ordering} → {x : α} → {t : RBTree.RBNode α} → Decidable (RBTree.RBNode.Mem cmp x t)
-- Init.Data.Nat.Lemmas
Nat.pred_eq_self_iff : ∀ {n : ℕ}, n.pred = n ↔ n = 0
-- Batteries.Data.List.Lemmas
List.length_idxsOf : ∀ {α : Type u_1} {xs : List α} {x : α} {s : ℕ} [inst : BEq α], (List.idxsOf x xs s).length = List.count x xs
-- Mathlib.Analysis.Quaternion
Quaternion.instCompleteSpaceReal : CompleteSpace (Quaternion ℝ)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn.IsCompatible.exists_desc : ∀ {n : ℕ} {X : SSet} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)},
  SSet.horn.IsCompatible f →
    ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (SSet.horn.ι i j hj) φ = f j hj
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageResponse : Type
-- Lean.Elab.PreDefinition.Basic
_private.Lean.Elab.PreDefinition.Basic.0.Lean.Elab.containsRecFn : Array Lean.Name → Lean.Expr → Bool
-- Mathlib.Analysis.Convex.Between
affineSegment_eq_segment : ∀ (R : Type u_1) {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [IsOrderedRing R] (x y : V), affineSegment R x y = segment R x y
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.bi_min_div_two_lt_one : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), b (AkraBazziRecurrence.min_bi b) / 2 < 1
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.mem_admissibleIndex_iff : ∀ {ι : Type u_1} {n : ℕ} [inst : NeZero n] [inst_1 : Fintype ι] {B : BoxIntegral.Box ι} {ν : ι → ℤ},
  ν ∈ BoxIntegral.unitPartition.admissibleIndex n B ↔ BoxIntegral.unitPartition.box n ν ≤ B
-- Mathlib.Data.Multiset.MapFold
Multiset.foldl_cons : ∀ {α : Type u_1} {β : Type v} (f : β → α → β) [inst : RightCommutative f] (b : β) (a : α) (s : Multiset α),
  Multiset.foldl f b (a ::ₘ s) = Multiset.foldl f (f b a) s
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊤` to the domain and codomain of a `SupHom`.  -/
SupHom.withTop : {α : Type u_1} →
  {β : Type u_2} → [inst : SemilatticeSup α] → [inst_1 : SemilatticeSup β] → SupHom α β → SupHom (WithTop α) (WithTop β)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.val_inv_logOrderIso_symm_apply : ∀ {G : Type u_3} [inst : Preorder G] [inst_1 : AddGroup G] (a : G),
  ↑((RelIso.symm WithZero.logOrderIso) a)⁻¹ = (↑(Multiplicative.ofAdd a))⁻¹
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_le_dist_coe_div_sqrt : ∀ (z w : UpperHalfPlane), dist z w ≤ dist ↑z ↑w / √(z.im * w.im)