mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.free.generatingSections_s : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] (I : Type u) (i : I),
  (SheafOfModules.free.generatingSections I).s i = SheafOfModules.freeSection i
-- Mathlib.Analysis.Convex.Gauge
gaugeSeminorm_toFun : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : RCLike 𝕜]
  [inst_3 : Module 𝕜 E] [inst_4 : IsScalarTower ℝ 𝕜 E] (hs₀ : Balanced 𝕜 s) (hs₁ : Convex ℝ s) (hs₂ : Absorbent ℝ s)
  (x : E), (gaugeSeminorm hs₀ hs₁ hs₂) x = gauge s x
-- Mathlib.SetTheory.ZFC.Class
/-- The definite description operator, which is `{x}` if `{y | A y} = {x}` and `∅` otherwise.  -/
Class.iota : Class.{u_1} → Class.{u_1}
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- An intermediate field inherits a field structure.  -/
IntermediateField.toField : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → (S : IntermediateField K L) → Field ↥S
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.zsmul_vadd_eq_iff_minimalPeriod_dvd : ∀ {α : Type v} {G : Type u} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} {b : α} {n : ℤ},
  n • a +ᵥ b = b ↔ ↑(Function.minimalPeriod (fun x => a +ᵥ x) b) ∣ n
-- Mathlib.Order.OrdContinuous
/-- A function `f` between preorders is left order continuous if it preserves all suprema of
nonempty sets. We define it using `IsLUB` instead of `sSup` so that the proof works both for
complete lattices and conditionally complete lattices.  -/
LeftOrdContinuous : {α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → Prop
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
LeftPreLieAlgebra.mk : {R : Type u_1} →
  [inst : CommRing R] →
    {L : Type u_2} →
      [inst_1 : LeftPreLieRing L] →
        [toModule : Module R L] →
          [toIsScalarTower : IsScalarTower R L L] → [toSMulCommClass : SMulCommClass R L L] → LeftPreLieAlgebra R L
-- Mathlib.ModelTheory.Order
FirstOrder.Language.model_linearOrder : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : LinearOrder M]
  [L.OrderedStructure M], M ⊨ L.linearOrderTheory
-- Mathlib.MeasureTheory.Measure.Prod
/-- **Tonelli's Theorem for set integrals**: For `ℝ≥0∞`-valued almost everywhere measurable
functions on `s ×ˢ t`, the integral of `f` on `s ×ˢ t` is equal to the iterated integral on `s`
and `t` respectively.  -/
MeasureTheory.setLIntegral_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set α} {t : Set β}
  (f : α × β → ENNReal),
  AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t)) →
    ∫⁻ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- A total complex shape for three complex shapes `c₁`, `c₂`, `c₁₂` on three types
`I₁`, `I₂` and `I₁₂` consists of the data and properties that will allow the construction
of a total complex functor `HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex C c₁₂` which
sends `K` to a complex which in degree `i₁₂ : I₁₂` consists of the coproduct
of the `(K.X i₁).X i₂` such that `π ⟨i₁, i₂⟩ = i₁₂`.  -/
TotalComplexShape : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} → ComplexShape I₁ → ComplexShape I₂ → ComplexShape I₁₂ → Type (max (max u_1 u_2) u_4)
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.Iso.mk_hom : ∀ {α β : AlexDisc} (e : ↑α.toTopCat ≃ₜ ↑β.toTopCat), (AlexDisc.Iso.mk e).hom = CategoryTheory.ConcreteCategory.ofHom ↑e
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_strictMap_inverseImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty D) (F : CategoryTheory.Functor C D),
  ((P.inverseImage F).strictMap F).inverseImage F = P.inverseImage F
-- Init.Control.Lawful.MonadAttach.Lemmas
LawfulMonadAttach.canReturn_bind_imp' : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} {b : β} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m]
  [LawfulMonadAttach m] {x : m α} {f : α → m β},
  MonadAttach.CanReturn (x >>= f) b → ∃ a, MonadAttach.CanReturn x a ∧ MonadAttach.CanReturn (f a) b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_of_mem_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  k ∈ t.insertMany l → (List.map Sigma.fst l).contains k = false → k ∈ t
-- Init.MetaTypes
/-- When `true` (default: `true`), performs beta reduction of applications of `fun` expressions.
That is, `(fun x => e[x]) v` reduces to `e[v]`.
 -/
Lean.Meta.DSimp.Config.beta : Lean.Meta.DSimp.Config → Bool
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.instReprGuessLexRel.repr : Lean.Elab.WF.GuessLex.GuessLexRel → ℕ → Std.Format
-- Mathlib.Algebra.Ring.Ext
Distrib.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : Distrib R⦄, HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- Two descents of the same morphism are homotopic.  -/
CategoryTheory.InjectiveResolution.descHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        (f : Y ⟶ Z) →
          {I : CategoryTheory.InjectiveResolution Y} →
            {J : CategoryTheory.InjectiveResolution Z} →
              (g h : I.cocomplex ⟶ J.cocomplex) →
                CategoryTheory.CategoryStruct.comp I.ι g =
                    CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) J.ι →
                  CategoryTheory.CategoryStruct.comp I.ι h =
                      CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) J.ι →
                    Homotopy g h
-- Aesop.Options.Public
/-- (aesop) Collect statistics about Aesop invocations.
 -/
Aesop.aesop.collectStats : Lean.Option Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {v : β}, Std.ExtDTreeMap.Const.get (t.insert k v) k ⋯ = v
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roc.forIn'_eq_match.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : none = none → motive none)
  (h_2 : (next : α) → none = some next → motive (some next)),
  (match hs : none with
    | none => h_1 hs
    | some next => h_2 next hs) =
    h_1 ⋯
-- Mathlib.Topology.Connected.Basic
instConnectedSpaceProd : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [ConnectedSpace α]
  [ConnectedSpace β], ConnectedSpace (α × β)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.adjoin.congr_simp : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (s s_1 : Set A),
  s = s_1 → NonUnitalStarAlgebra.adjoin R s = NonUnitalStarAlgebra.adjoin R s_1
-- Init.Data.Nat.Lemmas
Nat.pred_max_pred : ∀ (x y : ℕ), max x.pred y.pred = (max x y).pred
-- Lean.Meta.Tactic.Grind.EMatch
/-- Choices that still have to be processed.  -/
Lean.Meta.Grind.EMatch.SearchState.choiceStack : Lean.Meta.Grind.EMatch.SearchState → List Lean.Meta.Grind.EMatch.Choice
-- Init.Data.Int.Linear
Int.Internal.Linear.mod_eq : ∀ (a b k : ℤ), b = k → a % b = a % k
-- Aesop.Tracing
Aesop.ruleErrorEmoji : String
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opInverse_map : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {X Y : HomologicalComplex Vᵒᵖ c.symm} (f : X ⟶ Y),
  (HomologicalComplex.opInverse V c).map f = Quiver.Hom.op { f := fun i => (f.f i).unop, comm' := ⋯ }
-- Mathlib.Geometry.RingedSpace.SheafedSpace
CategoryTheory.Functor.comp.eq_1 : ∀ {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] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E),
  F.comp G = { obj := fun X => G.obj (F.obj X), map := fun {X Y} f => G.map (F.map f), map_id := ⋯, map_comp := ⋯ }
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.reindex_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.LimitPresentation J X) {J' : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J'] (F : CategoryTheory.Functor J' J) [inst_3 : F.Initial],
  (P.reindex F).π = F.whiskerLeft P.π
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.findSome?.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive x
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_app_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseRightKanExtension F L]
  [inst_5 : L.HasPointwiseRightKanExtension F] (a : A) {Z : D} (h : G.obj (F.obj a) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a))
      (CategoryTheory.CategoryStruct.comp ((L.pointwiseRightKanExtensionCounit (F.comp G)).app a) h) =
    CategoryTheory.CategoryStruct.comp (G.map ((L.pointwiseRightKanExtensionCounit F).app a)) h
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
/-- Expansion of `log (1 + a⁻¹)` as a series in powers of `1 / (2 * a + 1)`.  -/
Real.hasSum_log_one_add_inv : ∀ {a : ℝ}, 0 < a → HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (Real.log (1 + a⁻¹))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The discriminant `Δ'` of an elliptic curve is equal to the
discriminant `Δ` of it as a Weierstrass curve.  -/
WeierstrassCurve.coe_Δ' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic], ↑W.Δ' = W.Δ
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_interSmallerFn : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] (l sofar : List ((a : α) × β a)) (k k' : α),
  Std.Internal.List.getEntry? k' (Std.Internal.List.interSmallerFn l sofar k) =
    (Option.filter (fun kv => k == kv.fst) (Std.Internal.List.getEntry? k' l)).or (Std.Internal.List.getEntry? k' sofar)
-- Mathlib.Topology.Defs.Basic
/-- The frontier of a set is the set of points between the closure and interior.  -/
frontier : {X : Type u} → [TopologicalSpace X] → Set X → Set X
-- Mathlib.Logic.Embedding.Set
Function.Embedding.optionEmbeddingEquiv_symm_apply : ∀ (α : Type u_1) (β : Type u_2) (f : (f : α ↪ β) × ↑(Set.range ⇑f)ᶜ),
  (Function.Embedding.optionEmbeddingEquiv α β).symm f = f.fst.optionElim ↑f.snd ⋯
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `{ n_i }` is an `R`-basis of `N`, which is also `M`-linearly independent
(in this result it is stated as `Submodule.mulRightMap` is injective),
then `M` and `N` are linearly disjoint.  -/
Submodule.LinearDisjoint.of_basis_right' : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S)
  {ι : Type u_1} (n : Module.Basis ι R ↥N), Function.Injective ⇑(M.mulRightMap ⇑n) → M.LinearDisjoint N
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- The prime spectrum of the localization of a commutative ring R at a prime ideal I are in
order-preserving bijection with the interval $(-∞, I]$ in the prime spectrum of R.  -/
IsLocalization.AtPrime.primeSpectrumOrderIso : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (I : Ideal R) →
            [hI : I.IsPrime] →
              [IsLocalization.AtPrime S I] → PrimeSpectrum S ≃o ↑(Set.Iic { asIdeal := I, isPrime := hI })
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat),
  Topology.IsClosedEmbedding ⇑(CategoryTheory.PreGaloisCategory.autEmbedding F)
-- Mathlib.RingTheory.GradedAlgebra.Basic
/-- If `A` is graded by `ι` with degree `i` component `𝒜 i`, then it is isomorphic as
a ring to a direct sum of components.  -/
DirectSum.decomposeRingEquiv : {ι : Type u_1} →
  {A : Type u_3} →
    {σ : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : Semiring A] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] →
                (𝒜 : ι → σ) → [inst_5 : GradedRing 𝒜] → A ≃+* DirectSum ι fun i => ↥(𝒜 i)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.weierstrassPExcept_add_coe_aux : ∀ (L : PeriodPair),
  ∀ l₀ ∈ L.lattice,
    ∀ (l : ↥L.lattice),
      ↑l / 2 ∉ L.lattice →
        Set.EqOn (fun x => L.weierstrassPExcept l₀ (x + ↑l))
          (fun x => L.weierstrassPExcept (l₀ - ↑l) x + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)) (↑L.lattice \ {l₀ - ↑l})ᶜ
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.equiv'_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (g : Polynomial R)
  (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0)
  (h₂ : (Polynomial.aeval pb.gen) g = 0), ⇑(AdjoinRoot.equiv' g pb h₁ h₂).symm = ⇑(pb.lift (AdjoinRoot.root g) h₁)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_eq_head_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.minKey he = t.keys.head ⋯
-- Init.PropLemmas
exists_or_eq_left : ∀ {α : Sort u_1} (y : α) (p : α → Prop), ∃ x, x = y ∨ p x
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.mkHeader : Lean.Name → ℕ → Lean.InductiveVal → Lean.Elab.TermElabM Lean.Elab.Deriving.Header
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.curryFinFinset_symm_apply_piecewise_const : ∀ {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [inst : CommSemiring R] [inst_1 : AddCommMonoid M']
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M'] [inst_4 : Module R M₂] {k l n : ℕ} {s : Finset (Fin n)}
  (hk : s.card = k) (hl : sᶜ.card = l) (f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂))
  (x y : M'),
  ((MultilinearMap.curryFinFinset R M₂ M' hk hl).symm f) (s.piecewise (fun x_1 => x) fun x => y) =
    (f fun x_1 => x) fun x => y
-- Mathlib.Topology.Order.LeftRightNhds
nhdsLT_basis_of_exists_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α},
  (∃ b, b < a) → (nhdsWithin a (Set.Iio a)).HasBasis (fun x => x < a) fun x => Set.Ioo x a
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- Given a monomorphism `f : K ⟶ L` between complexes that are strictly `≥ n₀ + 1`,
this is a projective system in `CochainComplex C ℤ`, whose limit shall give
the intermediate object in the factorization lemma `cm5a_cof`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cochainComplexFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (f : K ⟶ L) →
          [CategoryTheory.EnoughInjectives C] →
            [CategoryTheory.Mono f] →
              (n₀ : ℤ) →
                [K.IsStrictlyGE (n₀ + 1)] → [L.IsStrictlyGE (n₀ + 1)] → CategoryTheory.Functor ℕᵒᵖ (CochainComplex C ℤ)
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.map₂HomologicalComplex_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.PreservesZeroMorphisms] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c : ComplexShape J)
  [inst_8 : DecidableEq J] [inst_9 : TotalComplexShape c₁ c₂ c]
  [inst_10 : ∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂), K₁.HasMapBifunctor K₂ F c]
  {X Y : HomologicalComplex C₁ c₁} (f : X ⟶ Y) (K₂ : HomologicalComplex C₂ c₂),
  ((F.map₂HomologicalComplex c₁ c₂ c).map f).app K₂ =
    HomologicalComplex.mapBifunctorMap f (CategoryTheory.CategoryStruct.id K₂) F c
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.cone_π_app : ∀ (P : ProfiniteGrp.{u}) (U : OpenNormalSubgroup ↑P.toProfinite.toTop), P.cone.π.app U = ProfiniteGrp.proj U
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.coeff_eval_eq_eval_coeff : ∀ {R : Type u} (S₁ : Type v) [inst : CommSemiring R] (s' : S₁ → R) (f : Polynomial (MvPolynomial S₁ R)) (i : ℕ),
  (Polynomial.map (MvPolynomial.eval s') f).coeff i = (MvPolynomial.eval s') (f.coeff i)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback.diagonal_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f)
      (CategoryTheory.Limits.pullback.snd f f) =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrLeft'_apply : ∀ {α : Sort u_1} {β : Sort u_4} (P : α → Sort u_9) (e : α ≃ β) (f : (a : α) → P a) (x : β),
  (Equiv.piCongrLeft' P e) f x = f (e.symm x)
-- Init.Data.String.Basic
String.Slice.Pos.str_le_str_iff : ∀ {s : String.Slice} {p q : s.Pos}, p.str ≤ q.str ↔ p ≤ q
-- Mathlib.Algebra.Group.TypeTags.Basic
ofAdd_neg : ∀ {α : Type u} [inst : Neg α] (x : α), Multiplicative.ofAdd (-x) = (Multiplicative.ofAdd x)⁻¹
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The (unique) morphism to a pointwise right Kan extension.  -/
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.homTo : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                {E : L.RightExtension F} → E.IsPointwiseRightKanExtension → (G : L.RightExtension F) → G ⟶ E
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.finite_dsupport : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  Memℓp f 0 → {i | f i ≠ 0}.Finite
-- Init.Data.String.Basic
String.Pos.Raw.isValid_eq_true_iff : ∀ {s : String} {p : String.Pos.Raw}, String.Pos.Raw.isValid s p = true ↔ String.Pos.Raw.IsValid s p
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- Restriction of a ring homomorphism to its range interpreted as a `NonUnitalSubring`.

This is the bundled version of `Set.rangeFactorization`.  -/
NonUnitalRingHom.rangeRestrict : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocRing R] → [inst_1 : NonUnitalNonAssocRing S] → (f : R →ₙ+* S) → R →ₙ+* ↥f.range
-- Mathlib.Topology.Separation.Hausdorff
isPreirreducible_iff_forall_mem_subset_closure_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {S : Set X}, IsPreirreducible S ↔ ∀ x ∈ S, S ⊆ closure {x}
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- The comparison map `image (f ≫ g) ⟶ image g`.  -/
CategoryTheory.Limits.image.preComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        {Z : C} →
          (g : Y ⟶ Z) →
            [inst_1 : CategoryTheory.Limits.HasImage g] →
              [inst_2 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)] →
                CategoryTheory.Limits.image (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.Limits.image g
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instAlgebra : {S : Type u_2} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {R : Type u_3} →
        {T : Type u_4} →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring T] → [Algebra R T] → (v : AbsoluteValue T S) → Algebra R (WithAbs v)
-- Init.Data.Array.Lemmas
Array.reverse_reverse : ∀ {α : Type u_1} (xs : Array α), xs.reverse.reverse = xs
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instMulZeroOneClass : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [MulZeroOneClass R] → MulZeroOneClass (l.Germ R)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote' : {α : Type u_1} → [Lean.Grind.Ring α] → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Poly → α
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- An `AddSubgroup` is isomorphic to its image under an injective function. If
you have an isomorphism, use `AddEquiv.addSubmonoidMap` for better definitional equalities.  -/
AddSubmonoid.equivMapOfInjective : {N : Type u_2} →
  [inst : AddZeroClass N] →
    {M : Type u_5} →
      [inst_1 : AddZeroClass M] →
        (S : AddSubmonoid M) → (f : M →+ N) → Function.Injective ⇑f → ↥S ≃+ ↥(AddSubmonoid.map f S)
-- Mathlib.Analysis.Complex.Trigonometric
Real.two_mul_sin_mul_cos : ∀ (x y : ℝ), 2 * Real.sin x * Real.cos y = Real.sin (x - y) + Real.sin (x + y)
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.induction_of_closure_eq_top_right : ∀ {M : Type u_1} [inst : Monoid M] {s : Set M} {motive : M → Prop},
  Submonoid.closure s = ⊤ → ∀ (x : M), motive 1 → (∀ (x y : M), y ∈ s → motive x → motive (x * y)) → motive x
-- Mathlib.Logic.Function.DependsOn
dependsOn_iff_exists_comp : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} [Nonempty β] {f : ((i : ι) → α i) → β} {s : Set ι},
  DependsOn f s ↔ ∃ g, f = g ∘ s.domRestrict
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agmSequences_min_max : ∀ {x y : NNReal}, (min x y).agmSequences (max x y) = x.agmSequences y
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_sub_const : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddGroup G]
  [inst_2 : AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G), f (x - a) = f x - b
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.symm_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵈ Y) (x : X),
  e.symm (e x) = x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_insertListConst_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited β] {l : List ((_ : α) × β)}
  {toInsert : List (α × β)} {k k' : α} {v : β},
  Std.Internal.List.DistinctKeys l →
    (k == k') = true →
      List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert →
        (k, v) ∈ toInsert → Std.Internal.List.getValue! k' (Std.Internal.List.insertListConst l toInsert) = v
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.nonnegative : {u : Lean.Level} →
  {α : Q(Type u)} →
    {zα : Q(Zero «$α»)} →
      {e : Q(«$α»)} → {pα : Q(PartialOrder «$α»)} → Q(0 ≤ «$e») → Mathlib.Meta.Positivity.Strictness zα e (some pα)