mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Int.Parity
Int.even_add' : ∀ {m n : ℤ}, Even (m + n) ↔ (Odd m ↔ Odd n)
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.coeHom_injective : ∀ {M : Type u} [inst : AddMonoid M], Function.Injective ⇑(AddUnits.coeHom M)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.glueMorphisms.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.Scheme} (f f_1 : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y)
  (e_f : f = f_1)
  (hf :
    ∀ (x y : 𝒰.I₀),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (f x) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) (f y)),
  AlgebraicGeometry.Scheme.Cover.glueMorphisms 𝒰 f hf = AlgebraicGeometry.Scheme.Cover.glueMorphisms 𝒰 f_1 ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Yoneda
/-- Naturally in `X`, we have `Hom(YX, colim_i Fi) ≅ colim_i Hom(YX, Fi)`.  -/
CategoryTheory.yonedaYonedaColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J (Type v₁)] →
          [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J (Type (max u₁ v₁))] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor Cᵒᵖ (Type v₁))) →
              CategoryTheory.yoneda.op.comp (CategoryTheory.yoneda.obj (CategoryTheory.Limits.colimit F)) ≅
                CategoryTheory.yoneda.op.comp (CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda))
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_mul : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
  A.adjugate * A = A.det • 1
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.prod_apply : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  [inst_5 : (x : B) → Zero (E₁ x)] [inst_6 : (x : B) → Zero (E₂ x)]
  (a : Bundle.TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x), ↑(e₁.prod e₂) a = Bundle.Trivialization.Prod.toFun' e₁ e₂ a
-- Mathlib.Analysis.MeanInequalities
/-- **Weighted Hölder inequality**.  -/
NNReal.inner_le_weight_mul_Lp : ∀ {ι : Type u} (s : Finset ι) {p : ℝ},
  1 ≤ p → ∀ (w f : ι → NNReal), ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
-- Lean.CoreM
/-- If set (when `showPartialSyntaxErrors` is not set and parsing failed), suppresses most elaboration
errors; see also `logMessage` below.
 -/
Lean.Core.Context.suppressElabErrors : Lean.Core.Context → Bool
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
HomotopicalAlgebra.IsFibrant.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] (X X_1 : C),
  X = X_1 → HomotopicalAlgebra.IsFibrant X = HomotopicalAlgebra.IsFibrant X_1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.startsWith_bool_eq_false_iff_get : ∀ {p : Char → Bool} {s : String}, s.startsWith p = false ↔ ∀ (h : s.startPos ≠ s.endPos), p (s.startPos.get h) = false
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.inr_zeroCoprodIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.zeroCoprodIso X).hom =
    CategoryTheory.CategoryStruct.id X
-- Lean.Elab.ComputedFields
/-- Marks a function as a computed field of an inductive.

Computed fields are specified in the with-block of an inductive type declaration. They can be used
to allow certain values to be computed only once at the time of construction and then later be
accessed immediately.

Example:
```
inductive NatList where
  | nil
  | cons : Nat → NatList → NatList
with
  @[computed_field] sum : NatList → Nat
  | .nil => 0
  | .cons x l => x + l.sum
  @[computed_field] length : NatList → Nat
  | .nil => 0
  | .cons _ l => l.length + 1
```
 -/
Lean.Elab.ComputedFields.computedFieldAttr : Lean.TagAttribute
-- Init.Data.BitVec.Lemmas
BitVec.concat_and_concat : ∀ {w : ℕ} (x y : BitVec w) (a b : Bool), x.concat a &&& y.concat b = (x &&& y).concat (a && b)
-- Mathlib.Probability.Distributions.Exponential
/-- The CDF of the exponential distribution equals ``1 - exp (-(r * x))``  -/
ProbabilityTheory.cdf_expMeasure_eq : ∀ {r : ℝ},
  0 < r →
    ∀ (x : ℝ),
      ↑(ProbabilityTheory.cdf (ProbabilityTheory.expMeasure r)) x = if 0 ≤ x then 1 - Real.exp (-(r * x)) else 0
-- Mathlib.Algebra.Notation.Defs
sub_ite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Sub α] (a b c : α),
  (a - if P then b else c) = if P then a - b else a - c
-- Mathlib.Topology.Constructions.SumProd
/-- Sum of two homeomorphisms.  -/
Homeomorph.sumCongr : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {X' : Type u_5} →
          {Y' : Type u_6} →
            [inst_2 : TopologicalSpace X'] → [inst_3 : TopologicalSpace Y'] → X ≃ₜ X' → Y ≃ₜ Y' → X ⊕ Y ≃ₜ X' ⊕ Y'
-- Mathlib.Algebra.Ring.NonZeroDivisors
mul_cancel_right_coe_nonZeroDivisors : ∀ {R : Type u_1} [inst : Ring R] {x y : R} {c : ↥(nonZeroDivisors R)}, x * ↑c = y * ↑c ↔ x = y
-- Mathlib.Data.Fintype.Pi
Finset.Nonempty.piFinset_const : ∀ {β : Type u_2} {ι : Type u_5} [inst : Fintype ι] [inst_1 : DecidableEq ι] {s : Finset β},
  s.Nonempty → (Fintype.piFinset fun x => s).Nonempty
-- Mathlib.Combinatorics.Enumerative.Composition
List.getElem_splitWrtCompositionAux : ∀ {α : Type u_1} (l : List α) (ns : List ℕ) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
  (l.splitWrtCompositionAux ns)[i] = List.drop (List.take i ns).sum (List.take (List.take (i + 1) ns).sum l)
-- Std.Data.DHashMap.RawDef
Std.DHashMap.Raw.instForMSigmaOfMonad : {α : Type u} → {β : α → Type v} → {m : Type w → Type w'} → [Monad m] → ForM m (Std.DHashMap.Raw α β) ((a : α) × β a)
-- Mathlib.CategoryTheory.Abelian.Transfer
CategoryTheory.ShrinkHoms.instAdditiveInverse : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.LocallySmall.{w, v_1, u_1} C]
  [inst_2 : CategoryTheory.Preadditive C], (CategoryTheory.ShrinkHoms.inverse C).Additive
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.Finite.smul_set : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set β} {a : α}, s.Finite → (a • s).Finite
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.comap_upperCentralSeries_quotient_center : ∀ {G : Type u_1} [inst : AddGroup G] (n : ℕ),
  AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.center G))
      (AddSubgroup.upperCentralSeries (G ⧸ AddSubgroup.center G) n) =
    AddSubgroup.upperCentralSeries G n.succ
-- Mathlib.Algebra.Order.Group.Unbundled.Int
abs_zsmul_eq_zero : ∀ {G : Type u_1} [inst : AddGroup G] (a : G) (n : ℤ), |n| • a = 0 ↔ n • a = 0
-- Mathlib.Algebra.Module.Submodule.Union
/-- A convenience variation of `Module.Dual.exists_forall_ne_zero_of_forall_exists` where we are
concerned only about behaviour on a fixed submodule.  -/
Module.Dual.exists_forall_mem_ne_zero_of_forall_exists : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [Finite ι] [Infinite K] (p : Submodule K M) (f : ι → Module.Dual K M),
  (∀ (i : ι), ∃ x ∈ p, (f i) x ≠ 0) → ∃ x ∈ p, ∀ (i : ι), (f i) x ≠ 0
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.ext : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} (α β : CategoryTheory.BasedNatTrans F G),
  α.toNatTrans = β.toNatTrans → α = β
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.prod_singleton : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (x : M i) (hne_one : x ≠ 1),
  (Monoid.CoprodI.NeWord.singleton x hne_one).prod = Monoid.CoprodI.of x
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConst.mk : Lean.AsyncConstantInfo → Option (Task (Array Lean.EnvExtensionState)) → Task Dynamic → Bool → Lean.AsyncConst✝
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `t : Cocone F` is a colimit cocone if and only if `t.op : Cone F.op` is a limit cone.
 -/
CategoryTheory.Limits.isColimitEquivIsLimitOp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} → CategoryTheory.Limits.IsColimit t ≃ CategoryTheory.Limits.IsLimit t.op
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.scMap_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i : ℕ)
  (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.scMap._auto_1),
  (CategoryTheory.ComposableArrows.scMap φ h₁ h₂ i hi).τ₁ = φ.app ⟨i, ⋯⟩
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_eq_liminf_sum_nat : ∀ {f : ℕ → ENNReal}, ∑' (i : ℕ), f i = Filter.liminf (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop
-- Mathlib.Combinatorics.Hall.Basic
hallMatchingsOn.eq_1 : ∀ {ι : Type u} {α : Type v} (t : ι → Finset α) (ι' : Finset ι),
  hallMatchingsOn t ι' = {f | Function.Injective f ∧ ∀ (x : ↥ι'), f x ∈ t ↑x}
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.toLipschitzWith : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α}, ContractingWith K f → LipschitzWith K f
-- Mathlib.Data.Nat.Multiplicity
Nat.Prime.dvd_choose_pow_iff : ∀ {p n k : ℕ}, Nat.Prime p → (p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n)
-- Mathlib.LinearAlgebra.Transvection.Generation
LinearEquiv.sup_span_singleton_lt_top : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] {W : Submodule K V} (v : V), 1 < Module.finrank K (V ⧸ W) → W ⊔ K ∙ v < ⊤
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.tensorObj.instTensorObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        {G H : C} →
          [CategoryTheory.AddGrpObj G] →
            [CategoryTheory.AddGrpObj H] →
              CategoryTheory.AddGrpObj (CategoryTheory.MonoidalCategoryStruct.tensorObj G H)
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.candidatesB.eq_1 : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : MetricSpace Y],
  GromovHausdorff.candidatesB✝ X Y = {f | ⇑f ∈ GromovHausdorff.candidates X Y}
-- Mathlib.Order.Heyting.Hom
CoheytingHom.id_apply : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), (CoheytingHom.id α) a = a
-- Aesop.Util.EqualUpToIds
Aesop.tacticStatesEqualUpToIds' : Option Lean.MetavarContext →
  Lean.MetavarContext →
    Lean.MetavarContext →
      Array Lean.MVarId → Array Lean.MVarId → optParam Bool false → Lean.MetaM (Bool × Aesop.EqualUpToIdsM.State)
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_nonneg : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : Zero M] {s : Set α} {f : α → M},
  (∀ a ∈ s, 0 ≤ f a) → ∀ (a : α), 0 ≤ s.indicator f a
-- Mathlib.Data.Finsupp.MonomialOrder
/-- `syn` is a well ordering  -/
MonomialOrder.wellFoundedLT_syn : ∀ {σ : Type u_1} (self : MonomialOrder σ), WellFoundedLT self.syn
-- Mathlib.Data.Int.Bitwise
Int.testBit_bitwise : ∀ (f : Bool → Bool → Bool) (m n : ℤ) (k : ℕ), (Int.bitwise f m n).testBit k = f (m.testBit k) (n.testBit k)
-- Mathlib.Analysis.Calculus.Deriv.Inverse
/-- If a function frequently (in `𝓝[s ∖ {x}] x`) takes values in a set `t` that does not
accumulate at `f x`, then its derivative within `s` at `x` equals zero,
either because it has derivative zero or because it isn't differentiable at this point.  -/
derivWithin_zero_of_frequently_mem : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} (t : Set F),
  ¬AccPt (f x) (Filter.principal t) → (∃ᶠ (y : 𝕜) in nhdsWithin x (s \ {x}), f y ∈ t) → derivWithin f s x = 0
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.instSubtypeMemSubgroupTop : ∀ {G : Type u_1} [inst : Group G] [Group.IsPerfect G], Group.IsPerfect ↥⊤
-- Init.Data.Iterators.Lemmas.Combinators.Take
Std.Iter.toTake_eq_toIter_toTake_toIterM : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.toTake = it.toIterM.toTake.toIter
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.mulOneClass.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst_1 : One M₂] [inst_2 : MulOneClass M₁] (f : M₁ → M₂)
  (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y),
  Function.Surjective.mulOneClass f hf one mul = { toOne := inst_1, toMul := inst, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.toIsOrderedAddMonoid : ∀ {α : Type u_3} [self : LinearOrderedAddCommGroupWithTop α], IsOrderedAddMonoid α
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.mk : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (obj : C → D → Type w) →
          (map : {X X' : C} → {Y Y' : D} → (X ⟶ X') → (Y ⟶ Y') → (obj X Y' ⟶ obj X' Y)) →
            autoParam
                (∀ (X : C) (Y : D),
                  map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) =
                    CategoryTheory.CategoryStruct.id (obj X Y))
                CategoryTheory.ProfunctorCore.map_id._autoParam →
              autoParam
                  (∀ {X₁ X₂ X₃ : C} {Y₁ Y₂ Y₃ : D} (f : X₁ ⟶ X₂) (f' : X₂ ⟶ X₃) (g : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃),
                    map (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g') =
                      CategoryTheory.CategoryStruct.comp (map f g') (map f' g))
                  CategoryTheory.ProfunctorCore.map_comp._autoParam →
                CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_div_const_Icc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => x / a) '' Set.Icc b c = Set.Icc (b / a) (c / a)
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.conv_smul_left : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] (μ ν : MeasureTheory.Measure M)
  [MeasureTheory.SFinite ν] (s : ENNReal), (s • μ).conv ν = s • μ.conv ν
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instVAddCommClass'' : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst_1 : VAdd N α] [VAddCommClass M N α],
  VAddCommClass M N (Lex α)
-- Mathlib.GroupTheory.Sylow
Sylow.mk : {p : ℕ} →
  {G : Type u_1} →
    [inst : Group G] →
      (toSubgroup : Subgroup G) →
        IsPGroup p ↥toSubgroup → (∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup ≤ Q → Q = toSubgroup) → Sylow p G
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.sum_integral_adjacent_intervals : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ}
  {a : ℕ → ℝ} {n : ℕ},
  (∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.range n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a 0..a n, f x ∂μ
-- Mathlib.Computability.RecursiveIn
/-- A partial function `f : α →. σ` between `Primcodable` types is recursive in a set of oracles
`O` if its encoding as a function `ℕ →. ℕ` is `Nat.RecursiveIn O`.  -/
RecursiveIn : {α : Type u_5} → {σ : Type u_6} → [Primcodable α] → [Primcodable σ] → Set (ℕ →. ℕ) → (α →. σ) → Prop
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt : ∀ {𝕜 : 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'} {x : M} {s : Set M},
  MDiffAt[s] f x ↔ ∃ f', HasMFDerivAt[s] f x f'
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.dvd_mul_leadingCoeff_inv : ∀ {K : Type u_1} [inst : DivisionRing K] {p q : Polynomial K}, p ≠ 0 → (q ∣ p * Polynomial.C p.leadingCoeff⁻¹ ↔ q ∣ p)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.ofTop_symm_apply_coe : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {s₁ : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s₁] (h : s₁ = ⊤) (x : P), ↑((AffineIsometryEquiv.ofTop s₁ h).symm x) = x
-- Batteries.Data.UnionFind.Basic
/-- Equivalence relation from a `UnionFind` structure  -/
Batteries.UnionFind.Equiv : Batteries.UnionFind → ℕ → ℕ → Prop
-- Mathlib.CategoryTheory.GradedObject
/-- Given maps `p : I → J`, `q : J → K` and `r : I → K` such that `q.comp p = r`,
`X : GradedObject I C`, `k : K`, the cofan constructed by `cofanMapObjComp` is a colimit.
In other words, if we have, for all `j : J` such that `hj : q j = k`,
a colimit cofan `c j hj` which computes the coproduct of the `X i` such that `p i = j`,
and also a colimit cofan which computes the coproduct of the points of these `c j hj`, then
the point of this latter cofan computes the coproduct of the `X i` such that `r i = k`.  -/
CategoryTheory.GradedObject.isColimitCofanMapObjComp : {I : Type u_1} →
  {J : Type u_2} →
    {K : Type u_3} →
      {C : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_4} C] →
          (X : CategoryTheory.GradedObject I C) →
            (p : I → J) →
              (q : J → K) →
                (r : I → K) →
                  (hpqr : ∀ (i : I), q (p i) = r i) →
                    (k : K) →
                      (c : (j : J) → q j = k → X.CofanMapObjFun p j) →
                        ((j : J) → (hj : q j = k) → CategoryTheory.Limits.IsColimit (c j hj)) →
                          (c' : CategoryTheory.Limits.Cofan fun j => (c ↑j ⋯).pt) →
                            CategoryTheory.Limits.IsColimit c' →
                              CategoryTheory.Limits.IsColimit (X.cofanMapObjComp p q r hpqr k c c')
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.coreOfNat.injEq : ∀ (e : Lean.Expr) (natStructId : ℕ) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) (e_1 : Lean.Expr)
  (natStructId_1 : ℕ) (lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.coreOfNat e natStructId lhs rhs =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.coreOfNat e_1 natStructId_1 lhs_1 rhs_1) =
    (e = e_1 ∧ natStructId = natStructId_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_sdiff_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ico a b \ Set.Iio c = Set.Ico (max a c) b
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_freeOn : ∀ {α : Type u_1} (X : Set α), (Matroid.freeOn X).eRank = X.encard
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : DecidableEq β] {f : α → β}, Finset.image f 1 = {f 1}
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.hom_comp : ∀ (R : Type u) [inst : CommRing R] {A B C : AlgCat R} (f : A ⟶ B) (g : B ⟶ C),
  AlgCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (AlgCat.Hom.hom g).comp (AlgCat.Hom.hom f)
-- Mathlib.RingTheory.MvPolynomial.Groebner
MonomialOrder.degree_reduce_lt : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {f b : MvPolynomial σ R}
  (hb : IsUnit (m.leadingCoeff b)),
  m.degree b ≤ m.degree f → m.degree f ≠ 0 → m.toSyn (m.degree (m.reduce hb f)) < m.toSyn (m.degree f)
-- Mathlib.Tactic.Abel
/-- A cleanup routine, which simplifies expressions in `abel` normal form to a more human-friendly
format.  -/
Mathlib.Tactic.Abel.cleanup : Mathlib.Tactic.Abel.AbelNF.Config → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Probability.CDF
ProbabilityTheory.ofReal_cdf : ∀ (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (x : ℝ),
  ENNReal.ofReal (↑(ProbabilityTheory.cdf μ) x) = μ (Set.Iic x)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.Nondegenerate.toMatrix : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] {ι : Type u_6}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {B : LinearMap.BilinForm R₂ M₂},
  B.Nondegenerate → ∀ (b : Module.Basis ι R₂ M₂), ((LinearMap.BilinForm.toMatrix b) B).Nondegenerate
-- Init.Data.Array.Lemmas
Array.mem_of_getElem : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {h : i < xs.size} {a : α}, xs[i] = a → a ∈ xs
-- Lean.Meta.WHNF
/-- Auxiliary function for reducing `Quot.lift` and `Quot.ind` applications.  -/
_private.Lean.Meta.WHNF.0.Lean.Meta.reduceQuotRec : {α : Type} → Lean.QuotVal → Array Lean.Expr → (Unit → Lean.MetaM α) → (Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Aesop.Util.Basic
Aesop.lBoolOr : Lean.LBool → Lean.LBool → Lean.LBool
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.baseChange.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u_1}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] (P : Algebra.Extension R S),
  P.baseChange =
    { Ring := TensorProduct R T P.Ring,
      commRing :=
        (Algebra.Extension.ofSurjective (Algebra.TensorProduct.map (AlgHom.id T T) (IsScalarTower.toAlgHom R P.Ring S))
            ⋯).commRing,
      algebra₁ :=
        (Algebra.Extension.ofSurjective (Algebra.TensorProduct.map (AlgHom.id T T) (IsScalarTower.toAlgHom R P.Ring S))
            ⋯).algebra₁,
      algebra₂ :=
        (Algebra.Extension.ofSurjective (Algebra.TensorProduct.map (AlgHom.id T T) (IsScalarTower.toAlgHom R P.Ring S))
            ⋯).algebra₂,
      isScalarTower := ⋯,
      σ :=
        (Algebra.Extension.ofSurjective (Algebra.TensorProduct.map (AlgHom.id T T) (IsScalarTower.toAlgHom R P.Ring S))
            ⋯).σ,
      algebraMap_σ := ⋯ }
-- Lean.Attributes
Lean.isAttribute : Lean.Environment → Lean.Name → Bool
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.Ordinal.instOrdOfDay : Ord Std.Time.Nanosecond.Ordinal.OfDay
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.GMonoid.toGOne : {ι : Type u_1} → {A : ι → Type u_2} → {inst : AddMonoid ι} → [self : GradedMonoid.GMonoid A] → GradedMonoid.GOne A
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.Int32.toBitVec_cond : ∀ {c : Bool} {t e : Int32}, (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpEntry.thm : Lean.Meta.SimpTheorem → Lean.Meta.SimpEntry
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.inter_of_isOpen_isCompact : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X} [PrespectralSpace X] [QuasiSeparatedSpace X],
  Topology.IsLocallyConstructible s → IsOpen t → IsCompact t → Topology.IsConstructible (s ∩ t)