mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
/-- The `reduce` function takes in a clause `c` and takes in an array of assignments and attempts to
eliminate every literal in the clause that is not compatible with the `assignments` argument.
- If `reduce` returns `encounteredBoth`, then this means that the `assignments` array has a `both`
  Assignment and is therefore fundamentally unsatisfiable.
- If `reduce` returns `reducedToEmpty`, then this means that every literal in `c` is incompatible
  with `assignments`. In other words, this means that the conjunction of `assignments` and `c` is
  unsatisfiable.
- If `reduce` returns `reducedToUnit l`, then this means that every literal in `c` is incompatible
  with `assignments` except for `l`. In other words, this means that the conjunction of
  `assignments` and `c` entail `l`.
- If `reduce` returns `reducedToNonunit`, then this means that there are multiple literals in `c`
  that are compatible with `assignments`. This is a failure condition for `confirmRupHint`
  (in `LRAT.Formula.Implementation.lean`) which calls `reduce`.  -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n →
    Array Std.Tactic.BVDecide.LRAT.Internal.Assignment →
      Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
-- Lean.Elab.DeprecatedSyntax
Lean.Elab.deprecatedSyntaxExt : Lean.SimplePersistentEnvExtension Lean.Elab.SyntaxDeprecationEntry (Lean.NameMap Lean.Elab.SyntaxDeprecationEntry)
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
/-- A morphism of spans is a morphism between the apices compatible
with the projections.  -/
CategoryTheory.Span.Hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} →
      {c c' : C} → CategoryTheory.Span Wₗ Wᵣ c c' → CategoryTheory.Span Wₗ Wᵣ c c' → Type v_1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_eq_getD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  {fallback : β a} {h : a ∈ m}, m.get a h = m.getD a fallback
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
/-- Given a measure `μ`, signed measures `s` and `t`, and a function `f` such that `t` is
mutually singular with respect to `μ` and `s = t + μ.withDensityᵥ f`, we have
`t = singularPart s μ`, i.e. `t` is the singular part of the Lebesgue decomposition between
`s` and `μ`.  -/
MeasureTheory.SignedMeasure.eq_singularPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : MeasureTheory.SignedMeasure α}
  (t : MeasureTheory.SignedMeasure α) (f : α → ℝ),
  MeasureTheory.VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure →
    s = t + μ.withDensityᵥ f → t = s.singularPart μ
-- Lean.Syntax
/-- Return kind of parser expected at this antiquotation, and whether it is a "pseudo" kind (see `mkAntiquot`).  -/
Lean.Syntax.antiquotKind? : Lean.Syntax → Option (Lean.SyntaxNodeKind × Bool)
-- Mathlib.Algebra.BigOperators.Group.Finset.Interval
Finset.sum_Ico_int_sub : ∀ (b : ℕ) {α : Type u_1} [inst : AddCommGroup α] (f : ℤ → α),
  ∑ n ∈ Finset.Ico (-↑b) ↑b, (f n - f (n + 1)) = f (-↑b) - f ↑b
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.lintegral_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : β → γ} (κ : ProbabilityTheory.Kernel α β),
  Measurable f → ∀ (a : α) {g' : γ → ENNReal}, Measurable g' → ∫⁻ (b : γ), g' b ∂(κ.map f) a = ∫⁻ (a : β), g' (f a) ∂κ a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.instPreservesColimitsOfSize : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {C' : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v',
        max (max (u + 1) u₁) v₁}
      F],
  CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, max u u', max u u₁, max (max (u + 1) u') v',
      max (max (u + 1) u₁) v₁}
    F
-- Mathlib.Topology.Order.OrderClosed
PredOrder.nhdsLE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {b : α} [PredOrder α],
  nhdsWithin b (Set.Iic b) = pure b
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instModuleQuotientIdealHSMulTopSubmodule : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) → {M : Type u_3} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module (R ⧸ I • ⊤) (M ⧸ I • ⊤)
-- Mathlib.Algebra.Order.Star.Basic
IsStarProjection.le_one : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {p : R},
  IsStarProjection p → p ≤ 1
-- Init.Data.String.Lemmas.Basic
String.Slice.pos!.eq_1 : ∀ (s : String.Slice) (off : String.Pos.Raw),
  s.pos! off =
    if h : String.Pos.Raw.isValidForSlice s off = true then s.pos off ⋯
    else
      panicWithPosWithDecl "Init.Data.String.Basic" "String.Slice.pos!" 1661 4
        "Offset is not at a valid UTF-8 character boundary"
-- Mathlib.LinearAlgebra.RootSystem.OfBilinear
LinearMap.IsReflective.dvd_two_mul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {B : M →ₗ[R] M →ₗ[R] R} {x : M}, B.IsReflective x → ∀ (y : M), (B x) x ∣ 2 * (B x) y
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.Embedding.age_subset_age : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {N : Type w} [inst_1 : L.Structure N]
  (MN : L.Embedding M N), L.age M ⊆ L.age N
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Rat.HeightOneSpectrum.natGenerator_dvd_iff : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  (v : IsDedekindDomain.HeightOneSpectrum R) {n : ℕ},
  Rat.HeightOneSpectrum.natGenerator v ∣ n ↔ ↑n ∈ Ideal.map (Rat.IsIntegralClosure.intEquiv R) v.asIdeal
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.valueMonoid.eq_1 : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : MonoidWithZero B] (f : A →*₀ B),
  f.valueMonoid = { carrier := Units.val ⁻¹' Set.range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_inverse_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max w v)))
  {X Y : CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{w, v, u} F} (f : X ⟶ Y),
  (CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence F).inverse.map f =
    (CategoryTheory.CategoryOfElements.homMk (F.elementsMk (Opposite.op Y.left) (CategoryTheory.uliftYonedaEquiv Y.hom))
        (F.elementsMk (Opposite.op X.left) (CategoryTheory.uliftYonedaEquiv X.hom)) f.left.op ⋯).op
-- Mathlib.Data.Set.Lattice
Set.compl_iUnion : ∀ {β : Type u_2} {ι : Sort u_5} (s : ι → Set β), (⋃ i, s i)ᶜ = ⋂ i, (s i)ᶜ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsGreatest.norm_cfcₙ : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A),
  autoParam (ContinuousOn f (quasispectrum 𝕜 a)) IsGreatest.norm_cfcₙ._auto_1 →
    autoParam (f 0 = 0) IsGreatest.norm_cfcₙ._auto_3 →
      autoParam (p a) IsGreatest.norm_cfcₙ._auto_5 → IsGreatest ((fun x => ‖f x‖) '' quasispectrum 𝕜 a) ‖cfcₙ f a‖
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.unop_toSubmonoid : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup Gᵐᵒᵖ), H.unop.toSubmonoid = H.unop
-- Mathlib.RingTheory.WittVector.Compare
/-- The following diagram commutes:
```text
          ZMod (p^n) ----------------------------> ZMod (p^m)
            |                                        |
            |                                        |
            v                                        v
TruncatedWittVector p n (ZMod p) ----> TruncatedWittVector p m (ZMod p)
```
Here the vertical arrows are `TruncatedWittVector.zmodEquivTrunc`,
the horizontal arrow at the top is `ZMod.castHom`,
and the horizontal arrow at the bottom is `TruncatedWittVector.truncate`.
 -/
TruncatedWittVector.commutes : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m),
  (TruncatedWittVector.truncate hm).comp (TruncatedWittVector.zmodEquivTrunc p m).toRingHom =
    (TruncatedWittVector.zmodEquivTrunc p n).toRingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ n)))
-- Init.Prelude
/-- Returns the greater of its two arguments. 

Conventions for notations in identifiers:

 * The recommended spelling of `max` in identifiers is `max`.

 * The recommended spelling of `⊔` in identifiers is `sup` (`⊔` is the preferred notation for `max` when the type is not linearly ordered.). -/
Max.max : {α : Type u} → [self : Max α] → α → α → α
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.UnpackedFloat.finite.sizeOf_spec : ∀ (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (exponent : ℤ) (mantissa_pos : 0 < mantissa),
  sizeOf (Float.Model.UnpackedFloat.finite sign mantissa exponent mantissa_pos) =
    1 + sizeOf sign + sizeOf mantissa + sizeOf exponent + sizeOf mantissa_pos
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.complete : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], CauSeq.IsComplete ℚ_[p] norm
-- Mathlib.Algebra.Group.Action.Basic
smul_eq_iff_eq_invOf_smul : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : MulAction α β] {c : α} {x y : β} [inst_2 : Invertible c],
  c • x = y ↔ x = ⅟c • y
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.πJ.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (s : Finset I),
  Profinite.NobelingProof.πJ C s =
    LocallyConstant.comapₗ ℤ { toFun := Profinite.NobelingProof.ProjRestrict C fun x => x ∈ s, continuous_toFun := ⋯ }
-- Init.Data.SInt.Lemmas
ISize.add_neg_eq_sub : ∀ {a b : ISize}, a + -b = a - b
-- Mathlib.Algebra.Group.MinimalAxioms
/-- Define a `Group` structure on a Type by proving `∀ a, 1 * a = a` and
`∀ a, a⁻¹ * a = 1`.
Note that this uses the default definitions for `npow`, `zpow` and `div`.
See note [reducible non-instances].  -/
Group.ofLeftAxioms : {G : Type u} →
  [inst : Mul G] →
    [inst_1 : Inv G] →
      [inst_2 : One G] →
        (∀ (a b c : G), a * b * c = a * (b * c)) → (∀ (a : G), 1 * a = a) → (∀ (a : G), a⁻¹ * a = 1) → Group G
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet`.

---

Given a predicate `P : Set J.obj → Prop` on the underlying type
of `J : CardinalDirectedPoset κ` such that all the subsets satisfying `P`
are `κ`-filtered, this is the cocone with point `J` given
by all the inclusions of the subsets satisfying `P`.  -/
CategoryTheory.CardinalFilteredPoset.coconeOfPredicateSet : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    {J : CategoryTheory.CardinalDirectedPoset κ} →
      (P : Set ↑J.obj → Prop) →
        [inst_1 : ∀ (S : Subtype P), CategoryTheory.IsCardinalFiltered (↑↑S) κ] →
          CategoryTheory.Limits.Cocone (CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet P)
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.leftRel_eq : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), ⇑(QuotientGroup.leftRel s) = fun x y => x⁻¹ * y ∈ s
-- Init.Data.SInt.Lemmas
Int64.toUInt64_ofBitVec : ∀ (b : BitVec 64), (Int64.ofBitVec b).toUInt64 = { toBitVec := b }
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstMulNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
ConvexOn.map_condExp_rnDeriv_le : ∀ {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ} (hm : m ≤ m𝓧),
  MeasureTheory.StronglyMeasurable f →
    ConvexOn ℝ (Set.Ici 0) f →
      ContinuousWithinAt f (Set.Ici 0) 0 →
        MeasureTheory.Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν →
          (fun x => f (ν[fun x => (μ.rnDeriv ν x).toReal | m] x)) ≤ᵐ[ν.trim hm] ν[fun x => f (μ.rnDeriv ν x).toReal | m]
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atTop_mul_const_right : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] (l : Filter α)
  {f : α → G} (C : G), Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x * C) l Filter.atTop
-- Init.Data.BitVec.Bitblast
BitVec.toInt_srem : ∀ {w : ℕ} (x y : BitVec w), (x.srem y).toInt = x.toInt.tmod y.toInt
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanILeanHeaderSetupInfoParams.mk.injEq : ∀ (version : ℕ) (isSetupFailure : Bool) (directImports : Array Lean.Lsp.ImportInfo) (version_1 : ℕ)
  (isSetupFailure_1 : Bool) (directImports_1 : Array Lean.Lsp.ImportInfo),
  ({ version := version, isSetupFailure := isSetupFailure, directImports := directImports } =
      { version := version_1, isSetupFailure := isSetupFailure_1, directImports := directImports_1 }) =
    (version = version_1 ∧ isSetupFailure = isSetupFailure_1 ∧ directImports = directImports_1)
-- Init.Data.Option.List
Option.length_toList_le : ∀ {α : Type u_1} {o : Option α}, o.toList.length ≤ 1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The fork defined in `BinaryBicone.sndKernelFork` is indeed a kernel.  -/
CategoryTheory.Limits.BinaryBicone.isLimitSndKernelFork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {c : CategoryTheory.Limits.BinaryBicone X Y} →
          CategoryTheory.Limits.IsLimit c.toCone → CategoryTheory.Limits.IsLimit c.sndKernelFork
-- Mathlib.Data.Num.Basic
/-- Returns a Boolean for whether the `PosNum` is `one`.  -/
PosNum.isOne : PosNum → Bool
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgHom.subsingleton : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B] [inst_7 : StarRing R]
  [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] [Subsingleton (NonUnitalStarSubalgebra R A)],
  Subsingleton (A →⋆ₙₐ[R] B)
-- Mathlib.Data.Set.Lattice
Set.biInter_gt_eq_iInf : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [NoMinOrder α] {s : α → Set β}, ⋂ n, ⋂ m, ⋂ (_ : m > n), s m = ⋂ n, s n
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.iInf_rat_gt_defaultRatCDF : ∀ (t : ℚ), ⨅ r, ProbabilityTheory.defaultRatCDF ↑r = ProbabilityTheory.defaultRatCDF t
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.tendsto_concat : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b c : α}
  [inst_3 : Fact (a ≤ b)] [inst_4 : Fact (b ≤ c)] {E : Type u_2} [inst_5 : TopologicalSpace E]
  {f : C(↑(Set.Icc a b), E)} {g : C(↑(Set.Icc b c), E)} {ι : Type u_3} {p : Filter ι} {F : ι → C(↑(Set.Icc a b), E)}
  {G : ι → C(↑(Set.Icc b c), E)},
  (∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥) →
    f ⊤ = g ⊥ →
      Filter.Tendsto F p (nhds f) →
        Filter.Tendsto G p (nhds g) → Filter.Tendsto (fun i => (F i).concat (G i)) p (nhds (f.concat g))
-- Batteries.Tactic.GeneralizeProofs
/-- The local fvars corresponding to bound variables.
Abstraction needs to be sure that these variables do not appear in abstracted terms.  -/
Batteries.Tactic.GeneralizeProofs.AContext.fvars : Batteries.Tactic.GeneralizeProofs.AContext → Array Lean.Expr
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation_ge_three_one : ∀ (n k : ℕ), hyperoperation (n + 3) 1 k = 1
-- Lean.Elab.Match
Lean.Elab.Term.PatternElabException.mk : Lean.Exception → ℕ → List ℕ → Lean.Elab.Term.PatternElabException
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.D₁.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
  [inst_20 : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] (j j' : ι₄),
  HomologicalComplex.mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' =
    HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc fun i₁ i₂ i₃ x =>
      HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
-- Mathlib.RingTheory.Ideal.Over
/-- An `A ⧸ p`-algebra isomorphism between `B ⧸ P` and `C ⧸ Q` induced by an `A`-algebra
isomorphism between `B` and `C`, where `Q = σ P`.  -/
Ideal.Quotient.algEquivOfEqMap : {A : Type u_3} →
  {B : Type u_4} →
    {C : Type u_5} →
      [inst : CommRing A] →
        [inst_1 : CommRing B] →
          [inst_2 : CommRing C] →
            [inst_3 : Algebra A B] →
              [inst_4 : Algebra A C] →
                {P : Ideal B} →
                  {Q : Ideal C} →
                    (p : Ideal A) →
                      [inst_5 : Q.LiesOver p] →
                        [inst_6 : P.LiesOver p] →
                          {E : Type u_7} →
                            [inst_7 : EquivLike E B C] →
                              [AlgEquivClass E A B C] → (σ : E) → Q = Ideal.map σ P → (B ⧸ P) ≃ₐ[A ⧸ p] C ⧸ Q
-- Mathlib.MeasureTheory.Function.EssSup
essInf_eq_iInf : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : CompleteLattice β],
  (∀ (a : α), μ {a} ≠ 0) → ∀ (f : α → β), essInf f μ = ⨅ i, f i
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.ext : ∀ {E : Type u_3} [inst : AddGroup E] {p q : AddGroupNorm E}, (∀ (x : E), p x = q x) → p = q
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.isIso_toLimit : ∀ (P : ProfiniteGrp.{u}), CategoryTheory.IsIso P.toLimit
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- The trivial monoid algebra is isomorphic to the base ring.  -/
MonoidAlgebra.bialgEquivOfSubsingleton : {R : Type u_1} →
  (M : Type u_8) → [inst : CommSemiring R] → [inst_1 : Monoid M] → [Subsingleton M] → MonoidAlgebra R M ≃ₐc[R] R
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.liftHom.eq_3 : ∀ {B : Type u₁} [inst : Quiver B] {C : Type u₂} [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} C] (F : B ⥤q C)
  (x x_1 : CategoryTheory.FreeBicategory B) (b : B) (f : CategoryTheory.FreeBicategory.Hom x b)
  (g : CategoryTheory.FreeBicategory.Hom b x_1),
  CategoryTheory.FreeBicategory.liftHom F (f.comp g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.liftHom F f)
      (CategoryTheory.FreeBicategory.liftHom F g)
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.toLoop_apply_coe : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  (p : ↑(GenLoop N X x)) (t : ↑unitInterval), ↑((GenLoop.toLoop i p) t) = ((↑p).comp ↑(Cube.insertAt i)).curry t
-- Mathlib.Order.Sublattice
Sublattice.coe_eq_univ : ∀ {α : Type u_2} [inst : Lattice α] {L : Sublattice α}, ↑L = Set.univ ↔ L = ⊤
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.State.mk.sizeOf_spec : ∀ (annotations : Lean.PrettyPrinter.Delaborator.OptionsPerPos) (postponed : Array (Lean.Expr × Lean.Expr)),
  sizeOf { annotations := annotations, postponed := postponed } = 1 + sizeOf annotations + sizeOf postponed
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr : ∀ {a b c : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x : a ⟶ b) (x_1 : b ⟶ c),
  (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x x_1).hom.τr =
    CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardComp x_1.as.unop x.as.unop).hom
-- Init.Data.List.Basic
List.isEqv_cons_cons : ∀ {α : Type u_1} {a : α} {as : List α} {b : α} {bs : List α} {eqv : α → α → Bool},
  (a :: as).isEqv (b :: bs) eqv = (eqv a b && as.isEqv bs eqv)
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- `filter` preserves well-formedness. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.filter : ∀ {α : Type u} [inst : Ord α] {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced}
  {f : (a : α) → x a → Bool}, t.WF → (Std.DTreeMap.Internal.Impl.filter f t h).impl.WF
-- Mathlib.Tactic.Explode
/-- Prepend the `line` of the `Entry` to `deps` if it's not `none`, but if the entry isn't marked
with `useAsDep` then it's not added to the list at all.  -/
_private.Mathlib.Tactic.Explode.0.Mathlib.Explode.explodeCore.consDep : Bool → Option Mathlib.Explode.Entry → List (Option ℕ) → List (Option ℕ)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.euclidean.integerLattice.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.euclidean.integerLattice K = NumberField.mixedEmbedding.euclidean.integerLattice K
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instInvOneClass.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : InvOneClass G],
  Filter.Germ.instInvOneClass = { toOne := Filter.Germ.instOne, toInv := Filter.Germ.instInv, inv_one := ⋯ }
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.isWeaklyRegular_append_iff : ∀ {R : Type u_1} (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (rs₁ rs₂ : List R),
  RingTheory.Sequence.IsWeaklyRegular M (rs₁ ++ rs₂) ↔
    RingTheory.Sequence.IsWeaklyRegular M rs₁ ∧ RingTheory.Sequence.IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
-- Mathlib.NumberTheory.Modular
/-- Given `z : ℍ` and a bottom row `(c,d)`, among the `g : SL(2,ℤ)` with this bottom row, minimize
`|(g•z).re|`.  -/
ModularGroup.exists_row_one_eq_and_min_re : ∀ (z : UpperHalfPlane) {cd : Fin 2 → ℤ},
  IsCoprime (cd 0) (cd 1) →
    ∃ g, ↑g 1 = cd ∧ ∀ (g' : Matrix.SpecialLinearGroup (Fin 2) ℤ), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
-- Mathlib.Topology.UniformSpace.Closeds
/-- In the Hausdorff uniformity, the powerset of a closed set is closed.  -/
IsClosed.powerset_hausdorff : ∀ {α : Type u_1} [inst : UniformSpace α] {F : Set α}, IsClosed F → IsClosed (𝒫 F)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.ext_iff : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] {f g : R ≃+* S},
  f = g ↔ ∀ (x : R), f x = g x
-- Init.Data.List.Nat.Modify
List.exists_of_modifyTailIdx : ∀ {α : Type u_1} (f : List α → List α) {i : ℕ} {l : List α},
  i ≤ l.length → ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = i ∧ l.modifyTailIdx i f = l₁ ++ f l₂
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instDFunLike : {ι : Type u_1} →
  (R : ι → Type u_2) →
    (A : (i : ι) → Set (R i)) → {𝓕 : Filter ι} → DFunLike (RestrictedProduct (fun i => R i) (fun i => A i) 𝓕) ι R