mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mk.sizeOf_spec : ∀ {R : Type u} [inst : NonAssocSemiring R] [inst_1 : SizeOf R] (toSubmonoid : Submonoid R)
  (add_mem' : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier)
  (zero_mem' : 0 ∈ toSubmonoid.carrier),
  sizeOf { toSubmonoid := toSubmonoid, add_mem' := add_mem', zero_mem' := zero_mem' } =
    1 + sizeOf toSubmonoid + sizeOf zero_mem'
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.ofHom_add : ∀ {k : Type u} {G : Type v} {X Y : Type w} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G]
  [inst_3 : AddCommGroup X] [inst_4 : Module k X] [inst_5 : TopologicalSpace X] [inst_6 : IsTopologicalAddGroup X]
  [inst_7 : ContinuousSMul k X] [inst_8 : AddCommGroup Y] [inst_9 : Module k Y] [inst_10 : TopologicalSpace Y]
  [inst_11 : IsTopologicalAddGroup Y] [inst_12 : ContinuousSMul k Y] {ρ : ContRepresentation k G X}
  {σ : ContRepresentation k G Y} (f g : ContIntertwiningMap ρ σ), TopRep.ofHom (f + g) = TopRep.ofHom f + TopRep.ofHom g
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.getTop : Lean.Meta.SynthInstance.SynthM Lean.Meta.SynthInstance.GeneratorNode
-- Mathlib.LinearAlgebra.TensorProduct.Prod
/-- Tensor products distribute over a product on the left .  -/
TensorProduct.prodLeft : (R : Type u_1) →
  (S : Type u_2) →
    (M₁ : Type u_3) →
      (M₂ : Type u_4) →
        (M₃ : Type u_5) →
          [inst : CommSemiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : AddCommMonoid M₁] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : AddCommMonoid M₃] →
                    [inst_5 : Algebra R S] →
                      [inst_6 : Module R M₁] →
                        [inst_7 : Module S M₁] →
                          [inst_8 : IsScalarTower R S M₁] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module R M₃] →
                                [inst_11 : Module S M₂] →
                                  [inst_12 : IsScalarTower R S M₂] →
                                    TensorProduct R (M₁ × M₂) M₃ ≃ₗ[S] TensorProduct R M₁ M₃ × TensorProduct R M₂ M₃
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSemilatticeSup : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [SemilatticeSup β] → SemilatticeSup (l.Germ β)
-- Batteries.Lean.Expr
/-- Like `traverseApp` but ignores metadata.  -/
Lean.Expr.traverseApp' : {m : Type → Type u_1} → [Monad m] → (Lean.Expr → m Lean.Expr) → Lean.Expr → m Lean.Expr
-- Mathlib.Topology.Connected.Basic
IsPreconnected.prod : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {t : Set β},
  IsPreconnected s → IsPreconnected t → IsPreconnected (s ×ˢ t)
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X}, JoinedIn F x y → JoinedIn F y x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.enumMember.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.enumMember = 1
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prodContinuousLinearEquiv_symm_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : Semiring 𝕜] [inst_3 : AddCommGroup α] [inst_4 : AddCommGroup β] [inst_5 : Module 𝕜 α] [inst_6 : Module 𝕜 β]
  (x : α × β), (WithLp.prodContinuousLinearEquiv p 𝕜 α β).symm x = WithLp.toLp p x
-- Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
SSet.instFiniteSigmaObjOfFinite : ∀ {ι : Type v} [Finite ι] (X : ι → SSet) [inst : CategoryTheory.Limits.HasCoproduct X] [∀ (j : ι), (X j).Finite],
  (∐ X).Finite
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle as a ratio of sides.  -/
Orientation.tan_oangle_add_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle x (x + y)).tan = ‖y‖ / ‖x‖
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.Relation.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {i j : E.I₀} [inst_1 : SizeOf C] (obj : C) (fst : obj ⟶ E.X i) (snd : obj ⟶ E.X j)
  (w : CategoryTheory.CategoryStruct.comp fst (E.f i) = CategoryTheory.CategoryStruct.comp snd (E.f j)),
  sizeOf { obj := obj, fst := fst, snd := snd, w := w } = 1 + sizeOf obj + sizeOf fst + sizeOf snd + sizeOf w
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.pullback.congr_simp : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f f_1 : X ⟶ B) (e_f : f = f_1) (g g_1 : Y ⟶ B) (e_g : g = g_1)
  [inst : CompHausLike.HasExplicitPullback f g], CompHausLike.pullback f g = CompHausLike.pullback f_1 g_1
-- Mathlib.Data.Fintype.EquivFin
instInfiniteFinset : ∀ {α : Type u_1} [Infinite α], Infinite (Finset α)
-- Mathlib.RingTheory.Nilpotent.Defs
nilpotencyClass_eq_zero_of_subsingleton : ∀ {R : Type u_1} {x : R} [inst : Zero R] [inst_1 : Pow R ℕ] [Subsingleton R], nilpotencyClass x = 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Integration by parts** (vector-valued). Special case of
`intervalIntegrable.integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right`
where the functions have a one-sided derivative at the endpoints.  -/
intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivWithinAt : ∀ {a b : ℝ} {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra ℝ 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E] [CompleteSpace E]
  [IsScalarTower ℝ 𝕜 E] {u u' : ℝ → 𝕜} {v v' : ℝ → E},
  (∀ x ∈ Set.uIcc a b, HasDerivWithinAt u (u' x) (Set.uIcc a b) x) →
    (∀ x ∈ Set.uIcc a b, HasDerivWithinAt v (v' x) (Set.uIcc a b) x) →
      IntervalIntegrable u' MeasureTheory.volume a b →
        IntervalIntegrable v' MeasureTheory.volume a b →
          ∫ (x : ℝ) in a..b, u x • v' x = u b • v b - u a • v a - ∫ (x : ℝ) in a..b, u' x • v x
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
ModularForm.instFiniteDimensionalComplexRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL : ∀ (k : ℤ), FiniteDimensional ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
-- Mathlib.CategoryTheory.Adjunction.Evaluation
/-- The adjunction showing that evaluation is a right adjoint.  -/
CategoryTheory.evaluationAdjunctionRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D] →
          (c : C) → CategoryTheory.evaluationLeftAdjoint D c ⊣ (CategoryTheory.evaluation C D).obj c
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Satisfying the inhabited linter  -/
CategoryTheory.Limits.strongEpiMonoFactorisationInhabited : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) → [CategoryTheory.StrongEpi f] → Inhabited (CategoryTheory.Limits.StrongEpiMonoFactorisation f)
-- Mathlib.CategoryTheory.Action.Limits
Action.instZeroHom : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} →
      [inst_1 : Monoid G] → [CategoryTheory.Limits.HasZeroMorphisms V] → {X Y : Action V G} → Zero (X ⟶ Y)
-- Mathlib.Data.Nat.Factorization.Defs
/-- `n.factorization` is the finitely supported function `ℕ →₀ ℕ`
mapping each prime factor of `n` to its multiplicity in `n`.  -/
Nat.factorization : ℕ → ℕ →₀ ℕ
-- Mathlib.Data.EReal.Inv
EReal.div_nonneg : ∀ {a b : EReal}, 0 ≤ a → 0 ≤ b → 0 ≤ a / b
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_mk : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →ₐ[R] B) (h : Continuous (↑↑f.toRingHom).toFun), ↑{ toAlgHom := f, cont := h } = f
-- Mathlib.LinearAlgebra.AffineSpace.Ceva
/-- Auxiliary lemma for `exists_affineCombination_eq_smul_eq`.  -/
_private.Mathlib.LinearAlgebra.AffineSpace.Ceva.0.AffineIndependent.exists_affineCombination_eq_smul_eq_aux : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] {p : ι → P},
  AffineIndependent k p →
    ∀ {s : Set ι},
      s.Nonempty →
        ∀ {fs : ↑s → Finset ι},
          (∀ (i : ↑s), ↑i ∈ fs i) →
            ∀ {w : ↑s → ι → k},
              (∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1) →
                ∀ {p' : P},
                  (∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]) →
                    ∃ w' fs',
                      ∑ j ∈ fs', w' j = 1 ∧
                        (Finset.affineCombination k fs' p) w' = p' ∧
                          ∀ (i : ↑s),
                            ∃ r, ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑fs' \ {↑i}).indicator w' j
-- Mathlib.Data.TypeVec
/-- given `F : TypeVec.{u} (n+1) → Type u`, `curry F : Type u → TypeVec.{u} → Type u`,
i.e. its first argument can be fed in separately from the rest of the vector of arguments  -/
TypeVec.Curry : {n : ℕ} → (TypeVec.{u} (n + 1) → Type u_1) → Type u → TypeVec.{u} n → Type u_1
-- Init.Data.Array.Find
Array.findSomeRev?_push_of_isNone : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α} {xs : Array α},
  (f a).isNone = true → Array.findSomeRev? f (xs.push a) = Array.findSomeRev? f xs
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_eq_some_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.maxKey? = some (t.maxKeyD fallback)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- An absolute left Kan lift is a left Kan lift.  -/
CategoryTheory.Bicategory.LeftLift.IsAbsKan.isKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : b ⟶ a} → {g : c ⟶ a} → {t : CategoryTheory.Bicategory.LeftLift f g} → t.IsAbsKan → t.IsKan
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.hasAdd.eq_1 : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M), c.hasAdd = { add := Quotient.map₂ (fun x1 x2 => x1 + x2) ⋯ }
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_eq_nat_iff_finset : ∀ {α : Type u} {n : ℕ}, Cardinal.mk α = ↑n ↔ ∃ t, ↑t = Set.univ ∧ t.card = n
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            CategoryTheory.Functor C V → CategoryTheory.MonoidalCategory.DayFunctor C V
-- Lean.ResolveName
/-- For identifiers taken from syntax, use `resolveGlobalConstNoOverload` instead, which respects preresolved names.  -/
Lean.resolveGlobalConstNoOverloadCore : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadResolveName m] →
      [Lean.MonadEnv m] →
        [Lean.MonadOptions m] →
          [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadError m] → Lean.Name → m Lean.Name
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instIsAddApplyForall : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂], IsAddApply (MultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.w_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (pres : CategoryTheory.Limits.ColimitPresentation J X) {i j : J} (f : i ⟶ j) {Z : C}
  (h : ((CategoryTheory.Functor.const J).obj X).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (pres.diag.map f) (CategoryTheory.CategoryStruct.comp (pres.ι.app j) h) =
    CategoryTheory.CategoryStruct.comp (pres.ι.app i) h
-- Init.Core
UInt64.ofBitVec.injEq : ∀ (toBitVec toBitVec_1 : BitVec 64), ({ toBitVec := toBitVec } = { toBitVec := toBitVec_1 }) = (toBitVec = toBitVec_1)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.le_pow_ramificationIdx' : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  {P : Ideal S}, Ideal.map (algebraMap R S) p ≤ P ^ p.ramificationIdx' P
-- Mathlib.Util.Notation3
/-- Matcher for `Expr.fvar`.
It checks that the user name agrees and that the type of the expression is matched by `matchTy`.  -/
Mathlib.Notation3.matchFVar : Lean.Name → Mathlib.Notation3.Matcher → Mathlib.Notation3.Matcher
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- The functor `LightCondSet ⥤ TopCat`  -/
lightCondSetToTopCat : CategoryTheory.Functor LightCondSet TopCat
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
/-- Generate the suggestion for applying `lem`.  -/
Mathlib.Tactic.ClickSuggestions.ApplyAtLemma.try : Mathlib.Tactic.ClickSuggestions.ApplyAtLemma →
  Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM
    (Mathlib.Tactic.ClickSuggestions.Result Mathlib.Tactic.ClickSuggestions.ApplyAtKey)
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.cauSeq_converges : ∀ (f : CauSeq ℝ abs), ∃ x, f ≈ CauSeq.const abs x
-- Lean.Environment
/-- An environment extension with support for storing/retrieving entries from a .olean file.
 - α is the type of the entries that are stored in .olean files.
 - β is the type of values used to update the state.
 - σ is the actual state.

For most extensions, α and β coincide. `α` and `β` do not coincide for extensions where the data
used to update the state contains elements which cannot be stored in files (for example, closures).

During elaboration of a module, state of type `σ` can be both read and written. When elaboration is
complete, the state of type `σ` is converted to serialized state of type `Array α` by
`exportEntriesFn`. To read the current module's state, use `PersistentEnvExtension.getState`. To
modify it, use `PersistentEnvExtension.addEntry`, with an `addEntryFn` that performs the appropriate
modification.

When a module is loaded, the values saved by all of its dependencies for this
`PersistentEnvExtension` are available as an `Array (Array α)` via the environment extension,
with one array per transitively imported module. The state of type `σ` used in the current module
can be initialized from these imports by specifying a suitable `addImportedFn`. The `addImportedFn`
runs at the beginning of elaboration for every module, so it's usually better for performance to
query the array of imported modules directly, because only a fraction of imported entries is usually
queried during elaboration of a module.

The most typical pattern for using `PersistentEnvExtension` is to set `σ` to a datatype such as
`NameMap` that efficiently tracks data for the current module. Then, in `exportEntriesFn`, this type
is converted to an array of pairs, sorted by the key. Given `ext : PersistentEnvExtension α β σ` and
`env : Environment`, the complete array of imported entries sorted by module index can be obtained
using `(ext.toEnvExtension.getState env).importedEntries`. To query the extension for some constant
name `n`, first use `env.getModuleIdxFor? n`. If it returns `none`, look up `n` in the current
module's state (the `NameMap`). If it returns `some idx`, use `ext.getModuleEntries env idx` to get
the array of entries for `n`'s defining module, and query it using `Array.binSearch`. This pattern
imposes a constraint that the extension can only track metadata that is declared in the same module
as the definition to which it applies; relaxing this restriction can make queries slower due to
needing to search _all_ modules. If it is necessary to search all modules, it is usually better to
initialize the state of type `σ` once from all imported entries and choose a more efficient search
datastructure for it.

Note that `addEntryFn` is not in `IO`. This is intentional, and allows us to write simple functions
such as
```
def addAlias (env : Environment) (a : Name) (e : Name) : Environment :=
aliasExtension.addEntry env (a, e)
```
without using `IO`. We have many functions like `addAlias`.
 -/
Lean.PersistentEnvExtension : Type → Type → Type → Type
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.trivial_comon_counit_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.ComonObj.counit.hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Std.Sat.AIG.CNF
/-- Add the CNF for a `Decl.atom` to the state.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.addAtom : {aig : Std.Sat.AIG ℕ} →
  {a : ℕ} →
    (state : Std.Sat.AIG.toCNF.State✝ aig) →
      (idx : ℕ) →
        (h : idx < aig.decls.size) →
          aig.decls[idx] = Std.Sat.AIG.Decl.atom a → { out // Std.Sat.AIG.toCNF.State.IsExtensionBy✝ state out idx h }
-- Mathlib.Geometry.Manifold.Instances.Real
Icc_isInteriorPoint_interior : ∀ {x y : ℝ} [hxy : Fact (x < y)] {p : ↑(Set.Icc x y)},
  x < ↑p ∧ ↑p < y → (modelWithCornersEuclideanHalfSpace 1).IsInteriorPoint p
-- Mathlib.Order.Minimal
MaximalFor.of_strictMonoOn_comp : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {Q : ι → Prop} {f : ι → α}
  {g : α → β} {i : ι}, StrictMonoOn g (f '' Set.ofPred Q) → MaximalFor Q (g ∘ f) i → MaximalFor Q f i
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.one_div_pos : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 < 1 / p
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- Given a natural isomorphism `i ⋙ exp A ⋙ leftAdjoint i ⋙ i ≅ i ⋙ exp A`, we can show `i`
is an exponential ideal.
 -/
CategoryTheory.ExponentialIdeal.mk_of_iso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalClosed C] [inst_4 : CategoryTheory.Reflective i]
  (h :
    (A : C) →
      i.comp ((CategoryTheory.ihom A).comp ((CategoryTheory.reflector i).comp i)) ≅ i.comp (CategoryTheory.ihom A)),
  CategoryTheory.ExponentialIdeal i
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.instMkEvalWhiskerRightMonoidalM : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight Mathlib.Tactic.Monoidal.MonoidalM
-- Mathlib.CategoryTheory.Enriched.Basic
/-- Composition of two morphisms in this category  -/
CategoryTheory.EnrichedCategory.comp : {V : Type v} →
  {inst : CategoryTheory.Category.{w, v} V} →
    {inst_1 : CategoryTheory.MonoidalCategory V} →
      {C : Type u₁} →
        [self : CategoryTheory.EnrichedCategory V C] →
          (X Y Z : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj (X ⟶[V] Y) (Y ⟶[V] Z) ⟶ X ⟶[V] Z
-- Mathlib.Order.SupClosed
/-- **Alias** of the reverse direction of `infClosed_preimage_ofDual`. -/
SupClosed.dual : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, SupClosed s → InfClosed (⇑OrderDual.ofDual ⁻¹' s)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.brecOn_1.eq : ∀ {motive_1 : Lean.Meta.Match.Example → Sort u} {motive_2 : List Lean.Meta.Match.Example → Sort u}
  (t : List Lean.Meta.Match.Example) (F_1 : (t : Lean.Meta.Match.Example) → t.below → motive_1 t)
  (F_2 : (t : List Lean.Meta.Match.Example) → Lean.Meta.Match.Example.below_1 t → motive_2 t),
  Lean.Meta.Match.Example.brecOn_1 t F_1 F_2 = F_2 t (Lean.Meta.Match.Example.brecOn_1.go t F_1 F_2).2
-- Mathlib.Computability.EpsilonNFA
/-- `M.toNFA` is an `NFA` constructed from an `εNFA` `M`.  -/
εNFA.toNFA : {α : Type u} → {σ : Type v} → εNFA α σ → NFA α σ
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- The fiber functor on sheaves is induced by the fiber functor on presheaves.  -/
CategoryTheory.GrothendieckTopology.Point.sheafToPresheafCompPresheafFiberIso : {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] →
            [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
              (CategoryTheory.sheafToPresheaf J A).comp Φ.presheafFiber ≅ Φ.sheafFiber
-- Mathlib.Topology.Order.Basic
/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(-∞, x)` is separated below from `f x` is countable.  -/
countable_image_lt_image_Iio : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : LinearOrder β] (f : β → α) [SecondCountableTopology α], {x | ∃ z < f x, ∀ y < x, f y ≤ z}.Countable
-- Mathlib.Data.Set.Restrict
/-- Restricting the domain and then the codomain is the same as `MapsTo.restrict`.  -/
Set.codRestrict_domRestrict : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} (h : ∀ (x : ↑s), f ↑x ∈ t),
  Set.codRestrict (s.domRestrict f) t h = Set.MapsTo.restrict f s t ⋯
-- Aesop.Forward.Match.Types
/-- Two matches are equivalent if (a) they have the same level; (b) for each
premise that appears in a slot greater than the matches' level, their
substitution assigns the same value; (c) for each premise that appears in the
rule's conclusion, their substitution assigns the same value.

If we already have a match `m₁` and we obtain an equivalent match `m₂`, then
`m₂` is redundant. This is because if the matches are partial, then `m₂` can be
completed by exactly the hypotheses that complete `m₁`, since they agree on the
premise instantiations that are relevant for the possible completions. And if
the matches are complete, then they assign the same instantiations to the
variables that appear in the rule's conclusion, and these are the only ones that
ultimately matter.  -/
Aesop.Match.equiv : Aesop.Match → Aesop.Match → Bool
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
/-- The chosen product of categories `C × D` yields a product cone in `Cat`.  -/
CategoryTheory.Cat.prodCone : (C D : CategoryTheory.Cat) → CategoryTheory.Limits.BinaryFan C D
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- If `K / E / F` is a field extension tower, `S ⊂ K` is such that `F(S) = K`,
then `E(S) = K`.  -/
IntermediateField.adjoin_eq_top_of_adjoin_eq_top : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u}
  [inst_3 : Field K] [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] {S : Set K},
  IntermediateField.adjoin F S = ⊤ → IntermediateField.adjoin E S = ⊤
-- Init.Prelude
_private.Init.Prelude.0.Lean.Macro.State.mk : Lean.MacroScope → List (Lean.Name × String) → List Lean.Name → Lean.Macro.State
-- Init.Data.Nat.Simproc
Nat.Simproc.add_sub_le : ∀ (a : ℕ) {b c : ℕ}, b ≤ c → a + b - c = a - (c - b)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).hom.app X).hom₁ =
    CategoryTheory.CategoryStruct.id X.obj₁
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.prod_monomial : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {ι : Type u_4} (f : ι → σ →₀ ℕ) (g : ι → R) (s : Finset ι),
  ∏ i ∈ s, (MvPowerSeries.monomial (f i)) (g i) = (MvPowerSeries.monomial (∑ i ∈ s, f i)) (∏ i ∈ s, g i)