mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∩ t₂).getKey! k = default
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.rankAtStalk_eq_zero_iff_notMem_support : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.Finite R M] (p : PrimeSpectrum R), Module.rankAtStalk M p = 0 ↔ p ∉ Module.support R M
-- Mathlib.Data.Nat.ModEq
/-- The forward direction of `modEq_iff_dvd'`, which does not require the `a ≤ b` assumption.  -/
Nat.ModEq.dvd' : ∀ {n a b : ℕ}, a ≡ b [MOD n] → n ∣ b - a
-- Init.Data.Format.Basic
/-- Specifies a “user-facing” way to convert from the type `α` to a `Format` object. There is no
expectation that the resulting string is valid code.

The `Repr` class is similar, but the expectation is that instances produce valid Lean code.
 -/
Std.ToFormat : Type u → Type u
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} {h' : k ∈ Std.ExtDHashMap.filterMap f m},
  (Std.ExtDHashMap.filterMap f m).get k h' = (f k (m.get k ⋯)).get ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
/-- If `d : MulticospanIndex J C` and `F : C ⥤ D`, this is the obvious isomorphism
`(d.map F).multicospan ≅ d.multicospan ⋙ F`.  -/
CategoryTheory.Limits.MulticospanIndex.multicospanMapIso : {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] →
        {J : CategoryTheory.Limits.MulticospanShape} →
          (d : CategoryTheory.Limits.MulticospanIndex J C) →
            (F : CategoryTheory.Functor C D) → (d.map F).multicospan ≅ d.multicospan.comp F
-- Mathlib.Algebra.Squarefree.Basic
isRadical_iff_squarefree_of_ne_zero : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {x : R} [DecompositionMonoid R],
  x ≠ 0 → (IsRadical x ↔ Squarefree x)
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.partNum_none_iff_s_none : ∀ {α : Type u_1} {g : GenContFract α} {n : ℕ}, g.partNums.get? n = none ↔ g.s.get? n = none
-- Mathlib.Data.FunLike.Fintype
/-- All `DFunLike`s are finite if their domain and codomain are.

Can't be an instance because it can cause infinite loops.
 -/
DFunLike.finite : ∀ (F : Sort u_1) {α : Sort u_3} {β : α → Sort u_5} [DFunLike F α β] [Finite α] [∀ (i : α), Finite (β i)], Finite F
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.toList_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, t.toArray.toList = t.toList
-- Mathlib.Data.List.TakeWhile
List.dropWhile_get_zero_not : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (hl : 0 < (List.dropWhile p l).length),
  ¬p ((List.dropWhile p l).get ⟨0, hl⟩) = true
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedGoalM : {σ : Type} → Inhabited (Lean.Meta.Grind.GoalM σ)
-- Init.Data.UInt.Lemmas
UInt32.ofNatClamp_uInt8ToNat : ∀ (n : UInt8), UInt32.ofNatClamp n.toNat = n.toUInt32
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.instHasHomologyF : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') (j : ι)
  [K.HasHomology j], (K.extend e).HasHomology (e.f j)
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1`, `*` and `⁻¹` is a group, if it admits a surjective map that preserves
`1`, `*` and `⁻¹` to a group. See note [reducible non-instances].  -/
Function.Surjective.group : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₂] →
      [inst_1 : One M₂] →
        [inst_2 : Pow M₂ ℕ] →
          [inst_3 : Inv M₂] →
            [inst_4 : Div M₂] →
              [inst_5 : Pow M₂ ℤ] →
                [inst_6 : Group M₁] →
                  (f : M₁ → M₂) →
                    Function.Surjective f →
                      f 1 = 1 →
                        (∀ (x y : M₁), f (x * y) = f x * f y) →
                          (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) →
                            (∀ (x y : M₁), f (x / y) = f x / f y) →
                              (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) →
                                (∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) → Group M₂
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.isPullback`. -/
CategoryTheory.Classifier.SubobjectRepresentableBy.isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {U X : C} (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m],
  CategoryTheory.IsPullback m (h.π m) (h.χ m) h.Ω₀.arrow
-- Mathlib.Topology.Closure
Disjoint.closure_left : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, Disjoint s t → IsOpen t → Disjoint (closure s) t
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPushout.inl_snd' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y}
  (h : b.IsBilimit), CategoryTheory.IsPushout b.inl 0 b.snd 0
-- Mathlib.MeasureTheory.Covering.Vitali
/-- Assume that around every point there are arbitrarily small scales at which the measure is
doubling. Then the set of closed sets `a` with nonempty interior contained in `closedBall x r` and
covering a fixed proportion `1/C` of the ball `closedBall x (3 * r)` forms a Vitali family.
This is essentially a restatement of the measurable Vitali theorem.  -/
Vitali.vitaliFamily : {α : Type u_1} →
  [inst : PseudoMetricSpace α] →
    [inst_1 : MeasurableSpace α] →
      [OpensMeasurableSpace α] →
        [SecondCountableTopology α] →
          (μ : MeasureTheory.Measure α) →
            [MeasureTheory.IsLocallyFiniteMeasure μ] →
              (C : NNReal) →
                (∀ (x : α),
                    ∃ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0),
                      μ (Metric.closedBall x (3 * r)) ≤ ↑C * μ (Metric.closedBall x r)) →
                  VitaliFamily μ
-- Lean.Parser.Module
_private.Lean.Parser.Module.0.Lean.Parser.setStartOfFileLeading : Lean.Syntax → Lean.Syntax × Bool
-- Mathlib.GroupTheory.FiniteAbelian.Duality
CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity : ∀ (G : Type u_1) (M : Type u_2) [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)], Nat.card (G →* Mˣ) = Nat.card G
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.single_sup : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → SemilatticeSup (f i)]
  [inst_2 : (i : I) → Zero (f i)] (i : I) (x y : f i), Pi.single i (x ⊔ y) = Pi.single i x ⊔ Pi.single i y
-- Mathlib.Data.Set.Lattice
Set.insert_iInter : ∀ {β : Type u_2} {ι : Sort u_5} (x : β) (t : ι → Set β), insert x (⋂ i, t i) = ⋂ i, insert x (t i)
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- Dyck words form an additive cancellative monoid under concatenation,
with the empty word as 0.  -/
instAddCancelMonoidDyckWord : AddCancelMonoid DyckWord
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- The natural transformation including the subpresheaf of functions satisfying a local predicate
into the presheaf of all functions.
 -/
TopCat.subpresheafToTypes.subtype : {X : TopCat} →
  {T : ↑X → Type u_1} → (P : TopCat.PrelocalPredicate T) → TopCat.subpresheafToTypes P ⟶ X.presheafToTypes T
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.instIsLocallyFiniteMeasureRestrict : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α} [inst : TopologicalSpace α] (μ : MeasureTheory.Measure α)
  [hμ : MeasureTheory.IsLocallyFiniteMeasure μ], MeasureTheory.IsLocallyFiniteMeasure (μ.restrict s)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- For a `C^n` vector bundle `E` over `B` with fiber modelled on `F`, the change-of-co-ordinates
between two trivializations `e`, `e'` for `E`, considered as charts to `B × F`, is `C^n` and
fiberwise linear.  -/
ContMDiffFiberwiseLinear.hasGroupoid : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB], HasGroupoid (Bundle.TotalSpace F E) (contMDiffFiberwiseLinear B F IB n)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If a category `C` has 0-morphisms, there is a canonical projection from a coproduct `X ⨿ Y` to
its second component `Y`.  -/
CategoryTheory.Limits.coprod.snd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) → [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y] → X ⨿ Y ⟶ Y
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- The restriction homomorphism from the Galois group of `C/A` to the Galois group of `B/A` where
`C/B/A` is a tower of domains with `C/A` and `B/A` Galois.  -/
IsGaloisGroup.restrictHom : (G : Type u_1) →
  (G' : Type u_2) →
    [inst : Group G] →
      [inst_1 : Group G'] →
        (A : Type u_5) →
          (B : Type u_6) →
            (C : Type u_7) →
              [inst_2 : CommRing A] →
                [inst_3 : CommRing B] →
                  [inst_4 : CommRing C] →
                    [IsDomain C] →
                      [inst_6 : Algebra A B] →
                        [inst_7 : Algebra A C] →
                          [inst_8 : Algebra B C] →
                            [FaithfulSMul A B] →
                              [FaithfulSMul B C] →
                                [IsScalarTower A B C] →
                                  [Finite G] →
                                    [Finite G'] →
                                      [inst_14 : MulSemiringAction G C] →
                                        [IsGaloisGroup G A C] →
                                          [inst_16 : MulSemiringAction G' B] → [IsGaloisGroup G' A B] → G →* G'
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.unop_op_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Fork f g), c.unop.op.ι = c.ι
-- Init.Data.String.Defs
String.Internal.pushnImpl : String → Char → ℕ → String
-- Mathlib.CategoryTheory.Sites.Localization
CategoryTheory.GrothendieckTopology.W_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {A : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  {P₁ P₂ : CategoryTheory.Functor Cᵒᵖ A} (f : P₁ ⟶ P₂),
  J.W f ↔ CategoryTheory.IsIso ((CategoryTheory.presheafToSheaf J A).map f)
-- Mathlib.Logic.Nonempty
nonempty_plift : ∀ {α : Sort u_3}, Nonempty (PLift α) ↔ Nonempty α
-- Mathlib.Algebra.Category.AlgCat.Monoidal
AlgCat.hom_hom_associator : ∀ {R : Type u} [inst : CommRing R] {M N K : AlgCat R},
  AlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).hom =
    ↑(Algebra.TensorProduct.assoc R R R ↑M ↑N ↑K)
-- Init.Data.Sum.Lemmas
Sum.map_map : ∀ {α' : Type u_1} {α'' : Type u_2} {β' : Type u_3} {β'' : Type u_4} {α : Type u_5} {β : Type u_6} (f' : α' → α'')
  (g' : β' → β'') (f : α → α') (g : β → β') (x : α ⊕ β), Sum.map f' g' (Sum.map f g x) = Sum.map (f' ∘ f) (g' ∘ g) x
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.reduce_replicate : ∀ {α : Type u_1} [inst : DecidableEq α] (n : ℕ) (x : α × Bool),
  FreeGroup.reduce (List.replicate n x) = List.replicate n x
-- Lean.Meta.Sym.SymM
/-- Returns the internalized `False` constant.   -/
Lean.Meta.Sym.getFalseExpr : Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.descTruncGE.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f f_1 : X ⟶ Y),
  f = f_1 → ∀ (n : ℤ) [inst_6 : t.IsGE Y n], t.descTruncGE f n = t.descTruncGE f_1 n
-- Lean.Meta.Tactic.Grind.Extension
/-- It instructs `grind` to postpone the instantiation of the theorem until `e` is known to be `true`.
 -/
Lean.Meta.Grind.EMatchTheoremConstraint.guard : Lean.Expr → Lean.Meta.Grind.EMatchTheoremConstraint
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_mapM_map : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_8 : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → γ} {g : γ → n δ} {it : Std.IterM m β},
  (Std.IterM.mapM g (Std.IterM.map f it)).toListRev = (Std.IterM.mapM (fun b => g (f b)) it).toListRev
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_iInf : ∀ {ι : Sort u_1} {M : Type u_2} [inst : MulOneClass M] (S : ι → Submonoid Mᵐᵒᵖ), (iInf S).unop = ⨅ i, (S i).unop
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- The inner product of two linear combinations of a set of orthonormal vectors, expressed as
a sum over the first `Finsupp`.  -/
Orthonormal.inner_finsupp_eq_sum_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E},
  Orthonormal 𝕜 v →
    ∀ (l₁ l₂ : ι →₀ 𝕜),
      inner 𝕜 ((Finsupp.linearCombination 𝕜 v) l₁) ((Finsupp.linearCombination 𝕜 v) l₂) =
        l₁.sum fun i y => (starRingEnd 𝕜) y * l₂ i
-- Mathlib.NumberTheory.AbelSummation
locallyIntegrableOn_mul_sum_Icc : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {a : ℝ} {m : ℕ},
  0 ≤ a →
    ∀ {g : ℝ → 𝕜},
      MeasureTheory.LocallyIntegrableOn g (Set.Ici a) MeasureTheory.volume →
        MeasureTheory.LocallyIntegrableOn (fun t => g t * ∑ k ∈ Finset.Icc m ⌊t⌋₊, c k) (Set.Ici a) MeasureTheory.volume
-- Mathlib.Data.ENNReal.Operations
/-- This is a special case of `WithTop.coe_sub` in the `ENNReal` namespace  -/
ENNReal.coe_sub : ∀ {r p : NNReal}, ↑(r - p) = ↑r - ↑p
-- Mathlib.Probability.Distributions.Beta
ProbabilityTheory.betaPDF_eq_zero_of_one_le : ∀ {α β x : ℝ}, 1 ≤ x → ProbabilityTheory.betaPDF α β x = 0
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- If `K` is complete, any `v` in `E` can be expressed as a sum of elements of `K` and `Kᗮ`.  -/
Submodule.exists_add_mem_mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [K.HasOrthogonalProjection] (v : E), ∃ y ∈ K, ∃ z ∈ Kᗮ, v = y + z
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.BitVecValue.mk.inj : ∀ {n : ℕ} {val : BitVec n} {n_1 : ℕ} {val_1 : BitVec n_1},
  { n := n, val := val } = { n := n_1, val := val_1 } → n = n_1 ∧ val ≍ val_1
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.finMulAntidiag_eq_piFinset_divisors_filter : ∀ {d m n : ℕ}, m ∣ n → n ≠ 0 → d.finMulAntidiag m = {f ∈ Fintype.piFinset fun x => n.divisors | ∏ i, f i = m}
-- Mathlib.Topology.Compactification.StoneCech
preStoneCechExtend_preStoneCechUnit : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [inst_2 : T2Space β]
  [inst_3 : CompactSpace β] {g : α → β} (hg : Continuous g) (a : α), preStoneCechExtend hg (preStoneCechUnit a) = g a
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.instDiv : {G : Type u_1} → [inst : Add G] → {a : G} → Div (AddConstEquiv G G a a)
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- A pretransitive action is preprimitive
iff the stabilizer of any point is a maximal subgroup (Wielandt, th. 7.5)  -/
MulAction.isCoatom_stabilizer_iff_preprimitive : ∀ (G : Type u_3) [inst : Group G] {X : Type u_4} [inst_1 : MulAction G X] [MulAction.IsPretransitive G X] [Nontrivial X]
  (a : X), IsCoatom (MulAction.stabilizer G a) ↔ MulAction.IsPreprimitive G X
-- Mathlib.AlgebraicTopology.CechNerve
/-- A helper function used in defining the Čech adjunction.  -/
CategoryTheory.SimplicialObject.equivalenceRightToLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 :
        ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
          CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] →
      (X : CategoryTheory.SimplicialObject.Augmented C) →
        (F : CategoryTheory.Arrow C) →
          (X ⟶ F.augmentedCechNerve) → (CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
/-- The postcomposition `Ext X Y a →ₗ[R] Ext X Z b` with `β : Ext Y Z n` when `a + n = b`.  -/
CategoryTheory.Abelian.Ext.postcompOfLinear : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {Y Z : C} →
          {n : ℕ} →
            CategoryTheory.Abelian.Ext Y Z n →
              (R : Type t) →
                [inst_3 : CommRing R] →
                  [inst_4 : CategoryTheory.Linear R C] →
                    (X : C) →
                      {a b : ℕ} → a + n = b → CategoryTheory.Abelian.Ext X Y a →ₗ[R] CategoryTheory.Abelian.Ext X Z b
-- Init.Data.Option.Lemmas
Option.pelim_none : ∀ {α : Sort u_1} {b : α} {α_1 : Type u_2} {f : (a : α_1) → none = some a → α}, none.pelim b f = b
-- Init.Data.List.Control
List.foldlM.eq_2 : ∀ {m : Type u → Type v} [inst : Monad m] {s : Type u} {α : Type w} (x : s → α → m s) (x_1 : s) (a : α) (as : List α),
  List.foldlM x x_1 (a :: as) = do
    let s' ← x x_1 a
    List.foldlM x s' as
-- Mathlib.Algebra.Group.Defs
AddSemigroup.ext_iff : ∀ {G : Type u} {x y : AddSemigroup G}, x = y ↔ Add.add = Add.add
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.empty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α], ∅.WF
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKey?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getKey? k = t₂.getKey? k
-- Init.Data.List.Sublist
_private.Init.Data.List.Sublist.0.List.isSublist.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (x : List α) → motive x [])
  (h_3 :
    (l₁ : List α) →
      (hd₁ : α) → (tl₁ : List α) → l₁ = hd₁ :: tl₁ → (hd₂ : α) → (tl₂ : List α) → motive (hd₁ :: tl₁) (hd₂ :: tl₂)),
  (match [], x with
    | [], x => h_1 x
    | x, [] => h_2 x
    | l₁@h:(hd₁ :: tl₁), hd₂ :: tl₂ => h_3 l₁ hd₁ tl₁ h hd₂ tl₂) =
    h_1 x
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.ofList.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (l : List ((a : α) × β a)),
  Std.DHashMap.Raw.ofList l = ∅.insertMany l
-- Mathlib.Data.TypeVec
TypeVec.repeatEq.eq_2 : ∀ (n : ℕ) (α : TypeVec.{u_1} n.succ), α.repeatEq = (α.drop.repeatEq ::: Function.uncurry Eq)
-- Lean.Meta.Instances
_private.Lean.Meta.Instances.0.Lean.Meta.computeSynthOrder.assignMVarsIn : Array Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.MetaM Unit
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- `Real.exp` as an `OpenPartialHomeomorph` with `source = univ` and `target = {z | 0 < z}`.  -/
Real.expPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongrLeft_apply_fst : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (ab : β₁ × α₁),
  ((Equiv.prodCongrLeft e) ab).1 = (e ab.2) ab.1
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin_sum : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F},
  (∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) → derivWithin (∑ i ∈ u, A i) s x = ∑ i ∈ u, derivWithin (A i) s x
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_iInf_uniformSpace' : ∀ {β : Type v} {ι : Sort u_1} {u : ι → UniformSpace β} {l : Filter β} [l.NeBot], Cauchy l ↔ ∀ (i : ι), Cauchy l
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Patterns with support exactly `U` form a finite set.  -/
SymbolicDynamics.FullShift.finite_setOfPred_pattern_support_eq : ∀ {A : Type u_3} {G : Type u_4} [Finite A] [inst : Inhabited A] (U : Finset G), {p | p.support = U}.Finite
-- Mathlib.Data.Rat.Defs
Rat.pow_eq_divInt : ∀ (q : ℚ) (n : ℕ), q ^ n = Rat.divInt (q.num ^ n) (↑q.den ^ n)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ →
    ∀ {g : α → ENNReal},
      AEMeasurable g (μ.withDensity f) →
        ∀ {s : Set α}, MeasurableSet s → ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueFree_map_iff : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : ℕ} {f : α ↪ β} [Nonempty α],
  (SimpleGraph.map (⇑f) G).CliqueFree n ↔ G.CliqueFree n
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Combinators.Monadic.FilterMap.0.Std.Iterators.Types.FilterMap.instFinitenessRelation : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      [inst : Monad n] →
        [inst_1 : Std.Iterator α m β] →
          {lift : ⦃α : Type w⦄ → m α → n α} →
            {f : β → Std.Iterators.PostconditionT n (Option γ)} →
              [Std.Iterators.Finite α m] →
                Std.Iterators.FinitenessRelation (Std.Iterators.Types.FilterMap α m n lift f) n
-- Mathlib.Analysis.Matrix.LDL
LDL.lowerInv_orthogonal : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n] [inst_2 : WellFoundedLT n]
  [inst_3 : LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [inst_4 : Fintype n] (hS : S.PosDef) {i j : n},
  i ≠ j → inner 𝕜 (WithLp.toLp 2 (LDL.lowerInv hS i)) (WithLp.toLp 2 (S.transpose.mulVec (LDL.lowerInv hS j))) = 0
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.add_mem_Icc_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a + b ∈ Set.Icc c d ↔ b ∈ Set.Icc (c - a) (d - a)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
null_frontier_inter : ∀ {α' : Type u_6} [inst : TopologicalSpace α'] [inst_1 : MeasurableSpace α'] {μ : MeasureTheory.Measure α'}
  {s s' : Set α'}, μ (frontier s) = 0 → μ (frontier s') = 0 → μ (frontier (s ∩ s')) = 0
-- Mathlib.Algebra.Field.Shrink
Shrink.instField : {α : Type u_1} → [inst : Small.{v, u_1} α] → [Field α] → Field (Shrink.{v, u_1} α)