mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.neg_extMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m) (hf : CategoryTheory.CategoryStruct.comp (R.complex.d m n) f = 0),
  -R.extMk f m hm hf = R.extMk (-f) m hm ⋯
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.map_div₂ : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : AddGroup M} {x_1 : AddZeroClass N} {x_2 : AddCommGroup P}
  (f : M →+ N →+ P) (m₁ m₂ : M) (n : N), (f (m₁ - m₂)) n = (f m₁) n - (f m₂) n
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.Saturate.below.transitive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Coverage C}
  {motive : (X : C) → (a : CategoryTheory.Sieve X) → K.Saturate X a → Prop} (X : C) (R S : CategoryTheory.Sieve X)
  (a : K.Saturate X R) (a_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (CategoryTheory.Sieve.pullback f S)),
  CategoryTheory.Coverage.Saturate.below a →
    motive X R a →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), CategoryTheory.Coverage.Saturate.below ⋯) →
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), motive Y (CategoryTheory.Sieve.pullback f S) ⋯) →
          CategoryTheory.Coverage.Saturate.below ⋯
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo_ofDual : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : αᵒᵈ),
  Set.uIoo (OrderDual.ofDual a) (OrderDual.ofDual b) = ⇑OrderDual.toDual ⁻¹' Set.uIoo a b
-- Mathlib.Algebra.Homology.Localization
/-- The functor `HomologicalComplexUpToQuasiIso C c ⥤ HomologicalComplexUpToQuasiIso D c`
induced by a functor `F : C ⥤ D` which preserves homology.  -/
CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (F : CategoryTheory.Functor C D) →
          {ι : Type u_3} →
            (c : ComplexShape ι) →
              [inst_2 : CategoryTheory.Preadditive C] →
                [inst_3 : CategoryTheory.Preadditive D] →
                  [inst_4 : CategoryTheory.CategoryWithHomology C] →
                    [inst_5 : CategoryTheory.CategoryWithHomology D] →
                      [inst_6 : (HomologicalComplex.quasiIso D c).HasLocalization] →
                        [inst_7 : F.Additive] →
                          [F.PreservesHomology] →
                            [inst_9 : (HomologicalComplex.quasiIso C c).HasLocalization] →
                              CategoryTheory.Functor (HomologicalComplexUpToQuasiIso C c)
                                (HomologicalComplexUpToQuasiIso D c)
-- Mathlib.Data.List.MinMax
List.minimum_of_length_pos_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} (h : 0 < l.length), List.minimum_of_length_pos h ∈ l
-- Aesop.Tree.ExtractProof
Aesop.extractSafePrefix : Aesop.TreeM (Array Lean.MVarId)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
le_mul_of_le_mul_of_nonneg_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α],
  a ≤ b * c → c ≤ d → 0 ≤ b → a ≤ b * d
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.colimit_cocone_comp_aux : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (s : CategoryTheory.Limits.Cocone (F.comp G)) (j : C),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.Final.homToLift F (F.obj j)))
      (s.ι.app (CategoryTheory.Functor.Final.lift F (F.obj j))) =
    s.ι.app j
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.δ₀Iter.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) {n m : ℕ}
  (i i_1 : ℕ) (e_i : i = i_1) (hi : n + i = m), X.δ₀Iter i hi = X.δ₀Iter i_1 ⋯
-- Init.Data.Option.Lemmas
Option.or_eq_left_of_none : ∀ {α : Type u_1} {o o' : Option α}, o' = none → o.or o' = o
-- Lean.Parser.Types
Lean.Parser.TokenCacheEntry : Type
-- Mathlib.Data.SetLike.Basic
SetLike.ext' : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, ↑p = ↑q → p = q
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.nnreal_smul_coe_apply : ∀ {α : Type u_1} {_m : MeasurableSpace α} (c : NNReal) (μ : MeasureTheory.Measure α) (s : Set α), c • μ s = ↑c * μ s
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.map_smul : ∀ {R : Type u_1} [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Linear R F] {X Y : C} (r : R) (f : X ⟶ Y),
  F.map (r • f) = r • F.map f
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- A `WeierstrassCurve` is in normal form of characteristic = 3 and j ≠ 0, if its
`a₁, a₃, a₄ = 0`. In other words it is `Y² = X³ + a₂X² + a₆`.  -/
WeierstrassCurve.IsCharThreeJNeZeroNF : {R : Type u_1} → [CommRing R] → WeierstrassCurve R → Prop
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CtorInfo.ssize : Lean.Compiler.LCNF.CtorInfo → ℕ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.Faithful.mapGrp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [F.Faithful], F.mapGrp.Faithful
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      k ∉ t → (f (Std.DTreeMap.Raw.Const.get? t k)).isNone = true → (Std.DTreeMap.Raw.Const.alter t k f).size = t.size
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.inv.eq_1 : ∀ {G : Type u_2} [inst : Group G],
  Submonoid.inv = { inv := fun S => { carrier := (↑S)⁻¹, mul_mem' := ⋯, one_mem' := ⋯ } }
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.toCostructuredArrow'_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (d : D) (X : (CategoryTheory.StructuredArrow (Opposite.op d) F.op)ᵒᵖ),
  (CategoryTheory.StructuredArrow.toCostructuredArrow' F d).obj X =
    CategoryTheory.CostructuredArrow.mk (Opposite.unop X).hom.unop
-- Mathlib.Order.SupClosed
infClosure_mono : ∀ {α : Type u_3} [inst : SemilatticeInf α], Monotone ⇑infClosure
-- Mathlib.CategoryTheory.FinCategory.Basic
/-- Applying `ULift` to morphisms and objects of a category preserves finiteness.  -/
CategoryTheory.finCategoryUlift : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.FinCategory J] → CategoryTheory.FinCategory (CategoryTheory.ULiftHom (ULift.{w, v} J))
-- Lean.Data.Array
/-- Compares each element of an array with all later elements using `f`. For each comparison, `f`
determines whether to keep both of its arguments. If `f` returns `false` for an argument, that
argument is removed from the array and does not participate in subsequent comparisons. Those
elements that were not discarded are returned.

This can be used to remove elements from an array where a “better” element, in some partial order,
exists in the array.

Example:
```lean example
#eval #["a", "r", "red", "x", "r"].filterPairsM fun x y =>
  pure (!(x.isPrefixOf y), true)
```
```output
#["a", "red", "x", "r"]
```
 -/
Lean.Array.filterPairsM : {m : Type → Type u_1} → [Monad m] → {α : Type} → Array α → (α → α → m (Bool × Bool)) → m (Array α)
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_I : ∀ {K : Type u_1} [inst : RCLike K], (starRingEnd K) RCLike.I = -RCLike.I
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivWithinAt_singleton : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E → F) (x : E), HasFDerivWithinAt f 0 {x} x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.Subcomplex.N.mk.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} {n : ℕ} (x x_1 : X.obj (Opposite.op { len := n })) (e_x : x = x_1)
  (hx : x ∈ X.nonDegenerate n) (hx' : x ∉ A.obj (Opposite.op { len := n })),
  SSet.Subcomplex.N.mk x hx hx' = SSet.Subcomplex.N.mk x_1 ⋯ ⋯
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.ennreal_toReal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ENNReal}, Measurable f → Measurable fun x => (f x).toReal
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instToJsonPublishDiagnosticsParams : Lean.ToJson Lean.Lsp.PublishDiagnosticsParams
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.eq_d₁₂_comp_inv_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ((Fin 2 → G) → ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₁ A).inv
      (CategoryTheory.CategoryStruct.comp
        (CochainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) → ↑A)) (fun n => inhomogeneousCochains.d A n) 1 2)
        h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.d₁₂ A)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₂ A).inv h)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.zero_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (p q : ℤ) (hpq : p + n = q), CochainComplex.HomComplex.Cochain.v 0 p q hpq = 0
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- The substitution `y = x ^ p` in integrals over `Ioi 0` preserves integrability.  -/
MeasureTheory.integrableOn_Ioi_comp_rpow_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) {p : ℝ},
  p ≠ 0 →
    (MeasureTheory.IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Set.Ioi 0) MeasureTheory.volume ↔
      MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.eq_ones_iff_le_length : ∀ {n : ℕ} {c : Composition n}, c = Composition.ones n ↔ n ≤ c.length
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.instInhabitedStrictOrLazy.default : {α β : Type} → [Inhabited α] → Lean.Widget.StrictOrLazy α β
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.brecOn.go : {pu : Lean.Compiler.LCNF.Purity} →
  {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u} →
    {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} →
      {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u} →
        {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} →
          {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u} →
            {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} →
              (t : Lean.Compiler.LCNF.FunDecl pu) →
                ((t : Lean.Compiler.LCNF.Alt pu) → t.below → motive_1 t) →
                  ((t : Lean.Compiler.LCNF.FunDecl pu) → t.below → motive_2 t) →
                    ((t : Lean.Compiler.LCNF.Cases pu) → t.below → motive_3 t) →
                      ((t : Lean.Compiler.LCNF.Code pu) → t.below → motive_4 t) →
                        ((t : Array (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_1 t → motive_5 t) →
                          ((t : List (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_2 t → motive_6 t) →
                            motive_2 t ×' t.below
-- Mathlib.Algebra.Ring.Int.Parity
Int.odd_pow : ∀ {m : ℤ} {n : ℕ}, Odd (m ^ n) ↔ Odd m ∨ n = 0
-- Mathlib.Algebra.Order.Group.Cone
GroupConeClass.mk : ∀ {S : Type u_1} {G : outParam (Type u_2)} [inst : CommGroup G] [inst_1 : SetLike S G]
  [toSubmonoidClass : SubmonoidClass S G], (∀ {C : S} {a : G}, a ∈ C → a⁻¹ ∈ C → a = 1) → GroupConeClass S G
-- Lean.Expr
Lean.Int.mkInstMul : Lean.Expr
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.comp_hom : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G H : CategoryTheory.SingleFunctors C D A} (f : F ⟶ G) (g : G ⟶ H) (a : A),
  (CategoryTheory.CategoryStruct.comp f g).hom a = CategoryTheory.CategoryStruct.comp (f.hom a) (g.hom a)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.isoOfComponents.congr_simp : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f f_1 : (i : ι) → C₁.X i ≅ C₂.X i) (e_f : f = f_1)
  (hf :
    ∀ (i j : ι),
      c.Rel i j →
        CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) =
          CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom),
  HomologicalComplex.Hom.isoOfComponents f hf = HomologicalComplex.Hom.isoOfComponents f_1 ⋯
-- Mathlib.Data.DFinsupp.Module
DFinsupp.comapDomain'_smul : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)]
  [inst_1 : (i : ι) → SMulZeroClass γ (β i)] (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) (r : γ)
  (f : Π₀ (i : ι), β i), DFinsupp.comapDomain' h hh' (r • f) = r • DFinsupp.comapDomain' h hh' f
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.integrable_llr_tilted_left : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable f μ →
      MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
        MeasureTheory.Integrable (fun x => Real.exp (f x)) μ →
          AEMeasurable f ν → MeasureTheory.Integrable (MeasureTheory.llr (μ.tilted f) ν) μ
-- Batteries.Data.List.Lemmas
List.replaceFTR.go.match_1.congr_eq_1 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (x : List α) (x_1 : Array α)
  (h_1 : (acc : Array α) → motive [] acc) (h_2 : (x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc)
  (acc : Array α),
  x = [] →
    x_1 = acc →
      (match x, x_1 with
        | [], acc => h_1 acc
        | x :: xs, acc => h_2 x xs acc) ≍
        h_1 acc
-- Mathlib.CategoryTheory.Monoidal.Closed.Zero
/-- A Cartesian closed category with a zero object is equivalent to the category with one object and
one morphism.
 -/
CategoryTheory.equivPUnit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.MonoidalClosed C] →
        [CategoryTheory.Limits.HasZeroObject C] → C ≌ CategoryTheory.Discrete PUnit.{w + 1}
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- An abbreviation for `HasColimit (pair X Y)`.  -/
CategoryTheory.Limits.HasBinaryCoproduct : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → C → Prop
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets_precomp_of_bijective : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ι → Set (Set Ω)} {ι' : Type u_5} {g : ι' → ι},
  Function.Bijective g → (ProbabilityTheory.Kernel.iIndepSets (π ∘ g) κ μ ↔ ProbabilityTheory.Kernel.iIndepSets π κ μ)
-- Init.Data.SInt.Bitwise
Int64.ofBitVec_not : ∀ (a : BitVec 64), Int64.ofBitVec (~~~a) = ~~~Int64.ofBitVec a
-- Mathlib.Data.Rat.Lemmas
Rat.isSquare_ofNat_iff : ∀ {n : ℕ}, IsSquare (OfNat.ofNat n) ↔ IsSquare (OfNat.ofNat n)
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
deriv2_sqrt_mul_log : ∀ (x : ℝ), deriv^[2] (fun x => √x * Real.log x) x = -Real.log x / (4 * √x ^ 3)
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Connection.mk.inj : ∀ {tokens : Array String} {valid : tokens.all Std.Http.Internal.isToken = true} {tokens_1 : Array String}
  {valid_1 : tokens_1.all Std.Http.Internal.isToken = true},
  { tokens := tokens, valid := valid } = { tokens := tokens_1, valid := valid_1 } → tokens = tokens_1
-- Mathlib.Topology.Algebra.Group.Basic
IsCompact.inv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G] {s : Set G},
  IsCompact s → IsCompact s⁻¹
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.mk_sub_mk : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddGroup R] (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R),
  { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } - { re := b₁, imI := b₂, imJ := b₃, imK := b₄ } =
    { re := a₁ - b₁, imI := a₂ - b₂, imJ := a₃ - b₃, imK := a₄ - b₄ }
-- Mathlib.Data.Nat.Choose.Basic
_private.Mathlib.Data.Nat.Choose.Basic.0.Nat.choose.match_1.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (n : ℕ) (h_1 : (x : ℕ) → motive x 0) (h_2 : (n : ℕ) → motive 0 n.succ)
  (h_3 : (n k : ℕ) → motive n.succ k.succ),
  (match 0, n.succ with
    | x, 0 => h_1 x
    | 0, n.succ => h_2 n
    | n.succ, k.succ => h_3 n k) =
    h_2 n
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An induction principle for `FiniteArchimedeanClass`.  -/
FiniteArchimedeanClass.ind : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  {motive : FiniteArchimedeanClass M → Prop},
  (∀ (a : M) (ha : a ≠ 0), motive (FiniteArchimedeanClass.mk a ha)) → ∀ (x : FiniteArchimedeanClass M), motive x
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Std.Internal.Do.EStateM.wpInst.match_1.eq_1 : ∀ {ε σ α : Type} (motive : EStateM.Result ε σ α → Sort u_1) (a : α) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (el : ε) → (s' : σ) → motive (EStateM.Result.error el s')),
  (match EStateM.Result.ok a s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error el s' => h_2 el s') =
    h_1 a s'
-- Aesop.Tree.Data
Aesop.Rapp.originalSubgoals : Aesop.Rapp → Array Lean.MVarId
-- Mathlib.Algebra.Group.Basic
sub_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - b - c = a - (b + c)
-- Init.Data.Order.Ord
/-- A typeclass for types with a comparison function that satisfies `compare a b = .eq` if and only if
the logical equality `a = b` holds.

This typeclass distinguishes itself from `LawfulBEqOrd` by using logical equality (`=`) instead of
boolean equality (`==`).
 -/
Std.LawfulEqOrd : (α : Type u) → [Ord α] → Prop
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.colimit_add_mk_eq' : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat) {j : J} (x y : ↑(F.obj j)),
  AddGrpCat.FilteredColimits.G.mk F ⟨j, x⟩ + AddGrpCat.FilteredColimits.G.mk F ⟨j, y⟩ =
    AddGrpCat.FilteredColimits.G.mk F ⟨j, x + y⟩
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_eq_false_iff_exists_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.isEmpty = false ↔ ∃ a, a ∈ m
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.instDenumerable : Denumerable Nat.Partrec.Code
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsStrictRestriction.exists_eq_restrict : ∀ {α : Type u_1} {M N : Matroid α}, N.IsStrictRestriction M → ∃ R ⊂ M.E, N = M.restrict R
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
/-- `S` is separating, that is, `S ⊓ i S` is the trivial subspace.  -/
StandardSubspace.IsSeparating : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] (self : StandardSubspace H),
  self.toClosedSubmodule ⊓ self.toClosedSubmodule.mulI = ⊥
-- Init.Data.Repr
instReprRaw_1 : Repr Substring.Raw
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_mapRange : ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β₁ i)]
  [inst_2 : (i : ι) → Zero (β₂ i)] [inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)]
  [inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)] {f : (i : ι) → β₁ i → β₂ i} {hf : ∀ (i : ι), f i 0 = 0}
  {g : Π₀ (i : ι), β₁ i}, (DFinsupp.mapRange f hf g).support ⊆ g.support
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.iSup_eq_span' : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_9}
  (p : ι → Submodule R M) (h : ι → Prop), ⨆ i, ⨆ (_ : h i), p i = Submodule.span R (⋃ i, ⋃ (_ : h i), ↑(p i))
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.mem_succ_iff : ∀ {α : Type u} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α] {lo a : α},
  a ∈ (Std.PRange.succ lo)...* ↔ ∃ a', a = Std.PRange.succ a' ∧ a' ∈ lo...*
-- Mathlib.Algebra.Polynomial.Inductions
/-- `divX p` returns a polynomial `q` such that `q * X + C (p.coeff 0) = p`.
It can be used in a semiring where the usual division algorithm is not possible  -/
Polynomial.divX : {R : Type u} → [inst : Semiring R] → Polynomial R → Polynomial R
-- Mathlib.Topology.MetricSpace.Isometry
/-- See Note [custom simps projection]  -/
IsometryEquiv.Simps.symm_apply : {α : Type u} → {β : Type v} → [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → α ≃ᵢ β → β → α
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariation_zero : ∀ {X : Type u_1} [inst : MeasurableSpace X], MeasureTheory.preVariation 0 ⋯ ⋯ = 0
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.eq_empty_of_insertMany_eq_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} {ρ : Type w}
  [inst : ForIn Id ρ (α × β)] [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ}, m.insertMany l = ∅ → m = ∅
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.contDiffAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → s ∈ nhds x → ContDiffAt 𝕜 n f x
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
CategoryTheory.ShortComplex.exact_iff_exact_map_forget₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [(CategoryTheory.forget₂ C Ab).PreservesHomology]
  (S : CategoryTheory.ShortComplex C) [S.HasHomology], S.Exact ↔ (S.map (CategoryTheory.forget₂ C Ab)).Exact
-- Mathlib.Order.Filter.Cofinite
/-- Every filter is the disjoint supremum of a principal filter and a free filter.  -/
exists_eq_principal_sup_free : ∀ {α : Type u_2} (f : Filter α),
  ∃ s, ∃ g ≤ Filter.cofinite, Disjoint (Filter.principal s) g ∧ f = Filter.principal s ⊔ g
-- Mathlib.Order.Hom.WithTopBot
WithBot.coeOrderHom.eq_1 : ∀ {α : Type u_4} [inst : Preorder α],
  WithBot.coeOrderHom =
    { toEmbedding := { toFun := WithBot.some, inj' := ⋯, map_rel_iff' := ⋯ }.toEmbedding, map_rel_iff' := ⋯ }
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false)
  {h : k ∈ m.insertMany l}, (m.insertMany l).getKey k h = m.getKey k ⋯