mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Construct a morphism in `P.Over Q X` from a morphism in `Over X`.  -/
CategoryTheory.MorphismProperty.Over.Hom.mk : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      {X : T} →
        [inst_1 : Q.IsMultiplicative] →
          {A B : P.Over Q X} →
            (f :
                (CategoryTheory.MorphismProperty.Over.forget P Q X).obj A ⟶
                  (CategoryTheory.MorphismProperty.Over.forget P Q X).obj B) →
              Q (CategoryTheory.Over.Hom.left f) → (A ⟶ B)
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.toGHSpace_lipschitz : ∀ {X : Type u} [inst : MetricSpace X], LipschitzWith 1 TopologicalSpace.NonemptyCompacts.toGHSpace
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_inv_assoc : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] [inst_6 : F.LaxRightLinear C] (d : D) {Z : D'}
  (h :
    F.obj
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxRightLinear.μᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h) =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).inv) h
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies expressions of the form `Nat.div a b`,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalNatDiv : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.brecOn.eq : ∀ {C : Type u} {motive : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C → Sort u_1}
  (t : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C)
  (F_1 :
    (t : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
      CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.below t → motive t),
  CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.brecOn t F_1 =
    F_1 t (CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.brecOn.go t F_1).2
-- Mathlib.MeasureTheory.Measure.FiniteMeasurePi
MeasureTheory.FiniteMeasure.mass_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.FiniteMeasure (α i)), (MeasureTheory.FiniteMeasure.pi μ).mass = ∏ i, (μ i).mass
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.kernel.ι_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.Limits.kernel.ι f.op).unop =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.kernelOpUnop f).inv)
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.brecOn.eq : ∀ {motive_1 : Mathlib.Tactic.Translate.ArgReorder → Sort u}
  {motive_2 : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u}
  {motive_3 : List (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u}
  {motive_4 : ℕ × Mathlib.Tactic.Translate.ArgReorder → Sort u} (t : Mathlib.Tactic.Translate.ArgReorder)
  (F_1 : (t : Mathlib.Tactic.Translate.ArgReorder) → t.below → motive_1 t)
  (F_2 :
    (t : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)) → Mathlib.Tactic.Translate.ArgReorder.below_1 t → motive_2 t)
  (F_3 :
    (t : List (ℕ × Mathlib.Tactic.Translate.ArgReorder)) → Mathlib.Tactic.Translate.ArgReorder.below_2 t → motive_3 t)
  (F_4 : (t : ℕ × Mathlib.Tactic.Translate.ArgReorder) → Mathlib.Tactic.Translate.ArgReorder.below_3 t → motive_4 t),
  t.brecOn F_1 F_2 F_3 F_4 = F_1 t (Mathlib.Tactic.Translate.ArgReorder.brecOn.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.fderivCLM_eq_of_scalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n k : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F]
  (𝕜' : Type u_6) [inst_8 : NontriviallyNormedField 𝕜'] [inst_9 : NormedSpace 𝕜' F] [inst_10 : Algebra ℝ 𝕜']
  [inst_11 : IsScalarTower ℝ 𝕜' F], ⇑(TestFunction.fderivCLM 𝕜 n k) = ⇑(TestFunction.fderivCLM 𝕜' n k)
-- Mathlib.GroupTheory.SchurZassenhaus
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime`  -/
_private.Mathlib.GroupTheory.SchurZassenhaus.0.Subgroup.exists_right_complement'_of_coprime_aux : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [IsMulCommutative ↥H] [H.FiniteIndex] [H.Normal],
  (Nat.card ↥H).Coprime H.index → ∃ K, H.IsComplement' K
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.trans_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E),
  (e.trans f).inverse = f.inverse.comp e.inverse
-- Mathlib.CategoryTheory.Products.Basic
/-- The forward direction for `functorProdFunctorEquiv`  -/
CategoryTheory.prodFunctorToFunctorProd : (A : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    (B : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        (C : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            CategoryTheory.Functor (CategoryTheory.Functor A B × CategoryTheory.Functor A C)
              (CategoryTheory.Functor A (B × C))
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.coprod.fst.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.Limits.coprod.fst X Y = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id X) 0
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- Characterisation of `2`-Freiman homomorphisms.  -/
isAddFreimanHom_two : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsAddFreimanHom 2 A B f ↔ Set.MapsTo f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a + b = c + d → f a + f b = f c + f d
-- Mathlib.Order.Interval.Set.Basic
Set.nonempty_Ioo_subtype : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} [DenselyOrdered α], a < b → Nonempty ↑(Set.Ioo a b)
-- Init.Data.Nat.ToString
Nat.toString_eq_ofList_toDigits : ∀ {n : ℕ}, toString n = String.ofList (Nat.toDigits 10 n)
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftEval_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ)
  (hi : n + i = i') (X : CochainComplex C ℤ),
  (CochainComplex.shiftEval C n i i' hi).hom.app X = (HomologicalComplex.XIsoOfEq X ⋯).hom
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.lintegral_tendsto_of_nat : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {φ : ℕ → Set α},
  MeasureTheory.AECover μ Filter.atTop φ →
    ∀ {f : α → ENNReal},
      AEMeasurable f μ → Filter.Tendsto (fun x => ∫⁻ (x : α) in φ x, f x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), f x ∂μ))
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.complete_completelyPseudoMetrizableMetric : ∀ (X : Type u_3) [ht : TopologicalSpace X] [h : TopologicalSpace.IsCompletelyPseudoMetrizableSpace X], CompleteSpace X
-- Mathlib.Data.Finset.Sups
Finset.compls_infs : ∀ {α : Type u_2} [inst : BooleanAlgebra α] [inst_1 : DecidableEq α] (s t : Finset α),
  (s ⊼ t).compls = s.compls ⊻ t.compls
-- Mathlib.Order.UpperLower.Closure
mem_upperClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {x : α}, x ∈ upperClosure s ↔ ∃ a ∈ s, a ≤ x
-- Mathlib.Util.Notation3
/-- Matcher that checks that the type of the expression is matched by `matchTy`.  -/
Mathlib.Notation3.matchTypeOf : Mathlib.Notation3.Matcher → Mathlib.Notation3.Matcher
-- Init.Data.Nat.Basic
Nat.lt_succ_iff : ∀ {m n : ℕ}, m < n.succ ↔ m ≤ n
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Arrow.changeProp_obj_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] {P' Q' W' : CategoryTheory.MorphismProperty T}
  [inst_3 : Q'.IsMultiplicative] [inst_4 : W'.IsMultiplicative] (hPP' : P ≤ P') (hQQ' : Q ≤ Q') (hWW' : W ≤ W')
  (Y : P.Arrow Q W), ((CategoryTheory.MorphismProperty.Arrow.changeProp hPP' hQQ' hWW').obj Y).hom = Y.hom
-- Lean.Data.Lsp.Basic
/-- A human-readable string which is rendered less prominent in the user interface.  -/
Lean.Lsp.ChangeAnnotation.description? : Lean.Lsp.ChangeAnnotation → Option String
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instIsScalarTower : ∀ (R : Type u_1) (R' : Type u_2) (A : Type u_3) (E : Type u_4) [inst : SMul R R'] [inst_1 : SMul R E]
  [inst_2 : SMul R' E] [IsScalarTower R R' E], IsScalarTower R R' (WithCStarModule A E)
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.coeFn_holder : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {p q r : ENNReal} [hpqr : p.HolderTriple q r] [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G)
  (f : ↥(MeasureTheory.Lp E p μ)) (g : ↥(MeasureTheory.Lp F q μ)),
  ↑↑(ContinuousLinearMap.holder r B f g) =ᵐ[μ] fun x => (B (↑↑f x)) (↑↑g x)
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
SSet.Truncated.HomotopyCategory₂.mk.injEq : ∀ {A : SSet.Truncated 2}
  (pt pt_1 : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })),
  ({ pt := pt } = { pt := pt_1 }) = (pt = pt_1)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.instLEInftySomeENat : ∀ (n : ℕ∞), ENat.LEInfty ↑n
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCloseds : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T2Space α],
  IsUniformEmbedding TopologicalSpace.NonemptyCompacts.toCloseds
-- Lean.Meta.WHNF
/-- Recall that `_sunfold` auxiliary definitions contains the markers: `markSmartUnfoldingMatch` (*) and `markSmartUnfoldingMatchAlt` (**).
For example, consider the following definition
```
def r (i j : Nat) : Nat :=
  i +
    match j with
    | Nat.zero => 1
    | Nat.succ j =>
      i + match j with
          | Nat.zero => 2
          | Nat.succ j => r i j
```
produces the following `_sunfold` auxiliary definition with the markers
```
def r._sunfold (i j : Nat) : Nat :=
  i +
    (*) match j with
    | Nat.zero => (**) 1
    | Nat.succ j =>
      i + (*) match j with
          | Nat.zero => (**) 2
          | Nat.succ j => (**) r i j
```

`match` expressions marked with `markSmartUnfoldingMatch` (*) must be reduced, otherwise the resulting term is not definitionally
 equal to the given expression. The recursion may be interrupted as soon as the annotation `markSmartUnfoldingAlt` (**) is reached.

For example, the term `r i j.succ.succ` reduces to the definitionally equal term `i + i * r i j`
 -/
Lean.Meta.smartUnfoldingReduce? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac.eq_1 : ∀ (n : ℕ), n.minFac = if 2 ∣ n then 2 else n.minFacAux 3
-- Mathlib.Algebra.Group.Submonoid.Membership
SMulCommClass.of_mclosure_eq_top : ∀ {M : Type u_1} {N : Type u_4} {α : Type u_5} [inst : Monoid M] [inst_1 : SMul N α] [inst_2 : MulAction M α]
  {s : Set M}, Submonoid.closure s = ⊤ → (∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z) → SMulCommClass M N α
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Return the number of arguments that the `Key` takes.  -/
Lean.Meta.RefinedDiscrTree.Key.arity : Lean.Meta.RefinedDiscrTree.Key → ℕ
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findSomeM?.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b))
  (h_2 : (x : Option β) → motive x),
  (match some b with
    | some b => h_1 b
    | x => h_2 x) =
    h_1 b
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.clPrehaar.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] (K₀ : Set G) (V : TopologicalSpace.OpenNhdsOf 1),
  MeasureTheory.Measure.haar.clPrehaar K₀ V =
    closure (MeasureTheory.Measure.haar.prehaar K₀ '' {U | U ⊆ ↑V.toOpens ∧ IsOpen U ∧ 1 ∈ U})
-- Init.Omega.IntList
Lean.Omega.IntList.neg_def : ∀ (xs : Lean.Omega.IntList), -xs = List.map (fun x => -x) xs
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyInfEntourage_le_coverEntropyInf : ∀ {X : Type u_1} {U : SetRel X X} [inst : UniformSpace X] (T : X → X) (F : Set X),
  U ∈ uniformity X → Dynamics.netEntropyInfEntourage T F U ≤ Dynamics.coverEntropyInf T F
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basis_pair_right : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {v : ι → F} {i j : ι},
  i ≠ j → Lagrange.basis {i, j} v j = Lagrange.basisDivisor (v j) (v i)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableLocallyUniformly.summableLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β], SummableLocallyUniformly f → SummableLocallyUniformlyOn f s
-- Mathlib.CategoryTheory.Sites.Whiskering
_private.Mathlib.CategoryTheory.Sites.Whiskering.0.CategoryTheory.GrothendieckTopology.Cover.multicospanComp.match_1.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (S : J.Cover X) (motive : CategoryTheory.Limits.WalkingMulticospan S.shape → Sort u_3) (a : S.shape.L)
  (h_1 : (a : S.shape.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left a))
  (h_2 : (a : S.shape.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right a)),
  (match CategoryTheory.Limits.WalkingMulticospan.left a with
    | CategoryTheory.Limits.WalkingMulticospan.left a => h_1 a
    | CategoryTheory.Limits.WalkingMulticospan.right a => h_2 a) =
    h_1 a
-- Mathlib.Algebra.Order.Floor.Defs
Int.ceil_nonneg : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a : α}, 0 ≤ a → 0 ≤ ⌈a⌉
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- **Alias** of the reverse direction of `OpenPartialHomeomorph.IsImage.iff_preimage_eq'`. -/
OpenPartialHomeomorph.IsImage.of_preimage_eq' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y},
  e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s → e.IsImage s t
-- Mathlib.Order.Category.PartOrdEmb
/-- The order isomorphism corresponding to an isomorphism in `PartOrdEmb`.  -/
PartOrdEmb.orderIsoOfIso : {α β : PartOrdEmb} → (α ≅ β) → ↑α ≃o ↑β
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.toClass_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F],
  WeierstrassCurve.Affine.Point.toClass 0 = 0
-- Lean.Declaration
Lean.instBEqInductiveType.beq : Lean.InductiveType → Lean.InductiveType → Bool
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- A type synonym for the category of paths in a quiver.
 -/
CategoryTheory.Paths : Type u₁ → Type u₁
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp.inj : ∀ {e : Lean.Expr} {isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift}
  {f₁ g₁ f₂ g₂ : Mathlib.Tactic.BicategoryLike.Mor₁} {η θ : Mathlib.Tactic.BicategoryLike.Mor₂} {e_1 : Lean.Expr}
  {isoLift?_1 : Option Mathlib.Tactic.BicategoryLike.IsoLift} {f₁_1 g₁_1 f₂_1 g₂_1 : Mathlib.Tactic.BicategoryLike.Mor₁}
  {η_1 θ_1 : Mathlib.Tactic.BicategoryLike.Mor₂},
  Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp e isoLift? f₁ g₁ f₂ g₂ η θ =
      Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp e_1 isoLift?_1 f₁_1 g₁_1 f₂_1 g₂_1 η_1 θ_1 →
    e = e_1 ∧ isoLift? = isoLift?_1 ∧ f₁ = f₁_1 ∧ g₁ = g₁_1 ∧ f₂ = f₂_1 ∧ g₂ = g₂_1 ∧ η = η_1 ∧ θ = θ_1
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The category of left resolutions of an object in the target category
of a localizer morphism.  -/
CategoryTheory.LocalizerMorphism.LeftResolution : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} → CategoryTheory.LocalizerMorphism W₁ W₂ → C₂ → Type (max u_1 v_2)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.isRatStieltjesPoint_ae : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel ν] (a : α),
      ∀ᵐ (t : β) ∂ν a, ProbabilityTheory.IsRatStieltjesPoint f (a, t)
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.hasDimensionLT_iff_of_iso : ∀ {X Y : SSet} (e : X ≅ Y) (d : ℕ), X.HasDimensionLT d ↔ Y.HasDimensionLT d
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShift.id : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F₁ : CategoryTheory.Functor C D) (A : Type u_5)
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A], CategoryTheory.NatTrans.CommShift (CategoryTheory.CategoryStruct.id F₁) A
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find_eq_iff : ∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] {i : Fin n} (h : ∃ k, p k), Fin.find p h = i ↔ p i ∧ ∀ j < i, ¬p j
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) {Z : CommRingCat}
  (h :
    X.presheaf.obj
        (Opposite.op ((TopologicalSpace.Opens.map f.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f U).inv
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Hom.app f ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)) h) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯).op) h
-- Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular
Matrix.IsTotallyUnimodular.submatrix : ∀ {m : Type u_1} {m' : Type u_2} {n : Type u_3} {n' : Type u_4} {R : Type u_5} [inst : CommRing R] {A : Matrix m n R}
  (f : m' → m) (g : n' → n), A.IsTotallyUnimodular → (A.submatrix f g).IsTotallyUnimodular
-- Mathlib.Data.List.Sigma
List.kerase_of_notMem_keys : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)}, a ∉ l.keys → List.kerase a l = l
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.instLawfulToForwardSearcherModelForallCharBoolDefaultForwardSearcher : ∀ {p : Char → Bool}, String.Slice.Pattern.Model.LawfulToForwardSearcherModel p
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanImportKind.toJson : Lean.Lsp.LeanImportKind → Lean.Json
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- The forget pseudofunctor from `Adj B` to `B`.  -/
CategoryTheory.Bicategory.Adj.forget₁ : {B : Type u} → [inst : CategoryTheory.Bicategory B] → CategoryTheory.Pseudofunctor (CategoryTheory.Bicategory.Adj B) B
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_mapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] {f : β → Std.Iterators.PostconditionT m γ} (it : Std.IterM Id β),
  (Std.IterM.mapWithPostcondition f it).toArray = Array.mapM (fun x => (f x).run) it.toArray.run
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongrRight_apply_snd : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (ab : α₁ × β₁),
  ((Equiv.prodCongrRight e) ab).2 = (e ab.1) ab.2
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.nnnorm_def : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F), ‖f‖₊ = sInf {c | ∀ (x : E), ‖f x‖₊ ≤ c * ‖x‖₊}
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.bicategory_associator_hom_unop2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : Bᵒᵖ} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  (CategoryTheory.Bicategory.associator f g h).hom.unop2 =
    (CategoryTheory.Bicategory.associator h.unop g.unop f.unop).inv
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_le_hausdorffEDist_of_mem`.

---

The distance to a set is controlled by the Hausdorff distance.  -/
EMetric.infEdist_le_hausdorffEdist_of_mem : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α},
  x ∈ s → Metric.infEDist x t ≤ Metric.hausdorffEDist s t
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.lintegral_eq_of_tendsto : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} [l.NeBot]
  [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → ENNReal} (I : ENNReal),
      AEMeasurable f μ → Filter.Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (nhds I) → ∫⁻ (x : α), f x ∂μ = I
-- Lean.Meta.Tactic.Simp.Types
/-- When processing `Simp` arguments, `zetaDelta` may be performed if `zetaDeltaSet` is not empty.
We save the local free variable ids in `initUsedZetaDelta`. `initUsedZetaDelta` is a subset of `zetaDeltaSet`.  -/
Lean.Meta.Simp.Context.initUsedZetaDelta : Lean.Meta.Simp.Context → Lean.FVarIdSet
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.RingEquiv.nontrivial_heightOneSpectrum : ∀ {R : Type u_5} {S : Type u_6} [inst : CommRing R] [inst_1 : CommRing S]
  [Nontrivial (IsDedekindDomain.HeightOneSpectrum S)] (e : R ≃+* S), Nontrivial (IsDedekindDomain.HeightOneSpectrum R)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.RatCoeff.mk.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {e : Q(«$α»)} {value : ℚ} {hyp : Option Lean.Expr} {value_1 : ℚ}
  {hyp_1 : Option Lean.Expr},
  { value := value, hyp := hyp } = { value := value_1, hyp := hyp_1 } → value = value_1 ∧ hyp = hyp_1
-- Batteries.Data.List.Basic
List.fillNones.eq_1 : ∀ {α : Type u_1} (x : List α), [].fillNones x = []
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.liftLinear.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β]
  (f f_1 : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β) (e_f : f = f_1)
  (hf : ∀ (μ : MeasureTheory.Measure α), inst ≤ (f μ.toOuterMeasure).caratheodory),
  MeasureTheory.Measure.liftLinear f hf = MeasureTheory.Measure.liftLinear f_1 ⋯