mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.isSeparatedMap : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f → IsSeparatedMap f
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅} {km : α},
  t.min he = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  [CategoryTheory.Limits.HasColimitsOfShape Jᵒᵖ Cᵒᵖ], CategoryTheory.Limits.HasLimitsOfShape J C
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc.eq_1 : ∀ {n : ℕ} (i j : Fin n),
  i.cycleIcc j =
    if hij : i ≤ j then ((j - i).castLT ⋯).cycleRange.extendDomain (Fin.natAdd_castLEEmb ⋯).toEquivRange else 1
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_nonneg_iff_neg_imp_nonpos : ∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R]
  [AddLeftMono R] [AddLeftReflectLE R], 0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
-- Init.Control.Lawful.Instances
ExceptT.run_tryCatch : ∀ {m : Type u_1 → Type u_2} {ε α : Type u_1} [inst : Monad m] [LawfulMonad m] (x : ExceptT ε m α)
  (h : ε → ExceptT ε m α),
  (tryCatch x h).run = do
    let r ← x.run
    match r with
      | Except.ok a => pure (Except.ok a)
      | Except.error e => (h e).run
-- Init.Data.Range.Polymorphic.SInt
Int8.lt.eq_1 : ∀ (a b : Int8), a.lt b = (a.toBitVec.slt b.toBitVec = true)
-- Mathlib.FieldTheory.PurelyInseparable.Basic
AlgEquiv.isPurelyInseparable_iff : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [inst_1 : Ring E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Ring K] [inst_4 : Algebra F K] (e : K ≃ₐ[F] E), IsPurelyInseparable F K ↔ IsPurelyInseparable F E
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The ring homomorphism from the colimit ring to the cone point of any other
cocone.  -/
RingCat.Colimits.descMorphism : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → (s : CategoryTheory.Limits.Cocone F) → RingCat.Colimits.colimit F ⟶ s.pt
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.p_fromOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology],
  CategoryTheory.CategoryStruct.comp S.pOpcycles S.fromOpcycles = S.g
-- Mathlib.Combinatorics.SimpleGraph.DegreeSum
SimpleGraph.dart_edge_fiber_card : ∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V],
  ∀ e ∈ G.edgeSet, {d | d.edge = e}.card = 2
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.coprod_inr_rightDistrib_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalRightDistrib C] {X Y Z : C},
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (∂R X Y Z).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inr X
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.inclLift_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (x : C),
  (CategoryTheory.WithInitial.inclLift F M hM).hom.app x =
    CategoryTheory.CategoryStruct.id
      (match CategoryTheory.WithInitial.incl.obj x with
      | CategoryTheory.WithInitial.of x => F.obj x
      | CategoryTheory.WithInitial.star => Z)
-- Aesop.Builder.Constructors
Aesop.RuleBuilderOptions.constructorsTransparency : Aesop.RuleBuilderOptions → Lean.Meta.TransparencyMode
-- Mathlib.Analysis.Normed.Unbundled.InvariantExtension
/-- Given a normed field `K`, a finite algebraic extension `L/K` and `σ : L ≃ₐ[K] L`, the function
`L → ℝ` sending `x : L` to `‖ σ x ‖`, where `‖ ⬝ ‖` is any power-multiplicative algebra norm on `L`
extending the norm on `K`, is an algebra norm on `K`.  -/
IsUltrametricDist.algNormOfAlgEquiv : {K : Type u_1} →
  [inst : NormedField K] →
    {L : Type u_2} →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [h_fin : FiniteDimensional K L] → [hu : IsUltrametricDist K] → Gal(L/K) → AlgebraNorm K L
-- Mathlib.Order.BoundedOrder.Basic
bot_unique : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a ≤ ⊥ → a = ⊥
-- Mathlib.Analysis.Calculus.TangentCone.Basic
IsOpen.uniqueDiffWithinAt : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : DivisionSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot] [ContinuousSMul 𝕜 E] {x : E}
  {s : Set E} [ContinuousAdd E], IsOpen s → x ∈ s → UniqueDiffWithinAt 𝕜 s x
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_eq_smul_one : ∀ {R : Type u} {σ : Type u_1} {a : R} [inst : CommSemiring R], MvPolynomial.C a = a • 1
-- Mathlib.Data.Set.Image
Set.compl_range_inr : ∀ {α : Type u_1} {β : Type u_2}, (Set.range Sum.inr)ᶜ = Set.range Sum.inl
-- Lean.Elab.InfoTree.Types
Lean.Elab.TacticInfo.mk.sizeOf_spec : ∀ (toElabInfo : Lean.Elab.ElabInfo) (mctxBefore : Lean.MetavarContext) (goalsBefore : List Lean.MVarId)
  (mctxAfter : Lean.MetavarContext) (goalsAfter : List Lean.MVarId),
  sizeOf
      { toElabInfo := toElabInfo, mctxBefore := mctxBefore, goalsBefore := goalsBefore, mctxAfter := mctxAfter,
        goalsAfter := goalsAfter } =
    1 + sizeOf toElabInfo + sizeOf mctxBefore + sizeOf goalsBefore + sizeOf mctxAfter + sizeOf goalsAfter
-- Mathlib.Data.Finset.Image
Finset.mapsTo_iff_image_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
  Set.MapsTo f ↑s ↑t ↔ Finset.image f s ⊆ t
-- Mathlib.Data.Finset.Card
Finset.card_cons : ∀ {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s), (Finset.cons a s h).card = s.card + 1
-- Aesop.Tree.UnsafeQueue
Aesop.PostponedSafeRule.toUnsafeRule : Aesop.PostponedSafeRule → Aesop.UnsafeRule
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.getDₘ.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α)
  (fallback : β),
  Std.DHashMap.Internal.Raw₀.Const.getDₘ m a fallback = (Std.DHashMap.Internal.Raw₀.Const.get?ₘ m a).getD fallback
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If `F ⋙ G` preserves limits and `G` reflects limits, then `F` preserves limits.  -/
CategoryTheory.Limits.preservesLimits_of_reflects_of_preserves : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (F.comp G)]
  [CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
-- Mathlib.Data.Option.Basic
Option.join_pmap_eq_pmap_join : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {x : Option (Option α)}
  (H : ∀ (a : Option α), x = some a → ∀ (a_2 : α), a = some a_2 → p a_2),
  (Option.pmap (Option.pmap f) x H).join = Option.pmap f x.join ⋯
-- Mathlib.CategoryTheory.Monoidal.Tor
CategoryTheory.Tor'_obj_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.HasProjectiveResolutions C] (n : ℕ) (k j : C),
  ((CategoryTheory.Tor' C n).obj k).obj j =
    (((CategoryTheory.MonoidalCategory.tensoringRight C).obj j).leftDerived n).obj k
-- Mathlib.Data.Vector.Defs
/-- `shiftLeftFill v i` is the vector obtained by left-shifting `v` `i` times and padding with the
`fill` argument. If `v.length < i` then this will return `replicate n fill`.  -/
List.Vector.shiftLeftFill : {α : Type u_1} → {n : ℕ} → List.Vector α n → ℕ → α → List.Vector α n
-- Mathlib.Data.NNRat.Floor
NNRat.instFloorSemiring : FloorSemiring ℚ≥0
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.ext_iff : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] {e e' : P ≃ᵃⁱ[𝕜] P₂}, e = e' ↔ ∀ (x : P), e x = e' x
-- Std.Async.System
_private.Std.Async.System.0.Std.Async.System.Environment.toHashMap : Std.Async.System.Environment → Std.HashMap String String
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_eq_circleMap_iff : ∀ {a b R : ℝ} (c : ℂ),
  R ≠ 0 → (circleMap c R a = circleMap c R b ↔ ∃ n, ↑a * Complex.I = ↑b * Complex.I + ↑n * (2 * ↑Real.pi * Complex.I))
-- Mathlib.Analysis.Convex.MetricSpace
Convexity.dist_convexCombPair_left : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] {s t : ℝ}
  (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X), dist (Convexity.convexCombPair s t hs ht h x y) x = t * dist x y
-- Lean.Server.References
Lean.Server.LoadedILean.mk.sizeOf_spec : ∀ (moduleUri : Lean.Lsp.DocumentUri) (ileanPath : System.FilePath) (directImports : Lean.Server.DirectImports)
  (refs : Lean.Lsp.ModuleRefs) (decls : Lean.Lsp.Decls),
  sizeOf
      { moduleUri := moduleUri, ileanPath := ileanPath, directImports := directImports, refs := refs, decls := decls } =
    1 + sizeOf moduleUri + sizeOf ileanPath + sizeOf directImports + sizeOf refs + sizeOf decls
-- Init.Data.List.Nat.Basic
_private.Init.Data.List.Nat.Basic.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlight.mk : Lean.Lsp.Range → Option Lean.Lsp.DocumentHighlightKind → Lean.Lsp.DocumentHighlight
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `sInf s = 0` when `s` is a set of reals that's unbounded below, it suffices to show that `s`
contains a nonpositive element to show that `sInf s ≤ 0`.  -/
Real.sInf_nonpos' : ∀ {s : Set ℝ}, (∃ x ∈ s, x ≤ 0) → sInf s ≤ 0
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedCommAux_lof_tmul : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  (i j : ι) (a : 𝒜 i) (b : ℬ j),
  (TensorProduct.gradedCommAux R 𝒜 ℬ)
      ((DirectSum.lof R (ι × ι) (fun i => TensorProduct R (𝒜 i.1) (ℬ i.2)) (i, j)) (a ⊗ₜ[R] b)) =
    (-1) ^ (j * i) • (DirectSum.lof R (ι × ι) (fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)) (j, i)) (b ⊗ₜ[R] a)
-- Mathlib.Data.Int.Init
/-- See `Int.inductionOn'` for an induction in both directions.  -/
Int.leInduction : {m : ℤ} →
  {motive : (n : ℤ) → m ≤ n → Sort u_1} →
    motive m ⋯ → ((n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯) → (n : ℤ) → (hmn : m ≤ n) → motive n hmn
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RiiSliceData.mk : {α : Type u} →
  {β : Type v} → (Std.DTreeMap.Internal.Impl α fun x => β) → Std.Rii α → Std.DTreeMap.Internal.Const.RiiSliceData α β
-- Init.Core
Eq.comm : ∀ {α : Sort u_1} {a b : α}, a = b ↔ b = a
-- Std.Data.DHashMap.RawLemmas
_private.Std.Data.DHashMap.RawLemmas.0.Std.DHashMap.Internal.Raw.baseNames : Array Lean.Name
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- If a function is differentiable on open sets `s i`, it is differentiable on their union.  -/
MDifferentiableOn.iUnion_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {ι : Type u_11}
  {s : ι → Set M}, (∀ (i : ι), MDiff[s i] f) → (∀ (i : ι), IsOpen (s i)) → MDiff[⋃ i, s i] f
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instAddCommMonoid : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → AddCommMonoid (E →ₛₗ.[σ] F)
-- Mathlib.Order.Heyting.Hom
HeytingHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β]
  [inst_2 : HeytingAlgebra γ] [inst_3 : HeytingAlgebra δ] (f : HeytingHom γ δ) (g : HeytingHom β γ)
  (h : HeytingHom α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.id_preservesColimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₁, u₁, u₁} (CategoryTheory.Functor.id C)
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.naturality_1_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ≅ G) (f : X ⟶ Y) {Z : D} (h : G.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.inv.app X)
      (CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (α.hom.app Y) h)) =
    CategoryTheory.CategoryStruct.comp (G.map f) h
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_eq_zero_of_forall_dual_of_isSeparable : ∀ {α : Type u_1} {E : Type u_2} (𝕜 : Type u_3) {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {t : Set E},
  TopologicalSpace.IsSeparable t →
    ∀ {f : α → E}, (∀ (c : StrongDual 𝕜 E), (fun x => c (f x)) =ᵐ[μ] 0) → (∀ᵐ (x : α) ∂μ, f x ∈ t) → f =ᵐ[μ] 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_add_arctan_lt_pi_div_two : ∀ {x y : ℝ}, x * y < 1 → Real.arctan x + Real.arctan y < Real.pi / 2
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.DTreeMap.Raw.keyAtIdxD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → ℕ → α → α
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.unmopMonObj_mul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : Cᴹᵒᵖ)
  [inst_2 : CategoryTheory.MonObj M], CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul.unmop
-- Mathlib.Algebra.Homology.BifunctorShift
CategoryTheory.Functor.commShiftIso_map₂CochainComplex_hom_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.Preadditive C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  [inst_8 : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F] (K₁ : CochainComplex C₁ ℤ)
  (K₂ : CochainComplex C₂ ℤ) (n : ℤ),
  (CategoryTheory.Functor.commShiftIso (F.map₂CochainComplex.obj K₁) n).hom.app K₂ =
    (K₁.mapBifunctorShift₂Iso K₂ F n).hom
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
/-- `AlgebraicIndepOn R v s` states that the elements in the family `v` that are indexed by the
elements of `s` are algebraically independent over `R`.  -/
AlgebraicIndepOn : {ι : Type u_1} →
  (R : Type u_3) → {A : Type u_5} → (ι → A) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Set ι → Prop
-- Lean.Util.FindExpr
Lean.Expr.FindStep.done.sizeOf_spec : sizeOf Lean.Expr.FindStep.done = 1
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsVanKampenColimit.precompose_isIso_iff : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} (α : F ⟶ G) [CategoryTheory.IsIso α] {c : CategoryTheory.Limits.Cocone G},
  CategoryTheory.IsVanKampenColimit ((CategoryTheory.Limits.Cocone.precompose α).obj c) ↔
    CategoryTheory.IsVanKampenColimit c
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.single_eq_same : ∀ (p : ENNReal) {ι : Type u_2} {β : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] (i : ι)
  (a : β i), (PiLp.single p i a).ofLp i = a
-- Mathlib.Data.Finset.Pi
Finset.restrict₂.eq_1 : ∀ {ι : Type u_2} {π : ι → Type u_3} {s t : Finset ι} (hst : s ⊆ t) (f : (i : ↥t) → π ↑i) (i : ↥s),
  Finset.restrict₂ hst f i = f ⟨↑i, ⋯⟩
-- Mathlib.Data.List.Basic
List.cons_sublist_cons' : ∀ {α : Type u} {l₁ l₂ : List α} {a b : α}, (a :: l₁).Sublist (b :: l₂) ↔ (a :: l₁).Sublist l₂ ∨ a = b ∧ l₁.Sublist l₂
-- Init.Data.Vector.Lemmas
Vector.not_all_eq_any_not : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool}, (!xs.all p) = xs.any fun a => !p a
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimInfo.targetsPos : Lean.Meta.ElimInfo → Array ℕ
-- Lean.Declaration
Lean.AxiomVal.mk.sizeOf_spec : ∀ (toConstantVal : Lean.ConstantVal) (isUnsafe : Bool),
  sizeOf { toConstantVal := toConstantVal, isUnsafe := isUnsafe } = 1 + sizeOf toConstantVal + sizeOf isUnsafe
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteColimitsSheafSheafFiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A],
  CategoryTheory.Limits.PreservesFiniteColimits Φ.sheafFiber
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideCoequalizer.π_desc_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f] [inst_2 : Nonempty J] {W : C} (k : Y ⟶ W)
  (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k) {Z : C}
  (h_1 : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.desc k h) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- A `completeEquipartiteGraph` is isomorphic to a corresponding `completeMultipartiteGraph`.

The difference is that the former vertices are a product type whereas the latter vertices are a
*dependent* product type.  -/
SimpleGraph.completeEquipartiteGraph.completeMultipartiteGraph : {r t : ℕ} →
  SimpleGraph.completeEquipartiteGraph r t ≃g SimpleGraph.completeMultipartiteGraph (Function.const (Fin r) (Fin t))
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.id_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (x : Cᵒᵖ),
  (CategoryTheory.Profunctor.id.map f).app x = TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp g f
-- Mathlib.Order.Filter.AtTopBot.Archimedean
tendsto_natCast_atTop_iff : ∀ {α : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R]
  {f : α → ℕ} {l : Filter α}, Filter.Tendsto (fun n => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
-- Mathlib.Algebra.Algebra.Pi
AlgEquiv.sumArrowEquivProdArrow_apply : ∀ {α : Type u_1} {β : Type u_2} {R : Type u_3} [inst : CommSemiring R] (S : Type u_8) [inst_1 : Semiring S]
  [inst_2 : Algebra R S] (x : α ⊕ β → S),
  (AlgEquiv.sumArrowEquivProdArrow α β R S) x = (Equiv.sumArrowEquivProdArrow α β S) x
-- Mathlib.Data.Matrix.Block
Matrix.toBlocks_fromBlocks₁₂ : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α)
  (C : Matrix o l α) (D : Matrix o m α), (Matrix.fromBlocks A B C D).toBlocks₁₂ = B
-- Mathlib.Algebra.Order.Ring.Finset
Nat.cast_finsetInf' : ∀ {ι : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {s : Finset ι}
  (f : ι → ℕ) (hs : s.Nonempty), ↑(s.inf' hs f) = s.inf' hs fun i => ↑(f i)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_head_idempotent : Lean.Grind.AC.Var → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.EqCnstrProof
-- Init.Data.SInt.Lemmas
Int8.sub_mul : ∀ {a b c : Int8}, (a - b) * c = a * c - b * c
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffSMul.of_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : SMul G M] {n m : WithTop ℕ∞},
  n ≤ m → ∀ [ContMDiffSMul I I' m G M], ContMDiffSMul I I' n G M
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.aemeasurable_bind : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {g : α → MeasureTheory.Measure β}
  {m : MeasureTheory.Measure (MeasureTheory.Measure α)}, AEMeasurable g m.join → AEMeasurable (fun x => x.bind g) m
-- Mathlib.Order.Basic
/-- monotonicity of `>` with respect to `→`  -/
gt_imp_gt_of_le_of_le : ∀ {α : Type u_2} [inst : Preorder α] {a b c d : α}, a ≤ c → d ≤ b → a > b → c > d
-- Mathlib.Tactic.Sat.FromLRAT
/-- A localized clause reference.
It is the same as `Clause` except that the proof is now a local variable.  -/
Mathlib.Tactic.Sat.LClause : Type
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- The property that morphisms between single complexes in arbitrary degrees are `w`-small
in the derived category.  -/
CategoryTheory.HasExt : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → Prop
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inverseAssociatorIsEquivalence : ∀ (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],
  (CategoryTheory.sum.inverseAssociator C D E).IsEquivalence
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
Lean.Meta.Grind.Arith.Linear.isHSMulNatInst : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr → Bool
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- The technical version of *Legendre's Theorem*.  -/
Real.exists_rat_eq_convergent' : ∀ {ξ : ℝ} {u : ℤ} {v : ℕ}, Real.ContfracLegendre.Ass ξ u ↑v → ∃ n, ↑u / ↑v = ξ.convergent n