mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the
proof obligation in the statement of `get_insertIfNew`.  -/
Std.DTreeMap.Internal.Impl.mem_of_mem_insertIfNew' : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {v : β k},
  a ∈ (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl → ¬(compare k a = Ordering.eq ∧ k ∉ t) → a ∈ t
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
AlgebraicGeometry.pointEquivClosedPoint_apply_coe : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [inst_1 : IsAlgClosed K]
  (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [inst_2 : AlgebraicGeometry.LocallyOfFiniteType f]
  (p :
    { p //
      CategoryTheory.CategoryStruct.comp p f =
        CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of K)) }),
  ↑((AlgebraicGeometry.pointEquivClosedPoint f) p) = ↑p (IsLocalRing.closedPoint K)
-- Mathlib.Algebra.Order.Group.PosPart
posPart_min : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : AddGroup α] (a b : α), (a ⊓ b)⁺ = a⁺ ⊓ b⁺
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_id_unbop : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : Bᵒᵖ} {f : a ⟶ b},
  Bicategory.Opposite.op2 (CategoryTheory.CategoryStruct.id f.unop) = CategoryTheory.CategoryStruct.id f
-- Std.Do.SPred.SPred
Std.Do.SPred.conjunction.eq_1 : ∀ {σs : List (Type u)}, Std.Do.SPred.conjunction [] = ⌜True⌝
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instOrdOffset : Ord Std.Time.Hour.Offset
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.of_projective : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Projective R M], Module.Flat R M
-- Mathlib.Tactic.ClickSuggestions.FindPremises
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.Entries.mk.sizeOf_spec : ∀
  (rw :
    Array
      (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.RwLemma))
  (grw :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.GrwLemma))
  (app :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyLemma))
  (appAt :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyAtLemma)),
  sizeOf { rw := rw, grw := grw, app := app, appAt := appAt } = 1 + sizeOf rw + sizeOf grw + sizeOf app + sizeOf appAt
-- Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
properSpace_iff_isProperMap_dist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α], ProperSpace α ↔ ∀ (x : α), IsProperMap (dist x)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.LeftExactFunctor.forget_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : C ⥤ₗ D} (α : F ⟶ G), (CategoryTheory.LeftExactFunctor.forget C D).map α = α.hom
-- Init.Data.Int.Order
Int.le_sub_one_iff : ∀ {m n : ℤ}, m ≤ n - 1 ↔ m < n
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_exp_mul_I_eq_sinc : ∀ (r : ℝ), ∫ (t : ℝ) in -r..r, Complex.exp (↑t * Complex.I) = 2 * ↑r * ↑(Real.sinc r)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.directiveExpandersFor : Lean.Ident →
  Lean.Elab.TermElabM
    (Array
      (Lean.Name ×
        (Lean.TSyntaxArray `block →
          StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))))
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.toAdd_bot : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderBot α], Multiplicative.toAdd ⊥ = ⊥
-- Mathlib.Order.BooleanSubalgebra
/-- Two Boolean subalgebras are equal if they have the same elements.  -/
BooleanSubalgebra.ext : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L M : BooleanSubalgebra α}, (∀ (a : α), a ∈ L ↔ a ∈ M) → L = M
-- Mathlib.LinearAlgebra.Dimension.Constructions
rank_finsupp' : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Free R M] (ι : Type v), Module.rank R (ι →₀ M) = Cardinal.mk ι * Module.rank R M
-- Mathlib.Analysis.Calculus.AbsolutelyMonotone
/-- Under `UniqueDiffOn`, a Taylor witness for an absolutely monotone function agrees with
`iteratedDerivWithin`, so the latter is nonnegative on `s`.  -/
AbsolutelyMonotoneOn.iteratedDerivWithin_nonneg : ∀ {f : ℝ → ℝ} {s : Set ℝ},
  AbsolutelyMonotoneOn f s → UniqueDiffOn ℝ s → ∀ (n : ℕ) {x : ℝ}, x ∈ s → 0 ≤ iteratedDerivWithin n f s x
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.stoppedAbove_le : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ℕ → Ω → ℝ} {r : ℝ} {R : NNReal},
  0 ≤ r →
    f 0 = 0 →
      (∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) →
        ∀ (i : ℕ), ∀ᵐ (ω : Ω) ∂μ, MeasureTheory.stoppedAbove f r i ω ≤ r + ↑R
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `S` a finite-dimensional ring extension of a PID `R` which is free as an `R`-module,
then any nonzero `S`-ideal `I` is free as an `R`-submodule of `S`, and we can
find a basis for `S` and `I` such that the inclusion map is a square diagonal
matrix; this is the basis for `I`. See:
* `Ideal.ringBasis` for the basis on `S`,
* `Ideal.smithCoeffs` for the entries of the diagonal matrix
* `Ideal.selfBasis_def` for the proof that the inclusion map forms a square diagonal matrix.
 -/
Ideal.selfBasis : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      [IsDomain R] →
        [IsPrincipalIdealRing R] →
          {S : Type u_4} →
            [inst_3 : CommRing S] →
              [IsDomain S] →
                [inst_5 : Algebra R S] → [Finite ι] → Module.Basis ι R S → (I : Ideal S) → I ≠ ⊥ → Module.Basis ι R ↥I
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivAtFilter.const_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)} (c : F),
  HasDerivAtFilter f f' L → HasDerivAtFilter (fun x => c - f x) (-f') L
-- Mathlib.Algebra.Ring.Equiv
/-- The equivalence of multiplicative monoids underlying an equivalence of (semi)rings.  -/
RingEquiv.toMulEquiv : {R : Type u_7} →
  {S : Type u_8} → [inst : Mul R] → [inst_1 : Mul S] → [inst_2 : Add R] → [inst_3 : Add S] → R ≃+* S → R ≃* S
-- Init.Data.String.Basic
String.Pos.lt_cast_iff : ∀ {s t : String} {pos : t.Pos} {pos' : s.Pos} {h : s = t}, pos < pos'.cast h ↔ pos.cast ⋯ < pos'
-- Init.Data.Array.Lemmas
Array.sum_toList : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] {as : Array α}, as.toList.sum = as.sum
-- Mathlib.Order.Fin.Basic
Fin.rev_last_eq_bot : ∀ (n : ℕ), (Fin.last n).rev = ⊥
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub_intCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℤ), toIcoDiv hp (a - ↑m * p) b = toIcoDiv hp a b + m
-- Mathlib.Order.Filter.Prod
Filter.bot_coprod_bot : ∀ {α : Type u_1} {β : Type u_2}, ⊥.coprod ⊥ = ⊥
-- Mathlib.Logic.Equiv.Prod
Equiv.uniqueProd_symm_apply : ∀ {α : Type u_9} {β : Type u_10} [inst : Unique β] (x : α), (Equiv.uniqueProd α β).symm x = (default, x)
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.isometryEquiv_map_mkMetric : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] (m : ENNReal → ENNReal) (f : X ≃ᵢ Y),
  (MeasureTheory.OuterMeasure.map ⇑f) (MeasureTheory.OuterMeasure.mkMetric m) = MeasureTheory.OuterMeasure.mkMetric m
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β], Measurable Sum.inl
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.Nonsingular.pow : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n R}
  [IsCancelAdd R], A.Nonsingular → ∀ (k : ℕ), (A ^ k).Nonsingular
-- Std.Sync.Notify
Std.Notify.Consumer.normal : {α : Type} → IO.Promise α → Std.Notify.Consumer α
-- Mathlib.Topology.Gluing
/-- We may construct a glue data from a family of open sets.  -/
TopCat.GlueData.ofOpenSubsets : {α : Type u} → [inst : TopologicalSpace α] → {J : Type u} → (J → TopologicalSpace.Opens α) → TopCat.GlueData
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.Util.0.Int.Internal.Linear.Poly.eval?.go : Lean.PArray ℚ → ℚ → Int.Internal.Linear.Poly → Option ℚ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.inr_inl_pushoutAssoc_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄]
  [inst_4 :
    CategoryTheory.Limits.HasPushout g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))]
  {Z : C}
  (h :
    CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ g₂)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inl
          (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₃ g₄)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inr g₁
          (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
        h)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {he : t.isEmpty = false}, t.getKey! (t.minKey he) = t.minKey he
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
PartialEquiv.trans'.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e e_1 : PartialEquiv α β) (e_e : e = e_1) (e' e'_1 : PartialEquiv β γ)
  (e_e' : e' = e'_1) (h : e.target = e'.source), e.trans' e' h = e_1.trans' e'_1 ⋯
-- Mathlib.Data.NNReal.Basic
NNReal.image_coe_Icc : ∀ (x y : NNReal), NNReal.toReal '' Set.Icc x y = Set.Icc ↑x ↑y
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find the trivial model on an inner product space.  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromInnerProductSpace : Lean.Expr → Lean.Elab.TermElabM Manifold.Elab.FindModelResult
-- Lean.Parser.Extra
Lean.Parser.sepBy.parenthesizer : Lean.PrettyPrinter.Parenthesizer →
  String → Lean.PrettyPrinter.Parenthesizer → optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Ideal.Operations
Ideal.sup_prod_eq_top : ∀ {R : Type u} {ι : Type u_1} [inst : CommSemiring R] {I : Ideal R} {s : Finset ι} {J : ι → Ideal R},
  (∀ i ∈ s, I ⊔ J i = ⊤) → I ⊔ ∏ i ∈ s, J i = ⊤
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.norm_zero : ∀ {α : Type u_1} [inst : DecidableEq α], FreeAddGroup.norm 0 = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- `biproduct_comparison F f` is a split epimorphism.  -/
CategoryTheory.Functor.splitEpiBiproductComparison : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {J : Type w₁} →
              (F : CategoryTheory.Functor C D) →
                (f : J → C) →
                  [inst_4 : CategoryTheory.Limits.HasBiproduct f] →
                    [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] →
                      [F.PreservesZeroMorphisms] → CategoryTheory.SplitEpi (F.biproductComparison f)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_singularPart : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
  (μ.singularPart ν).singularPart ν = μ.singularPart ν
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- Goals targeted by the tactic  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.TacticData.goalsTargetedBy : Mathlib.Linter.Flexible.TacticData✝ → List Lean.MVarId
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.instDecidablePredMemSubgroupStabilizerOfDecidableEq : {G : Type u_1} →
  {α : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G α] → [DecidableEq α] → (a : α) → DecidablePred fun x => x ∈ MulAction.stabilizer G a
-- Mathlib.Order.LiminfLimsup
Filter.liminf_sdiff : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) [f.NeBot] (a : α),
  Filter.liminf u f \ a = Filter.liminf (fun b => u b \ a) f
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.lt_of_tendsto_zero_of_pos : ∀ {f : ℕ → ℝ}, Filter.Tendsto f Filter.atTop (nhds 0) → ∀ {r : ℝ}, 0 < r → Hyperreal.ofSeq f < ↑r
-- Mathlib.Order.CompleteLattice.Basic
iInf_mono : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f g : ι → α}, (∀ (i : ι), g i ≤ f i) → iInf g ≤ iInf f
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.toSignedMeasure.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α),
  j.toSignedMeasure = j.posPart.toSignedMeasure - j.negPart.toSignedMeasure
-- Mathlib.Tactic.NormNum.Result
/-- Represent an integer as a "raw" typed expression.

This uses `.lit (.natVal n)` internally to represent a natural number,
rather than the preferred `OfNat.ofNat` form.
We use this internally to avoid unnecessary typeclass searches.

This function is the inverse of `Expr.intLit!`.
 -/
Mathlib.Meta.NormNum.mkRawIntLit : ℤ → Q(ℤ)
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.neg_mem_addUnits : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M}, x ∈ S.addUnits → -x ∈ S.addUnits
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.instMonoModuleCatFShortComplexH0 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G),
  CategoryTheory.Mono (groupCohomology.shortComplexH0 A).f
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.finite_co_support_prod_mul : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : Semiring R] (s : HahnSeries.SummableFamily Γ R α)
  (t : HahnSeries.SummableFamily Γ R β) (g : Γ), Finite ↑{a | ((fun a => s a.1 * t a.2) a).coeff g ≠ 0}
-- Lean.Compiler.IR.Format
Lean.IR.formatFnBody : Lean.IR.FnBody → optParam ℕ 2 → Std.Format
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.mono : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R), Monotone ↑f
-- Mathlib.Algebra.Homology.ComplexShapeSigns
TotalComplexShape.ε₂_ε₁ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  {c₁₂ : ComplexShape I₁₂} [self : TotalComplexShape c₁ c₂ c₁₂] {i₁ i₁' : I₁} {i₂ i₂' : I₂},
  c₁.Rel i₁ i₁' →
    c₂.Rel i₂ i₂' →
      TotalComplexShape.ε₂ c₁ c₂ c₁₂ (i₁, i₂) * TotalComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂') =
        -TotalComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂) * TotalComplexShape.ε₂ c₁ c₂ c₁₂ (i₁', i₂)
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_hom_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) (a : Bᵒᵖ) (X : Opposite.unop a ⟶ x),
  ((CategoryTheory.Bicategory.yoneda.obj x).mapId a).hom.toNatTrans.app X = (CategoryTheory.Bicategory.leftUnitor X).hom
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv_comp : ∀ {𝕜 : 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} {g : M → 𝕜} (x : M'),
  MDiffAt g (f x) → MDiffAt f x → d% (g ∘ f) x = d% g (f x) ∘SL mfderiv% f x
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort_k : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.symm : ∀ {p q r : ℝ}, p.HolderTriple q r → q.HolderTriple p r
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.encode : Mathlib.Deriving.Encodable.S✝ → ℕ
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
AlgebraicGeometry.pointOfClosedPoint.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [inst_1 : IsAlgClosed K]
  (f f_1 : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) (e_f : f = f_1)
  [inst_2 : AlgebraicGeometry.LocallyOfFiniteType f] (x x_1 : ↥X) (e_x : x = x_1) (hx : IsClosed {x}),
  AlgebraicGeometry.pointOfClosedPoint f x hx = AlgebraicGeometry.pointOfClosedPoint f_1 x_1 ⋯
-- Mathlib.RingTheory.RingHom.Locally
/-- If `P` is preserved by localizations and stable under composition with localization
away maps, then `Locally P` is a local property of ring homomorphisms.  -/
RingHom.locally_propertyIsLocal : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P) →
      RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] =>
        RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P
-- Init.Data.List.Lemmas
List.get_cons_zero : ∀ {α : Type u_1} {a : α} {l : List α}, (a :: l).get 0 = a
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosed.exists_algebraMap_eq_of_pow_mem_subalgebra : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_4} [inst_1 : CommRing K] [inst_2 : Algebra R K] {S : Subalgebra R K}
  [IsIntegrallyClosed ↥S] [IsFractionRing (↥S) K] {x : K} {n : ℕ}, 0 < n → x ^ n ∈ S → ∃ y, (algebraMap (↥S) K) y = x
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
CategoryTheory.Abelian.Ext.linearEquiv₀_symm_apply : ∀ {R : Type t} [inst : Ring R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : CategoryTheory.HasExt C] {X Y : C}
  (a : X ⟶ Y), CategoryTheory.Abelian.Ext.linearEquiv₀.symm a = CategoryTheory.Abelian.Ext.mk₀ a
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factorSetMem_eq_mem : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] (p : Associates α) (s : Associates.FactorSet α),
  Associates.FactorSetMem s p = (p ∈ s)
-- Mathlib.Algebra.Homology.AlternatingConst
/-- `alternatingConst.obj X` is homotopy equivalent to the chain
complex `(single₀ C).obj X`.  -/
ChainComplex.alternatingConstHomotopyEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        (X : C) → HomotopyEquiv (ChainComplex.alternatingConst.obj X) ((ChainComplex.single₀ C).obj X)
-- Mathlib.CategoryTheory.Category.PartialFun
typeToPartialFunIsoPartialFunToPointed_hom_app_toFun : ∀ (X : Type u_1) (a : ((typeToPartialFun.comp partialFunToPointed).obj X).X),
  (typeToPartialFunIsoPartialFunToPointed.hom.app X).toFun a = a
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function is analytic within a set with unique differentials, then so is its derivative.
Note that this theorem does not require completeness of the space.  -/
AnalyticOn.fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E}, AnalyticOn 𝕜 f s → UniqueDiffOn 𝕜 s → AnalyticOn 𝕜 (fderivWithin 𝕜 f s) s
-- Init.Data.Nat.Dvd
Nat.dvd_mul_left : ∀ (a b : ℕ), a ∣ b * a
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
one_mem_posTangentConeAt_iff_frequently : ∀ {s : Set ℝ} {a : ℝ}, 1 ∈ posTangentConeAt s a ↔ ∃ᶠ (x : ℝ) in nhdsWithin a (Set.Ioi a), x ∈ s
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
WithCStarModule.equiv.eq_1 : ∀ (A : Type u_3) (E : Type u_4), WithCStarModule.equiv A E = Equiv.refl (WithCStarModule A E)
-- Mathlib.Algebra.Group.Defs
InvOneClass.mk : {G : Type u_2} → [toOne : One G] → [toInv : Inv G] → 1⁻¹ = 1 → InvOneClass G
-- Mathlib.CategoryTheory.Comma.Final
/-- `Comma L R` with `L : A ⥤ T` and `R : B ⥤ T` is connected if `L` is initial and `B` is
connected.  -/
CategoryTheory.Comma.isConnected_comma_of_initial : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [CategoryTheory.IsConnected B] [L.Initial],
  CategoryTheory.IsConnected (CategoryTheory.Comma L R)
-- Mathlib.Algebra.Group.Ideal
AddSemigroupIdeal.closure.eq_1 : ∀ {M : Type u_1} [inst : Add M] (s : Set M), AddSemigroupIdeal.closure s = SubAddAction.closure M s
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Constructs `∃ f₁ f₂ ... fₙ, body`, where `[f₁, ..., fₙ] = fvars`.  -/
ExistsAndEq.mkNestedExists : List ExistsAndEq.VarQ → Q(Prop) → Lean.MetaM Q(Prop)
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered additive monoids M, N, the natural projection
ordered homomorphism from M × N to M.  -/
OrderAddMonoidHom.fst : (α : Type u_1) →
  (β : Type u_2) →
    [inst : AddMonoid α] → [inst_1 : PartialOrder α] → [inst_2 : AddMonoid β] → [inst_3 : Preorder β] → α × β →+o α
-- Mathlib.Topology.NhdsWithin
nhdsSetWithin_mono_right : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t t' : Set α}, t ⊆ t' → nhdsSetWithin s t ≤ nhdsSetWithin s t'
-- Lean.Declaration
Lean.instInhabitedReducibilityHints.default : Lean.ReducibilityHints
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- The determinant of a unit matrix is itself a unit.  -/
Matrix.GeneralLinearGroup.det : {n : Type u} → [inst : DecidableEq n] → [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → GL n R →* Rˣ
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.toLinearMap_ofTop : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p : Submodule R M) {h : p = ⊤}, ↑(LinearEquiv.ofTop p h) = p.subtype
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.homMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (A B : CategoryTheory.Pretriangulated.Triangle C) (hom₁ hom₁_1 : A.obj₁ ⟶ B.obj₁) (e_hom₁ : hom₁ = hom₁_1)
  (hom₂ hom₂_1 : A.obj₂ ⟶ B.obj₂) (e_hom₂ : hom₂ = hom₂_1) (hom₃ hom₃_1 : A.obj₃ ⟶ B.obj₃) (e_hom₃ : hom₃ = hom₃_1)
  (comm₁ : CategoryTheory.CategoryStruct.comp A.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ B.mor₁)
  (comm₂ : CategoryTheory.CategoryStruct.comp A.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ B.mor₂)
  (comm₃ :
    CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) =
      CategoryTheory.CategoryStruct.comp hom₃ B.mor₃),
  A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃ = A.homMk B hom₁_1 hom₂_1 hom₃_1 ⋯ ⋯ ⋯