mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
/-- The scalar multiplication on the sheafification of a presheaf of modules.  -/
PresheafOfModules.Sheafify.smul : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [CategoryTheory.Presheaf.IsLocallySurjective J α] →
                {M₀ : PresheafOfModules R₀} →
                  {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                    (φ : M₀.presheaf ⟶ A.obj) →
                      [CategoryTheory.Presheaf.IsLocallyInjective J φ] →
                        [CategoryTheory.Presheaf.IsLocallySurjective J φ] →
                          {X : Cᵒᵖ} → ↑(R.obj.obj X) → ↑(A.obj.obj X) → ↑(A.obj.obj X)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.instInhabited : {R : Type u} →
  {S : Type u₁} →
    [inst : Monoid R] →
      [inst_1 : Monoid S] →
        {φ : R →* S} →
          {A : Type v} →
            {B : Type w} →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [inst_3 : DistribMulAction R A] →
                  [inst_4 : NonUnitalNonAssocSemiring B] → [inst_5 : DistribMulAction S B] → Inhabited (A →ₛₙₐ[φ] B)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.isNonZero.eq_def : ∀ (p : Nat.Internal.Linear.Poly),
  p.isNonZero =
    match p with
    | [] => false
    | (k, v) :: p => bif v == Nat.Internal.Linear.fixedVar then decide (k > 0) else Nat.Internal.Linear.Poly.isNonZero p
-- Init.Meta.Defs
/-- Ensure head position is synthetic. The server regards syntax as "original" only if both head and tail info are `original`.  -/
Lean.Syntax.mkSynthetic : Lean.Syntax → Lean.Syntax
-- Mathlib.NumberTheory.LucasLehmer
/-- If `3` is not a square then `(2 * ω) ^ ((q + 1) / 2) = -2`.  -/
LucasLehmer.X.two_mul_ω_pow : ∀ {q : ℕ} [inst : Fact (Nat.Prime q)], Odd q → legendreSym q 3 = -1 → (2 * LucasLehmer.X.ω) ^ ((q + 1) / 2) = -2
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
/-- The second horizontal arrow in the top row.  -/
_private.Mathlib.RingTheory.AdicCompletion.AsTensorProduct.0.AdicCompletion.lTensorf : {R : Type u} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {ι : Type} →
              ((ι → R) →ₗ[R] M) →
                TensorProduct R (AdicCompletion I R) (ι → R) →ₗ[AdicCompletion I R]
                  TensorProduct R (AdicCompletion I R) M
-- Mathlib.LinearAlgebra.Matrix.ToLin
Algebra.leftMulMatrix_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {m : Type u_3}
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (b : Module.Basis m R S) (x : S),
  (Algebra.leftMulMatrix b) x = (LinearMap.toMatrix b b) ((Algebra.lmul R S) x)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Γ'.inhabited : {K : Type u_1} → {Γ : K → Type u_2} → Inhabited (Turing.TM2to1.Γ' K Γ)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {f : (a : α) → β a → Option (γ a)}
  {k : α} (h : t.WF),
  (Std.DTreeMap.Raw.filterMap f t).getKey! k = ((t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome).get!
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.π₁Toπ₂_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.π₁Toπ₂.app S = S.f
-- Mathlib.ModelTheory.Basic
/-- The underlying function of a homomorphism of structures  -/
FirstOrder.Language.Hom.toFun : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Hom M N → M → N
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_abs_toReal_of_sign_nonneg : ∀ {θ : Real.Angle}, 0 ≤ θ.sign → ↑|θ.toReal| = θ
-- Std.Time.Time.Unit.Second
/-- Creates an `Second.Offset` from a natural number.
 -/
Std.Time.Second.Offset.ofNat : ℕ → Std.Time.Second.Offset
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.instPartialOrderSubtypeMem : {α : Type u_2} → [inst : BooleanAlgebra α] → (L : BooleanSubalgebra α) → PartialOrder ↥L
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- Injection of `Y` in the optimal coupling between `X` and `Y`  -/
GromovHausdorff.optimalGHInjr : (X : Type u) →
  (Y : Type v) →
    [inst : MetricSpace X] →
      [inst_1 : CompactSpace X] →
        [inst_2 : Nonempty X] →
          [inst_3 : MetricSpace Y] →
            [inst_4 : CompactSpace Y] → [inst_5 : Nonempty Y] → Y → GromovHausdorff.OptimalGHCoupling X Y
-- Mathlib.LinearAlgebra.Projectivization.Cardinality
/-- Cardinality formula for the points of `ℙ k V` if `k` and `V` are finite with less
natural subtraction.  -/
Projectivization.card' : ∀ (k : Type u_1) (V : Type u_2) [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [Finite V],
  Nat.card V = Nat.card (Projectivization k V) * (Nat.card k - 1) + 1
-- Mathlib.Order.WellFoundedSet
Set.WellFoundedOn.subset : ∀ {α : Type u_2} {r : α → α → Prop} {s t : Set α}, t.WellFoundedOn r → s ⊆ t → s.WellFoundedOn r
-- Mathlib.GroupTheory.Torsion
/-- Torsion monoids are really groups.  -/
IsMulTorsion.group : {G : Type u_1} → [inst : Monoid G] → IsMulTorsion G → Group G
-- Mathlib.LinearAlgebra.Pi
/-- To show a property `motive` of modules holds for arbitrary finite products of modules, it suffices
to show
1. `motive` is stable under isomorphism.
2. `motive` holds for the zero module.
3. `motive` holds for `M × N` if it holds for both `M` and `N`.

Since we need to apply `motive` to modules in `Type u` and in `Type (max u v)`, there is a second
`motive'` argument which is required to be equivalent to `motive` up to universe lifting by `equiv`.

See `Module.pi_induction'` for a version where `motive` assumes `AddCommGroup` instead.
 -/
Module.pi_induction : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} [Finite ι]
  (motive : (N : Type u) → [inst_2 : AddCommMonoid N] → [Module R N] → Prop)
  (motive' : (N : Type (max u v)) → [inst_2 : AddCommMonoid N] → [Module R N] → Prop),
  (∀ {N : Type u} {N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
      [inst_5 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N') →
    (∀ {N N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : Module R N]
        [inst_5 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N') →
      motive PUnit.{u + 1} →
        (∀ {N : Type u} {N' : Type (max u v)} [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N']
            [inst_4 : Module R N] [inst_5 : Module R N'], motive N → motive' N' → motive' (N × N')) →
          ∀ (M : ι → Type u) [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)],
            (∀ (i : ι), motive (M i)) → motive' ((i : ι) → M i)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y},
  f = g ↔ ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n
-- ProofWidgets.Compat
ProofWidgets.ExprWithCtx.mk.sizeOf_spec : ∀ (ci : Lean.Elab.ContextInfo) (lctx : Lean.LocalContext) (linsts : Lean.LocalInstances) (expr : Lean.Expr),
  sizeOf { ci := ci, lctx := lctx, linsts := linsts, expr := expr } =
    1 + sizeOf ci + sizeOf lctx + sizeOf linsts + sizeOf expr
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- The natural equivalence between `Snowflaking X α hr₀ hr₁` and `X`.  -/
Metric.Snowflaking.ofSnowflaking : {X : Type u_1} → {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → Metric.Snowflaking X α hα₀ hα₁ ≃ X
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k : α}, k ∉ m₁ → (m₁ ∩ m₂).getKey! k = default
-- Mathlib.Probability.Kernel.Composition.MeasureComp
ProbabilityTheory.absolutelyContinuous_boolKernel_comp_left : ∀ {α : Type u_1} {mα : MeasurableSpace α} {π : MeasureTheory.Measure Bool} (μ ν : MeasureTheory.Measure α),
  π {false} ≠ 0 → μ.AbsolutelyContinuous (π.bind ⇑(ProbabilityTheory.Kernel.boolKernel μ ν))
-- Mathlib.Data.Nat.Squarefree
Nat.minSqFacAux.eq_def : ∀ (x x_1 : ℕ),
  x.minSqFacAux x_1 =
    match x, x_1 with
    | n, k =>
      if h : n < k * k then none
      else
        have this := ⋯;
        if k ∣ n then
          let n' := n / k;
          have this := ⋯;
          if k ∣ n' then some k else n'.minSqFacAux (k + 2)
        else n.minSqFacAux (k + 2)
-- Mathlib.Data.Set.Lattice
Set.inter_eq_iInter : ∀ {α : Type u_1} {s₁ s₂ : Set α}, s₁ ∩ s₂ = ⋂ b, bif b then s₁ else s₂
-- Mathlib.Algebra.Order.Floor.Div
Finsupp.coe_ceilDiv_def : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : AddCommMonoid β] [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : CeilDiv α β] (f : ι →₀ β)
  (a : α), ⇑(f ⌈/⌉ a) = fun i => f i ⌈/⌉ a
-- Mathlib.Data.Matrix.Basic
Matrix.entryAddMonoidHom_apply : ∀ {m : Type u_2} {n : Type u_3} (α : Type u_11) [inst : AddZeroClass α] (i : m) (j : n) (M : Matrix m n α),
  (Matrix.entryAddMonoidHom α i j) M = M i j
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialOn.analyticOn : ∀ {𝕜 : 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} {s : Set E},
  CPolynomialOn 𝕜 f s → AnalyticOn 𝕜 f s
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.Hom.naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (self : M₁.Hom M₂) {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (M₁.map f)
      ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (self.app Y)) =
    CategoryTheory.CategoryStruct.comp (self.app X) (M₂.map f)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.prod_mk : ∀ {α : Type u} {L : List (α × Bool)} [inst : Group α],
  FreeGroup.prod (FreeGroup.mk L) = (List.map (fun x => bif x.2 then x.1 else x.1⁻¹) L).prod
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.semilength.eq_1 : ∀ (p : DyckWord), p.semilength = List.count DyckStep.U ↑p
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- If the vector passed to `secondInter` is given by a subtraction involving the point in
`secondInter`, the three points are collinear.  -/
EuclideanGeometry.Sphere.secondInter_collinear : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p p' : P),
  Collinear ℝ {p, p', s.secondInter p (p' -ᵥ p)}
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.coe_id : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E],
  ⇑LinearIsometry.id = id
-- Mathlib.Order.MinMax
le_max_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a ≤ max b c ↔ a ≤ b ∨ a ≤ c
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instIsStableUnderBaseChangeTrivialFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)],
  (HomotopicalAlgebra.trivialFibrations C).IsStableUnderBaseChange
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instAddMonoidWithOne : {R : Type u_1} → [inst : AddMonoidWithOne R] → AddMonoidWithOne (ArithmeticFunction R)
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Finite.of_ideal_quotient : ∀ {R : Type u_3} [inst : Ring R] (I : Ideal R) [Finite ↥I] [Finite (R ⧸ I)], Finite R
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoShortComplexH1_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupCohomology.isoShortComplexH1 A).hom =
    CategoryTheory.CategoryStruct.comp
      ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.up ℕ) 0 1 2 groupCohomology.isoShortComplexH1._proof_1
              groupCohomology.isoShortComplexH1._proof_2).hom.app
        (groupCohomology.inhomogeneousCochains A))
      (CategoryTheory.ShortComplex.isoMk (groupCohomology.cochainsIso₀ A) (groupCohomology.cochainsIso₁ A)
          (groupCohomology.cochainsIso₂ A) ⋯ ⋯).hom
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.compQuadraticMap_polar : ∀ {S : Type u_1} {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] {N' : Type u_8} [inst_5 : AddCommGroup N']
  [inst_6 : CommSemiring S] [inst_7 : Algebra S R] [inst_8 : Module S N] [inst_9 : Module S N']
  [inst_10 : IsScalarTower S R N] [inst_11 : Module S M] [inst_12 : IsScalarTower S R M] (f : N →ₗ[S] N')
  (Q : QuadraticMap R M N) (x y : M),
  QuadraticMap.polar (⇑(f.compQuadraticMap' Q)) x y = f (QuadraticMap.polar (⇑Q) x y)
-- Mathlib.Analysis.Normed.Group.Basic
eq_of_norm_div_le_zero : ∀ {E : Type u_5} [inst : NormedGroup E] {a b : E}, ‖a / b‖ ≤ 0 → a = b
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
/-- An open partial homeomorphism is an open map on its source:
the image of an open subset of the source is open.  -/
OpenPartialHomeomorph.isOpen_image_of_subset_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X}, IsOpen s → s ⊆ e.source → IsOpen (↑e '' s)
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.balanced_inter : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} (ht : t₁.Balanced),
  (t₁.inter t₂ ht).Balanced
-- Init.Data.Sum.Basic
/-- Checks whether a sum is the right injection `inr`.  -/
Sum.isRight : {α : Type u_1} → {β : Type u_2} → α ⊕ β → Bool
-- Mathlib.Algebra.Order.AddTorsor
SMul.smul_lt_smul_of_lt_of_le : ∀ {G : Type u_1} {P : Type u_2} [inst : Preorder G] [inst_1 : Preorder P] [inst_2 : SMul G P] [IsOrderedCancelSMul G P]
  {a b : G} {c d : P}, a < b → c ≤ d → a • c < b • d
-- Lean.Meta.Tactic.Grind.AC.PP
_private.Lean.Meta.Tactic.Grind.AC.PP.0.Lean.Meta.Grind.AC.ppBasis? : Lean.Meta.Grind.AC.M✝ (Option Lean.MessageData)
-- Init.System.IO
/-- Reads UTF-8-encoded text up to and including the next line break from the handle. If the returned
string is empty, an end-of-file marker (EOF) has been reached.

Encountering an EOF does not close a handle. Subsequent reads may block and return more data.
 -/
IO.FS.Handle.getLine : IO.FS.Handle → IO String
-- Mathlib.Tactic.ComputeDegree
/-- `compute_degree` is a tactic to solve goals of the form
*  `natDegree f = d`,
*  `degree f = d`,
*  `natDegree f ≤ d` (or `<`),
*  `degree f ≤ d` (or `<`),
*  `coeff f d = r`, if `d` is the degree of `f`.

The tactic may leave goals of the form `d' = d`, `d' ≤ d`, `d' < d`, or `r ≠ 0`, where `d'` in `ℕ`
or `WithBot ℕ` is the tactic's guess of the degree, and `r` is the coefficient's guess of the
leading coefficient of `f`.

`compute_degree` applies `norm_num` to the left-hand side of all side goals, trying to close them.

The variant `compute_degree!` first applies `compute_degree`.
Then it uses `norm_num` on all the remaining goals and tries `assumption`.
 -/
Mathlib.Tactic.ComputeDegree.computeDegree : Lean.ParserDescr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.unitOfList_eq_insertManyIfNewUnit_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α},
  Std.DTreeMap.Const.unitOfList l cmp = Std.DTreeMap.Const.insertManyIfNewUnit ∅ l
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.Proj.stalkIso'_germ : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)) (x : ↑(ProjectiveSpectrum.top 𝒜))
  (hx : x ∈ U) (s : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op U))),
  (AlgebraicGeometry.Proj.stalkIso' 𝒜 x)
      ((CategoryTheory.ConcreteCategory.hom
          ((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.germ U x hx))
        s) =
    ↑s ⟨x, hx⟩
-- Mathlib.Topology.UniformSpace.Separation
Filter.HasBasis.inseparable_iff_uniformity : ∀ {α : Type u} [inst : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → Set (α × α)},
  (uniformity α).HasBasis p s → ∀ {x y : α}, Inseparable x y ↔ ∀ (i : ι), p i → (x, y) ∈ s i
-- Init.Data.Int.Gcd
/-- Represent a divisor of `m * n` as a product of a divisor of `m` and a divisor of `n`.  -/
Int.dvdProdDvdOfDvdProd : {k m n : ℤ} → k ∣ m * n → { d // k = ↑d.1 * ↑d.2 }
-- Mathlib.Data.Finsupp.Single
/-- `Finsupp.single a b` is injective in `a`. For the statement that it is injective in `b`, see
`Finsupp.single_injective`  -/
Finsupp.single_left_injective : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {b : M}, b ≠ 0 → Function.Injective fun a => fun₀ | a => b
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.State.mk.inj : ∀ {out : String} {column : ℕ} {out_1 : String} {column_1 : ℕ},
  { out := out, column := column } = { out := out_1, column := column_1 } → out = out_1 ∧ column = column_1
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- The Euler product for the Riemann ζ function, valid for `s.re > 1`.
This version is stated in terms of `tprod`.  -/
riemannZeta_eulerProduct_tprod : ∀ {s : ℂ}, 1 < s.re → ∏' (p : Nat.Primes), (1 - ↑↑p ^ (-s))⁻¹ = riemannZeta s
-- Mathlib.Data.List.Pairwise
List.Pairwise.rel_get_of_lt : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α},
  List.Pairwise R l → ∀ {a b : Fin l.length}, a < b → R (l.get a) (l.get b)
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.invQParam_tendsto : ∀ {h : ℝ},
  0 < h → Filter.Tendsto (Function.Periodic.invQParam h) (nhdsWithin 0 {0}ᶜ) (Filter.comap Complex.im Filter.atTop)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_le_sub_left : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] [AddRightMono α] {a b : α},
  a ≤ b → ∀ (c : α), c - b ≤ c - a
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Ideal.exists_spanRank_eq_and_height_eq : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (I : Ideal R),
  I ≠ ⊤ → ∃ J ≤ I, Submodule.spanRank J = ↑I.height ∧ J.height = I.height
-- Mathlib.Algebra.BigOperators.Finprod
finsum_eq_sum_plift_of_support_subset : ∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M] {f : α → M} {s : Finset (PLift α)},
  Function.support (f ∘ PLift.down) ⊆ ↑s → ∑ᶠ (i : α), f i = ∑ i ∈ s, f i.down
-- Mathlib.Analysis.InnerProductSpace.l2Space
LinearIsometryEquiv.ofSurjective.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E₂] [inst_5 : Module R₂ E₂] [inst_6 : NormedAddCommGroup F] [inst_7 : Module R F]
  (f f_1 : F →ₛₗᵢ[σ₁₂] E₂) (e_f : f = f_1) (hfr : Function.Surjective ⇑f),
  LinearIsometryEquiv.ofSurjective f hfr = LinearIsometryEquiv.ofSurjective f_1 ⋯
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Transfer `Frame` across an `Equiv`.  -/
Equiv.frame : {α : Type u} → {β : Type v} → α ≃ β → [Order.Frame β] → Order.Frame α
-- Init.Data.Int.Lemmas
Int.sub_eq_add_neg : ∀ {a b : ℤ}, a - b = a + -b
-- Mathlib.GroupTheory.GroupAction.Hom
Pi.evalMulActionHom_apply : ∀ {ι : Type u_1} {M : Type u_2} {X : ι → Type u_3} [inst : (i : ι) → SMul M (X i)] (i : ι) (f : (x : ι) → X x),
  (Pi.evalMulActionHom i) f = Function.eval i f
-- Mathlib.Algebra.Ring.GrindInstances
CommSemiring.toGrindCommSemiring : (α : Type u_1) → [s : CommSemiring α] → Lean.Grind.CommSemiring α
-- Mathlib.Order.Basic
Ne.eq_def : ∀ {α : Sort u} (a b : α), (a ≠ b) = ¬a = b
-- Mathlib.Data.Ordmap.Invariants
Ordnode.size.eq_1 : ∀ {α : Type u_1}, Ordnode.nil.size = 0
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.mk : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            (functor : CategoryTheory.Functor C₁ C₂) →
              W₁ ≤ W₂.inverseImage functor → CategoryTheory.LocalizerMorphism W₁ W₂
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.isMaximal_iff : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : IsLocalRing R] {I : Ideal R},
  I.IsMaximal ↔ I = IsLocalRing.maximalIdeal R
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.elabAppFnId.throwUnknownIdWithSuggestions : Lean.Syntax → Lean.Name → Lean.Elab.TermElabM Unit
-- Lean.Environment
Lean.OLeanEntries.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (exported server «private» : α),
  sizeOf { exported := exported, server := server, «private» := «private» } =
    1 + sizeOf exported + sizeOf server + sizeOf «private»
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingSeminorm.funLike : {R : Type u_1} → [inst : NonAssocRing R] → FunLike (MulRingSeminorm R) R ℝ
-- Mathlib.Data.Set.Prod
Set.preimage.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set β), f ⁻¹' s = {x | f x ∈ s}
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (t.alter k f).isEmpty = false →
        ∀ {fallback : α},
          (t.alter k f).minKeyD fallback = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.GroupTheory.Index
/-- Finite index implies finite quotient.  -/
Subgroup.fintypeOfIndexNeZero : {G : Type u_1} → [inst : Group G] → {H : Subgroup G} → H.index ≠ 0 → Fintype (G ⧸ H)
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.of_homeoOfIso : ∀ {X Y : TopCat} (f : X ≅ Y), TopCat.isoOfHomeo (TopCat.homeoOfIso f) = f
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.ctor.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (i : Lean.Compiler.LCNF.CtorInfo) (args : Array (Lean.Compiler.LCNF.Arg pu))
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_5)
  (i_1 : Lean.Compiler.LCNF.CtorInfo) (args_1 : Array (Lean.Compiler.LCNF.Arg pu))
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_5),
  (Lean.Compiler.LCNF.LetValue.ctor i args h = Lean.Compiler.LCNF.LetValue.ctor i_1 args_1 h_1) =
    (i = i_1 ∧ args = args_1)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.dropSliceTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → Array α → Sort u_2) (x : ℕ) (x_1 : Array α)
  (h_1 : (x : ℕ) → (x_2 : Array α) → motive [] x x_2)
  (h_2 : (head : α) → (xs : List α) → (acc : Array α) → motive (head :: xs) 0 acc)
  (h_3 : (x : α) → (xs : List α) → (n : ℕ) → (acc : Array α) → motive (x :: xs) n.succ acc),
  (match [], x, x_1 with
    | [], x, x_2 => h_1 x x_2
    | head :: xs, 0, acc => h_2 head xs acc
    | x :: xs, n.succ, acc => h_3 x xs n acc) =
    h_1 x x_1