mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
Subsemigroup.decidableMemCentralizer : {M : Type u_1} →
  {S : Set M} →
    [inst : Semigroup M] → (a : M) → [Decidable (∀ b ∈ S, b * a = a * b)] → Decidable (a ∈ Subsemigroup.centralizer S)
-- Mathlib.Analysis.Seminorm
Seminorm.instSup : {𝕜 : Type u_3} →
  {E : Type u_7} → [inst : SeminormedRing 𝕜] → [inst_1 : AddGroup E] → [inst_2 : SMul 𝕜 E] → Max (Seminorm 𝕜 E)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.inl_inr_pushoutAssoc_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄]
  [inst_4 :
    CategoryTheory.Limits.HasPushout g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))]
  {Z : C}
  (h :
    CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₃ g₄)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inr g₁
          (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ g₂)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inl
          (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
        h)
-- Mathlib.Algebra.Module.Injective
Module.Baer.extension_property_addMonoidHom : ∀ {Q : Type v} [inst : AddCommGroup Q] {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N], Module.Baer ℤ Q → ∀ (f : M →+ N), Function.Injective ⇑f → ∀ (g : M →+ Q), ∃ h, h.comp f = g
-- Mathlib.AlgebraicTopology.Quasicategory.Basic
SSet.quasicategory_of_filler : ∀ (S : SSet),
  (∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : (SSet.horn (n + 2) i).toSSet ⟶ S),
      0 < i →
        i < Fin.last (n + 2) →
          ∃ σ,
            ∀ (j : Fin (n + 3)) (h : j ≠ i),
              (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S j)) σ =
                (CategoryTheory.ConcreteCategory.hom (σ₀.app (Opposite.op { len := n + 1 }))) (SSet.horn.face i j h)) →
    S.Quasicategory
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.subsheafToTypes_obj : ∀ {X : TopCat} {T : ↑X → Type u_1} (P : TopCat.LocalPredicate T),
  (TopCat.subsheafToTypes P).obj = TopCat.subpresheafToTypes P.toPrelocalPredicate
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.tensorObj_def : ∀ {R : Type u} [inst : CommSemiring R] (M N : SemimoduleCat R),
  CategoryTheory.MonoidalCategoryStruct.tensorObj M N = SemimoduleCat.MonoidalCategory.tensorObj M N
-- Mathlib.Algebra.Order.GroupWithZero.Lex
LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedCommGroupWithZero α] [inst_1 : LinearOrderedCommGroupWithZero β]
  {n : β} (hn : n ≠ 0), (LinearOrderedCommGroupWithZero.inr α β) n = ↑((OrderMonoidHom.inrₗ αˣ βˣ) (Units.mk0 n hn))
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Functor.mapArrow_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (a : CategoryTheory.Arrow C),
  F.mapArrow.obj a = CategoryTheory.Arrow.mk (F.map a.hom)
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.sum_apply : ∀ {α : Type u_1} {ι : Type u_3} (f : ι → MeasureTheory.OuterMeasure α) (s : Set α),
  (MeasureTheory.OuterMeasure.sum f) s = ∑' (i : ι), (f i) s
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.map_eq_gaussianReal : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  ProbabilityTheory.HasGaussianLaw X P →
    MeasureTheory.Measure.map X P =
      ProbabilityTheory.gaussianReal (∫ (x : Ω), X x ∂P) (ProbabilityTheory.variance X P).toNNReal
-- Init.Data.UInt.Lemmas
UInt64.add_right_inj : ∀ {a b : UInt64} (c : UInt64), c + a = c + b ↔ a = b
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.coe_inv : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f : CauSeq β abv} (hf : ¬f.LimZero),
  ↑(f.inv hf) = (↑f)⁻¹
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetFilterResult.mk.inj : ∀ {finset : BigOperators.FinsetResult✝} {filter : Option Lean.Term} {finset_1 : BigOperators.FinsetResult✝}
  {filter_1 : Option Lean.Term},
  { finset := finset, filter := filter } = { finset := finset_1, filter := filter_1 } →
    finset = finset_1 ∧ filter = filter_1
-- Mathlib.GroupTheory.Commensurable
Subgroup.Commensurable.refl : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.Commensurable H
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_Iic_add_Ioi : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  MeasureTheory.IntegrableOn f (Set.Iic b) μ →
    MeasureTheory.IntegrableOn f (Set.Ioi b) μ →
      ∫ (x : ℝ) in Set.Iic b, f x ∂μ + ∫ (x : ℝ) in Set.Ioi b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitRightUnit : ∀ {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]
  (F G H : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)],
  (CategoryTheory.MonoidalCategory.externalProduct F
        (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)).IsLeftKanExtension
    (CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitRight
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)
      (CategoryTheory.MonoidalCategory.DayConvolution.unit G H) F)
-- Mathlib.Topology.Separation.CompletelyRegular
CompletelyRegularSpace.instRegularSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [CompletelyRegularSpace X], RegularSpace X
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.instIsSplitMonoInl : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q), CategoryTheory.IsSplitMono c.inl
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.merge.eq_2 : ∀ {α : Type u_1} (xs : List α) (le : α → α → Bool), (xs = [] → False) → xs.merge [] le = xs
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.eval_modulus_sub : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) (x : ZMod n), χ (↑n - x) = χ (-x)
-- Lean.Parser.Term.Basic
/-- Same as [`tacticSeq`] but requires delimiter-free tactic sequence to have strict indentation.
Falls back to an empty tactic sequence when no appropriately indented content follows, producing
an elaboration error (unsolved goals) rather than a parse error.  -/
Lean.Parser.Tactic.tacticSeqIndentGt : Lean.Parser.Parser
-- Mathlib.Topology.JacobsonSpace
Set.Finite.isDiscrete_of_subset_closedPoints : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, s.Finite → s ⊆ closedPoints X → IsDiscrete s
-- Mathlib.Order.Filter.SmallSets
Filter.eventually_smallSets : ∀ {α : Type u_1} {l : Filter α} {p : Set α → Prop}, (∀ᶠ (s : Set α) in l.smallSets, p s) ↔ ∃ s ∈ l, ∀ t ⊆ s, p t
-- Mathlib.MeasureTheory.Function.EssSup
essInf_count : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : CompleteLattice β] [MeasurableSingletonClass α]
  (f : α → β), essInf f MeasureTheory.Measure.count = ⨅ i, f i
-- Mathlib.Tactic.Lift
CanLift.mk : ∀ {α : Sort u_1} {β : Sort u_2} {coe : outParam (β → α)} {cond : outParam (α → Prop)},
  (∀ (x : α), cond x → ∃ y, coe y = x) → CanLift α β coe cond
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalence_unitIso_inv_app_unmop_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Cᴹᵒᵖᴹᵒᵖ),
  ((CategoryTheory.MonoidalOpposite.mopMopEquivalence C).unitIso.inv.app X).unmop.unmop =
    (CategoryTheory.CategoryStruct.id X.unmop).unmop
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.map_vadd : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace V]
  [inst_10 : IsTopologicalAddTorsor P] [inst_11 : TopologicalSpace W] [inst_12 : IsTopologicalAddTorsor Q]
  (f : P →ᴬ[R] Q) (p : P) (v : V), f (v +ᵥ p) = f.contLinear v +ᵥ f p
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- A group action is `n`-multiply preprimitive if it is `n`-multiply
pretransitive and if, when `n ≥ 1`, for every set `s` of cardinality
`n - 1`, the action of `fixingSubgroup M s` on the complement of `s`
is preprimitive.  -/
MulAction.IsMultiplyPreprimitive : (M : Type u_1) → (α : Type u_2) → [inst : Group M] → [MulAction M α] → ℕ → Prop
-- Lean.Meta.Tactic.Simp.Types
/-- Construct the `Expr` `h.mpr e`, from a `Simp.Result` with proof `h`.  -/
Lean.Meta.Simp.Result.mkEqMPR : Lean.Meta.Simp.Result → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.copy.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (f : α →+o β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = { toFun := f', map_zero' := ⋯, map_add' := ⋯, monotone' := ⋯ }
-- Init.Data.Int.Order
Int.add_lt_add_right : ∀ {a b : ℤ}, a < b → ∀ (c : ℤ), a + c < b + c
-- Mathlib.Order.CompleteLattice.Basic
iInf_lt_top : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {s : ι → α}, ⨅ i, s i < ⊤ ↔ ∃ i, s i < ⊤
-- Mathlib.CategoryTheory.Sites.SheafHom
CategoryTheory.presheafHom_map_app_op_mk_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {F G : CategoryTheory.Functor Cᵒᵖ A} {X Y : C} (g : Y ⟶ X) (α : (CategoryTheory.presheafHom F G).obj (Opposite.op X)),
  ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.presheafHom F G).map g.op)) α).app
      (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id Y))) =
    α.app (Opposite.op (CategoryTheory.Over.mk g))
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_xor : ∀ {w i : ℕ} {x y : BitVec w}, (x ^^^ y).getMsbD i = (x.getMsbD i ^^ y.getMsbD i)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isLE_iff_isZero_truncGE_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ → ∀ (X : C), t.IsLE X n₀ ↔ CategoryTheory.Limits.IsZero ((t.truncGE n₁).obj X)
-- Init.Data.List.Basic
List.find?_nil : ∀ {α : Type u} {p : α → Bool}, List.find? p [] = none
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.right_unitor_hom_inv : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b), CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Order.Filter.NAry
/-- If `a` is a left identity for `f : α → β → β`, then `pure a` is a left identity for
`Filter.map₂ f`.  -/
Filter.map₂_left_identity : ∀ {α : Type u_1} {β : Type u_3} {f : α → β → β} {a : α},
  (∀ (b : β), f a b = b) → ∀ (l : Filter β), Filter.map₂ f (pure a) l = l
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isIso_πTruncGE_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ),
  CategoryTheory.IsIso (K.πTruncGE n) ↔ K.IsStrictlyGE n
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
/-- This lemma reorders the elements of a triangle in the tripartite graph. It turns a triangle
`{x, y, z}` into a triangle `{a, b, c}` where `a : α `, `b : β`, `c : γ`.  -/
SimpleGraph.TripartiteFromTriangles.graph_triple : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : DecidableEq γ] ⦃x y z : α ⊕ β ⊕ γ⦄,
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj x y →
    (SimpleGraph.TripartiteFromTriangles.graph t).Adj x z →
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj y z →
        ∃ a b c,
          {Sum3.in₀ a, Sum3.in₁ b, Sum3.in₂ c} = {x, y, z} ∧
            (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ∧
              (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ∧
                (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.toStream_toList : ∀ {α : Type u_1} {t : RBTree.RBNode α}, t.toStream.toList = t.toList
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_dropWhile_takeWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, ((s.takeWhile pat).dropWhile pat).isEmpty = true
-- Lean.Elab.Syntax
Lean.Elab.Term.ToParserDescrContext.mk.injEq : ∀ (catName : Lean.Name) (first leftRec : Bool) (behavior : Lean.Parser.LeadingIdentBehavior) (catName_1 : Lean.Name)
  (first_1 leftRec_1 : Bool) (behavior_1 : Lean.Parser.LeadingIdentBehavior),
  ({ catName := catName, first := first, leftRec := leftRec, behavior := behavior } =
      { catName := catName_1, first := first_1, leftRec := leftRec_1, behavior := behavior_1 }) =
    (catName = catName_1 ∧ first = first_1 ∧ leftRec = leftRec_1 ∧ behavior = behavior_1)
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.instComonObjModuleCatOfCarrier : {R : Type u} → [inst : CommRing R] → (X : CoalgCat R) → CategoryTheory.ComonObj (ModuleCat.of R ↑X.toModuleCat)
-- Init.Simproc
/-- A builtin defeq simplification procedure.
 -/
Lean.Parser.«command__Builtin_dsimproc__[_]_(_):=_» : Lean.ParserDescr
-- Lean.Meta.Hint
/-- Creates a hint message with associated code action suggestions.

To provide a hint without an associated code action, use `MessageData.hint'`.

The arguments are as follows:
* `hint`: the main message of the hint, which precedes its code action suggestions.
* `suggestions`: the suggestions to display.
* `ref?`: if specified, the syntax location for the code action suggestions; otherwise, default to
  the syntax reference in the monadic state. Will be overridden by the `span?` field on any
  suggestions that specify it.
* `codeActionPrefix?`: if specified, text to display in place of "Try this: " in the code action
  label
* `forceList`: if `true`, suggestions will be displayed as a bulleted list even if there is only one.
 -/
Lean.MessageData.hint : Lean.MessageData →
  Array Lean.Meta.Hint.Suggestion →
    optParam (Option Lean.Syntax) none →
      optParam (Option String) none → optParam Bool false → Lean.CoreM Lean.MessageData
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
CategoryTheory.PreservesImage.factorThruImage_comp_hom_assoc : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Limits.HasEqualizers A] [inst_3 : CategoryTheory.Limits.HasImages A]
  [inst_4 : CategoryTheory.StrongEpiCategory B] [inst_5 : CategoryTheory.Limits.HasImages B]
  (L : CategoryTheory.Functor A B)
  [inst_6 :
    ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L]
  [inst_7 :
    ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L]
  {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj (CategoryTheory.Limits.image f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (L.map f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom h) =
    CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.factorThruImage f)) h
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.isInvertible_equiv_comp : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [inst : TopologicalSpace M]
  [inst_1 : TopologicalSpace M₂] [inst_2 : TopologicalSpace M₃] [inst_3 : Semiring R] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₂] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] {e : M₂ ≃L[R] M₃} {f : M →L[R] M₂}, (↑e ∘SL f).IsInvertible ↔ f.IsInvertible
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.mk.injEq : ∀ {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₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (φQ : h₁.Q ⟶ h₂.Q) (φH : h₁.H ⟶ h₂.H)
  (commp :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.p φQ = CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p)
      CategoryTheory.ShortComplex.RightHomologyMapData.commp._autoParam)
  (commg' :
    autoParam (CategoryTheory.CategoryStruct.comp φQ h₂.g' = CategoryTheory.CategoryStruct.comp h₁.g' φ.τ₃)
      CategoryTheory.ShortComplex.RightHomologyMapData.commg'._autoParam)
  (commι :
    autoParam (CategoryTheory.CategoryStruct.comp φH h₂.ι = CategoryTheory.CategoryStruct.comp h₁.ι φQ)
      CategoryTheory.ShortComplex.RightHomologyMapData.commι._autoParam)
  (φQ_1 : h₁.Q ⟶ h₂.Q) (φH_1 : h₁.H ⟶ h₂.H)
  (commp_1 :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.p φQ_1 = CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p)
      CategoryTheory.ShortComplex.RightHomologyMapData.commp._autoParam)
  (commg'_1 :
    autoParam (CategoryTheory.CategoryStruct.comp φQ_1 h₂.g' = CategoryTheory.CategoryStruct.comp h₁.g' φ.τ₃)
      CategoryTheory.ShortComplex.RightHomologyMapData.commg'._autoParam)
  (commι_1 :
    autoParam (CategoryTheory.CategoryStruct.comp φH_1 h₂.ι = CategoryTheory.CategoryStruct.comp h₁.ι φQ_1)
      CategoryTheory.ShortComplex.RightHomologyMapData.commι._autoParam),
  ({ φQ := φQ, φH := φH, commp := commp, commg' := commg', commι := commι } =
      { φQ := φQ_1, φH := φH_1, commp := commp_1, commg' := commg'_1, commι := commι_1 }) =
    (φQ = φQ_1 ∧ φH = φH_1)
-- Mathlib.Testing.Plausible.Functions
List.dlookup.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (x : List (Sigma β)),
  List.dlookup a x =
    match x with
    | [] => none
    | ⟨a', b⟩ :: l => if h : a' = a then some (Eq.recOn h b) else List.dlookup a l
-- Std.Data.Iterators.Consumers.Monadic.Set
/-- Traverses the given iterator and stores the emitted values in a {name}`ExtHashSet`.

If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α m`,
the variant {lean}`it.ensureTermination.toExtHashSet` always terminates after finitely many steps.
 -/
Std.IterM.toExtHashSet : {α β : Type w} →
  [inst : BEq β] →
    [inst_1 : Hashable β] →
      [EquivBEq β] →
        [LawfulHashable β] →
          {m : Type w → Type w'} →
            [Monad m] → [inst_5 : Std.Iterator α m β] → [Std.IteratorLoop α m m] → Std.IterM m β → m (Std.ExtHashSet β)
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.pushforward.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : AddGroup A] [inst_1 : AddGroup B]
  [inst_2 : AddGroup C] [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C]
  {φ : A →+ B} {ψ : B →+ C} (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A]
  [inst_7 : IsTopologicalAddGroup B] [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A]
  [inst_10 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [inst_11 : NormedSpace ℝ E]
  [inst_12 : IsTopologicalAddGroup C] [inst_13 : LocallyCompactSpace B],
  H.pushforward μA =
    {
      toFun := fun f =>
        { toFun := fun c => ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA, continuous_toFun := ⋯,
          hasCompactSupport' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
CategoryTheory.Abelian.Ext.smul_hom : ∀ {R : Type t} [inst : Ring R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : CategoryTheory.HasExt C] {X Y : C}
  {n : ℕ} (x : CategoryTheory.Abelian.Ext X Y n) (r : R) [inst_5 : HasDerivedCategory C], (r • x).hom = r • x.hom
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.differentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (iso : E ≃L[𝕜] F), Differentiable 𝕜 ⇑iso
-- Mathlib.Algebra.Group.End
Equiv.Perm.one_trans : ∀ {α : Type u_7} {β : Sort u_8} (e : α ≃ β), Equiv.trans 1 e = e
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.instMonadQuotationParenthesizerM : Lean.MonadQuotation Lean.PrettyPrinter.ParenthesizerM
-- Mathlib.Data.Nat.Totient
Nat.sum_totient' : ∀ (n : ℕ), ∑ m ∈ Finset.range n.succ with m ∣ n, m.totient = n
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.HasBiproduct.mk' : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C},
  Nonempty (CategoryTheory.Limits.LimitBicone F) → CategoryTheory.Limits.HasBiproduct F
-- Mathlib.Data.Multiset.Fintype
Multiset.map_univ : ∀ {α : Type u_1} [inst : DecidableEq α] {β : Type u_3} (m : Multiset α) (f : α → β),
  Multiset.map (fun x => f x.fst) Finset.univ.val = Multiset.map f m
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid contains `1`.  -/
Submonoid.one_mem' : ∀ {M : Type u_3} [inst : MulOneClass M] (self : Submonoid M), 1 ∈ self.carrier
-- Lean.Expr
/-- Cached hash code, cached results, and other data for `Expr`.
-  hash           : 32-bits
-  approxDepth    : 8-bits -- the approximate depth is used to minimize the number of hash collisions
-  hasFVar        : 1-bit -- does it contain free variables?
-  hasExprMVar    : 1-bit -- does it contain metavariables?
-  hasLevelMVar   : 1-bit -- does it contain level metavariables?
-  hasLevelParam  : 1-bit -- does it contain level parameters?
-  looseBVarRange : 20-bits

Remark: this is mostly an internal datastructure used to implement `Expr`,
most will never have to use it.
 -/
Lean.Expr.Data : Type