mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_norm_add_const_of_dist_le : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a b : E} {r : ℝ}, dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
/-- `f : M → N` is a **`C^n` local diffeomorphism** iff it is a local diffeomorphism
at each `x ∈ M`.  -/
IsLocalDiffeomorph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H₁ : Type u_5} →
                  [inst_5 : TopologicalSpace H₁] →
                    {H₂ : Type u_6} →
                      [inst_6 : TopologicalSpace H₂] →
                        ModelWithCorners 𝕜 E H₁ →
                          ModelWithCorners 𝕜 F H₂ →
                            {M : Type u_8} →
                              [inst : TopologicalSpace M] →
                                [ChartedSpace H₁ M] →
                                  {N : Type u_9} →
                                    [inst : TopologicalSpace N] → [ChartedSpace H₂ N] → WithTop ℕ∞ → (M → N) → Prop
-- Std.Http.Data.URI.Config
Std.Http.URI.Config.mk.injEq : ∀
  (maxSchemeLength maxHostLength maxUserInfoLength maxSegmentLength maxQueryLength maxFragmentLength maxPathSegments
    maxTotalPathLength maxQueryParams maxSchemeLength_1 maxHostLength_1 maxUserInfoLength_1 maxSegmentLength_1
    maxQueryLength_1 maxFragmentLength_1 maxPathSegments_1 maxTotalPathLength_1 maxQueryParams_1 : ℕ),
  ({ maxSchemeLength := maxSchemeLength, maxHostLength := maxHostLength, maxUserInfoLength := maxUserInfoLength,
        maxSegmentLength := maxSegmentLength, maxQueryLength := maxQueryLength, maxFragmentLength := maxFragmentLength,
        maxPathSegments := maxPathSegments, maxTotalPathLength := maxTotalPathLength,
        maxQueryParams := maxQueryParams } =
      { maxSchemeLength := maxSchemeLength_1, maxHostLength := maxHostLength_1,
        maxUserInfoLength := maxUserInfoLength_1, maxSegmentLength := maxSegmentLength_1,
        maxQueryLength := maxQueryLength_1, maxFragmentLength := maxFragmentLength_1,
        maxPathSegments := maxPathSegments_1, maxTotalPathLength := maxTotalPathLength_1,
        maxQueryParams := maxQueryParams_1 }) =
    (maxSchemeLength = maxSchemeLength_1 ∧
      maxHostLength = maxHostLength_1 ∧
        maxUserInfoLength = maxUserInfoLength_1 ∧
          maxSegmentLength = maxSegmentLength_1 ∧
            maxQueryLength = maxQueryLength_1 ∧
              maxFragmentLength = maxFragmentLength_1 ∧
                maxPathSegments = maxPathSegments_1 ∧
                  maxTotalPathLength = maxTotalPathLength_1 ∧ maxQueryParams = maxQueryParams_1)
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.Pattern.pattern : Lean.Meta.Sym.Pattern → Lean.Expr
-- Mathlib.SetTheory.ZFC.Ordinal
/-- **Alias** of `ZFSet.isOrdinal_iff_trichotomous`.

---

An ordinal is a transitive set, trichotomous under membership.  -/
ZFSet.isOrdinal_iff_isTrichotomous : ∀ {x : ZFSet.{u}}, x.IsOrdinal ↔ x.IsTransitive ∧ Std.Trichotomous (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_inter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂).getKey k h_mem = m₁.getKey k ⋯
-- Mathlib.Order.Category.BddDistLat
BddDistLat.coe_id : ∀ {X : BddDistLat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.lift_inv_comp_left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj A] [inst_3 : CategoryTheory.GrpObj B] (f : A ⟶ B)
  [CategoryTheory.IsMonHom f] {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv f) f)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
-- Mathlib.Topology.Algebra.Monoid.Defs
instSeparatelyContinuousAddOfContinuousAdd : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M], SeparatelyContinuousAdd M
-- Mathlib.Order.Sublattice
/-- Sublattices of a lattice form a complete lattice.  -/
Sublattice.instCompleteLattice : {α : Type u_2} → [inst : Lattice α] → CompleteLattice (Sublattice α)
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.isStandardSmooth_holdsForLocalizationAway : RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => RingHom.IsStandardSmooth
-- Mathlib.Order.Filter.CardinalInter
Filter.cardinalInter_ofCardinalGenerate : ∀ {α : Type u} {c : Cardinal.{u}} (g : Set (Set α)) (hc : 2 < c), CardinalInterFilter (Filter.cardinalGenerate g hc) c
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.SurjectiveOnStalks.comp : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {T : Type u_3} [inst_2 : CommRing T]
  {g : S →+* T} {f : R →+* S}, g.SurjectiveOnStalks → f.SurjectiveOnStalks → (g.comp f).SurjectiveOnStalks
-- Mathlib.Order.RelClasses
/-- **Alias** of `LT.lt.not_superset`.

---

Set notation form of `LT.lt.not_ge` -/
HasSSubset.SSubset.not_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊂ b → ¬b ⊆ a
-- Mathlib.Combinatorics.Quiver.Prefunctor
/-- This may be a more useful form of `Prefunctor.ext`.  -/
Prefunctor.ext' : ∀ {V W : Type u} [inst : Quiver V] [inst_1 : Quiver W] {F G : V ⥤q W} (h_obj : ∀ (X : V), F.obj X = G.obj X),
  (∀ (X Y : V) (f : X ⟶ Y), F.map f = Quiver.homOfEq (G.map f) ⋯ ⋯) → F = G
-- Mathlib.Order.RelSeries
RelSeries.map_length : ∀ {α : Type u_1} {r : SetRel α α} {β : Type u_2} {s : SetRel β β} (p : RelSeries r) (f : r.Hom s),
  (p.map f).length = p.length
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasSum_sum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} [ContinuousAdd α] {f : γ → β → α} {a : γ → α} {s : Finset γ},
  (∀ i ∈ s, HasSum (f i) (a i) L) → HasSum (fun b => ∑ i ∈ s, f i b) (∑ i ∈ s, a i) L
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- `P` is local at the target if
1. `P` respects isomorphisms.
2. If `P` holds for `f : X ⟶ Y`, then `P` holds for `f ∣_ U` for any `U`.
3. If `P` holds for `f ∣_ U` for an open cover `U` of `Y`, then `P` holds for `f`.
 -/
AlgebraicGeometry.IsZariskiLocalAtTarget.mk' : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso],
  (∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)) →
    (∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
        iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f) →
      AlgebraicGeometry.IsZariskiLocalAtTarget P
-- Mathlib.Algebra.BigOperators.Group.Finset.Preimage
Finset.sum_preimage : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_3} [inst : AddCommMonoid β] (f : ι → κ) (s : Finset κ)
  (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β),
  (∀ x ∈ s, x ∉ Set.range f → g x = 0) → ∑ x ∈ s.preimage f hf, g (f x) = ∑ x ∈ s, g x
-- Mathlib.Data.List.Basic
List.foldlM_eq_foldl : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] [LawfulMonad m] (f : β → α → m β) (b : β)
  (l : List α),
  List.foldlM f b l =
    List.foldl
      (fun mb a => do
        let b ← mb
        f b a)
      (pure b) l
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Restating the definition of a colimit cocone in terms of the ∃! operator.  -/
CategoryTheory.Limits.IsColimit.existsUnique : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t)
  (s : CategoryTheory.Limits.Cocone F), ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) l = s.ι.app j
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Bijection between compositions of `n` and subsets of `{0, ..., n-2}`, defined by
considering the restriction of the subset to `{1, ..., n-1}` and shifting to the left by one.  -/
compositionAsSetEquiv : (n : ℕ) → CompositionAsSet n ≃ Finset (Fin (n - 1))
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- The 2-morphism underlying the lax unity constraint.  -/
CategoryTheory.LaxFunctor.mapId : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (self : CategoryTheory.LaxFunctor B C) →
          (a : B) → CategoryTheory.CategoryStruct.id (self.obj a) ⟶ self.map (CategoryTheory.CategoryStruct.id a)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.instTransIsBigOTVSIsBigOTVS : {α : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_4} →
      {F : Type u_5} →
        {G : Type u_6} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : AddCommGroup E] →
              [inst_2 : TopologicalSpace E] →
                [inst_3 : Module 𝕜 E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : TopologicalSpace F] →
                      [inst_6 : Module 𝕜 F] →
                        [inst_7 : AddCommGroup G] →
                          [inst_8 : TopologicalSpace G] →
                            [inst_9 : Module 𝕜 G] →
                              {l : Filter α} →
                                Trans (Asymptotics.IsBigOTVS 𝕜 l) (Asymptotics.IsBigOTVS 𝕜 l)
                                  (Asymptotics.IsBigOTVS 𝕜 l)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- **Alias** of the forward direction of `intervalIntegrable_congr`. -/
IntervalIntegrable.congr : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ε},
  Set.EqOn f g (Set.uIoc a b) → IntervalIntegrable f μ a b → IntervalIntegrable g μ a b
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], (t₁ ∩ t₂)[k]! = if k ∈ t₂ then t₁[k]! else default
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.iterate_minimalPeriod : ∀ {α : Type u_1} {f : α → α} {x : α}, f^[Function.minimalPeriod f x] x = x
-- Mathlib.Data.Fintype.Sets
Set.subsingleton_toFinset_iff : ∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s], Subsingleton ↥s.toFinset ↔ s.Subsingleton
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualRestrict_surjective : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {W : Subspace K V},
  Function.Surjective ⇑(Submodule.dualRestrict W)
-- Mathlib.Algebra.Order.Group.Indicator
Function.support_inf : ∀ {α : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : SemilatticeInf M] (f g : α → M),
  (Function.support fun x => f x ⊓ g x) ⊆ Function.support f ∪ Function.support g
-- Mathlib.Order.Disjoint
Disjoint.ne_top_of_ne_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {a b : α}, Disjoint a b → a ≠ ⊥ → b ≠ ⊤
-- Init.Data.Fin.Lemmas
Fin.instCommutativeHMul : ∀ {n : ℕ}, Std.Commutative fun x1 x2 => x1 * x2
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.disjoint_toSubmodule : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {K K' : LieSubalgebra R L}, Disjoint K.toSubmodule K'.toSubmodule ↔ Disjoint K K'
-- Mathlib.Topology.UniformSpace.Equicontinuity
Filter.HasBasis.equicontinuousAt_iff_left : ∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α]
  {p : κ → Prop} {s : κ → Set X} {F : ι → X → α} {x₀ : X},
  (nhds x₀).HasBasis p s →
    (EquicontinuousAt F x₀ ↔ ∀ U ∈ uniformity α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U)
-- Mathlib.NumberTheory.NumberField.Norm
Algebra.coe_trace_int : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.RingOfIntegers K),
  ↑((Algebra.trace ℤ (NumberField.RingOfIntegers K)) x) = (Algebra.trace ℚ K) ↑x
-- Mathlib.Topology.Algebra.Group.Basic
continuousAt_neg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [ContinuousNeg G] {x : G}, ContinuousAt Neg.neg x
-- Mathlib.Analysis.Calculus.Darboux
/-- **Darboux's theorem**: if `a ≤ b` and `f' a < m < f' b`, then `f' c = m` for some
`c ∈ (a, b)`.  -/
exists_hasDerivWithinAt_eq_of_gt_of_lt : ∀ {a b : ℝ} {f f' : ℝ → ℝ},
  a ≤ b →
    (∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) →
      ∀ {m : ℝ}, f' a < m → m < f' b → m ∈ f' '' Set.Ioo a b
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
CochainComplex.singleFunctor_obj_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : C) (n p q : ℤ),
  ((CochainComplex.singleFunctor C n).obj X).d p q = 0
-- Mathlib.Analysis.Polynomial.Fourier
Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero : ∀ (p : Polynomial ℂ), ∀ n < 0, fourierCoeff (⇑(Polynomial.toAddCircle p)) n = 0
-- Mathlib.Control.Fold
Traversable.foldlm_toList : ∀ {α β : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {m : Type u → Type u}
  [inst_2 : Monad m] [LawfulMonad m] {f : α → β → m α} {x : α} {xs : t β},
  Traversable.foldlm f x xs = List.foldlM f x (Traversable.toList xs)
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.ACM.getStruct : Lean.Meta.Grind.AC.ACM Lean.Meta.Grind.AC.Struct
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {M N : CategoryTheory.Comonad C}
  {x y : CategoryTheory.ComonadHom M N}, x = y ↔ x.app = y.app
-- Lean.Meta.Tactic.Grind.PP
/-- Helper function for pretty printing the state for debugging purposes.  -/
Lean.Meta.Grind.ppENodeRef : Lean.Expr → Lean.Meta.Grind.GoalM Lean.MessageData
-- Init.Control.Lawful.Instances
ReaderT.run_mapConst : ∀ {m : Type u_1 → Type u_2} {α ρ β : Type u_1} [inst : Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ),
  (Functor.mapConst a x).run ctx = Functor.mapConst a (x.run ctx)
-- Lean.Elab.PatternVar
/-- Collect pattern variables occurring in the `match`-alternative object views.
It also returns the updated views.
 -/
Lean.Elab.Term.collectPatternVars : {k : Lean.SyntaxNodeKinds} →
  Lean.Elab.Term.MatchAltView k → Lean.Elab.TermElabM (Array Lean.Elab.Term.PatternVar × Lean.Elab.Term.MatchAltView k)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_smul : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] (a : S) (b : AddMonoidAlgebra R ℕ),
  { toFinsupp := a • b } = a • { toFinsupp := b }
-- Init.Data.UInt.Bitwise
UInt16.xor_neg_one : ∀ {a : UInt16}, a ^^^ -1 = ~~~a
-- Init.Data.Iterators.Basic
Std.IterStep.successor.eq_3 : ∀ {α : Type u} {β : Type w}, Std.IterStep.done.successor = none
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.parallelComp_sum_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {ι : Type u_5} [inst : Countable ι]
  (κ : ι → ProbabilityTheory.Kernel α β) [∀ (i : ι), ProbabilityTheory.IsSFiniteKernel (κ i)]
  (η : ProbabilityTheory.Kernel γ δ),
  (ProbabilityTheory.Kernel.sum κ).parallelComp η = ProbabilityTheory.Kernel.sum fun i => (κ i).parallelComp η
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `F` is a field of exponential characteristic `q`, `F(S) / F` is separable, then
`F(S) = F(S ^ q)`.  -/
IntermediateField.adjoin_eq_adjoin_pow_expChar_of_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E)
  [Algebra.IsSeparable F ↥(IntermediateField.adjoin F S)] (q : ℕ) [ExpChar F q],
  IntermediateField.adjoin F S = IntermediateField.adjoin F ((fun x => x ^ q) '' S)
-- Mathlib.Data.PFunctor.Multivariate.M
/-- Implementation of destructor for M-type of `P`  -/
MvPFunctor.M.pathDestRight : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u_1} n} →
      {x : P.last.M} →
        {a : P.A} →
          {f : P.last.B a → P.last.M} →
            x.dest = ⟨a, f⟩ →
              TypeVec.Arrow (MvPFunctor.M.Path P x) α → (j : P.last.B a) → TypeVec.Arrow (MvPFunctor.M.Path P (f j)) α
-- Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.Structural.RecArgCandidates.mk.injEq : ∀ (candidates : Array Lean.Elab.Structural.RecArgCandidate) (report : Lean.MessageData)
  (candidates_1 : Array Lean.Elab.Structural.RecArgCandidate) (report_1 : Lean.MessageData),
  ({ candidates := candidates, report := report } = { candidates := candidates_1, report := report_1 }) =
    (candidates = candidates_1 ∧ report = report_1)
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
/-- If `H' : D' ⥤ V` is a pointwise left Kan extension along `L : D ⥤ D'` and
if tensoring left with an object preserves colimits in `V`,
then `K ⊠ H' : D' × E ⥤ V` is a pointwise left Kan extension along `(𝟭 E) × L`.  -/
CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionExtensionUnitRight : {V : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {D : Type u₂} →
        {D' : Type u₃} →
          {E : Type u₄} →
            [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} D'] →
                [inst_4 : CategoryTheory.Category.{v₄, u₄} E] →
                  {H : CategoryTheory.Functor D V} →
                    {L : CategoryTheory.Functor D D'} →
                      (H' : CategoryTheory.Functor D' V) →
                        (α : H ⟶ L.comp H') →
                          (K : CategoryTheory.Functor E V) →
                            [∀ (d : D') (e : E),
                                  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow L d)
                                    (CategoryTheory.MonoidalCategory.tensorLeft (K.obj e))] →
                              (CategoryTheory.Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtension →
                                (CategoryTheory.Functor.LeftExtension.mk
                                    (CategoryTheory.MonoidalCategory.externalProduct K H')
                                    (CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitRight H' α
                                      K)).IsPointwiseLeftKanExtension
-- Mathlib.Algebra.Lie.LieTheorem
_private.Mathlib.Algebra.Lie.LieTheorem.0.LieModule.T : {R : Type u_1} →
  {A : Type u_3} →
    {V : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing A] →
          [inst_2 : LieAlgebra R A] →
            [inst_3 : AddCommGroup V] →
              [inst_4 : Module R V] → [inst_5 : LieRingModule A V] → [LieModule R A V] → (A → R) → A → Module.End R V
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.eqvGen_step_iff_join_red : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, Relation.EqvGen FreeGroup.Red.Step L₁ L₂ ↔ Relation.Join FreeGroup.Red L₁ L₂
-- Mathlib.Tactic.Positivity.Core
_private.Mathlib.Tactic.Positivity.Core.0.Mathlib.Meta.Positivity.OrderRel.le : Mathlib.Meta.Positivity.OrderRel✝
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.isoApp_trans : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y Z : (i : I) → C i}
  (f : X ≅ Y) (g : Y ≅ Z) (i : I),
  CategoryTheory.Pi.isoApp (f ≪≫ g) i = CategoryTheory.Pi.isoApp f i ≪≫ CategoryTheory.Pi.isoApp g i
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_empty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α}, ∅.contains a = false
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_div : ∀ {K : Type u_1} [inst : RCLike K] (x y : K), (starRingEnd K) (x / y) = (starRingEnd K) x / (starRingEnd K) y
-- Mathlib.Order.PartialSups
partialSups_disjoint_of_disjoint : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι] [inst_2 : DistribLattice α]
  [inst_3 : OrderBot α] (f : ι → α),
  Pairwise (Function.onFun Disjoint f) → ∀ {i j : ι}, i < j → Disjoint ((partialSups f) i) (f j)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.Hom.toImageAux_spec : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toImageAux f)
      (AlgebraicGeometry.Scheme.Hom.imageι f) =
    f
-- Mathlib.RingTheory.Spectrum.Maximal.Defs
MaximalSpectrum.ext_iff : ∀ {R : Type u_1} {inst : CommSemiring R} {x y : MaximalSpectrum R}, x = y ↔ x.asIdeal = y.asIdeal
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
/-- The collection of elements of a `MonoidWithZero` that are not left zero divisors form a
`Submonoid`.  -/
nonZeroDivisorsLeft : (M₀ : Type u_1) → [inst : MonoidWithZero M₀] → Submonoid M₀
-- Mathlib.Topology.Algebra.FilterBasis
/-- The trivial group filter basis consists of `{1}` only. The associated topology
is discrete.  -/
GroupFilterBasis.instInhabited : {G : Type u} → [inst : Group G] → Inhabited (GroupFilterBasis G)
-- Mathlib.Order.CompleteLattice.Basic
iSup_true : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : True → α}, iSup s = s trivial
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- The empty graph is regular of any degree `d`  -/
SimpleGraph.IsRegularOfDegree.of_isEmpty : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : G.LocallyFinite] [IsEmpty V] {d : ℕ}, G.IsRegularOfDegree d
-- Mathlib.Algebra.Field.IsField
/-- For each field, and for each nonzero element of said field, there is a unique inverse.
Since `IsField` doesn't remember the data of an `inv` function and as such,
a lemma that there is a unique inverse could be useful.
 -/
uniq_inv_of_isField : ∀ (R : Type u) [inst : Ring R], IsField R → ∀ (x : R), x ≠ 0 → ∃! y, x * y = 1
-- Mathlib.Topology.Algebra.Module.Star
symm_starL : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousStar A], (starL R).symm = starL R
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.inertiaEquiv_symm_apply_smul : ∀ {M : Type u_1} [inst : Group M] {N : Type u_4} [inst_1 : Group N] {R : Type u_5} [inst_2 : Ring R]
  [inst_3 : MulSemiringAction M R] [inst_4 : MulSemiringAction N R] (I : Ideal R) (e : M ≃* N)
  (he : ∀ (m : M) (x : R), e m • x = m • x) (n : ↥(Ideal.inertia N I)) (x : R), (I.inertiaEquiv e he).symm n • x = n • x
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      ∀ {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] [inst_5 : Module 𝔸 F] [IsBoundedSMul 𝔸 F]
        [IsScalarTower 𝕜 𝔸 F] {f : 𝕜 → 𝔸},
        ContDiffWithinAt 𝕜 (↑n) f s x →
          ∀ (v : F), iteratedDerivWithin n (fun y => f y • v) s x = iteratedDerivWithin n f s x • v
-- Mathlib.FieldTheory.SeparableClosure
Field.insepDegree.eq_1 : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Field.insepDegree F E = Module.rank (↥(separableClosure F E)) E