mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Calculus
differentiableOn_euclidean : ∀ {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H]
  [inst_2 : NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {t : Set H} [Finite ι],
  DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x => (f x).ofLp i) t
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.IsLimit.homIso_apply_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : CategoryTheory.Limits.Fork f g}
  (ht : CategoryTheory.Limits.IsLimit t) (Z : C) (k : Z ⟶ t.pt),
  ↑((CategoryTheory.Limits.Fork.IsLimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp k t.ι
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.ker_π : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M},
  solution.IsPresentation → solution.π.ker = Submodule.span A (Set.range relations.relation)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_iff₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop},
  MeasureTheory.NullMeasurableSet {x | p x} (μ.restrict s) →
    ((∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x)
-- Mathlib.Algebra.Module.Equiv.Basic
/-- `x ↦ -x` as a `LinearEquiv`  -/
LinearEquiv.neg : (R : Type u_1) → {M : Type u_5} → [inst : Semiring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → M ≃ₗ[R] M
-- Mathlib.CategoryTheory.Limits.Cones
/-- The category of cocones on `F` is equivalent to the opposite category of
the category of cones on the opposite of `F`.
 -/
CategoryTheory.Limits.coconeEquivalenceOpConeOp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) → CategoryTheory.Limits.Cocone F ≌ (CategoryTheory.Limits.Cone F.op)ᵒᵖ
-- Lean.Parser.Syntax
Lean.Parser.Command.syntaxAbbrev.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_smul_of_nonneg : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] [StarModule ℝ A] {r : ℝ},
  0 ≤ r → ∀ {a : A}, (r • a)⁻ = r • a⁻
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.isoOfComponents_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (H : ↑X ≅ ↑Y)
  (α : (TopCat.Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf),
  (AlgebraicGeometry.PresheafedSpace.isoOfComponents H α).inv =
    { base := H.inv, c := TopCat.Presheaf.toPushforwardOfIso H α.hom }
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.int_gcd_helper : ∀ {x y : ℤ} {x' y' d : ℕ}, x.natAbs = x' → y.natAbs = y' → x'.gcd y' = d → x.gcd y = d
-- Aesop.Tree.Data
Aesop.Goal.parentRapp? : Aesop.Goal → BaseIO (Option Aesop.RappRef)
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib_congr_left : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {Y' : α → Ω},
  Y =ᵐ[μ] Y' → ProbabilityTheory.condDistrib Y X μ = ProbabilityTheory.condDistrib Y' X μ
-- Lean.Parser.Term
Lean.Parser.Term.structInst.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Defs.Unbundled
/-- `MinimalFor P f i` means that `f i` is minimal over all `i` satisfying `P`.  -/
MinimalFor : {ι : Sort u_1} → {α : Type u_2} → [LE α] → (ι → Prop) → (ι → α) → ι → Prop
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.true_or : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, ⌜True⌝ ∨ P ⊣⊢ₛ ⌜True⌝
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instSMul : {β : Type u_2} → {α : Type u_1} → [SMul β α] → SMul β (Lex α)
-- Mathlib.Topology.Semicontinuity.Basic
UpperSemicontinuousOn.inf : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α},
  UpperSemicontinuousOn f s → UpperSemicontinuousOn g s → UpperSemicontinuousOn (fun x => min (f x) (g x)) s
-- Mathlib.Order.Partition.Finpartition
Finpartition.combine.congr_simp : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α]
  {ι : Type u_2} {I : Finset ι} {a : ι → α} (P P_1 : (i : ι) → Finpartition (a i)),
  P = P_1 → ∀ (ha : I.SupIndep a), Finpartition.combine P ha = Finpartition.combine P_1 ha
-- Mathlib.Algebra.GroupWithZero.Associated
associated_isUnit_mul_right_iff : ∀ {N : Type u_2} [inst : CommMonoid N] {a u b : N}, IsUnit u → (Associated a (u * b) ↔ Associated a b)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- A short-cut instance for the common case, where the requirements for the `compatible_smul`
instances are sufficient.  -/
TensorProduct.isScalarTower : ∀ {R : Type u_1} {R' : Type u_4} [inst : CommSemiring R] [inst_1 : Monoid R'] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : DistribMulAction R' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : SMulCommClass R R' M] [inst_8 : SMul R' R] [IsScalarTower R' R M],
  IsScalarTower R' R (TensorProduct R M N)
-- Init.Omega.Int
Lean.Omega.Fin.ofNat_val_natCast : ∀ {n x y : ℕ}, y = x % (n + 1) → ↑↑(OfNat.ofNat x) = OfNat.ofNat y
-- Init.Data.SInt.Bitwise
Int16.xor_comm : ∀ (a b : Int16), a ^^^ b = b ^^^ a
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
/-- **Alias** of the reverse direction of `isTranscendenceBasis_equiv`. -/
IsTranscendenceBasis.comp_equiv : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (e : ι ≃ ι') {f : ι' → A}, IsTranscendenceBasis R f → IsTranscendenceBasis R (f ∘ ⇑e)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.ballAddSubgroup_top : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M], ⊤.ballAddSubgroup = ⊥
-- Std.Time.Time.PlainTime
Std.Time.instReprPlainTime : Repr Std.Time.PlainTime
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
ClosedSubmodule.orthogonal_eq_orthogonal_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K₁ K₂ : ClosedSubmodule 𝕜 E) [(↑K₁).HasOrthogonalProjection] [(↑K₂).HasOrthogonalProjection], K₁ᗮ = K₂ᗮ ↔ K₁ = K₂
-- Mathlib.RingTheory.Congruence.Basic
RingCon.comap_ringConGen_ringEquiv : ∀ {R : Type u_5} {R' : Type u_6} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring R'] (r : R' → R' → Prop)
  (f : R ≃+* R'), (ringConGen r).comap f = ringConGen (Function.onFun r ⇑f)
-- Mathlib.CategoryTheory.Sites.Preserves
CategoryTheory.Presieve.isSheafFor_iff_preservesProduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a) →
    ∀ (hI : CategoryTheory.Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C}
      (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c)
      [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [inst_3 : CategoryTheory.Limits.HasInitial C]
      [∀ (i : α), CategoryTheory.Mono (c.inj i)],
      (Pairwise fun i j =>
          CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j))
            (c.inj i) (c.inj j)) →
        (CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj) ↔
          CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.ext : ∀ {R : Type u_1} {x y : Cubic R}, x.a = y.a → x.b = y.b → x.c = y.c → x.d = y.d → x = y
-- Mathlib.MeasureTheory.Category.MeasCat
/-- Construct a bundled `MeasCat` from the underlying type and the typeclass.  -/
MeasCat.of : (carrier : Type u) → [str : MeasurableSpace carrier] → MeasCat
-- Mathlib.CategoryTheory.Quotient
/-- Generates the closure of a family of relations w.r.t. composition from left and right.  -/
CategoryTheory.HomRel.CompClosure : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → HomRel C → HomRel C
-- Init.Data.List.Lex
List.lt_of_le_of_lt' : ∀ {α : Type u_1} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  [Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2] {l₁ l₂ l₃ : List α},
  l₁ ≤ l₂ → l₂ < l₃ → l₁ < l₃
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The inverse Fourier transform from `L1` functions to bounded continuous functions.  -/
Real.Lp.fourierTransformInv : {V : Type u_1} →
  {E : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℂ E] →
        [inst_2 : NormedAddCommGroup V] →
          [inst_3 : InnerProductSpace ℝ V] →
            [inst_4 : MeasurableSpace V] →
              [inst_5 : BorelSpace V] →
                [inst_6 : FiniteDimensional ℝ V] →
                  ↥(MeasureTheory.Lp E 1 MeasureTheory.volume) → BoundedContinuousFunction V E
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- `splitSetByVarSign a comps` partitions the set `comps` into three parts.
* `pos` contains the elements of `comps` in which `a` has a positive coefficient.
* `neg` contains the elements of `comps` in which `a` has a negative coefficient.
* `notPresent` contains the elements of `comps` in which `a` has coefficient 0.

Returns `(pos, neg, notPresent)`.
 -/
Mathlib.Tactic.Linarith.splitSetByVarSign : ℕ →
  Mathlib.Tactic.Linarith.PCompSet →
    Mathlib.Tactic.Linarith.PCompSet × Mathlib.Tactic.Linarith.PCompSet × Mathlib.Tactic.Linarith.PCompSet
-- Mathlib.NumberTheory.LSeries.MellinEqDirichlet
/-- Version allowing some constant terms (which are omitted from the sums).  -/
hasSum_mellin_pi_mul₀ : ∀ {ι : Type u_1} [Countable ι] {a : ι → ℂ} {p : ι → ℝ} {F : ℝ → ℂ} {s : ℂ},
  (∀ (i : ι), 0 ≤ p i) →
    0 < s.re →
      (∀ t ∈ Set.Ioi 0, HasSum (fun i => if p i = 0 then 0 else a i * ↑(Real.exp (-Real.pi * p i * t))) (F t)) →
        (Summable fun i => ‖a i‖ / p i ^ s.re) →
          HasSum (fun i => ↑Real.pi ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.getLastD.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → α → Sort u_2) (a₀ : α) (h_1 : (a₀ : α) → motive [] a₀)
  (h_2 : (a : α) → (as : List α) → (x : α) → motive (a :: as) x),
  (match [], a₀ with
    | [], a₀ => h_1 a₀
    | a :: as, x => h_2 a as x) =
    h_1 a₀
-- Mathlib.Data.PNat.Factors
/-- The multiset consisting of a single prime  -/
PrimeMultiset.ofPrime : Nat.Primes → PrimeMultiset
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.mk.injEq : ∀ {M : Type u_10} {N : Type u_11} [inst : Zero M] [inst_1 : Zero N] (toFun : M → N) (map_zero' : toFun 0 = 0)
  (toFun_1 : M → N) (map_zero'_1 : toFun_1 0 = 0),
  ({ toFun := toFun, map_zero' := map_zero' } = { toFun := toFun_1, map_zero' := map_zero'_1 }) = (toFun = toFun_1)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.mem_homogeneousCore_of_homogeneous_of_mem : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  {I : Ideal A} {x : A}, SetLike.IsHomogeneousElem 𝒜 x → x ∈ I → x ∈ Ideal.homogeneousCore 𝒜 I
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.upperSubLower_apply : ∀ {n : ℕ} {G : Type u} [inst : AddCommGroup G] (I₀ : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1))
  (f : ℝ → BoxIntegral.Box (Fin n) → G)
  (fb : ↑(Set.Icc (I₀.lower i) (I₀.upper i)) → BoxIntegral.BoxAdditiveMap (Fin n) G ↑(I₀.face i))
  (hf : ∀ (x : ℝ) (hx : x ∈ Set.Icc (I₀.lower i) (I₀.upper i)) (J : BoxIntegral.Box (Fin n)), f x J = (fb ⟨x, hx⟩) J)
  (J : BoxIntegral.Box (Fin (n + 1))),
  (BoxIntegral.BoxAdditiveMap.upperSubLower I₀ i f fb hf) J = f (J.upper i) (J.face i) - f (J.lower i) (J.face i)
-- Lean.Util.NumObjs
Lean.Expr.NumObjs.State.mk : Lean.PtrSet Lean.Expr → ℕ → Lean.Expr.NumObjs.State
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.le_of_dvd : ∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B] (n₁ n₂ : ℕ)
  (C₁ C₂ : Subalgebra A B) [h₁ : IsCyclotomicExtension {n₁} A ↥C₁] [h₂ : IsCyclotomicExtension {n₂} A ↥C₂] [NeZero n₂],
  n₁ ∣ n₂ → C₁ ≤ C₂
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `not_isAddTorsion_of_isAddTorsionFree`.

---

A nontrivial torsion-free additive abelian group is not torsion.  -/
not_isTorsion_of_isAddTorsionFree : ∀ {G : Type u_1} [inst : AddCommGroup G] [Nontrivial G] [IsAddTorsionFree G], ¬IsAddTorsion G
-- Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
/-- Given an integrable function `f` with values in `ℝ≥0`, there exists an upper semicontinuous
function `g ≤ f` with integral arbitrarily close to that of `f`. Formulation in terms of
`lintegral`.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`.  -/
MeasureTheory.exists_upperSemicontinuous_le_lintegral_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] {μ : MeasureTheory.Measure α}
  [μ.WeaklyRegular] (f : α → NNReal),
  ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤ →
    ∀ {ε : ENNReal},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
-- Mathlib.GroupTheory.Congruence.Basic
Con.comapQuotientEquivOfSurj_symm_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (c : Con M) {f : N →* M}
  (hf : Function.Surjective ⇑f) (x : N), (c.comapQuotientEquivOfSurj f hf).symm ↑(f x) = ↑x
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.unop2_id : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : Bᵒᵖ} {f : a ⟶ b},
  (CategoryTheory.CategoryStruct.id f).unop2 = CategoryTheory.CategoryStruct.id f.unop
-- Mathlib.Analysis.MeanInequalities
/-- **AM-GM inequality**: The geometric mean is less than or equal to the arithmetic mean, weighted
version for two `NNReal` numbers.  -/
NNReal.geom_mean_le_arith_mean2_weighted : ∀ (w₁ w₂ p₁ p₂ : NNReal), w₁ + w₂ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ ≤ w₁ * p₁ + w₂ * p₂
-- Mathlib.LinearAlgebra.Basis.Basic
/-- Any basis is a maximal linear independent set.
 -/
Module.Basis.maximal : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Nontrivial R] (b : Module.Basis ι R M), ⋯.Maximal
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.interedges_biUnion : ∀ {ι : Type u_2} {κ : Type u_3} {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq α]
  (s : Finset ι) (t : Finset κ) (f : ι → Finset α) (g : κ → Finset α),
  G.interedges (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun ab => G.interedges (f ab.1) (g ab.2)
-- Mathlib.Algebra.Group.Pi.Basic
Sum.elim_div_div : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a a' : α → γ) (b b' : β → γ) [inst : Div γ],
  Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'
-- Init.Data.Array.Lemmas
Array.and_any_distrib_right : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool} {q : Bool}, (xs.any p && q) = xs.any fun a => p a && q
-- Mathlib.LinearAlgebra.Finsupp.Pi
/-- If `α` has a unique term, then the type of finitely supported functions `α →₀ M` is
`R`-linearly equivalent to `M`.  -/
Finsupp.uniqueLinearEquiv : (R : Type u_1) →
  {α : Type u_3} →
    (M : Type u_4) →
      [inst : AddCommMonoid M] → [inst_1 : Semiring R] → [inst_2 : Module R M] → [Subsingleton α] → α → (α →₀ M) ≃ₗ[R] M
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.transport_η_assoc : ∀ {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 G : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (i : F ≅ G) {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η G) h =
    CategoryTheory.CategoryStruct.comp (i.inv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) h)
-- Lean.Meta.Instances
Lean.Meta.instInhabitedInstances.default : Lean.Meta.Instances
-- Mathlib.Topology.FiberBundle.Trivialization
/-- See Note [custom simps projection]  -/
Bundle.Trivialization.Simps.apply : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : TopologicalSpace Z] → (proj : Z → B) → Bundle.Trivialization F proj → Z → B × F
-- Mathlib.Analysis.Complex.Basic
Complex.continuous_conj : Continuous ⇑(starRingEnd ℂ)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.ε_down_ℕ : ∀ (n : ℕ), (ComplexShape.down ℕ).ε n = (-1) ^ n
-- Mathlib.Data.Multiset.Filter
Multiset.filter.congr_simp : ∀ {α : Type u_1} (p p_1 : α → Prop),
  p = p_1 →
    ∀ {inst : DecidablePred p} [inst_1 : DecidablePred p_1] (s s_1 : Multiset α),
      s = s_1 → Multiset.filter p s = Multiset.filter p_1 s_1
-- Mathlib.Tactic.FunProp.FunctionData
/-- Can't generate function data as function body has lambda binder.  -/
Mathlib.Meta.FunProp.MaybeFunctionData.lam : Lean.Expr → Mathlib.Meta.FunProp.MaybeFunctionData
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_multiset_sum : ∀ {n : Type u_3} {R : Type u_6} [inst : Fintype n] [inst_1 : AddCommMonoid R] (s : Multiset (Matrix n n R)),
  s.sum.trace = (Multiset.map Matrix.trace s).sum
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.ExtTheorem.mk.sizeOf_spec : ∀ (declName : Lean.Name) (priority : ℕ) (keys : Array Lean.Meta.DiscrTree.Key),
  sizeOf { declName := declName, priority := priority, keys := keys } =
    1 + sizeOf declName + sizeOf priority + sizeOf keys
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β} {hc : k ∈ Std.DTreeMap.Const.alter t k f},
  Std.DTreeMap.Const.get (Std.DTreeMap.Const.alter t k f) k hc = (f (Std.DTreeMap.Const.get? t k)).get ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideEqualizer.trident_π_app_zero : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y))
  [inst_1 : CategoryTheory.Limits.HasWideEqualizer f],
  (CategoryTheory.Limits.wideEqualizer.trident f).π.app CategoryTheory.Limits.WalkingParallelFamily.zero =
    CategoryTheory.Limits.wideEqualizer.ι f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_ofList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List ((a : α) × β a)} {k : α}, k ∈ Std.DTreeMap.ofList l cmp ↔ (List.map Sigma.fst l).contains k = true
-- Mathlib.Analysis.Analytic.Inverse
_private.Mathlib.Analysis.Analytic.Inverse.0.FormalMultilinearSeries.leftInv.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_1 ()
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.disjointed : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → Set α},
  (∀ (i : ℕ), MeasureTheory.NullMeasurableSet (f i) μ) → ∀ (n : ℕ), MeasureTheory.NullMeasurableSet (disjointed f n) μ
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrX_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i)
      (HomologicalComplex.homotopyCofiber.d φ i j) =
    CategoryTheory.CategoryStruct.comp (G.d i j) (HomologicalComplex.homotopyCofiber.inrX φ j)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) (M : Type uM) [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M],
  ∃ f, f.IsSubordinate fun x => (chartAt H x).source
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_to_real : ∀ {x : ℝ}, (starRingEnd ℝ) x = x
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.exponent_min : ∀ {K : Type u_2} {L : Type u_3} [inst : CommRing K] [inst_1 : Ring L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable.HasExponent K L] {e : ℕ},
  e < IsPurelyInseparable.exponent K L → ∃ a, a ^ ringExpChar K ^ e ∉ (algebraMap K L).range
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.mk.injEq : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (toLinearMap : V →ₗ[A] W)
  (isIntertwining' : ∀ (g : G), toLinearMap ∘ₗ ρ g = σ g ∘ₗ toLinearMap) (toLinearMap_1 : V →ₗ[A] W)
  (isIntertwining'_1 : ∀ (g : G), toLinearMap_1 ∘ₗ ρ g = σ g ∘ₗ toLinearMap_1),
  ({ toLinearMap := toLinearMap, isIntertwining' := isIntertwining' } =
      { toLinearMap := toLinearMap_1, isIntertwining' := isIntertwining'_1 }) =
    (toLinearMap = toLinearMap_1)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.Hom.ideal_ker_le : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) (U : ↑Y.affineOpens),
  f.ker.ideal U ≤ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))
-- Mathlib.Algebra.Group.Action.Option
Option.instVAddCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst_1 : VAdd N α] [VAddCommClass M N α],
  VAddCommClass M N (Option α)
-- Init.Data.Format.Instances
/-- Converts a string to a pretty-printer document, replacing newlines in the string with
`Std.Format.line`.
 -/
String.toFormat : String → Std.Format
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_alter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.size =
    if k ∈ t ∧ (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isNone = true then t.size - 1
    else if k ∉ t ∧ (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then t.size + 1 else t.size
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Constructor for the W-type of `P`  -/
MvPFunctor.wMk' : {n : ℕ} → (P : MvPFunctor.{u} (n + 1)) → {α : TypeVec.{u} n} → ↑P (α ::: P.W α) → P.W α
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_symm_sum : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] {ι' : Type u_5} (s : Finset ι')
  (f : ι' → DirectSum ι fun i => ↥(ℳ i)),
  (DirectSum.decompose ℳ).symm (∑ i ∈ s, f i) = ∑ i ∈ s, (DirectSum.decompose ℳ).symm (f i)
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.polynomial : ∀ (R : Type u_4) [inst : CommRing R], Algebra.FormallySmooth R (Polynomial R)