mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
CategoryTheory.Bicategory.LeftExtension.instCommuteWithOfIsLeftAdjoint : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c} {x : B} {h : c ⟶ x}
  [CategoryTheory.Bicategory.IsLeftAdjoint h] [inst_2 : CategoryTheory.Bicategory.HasLeftKanExtension f g],
  CategoryTheory.Bicategory.Lan.CommuteWith f g h
-- Mathlib.Topology.Defs.Basic
/-- A set is dense in a topological space if every point belongs to its closure.  -/
Dense : {X : Type u} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.Analysis.Analytic.IteratedFDeriv
Equiv.embeddingEquivOfFinite.congr_simp : ∀ (α : Type u_4) [inst : Finite α], Equiv.embeddingEquivOfFinite α = Equiv.embeddingEquivOfFinite α
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.comp_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor E D} (adj₁ : F ⊣ G)
  (adj₂ : H ⊣ I),
  (adj₁.comp adj₂).unit =
    CategoryTheory.CategoryStruct.comp adj₁.unit
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.rightUnitor.inv G)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (F.whiskerLeft adj₂.unit) G)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (F.associator H I).inv G)
            ((F.comp H).associator I G).hom)))
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.val_smul_of_tower : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M) (s : S) (x : ↥p), ↑(s • x) = s • ↑x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_minKey?_iff_isEmpty_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → (t.minKey?.isSome = true ↔ t.isEmpty = false)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.rescaleAlgHom_apply : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (a : σ → R) (f : MvPowerSeries σ R),
  (MvPowerSeries.rescaleAlgHom a) f = (MvPowerSeries.rescale a) f
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F :
        CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
          (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              (obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }).obj) →
                (hom :
                    (i₁ i₂ : ι) →
                      obj i₁ ⟶
                        (F.map (f i₁).op.toLoc).l.toFunctor.obj ((F.map (f i₂).op.toLoc).r.toFunctor.obj (obj i₂))) →
                  autoParam
                      (∀ (i : ι),
                        CategoryTheory.CategoryStruct.comp (hom i i)
                            ((F.map (f i).op.toLoc).adj.counit.toNatTrans.app (obj i)) =
                          CategoryTheory.CategoryStruct.id (obj i))
                      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.counit._autoParam →
                    autoParam
                        (∀ (i₁ i₂ i₃ : ι),
                          CategoryTheory.CategoryStruct.comp (hom i₁ i₂)
                              ((F.map (f i₁).op.toLoc).l.toFunctor.map
                                ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom i₂ i₃))) =
                            CategoryTheory.CategoryStruct.comp (hom i₁ i₃)
                              ((F.map (f i₁).op.toLoc).l.toFunctor.map
                                ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app
                                  ((F.map (f i₃).op.toLoc).r.toFunctor.1 (obj i₃)))))
                        CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc._autoParam →
                      F.DescentDataAsCoalgebra f
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.eq_zero_of_eval_eq_zero : ∀ (σ K : Type u) [inst : Fintype K] [inst_1 : Field K] [Finite σ] (p : MvPolynomial σ K),
  (∀ (v : σ → K), (MvPolynomial.eval v) p = 0) → p ∈ MvPolynomial.restrictDegree σ K (Fintype.card K - 1) → p = 0
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.normOneClass : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] [NontrivialTopology E], NormOneClass (E →L[𝕜] E)
-- Lean.Meta.MethodSpecs
Lean.getMethodSpecTheorems : Lean.Name → String → Lean.MetaM (Option (Array Lean.Name))
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.M : Type → Type
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
CategoryTheory.EnrichedCat.str : (V : Type v) →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : CategoryTheory.EnrichedCat V) → CategoryTheory.EnrichedCategory V ↑C
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.ihom_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] [inst_3 : CategoryTheory.MonoidalClosed C]
  [inst_4 : P.IsMonoidalClosed] (X Y : P.FullSubcategory), (X ⟹ Y).obj = (X.obj ⟹ Y.obj)
-- Mathlib.FieldTheory.Separable
/-- If `IsUnit n` in a `CommRing R`, then `X ^ n - u` is separable for any unit `u`.  -/
Polynomial.separable_X_pow_sub_C_unit : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} (u : Rˣ), IsUnit ↑n → (Polynomial.X ^ n - Polynomial.C ↑u).Separable
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instNeg : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → Neg (CauSeq β abv)
-- Mathlib.CategoryTheory.Idempotents.Basic
CategoryTheory.Idempotents.isIdempotentComplete_of_isIdempotentComplete_opposite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  CategoryTheory.IsIdempotentComplete Cᵒᵖ → CategoryTheory.IsIdempotentComplete C
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- The edges of G consist of the unordered pairs of vertices related by
`G.Adj`. This is the order embedding; for the edge set of a particular graph, see
`SimpleGraph.edgeSet`.

The way `edgeSet` is defined is such that `mem_edgeSet` is proved by `Iff.rfl`.
(That is, `s(v, w) ∈ G.edgeSet` is definitionally equal to `G.Adj v w`.)
 -/
SimpleGraph.edgeSetEmbedding : (V : Type u_2) → SimpleGraph V ↪o Set (Sym2 V)
-- Mathlib.GroupTheory.Perm.List
List.formPerm_apply_head : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (xs : List α), (x :: y :: xs).Nodup → (x :: y :: xs).formPerm x = y
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.UnsatProof.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u}
  {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u}
  {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u}
  {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u}
  {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u}
  {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} (t : Lean.Meta.Grind.Arith.Linear.UnsatProof)
  (F_1 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t)
  (F_3 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t)
  (F_4 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t)
  (F_5 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t)
  (F_6 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t)
  (F_7 : (t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_7 t (Lean.Meta.Grind.Arith.Linear.UnsatProof.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
/-- The property of reflecting equalizers expressed in terms of forks.  -/
CategoryTheory.Limits.isLimitOfIsLimitForkMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {X Y Z : C} →
            {f g : X ⟶ Y} →
              {h : Z ⟶ X} →
                (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) →
                  [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.parallelPair f g) G] →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (G.map h) ⋯) →
                      CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι h w)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_union_eq_left : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : CommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  (∀ a ∈ s₂, a ∉ s₁ → f a = 1) → ∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₁, f a
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.toTransport_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (x : CategoryTheory.Grothendieck F) {c : C} (t : x.base ⟶ c),
  (x.toTransport t).fiber = CategoryTheory.CategoryStruct.id ((F.map t).toFunctor.obj x.fiber)
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Context.mk : Bool → Lean.Meta.Grind.EMatchTheorem → Lean.Expr → Lean.Meta.Grind.EMatch.Context
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- The preimage by a fully faithful functor of a homotopy between morphisms
of homological complexes.  -/
CategoryTheory.Functor.preimageHomotopy : {ι : Type u_2} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {W : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_1, u_3} W] →
              [inst_3 : CategoryTheory.Preadditive W] →
                (F : CategoryTheory.Functor V W) →
                  [inst_4 : F.Additive] →
                    [F.Full] →
                      [F.Faithful] →
                        {K L : HomologicalComplex V c} →
                          {f₁ f₂ : K ⟶ L} →
                            Homotopy ((F.mapHomologicalComplex c).map f₁) ((F.mapHomologicalComplex c).map f₂) →
                              Homotopy f₁ f₂
-- Init.Grind.Module.Basic
Lean.Grind.IntModule.mk : {M : Type u} →
  [toAddCommGroup : Lean.Grind.AddCommGroup M] →
    [nsmul : SMul ℕ M] →
      [zsmul : SMul ℤ M] →
        (∀ (a : M), 0 • a = 0) →
          (∀ (a : M), 1 • a = a) →
            (∀ (n m : ℤ) (a : M), (n + m) • a = n • a + m • a) →
              (∀ (n : ℕ) (a : M), ↑n • a = n • a) → Lean.Grind.IntModule M
-- Mathlib.Order.SemiconjSup
Function.semiconj_of_isLUB : ∀ {α : Type u_1} {G : Type u_4} [inst : PartialOrder α] [inst_1 : Group G] (f₁ f₂ : G →* α ≃o α) {h : α → α},
  (∀ (x : α), IsLUB (Set.range fun g' => (f₁ g')⁻¹ ((f₂ g') x)) (h x)) → ∀ (g : G), Function.Semiconj h ⇑(f₂ g) ⇑(f₁ g)
-- Mathlib.Data.List.Lex
List.lt.eq_1 : ∀ {α : Type u} [inst : LT α], List.lt = List.Lex fun x1 x2 => x1 < x2
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.fst_inl : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0] (x : G₀), (MonoidWithZeroHom.fst G₀ H₀) ((MonoidWithZeroHom.inl G₀ H₀) x) = x
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getEntryGT?_eq_find? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered →
    ∀ {k : α}, Std.DTreeMap.Internal.Impl.getEntryGT? k t = List.find? (fun e => (compare e.fst k).isGT) t.toListModel
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.IsRegularOfDegree.top : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V], ⊤.IsRegularOfDegree (Fintype.card V - 1)
-- Init.Data.Float.Model.Format.Basic
/-- The exponent bias. In packed formats, we store the sum of the true exponent and
the bias.
 -/
Float.Model.Format.exponentBias : Float.Model.Format → ℕ
-- Mathlib.Data.Set.Card
Set.ncard_le_ncard : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → autoParam t.Finite Set.ncard_le_ncard._auto_1 → s.ncard ≤ t.ncard
-- Mathlib.LinearAlgebra.Dimension.Subsingleton
rank_punit : ∀ (R : Type u_1) [inst : Semiring R] [Nontrivial R], Module.rank R PUnit.{u_3 + 1} = 0
-- Std.Async.Timer
/-- `Sleep` can be used to sleep for some duration once.
The underlying timer has millisecond resolution.
 -/
Std.Async.Sleep : Type
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
PresheafOfModules.instMonoModuleCatCarrierObjOppositeRingCatApp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) [CategoryTheory.Mono f] (X : Cᵒᵖ), CategoryTheory.Mono (f.app X)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.instFaithfulMonFunctorOppositeMonCatYonedaAddMon : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaAddMon.Faithful
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.union m₂ ⋯ ⋯).get? k = m₁.get? k
-- Init.Data.Float.Model.Unpacked.Sign
Float.Model.UnpackedFloat.Sign.positive.sizeOf_spec : sizeOf Float.Model.UnpackedFloat.Sign.positive = 1
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instMonoidalMonForget₂Mon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.Grp.forget₂Mon C).Monoidal
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.min_le_agm : ∀ {x y : NNReal}, min x y ≤ x.agm y
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.hasPointwiseLeftKanExtension_iff_of_iso : ∀ {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 L' : CategoryTheory.Functor C D} {F F' : CategoryTheory.Functor C H} (e₁ : L ≅ L') (e₂ : F ≅ F'),
  L.HasPointwiseLeftKanExtension F ↔ L'.HasPointwiseLeftKanExtension F'
-- Mathlib.Geometry.Manifold.Algebra.Monoid
mdifferentiable_mul_left : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : Mul G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I 1 G] {a : G},
  MDiff fun x => a * x
-- Init.Data.List.Nat.TakeDrop
List.take_eq_take_iff : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, List.take i l = List.take j l ↔ min i l.length = min j l.length
-- Lean.Meta.Hint
Lean.Meta.Hint.instToMessageDataSuggestion : Lean.ToMessageData Lean.Meta.Hint.Suggestion
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_meet_of_eq : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R T : l},
  T = Lean.Order.meet Q R →
    Lean.Order.PartialOrder.rel P Q → Lean.Order.PartialOrder.rel P R → Lean.Order.PartialOrder.rel P T
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ_stalkPullbackHom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C Y) (x : ↑X) (U : TopologicalSpace.Opens ↑Y)
  (hU : (CategoryTheory.ConcreteCategory.hom f) x ∈ U),
  CategoryTheory.CategoryStruct.comp (F.germ U ((CategoryTheory.ConcreteCategory.hom f) x) hU)
      (TopCat.Presheaf.stalkPullbackHom C f F x) =
    CategoryTheory.CategoryStruct.comp
      (((TopCat.Presheaf.pullbackPushforwardAdjunction C f).unit.app F).app (Opposite.op U))
      (((TopCat.Presheaf.pullback C f).obj F).germ ((TopologicalSpace.Opens.map f).obj U) x hU)
-- Mathlib.Data.Fintype.EquivFin
/-- Noncomputably get a `Fintype` instance from a `Finite` instance. This is not an
instance because we want `Fintype` instances to be useful for computations.  -/
Fintype.ofFinite : (α : Type u_4) → [Finite α] → Fintype α
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
ContDiffAt.localInverse_apply_image : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕂 E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕂 F] [inst_5 : CompleteSpace E] {f : E → F}
  {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : n ≠ 0),
  hf.localInverse hf' hn (f a) = a
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.of_isLocalization : ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (f : R) [IsLocalization.Away f S],
  AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
-- Lean.Meta.Basic
Lean.Meta.ProjReductionKind.no.sizeOf_spec : sizeOf Lean.Meta.ProjReductionKind.no = 1
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (β_ Y' Y).inv =
    CategoryTheory.CategoryStruct.comp (β_ X' X).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom g f)
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.Simps.val_neg.eq_1 : ∀ {α : Type u} [inst : AddMonoid α] (u : AddUnits α), AddUnits.Simps.val_neg u = ↑(-u)
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
_private.Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue.0.«term_≺_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.instHasSmallObjectArgumentInnerHornInclusions : SSet.innerHornInclusions.HasSmallObjectArgument
-- Lean.Elab.AutoBound
Lean.Elab.isValidAutoBoundLevelName : Lean.Name → Bool → Bool
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.functor_id : ∀ (J : Type u) [inst : LinearOrder J],
  CategoryTheory.SimplicialThickening.functor OrderHom.id =
    CategoryTheory.EnrichedFunctor.id SSet (CategoryTheory.SimplicialThickening J)
-- Mathlib.Data.EReal.Operations
EReal.mul_bot_of_pos : ∀ {x : EReal}, 0 < x → x * ⊥ = ⊥
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapRingHom_comp_algebraMap : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_7} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : AddMonoid M]
  (f : R →+* S),
  (AddMonoidAlgebra.mapRingHom M f).comp (algebraMap R (AddMonoidAlgebra R M)) =
    (algebraMap S (AddMonoidAlgebra S M)).comp f
-- Init.Data.BitVec.Lemmas
BitVec.pow_add : ∀ {w : ℕ} {x : BitVec w} {n m : ℕ}, x ^ (n + m) = x ^ n * x ^ m
-- Mathlib.Data.Nat.PrimeFin
Nat.disjoint_primeFactors : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → (Disjoint a.primeFactors b.primeFactors ↔ a.Coprime b)
-- Mathlib.CategoryTheory.Sums.Associator
/-- Characterizing the composition of the associator and the right inclusion.  -/
CategoryTheory.sum.inrCompAssociator : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (CategoryTheory.Sum.inr_ (C ⊕ D) E).comp (CategoryTheory.sum.associator C D E) ≅
              (CategoryTheory.Sum.inr_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E))
-- Init.SimpLemmas
bne_self_eq_false : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a : α), (a != a) = false
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.comp_antitone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {a : α}, IsLocalMin f a → ∀ {g : β → γ}, Antitone g → IsLocalMax (g ∘ f) a
-- Mathlib.Order.Hom.Lattice
SupHom.instBot : {α : Type u_2} → {β : Type u_3} → [inst : Max α] → [inst_1 : SemilatticeSup β] → [Bot β] → Bot (SupHom α β)
-- Mathlib.Analysis.Analytic.Constructions
/-- If `𝕝` is a normed field extension of `𝕜`, then the inverse map `𝕝 → 𝕝` is `𝕜`-analytic
away from 0.  -/
analyticAt_inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {𝕝 : Type u_8} [inst_1 : NormedDivisionRing 𝕝]
  [inst_2 : NormedAlgebra 𝕜 𝕝] {z : 𝕝}, z ≠ 0 → AnalyticAt 𝕜 Inv.inv z
-- Batteries.Data.List.Basic
List.zipWithLeft'TR.go.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : List α) (a_1 : Array γ),
  (a = [] → False) →
    List.zipWithLeft'TR.go f a [] a_1 = ((List.foldl (fun acc a => acc.push (f a none)) a_1 a).toList, [])
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.coneLift.match_1.splitter : {J : Type u_1} →
  (motive : CategoryTheory.WithTerminal J → Sort u_2) →
    (x : CategoryTheory.WithTerminal J) →
      ((a : J) → motive (CategoryTheory.WithTerminal.of a)) →
        (Unit → motive CategoryTheory.WithTerminal.star) → motive x
-- Mathlib.Algebra.Tropical.Basic
/-- Recursing on an `x' : Tropical R` is the same as recursing on an `x : R` reinterpreted
as a term of `Tropical R` via `trop x`.  -/
Tropical.tropRec : {R : Type u} → {F : Tropical R → Sort v} → ((X : R) → F (Tropical.trop X)) → (X : Tropical R) → F X
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddCommMonCat.FilteredColimits.colimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddCommMonCat),
  AddCommMonCat.FilteredColimits.colimit F = AddCommMonCat.of ↑(AddCommMonCat.FilteredColimits.M F)
-- Init.Data.Int.DivMod.Bootstrap
Int.emod_add_mul_ediv : ∀ (a b : ℤ), a % b + b * (a / b) = a
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesWithinAt.hasFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {s : Set E},
  HasFPowerSeriesWithinAt f p s x → HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) (insert x s) x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_eq_isSome_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α}, t.contains a = (t.get? a).isSome
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.op_map_id_obj : ∀ {X : TopCat} (x : ↑X) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ),
  (TopologicalSpace.OpenNhds.map (CategoryTheory.CategoryStruct.id X) x).op.obj U = U
-- Mathlib.Topology.Constructions
continuous_rangeFactorization_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous (Set.rangeFactorization f) ↔ Continuous f
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.toDigitsCore.eq_2 : ∀ (base x : ℕ) (x_1 : List Char) (fuel : ℕ),
  base.toDigitsCore fuel.succ x x_1 =
    if x / base = 0 then (x % base).digitChar :: x_1
    else base.toDigitsCore fuel (x / base) ((x % base).digitChar :: x_1)