mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
/-- The two definitions of the conditional expectation `condExp` and `condLExp` (for Bochner and
Lebesgue integrals respectively) agree almost everywhere.  -/
MeasureTheory.condLExp_ofReal : ∀ {𝓧 : Type u_1} (m : MeasurableSpace 𝓧) {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} {f : 𝓧 → ℝ},
  MeasureTheory.Integrable f μ →
    0 ≤ᵐ[μ] f → μ⁻[fun x => ENNReal.ofReal (f x) | m] =ᵐ[μ] fun x => ENNReal.ofReal (μ[f | m] x)
-- Mathlib.Logic.Pairwise
Set.pairwise_of_forall : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), (∀ (a b : α), r a b) → s.Pairwise r
-- Mathlib.RingTheory.IsTensorProduct
TensorProduct.isBaseChange : ∀ (R : Type u_1) (M : Type v₁) (S : Type v₃) [inst : AddCommMonoid M] [inst_1 : CommSemiring R]
  [inst_2 : CommSemiring S] [inst_3 : Algebra R S] [inst_4 : Module R M], IsBaseChange S ((TensorProduct.mk R S M) 1)
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.below : {R : Type u} →
  {X : Type v} →
    [inst : CommRing R] →
      {motive : (a a_1 : FreeNonUnitalNonAssocAlgebra R X) → FreeLieAlgebra.Rel R X a a_1 → Prop} →
        {a a_1 : FreeNonUnitalNonAssocAlgebra R X} → FreeLieAlgebra.Rel R X a a_1 → Prop
-- Init.Core
/-- When the kernel tries to reduce a term `Lean.reduceBool c`, it will invoke the Lean interpreter to evaluate `c`.
The kernel will not use the interpreter if `c` is not a constant.
This feature is useful for performing proofs by reflection.

Remark: the Lean frontend allows terms of the from `Lean.reduceBool t` where `t` is a term not containing
free variables. The frontend automatically declares a fresh auxiliary constant `c` and replaces the term with
`Lean.reduceBool c`. The main motivation is that the code for `t` will be pre-compiled.

Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
This is extra 30k lines of code. More importantly, you will probably not be able to check your development using
external type checkers that do not implement this feature.
Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
So, you are mainly losing the capability of type checking your development using external checkers.

Recall that the compiler trusts the correctness of all `[implemented_by ...]` and `[extern ...]` annotations.
If an extern function is executed, then the trusted code base will also include the implementation of the associated
foreign function.
 -/
Lean.reduceBool : Bool → Bool
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualAnnihilator_le_dualAnnihilator_iff : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {W W' : Subspace K V},
  Submodule.dualAnnihilator W ≤ Submodule.dualAnnihilator W' ↔ W' ≤ W
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.Equiv.beq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [inst : BEq β] {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] [ReflBEq β], m₁.WF → m₂.WF → m₁.Equiv m₂ → Std.DTreeMap.Internal.Impl.Const.beq m₁ m₂ = true
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α} {fallback : β a}, t.isEmpty = true → t.getD a fallback = fallback
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- If `φ : S₁ ⟶ S₂` is a morphism of short complexes such that `φ.τ₁` is epi, `φ.τ₂` is an iso
and `φ.τ₃` is mono, then a right homology data for `S₂` induces a right homology data for `S₁` with
the same `Q` and `H` fields. This is obtained by dualising `LeftHomologyData.ofEpiOfIsIsoOfMono`.
The inverse construction is `ofEpiOfIsIsoOfMono`.  -/
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          S₂.RightHomologyData →
            [CategoryTheory.Epi φ.τ₁] → [CategoryTheory.IsIso φ.τ₂] → [CategoryTheory.Mono φ.τ₃] → S₁.RightHomologyData
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.End.mem_subsemigroupCenter_iff : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  {f : Module.End R M},
  f ∈ Subsemigroup.center (Module.End R M) ↔ ∃ α, ∃ (hα : α ∈ Subsemigroup.center R), f = Module.End.smulLeft α hα
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
_private.Mathlib.CategoryTheory.Limits.Shapes.Countable.0.CategoryTheory.Limits.IsCofiltered.preorder_of_cofiltered : (J : Type u_3) →
  [inst : CategoryTheory.Category.{v_2, u_3} J] →
    [CategoryTheory.IsCofiltered J] → ProofWanted (∃ I x, ∃ (_ : CategoryTheory.IsCofiltered I), ∃ F, F.Initial)
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetsExtEntry.global : Lean.Name → Lean.Widget.PanelWidgetsExtEntry
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.slope.eq_1 : ∀ {F : Type u} [inst : Field F] (W : WeierstrassCurve.Affine F) [inst_1 : DecidableEq F] (x₁ x₂ y₁ y₂ : F),
  W.slope x₁ x₂ y₁ y₂ =
    if x₁ = x₂ then
      if y₁ = W.negY x₂ y₂ then 0 else (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
    else (y₁ - y₂) / (x₁ - x₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- A morphism from the wide pullback `(f₁, f₂, f₃)` to the pullback of `f₁` and `f₃`
that is compatible with projections.  -/
CategoryTheory.Limits.ChosenPullback₃.l : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {f₃ : X₃ ⟶ S} →
            {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} →
              {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃} →
                {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} →
                  (self : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) → h₁₃.LiftStruct self.p₁ self.p₃ self.p
-- Mathlib.Algebra.Category.Ring.Limits
/-- If `(F ⋙ forget SemiRingCat).sections` is `u`-small, `F` has a limit.  -/
SemiRingCat.hasLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J SemiRingCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections], CategoryTheory.Limits.HasLimit F
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_eq_arg_iff : ∀ {x y : ℂ}, x ≠ 0 → y ≠ 0 → (x.arg = y.arg ↔ ↑‖y‖ / ↑‖x‖ * x = y)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_roo_eq_some_iff : ∀ {k m n i : ℕ}, (m<...n).toList[i]? = some k ↔ i < n - (m + 1) ∧ m + 1 + i = k
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.inverse'_toFun : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {φ' : N →* M} {R : Type u_10}
  [inst_2 : Semiring R] [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S]
  [inst_5 : MulSemiringAction N S] (f : R →ₑ+*[φ] S) (g : S → R) (k : Function.RightInverse ⇑φ' ⇑φ)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (a : S), (f.inverse' g k h₁ h₂) a = g a
-- Init.Data.Fin.Lemmas
Fin.castSucc_natAdd : ∀ {k : ℕ} (n : ℕ) (i : Fin k), (Fin.natAdd n i).castSucc = Fin.natAdd n i.castSucc
-- Mathlib.Algebra.Homology.HomotopyCategory
CategoryTheory.instAdditiveHomotopyCategoryMapHomotopyCategory : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {W : Type u_3} [inst_2 : CategoryTheory.Category.{v_1, u_3} W] [inst_3 : CategoryTheory.Preadditive W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.Additive] (c : ComplexShape ι), (F.mapHomotopyCategory c).Additive
-- Mathlib.Data.List.Forall2
List.SublistForall₂.below.cons_right : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}
  {motive : (a : List α) → (a_1 : List β) → List.SublistForall₂ R a a_1 → Prop} {a : β} {l₁ : List α} {l₂ : List β}
  (a_1 : List.SublistForall₂ R l₁ l₂), List.SublistForall₂.below a_1 → motive l₁ l₂ a_1 → List.SublistForall₂.below ⋯
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- The type of continuous maps which map zero to zero.

Note that one should never use the structure projection `ContinuousMapZero.toContinuousMap` and
instead favor the coercion `(↑) : C(X, R)₀ → C(X, R)` available from the instance of
`ContinuousMapClass`. All the instances on `C(X, R)₀` from `C(X, R)` passes through this coercion,
not the structure projection. Of course, the two are definitionally equal, but not reducibly so.  -/
ContinuousMapZero : (X : Type u_1) → (R : Type u_2) → [Zero X] → [Zero R] → [TopologicalSpace X] → [TopologicalSpace R] → Type (max u_1 u_2)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_left_Ici : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → ∀ (b : G₀), (fun x => a * x) '' Set.Ici b = Set.Ici (a * b)
-- Mathlib.Topology.Algebra.Monoid
/-- This lemma exists to ensure that we can still do the simplification `pure_le_nhds_iff`
after simplifying with `pure_one`.  -/
one_le_nhds_iff : ∀ {X : Type u_5} [inst : TopologicalSpace X] [T1Space X] [inst_2 : One X] {b : X}, 1 ≤ nhds b ↔ 1 = b
-- Mathlib.Order.Filter.Map
Filter.le_map_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {g : Filter β}, g ≤ Filter.map m f ↔ ∀ s ∈ f, m '' s ∈ g
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.sdiv.match_1.splitter : (motive : Bool → Bool → Sort u_1) →
  (x x_1 : Bool) →
    (Unit → motive false false) →
      (Unit → motive false true) → (Unit → motive true false) → (Unit → motive true true) → motive x x_1
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The minimum of an integrable function is smaller than its integral.  -/
MeasureTheory.exists_le_integral : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.Integrable f μ → ∃ x, f x ≤ ∫ (a : α), f a ∂μ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_source : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.expMap.source = Set.univ
-- Mathlib.Algebra.Torsor.Basic
/-- Pushforward of an add torsor along a surjective map.  -/
Function.Surjective.addTorsor : {G : Type u_1} →
  {P : Type u_2} →
    {Q : Type u_3} →
      [inst : AddGroup G] →
        [inst_1 : AddTorsor G P] →
          [inst_2 : VAdd G Q] →
            [inst_3 : VSub G Q] →
              (f : P → Q) →
                Function.Surjective f →
                  (∀ (c : G) (x : P), f (c +ᵥ x) = c +ᵥ f x) → (∀ (x y : P), x -ᵥ y = f x -ᵥ f y) → AddTorsor G Q
-- Lean.MetavarContext
Lean.instHashableLocalInstance : Hashable Lean.LocalInstance
-- Init.Data.Int.Order
Int.eq_nat_or_neg : ∀ (a : ℤ), ∃ n, a = ↑n ∨ a = -↑n
-- Mathlib.Algebra.Colimit.Ring
/-- The canonical map from a component to the direct limit.  -/
Ring.DirectLimit.of : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [inst_1 : (i : ι) → CommRing (G i)] → (f : (i j : ι) → i ≤ j → G i → G j) → (i : ι) → G i →+* Ring.DirectLimit G f
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.toAddEquiv_reindexLinearEquiv : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [inst : Semiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] (eₘ : m ≃ m') (eₙ : n ≃ n'),
  ↑(Matrix.reindexLinearEquiv R A eₘ eₙ) = Matrix.reindexAddEquiv A eₘ eₙ
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.le_iff : ∀ {M : Type u_1} [inst : AddZeroClass M] {c d : AddCon M}, c ≤ d ↔ ↑c ≤ ↑d
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.model_nonemptyTheory_iff : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M], M ⊨ L.nonemptyTheory ↔ Nonempty M
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.norm_comp_le : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] (g : NormedAddGroupHom V₂ V₃)
  (f : NormedAddGroupHom V₁ V₂), ‖g.comp f‖ ≤ ‖g‖ * ‖f‖
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.toArray_toList : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → m.toList.toArray = m.toArray
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.id_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.Hom.id sq).τ₁ = CategoryTheory.CategoryStruct.id sq.X₁
-- Mathlib.Topology.Category.TopCat.Opens
Topology.IsInducing.map_functorObj : ∀ {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f))
  (U : TopologicalSpace.Opens ↑X), (TopologicalSpace.Opens.map f).obj (hf.functorObj U) = U
-- Std.Http.Data.URI.Basic
Std.Http.RequestTarget.instToString : ToString Std.Http.RequestTarget
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndepOn_insert : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {s : Set ι} {a : ι} {f : ι → V},
  a ∉ s → (LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ Submodule.span K (f '' s))
-- Std.Async.Select
Std.Async.Selectable.case : {α β : Type} → Std.Async.Selector β → (β → Std.Async.Async α) → Std.Async.Selectable α
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that the integer parts of the continued fraction are at least one.  -/
GenContFract.of_one_le_get?_partDen : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K] {b : K}, (GenContFract.of v).partDens.get? n = some b → 1 ≤ b
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : LawfulBEq α] {k : α} (h : k ∈ m),
  m.get k h = k
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.instInvSubtypeMemSubmonoidSpecialUnitaryGroup : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {α : Type v} → [inst_2 : CommRing α] → [inst_3 : StarRing α] → Inv ↥(Matrix.specialUnitaryGroup n α)
-- Mathlib.Analysis.Normed.Group.Quotient
/-- An isometric version of `Submodule.quotientQuotientEquivQuotientSup`.  -/
Submodule.quotientQuotientLIEQuotientSup : {M : Type u_1} →
  [inst : SeminormedAddCommGroup M] →
    {R : Type u_3} →
      [inst_1 : Ring R] →
        [inst_2 : Module R M] → (S T : Submodule R M) → (M ⧸ S) ⧸ Submodule.map S.mkQ T ≃ₗᵢ[R] M ⧸ S ⊔ T
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_mul_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {β : Type u_5} [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] {s t : Finset α} {f : α → β} {a : β}, (s * t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x * y) ≤ a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.hasNumericLoHi : Lean.Meta.Grind.Arith.Cutsat.ToIntM Bool
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.evaluationPreservesLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [CategoryTheory.Limits.HasLimits C] (k : K),
  CategoryTheory.Limits.PreservesLimits ((CategoryTheory.evaluation K C).obj k)
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mapRingHom_algebraMap : ∀ {R : Type u} [inst : CommSemiring R] {A : Type u_5} [inst_1 : CommSemiring A] [inst_2 : Algebra R A],
  CommRing.Pic.mapRingHom (algebraMap R A) = CommRing.Pic.mapAlgebra R A
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.denom_add_dvd : ∀ {K : Type u} [inst : Field K] (x y : RatFunc K), (x + y).denom ∣ x.denom * y.denom
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.of'_commute : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M] {a : M},
  (∀ (a' : M), AddCommute a a') → ∀ (f : AddMonoidAlgebra R M), Commute (AddMonoidAlgebra.of' R M a) f
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.mod_eq_self_iff : ∀ {R : Type u} [inst : Field R] {p q : Polynomial R}, q ≠ 0 → (p % q = p ↔ p.degree < q.degree)
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.geometricPMFReal_pos : ∀ {p : ℝ} {n : ℕ}, 0 < p → p < 1 → 0 < ProbabilityTheory.geometricPMFReal p n
-- Mathlib.CategoryTheory.Abelian.ShortExact
CategoryTheory.ShortExact.shortExact_map_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] [F.Faithful] {S : CategoryTheory.ShortComplex C}
  [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Limits.PreservesFiniteLimits F],
  (S.map F).ShortExact ↔ S.ShortExact
-- Mathlib.CategoryTheory.Preadditive.LiftToFinset
CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app_eq_sum : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {α : Type w} [inst_3 : DecidableEq α] (f : α → C)
  [inst_4 : CategoryTheory.Limits.HasCoproduct f] (S : Finset (CategoryTheory.Discrete α)),
  (CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone f).ι.app S =
    ∑ a ∈ S.attach,
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.π (fun a => f (↑a).as) a)
        (CategoryTheory.Limits.Sigma.ι f (↑a).as)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_insert_le_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k fallback : α}, (cmp ((t.insert k).minD fallback) k).isLE = true
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.TriangleIndexData.mk.sizeOf_spec : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [inst : Zero I₂] {r : I₁ × I₂ × I₃ → J}
  {π : I₁ × I₃ → J} [inst_1 : SizeOf I₁] [inst_2 : SizeOf I₂] [inst_3 : SizeOf I₃] [inst_4 : SizeOf J]
  (p₁₂ : I₁ × I₂ → I₁) (hp₁₂ : ∀ (i : I₁ × I₂ × I₃), π (p₁₂ (i.1, i.2.1), i.2.2) = r i) (p₂₃ : I₂ × I₃ → I₃)
  (hp₂₃ : ∀ (i : I₁ × I₂ × I₃), π (i.1, p₂₃ i.2) = r i) (h₁ : ∀ (i₁ : I₁), p₁₂ (i₁, 0) = i₁)
  (h₃ : ∀ (i₃ : I₃), p₂₃ (0, i₃) = i₃),
  sizeOf { p₁₂ := p₁₂, hp₁₂ := hp₁₂, p₂₃ := p₂₃, hp₂₃ := hp₂₃, h₁ := h₁, h₃ := h₃ } = 1
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.modifyBody : (Lean.IR.FnBody → Lean.IR.FnBody) → Lean.IR.Alt → Lean.IR.Alt
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.inv_hom_apply : ∀ {X Y : PartOrdEmb} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
/-- The standard setup for the commutation of bifunctors with shifts by `ℤ`.  -/
CategoryTheory.CommShift₂Setup.int : {D : Type u_5} →
  [inst : CategoryTheory.Category.{v_5, u_5} D] →
    [inst_1 : CategoryTheory.Preadditive D] →
      [inst_2 : CategoryTheory.HasShift D ℤ] →
        [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] → CategoryTheory.CommShift₂Setup D ℤ
-- Mathlib.Order.SuccPred.InitialSeg
InitialSeg.apply_wCovBy_apply_iff : ∀ {α : Type u_1} {β : Type u_2} {a b : α} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α ≤i β),
  f a ⩿ f b ↔ a ⩿ b
-- Lean.Meta.Tactic.Grind.Inv
_private.Lean.Meta.Tactic.Grind.Inv.0.Lean.Meta.Grind.checkParents : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- The homomorphisms induced by extension of fractional ideals compose in towers.  -/
FractionalIdeal.extendedHom'_comp : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N)
  {C : Type u_5} {W : Type u_6} [inst_8 : CommRing C] [inst_9 : CommRing W] [inst_10 : Algebra C W] {P : Submonoid C}
  [inst_11 : IsLocalization P W] {g : B →+* C} (hg : N ≤ Submonoid.comap g P),
  (FractionalIdeal.extendedHom' W hg).comp (FractionalIdeal.extendedHom' L hf) = FractionalIdeal.extendedHom' W ⋯
-- Std.Sat.AIG.CachedGates
/-- Create an or gate in the input AIG. This uses the builtin cache to enable automated subterm sharing.
 -/
Std.Sat.AIG.mkOrCached : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- Typeclass expressing that for all `G`-split pairs `f,g`, `f` and `g` have a coequalizer.  -/
CategoryTheory.Monad.HasCoequalizerOfIsSplitPair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] → CategoryTheory.Functor D C → Prop
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.coe_zero_iff : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] M₂), ⇑f = 0 ↔ f = 0
-- Mathlib.Analysis.LocallyConvex.Montel
ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : IsTopologicalAddGroup E] [inst_6 : ContinuousSMul 𝕜₁ E] [inst_7 : AddCommGroup F] [inst_8 : Module 𝕜₂ F]
  [inst_9 : TopologicalSpace F] [inst_10 : IsTopologicalAddGroup F] [inst_11 : ContinuousSMul 𝕜₂ F]
  [inst_12 : T1Space E] [inst_13 : MontelSpace 𝕜₁ E] (f : CompactConvergenceCLM σ E F) (x : E),
  ((ContinuousLinearEquiv.toCompactConvergenceCLM σ E F).symm f) x = f x
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_functor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max w v)))
  {X Y : F.Elementsᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence F).functor.map f =
    CategoryTheory.CostructuredArrow.homMk (↑(Opposite.unop f)).unop ⋯
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- A version that takes a natural number and `Nat.Prime`.  -/
Ideal.exists_isMaximal_dvd_of_dvd_absNorm' : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  {p : ℕ},
  Nat.Prime p → ∀ (I : Ideal S), p ∣ Ideal.absNorm I → ∃ P, P.IsMaximal ∧ Ideal.under ℤ P = Ideal.span {↑p} ∧ P ∣ I
-- Mathlib.Algebra.Group.Pi.Units
MulEquiv.val_inv_piUnits_symm_apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (f : (i : ι) → (M i)ˣ) (x : ι),
  ↑(MulEquiv.piUnits.symm f)⁻¹ x = (f x).inv
-- Aesop.RuleTac.Basic
Aesop.RuleTacOutput.mk : Array Aesop.RuleApplication → Aesop.RuleTacOutput
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.forM_eq_forM_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit.{w + 1}}, forM t f = forM t.toList f
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.left_inv : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (self : L ≃ᴸ L'),
  self.invLHom.comp self.toLHom = FirstOrder.Language.LHom.id L