mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- A section `s` of `V` is `C^k` on a trivialisation domain `e.baseSet` iff each of its
coefficients `(LinearMap.piApply (b.localFrameCoeff e i) s)` in a local frame near `x` is  -/
contMDiffOn_baseSet_iff_localFrameCoeff : ∀ {𝕜 : 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]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {k : WithTop ℕ∞}
  [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜] [ContMDiffVectorBundle k F V I],
  ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x => ⟨x, s x⟩) e.baseSet ↔
    ∀ (i : ι),
      ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) k ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s)
        e.baseSet
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.le_one' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν → ∀ (a : α) (q : ℚ), ∀ᵐ (c : β) ∂ν a, f (a, c) q ≤ 1
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.mem_supported' : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {s : Set α} (p : α →₀ M), p ∈ Finsupp.supported M R s ↔ ∀ x ∉ s, p x = 0
-- Mathlib.Data.List.Sublists
List.sublistsLenAux.eq_1 : ∀ {α : Type u} {β : Type v} (x : List α) (x_1 : List α → β) (x_2 : List β),
  List.sublistsLenAux 0 x x_1 x_2 = x_1 [] :: x_2
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.natCast_def : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : NatCast M] (n : ℕ), (↑fun x => ↑n) = ↑n
-- Mathlib.Topology.UniformSpace.UniformEmbedding
Equiv.isUniformEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] (f : α ≃ β),
  UniformContinuous ⇑f → UniformContinuous ⇑f.symm → IsUniformEmbedding ⇑f
-- Mathlib.Algebra.Order.Group.Synonym
toColex_vadd' : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α), toColex b +ᵥ a = b +ᵥ a
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.pairwise_toList_lt : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.Rxc.IsAlwaysFinite α],
  List.Pairwise (fun a b => a < b) r.toList
-- Batteries.Recycling.MonadSatisfying.Array
_private.Batteries.Recycling.MonadSatisfying.Array.0.Array.foldlM.loop.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (i' : ℕ) (h_1 : Unit → motive 0) (h_2 : (i' : ℕ) → motive i'.succ),
  (match i'.succ with
    | 0 => h_1 ()
    | i'.succ => h_2 i') =
    h_2 i'
-- Init.Data.List.MapIdx
/-- Auxiliary for `mapIdxM`:
`mapIdxM.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]`  -/
List.mapIdxM.go : {m : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_1} → [Monad m] → (ℕ → α → m β) → List α → Array β → m (List β)
-- Aesop.Stats.Basic
Aesop.enableStatsCollection : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → m Bool
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.mul_vle_mul_iff_right`. -/
ValuativeRel.vle_mul_left_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, 0 <ᵥ x → (x * y ≤ᵥ x * z ↔ y ≤ᵥ z)
-- Mathlib.Analysis.Meromorphic.Basic
/-- With our definitions, `MeromorphicAt f x` depends only on the values of `f` on a punctured
neighbourhood of `x` (not on `f x`)  -/
MeromorphicAt.congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E}, MeromorphicAt f x → f =ᶠ[nhdsWithin x {x}ᶜ] g → MeromorphicAt g x
-- Batteries.Tactic.GeneralizeProofs
/-- Generalize proofs in the hypotheses `fvars` and, if `target` is true, the target.
Returns the fvars for the generalized proofs and the new goal.

If a hypothesis is a proposition and a `let` binding, this will clear the value of the let binding.

If a hypothesis is a proposition that already appears in the local context, it will be eliminated.

Only *nontrivial* proofs are generalized. These are proofs that aren't of the form `f a b ...`
where `f` is atomic and `a b ...` are bound variables.
These sorts of proofs cannot be meaningfully generalized, and also these are the sorts of proofs
that are left in a term after generalization.
 -/
Lean.MVarId.generalizeProofs : Lean.MVarId →
  Array Lean.FVarId →
    Bool → optParam Batteries.Tactic.GeneralizeProofs.Config { } → Lean.MetaM (Array Lean.Expr × Lean.MVarId)
-- Mathlib.ModelTheory.Graph
FirstOrder.Language.Theory.simpleGraph_isSatisfiable : FirstOrder.Language.Theory.simpleGraph.IsSatisfiable
-- Mathlib.Algebra.Group.AddChar
/-- An additive character maps integer scalar multiples to integer powers.  -/
AddChar.map_zsmul_eq_zpow : ∀ {A : Type u_1} {M : Type u_2} [inst : AddGroup A] [inst_1 : DivisionMonoid M] (ψ : AddChar A M) (n : ℤ) (a : A),
  ψ (n • a) = ψ a ^ n
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.GradedNatTrans.mk.injEq : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D}
  (app : (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X)
  (naturality :
    ∀ (X Y : C),
      CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (app Y))
            (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (app X) (G.map X Y))
          (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y)))
  (app_1 : (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X)
  (naturality_1 :
    ∀ (X Y : C),
      CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (app_1 Y))
            (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (app_1 X) (G.map X Y))
          (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))),
  ({ app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 }) = (app = app_1)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
/-- **Alias** of `SimpleGraph.Walk.setOfPred_length_eq_add_one`. -/
SimpleGraph.Walk.setOf_length_eq_add_one : ∀ {V : Type u} (G : SimpleGraph V) (u v : V) (n : ℕ),
  {p | p.length = n + 1} = ⋃ w, ⋃ (h : G.Adj u w), SimpleGraph.Walk.cons h '' {p' | p'.length = n}
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instZero : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] →
        {X : Type u_2} → [inst_2 : AddAction R X] → [Zero X] → Zero (AddOreLocalization S X)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_sub_pi : ∀ (x : ℝ), Real.cos (x - Real.pi) = -Real.cos x
-- Mathlib.Algebra.Ring.Defs
/-- **Alias** of `add_sq`. -/
add_pow_two : ∀ {α : Type u} [inst : CommSemiring α] (a b : α), (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instMaxOfSeparatelyContinuousMul.eq_1 : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : SeparatelyContinuousMul G],
  OpenNormalSubgroup.instMaxOfSeparatelyContinuousMul =
    { max := fun U V => { toOpenSubgroup := U.toOpenSubgroup ⊔ V.toOpenSubgroup, isNormal' := ⋯ } }
-- Lean.Util.Trace
Lean.TraceElem.msg : Lean.TraceElem → Lean.MessageData
-- Mathlib.Geometry.Euclidean.Incenter
/-- A touchpoint is where an exsphere of a simplex is tangent to one of the faces.  -/
Affine.Simplex.touchpoint : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] →
            {n : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → Finset (Fin (n + 1)) → Fin (n + 1) → P
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.ext_hom : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  {s t : CategoryTheory.Limits.Cofork f g} (i : s.pt ≅ t.pt)
  (w : autoParam (CategoryTheory.CategoryStruct.comp s.π i.hom = t.π) CategoryTheory.Limits.Cofork.ext._auto_1),
  (CategoryTheory.Limits.Cofork.ext i w).hom = CategoryTheory.Limits.Cofork.mkHom i.hom w
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ord_le_ord_iff : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] {x y : ↥X} (hx : Order.coheight x = 1) (hy : Order.coheight y = 1)
  {f g : ↑X.functionField},
  f ≠ 0 →
    g ≠ 0 →
      (AlgebraicGeometry.Scheme.ord f x ≤ AlgebraicGeometry.Scheme.ord g y ↔
        (AlgebraicGeometry.Scheme.ordHom x hx) f ≤ (AlgebraicGeometry.Scheme.ordHom y hy) g)
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.pairwise_coprime_X_sub_C : ∀ {K : Type u_1} [inst : Field K] {I : Type v} {s : I → K},
  Function.Injective s → Pairwise (Function.onFun IsCoprime fun i => Polynomial.X - Polynomial.C (s i))
-- Mathlib.CategoryTheory.Shift.Basic
/-- Shifting by zero is the identity functor.  -/
CategoryTheory.shiftZero : {C : Type u} →
  (A : Type u_1) →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] → (X : C) → (CategoryTheory.shiftFunctor C 0).obj X ≅ X
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trStmts₁.match_1.eq_3 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ')
  (h_1 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k₁ k₂ : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.move p k₁ k₂ q → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.K') →
        (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.push k s q → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 :
    (Q : Turing.PartrecToTM2.Λ') →
      (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') →
        Q = Turing.PartrecToTM2.Λ'.read q → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.clear p k q → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.copy → motive q.copy)
  (h_6 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.succ → motive q.succ)
  (h_7 : (Q q₁ q₂ : Turing.PartrecToTM2.Λ') → Q = q₁.pred q₂ → motive (q₁.pred q₂))
  (h_8 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.Cont') → Q = Turing.PartrecToTM2.Λ'.ret k → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match Turing.PartrecToTM2.Λ'.read q with
    | Q@h:(Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) => h_1 Q p k₁ k₂ q h
    | Q@h:(Turing.PartrecToTM2.Λ'.push k s q) => h_2 Q k s q h
    | Q@h:(Turing.PartrecToTM2.Λ'.read q) => h_3 Q q h
    | Q@h:(Turing.PartrecToTM2.Λ'.clear p k q) => h_4 Q p k q h
    | Q@h:q.copy => h_5 Q q h
    | Q@h:q.succ => h_6 Q q h
    | Q@h:(q₁.pred q₂) => h_7 Q q₁ q₂ h
    | Q@h:(Turing.PartrecToTM2.Λ'.ret k) => h_8 Q k h) =
    h_3 (Turing.PartrecToTM2.Λ'.read q) q ⋯
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.isClosed_sphere : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, IsClosed (Metric.sphere x ε)
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a limit for `F : Jᵒᵖ ⥤ C` into a colimit for `F.rightOp : J ⥤ Cᵒᵖ.`  -/
CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp : {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.rightOp} →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeRightOp c) →
              CategoryTheory.Limits.IsColimit c
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.withBRecOnArgs : (Array Lean.Expr → Array Lean.Expr → Lean.MetaM Unit) → Lean.Meta.IndPredBelow.Context✝ → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Sites.Sheafification
/-- The sheafification functor, left adjoint to the inclusion.  -/
CategoryTheory.presheafToSheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₂) →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          [CategoryTheory.HasWeakSheafify J A] →
            CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
/-- Evaluating a product of functors amounts to taking the product of the evaluations.  -/
CategoryTheory.Limits.piObjIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
        {α : Type w} →
          [inst_2 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C] →
            (f : α → CategoryTheory.Functor D C) → (d : D) → (∏ᶜ f).obj d ≅ ∏ᶜ fun s => (f s).obj d
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.ofList_singleton : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α} {v : β}, Std.TreeMap.ofList [(k, v)] cmp = ∅.insert k v
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_coprod_of_isSeparator_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (G H : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct G H],
  CategoryTheory.IsSeparator G → CategoryTheory.IsSeparator (G ⨿ H)
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFacAux.eq_def : ∀ (n x : ℕ),
  n.minFacAux x =
    have k := x;
    if n < k * k then n else if k ∣ n then k else n.minFacAux (k + 2)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHint.mk.sizeOf_spec : ∀ (position : Lean.Lsp.Position) (label : Lean.Lsp.InlayHintLabel) (kind? : Option Lean.Lsp.InlayHintKind)
  (textEdits? : Option (Array Lean.Lsp.TextEdit)) (tooltip? : Option Lean.Lsp.InlayHintTooltip)
  (paddingLeft? paddingRight? : Option Bool) (data? : Option Lean.Json),
  sizeOf
      { position := position, label := label, kind? := kind?, textEdits? := textEdits?, tooltip? := tooltip?,
        paddingLeft? := paddingLeft?, paddingRight? := paddingRight?, data? := data? } =
    1 + sizeOf position + sizeOf label + sizeOf kind? + sizeOf textEdits? + sizeOf tooltip? + sizeOf paddingLeft? +
        sizeOf paddingRight? +
      sizeOf data?
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.pmap_congr : ∀ {m : Type w → Type w'} {α : Type u} {β : Type v} [inst : Monad m] [LawfulMonad m] {x y : Std.Iterators.HetT m α}
  {f : (a : α) → x.Property a → β} (h : x = y), x.pmap f = y.pmap fun a ha => f a ⋯
-- Mathlib.MeasureTheory.Integral.TorusIntegral
/-- In dimension one, `torusIntegral` is the same as `circleIntegral`
(up to the natural equivalence between `ℂ` and `Fin 1 → ℂ`).  -/
torusIntegral_dim1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : (Fin 1 → ℂ) → E) (c : Fin 1 → ℂ)
  (R : Fin 1 → ℝ), (∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => z
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.mk'.inj : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {functor : CategoryTheory.Functor C D} {inverse : CategoryTheory.Functor D C}
  {unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse}
  {counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D}
  {functor_unitIso_comp :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (functor.map (unitIso.hom.app X)) (counitIso.hom.app (functor.obj X)) =
          CategoryTheory.CategoryStruct.id (functor.obj X))
      CategoryTheory.Equivalence.functor_unitIso_comp._autoParam}
  {functor_1 : CategoryTheory.Functor C D} {inverse_1 : CategoryTheory.Functor D C}
  {unitIso_1 : CategoryTheory.Functor.id C ≅ functor_1.comp inverse_1}
  {counitIso_1 : inverse_1.comp functor_1 ≅ CategoryTheory.Functor.id D}
  {functor_unitIso_comp_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (functor_1.map (unitIso_1.hom.app X))
            (counitIso_1.hom.app (functor_1.obj X)) =
          CategoryTheory.CategoryStruct.id (functor_1.obj X))
      CategoryTheory.Equivalence.functor_unitIso_comp._autoParam},
  { functor := functor, inverse := inverse, unitIso := unitIso, counitIso := counitIso,
        functor_unitIso_comp := functor_unitIso_comp } =
      { functor := functor_1, inverse := inverse_1, unitIso := unitIso_1, counitIso := counitIso_1,
        functor_unitIso_comp := functor_unitIso_comp_1 } →
    functor = functor_1 ∧ inverse = inverse_1 ∧ unitIso ≍ unitIso_1 ∧ counitIso ≍ counitIso_1
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
/-- Assuming `G` is preconnected and `K` not empty, given any connected component `C` outside of `K`,
there exists a vertex `k ∈ K` adjacent to a vertex `v ∈ C`.
 -/
SimpleGraph.ComponentCompl.exists_adj_boundary_pair : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V},
  G.Preconnected → K.Nonempty → ∀ (C : G.ComponentCompl K), ∃ ck, ck.1 ∈ C ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2
-- Mathlib.Geometry.Manifold.Immersion
/-- `f : M → N` is a `C^n` immersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
around `x` and `f x`, respectively such that in these charts, `f` looks like `u ↦ (u, 0)`.
This version does not assume that `f` maps `φ.source` to `ψ.source`,
but that `f` is continuous at `x`.  -/
Manifold.IsImmersionAt.mk_of_continuousAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M},
  ContinuousAt f x →
    ∀ (equiv : (E × F) ≃L[𝕜] E'') (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G),
      x ∈ domChart.source →
        f x ∈ codChart.source →
          domChart ∈ IsManifold.maximalAtlas I n M →
            codChart ∈ IsManifold.maximalAtlas J n N →
              Set.EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun x => (x, 0))
                  (domChart.extend I).target →
                Manifold.IsImmersionAt I J n f x
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.universallyClosed_fst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hg : AlgebraicGeometry.UniversallyClosed g],
  AlgebraicGeometry.UniversallyClosed (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Topology.Order.WithTop
TopologicalSpace.instSecondCountableTopologyWithTop : ∀ {ι : Type u_1} [inst : Preorder ι] [ts : TopologicalSpace ι] [ht : OrderTopology ι] [SecondCountableTopology ι],
  SecondCountableTopology (WithTop ι)
-- Lean.Elab.Command
/-- Lift the `TermElabM` monadic action `x` into a `CommandElabM` monadic action.

Note that `x` is executed with an empty message log. Thus, `x` cannot modify/view messages produced by
previous commands.

If you need to access the free variables corresponding to the ones declared using the `variable` command,
consider using `runTermElabM`.

Recall that `TermElabM` actions can automatically lift `MetaM` and `CoreM` actions.
Example:
```
public import Lean

open Lean Elab Command Meta

def printExpr (e : Expr) : MetaM Unit := do
  IO.println s!"{← ppExpr e} : {← ppExpr (← inferType e)}"

#eval
  liftTermElabM do
    printExpr (mkConst ``Nat)
```
 -/
Lean.Elab.Command.liftTermElabM : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.Command.CommandElabM α
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The condition that a functor `F` has a pointwise right Kan extension along `L`: it means
that it has a pointwise right Kan extension at any object.  -/
CategoryTheory.Functor.HasPointwiseRightKanExtension : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            CategoryTheory.Functor C D → CategoryTheory.Functor C H → Prop
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addU_of_Z_eq_zero_right : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F}, Q 2 = 0 → WeierstrassCurve.Projective.addU P Q = 0
-- Mathlib.Algebra.Quaternion
Quaternion.im_add : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R), (a + b).im = a.im + b.im
-- Lean.Attributes
Lean.Attribute.erase : Lean.Name → Lean.Name → Lean.AttrM Unit
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.ofList_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k : α}
  {v : β} {tl : List (α × β)},
  Std.ExtDHashMap.Const.ofList ((k, v) :: tl) = Std.ExtDHashMap.Const.insertMany (∅.insert k v) tl
-- Mathlib.Control.Functor.Multivariate
TypeVec.PredLast.eq_1 : ∀ {n : ℕ} (α : TypeVec.{u_1} n) {β : Type u_1} (p : β → Prop) (i : Fin2 n),
  α.PredLast p =
    match (motive := (x : Fin2 (n + 1)) → (α ::: β) x → Prop) i.fs with
    | a.fs => fun x => True
    | Fin2.fz => p
-- Lean.Environment
_private.Lean.Environment.0.Lean.VisibilityMap.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] («private» «public» : α),
  sizeOf { «private» := «private», «public» := «public» } = 1 + sizeOf «private» + sizeOf «public»
-- Mathlib.Topology.Order.LiminfLimsup
/-- The `limsSup` of a filter `f` is a cluster point of `f`.  -/
ClusterPt.limsSup : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {f : Filter α} [f.NeBot],
  autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f) ClusterPt.limsSup._auto_1 →
    autoParam (Filter.IsBounded (fun x1 x2 => x1 ≤ x2) f) ClusterPt.limsSup._auto_3 → ClusterPt f.limsSup f
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Turn an exact functor into a left exact functor.  -/
CategoryTheory.LeftExactFunctor.ofExact : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor (C ⥤ₑ D) (C ⥤ₗ D)