mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Lp.PiLp
LinearIsometryEquiv.piLpCongrLeft_single : ∀ {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} [hp : Fact (1 ≤ p)] [inst : Fintype ι] [inst_1 : Semiring 𝕜]
  {ι' : Type u_5} [inst_2 : Fintype ι'] {E : Type u_6} [inst_3 : SeminormedAddCommGroup E] [inst_4 : Module 𝕜 E]
  [inst_5 : DecidableEq ι] [inst_6 : DecidableEq ι'] (e : ι ≃ ι') (i : ι) (v : E),
  (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) (PiLp.single p i v) = PiLp.single p (e i) v
-- Mathlib.Order.Bounded
Set.bounded_le_inter_le : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
  Set.Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a ≤ b}) ↔ Set.Bounded (fun x1 x2 => x1 ≤ x2) s
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.countKnown.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} (aig : Std.Sat.AIG α) (s : aig.RefVec len)
  (idx acc : ℕ),
  Std.Sat.AIG.RefVec.countKnown.go aig s idx acc =
    if h : idx < len then
      let ref := s.refs[idx];
      have decl := aig.decls[ref.gate];
      match decl with
      | Std.Sat.AIG.Decl.false => Std.Sat.AIG.RefVec.countKnown.go aig s (idx + 1) (acc + 1)
      | x => Std.Sat.AIG.RefVec.countKnown.go aig s (idx + 1) acc
    else acc
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.isHermitian_kernel : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V], (RKHS.kernel H).IsHermitian
-- Mathlib.Algebra.Torsor.Basic
Pi.sdiv_apply : ∀ {I : Type u} {fg : I → Type v} [inst : (i : I) → Group (fg i)] {fp : I → Type w}
  [inst_1 : (i : I) → Torsor (fg i) (fp i)] (p q : (i : I) → fp i) (i : I), (p /ₛ q) i = p i /ₛ q i
-- Mathlib.Control.Fold
Monoid.Foldr.get : {α : Type u} → Monoid.Foldr α → α → α
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instIsMulCommutative_iSup : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] {ι : Type u_1} [inst_4 : StarRing R] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] [inst_7 : StarModule R A] [Nonempty ι] [inst_9 : Preorder ι] [IsDirectedOrder ι]
  {S : ι →o NonUnitalStarSubalgebra R A} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], IsMulCommutative ↥(⨆ i, S i)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseIdxTR.go.eq_3 : ∀ {α : Type u_1} (l : List α) (a : Array α) (x_3 : α) (xs : List α) (n : ℕ),
  List.eraseIdxTR.go✝ l (x_3 :: xs) n.succ a = List.eraseIdxTR.go✝ l xs n (a.push x_3)
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.comp_surjective : ∀ (R : Type u) (A : Type v) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_1}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallySmooth R A] (I : Ideal B),
  I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_inv : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (x : ↥S), ↑x⁻¹ = (↑x)⁻¹
-- Init.Prelude
/-- The implementation of `a &&& b : α`. See `HAnd`.  -/
AndOp.and : {α : Type u} → [self : AndOp α] → α → α → α
-- Lean.Meta.Basic
/-- `inTypeClassResolution := true` when `isDefEq` is invoked at `tryResolve` in the type class
resolution module. We don't use `isDefEqProjDelta` when performing TC resolution due to performance issues.
This is not a great solution, but a proper solution would require a more sophisticated caching mechanism.
 -/
Lean.Meta.Context.inTypeClassResolution : Lean.Meta.Context → Bool
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.EvenHom.ext_iff : ∀ {R : Type u_1} {M : Type u_2} {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  {Q : QuadraticForm R M} {A : Type u_3} {inst_3 : Ring A} {inst_4 : Algebra R A} {x y : CliffordAlgebra.EvenHom Q A},
  x = y ↔ x.bilin = y.bilin
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.restrictScalars_powers : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] {A : Type u_5}
  [inst_2 : CommSemiring A] [inst_3 : Algebra R A] [inst_4 : Module R M] [inst_5 : Module A M] {N : Type u_6}
  [inst_6 : AddCommMonoid N] [inst_7 : Module R N] [inst_8 : Module A N] [inst_9 : IsScalarTower R A M]
  [inst_10 : IsScalarTower R A N] (r : R) (f : M →ₗ[A] N)
  [h : IsLocalizedModule (Submonoid.powers ((algebraMap R A) r)) f], IsLocalizedModule (Submonoid.powers r) (↑R f)
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_inv_app_app_hom_apply : ∀ (J : Type v) [inst : CategoryTheory.SmallCategory J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  (X : (CategoryTheory.Functor J C)ᵒᵖ) (X_1 : C) (t : Opposite.unop X ⟶ (CategoryTheory.Functor.const J).obj X_1),
  (CategoryTheory.ConcreteCategory.hom
        (((CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones J C).inv.app X).app X_1))
      t =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.lift ((Opposite.unop X).op.comp (CategoryTheory.yoneda.obj X_1))
          (CategoryTheory.Limits.Types.coneOfSection ⋯)))
      PUnit.unit
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_diff! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k fallback : α},
        (m₁.diff! m₂).getKeyD k fallback =
          if Std.DTreeMap.Internal.Impl.contains k m₂ = true then fallback else m₁.getKeyD k fallback
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.inclusion_linear : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] {S₁ S₂ : AffineSubspace k P₁} [inst_4 : Nonempty ↥S₁] (h : S₁ ≤ S₂),
  (AffineSubspace.inclusion h).linear = Submodule.inclusion ⋯
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.termN : Lean.ParserDescr
-- Mathlib.Tactic.Linter.Multigoal
/-- The `SyntaxNodeKind`s in `ignoreBranch` correspond to tactics that disable the linter from
their first application until the corresponding proof branch is closed.
Reasons for ignoring these tactics include
* the linter gets confused by the proof management, e.g. `conv`;
* the tactics are *intended* to act on multiple goals, e.g. `repeat`, `any_goals`, `all_goals`, ...

There is some overlap in scope between `exclusions` and `ignoreBranch`.
 -/
_private.Mathlib.Tactic.Linter.Multigoal.0.Mathlib.Linter.Style.multiGoal.ignoreBranch : Std.HashSet Lean.SyntaxNodeKind
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.boxProd_adj_right : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {a : α} {b₁ b₂ : β},
  (G □ H).Adj (a, b₁) (a, b₂) ↔ H.Adj b₁ b₂
-- Mathlib.Geometry.Group.Growth.QuotientInter
Finset.le_card_quotient_add_sq_inter_addSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {H : AddSubgroup G}
  [inst_2 : DecidablePred fun x => x ∈ H] [inst_3 : H.Normal] {A : Finset G},
  -A = A → A.card ≤ (Finset.image (⇑(QuotientAddGroup.mk' H)) A).card * {x ∈ 2 • A | x ∈ H}.card
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.instBEqCancelParams.beq : Lean.Lsp.CancelParams → Lean.Lsp.CancelParams → Bool
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.addSubgroupCongr_symm_apply : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (h : H = K) (x : ↥K),
  ↑((AddEquiv.addSubgroupCongr h).symm x) = ↑x
-- Mathlib.Algebra.Category.BoolRing
BoolRing.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory BoolRing fun x1 x2 => ↑x1 →+* ↑x2
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right : ∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T}
  (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens}
  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US)
  {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT)
  [AlgebraicGeometry.Flat f],
  AlgebraicGeometry.IsAffineOpen US →
    AlgebraicGeometry.IsAffineOpen UT →
      IsCompact ↑UX → CategoryTheory.Mono (AlgebraicGeometry.pushoutSection H hUST hUSX hUY)
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instAddCommGroup : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] →
                        [inst_7 : ContMDiffMul I (↑⊤) G] → AddCommGroup (LeftInvariantDerivation I G)
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.isPositive_self_comp_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (S : E →ₗ[𝕜] F),
  (S ∘ₗ LinearMap.adjoint S).IsPositive
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryLE! : {α : Type u} →
  {β : α → Type v} → [Ord α] → [Inhabited ((a : α) × β a)] → α → Std.DTreeMap.Internal.Impl α β → (a : α) × β a
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.const_sub : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommGroup α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → ∀ (a : α), Function.Antiperiodic (fun x => f (a - x)) c
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {a b : α} {fallback : β},
      (a == b) = true →
        Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = Std.DHashMap.Internal.Raw₀.Const.getD m b fallback
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Version of `fderivWithin_fun_neg` where the function is written `-f` instead of `fun y ↦ -f y`.
For the special case `E = 𝕜` without a `UniqueDiffWithinAt 𝕜 s x` hypothesis, see
`fderivWithin_neg'`.  -/
fderivWithin_neg : ∀ {𝕜 : 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] {f : E → F}
  {x : E} {s : Set E}, UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (-f) s x = -fderivWithin 𝕜 f s x
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- A natural transformation of bifunctors induces a map on chosen ends.  -/
CategoryTheory.Limits.chosenEnd.map : {J : Type u_3} →
  {C : Type u_4} →
    [inst : CategoryTheory.Category.{v_3, u_4} C] →
      [inst_1 : CategoryTheory.Category.{v_4, u_3} J] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] →
            {G : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
              (F ⟶ G) → (CategoryTheory.Limits.chosenEnd F ⟶ CategoryTheory.Limits.chosenEnd G)
-- Mathlib.GroupTheory.Sylow
Sylow.nonempty : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], Nonempty (Sylow p G)
-- Mathlib.Topology.Semicontinuity.Defs
lowerHemicontinuousOn_univ_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  LowerHemicontinuousOn f Set.univ ↔ LowerHemicontinuous f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- The predicate of type `Nat → Prop`, which serves as the conclusion of the
`cooper_left`, `cooper_right`, `cooper_dvd_left`, and `cooper_dvd_right` theorems.

The specific predicate used is determined as follows:
- `cooper_left_split` (if `left` is `true` and `c₃?` is `none`)
- `cooper_right_split` (if `left` is `false` and `c₃?` is `none`)
- `cooper_dvd_left_split` (if `left` is `true` and `c₃?` is `some`)
- `cooper_dvd_right_split` (if `left` is `false` and `c₃?` is `some`)

See `CooperSplit`
 -/
Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred : Type
-- Mathlib.CategoryTheory.Subfunctor.OfSection
CategoryTheory.Subfunctor.ofSection_eq_range' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type (max v w))} {X : Cᵒᵖ}
  (x : F.obj X),
  CategoryTheory.Subfunctor.ofSection x = CategoryTheory.Subfunctor.range (CategoryTheory.uliftYonedaEquiv.symm x)
-- Mathlib.CategoryTheory.Action.Continuous
ContAction.res_map : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {FV : V → V → Type u_2} {CV : V → Type u_3}
  [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_2 : CategoryTheory.ConcreteCategory V FV]
  [inst_3 : CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [inst_4 : Monoid G] [inst_5 : TopologicalSpace G]
  {H : Type u_5} [inst_6 : Monoid H] [inst_7 : TopologicalSpace H] (f : G →ₜ* H) {X Y : ContAction V H} (f_1 : X ⟶ Y),
  (ContAction.res V f).map f_1 = CategoryTheory.ObjectProperty.homMk ((Action.res V ↑f).map f_1.hom)
-- Mathlib.RingTheory.ZariskisMainTheorem
/-- We say that an `R` algebra `S` satisfies the Zariski's main property at a prime `p` of `S`
if there exists `r ∉ p` in the integral closure `S'` of `R` in `S`, such that `S'[1/r] = S[1/r]`.  -/
Algebra.ZariskisMainProperty : (R : Type u_1) → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Ideal S → Prop
-- Lean.Environment
Lean.ConstantKind.quot.sizeOf_spec : sizeOf Lean.ConstantKind.quot = 1
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.whiskerRight_tensorUnit_comp_rightUnitor_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.Functor.LaxMonoidal.ε F))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom) h))
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.contsAux.eq_1 : ∀ {K : Type u_2} [inst : DivisionRing K] (g : GenContFract K), g.contsAux 0 = { a := 1, b := 0 }
-- Mathlib.RingTheory.LaurentSeries
/-- The algebra equivalence between `K⸨X⸩` and the `X`-adic completion of `RatFunc X`  -/
LaurentSeries.LaurentSeriesAlgEquiv : (K : Type u_2) → [inst : Field K] → LaurentSeries K ≃ₐ[K] LaurentSeries.RatFuncAdicCompl K
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.constAlter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] (k : α) (f : Option β → Option β),
  m₁.Equiv m₂ → (Std.DHashMap.Const.alter m₁ k f).Equiv (Std.DHashMap.Const.alter m₂ k f)
-- Lean.Elab.InfoTree.Main
/-- Resets the trees state `t₀`, runs `x` to produce a new trees state `t₁` and sets the state to be
`t₀ ++ (InfoTree.context (PartialContextInfo.parentDeclCtx Γ) <$> t₁)` where `Γ` is the parent decl
name provided by `MonadParentDecl m`.
 -/
Lean.Elab.withSaveParentDeclInfoContext : {m : Type → Type} →
  [Monad m] → [Lean.Elab.MonadInfoTree m] → {α : Type} → [MonadFinally m] → [Lean.Elab.MonadParentDecl m] → m α → m α
-- Mathlib.Data.Set.Function
Set.BijOn.invOn_invFunOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} [inst : Nonempty α],
  Set.BijOn f s t → Set.InvOn (Function.invFunOn f s) f s t
-- Lean.Parser.Command
Lean.Parser.Command.withExporting.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.mk.inj : ∀ {A : Type u_7} {B : Type u_8} {inst : AddMonoid A} {inst_1 : AddMonoid B} {inst_2 : TopologicalSpace A}
  {inst_3 : TopologicalSpace B} {toAddMonoidHom : A →+ B}
  {continuous_toFun : autoParam (Continuous (↑toAddMonoidHom).toFun) ContinuousMap.continuous_toFun._autoParam}
  {toAddMonoidHom_1 : A →+ B}
  {continuous_toFun_1 : autoParam (Continuous (↑toAddMonoidHom_1).toFun) ContinuousMap.continuous_toFun._autoParam},
  { toAddMonoidHom := toAddMonoidHom, continuous_toFun := continuous_toFun } =
      { toAddMonoidHom := toAddMonoidHom_1, continuous_toFun := continuous_toFun_1 } →
    toAddMonoidHom = toAddMonoidHom_1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.alterKey.match_1.eq_2 : ∀ {α : Type u_3} {β : α → Type u_1} (k : α) (motive : Option (β k) → Sort u_2) (v : β k) (h_1 : Unit → motive none)
  (h_2 : (v : β k) → motive (some v)),
  (match some v with
    | none => h_1 ()
    | some v => h_2 v) =
    h_2 v
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffWithinAt.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E} {𝕜' : Type u_4} [inst_3 : NormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {f : E → 𝕜'} {n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f s x → f x ≠ 0 → ContDiffWithinAt 𝕜 n f⁻¹ s x
-- Mathlib.Geometry.Manifold.Notation
Manifold.Elab.FindModelResult.mk.inj : ∀ {model : Lean.Expr} {normedSpaceInfo? : Option Manifold.Elab.NormedSpaceInfo} {model_1 : Lean.Expr}
  {normedSpaceInfo?_1 : Option Manifold.Elab.NormedSpaceInfo},
  { model := model, normedSpaceInfo? := normedSpaceInfo? } =
      { model := model_1, normedSpaceInfo? := normedSpaceInfo?_1 } →
    model = model_1 ∧ normedSpaceInfo? = normedSpaceInfo?_1
-- Mathlib.Combinatorics.SetFamily.Shadow
Finset.upShadow.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (𝒜 : Finset (Finset α)),
  𝒜.upShadow = 𝒜.sup fun s => Finset.image (fun a => insert a s) sᶜ
-- Mathlib.Data.Set.Sups
Set.Nonempty.of_sups_right : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t : Set α}, (s ⊻ t).Nonempty → t.Nonempty
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- Turn a function `f : C(X, ℝ)` into a continuous map into `Set.Icc (-‖f‖) (‖f‖)`,
thereby explicitly attaching bounds.
 -/
ContinuousMap.attachBound : {X : Type u_1} → [inst : TopologicalSpace X] → [inst_1 : CompactSpace X] → (f : C(X, ℝ)) → C(X, ↑(Set.Icc (-‖f‖) ‖f‖))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.diagramIsoPair_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C)
  (X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
  (CategoryTheory.Limits.diagramIsoPair F).inv.app X =
    (match X with
      | { as := CategoryTheory.Limits.WalkingPair.left } =>
        CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.left })
      | { as := CategoryTheory.Limits.WalkingPair.right } =>
        CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.right })).inv
-- Mathlib.Data.Finset.Basic
Finset.disjoint_filter_filter_not : ∀ {α : Type u_1} (s t : Finset α) (p : α → Prop) [inst : DecidablePred p] [inst_1 : (x : α) → Decidable ¬p x],
  Disjoint (Finset.filter p s) ({a ∈ t | ¬p a})
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_of_ker_bot : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_5} [inst : Ring R] [inst_1 : Ring S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module S P] [IsNoetherian S P]
  {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (f : M →ₛₗ[σ] P),
  f.ker = ⊥ → IsNoetherian R M
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_mul_ofNat : ∀ (x y : ℂ) (n : ℕ) [inst : n.AtLeastTwo], x ^ (y * OfNat.ofNat n) = (x ^ y) ^ OfNat.ofNat n
-- Mathlib.Order.OrderIsoNat
RelEmbedding.not_acc : ∀ {α : Type u_1} {r : α → α → Prop} [IsStrictOrder α r] (f : (fun x1 x2 => x1 > x2) ↪r r) (k : ℕ), ¬Acc r (f k)
-- Init.Data.BitVec.Lemmas
BitVec.ule_iff_le : ∀ {w : ℕ} {x y : BitVec w}, x.ule y = true ↔ x ≤ y
-- Init.Data.String.Lemmas.Splits
/-- You might want to invoke `Slice.Pos.Splits.exists_eq_append_singleton` to be able to apply this.  -/
String.Slice.Pos.Splits.of_next : ∀ {t₁ : String} {c : Char} {t₂ : String} {s : String.Slice} {p : s.Pos} {hp : p ≠ s.endPos},
  (p.next hp).Splits (t₁ ++ String.singleton c) t₂ → p.Splits t₁ (String.singleton c ++ t₂)
-- Mathlib.Topology.MetricSpace.Closeds
/-- The distance on `NonemptyCompacts α` is the Hausdorff distance, by construction  -/
Metric.NonemptyCompacts.dist_eq : ∀ {α : Type u_1} [inst : MetricSpace α] {x y : TopologicalSpace.NonemptyCompacts α},
  dist x y = Metric.hausdorffDist ↑x ↑y
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateMulAct.mk.inj : ∀ {α : Type u_1} {f : α → α} {val val_1 : ℕ}, { val := val } = { val := val_1 } → val = val_1
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.instRatCast : {K : Type u_1} →
  [inst : LinearOrder K] → [inst_1 : Field K] → [inst_2 : IsOrderedRing K] → RatCast (ArchimedeanClass.FiniteElement K)
-- Mathlib.Order.Hom.Lattice
LatticeHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Lattice α] →
      [inst_1 : Lattice β] →
        (toSupHom : SupHom α β) →
          (∀ (a b : α), toSupHom.toFun (a ⊓ b) = toSupHom.toFun a ⊓ toSupHom.toFun b) → LatticeHom α β
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.repr_unitsSMul : ∀ {ι : Type u_1} {R₂ : Type u_3} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : CommSemiring R₂]
  [inst_2 : Module R₂ M] (e : Module.Basis ι R₂ M) (w : ι → R₂ˣ) (v : M) (i : ι),
  ((e.unitsSMul w).repr v) i = (w i)⁻¹ • (e.repr v) i
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.GoalM.run' : Lean.Meta.Grind.Goal → Lean.Meta.Grind.GoalM Unit → Lean.Meta.Grind.GrindM Lean.Meta.Grind.Goal
-- Std.Do.SPred.SVal
_private.Std.Do.SPred.SVal.0.Std.Do.SVal.curry.match_1.splitter : {α : Type u_1} →
  (motive : (σs : List (Type u_1)) → (Std.Do.SVal.StateTuple σs → α) → Sort u_2) →
    (σs : List (Type u_1)) →
      (f : Std.Do.SVal.StateTuple σs → α) →
        ((f : Std.Do.SVal.StateTuple [] → α) → motive [] f) →
          ((head : Type u_1) →
              (tail : List (Type u_1)) → (f : Std.Do.SVal.StateTuple (head :: tail) → α) → motive (head :: tail) f) →
            motive σs f
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isClosedMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y), IsClosedMap ⇑h
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- `HasImage f` means that there exists an image factorisation of `f`.  -/
CategoryTheory.Limits.HasImage : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → Prop
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.tendsto_nhds_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {ι : Type u_3} {f : α → β}
  {g : ι → α} {a : Filter ι} {b : α}, Isometry f → (Filter.Tendsto g a (nhds b) ↔ Filter.Tendsto (f ∘ g) a (nhds (f b)))
-- Mathlib.LinearAlgebra.Pi
Submodule.pi_top : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] (s : Set ι), (Submodule.pi s fun i => ⊤) = ⊤