mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Basis
/-- From a basis `e : ι → M`, build a linear equivalence between families of vectors `v : ι → M`,
and matrices, making the matrix whose columns are the vectors `v i` written in the basis `e`.  -/
Module.Basis.toMatrixEquiv : {ι : Type u_1} →
  {R : Type u_5} →
    {M : Type u_6} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [Fintype ι] → Module.Basis ι R M → (ι → M) ≃ₗ[R] Matrix ι ι R
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.exists_mulVec_eq_zero_iff : ∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} [inst_1 : CommRing A] [IsDomain A] {M : Matrix n n A}
  [inst_3 : DecidableEq n], (∃ v, v ≠ 0 ∧ M.mulVec v = 0) ↔ M.det = 0
-- Mathlib.Analysis.Convex.Side
/-- If `x` and `y` are displaced from points of `s` by multiples of a common vector whose
coefficients have nonpositive product, they are weakly on opposite sides of `s`.  -/
AffineSubspace.wOppSide_of_vsub_eq_smul : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y p₁ p₂ : P} {m : V} {c₁ c₂ : R},
  p₁ ∈ s → p₂ ∈ s → x -ᵥ p₁ = c₁ • m → y -ᵥ p₂ = c₂ • m → c₁ * c₂ ≤ 0 → s.WOppSide x y
-- Init.Control.Id
/-- Runs a computation in the identity monad.

This function is the identity function. Because its parameter has type `Id α`, it causes
`do`-notation in its arguments to use the `Monad Id` instance.
 -/
Id.run : {α : Type u_1} → Id α → α
-- Mathlib.Data.Fin.SuccPred
Fin.val_sub_castPred_of_le : ∀ {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ Fin.last n) (h : b ≤ a), ↑(a.castPred ha - b.castPred ⋯) = ↑(a - b)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.not_nil : ¬Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg []
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
/-- Given a finite family of points `v` in a monoid `M`, together with a morphism into a
linearly-ordered monoid `f : M →* S`, the submonoid generated by those points of `v` which lie in
the "half space" where `f > 1` is generated by the subset of such points which are indecomposable
with respect to points in this half space.  -/
Submonoid.closure_image_isMulIndecomposable_baseOf : ∀ {ι : Type u_1} {M : Type u_2} {S : Type u_4} [inst : Monoid M] [inst_1 : LinearOrder S] [Finite ι]
  [inst_3 : CommMonoid S] [IsOrderedCancelMonoid S] (v : ι → M) (f : M →* S),
  Submonoid.closure (v '' IsMulIndecomposable.baseOf v f) = Submonoid.closure (v '' {i | 1 < f (v i)})
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₂Toδ₁' : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ),
  CategoryTheory.IsIso ((X'.H n₁).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀' i₁ i₂ i₃ hi₁₂ hi₂₃)) →
    CategoryTheory.IsIso ((X'.H n₂).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁' i₀ i₁ i₂ hi₀₁ hi₁₂)) →
      ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₂Toδ₁'._auto_1)
        (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isIso_mapFourδ₂Toδ₁'._auto_3),
        CategoryTheory.IsIso (X'.mapFourδ₂Toδ₁' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Topology.Compactification.StoneCech
eq_if_stoneCechUnit_eq : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [T2Space β] [CompactSpace β]
  {a b : α} {f : α → β}, Continuous f → stoneCechUnit a = stoneCechUnit b → f a = f b
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfLEArgs.min_eq : ∀ {α : Type u} (self : Std.Packages.LinearOrderOfLEArgs α),
  let this := self.le;
  let this_1 := self.decidableLE;
  let this_2 := self.min;
  ∀ (a b : α), a ⊓ b = if a ≤ b then a else b
-- Mathlib.Computability.TuringMachine.Computable
/-- input resp. output stack  -/
Turing.FinTM2.k₀ : (self : Turing.FinTM2) → self.K
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.instZeroValueGroup : (A : Type u) →
  [inst : CommRing A] → (K : Type v) → [inst_1 : Field K] → [inst_2 : Algebra A K] → Zero (ValuationRing.ValueGroup A K)
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesOnBall.finite : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ} {r : ENNReal},
  HasFiniteFPowerSeriesOnBall f p x n r → ∀ (m : ℕ), n ≤ m → p m = 0
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.EquivEven.Q'_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M × R), (CliffordAlgebra.EquivEven.Q' Q) m = Q m.1 - m.2 * m.2
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_mod : ∀ {a b : ISize} (h : System.Platform.numBits = 32), (a % b).toBitVec32 h = (a.toBitVec32 h).srem (b.toBitVec32 h)
-- Mathlib.Algebra.Group.Hom.Defs
/-- `0` is the additive monoid homomorphism sending all elements to `0`.  -/
instZeroAddMonoidHom : {M : Type u_4} → {N : Type u_5} → [inst : AddZero M] → [inst_1 : AddZeroClass N] → Zero (M →+ N)
-- Lean.Declaration
Lean.ReducibilityHints.regular.inj : ∀ {a a_1 : UInt32}, Lean.ReducibilityHints.regular a = Lean.ReducibilityHints.regular a_1 → a = a_1
-- Mathlib.CategoryTheory.Comma.Over.OverClass
/-- The structure morphism. Use `X ↘ S` instead.  -/
CategoryTheory.OverClass.hom : {C : Type u} → {inst : CategoryTheory.Category.{v, u} C} → {X S : C} → [self : CategoryTheory.OverClass X S] → X ⟶ S
-- Mathlib.Algebra.Polynomial.Degree.Units
Polynomial.Monic.degree_pos_of_not_isUnit : ∀ {R : Type u} [inst : CommSemiring R] {p : Polynomial R}, p.Monic → ¬IsUnit p → 0 < p.degree
-- Aesop.Script.CtorNames
Aesop.CtorNames.mk.injEq : ∀ (ctor : Lean.Name) (args : Array Lean.Name) (hasImplicitArg : Bool) (ctor_1 : Lean.Name) (args_1 : Array Lean.Name)
  (hasImplicitArg_1 : Bool),
  ({ ctor := ctor, args := args, hasImplicitArg := hasImplicitArg } =
      { ctor := ctor_1, args := args_1, hasImplicitArg := hasImplicitArg_1 }) =
    (ctor = ctor_1 ∧ args = args_1 ∧ hasImplicitArg = hasImplicitArg_1)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.toSubgroup_comap : ∀ {A : Type u_7} {A₂ : Type u_8} [inst : AddGroup A] [inst_1 : AddGroup A₂] (f : A →+ A₂) (s : AddSubgroup A₂),
  Subgroup.comap (AddMonoidHom.toMultiplicative f) (AddSubgroup.toSubgroup s) =
    AddSubgroup.toSubgroup (AddSubgroup.comap f s)
-- Std.Internal.Do.Triple.Basic
/-- A Hoare triple for reasoning about programs. A Hoare triple `Triple x pre post epost`
is a *specification* for `x`: if assertion `pre` holds before `x`, then postcondition `post` holds
after running `x` (and `epost` handles any errors).  -/
Std.Internal.Do.Triple : {Pred EPred : Type u} →
  {Prog : Type v} →
    {Value : Type u} →
      [inst : Std.Internal.Do.Assertion Pred] →
        [inst_1 : Std.Internal.Do.Assertion EPred] →
          Prog → [Std.Internal.Do.WP Prog Value Pred EPred] → Pred → (Value → Pred) → EPred → Prop
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.locallyRingedSpaceMap_comp : ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T),
  AlgebraicGeometry.Spec.locallyRingedSpaceMap (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.locallyRingedSpaceMap g)
      (AlgebraicGeometry.Spec.locallyRingedSpaceMap f)
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Finset.sum_single_ite : ∀ {R : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : Semiring R] [inst_2 : Fintype n] (a : R) (i : n),
  (∑ x, fun₀ | x => if i = x then a else 0) = fun₀ | i => a
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Truncated.trunc_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (n m : ℕ)
  (h : autoParam (m ≤ n) CategoryTheory.SimplicialObject.Truncated.trunc._auto_1)
  (G : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C) {X Y : (SimplexCategory.Truncated m)ᵒᵖ} (f : X ⟶ Y),
  ((CategoryTheory.SimplicialObject.Truncated.trunc C n m h).obj G).map f =
    G.map (CategoryTheory.ObjectProperty.homMk f.unop.hom).op
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.uliftFunctor_obj : ∀ (X : AddCommGrpCat), AddCommGrpCat.uliftFunctor.obj X = AddCommGrpCat.of (ULift.{u, v} ↑X)
-- Mathlib.Tactic.DefEqAbuse
/-- Format and log the `#defeq_abuse` diagnostic report.
`kind` is `"tactic"` or `"command"`.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Mathlib.Tactic.DefEqAbuse.reportDefEqAbuse : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [Lean.AddMessageContext m] →
        [Lean.MonadOptions m] →
          String → Array Lean.MessageData → Array (Lean.MessageData × Array Lean.MessageData) → m Unit
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap.congr_simp : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  (f f_1 : F),
  f = f_1 → ∀ [inst_3 : RingHomClass F R S] (I I_1 : Ideal S), I = I_1 → Ideal.comap f I = Ideal.comap f_1 I_1
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instFromJsonWorkspaceFolder : Lean.FromJson Lean.Lsp.WorkspaceFolder
-- Mathlib.Tactic.Variable
/-- Tries elaborating binders, inserting new binders whenever typeclass inference fails.
`i` is the index of the next binder that needs to be checked.

The `toOmit` array keeps track of which binders should be removed at the end,
in particular the `variable_alias` binders and any redundant binders.  -/
Mathlib.Command.Variable.completeBinders' : ℕ →
  ℕ →
    Bool →
      Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder →
        Array Bool → ℕ → Lean.Elab.TermElabM (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder × Array Bool)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toSpanSingleton_comp_toSpanSingleton : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₂ : Type u_6} [inst_1 : TopologicalSpace M₂] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R₁ M₂] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₂] [inst_6 : ContinuousMul R₁]
  {x : M₂} {c : R₁},
  ContinuousLinearMap.toSpanSingleton R₁ x ∘SL ContinuousLinearMap.toSpanSingleton R₁ c =
    ContinuousLinearMap.toSpanSingleton R₁ (c • x)
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.of_constant_on_connected_components : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [LocallyConnectedSpace X] {f : X → Y},
  (∀ (x y : X), y ∈ connectedComponent x → f y = f x) → IsLocallyConstant f
-- Mathlib.Algebra.Group.Action.TypeTags
Additive.addAction : {α : Type u_2} → {β : Type u_3} → [inst : Monoid α] → [MulAction α β] → AddAction (Additive α) β
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.of_mem_specialOrthogonalGroup_fin_two_iff : ∀ {R : Type v} [inst : CommRing R] {a b c d : R},
  !![a, b; c, d] ∈ Matrix.specialOrthogonalGroup (Fin 2) R ↔ a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1
-- Init.Data.String.Lemmas.FindPos
_private.Init.Data.String.Lemmas.FindPos.0.String.posGE.eq_1 : ∀ (s : String) (offset : String.Pos.Raw) (h : offset ≤ s.rawEndPos),
  s.posGE offset h = String.Pos.ofToSlice (s.toSlice.posGE offset ⋯)
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instAddGroup : {𝕜 : Type u_2} → {α : Type u_5} → [inst : AddGroup 𝕜] → [inst_1 : LE α] → AddGroup (IncidenceAlgebra 𝕜 α)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.PreElabHeaderResult.levelNames : Lean.Elab.Command.PreElabHeaderResult → List Lean.Name
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImageMap.transport : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g)
  (F : CategoryTheory.Limits.MonoFactorisation f.hom) {F' : CategoryTheory.Limits.MonoFactorisation g.hom}
  (hF' : CategoryTheory.Limits.IsImage F') (map : F.I ⟶ F'.I),
  CategoryTheory.CategoryStruct.comp map F'.m =
      CategoryTheory.CategoryStruct.comp F.m (CategoryTheory.Arrow.Hom.right sq) →
    CategoryTheory.Limits.HasImageMap sq
-- Lean.Data.NameMap.Basic
Lean.NameSet.instEmptyCollection : EmptyCollection Lean.NameSet
-- Mathlib.CategoryTheory.Sigma.Basic
/-- Composition of sigma homomorphisms.  -/
CategoryTheory.Sigma.SigmaHom.comp : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {X Y Z : (i : I) × C i} →
        CategoryTheory.Sigma.SigmaHom X Y → CategoryTheory.Sigma.SigmaHom Y Z → CategoryTheory.Sigma.SigmaHom X Z
-- Lean.Data.Options
Lean.getOptionDecl : Lean.Name → IO Lean.OptionDecl
-- Mathlib.Analysis.Analytic.Binomial
Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zero : ∀ (a : ℕ) {z : ℂ},
  z ≠ 0 →
    HasFPowerSeriesOnBall (fun x => 1 / (z - x) ^ (a + 1))
      (FormalMultilinearSeries.ofScalars ℂ fun n => (z ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) 0 ‖z‖ₑ
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_succ_succ' : ∀ (n k : ℕ), (n + 1).choose (k + 1) = n.choose k + n.choose (k + 1)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_eq_zero`. -/
Ideal.ramificationIdx_eq_zero : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  {P : Ideal S}, (∀ (n : ℕ), ∃ k, Ideal.map (algebraMap R S) p ≤ P ^ k ∧ n < k) → p.ramificationIdx' P = 0
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- The Galois insertion between `Submodule R M` and `Submodule S N`,
where `S` is the localization of `R` at `p` and `N` is the localization of `M` at `p`.  -/
Submodule.localized'gi : {R : Type u_1} →
  (S : Type u_2) →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Algebra R S] →
                      [inst_7 : Module S N] →
                        [inst_8 : IsScalarTower R S N] →
                          (p : Submonoid R) →
                            [inst_9 : IsLocalization p S] →
                              (f : M →ₗ[R] N) →
                                [inst_10 : IsLocalizedModule p f] →
                                  GaloisInsertion (Submodule.localized' S p f) fun x =>
                                    Submodule.comap f (Submodule.restrictScalars R x)
-- Mathlib.Order.Filter.Extr
/-- If `f` is monotone on `Icc a b` and antitone on `Icc b c`, then the maximum of `f` on
`Icc a c` is attained at `b`.  -/
isMaxOn_Icc_of_mono_anti : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b c : α} {f : α → β},
  MonotoneOn f (Set.Icc a b) → AntitoneOn f (Set.Icc b c) → IsMaxOn f (Set.Icc a c) b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_eq_arcsin : ∀ (x : ℝ), Real.arctan x = Real.arcsin (x / √(1 + x ^ 2))
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- Theorems about `padicNormE` are named with a `'` so the names do not conflict with the
equivalent theorems about `norm` (`‖ ‖`).  -/
padicNormE.add_eq_max_of_ne' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {q r : ℚ_[p]},
  padicNormE q ≠ padicNormE r → padicNormE (q + r) = max (padicNormE q) (padicNormE r)
-- Mathlib.Analysis.Convex.Quasiconvex
QuasiconcaveOn.convex : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LE β] [inst_4 : SMul 𝕜 E] {s : Set E} {f : E → β} [IsCodirectedOrder β], QuasiconcaveOn 𝕜 s f → Convex 𝕜 s
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit = 1
-- Mathlib.Tactic.Choose
/-- Changes `(h : ∀ xs, ∃ a:α, p a) ⊢ g` to `(d : ∀ xs, a) ⊢ (s : ∀ xs, p (d xs)) → g` and
`(h : ∀ xs, p xs ∧ q xs) ⊢ g` to `(d : ∀ xs, p xs) ⊢ (s : ∀ xs, q xs) → g`.
`choose1` returns a tuple of

- the error result (see `ElimStatus`)
- the data new free variable that was "chosen"
- the new goal (which contains the spec of the data as domain of an arrow type)

If `nondep` is true and `α` is inhabited, then it will remove the dependency of `d` on
all propositional assumptions in `xs`. For example if `ys` are propositions then
`(h : ∀ xs ys, ∃ a:α, p a) ⊢ g` becomes `(d : ∀ xs, a) (s : ∀ xs ys, p (d xs)) ⊢ g`.  -/
Mathlib.Tactic.Choose.choose1 : Lean.MVarId →
  Bool → Option Lean.Expr → Lean.Name → Lean.MetaM (Mathlib.Tactic.Choose.ElimStatus × Lean.Expr × Lean.MVarId)
-- Init.PropLemmas
not_and_of_not_right : ∀ (a : Prop) {b : Prop}, ¬b → ¬(a ∧ b)
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.self_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) [inst_3 : CategoryTheory.Projective Z],
  (CategoryTheory.ProjectiveResolution.self Z).π = CategoryTheory.CategoryStruct.id ((ChainComplex.single₀ C).obj Z)
-- Mathlib.RingTheory.AlgebraTower
/-- Extend the scalars of an `AlgHom`.  -/
AlgHom.extendScalars : {A : Type u_3} →
  (B : Type u_4) →
    {C : Type u_5} →
      {D : Type u_6} →
        [inst : CommSemiring A] →
          [inst_1 : CommSemiring C] →
            [inst_2 : CommSemiring D] →
              [inst_3 : Algebra A C] →
                [inst_4 : Algebra A D] →
                  [inst_5 : CommSemiring B] →
                    [inst_6 : Algebra A B] →
                      [inst_7 : Algebra B C] → [inst_8 : IsScalarTower A B C] → (f : C →ₐ[A] D) → C →ₐ[B] D
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_inj : ∀ {M : Type u_2} [inst : AddZeroClass M] {S T : AddSubmonoid Mᵃᵒᵖ}, S.unop = T.unop ↔ S = T
-- Mathlib.Analysis.Calculus.MeanValue
IsOpen.isOpen_inter_preimage_of_deriv_eq_zero : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : 𝕜 → G}
  {s : Set 𝕜}, IsOpen s → DifferentiableOn 𝕜 f s → Set.EqOn (deriv f) 0 s → ∀ (t : Set G), IsOpen (s ∩ f ⁻¹' t)
-- Mathlib.Analysis.Complex.LocallyUniformLimit
/-- The logarithmic derivative of a sequence of functions converging locally uniformly to a
function is the logarithmic derivative of the limit function.  -/
Complex.logDeriv_tendsto : ∀ {ι : Type u_3} {p : Filter ι} {f : ι → ℂ → ℂ} {g : ℂ → ℂ} {s : Set ℂ},
  IsOpen s →
    ∀ {x : ℂ},
      x ∈ s →
        TendstoLocallyUniformlyOn f g p s →
          (∀ᶠ (n : ι) in p, DifferentiableOn ℂ (f n) s) →
            g x ≠ 0 → Filter.Tendsto (fun n => logDeriv (f n) x) p (nhds (logDeriv g x))
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
LinearMap.BilinForm.baseChange_eq_zero_iff : ∀ {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Algebra R A] [inst_4 : Module R M₂] [FaithfulSMul R A]
  (B : LinearMap.BilinForm R M₂), LinearMap.BilinForm.baseChange A B = 0 ↔ B = 0
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.takeWhileAux.eq_def : ∀ (s : String) (stopPos : String.Pos.Raw) (p : Char → Bool) (i : String.Pos.Raw),
  Substring.Raw.takeWhileAux s stopPos p i =
    if h : i < stopPos then
      if p (String.Pos.Raw.get s i) = true then
        have this := ⋯;
        Substring.Raw.takeWhileAux s stopPos p (String.Pos.Raw.next s i)
      else i
    else i
-- Mathlib.Geometry.Diffeology.Basic
/-- Technical condition saying that the diffeology on a space is the one coming from
smoothness in the sense of `ContDiff ℝ ∞`. Necessary as a hypothesis for some theorems
because some normed spaces carry a diffeology that is equal but not defeq to the normed space
diffeology (for example the product diffeology in the case of `Fin n → ℝ`), so the information
that these theorems still holds needs to be made available via this typeclass.  -/
Diffeology.IsContDiffCompatible : (X : Type u_1) → [inst : NormedAddCommGroup X] → [NormedSpace ℝ X] → [DiffeologicalSpace X] → Prop
-- Mathlib.Data.List.Permutation
List.permutationsAux.rec.eq_2 : ∀ {α : Type u_1} {C : List α → List α → Sort v} (H0 : (is : List α) → C [] is)
  (H1 : (t : α) → (ts is : List α) → C ts (t :: is) → C is [] → C (t :: ts) is) (x : List α) (t : α) (ts : List α),
  List.permutationsAux.rec H0 H1 (t :: ts) x =
    H1 t ts x (List.permutationsAux.rec H0 H1 ts (t :: x)) (List.permutationsAux.rec H0 H1 x [])
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.OfLocalizationSpan.ofIsLocalization : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
      ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set R),
        Ideal.span s = ⊤ →
          (∀ (r : ↑s),
              ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
                ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
                  ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ) →
            P f
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.eq_bot_of_subsingleton : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [Subsingleton ↥H], H = ⊥
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.processFirstVarDone : Lean.Meta.Match.Problem → Lean.Meta.Match.Problem
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : Inhabited α]
  [EquivBEq α] [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∪ m₂).getKey! k = m₁.getKey! k
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.neg_toSimpleFunc : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
  ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (-f)) =ᵐ[μ] -⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.qaryEntropy_one : ∀ (q : ℕ), Real.qaryEntropy q 1 = Real.log ↑(↑q - 1)
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (f g : M₁ →ₗ[R] M₁),
  (LinearMap.toMatrix v₁ v₁) (f * g) = (LinearMap.toMatrix v₁ v₁) f * (LinearMap.toMatrix v₁ v₁) g
-- Mathlib.Data.Part
Part.assert.eq_1 : ∀ {α : Type u_1} (p : Prop) (f : p → Part α),
  Part.assert p f = { Dom := ∃ (h : p), (f h).Dom, get := fun ha => (f ⋯).get ⋯ }
-- Mathlib.Order.Basic
eq_of_forall_gt_iff : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ (c : α), a < c ↔ b < c) → a = b
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Canon.State.mk.inj : ∀ {cache cacheInType cache_1 cacheInType_1 : Std.HashMap Lean.Expr Lean.Expr},
  { cache := cache, cacheInType := cacheInType } = { cache := cache_1, cacheInType := cacheInType_1 } →
    cache = cache_1 ∧ cacheInType = cacheInType_1
-- Lean.Environment
/-- Kernel environment task that is fulfilled when all asynchronously elaborated declarations are
finished, containing the resulting environment. Also collects the environment extension state of
all environment branches that contributed contained declarations.
 -/
Lean.Environment.checked : Lean.Environment → Task Lean.Kernel.Environment