mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- The fixator of a subset of cardinal `d` in an `n`-primitive action
acts `n-d`-primitively on the remaining (`d ≤ n`).  -/
AddAction.ofFixingSubgroup.isMultiplyPreprimitive : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] {m n : ℕ}
  [AddAction.IsMultiplyPreprimitive M α n] {s : Set α} [Finite ↑s],
  s.ncard + m = n →
    AddAction.IsMultiplyPreprimitive (↥(fixingAddSubgroup M s)) (↥(SubAddAction.ofFixingAddSubgroup M s)) m
-- Mathlib.RingTheory.Valuation.Basic
Valuation.instValuationClass : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀],
  ValuationClass (Valuation R Γ₀) R Γ₀
-- Aesop.Rule
Aesop.UnsafeRuleInfo.mk.sizeOf_spec : ∀ (successProbability : Aesop.Percent),
  sizeOf { successProbability := successProbability } = 1 + sizeOf successProbability
-- Mathlib.Analysis.Analytic.Linear
analyticOn_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {t : Set (E × F)}, AnalyticOn 𝕜 (fun p => p.2) t
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_eq_var : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr) (x y : Int.Internal.Linear.Var),
  Int.Internal.Linear.norm_eq_var_cert lhs rhs x y = true →
    (Int.Internal.Linear.Expr.denote ctx lhs = Int.Internal.Linear.Expr.denote ctx rhs) =
      (Int.Internal.Linear.Var.denote ctx x = Int.Internal.Linear.Var.denote ctx y)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertManyIfNew!_eq_foldl_impl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β},
  ↑(t₁.insertManyIfNew! t₂) =
    Std.DTreeMap.Internal.Impl.foldl (fun acc k v => Std.DTreeMap.Internal.Impl.insertIfNew! k v acc) t₁ t₂
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
instZeroLEOneClassOfExistsAddOfLEOfPosMulMonoOfAddLeftMono : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R],
  ZeroLEOneClass R
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- `χ₁` is (local) notation for the (necessarily trivial) Dirichlet character modulo `1`.  -/
_private.Mathlib.NumberTheory.LSeries.Dirichlet.0.Dchar_one : Lean.ParserDescr
-- Lean.DocString.Parser
/-- Reads a prefix of a line of text, stopping at a text-mode special character.  -/
Lean.Doc.Parser.text : Lean.Parser.ParserFn
-- Mathlib.MeasureTheory.Function.Holder
/-- Heterogeneous scalar multiplication of `MeasureTheory.Lp` functions by `MeasureTheory.Lp`
functions when the exponents satisfy `ENNReal.HolderTriple p q r`.  -/
MeasureTheory.Lp.instHSMulSubtypeAEEqFunMemAddSubgroup : {α : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_4} →
      {m : MeasurableSpace α} →
        {μ : MeasureTheory.Measure α} →
          {p q r : ENNReal} →
            [hpqr : p.HolderTriple q r] →
              [inst : NormedRing 𝕜] →
                [inst_1 : NormedAddCommGroup E] →
                  [inst_2 : MulActionWithZero 𝕜 E] →
                    [IsBoundedSMul 𝕜 E] →
                      HSMul ↥(MeasureTheory.Lp 𝕜 p μ) ↥(MeasureTheory.Lp E q μ) ↥(MeasureTheory.Lp E r μ)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.natDegree_U : ∀ (R : Type u_1) [inst : CommRing R] [IsDomain R] [NeZero 2] (n : ℤ),
  (Polynomial.Chebyshev.U R n).natDegree = (n + 1).natAbs - 1
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Std.Do.EStateM.instWP.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s' : σ) → motive (EStateM.Result.ok a s')) →
        ((e : ε) → (s' : σ) → motive (EStateM.Result.error e s')) → motive x
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemHandlerKind.noConfusionType : Sort v✝ → Lean.Elab.ConfigEval.EvalConfigItemHandlerKind → Lean.Elab.ConfigEval.EvalConfigItemHandlerKind → Sort v✝
-- Mathlib.Order.Interval.Finset.Defs
/-- The finset $(-∞, b)$ of elements `x` such that `x < b`. Basically `Set.Iio b` as a finset.  -/
Finset.Iio : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderBot α] → α → Finset α
-- Init.Data.SInt.Lemmas
Int64.neg_add_mul_eq_mul_not : ∀ {a b : Int64}, -(a + a * b) = a * ~~~b
-- Init.Data.Iterators.Combinators.Monadic.ULift
/-- Transforms a step of the base iterator into a step of the `uLift` iterator.
 -/
Std.Iterators.Types.ULiftIterator.Monadic.modifyStep : {α : Type u} →
  {m : Type u → Type u'} →
    {n : Type (max u v) → Type v'} →
      {β : Type u} →
        {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} →
          Std.IterStep (Std.IterM m β) β → Std.IterStep (Std.IterM n (ULift.{v, u} β)) (ULift.{v, u} β)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instSubCoeOfAddSubgroupClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → SubNegMonoid (R i)] →
              [∀ (i : ι), AddSubgroupClass (S i) (R i)] → Sub (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.Iter.step_drop.match_3.eq_3 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2)
  (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.Data.Nat.Totient
Nat.filter_coprime_Ico_eq_totient : ∀ (a n : ℕ), {x ∈ Finset.Ico n (n + a) | a.Coprime x}.card = a.totient
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.neg_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Neg β] (f : MeasureTheory.SimpleFunc α β) (x : α),
  (-f) x = -f x
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {I J : Ideal A}
  (h : I ≤ J), (DoubleQuot.quotQuotEquivQuotOfLEₐ R h).toRingEquiv = DoubleQuot.quotQuotEquivQuotOfLE h
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.symm_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (f : M ≃ₜ+ N), f.symm.symm = f
-- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
ConvexOn.integrable_comp_condExp_rnDeriv : ∀ {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ},
  m ≤ m𝓧 →
    μ.AbsolutelyContinuous ν →
      MeasureTheory.StronglyMeasurable f →
        ConvexOn ℝ (Set.Ici 0) f →
          ContinuousWithinAt f (Set.Ici 0) 0 →
            MeasureTheory.Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν →
              MeasureTheory.Integrable (fun x => f (ν[fun x => (μ.rnDeriv ν x).toReal | m] x)) ν
-- Mathlib.Algebra.Notation.Indicator
/-- Evaluating the indicator of a family of functions at a point commutes with the indicator:
`s.mulIndicator f a b = s.mulIndicator (f · b) a`.  -/
Set.mulIndicator_apply_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : One M] {s : Set α} {a : α} (f : α → β → M) (b : β),
  s.mulIndicator f a b = s.mulIndicator (fun i => f i b) a
-- Mathlib.Algebra.Group.Prod
AddHom.coe_snd : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N], ⇑(AddHom.snd M N) = Prod.snd
-- Mathlib.CategoryTheory.Abelian.Basic
/-- The canonical map `pullback f g ⟶ X ⊞ Y`  -/
CategoryTheory.Abelian.PullbackToBiproductIsKernel.pullbackToBiproduct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.pullback f g ⟶ X ⊞ Y
-- Init.Data.Float.Model.Unpacked.Operations.ToNat
/-- Converts an `UnpackedFloat` to an `Int64`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.UnpackedFloat.toInt64 : Float.Model.UnpackedFloat → Int64
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- If `F` preserves terminal objects, then `terminalComparison F` is an isomorphism.  -/
CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [h : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F] →
                F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅
                  CategoryTheory.MonoidalCategoryStruct.tensorUnit D
-- Lean.Util.Diff
Lean.Diff.Histogram.Entry.mk.inj : ∀ {α : Type u} {lsize rsize leftCount : ℕ} {leftIndex : Option (Fin lsize)} {leftWF : leftCount = 0 ↔ leftIndex = none}
  {rightCount : ℕ} {rightIndex : Option (Fin rsize)} {rightWF : rightCount = 0 ↔ rightIndex = none} {leftCount_1 : ℕ}
  {leftIndex_1 : Option (Fin lsize)} {leftWF_1 : leftCount_1 = 0 ↔ leftIndex_1 = none} {rightCount_1 : ℕ}
  {rightIndex_1 : Option (Fin rsize)} {rightWF_1 : rightCount_1 = 0 ↔ rightIndex_1 = none},
  { leftCount := leftCount, leftIndex := leftIndex, leftWF := leftWF, rightCount := rightCount,
        rightIndex := rightIndex, rightWF := rightWF } =
      { leftCount := leftCount_1, leftIndex := leftIndex_1, leftWF := leftWF_1, rightCount := rightCount_1,
        rightIndex := rightIndex_1, rightWF := rightWF_1 } →
    leftCount = leftCount_1 ∧ leftIndex = leftIndex_1 ∧ rightCount = rightCount_1 ∧ rightIndex = rightIndex_1
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsProper
-- Init.Notation
/-- Minimum precedence used in term parsers.  -/
precMin : Lean.ParserDescr
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.IsometryEquiv.prodProdProdComm_toFun : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} {P : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N₁] [inst_4 : AddCommMonoid N₂]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R N₁] [inst_9 : Module R N₂]
  [inst_10 : Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R N₁ P)
  (Q₄ : QuadraticMap R N₂ P) (mnmn : (M₁ × M₂) × N₁ × N₂),
  (QuadraticMap.IsometryEquiv.prodProdProdComm Q₁ Q₂ Q₃ Q₄) mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.not_modEq_iff_ne_add_zsmul : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G}, ¬a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b ≠ a + z • p
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.subtypeCongr.right_apply : ∀ {ε : Type u_9} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a }) (en : Equiv.Perm { a // ¬p a })
  {a : ε} (h : ¬p a), (ep.subtypeCongr en) a = ↑(en ⟨a, h⟩)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The preorder on `WithPreorder R` arising from the valuative relation on `R`.  -/
ValuativeRel.instPreorderWithPreorder : {R : Type u_1} → [inst : Semiring R] → [ValuativeRel R] → Preorder (ValuativeRel.WithPreorder R)
-- Mathlib.Order.Category.DistLat
distLat_dual_comp_forget_to_Lat : DistLat.dual.comp (CategoryTheory.forget₂ DistLat Lat) = (CategoryTheory.forget₂ DistLat Lat).comp Lat.dual
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_of_neg : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], a < 0 → |a| = -a
-- Mathlib.RingTheory.Jacobson.Radical
Ring.instIsTwoSidedJacobson : ∀ (R : Type u_1) [inst : Ring R], (Ring.jacobson R).IsTwoSided
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → Std.DHashMap.Raw.Const.get! (m₁.diff m₂) k = default
-- Mathlib.CategoryTheory.Generator.Basic
/-- For a category `C` and an object `G : C`, `G` is a coseparator of `C` if
the functor `C(-, G)` is faithful.

While `IsCoseparator G : Prop` is the proposition that `G` is a coseparator of `C`,
an `HasCoseparator C : Prop` is the proposition that such a coseparator exists.
Note that `HasCoseparator C` is a proposition. It does not designate a favored coseparator
and merely asserts the existence of one.
 -/
CategoryTheory.HasCoseparator : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.toPoly'.go.induct : ∀ (motive : ℤ → Int.Internal.Linear.Expr → Prop),
  (∀ (coeff k : ℤ), (k == 0) = true → motive coeff (Int.Internal.Linear.Expr.num k)) →
    (∀ (coeff k : ℤ), (k == 0) = false → motive coeff (Int.Internal.Linear.Expr.num k)) →
      (∀ (coeff : ℤ) (v : Int.Internal.Linear.Var), motive coeff (Int.Internal.Linear.Expr.var v)) →
        (∀ (coeff : ℤ) (a b : Int.Internal.Linear.Expr), motive coeff a → motive coeff b → motive coeff (a.add b)) →
          (∀ (coeff : ℤ) (a b : Int.Internal.Linear.Expr),
              motive coeff a → motive (-coeff) b → motive coeff (a.sub b)) →
            (∀ (coeff k : ℤ) (a : Int.Internal.Linear.Expr),
                (k == 0) = true → motive coeff (Int.Internal.Linear.Expr.mulL k a)) →
              (∀ (coeff k : ℤ) (a : Int.Internal.Linear.Expr),
                  (k == 0) = false → motive (coeff.mul k) a → motive coeff (Int.Internal.Linear.Expr.mulL k a)) →
                (∀ (coeff : ℤ) (a : Int.Internal.Linear.Expr) (k : ℤ), (k == 0) = true → motive coeff (a.mulR k)) →
                  (∀ (coeff : ℤ) (a : Int.Internal.Linear.Expr) (k : ℤ),
                      (k == 0) = false → motive (coeff.mul k) a → motive coeff (a.mulR k)) →
                    (∀ (coeff : ℤ) (a : Int.Internal.Linear.Expr), motive (-coeff) a → motive coeff a.neg) →
                      ∀ (coeff : ℤ) (a : Int.Internal.Linear.Expr), motive coeff a
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.mul_go_NonnegCoeffs : ∀ (p₁ p₂ acc : Lean.Grind.CommRing.Poly),
  p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → (Lean.Grind.CommRing.Poly.mul.go p₂ p₁ acc).NonnegCoeffs
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the sign of the angle between three points is nonzero, the first two points are not
equal.  -/
EuclideanGeometry.left_ne_of_oangle_sign_ne_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign ≠ 0 → p₁ ≠ p₂
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.center_eq_inversion' : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c x : P} {R : ℝ}, c = EuclideanGeometry.inversion c R x ↔ x = c ∨ R = 0
-- Mathlib.Order.Interval.Basic
NonemptyInterval.map_snd : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (a : NonemptyInterval α),
  (NonemptyInterval.map f a).toProd.2 = f a.1.2
-- Init.Tactics
/-- `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.
```
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
  simp? -- prints "Try this: simp only [ite_true]"
```

This command can also be used in `simp_all` and `dsimp`.
 -/
Lean.Parser.Tactic.dsimpTrace : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.BaseChange
Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_right : ∀ {m : Type u_1} {n : Type u_2} {L : Type u_3} [Finite m] [inst : Fintype n] [inst_1 : DecidableEq m] [inst_2 : Field L]
  (e : m ≃ n) (K : Subfield L) {A : Matrix m n L} {B : Matrix n m L},
  A * B = 1 → (∀ (i : m) (j : n), A i j ∈ K) → ∀ (i : n) (j : m), B i j ∈ K
-- Init.Data.String.Basic
String.Pos.Raw.isValid_iff_exists_append : ∀ {s : String} {p : String.Pos.Raw}, String.Pos.Raw.IsValid s p ↔ ∃ s₁ s₂, s = s₁ ++ s₂ ∧ p = s₁.rawEndPos
-- Mathlib.Algebra.Module.Shrink
Shrink.linearEquiv_symm_apply : ∀ (R : Type u_1) (α : Type u_2) [inst : Small.{v, u_2} α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid α]
  [inst_3 : Module R α] (a : α), (Shrink.linearEquiv R α).symm a = (equivShrink α) a
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.isKInjective_iff_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {L₁ L₂ : CochainComplex C ℤ} (e : L₁ ≅ L₂), L₁.IsKInjective ↔ L₂.IsKInjective
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.collectInstantiateParams : Lean.Syntax.TSepArray `Lean.Parser.Tactic.Grind.thm "," → Lean.Meta.Grind.Collector.Collect✝ Unit
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.equivOfInverse_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁)
  (h₁ : Function.LeftInverse ⇑f₂ ⇑f₁) (h₂ : Function.RightInverse ⇑f₂ ⇑f₁) (x : M₁),
  (ContinuousLinearEquiv.equivOfInverse f₁ f₂ h₁ h₂) x = f₁ x
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.Functor.op_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor C D) [F.Additive], F.op.Additive
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.leftOp_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ),
  X.leftOp.right = Opposite.unop X.left
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_counitIso_hom_app_left : ∀ {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] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeftIso R i).counitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Data.Num.Basic
/-- The predecessor of a `PosNum` as a `Num`.  -/
PosNum.pred' : PosNum → Num
-- Aesop.Tree.Data.ForwardRuleMatches
_private.Aesop.Tree.Data.ForwardRuleMatches.0.Aesop.ForwardRuleMatches.pHashSetToArray : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PHashSet α → Array α
-- Mathlib.Order.SuccPred.Basic
Order.le_pred_of_lt : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α}, b < a → b ≤ Order.pred a
-- Mathlib.Data.Finset.NAry
Finset.sup_image₂_le : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
  {t : Finset β} [inst_1 : SemilatticeSup δ] [inst_2 : OrderBot δ] {g : γ → δ} {a : δ},
  (Finset.image₂ f s t).sup g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.Pseudofunctor B C} (θ : G ⟶ H) {a : B} {a' : C} (f : a' ⟶ G.obj a),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.id a)).hom)
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapId a).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapId a).hom (θ.app a)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor (θ.app a)).hom)
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor (θ.app a)).inv))
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (CategoryTheory.LaxBraidedFunctor C D)
-- Init.Data.Rat.Basic
instHashableRat : Hashable ℚ
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.comp.match_1.eq_2 : ∀ {C : Type u_1}
  (motive : CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Sort u_2)
  (_X : C) (x : CategoryTheory.WithTerminal C)
  (h_1 :
    (_X _Y _Z : C) →
      motive (CategoryTheory.WithTerminal.of _X) (CategoryTheory.WithTerminal.of _Y)
        (CategoryTheory.WithTerminal.of _Z))
  (h_2 :
    (_X : C) →
      (x : CategoryTheory.WithTerminal C) →
        motive (CategoryTheory.WithTerminal.of _X) x CategoryTheory.WithTerminal.star)
  (h_3 :
    (_X : C) →
      (x : CategoryTheory.WithTerminal C) →
        motive CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of _X) x)
  (h_4 :
    (x : CategoryTheory.WithTerminal C) →
      (_Y : C) → motive x CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of _Y))
  (h_5 :
    Unit → motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.of _X, x, CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of _X, CategoryTheory.WithTerminal.of _Y, CategoryTheory.WithTerminal.of _Z =>
      h_1 _X _Y _Z
    | CategoryTheory.WithTerminal.of _X, x, CategoryTheory.WithTerminal.star => h_2 _X x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _X, x => h_3 _X x
    | x, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _Y => h_4 x _Y
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star => h_5 ()) =
    h_2 _X x
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.dvdCnstr? : Lean.Expr → Lean.Meta.Simp.Arith.Int.ToLinear.M (Option (ℤ × Int.Internal.Linear.Expr))
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Theory.model_iff : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (T : L.Theory), M ⊨ T ↔ ∀ φ ∈ T, M ⊨ φ