mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trCont.match_1.eq_4 : ∀ (motive : Turing.ToPartrec.Cont → Sort u_1) (c : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont)
  (h_1 : Unit → motive Turing.ToPartrec.Cont.halt)
  (h_2 :
    (c : Turing.ToPartrec.Code) →
      (a : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₁ c a k))
  (h_3 : (a : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₂ a k))
  (h_4 : (c : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.comp c k))
  (h_5 : (c : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.fix c k)),
  (match Turing.ToPartrec.Cont.comp c k with
    | Turing.ToPartrec.Cont.halt => h_1 ()
    | Turing.ToPartrec.Cont.cons₁ c a k => h_2 c a k
    | Turing.ToPartrec.Cont.cons₂ a k => h_3 a k
    | Turing.ToPartrec.Cont.comp c k => h_4 c k
    | Turing.ToPartrec.Cont.fix c k => h_5 c k) =
    h_4 c k
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Adj.not_isIsolated_right : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Adj u v → ¬G.IsIsolated v
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- A product of spaces is locally path-connected iff it is empty, or every factor is locally
path-connected and all but finitely many factors are path-connected.  -/
Pi.locallyPathConnectedSpace_iff : ∀ {ι : Type u_3} {Z : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (Z i)],
  LocallyPathConnectedSpace ((i : ι) → Z i) ↔
    IsEmpty ((i : ι) → Z i) ∨ (∀ (i : ι), LocallyPathConnectedSpace (Z i)) ∧ {i | ¬PathConnectedSpace (Z i)}.Finite
-- Init.Data.Slice.List.Basic
instSliceableListNatListSlice_7 : {α : Type u} → Std.Rio.Sliceable (List α) ℕ (ListSlice α)
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
LieAddGroup.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : AddGroup G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G]
  [toContMDiffAdd : ContMDiffAdd I n G], (ContMDiff I I n fun a => -a) → LieAddGroup I n G
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepSets.biUnion : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : ι → Set (Set Ω)} {s' : Set (Set Ω)}
  {u : Set ι},
  (∀ n ∈ u, ProbabilityTheory.CondIndepSets m' hm' (s n) s' μ) →
    ProbabilityTheory.CondIndepSets m' hm' (⋃ n ∈ u, s n) s' μ
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.mapEmbedding_isLoop_iff : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {e : α} {f : α ↪ β}, (M.mapEmbedding f).IsLoop (f e) ↔ M.IsLoop e
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharThreeJNeZeroNF.mk : ∀ {R : Type u_1} [inst : CommRing R] {W : WeierstrassCurve R}, W.a₁ = 0 → W.a₃ = 0 → W.a₄ = 0 → W.IsCharThreeJNeZeroNF
-- Mathlib.Algebra.Group.End
AddAut.eq_1 : ∀ (M : Type u_7) [inst : Add M], AddAut M = (M ≃+ M)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMonNatIso_inv_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_6 : F.LaxBraided] [inst_7 : F'.LaxBraided] (e : F ≅ F')
  [inst_8 : CategoryTheory.NatTrans.IsMonoidal e.hom] (X : CategoryTheory.CommMon C),
  ((CategoryTheory.Functor.mapCommMonNatIso e).inv.app X).hom.hom = e.inv.app X.X
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- The identity oplax functor.  -/
CategoryTheory.OplaxFunctor.id : (B : Type u₁) → [inst : CategoryTheory.Bicategory B] → CategoryTheory.OplaxFunctor B B
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
/-- **Alias** of `SimpleGraph.Walk.setOfPred_length_eq_zero_of_ne`. -/
SimpleGraph.set_walk_length_zero_eq_of_ne : ∀ {V : Type u} (G : SimpleGraph V) {u v : V}, u ≠ v → {p | p.length = 0} = ∅
-- Mathlib.Analysis.Quaternion
Quaternion.linearIsometryEquivTuple_apply : ∀ (a : Quaternion ℝ), Quaternion.linearIsometryEquivTuple a = !₂[a.re, a.imI, a.imJ, a.imK]
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.commRingEquiv_single_zero : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  (m : M),
  AddMonoidAlgebra.commRingEquiv (AddMonoidAlgebra.single m 1) = AddMonoidAlgebra.single 0 (AddMonoidAlgebra.single m 1)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateCol_inj : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} [Nonempty ι] {v w : m → α},
  Matrix.replicateCol ι v = Matrix.replicateCol ι w ↔ v = w
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.ordered_keys_toList : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) t.toList
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- Weighted homogeneous power series  -/
MvPowerSeries.IsWeightedHomogeneous : {σ : Type u_1} → {R : Type u_2} → [Semiring R] → (σ → ℕ) → MvPowerSeries σ R → ℕ → Prop
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instIsAndAnd : ∀ (σs : List (Type u_1)) (Q₁ Q₂ : Std.Do.SPred σs), Std.Do.SPred.Tactic.IsAnd spred(Q₁ ∧ Q₂) Q₁ Q₂
-- Mathlib.RingTheory.PowerBasis
PowerBasis.minpolyGen.eq_1 : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] (pb : PowerBasis A S),
  pb.minpolyGen = Polynomial.X ^ pb.dim - ∑ i, Polynomial.C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * Polynomial.X ^ ↑i
-- Mathlib.Analysis.SpecialFunctions.Sqrt
ContDiff.sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞},
  ContDiff ℝ n f → (∀ (x : E), f x ≠ 0) → ContDiff ℝ n fun y => √(f y)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGetEntryLT?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.getEntryLT? t₁ k = Std.DTreeMap.Raw.Const.getEntryLT? t₂ k
-- Mathlib.MeasureTheory.Integral.CircleTransform
/-- Given a function `f : ℂ → E`, `circleTransform R z w f` is the function mapping `θ` to
`(2 * ↑π * I)⁻¹ • deriv (circleMap z R) θ • ((circleMap z R θ) - w)⁻¹ • f (circleMap z R θ)`.

If `f` is differentiable and `w` is in the interior of the ball, then the integral from `0` to
`2 * π` of this gives the value `f(w)`.  -/
Complex.circleTransform : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → ℝ → ℂ → ℂ → (ℂ → E) → ℝ → E
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.range_sigmoid : Set.range unitInterval.sigmoid = Set.Ioo 0 1
-- Mathlib.Order.Filter.Germ.OrderedMonoid
Filter.Germ.instCanonicallyOrderedMul : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : Mul β] [inst_1 : LE β] [CanonicallyOrderedMul β],
  CanonicallyOrderedMul (l.Germ β)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  [inst_2 : Inhabited (β a)],
  Std.Internal.List.getValueCast! a (Std.Internal.List.insertEntryIfNew k v l) =
    if h : (k == a) = true ∧ Std.Internal.List.containsKey k l = false then cast ⋯ v
    else Std.Internal.List.getValueCast! a l
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.toList_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β},
  m.WF → (Std.DHashMap.Raw.Const.toArray m).toList = Std.DHashMap.Raw.Const.toList m
-- Mathlib.Data.Finset.Union
Finset.biUnion_subset_iff_forall_subset : ∀ {α : Type u_4} {β : Type u_5} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → Finset β},
  s.biUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
GromovHausdorff.candidatesBDist_mem_candidatesB : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [inst_2 : CompactSpace X]
  [inst_3 : CompactSpace Y] [inst_4 : Nonempty X] [inst_5 : Nonempty Y],
  GromovHausdorff.candidatesBDist X Y ∈ GromovHausdorff.candidatesB✝ X Y
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- **Alias** of `AEMeasurable.div`. -/
AEMeasurable.div' : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Div G] {m : MeasurableSpace α} {f g : α → G}
  {μ : MeasureTheory.Measure α} [MeasurableDiv₂ G], AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f / g) μ
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.norm_deriv_eq : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {ncs : CauSeq ℤ_[p] norm} {F : Polynomial R} {a : ℤ_[p]},
  (∀ (n : ℕ),
      ‖(Polynomial.aeval (↑ncs n)) (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖) →
    ‖(Polynomial.aeval ncs.lim) (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim.eq_1 : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape K C],
  CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F =
    (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F.flip).symm ≪≫
      CategoryTheory.Limits.HasLimit.isoOfNatIso F.uncurryObjFlip ≪≫
        CategoryTheory.Limits.HasLimit.isoOfEquivalence (CategoryTheory.Prod.braiding K J)
            (CategoryTheory.NatIso.ofComponents
              (fun x =>
                CategoryTheory.Iso.refl
                  (((CategoryTheory.Prod.braiding K J).functor.comp (CategoryTheory.Functor.uncurry.obj F)).obj x))
              ⋯) ≪≫
          CategoryTheory.Limits.limitUncurryIsoLimitCompLim F
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.LocalGeneratorsData.IsFiniteType.isFiniteType : ∀ {C : Type u'} {inst : CategoryTheory.Category.{v', u'} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R}
  {inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat}
  {inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat} {p : M.LocalGeneratorsData}
  [self : p.IsFiniteType] (i : p.I), (p.generators i).IsFiniteType
-- Lean.Widget.TaggedText
Lean.Widget.instReprTaggedText : {α : Type u_1} → [Repr α] → Repr (Lean.Widget.TaggedText α)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] [inst_4 : HasDerivedCategory C]
  [inst_5 : HasDerivedCategory D] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact)
  (F : CategoryTheory.Functor C D) [inst_6 : F.Additive] [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F],
  CategoryTheory.ShiftedHom.map hS.singleδ F.mapDerivedCategory =
    CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₃)
      (CategoryTheory.CategoryStruct.comp ⋯.singleδ
        ((CategoryTheory.shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₁)))
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.toSingleMk_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0)
  (hg : CategoryTheory.CategoryStruct.comp (K.d p' p) g = 0),
  CochainComplex.HomComplex.Cocycle.toSingleMk (f - g) h p' hp' ⋯ =
    CochainComplex.HomComplex.Cocycle.toSingleMk f h p' hp' hf -
      CochainComplex.HomComplex.Cocycle.toSingleMk g h p' hp' hg
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.homologyData'_left_π : ∀ {ι : 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]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hk : c.next j = k) (h : (K.sc' i j k).HomologyData),
  (HomologicalComplex.extend.homologyData' K e hj' hi hk h).left.π = h.left.π
-- Mathlib.LinearAlgebra.Span.Basic
/-- Two linear maps are equal on `Submodule.span s` iff they are equal on `s`.  -/
LinearMap.eqOn_span_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {s : Set M} {f g : M →ₛₗ[σ₁₂] M₂}, Set.EqOn ⇑f ⇑g ↑(Submodule.span R s) ↔ Set.EqOn (⇑f) (⇑g) s
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.recordTheoremWithBadKeys : Lean.Meta.SimpTheorem → Lean.Meta.SimpM Unit
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_subtype_mono : ∀ {α : Type u} {p q : α → Prop}, (∀ (x : α), p x → q x) → Cardinal.mk { x // p x } ≤ Cardinal.mk { x // q x }
-- Mathlib.Topology.TietzeExtension
/-- **Alias** of `BoundedContinuousFunction.exists_norm_eq_domRestrict_eq_of_closed`.

---

**Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
set. If `f` is a bounded continuous real-valued function defined on a closed set in a normal
topological space, then it can be extended to a bounded continuous function of the same norm defined
on the whole space.  -/
BoundedContinuousFunction.exists_norm_eq_restrict_eq_of_closed : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : BoundedContinuousFunction ↑s ℝ),
  IsClosed s → ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f
-- Mathlib.Analysis.Analytic.Constructions
/-- `f x / g x` is analytic away from `g x = 0`  -/
AnalyticAt.div : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f g : E → 𝕝}
  {x : E}, AnalyticAt 𝕜 f x → AnalyticAt 𝕜 g x → g x ≠ 0 → AnalyticAt 𝕜 (f / g) x
-- Mathlib.Order.Concept
mem_lowerPolar_singleton : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {a : α} {b : β}, a ∈ lowerPolar r {b} ↔ r a b
-- Mathlib.Order.Hom.Lattice
/-- An order homomorphism from a linear order is a lattice homomorphism.  -/
OrderHomClass.toLatticeHomClass : ∀ {F : Type u_1} (α : Type u_2) (β : Type u_3) [inst : FunLike F α β] [inst_1 : LinearOrder α] [inst_2 : Lattice β]
  [OrderHomClass F α β], LatticeHomClass F α β
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inr_opIso_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.Limits.biprod.opIso P Q).inv =
    CategoryTheory.Limits.biprod.snd.op
-- Mathlib.Topology.Defs.Induced
Topology.IsQuotientMap.mk : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsCoinducing f → Function.Surjective f → Topology.IsQuotientMap f
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nontrivial.mul_right : ∀ {α : Type u_2} [inst : Mul α] [IsRightCancelMul α] [inst_2 : DecidableEq α] {s t : Finset α},
  s.Nontrivial → t.Nonempty → (s * t).Nontrivial
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_map_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  {X Y : CategoryTheory.Endofunctor.Coalgebra G} (f : X ⟶ Y),
  ((CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv adj).inverse.map f).f = f.f
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.ext : ∀ {E : Type u_3} [inst : AddGroup E] {p q : AddGroupSeminorm E}, (∀ (x : E), p x = q x) → p = q
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- A morphism of schemes `X ⟶ Y` is a closed immersion if the underlying
topological map is a closed embedding and the induced stalk maps are surjective.  -/
AlgebraicGeometry.IsClosedImmersion : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- Given an injective presentation `M → I`, the short complex `0 → M → I → N → 0`.  -/
CategoryTheory.InjectivePresentation.shortComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X : C} → CategoryTheory.InjectivePresentation X → CategoryTheory.ShortComplex C
-- Mathlib.Data.Nat.Prime.Defs
Nat.Primes.coeNat : Coe Nat.Primes ℕ
-- Lean.Meta.Sym.Simp.SimpM
/-- Simplifier configuration options.  -/
Lean.Meta.Sym.Simp.Context.config : Lean.Meta.Sym.Simp.Context → Lean.Meta.Sym.Simp.Config
-- Init.Data.String.Lemmas.Order
String.Pos.ofSlice_le_iff : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos},
  String.Pos.ofSlice p ≤ q ↔ ∀ (h₁ : q ≤ p₁), ∃ (h₀ : p₀ ≤ q), p ≤ q.slice p₀ p₁ h₀ h₁
-- Lean.Environment
_private.Lean.Environment.0.Lean.finalizeImport.unsafe_impl_6 : Lean.Environment → BaseIO Lean.Environment
-- Mathlib.Algebra.Lie.Basic
lie_skew : ∀ {L : Type v} [inst : LieRing L] (x y : L), -⁅y, x⁆ = ⁅x, y⁆
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.FullyFaithful.mapAddMon_preimage_hom : ∀ {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.Monoidal] (hF : F.FullyFaithful) {X Y : CategoryTheory.AddMon C}
  (f : F.mapAddMon.obj X ⟶ F.mapAddMon.obj Y), (hF.mapAddMon.preimage f).hom = hF.preimage f.hom
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.coconeAt_pt : ∀ {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]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.LeftExtension F) (Y : D),
  (E.coconeAt Y).pt = (CategoryTheory.StructuredArrow.right E).obj Y
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- The (colimit) cocone which defines the fiber of a presheaf.  -/
CategoryTheory.GrothendieckTopology.Point.presheafFiberCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
              (P : CategoryTheory.Functor Cᵒᵖ A) →
                CategoryTheory.Limits.Cocone ((CategoryTheory.CategoryOfElements.π Φ.fiber).op.comp P)
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instDecidableEqOfLawfulEqCmpOfTransCmp : {α : Type u} →
  {cmp : α → α → Ordering} → [Std.LawfulEqCmp cmp] → [Std.TransCmp cmp] → DecidableEq (Std.ExtTreeSet α cmp)
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- If `i ≠ j` and `Xᵢ ← Y → Xⱼ` is a pullback diagram over `Z`, where `Z` is the
coproduct of the `Xᵢ`, then `Y` is initial.  -/
CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsColimitOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {X : ι → C} →
        [CategoryTheory.Limits.CoproductDisjoint X] →
          {i j : ι} →
            i ≠ j →
              {c : CategoryTheory.Limits.Cofan X} →
                CategoryTheory.Limits.IsColimit c →
                  {s : CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j)} →
                    CategoryTheory.Limits.IsLimit s → CategoryTheory.Limits.IsInitial s.pt
-- Mathlib.Algebra.Group.Basic
add_right_comm : ∀ {G : Type u_3} [inst : AddCommSemigroup G] (a b c : G), a + b + c = a + c + b
-- Lean.Meta.Constructions.CtorElim
/-- Specialies `T.CtorElim` for each constructor as `T.ctor.elim`.
 -/
_private.Lean.Meta.Constructions.CtorElim.0.Lean.mkConstructorElim : Lean.Name → Lean.MetaM Unit
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.top_F : ∀ {α : Type u_1} (u : Unit), Filter.Realizer.top.F.f u = Set.univ
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_hom_isHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsCartesian f φ] {a' : 𝒳}
  (φ' : a' ⟶ b) [inst_3 : p.IsCartesian f φ'],
  p.IsHomLift (CategoryTheory.CategoryStruct.id R) (CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso p f φ φ').inv
-- Mathlib.CategoryTheory.Types.Basic
/-- Equivalences (between types in the same universe) are the same as (equivalent to) isomorphisms
of types.  -/
equivEquivIso : {X Y : Type u} → X ≃ Y ≃ (X ≅ Y)
-- Lean.DocString.Syntax
/-- Arguments  -/
Lean.Parser.Category.doc_arg : Lean.Parser.Category
-- Mathlib.Data.Multiset.Filter
Multiset.filter_false : ∀ {α : Type u_1} (s : Multiset α), Multiset.filter (fun x => False) s = 0
-- Mathlib.Topology.Order
/-- A function to a discrete topological space is continuous if and only if the preimage of every
singleton is open.  -/
continuous_discrete_rng : ∀ {β : Type u_2} {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [DiscreteTopology β]
  {f : α → β}, Continuous f ↔ ∀ (b : β), IsOpen (f ⁻¹' {b})
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} [inst_3 : F.IsWellOrderContinuous] {j : J} (hj : Order.IsSuccLimit j)
  (s : ↑(⋯.functor.op.comp (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g)).sections)
  (i : J) (hi : i < j),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯))
      (CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom hj s) =
    (↑s (Opposite.op ⟨i, hi⟩)).f'
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddGroup.toSeminormedAddGroup.eq_1 : ∀ {E : Type u_5} [inst : NormedAddGroup E],
  NormedAddGroup.toSeminormedAddGroup =
    { toNorm := inst.toNorm, toAddGroup := inst.toAddGroup, toPseudoMetricSpace := inst.toPseudoMetricSpace,
      dist_eq := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.mk_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P),
  (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).inr = ι₂