mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.lTensor_reflects_triviality : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.FaithfullyFlat R M] (N : Type u_1) [inst_4 : AddCommGroup N] [inst_5 : Module R N]
  [Subsingleton (TensorProduct R M N)], Subsingleton N
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.findSomeM?_eq_match_step.match_1.eq_1 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (h_1 : Unit → motive none) (h_2 : (fx : γ) → motive (some fx)),
  (match none with
    | none => h_1 ()
    | some fx => h_2 fx) =
    h_1 ()
-- Aesop.Script.TacticState
_private.Aesop.Script.TacticState.0.Aesop.Script.TacticState.eraseSolvedGoals.mvarWasSolved : Lean.MetavarContext → Lean.MetavarContext → Lean.MVarId → Bool
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β} {f : Option β → Option β},
  (m.alter k f).getD k fallback = (f m[k]?).getD fallback
-- Mathlib.RepresentationTheory.Basic
Representation.linHom_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring k] [inst_1 : Group G]
  [inst_2 : AddCommMonoid V] [inst_3 : Module k V] [inst_4 : AddCommMonoid W] [inst_5 : Module k W]
  (ρV : Representation k G V) (ρW : Representation k G W) (g : G) (f : V →ₗ[k] W),
  ((ρV.linHom ρW) g) f = ρW g ∘ₗ f ∘ₗ ρV g⁻¹
-- Init.Data.BitVec.Bitblast
/-- If `y &&& z = 0`, `x.sshiftRight (y ||| z) = (x.sshiftRight y).sshiftRight z`.
This follows as `y &&& z = 0` implies `y ||| z = y + z`,
and thus `x.sshiftRight (y ||| z) = x.sshiftRight (y + z) = (x.sshiftRight y).sshiftRight z`.
 -/
BitVec.sshiftRight'_or_of_and_eq_zero : ∀ {w₁ w₂ : ℕ} {x : BitVec w₁} {y z : BitVec w₂},
  y &&& z = 0#w₂ → x.sshiftRight' (y ||| z) = (x.sshiftRight' y).sshiftRight' z
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Precoverage.toCoverage_toPrecoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.Precoverage C)
  [inst_1 : J.HasPullbacks] [inst_2 : J.IsStableUnderBaseChange], J.toCoverage.toPrecoverage = J
-- Mathlib.MeasureTheory.Measure.Hausdorff
IsometryEquiv.measurePreserving_hausdorffMeasure : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] (e : X ≃ᵢ Y) (d : ℝ),
  MeasureTheory.MeasurePreserving (⇑e) (MeasureTheory.Measure.hausdorffMeasure d)
    (MeasureTheory.Measure.hausdorffMeasure d)
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.isoMk_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C}
  (e : X.toPresheafedSpace ≅ Y.toPresheafedSpace),
  (AlgebraicGeometry.SheafedSpace.isoMk e).hom = CategoryTheory.InducedCategory.homMk e.hom
-- Lean.Expr
/-- `.mvar mvarId` is now the preferred form.
This function is seldom used, metavariables are often created using functions such
as `mkFreshExprMVar` at `MetaM`.
 -/
Lean.mkMVar : Lean.MVarId → Lean.Expr
-- Mathlib.Order.Sublocale
Sublocale.range_toNucleus : ∀ {X : Type u_1} [inst : Order.Frame X] {S : Sublocale X}, Set.range ⇑S.toNucleus = ↑S
-- Mathlib.Algebra.Group.Prod
/-- Product of additive isomorphisms; the maps come from `Equiv.prodCongr`.  -/
AddEquiv.prodCongr : {M : Type u_3} →
  {N : Type u_4} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        {M' : Type u_6} →
          {N' : Type u_7} →
            [inst_2 : AddZeroClass N'] → [inst_3 : AddZeroClass M'] → M ≃+ M' → N ≃+ N' → M × N ≃+ M' × N'
-- Mathlib.Order.Filter.Defs
/-- Construct a filter from a property that is stable under finite unions.
A set `s` belongs to `Filter.comk p _ _ _` iff its complement satisfies the predicate `p`.
This constructor is useful to define filters like `Filter.cofinite`.  -/
Filter.comk : {α : Type u_1} →
  (p : Set α → Prop) →
    p ∅ → (∀ (t : Set α), p t → ∀ s ⊆ t, p s) → (∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)) → Filter α
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instCompleteLinearOrder : {α : Type u_1} → [inst : LinearOrder α] → CompleteLinearOrder (UpperSet α)
-- Mathlib.SetTheory.Ordinal.Basic
/-- There exists a well-order on `α` whose order type is exactly `ord #α`.  -/
Cardinal.exists_ord_eq : ∀ (α : Type u_1), ∃ r, ∃ (x : IsWellOrder α r), (Cardinal.mk α).ord = Ordinal.type r
-- Std.Net.Addr
/-- A pair of an `IPv4Addr` and a port.
 -/
Std.Net.SocketAddressV4 : Type
-- Mathlib.Topology.Algebra.UniformConvergence
instMulUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Mul β],
  instMulUniformOnFun = { mul := instMulUniformOnFun._aux_1 }
-- Mathlib.Algebra.Group.Hom.Instances
instIsCancelAddZeroHom : ∀ {M : Type uM} {N : Type uN} [inst : Zero M] [inst_1 : AddZeroClass N] [IsCancelAdd N], IsCancelAdd (ZeroHom M N)
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.mapMulHom_id : ∀ {α : Type u} [inst : Mul α], WithOne.mapMulHom (MulHom.id α) = MonoidHom.id (WithOne α)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.natTransOfLe_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S T : CategoryTheory.Sieve X} (h : S ≤ T)
  (x : Cᵒᵖ), (CategoryTheory.Sieve.natTransOfLe h).app x = TypeCat.ofHom fun f => ⟨↑f, ⋯⟩
-- Mathlib.Data.Sigma.Basic
Sigma.instDecidableEqSigma : {α : Type u_1} → {β : α → Type u_4} → [h₁ : DecidableEq α] → [h₂ : (a : α) → DecidableEq (β a)] → DecidableEq (Sigma β)
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.mem_stabilizer_set_iff_subset_smul_set : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {a : G} {s : Set α},
  s.Finite → (a ∈ MulAction.stabilizer G s ↔ s ⊆ a • s)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} [inst_1 : Inhabited (β k)], k ∉ m₂ → (m₁ \ m₂).get! k = m₁.get! k
-- Batteries.Lean.PersistentHashSet
/-- Returns `true` if `f` returns `true` for all elements of the set.
 -/
Lean.PersistentHashSet.all : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashSet α → (α → Bool) → Bool
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.MorphismProperty.tensorHom_mem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [W.IsMonoidal] {X₁ X₂ : C} (f : X₁ ⟶ X₂) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂),
  W f → W g → W (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableOn.clm_prodMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_17}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {g : M → F₁ →L[𝕜] F₃} {f : M → F₂ →L[𝕜] F₄}
  {s : Set M}, MDiff[s] g → MDiff[s] f → MDiff[s] fun x => (g x).prodMap (f x)
-- Init.Data.Format.Basic
Std.ToFormat.mk : {α : Type u} → (α → Std.Format) → Std.ToFormat α
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rco.toList_iter_eq_toList : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rco α}, r.iter.toList = r.toList
-- Mathlib.Order.Filter.Pointwise
Filter.vadd_le_vadd_right : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f₁ f₂ : Filter α} {g : Filter β}, f₁ ≤ f₂ → f₁ +ᵥ g ≤ f₂ +ᵥ g
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabel.name.injEq : ∀ (n n_1 : String), (Lean.Lsp.InlayHintLabel.name n = Lean.Lsp.InlayHintLabel.name n_1) = (n = n_1)
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.ExtendByOne.hom_apply : ∀ {ι : Type u_1} {η : Type v} (R : Type w) (s : ι → η) [inst : MulOneClass R] (f : ι → R) (a : η),
  (Function.ExtendByOne.hom R s) f a = Function.extend s f 1 a
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.Monic.mem_rootSet : ∀ {T : Type w} [inst : CommRing T] {p : Polynomial T},
  p.Monic →
    ∀ {S : Type u_1} [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S] {a : S},
      a ∈ p.rootSet S ↔ (Polynomial.aeval a) p = 0
-- Lean.Compiler.IR.Format
Lean.IR.formatDecl : Lean.IR.Decl → optParam ℕ 2 → Std.Format
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenRatio.eq_1 : Real.goldenRatio = (1 + √5) / 2
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.reinsertAux.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : { d // 0 < d.size } → Sort u_3) →
      (data : { d // 0 < d.size }) →
        ((data : Array (Std.DHashMap.Internal.AssocList α β)) → (hd : 0 < data.size) → motive ⟨data, hd⟩) → motive data
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_neg_iff : ∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R]
  [AddLeftReflectLT R] [AddLeftStrictMono R], a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
-- Mathlib.Analysis.Normed.Lp.ProdLp
LinearIsometryEquiv.withLpProdUnique_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : Semiring 𝕜]
  [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β] [inst_4 : Module 𝕜 β]
  [inst_5 : Unique β] (x : WithLp p (α × β)), (LinearIsometryEquiv.withLpProdUnique p 𝕜 α β) x = x.fst
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_zero : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R], QuaternionAlgebra.imK 0 = 0
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- Multiplication in a normed `𝕜`-algebra as a bounded bilinear map.  -/
isBoundedBilinearMap_mul : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : SeminormedRing A] [inst_2 : Algebra 𝕜 A],
  IsBoundedBilinearMap 𝕜 fun p => p.1 * p.2
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.mono_inl_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [CategoryTheory.Limits.HasPushouts C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Mono g]
  {s : CategoryTheory.Limits.PushoutCocone f g} (hs : CategoryTheory.Limits.IsColimit s), CategoryTheory.Mono s.inl
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_comp_unsym : ∀ {α : Type u_1}, ⇑SymAlg.sym ∘ ⇑SymAlg.unsym = id
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_of_contains_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k : α}, (Std.HashMap.map f m).contains k = true → m.contains k = true
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The cosine of the angle between three points is -1 if and only if the angle is π.  -/
EuclideanGeometry.cos_eq_neg_one_iff_angle_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  Real.cos (EuclideanGeometry.angle p₁ p₂ p₃) = -1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.comp_toPath_eq_cons : ∀ {V : Type u_1} [inst : Quiver V] {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c), p.comp e.toPath = p.cons e
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.brecOn.go : {motive : FBinopElab.Tree✝ → Sort u} →
  (t : FBinopElab.Tree✝) →
    ((t : FBinopElab.Tree✝) → FBinopElab.Tree.below✝ t → motive t) → motive t ×' FBinopElab.Tree.below✝ t
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Eta-expanded form of `Measurable.const_smul` -/
Measurable.fun_const_smul : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : SMul M X] {m : MeasurableSpace α}
  {g : α → X} [MeasurableConstSMul M X], Measurable g → ∀ (c : M), Measurable fun i => c • g i
-- Mathlib.Computability.Partrec
Computable.succ : Computable Nat.succ
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.exists_int_gt_of_mk_nonneg : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {x : R},
  0 ≤ ArchimedeanClass.mk x → ∃ n, x < ↑n
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
FirstOrder.Field.ACF_isSatisfiable : ∀ {p : ℕ}, Nat.Prime p ∨ p = 0 → (FirstOrder.Language.Theory.ACF p).IsSatisfiable
-- Init.Data.Order.Ord
Option.instLawfulBEqOrd : ∀ {α : Type u_1} [inst : Ord α] [inst_1 : BEq α] [Std.LawfulBEqOrd α], Std.LawfulBEqOrd (Option α)
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.isoOfHomeo_inv : ∀ {X Y : CompactlyGenerated} (f : ↑X.toTop ≃ₜ ↑Y.toTop),
  (CompactlyGenerated.isoOfHomeo f).inv = CompactlyGenerated.ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ }
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
Unitization.starLift.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : StarRing C]
  [inst_10 : StarModule R C], Unitization.starLift = Unitization.starLift
-- Init.Data.Cast
instNatCastNat : NatCast ℕ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.containsThenInsertIfNew_fst : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.containsThenInsertIfNew k v).1 = m.contains k
-- Mathlib.Combinatorics.HalesJewett
/-- The diagonal line. It is the identity at every coordinate.  -/
Combinatorics.Line.diagonal : (α : Type u_5) → (ι : Type u_6) → [Nonempty ι] → Combinatorics.Line α ι
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trList.eq_1 : Turing.PartrecToTM2.trList [] = []
-- Batteries.Data.String.Lemmas
String.utf8Len_data : ∀ (s : String), String.utf8Len s.toList = s.utf8ByteSize
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.Hom.ext : ∀ {X Y : SFinKer} {x y : X.Hom Y}, x.hom = y.hom → x = y
-- Aesop.RuleSet
Aesop.LocalRuleSet.mk : Aesop.BaseRuleSet →
  (simpTheoremsArray : Array (Lean.Name × Lean.Meta.SimpTheorems)) →
    0 < simpTheoremsArray.size →
      (simprocsArray : Array (Lean.Name × Lean.Meta.Simprocs)) →
        0 < simprocsArray.size → Array Aesop.LocalNormSimpRule → Aesop.LocalRuleSet
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.integrable : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] [CompleteSpace E]
  [SecondCountableTopology E], ProbabilityTheory.HasGaussianLaw X P → MeasureTheory.Integrable X P
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.CC_exact : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  IsClosed C →
    ∀ (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2)
      {f : LocallyConstant ↑C ℤ},
      (Profinite.NobelingProof.Linear_CC' C hsC ho) f = 0 → ∃ y, (Profinite.NobelingProof.πs C o) y = f
-- Mathlib.Topology.MetricSpace.Congruence
/-- Congruence holds if and only if all distances are the same.  -/
congruent_iff_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂], Congruent v₁ v₂ ↔ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.instInhabitedHomOplaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → {F G : CategoryTheory.OplaxFunctor B C} → {η : F ⟶ G} → Inhabited (η ⟶ η)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.Derives.trans_produces : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)},
  g.Derives u v → g.Produces v w → g.Derives u w
-- Mathlib.Topology.Bornology.Constructions
Bornology.isBounded_pi_of_nonempty : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → Bornology (X i)] {S : (i : ι) → Set (X i)},
  (Set.univ.pi S).Nonempty → (Bornology.IsBounded (Set.univ.pi S) ↔ ∀ (i : ι), Bornology.IsBounded (S i))
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.νNatTrans_app : ∀ (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]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  (x : CategoryTheory.Discrete PUnit.{1}),
  (CategoryTheory.MonoidalCategory.DayFunctor.νNatTrans C V).app x = CategoryTheory.MonoidalCategory.DayFunctor.ν C V
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyInfEntourage_univ : ∀ {X : Type u_1} (T : X → X) {F : Set X}, F.Nonempty → Dynamics.netEntropyInfEntourage T F Set.univ = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_id : ∀ {P : Type u_3} [inst : MulOneClass P] (S : Submonoid P), Submonoid.comap (MonoidHom.id P) S = S
-- Mathlib.Data.DFinsupp.Defs
/-- Redefine `f i` to be `0`.  -/
DFinsupp.erase : {ι : Type u} →
  {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → [DecidableEq ι] → ι → (Π₀ (i : ι), β i) → Π₀ (i : ι), β i
-- Lean.Meta.Sym.Arith.Types
/-- Mapping from types to their classification result. Caches failures as `.none`.  -/
Lean.Meta.Sym.Arith.State.typeClassify : Lean.Meta.Sym.Arith.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.Arith.ClassifyResult
-- Mathlib.Analysis.Analytic.Constructions
/-- `f x / g x` is analytic away from `g x = 0`  -/
AnalyticOnNhd.div : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f g : E → 𝕝}
  {s : Set E}, AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 g s → (∀ x ∈ s, g x ≠ 0) → AnalyticOnNhd 𝕜 (fun x => f x / g x) s
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Iso.hom_inv_id_triangle_hom₃_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (e : A ≅ B) {Z : C} (h : A.obj₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp e.hom.hom₃ (CategoryTheory.CategoryStruct.comp e.inv.hom₃ h) = h
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The image of a subsemiring along a ring homomorphism is a subsemiring.  -/
Subsemiring.map : {R : Type u} →
  {S : Type v} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → (R →+* S) → Subsemiring R → Subsemiring S
-- Lean.Data.PersistentArray
Lean.PersistentArray.foldr : {α : Type u} → {β : Type u_1} → Lean.PersistentArray α → (α → β → β) → β → β
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a : α},
      Std.DTreeMap.Raw.Const.get? (t.erase k) a =
        if cmp k a = Ordering.eq then none else Std.DTreeMap.Raw.Const.get? t a
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
ConditionallyCompleteLattice.toLattice : {α : Type u_5} → [self : ConditionallyCompleteLattice α] → Lattice α
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- The complex-valued arithmetic function that is the convolution of the constant
function `1` with `χ`.  -/
DirichletCharacter.zetaMul : {N : ℕ} → DirichletCharacter ℂ N → ArithmeticFunction ℂ
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_preimage : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] (s : Set α) (f : α → M) (B : Set M),
  s.mulIndicator f ⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B)
-- Mathlib.RingTheory.RootsOfUnity.Complex
IsPrimitiveRoot.nnnorm_eq_one : ∀ {ζ : ℂ} {n : ℕ}, IsPrimitiveRoot ζ n → n ≠ 0 → ‖ζ‖₊ = 1
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.discreteUniformity_iff : ∀ {α : Type u_1} [inst : UniformSpace α],
  DiscreteUniformity (TopologicalSpace.NonemptyCompacts α) ↔ DiscreteUniformity α
-- Mathlib.NumberTheory.LSeries.SumCoeff
_private.Mathlib.NumberTheory.LSeries.SumCoeff.0.lemma₁ : ∀ {f : ℕ → ℂ} {l : ℂ},
  Filter.Tendsto (fun n => (∑ k ∈ Finset.Icc 1 n, f k) / ↑n) Filter.atTop (nhds l) →
    ∀ {s : ℝ},
      1 < s →
        MeasureTheory.IntegrableOn (fun t => (∑ k ∈ Finset.Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1)
          MeasureTheory.volume
-- Init.Prelude
/-- Computations in the monad `m` can be run in the monad `n`. These translations are inserted
automatically by the compiler.

Usually, `n` consists of some number of monad transformers applied to `m`, but this is not
mandatory.

New instances should use this class, `MonadLift`. Clients that require one monad to be liftable into
another should instead request `MonadLiftT`, which is the reflexive, transitive closure of
`MonadLift`.
 -/
MonadLift : semiOutParam (Type u → Type v) → (Type u → Type w) → Type (max (max (u + 1) v) w)
-- Mathlib.Algebra.GCDMonoid.Nat
Int.normalize_coe_nat : ∀ (n : ℕ), normalize ↑n = ↑n
-- Mathlib.Algebra.Module.PID
DirectSum.eq_1 : ∀ (ι : Type v) (β : ι → Type w) [inst : (i : ι) → AddCommMonoid (β i)], DirectSum ι β = Π₀ (i : ι), β i