mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The composition of two applications of `map₂` is naturally isomorphic to a single such one.  -/
CategoryTheory.CostructuredArrow.map₂CompMap₂Iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : D} →
          {S : CategoryTheory.Functor C D} →
            {A : Type u₃} →
              [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
                {B : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] →
                    {U : CategoryTheory.Functor A B} →
                      {V : B} →
                        {F : CategoryTheory.Functor C A} →
                          {G : CategoryTheory.Functor D B} →
                            (α : F.comp U ⟶ S.comp G) →
                              (β : G.obj T ⟶ V) →
                                {C' : Type u₆} →
                                  [inst_4 : CategoryTheory.Category.{v₆, u₆} C'] →
                                    {D' : Type u₅} →
                                      [inst_5 : CategoryTheory.Category.{v₅, u₅} D'] →
                                        {R : CategoryTheory.Functor C' D'} →
                                          {F' : CategoryTheory.Functor C' C} →
                                            {G' : CategoryTheory.Functor D' D} →
                                              {X : D'} →
                                                (α' : F'.comp S ⟶ R.comp G') →
                                                  (β' : G'.obj X ⟶ T) →
                                                    (CategoryTheory.CostructuredArrow.map₂ α' β').comp
                                                        (CategoryTheory.CostructuredArrow.map₂ α β) ≅
                                                      CategoryTheory.CostructuredArrow.map₂
                                                        (CategoryTheory.CategoryStruct.comp (F'.associator F U).hom
                                                          (CategoryTheory.CategoryStruct.comp (F'.whiskerLeft α)
                                                            (CategoryTheory.CategoryStruct.comp (F'.associator S G).inv
                                                              (CategoryTheory.CategoryStruct.comp
                                                                (CategoryTheory.Functor.whiskerRight α' G)
                                                                (R.associator G' G).hom))))
                                                        (CategoryTheory.CategoryStruct.comp (G.map β') β)
-- Mathlib.Probability.Process.Predictable
/-- **Alias** of `MeasureTheory.IsStronglyPredictable.isStronglyProgressive`.

---

A predictable process is progressively measurable.  -/
MeasureTheory.IsPredictable.progMeasurable : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {E : Type u_3} [inst : TopologicalSpace E]
  [inst_1 : LinearOrder ι] [inst_2 : OrderBot ι] [inst_3 : MeasurableSpace ι] [inst_4 : TopologicalSpace ι]
  [OpensMeasurableSpace ι] [OrderClosedTopology ι] {𝓕 : MeasureTheory.Filtration ι m} {u : ι → Ω → E},
  MeasureTheory.IsStronglyPredictable 𝓕 u → MeasureTheory.IsStronglyProgressive 𝓕 u
-- Batteries.Data.NameSet
Lean.NameSet.instUnion_batteries : Union Lean.NameSet
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_of_one_to_one : ∀ (f : { len := 1 } ⟶ { len := 1 }),
  (∃ a, f = { len := 1 }.const { len := 1 } a) ∨ f = CategoryTheory.CategoryStruct.id { len := 1 }
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- If the scalar product forms a `MulAction`, then the subset inherits this action  -/
SubMulAction.mulAction' : {S : Type u'} →
  {R : Type u} →
    {M : Type v} →
      [inst : Monoid R] →
        [inst_1 : MulAction R M] →
          [inst_2 : Monoid S] →
            [inst_3 : SMul S R] →
              [inst_4 : MulAction S M] → [IsScalarTower S R M] → (p : SubMulAction R M) → MulAction S ↥p
-- Mathlib.Topology.AlexandrovDiscrete
/-- A topological space is **Alexandrov-discrete** or **finitely generated** if the intersection of
a family of open sets is open.  -/
AlexandrovDiscrete : (α : Type u_1) → [TopologicalSpace α] → Prop
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.FG.range : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : Type u_2} [inst_1 : L.Structure N],
  FirstOrder.Language.Structure.FG L M → ∀ (f : L.Hom M N), f.range.FG
-- Init.Omega.Constraint
Lean.Omega.Constraint.translate.eq_1 : ∀ (c : Lean.Omega.Constraint) (t : ℤ), c.translate t = c.map fun x => x + t
-- Mathlib.Logic.Function.Defs
/-- A function fixes every point iff it is the identity.  -/
Function.forall_isFixedPt_iff : ∀ {α : Type u₁} {f : α → α}, (∀ (x : α), Function.IsFixedPt f x) ↔ f = id
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.allLTTR.loop.match_1.eq_2 : ∀ (n : ℕ) (motive : (x : ℕ) → x ≤ n → Sort u_1) (i : ℕ) (h : i + 1 ≤ n) (h_1 : (x : 0 ≤ n) → motive 0 x)
  (h_2 : (i : ℕ) → (h : i + 1 ≤ n) → motive i.succ h),
  (match i.succ, h with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_2 i h
-- Mathlib.Analysis.Normed.Group.Completion
UniformSpace.Completion.instNormedAddCommGroup : (E : Type u_1) → [inst : SeminormedAddCommGroup E] → NormedAddCommGroup (UniformSpace.Completion E)
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasStrictDerivAt_exp_smul_const_of_mem_ball' : ∀ {𝕂 : Type u_1} {𝔸 : Type u_3} [inst : NontriviallyNormedField 𝕂] [CharZero 𝕂] [inst_2 : NormedRing 𝔸]
  [inst_3 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕂),
  t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius →
    HasStrictDerivAt (fun u => NormedSpace.exp (u • x)) (x * NormedSpace.exp (t • x)) t
-- Mathlib.Computability.Primrec.Basic
PrimrecRel.not : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [inst : Primcodable α] [inst_1 : Primcodable β],
  PrimrecRel R → PrimrecRel fun a b => ¬R a b
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.Mon C),
  (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F).inv = CategoryTheory.CategoryStruct.id F.X
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
/-- The base change natural transformation for left Kan extensions associated to
a 2-square.  -/
CategoryTheory.TwoSquare.lanBaseChange : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        {D : Type u₅} →
          [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
            [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
              [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
                [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                  [inst_4 : CategoryTheory.Category.{v₅, u₅} D] →
                    {T : CategoryTheory.Functor C₁ C₂} →
                      {L : CategoryTheory.Functor C₁ C₃} →
                        {R : CategoryTheory.Functor C₂ C₄} →
                          {B : CategoryTheory.Functor C₃ C₄} →
                            CategoryTheory.TwoSquare T L R B →
                              [inst_5 : ∀ (F : CategoryTheory.Functor C₁ D), L.HasLeftKanExtension F] →
                                [inst_6 : ∀ (F : CategoryTheory.Functor C₂ D), R.HasLeftKanExtension F] →
                                  ((CategoryTheory.Functor.whiskeringLeft C₁ C₂ D).obj T).comp L.lan ⟶
                                    R.lan.comp ((CategoryTheory.Functor.whiskeringLeft C₃ C₄ D).obj B)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.toSubmodule_eq_top : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S : Subalgebra R A},
  Subalgebra.toSubmodule S = ⊤ ↔ S = ⊤
-- Mathlib.NumberTheory.Dioph
IsPoly.below : {α : Type u_1} → {motive : (a : (α → ℕ) → ℤ) → IsPoly a → Prop} → {a : (α → ℕ) → ℤ} → IsPoly a → Prop
-- Mathlib.Order.Filter.Basic
Filter.forall_mem_nonempty_iff_neBot : ∀ {α : Type u} {f : Filter α}, (∀ s ∈ f, s.Nonempty) ↔ f.NeBot
-- Mathlib.Data.Fin.Parity
Fin.odd_iff_of_even : ∀ {n : ℕ} {k : Fin n} [inst : NeZero n], Even n → (Odd k ↔ Odd ↑k)
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_diagonal : ∀ {m : Type u_2} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α] [inst_2 : DecidableEq m]
  (d : o → m → α), (Matrix.blockDiagonal fun k => Matrix.diagonal (d k)) = Matrix.diagonal fun ik => d ik.2 ik.1
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.PEquivOn.mk.injEq : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [inst : LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i}
  [inst_1 : SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s : Set ι}
  (equiv : (i : ↑s) → F ↑i ≃ InverseSystem.piLT X ↑i) (nat : InverseSystem.IsNatEquiv f equiv)
  (compat :
    ∀ {i : ι} (hsi : Order.succ i ∈ s) (hi : ¬IsMax i) (x : F ↑⟨Order.succ i, hsi⟩),
      (equiv ⟨Order.succ i, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2)
  (equiv_1 : (i : ↑s) → F ↑i ≃ InverseSystem.piLT X ↑i) (nat_1 : InverseSystem.IsNatEquiv f equiv_1)
  (compat_1 :
    ∀ {i : ι} (hsi : Order.succ i ∈ s) (hi : ¬IsMax i) (x : F ↑⟨Order.succ i, hsi⟩),
      (equiv_1 ⟨Order.succ i, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2),
  ({ equiv := equiv, nat := nat, compat := compat } = { equiv := equiv_1, nat := nat_1, compat := compat_1 }) =
    (equiv = equiv_1)
-- Init.Data.Nat.Lemmas
Nat.pred_add_self : ∀ (n : ℕ), n.pred + n = (2 * n).pred
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_erase_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, (m.erase k).getKey! k = default
-- Std.Async.System
/-- OS version.
 -/
Std.Async.System.OSInfo.release : Std.Async.System.OSInfo → String
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.mk.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (weightMap weightMap_1 : M →ₗ[R] M₂)
  (e_weightMap : weightMap = weightMap_1) (coweightMap coweightMap_1 : N₂ →ₗ[R] N)
  (e_coweightMap : coweightMap = coweightMap_1) (indexEquiv indexEquiv_1 : ι ≃ ι₂)
  (e_indexEquiv : indexEquiv = indexEquiv_1)
  (weight_coweight_transpose : weightMap.dualMap ∘ₗ ↑Q.flip.toPerfPair = ↑P.flip.toPerfPair ∘ₗ coweightMap)
  (root_weightMap : ⇑weightMap ∘ ⇑P.root = ⇑Q.root ∘ ⇑indexEquiv)
  (coroot_coweightMap : ⇑coweightMap ∘ ⇑Q.coroot = ⇑P.coroot ∘ ⇑indexEquiv.symm),
  { weightMap := weightMap, coweightMap := coweightMap, indexEquiv := indexEquiv,
      weight_coweight_transpose := weight_coweight_transpose, root_weightMap := root_weightMap,
      coroot_coweightMap := coroot_coweightMap } =
    { weightMap := weightMap_1, coweightMap := coweightMap_1, indexEquiv := indexEquiv_1,
      weight_coweight_transpose := ⋯, root_weightMap := ⋯, coroot_coweightMap := ⋯ }
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.dArrowIso₀₁_inv_left : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupCohomology.dArrowIso₀₁ A).inv.left = (groupCohomology.cochainsIso₀ A).inv
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_natCast_mul : ∀ (x : ENNReal) (n : ℕ) (z : ℝ), x ^ (↑n * z) = (x ^ n) ^ z
-- Mathlib.Order.Height
Set.chainHeight_eq_zero_iff : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), s.chainHeight r = 0 ↔ s = ∅
-- Mathlib.Control.EquivFunctor
EquivFunctor.ofLawfulFunctor : (f : Type u₀ → Type u₁) → [inst : Functor f] → [LawfulFunctor f] → EquivFunctor f
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.countable_fg_substructures_of_countable : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [Countable M], Countable { S // S.FG }
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.fixingSubgroup_sup : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  {K L : IntermediateField F E}, (K ⊔ L).fixingSubgroup = K.fixingSubgroup ⊓ L.fixingSubgroup
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_comp_eq : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N] (g : M → N),
  (∀ {x : M}, g x = 1 ↔ x = 1) → ∀ (f : ι → M), Function.mulSupport (g ∘ f) = Function.mulSupport f
-- Lean.Elab.WhereFinally
/-- Creates a view of the `finally` section of a `whereDecls` syntax object  -/
Lean.Elab.mkWhereFinallyView : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → Lean.TSyntax `Lean.Parser.Term.whereDecls → m Lean.Elab.WhereFinallyView
-- Mathlib.Data.Finset.Defs
Finset.ssubset_iff_of_subset : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁ ⊆ s₂ → (s₁ ⊂ s₂ ↔ ∃ x ∈ s₂, x ∉ s₁)
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.coindep_iff_exists : ∀ {α : Type u_1} {M : Matroid α} {X : Set α},
  autoParam (X ⊆ M.E) Matroid.coindep_iff_exists._auto_1 → (M.Coindep X ↔ ∃ B, M.IsBase B ∧ B ⊆ M.E \ X)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_pt : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)),
  (CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.obj b).pt = b.pt
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `≥` on `BitVec`s.  -/
BitVec.reduceGE : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.coe_unop : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup Gᵃᵒᵖ), ↑H.unop = AddOpposite.op ⁻¹' ↑H
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.hasStrictDerivAt_sinh : ∀ (x : ℝ), HasStrictDerivAt Real.sinh (Real.cosh x) x
-- Std.Http.Protocol.H1
/-- Send the head of a message to the machine.

Must only be called when `machine.isWaitingMessage` is true. If called in any
other state (e.g. called twice), the machine panics.

Informational (1xx) responses are written directly to the output buffer; the writer
stays in `waitingHeaders` so the application can send additional interim responses or
the final response. The reader state is not affected — use `canContinue` to resolve
an `Expect: 100-continue` decision separately.
 -/
Std.Http.Protocol.H1.Machine.send : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Message.Head dir.swap → Std.Http.Protocol.H1.Machine dir
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- Another characterization lemma for the vector addition on the
Ore localization delivering Ore witnesses and conditions bundled in a sigma type.  -/
AddOreLocalization.oreSubVAddChar' : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] →
        {X : Type u_2} →
          [inst_2 : AddAction R X] →
            (r₁ : R) →
              (r₂ : X) →
                (s₁ s₂ : ↥S) →
                  (r' : R) ×' (s' : ↥S) ×' ↑s' + r₁ = r' + ↑s₂ ∧ (r₁ -ₒ s₁) +ᵥ r₂ -ₒ s₂ = (r' +ᵥ r₂) -ₒ (s' + s₁)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
riemannZeta_two : riemannZeta 2 = ↑Real.pi ^ 2 / 6
-- Mathlib.Algebra.Order.Group.OrderIso
/-- `x ↦ x - a` as an order isomorphism.  -/
OrderIso.subRight : {α : Type u} → [inst : AddGroup α] → [inst_1 : LE α] → [AddRightMono α] → α → α ≃o α
-- Mathlib.Topology.Baire.BaireMeasurable
BaireMeasurableSet.biUnion : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_3} {s : ι → Set α} {t : Set ι},
  t.Countable → (∀ i ∈ t, BaireMeasurableSet (s i)) → BaireMeasurableSet (⋃ i ∈ t, s i)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_lt_aleph0 : ∀ {m : ℕ∞}, ↑m < Cardinal.aleph0 ↔ m < ⊤
-- Lean.Expr
Lean.Expr.letValue! : Lean.Expr → Lean.Expr
-- Mathlib.Analysis.Analytic.Basic
/-- If `f` has formal power series `∑ n, pₙ` on a ball of radius `r`, then for `y, z` in any smaller
ball, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is bounded above by
`C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`.  -/
HasFPowerSeriesOnBall.image_sub_sub_deriv_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r r' : ENNReal},
  HasFPowerSeriesOnBall f p x r →
    r' < r →
      ∃ C,
        ∀ y ∈ Metric.eball x r',
          ∀ z ∈ Metric.eball x r', ‖f y - f z - (p 1) fun x => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖
-- Init.Data.Slice.Array.Lemmas
Array.size_mkSlice_roc : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  Std.Slice.size (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = min (hi + 1) xs.size - (lo + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.sigmaπ.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.left] [inst_3 : CategoryTheory.Limits.HasCoproduct I.right],
  CategoryTheory.Limits.Multicoequalizer.sigmaπ I =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π I.fstSigmaMap I.sndSigmaMap)
      (CategoryTheory.Limits.Multicoequalizer.isoCoequalizer I).inv
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.castNum.match_1.eq_1 : ∀ (motive : Num → Sort u_1) (h_1 : Unit → motive Num.zero) (h_2 : (p : PosNum) → motive (Num.pos p)),
  (match Num.zero with
    | Num.zero => h_1 ()
    | Num.pos p => h_2 p) =
    h_1 ()
-- Mathlib.CategoryTheory.Localization.Adjunction
CategoryTheory.Adjunction.Localization.η_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂)
  (W₂ : CategoryTheory.MorphismProperty C₂) [inst_4 : L₂.IsLocalization W₂] (G' : CategoryTheory.Functor D₁ D₂)
  (F' : CategoryTheory.Functor D₂ D₁) [inst_5 : CategoryTheory.CatCommSq G L₁ L₂ G']
  [inst_6 : CategoryTheory.CatCommSq F L₂ L₁ F'] (X₂ : C₂),
  (CategoryTheory.Adjunction.Localization.η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) =
    CategoryTheory.CategoryStruct.comp (G'.map ((CategoryTheory.CatCommSq.iso F L₂ L₁ F').inv.app X₂))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂))
        (L₂.map (adj.counit.app X₂)))
-- Mathlib.Order.Filter.Basic
Filter.frequently_iff_forall_eventually_exists_and : ∀ {α : Type u} {p : α → Prop} {f : Filter α},
  (∃ᶠ (x : α) in f, p x) ↔ ∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, p x ∧ q x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : Inhabited α]
  [EquivBEq α] [LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∪ m₂).getKey! k = m₁.getKey! k
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.unit.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.unit = 1
-- Mathlib.CategoryTheory.ObjectProperty.Ind
CategoryTheory.Limits.ColimitPresentation.reindex.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P P_1 : CategoryTheory.Limits.ColimitPresentation J X),
  P = P_1 →
    ∀ {J' : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} J'] (F F_1 : CategoryTheory.Functor J' J)
      (e_F : F = F_1) [inst_3 : F.Final], P.reindex F = P_1.reindex F_1
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- A locally compact manifold must be modelled on a locally compact space.  -/
LocallyCompactSpace.of_locallyCompact_manifold : ∀ {E : Type u_8} {𝕜 : Type u_9} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_10} [inst_3 : TopologicalSpace H] (M : Type u_11) [inst_4 : TopologicalSpace M]
  [ChartedSpace H M] (I : ModelWithCorners 𝕜 E H) [h : Nonempty M] [LocallyCompactSpace M], LocallyCompactSpace E
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- The range of an `AddMonoidHom` from an `AddGroup` is an `AddSubgroup`.  -/
AddMonoidHom.range : {G : Type u_1} → [inst : AddGroup G] → {N : Type u_5} → [inst_1 : AddGroup N] → (G →+ N) → AddSubgroup N
-- Mathlib.Algebra.MvPolynomial.Derivation
/-- The derivation on `MvPolynomial σ R` that takes value `f i` on `X i`.  -/
MvPolynomial.mkDerivation : {σ : Type u_1} →
  (R : Type u_2) →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : Module R A] →
            [inst_3 : Module (MvPolynomial σ R) A] →
              [IsScalarTower R (MvPolynomial σ R) A] → (σ → A) → Derivation R (MvPolynomial σ R) A
-- Mathlib.Data.ENNReal.Inv
/-- If `a ≠ 0` and `a ≠ ∞`, then division by `a` maps infimum to infimum.

See `ENNReal.iInf_div'` for the general case, and `ENNReal.iInf_div` for another special case that
assumes `Nonempty ι` but does not require `a ≠ ∞`.  -/
ENNReal.iInf_div_of_ne : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → (⨅ i, f i) / a = ⨅ i, f i / a
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_dite_of_false : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : AddCommMonoid M] {p : ι → Prop} [inst_1 : DecidablePred p]
  (h : ∀ i ∈ s, ¬p i) (f : (i : ι) → p i → M) (g : (i : ι) → ¬p i → M),
  (∑ i ∈ s, if hi : p i then f i hi else g i hi) = ∑ i, g ↑i ⋯
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instHasFiniteCoproductsScheme : CategoryTheory.Limits.HasFiniteCoproducts AlgebraicGeometry.Scheme
-- Mathlib.Probability.Distributions.Gaussian.Fernique
/-- If `x ↦ exp (C * ‖x‖ ^ 2)` is integrable with respect to the centered Gaussian
`μ ∗ (μ.map (ContinuousLinearEquiv.neg ℝ))`, then for all `C' < C`, `x ↦ exp (C' * ‖x‖ ^ 2)`
is integrable with respect to `μ`.  -/
ProbabilityTheory.IsGaussian.integrable_exp_sq_of_conv_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [SecondCountableTopology E] (μ : MeasureTheory.Measure E) [ProbabilityTheory.IsGaussian μ] {C C' : ℝ},
  MeasureTheory.Integrable (fun x => Real.exp (C * ‖x‖ ^ 2))
      (μ.conv (MeasureTheory.Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)) →
    0 < C' → C' < C → MeasureTheory.Integrable (fun x => Real.exp (C' * ‖x‖ ^ 2)) μ
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.dilatransvection.baseChange : ∀ {R : Type u_3} {V : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : CommRing A] [inst_4 : Algebra R A],
  ∀ e ∈ LinearEquiv.dilatransvections R V,
    LinearEquiv.baseChange R A V V e ∈ LinearEquiv.dilatransvections A (TensorProduct R A V)
-- Mathlib.SetTheory.Cardinal.Pigeonhole
/-- A function whose domain's cardinality is uncountable and strictly greater than its codomain's
has an uncountable fiber.  -/
Cardinal.exists_uncountable_fiber : ∀ {β α : Type u} (f : β → α), Cardinal.mk α < Cardinal.mk β → ∀ [Uncountable β], ∃ a, Uncountable ↑(f ⁻¹' {a})