mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Dual.Basis
/-- Try using `Set.toFinite` to dispatch a `Set.Finite` goal.  -/
tacticUse_finite_instance : Lean.ParserDescr
-- Batteries.Data.String.Legacy
/-- Finds the position of the first character in a string for which the Boolean predicate `p` returns
`true`. If there is no such character in the string, then the end position of the string is
returned.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.

Examples:
 * `"coffee tea water".find (·.isWhitespace) = ⟨6⟩`
 * `"tea".find (· == 'X') = ⟨3⟩`
 * `"".find (· == 'X') = ⟨0⟩`
 -/
String.Legacy.find : String → (Char → Bool) → String.Pos.Raw
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.eval₂_sub : ∀ {R : Type u} {S : Type v} {σ : Type u_1} [inst : CommRing R] (p : MvPolynomial σ R) {q : MvPolynomial σ R}
  [inst_1 : CommRing S] (f : R →+* S) (g : σ → S),
  MvPolynomial.eval₂ f g (p - q) = MvPolynomial.eval₂ f g p - MvPolynomial.eval₂ f g q
-- Mathlib.Algebra.Homology.ComplexShape
/-- Nonzero differentials `X i ⟶ X j` shall be allowed
on homological complexes when `Rel i j` holds.  -/
ComplexShape.Rel : {ι : Type u_1} → ComplexShape ι → ι → ι → Prop
-- Mathlib.Probability.HasCondDistrib
ProbabilityTheory.HasCondDistrib.snd : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {𝓩 : Type u_4} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {m𝓩 : MeasurableSpace 𝓩} {P : MeasureTheory.Measure Ω} {X : Ω → 𝓧} [MeasureTheory.SFinite P]
  {Y : Ω → 𝓨 × 𝓩} {κ : ProbabilityTheory.Kernel 𝓧 (𝓨 × 𝓩)} [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.HasCondDistrib Y X κ P → ProbabilityTheory.HasCondDistrib (fun ω => (Y ω).2) X κ.snd P
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
/-- The linear map from `⨂[𝕜] i, Eᵢ` to `ContinuousMultilinearMap 𝕜 E F →L[𝕜] F` sending
`x` in `⨂[𝕜] i, Eᵢ` to the map `f ↦ f.lift x`.  -/
PiTensorProduct.toDualContinuousMultilinearMap : {ι : Type uι} →
  [Fintype ι] →
    {𝕜 : Type u𝕜} →
      [inst : NontriviallyNormedField 𝕜] →
        {E : ι → Type uE} →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
              (F : Type u_1) →
                [inst_3 : SeminormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    (PiTensorProduct 𝕜 fun i => E i) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] F
-- Std.Http.Data.Chunk
Std.Http.Chunk.ExtensionValue.mk.sizeOf_spec : ∀ (value : String)
  (isValidExtensionValue :
    autoParam (Std.Http.Chunk.IsValidExtensionValue value)
      Std.Http.Chunk.ExtensionValue.isValidExtensionValue._autoParam),
  sizeOf { value := value, isValidExtensionValue := isValidExtensionValue } =
    1 + sizeOf value + sizeOf isValidExtensionValue
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.coe_coe_orderMonoidWithZeroHom : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β), ⇑↑f = ⇑f
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.card_subtype : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) (L : AddSubgroup ↥K),
  Nat.card ↥(AddSubgroup.map K.subtype L) = Nat.card ↥L
-- Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Nat.instUniqueFactorizationMonoid : UniqueFactorizationMonoid ℕ
-- Mathlib.Topology.ContinuousMap.Ideals
/-- This is the natural homeomorphism between a compact Hausdorff space `X` and the
`WeakDual.characterSpace 𝕜 C(X, 𝕜)`.  -/
WeakDual.CharacterSpace.homeoEval : (X : Type u_1) →
  (𝕜 : Type u_2) →
    [inst : TopologicalSpace X] →
      [CompactSpace X] → [T2Space X] → [inst_3 : RCLike 𝕜] → X ≃ₜ ↑(WeakDual.characterSpace 𝕜 C(X, 𝕜))
-- Init.Data.String.Basic
String.Pos.offset_ofToSlice : ∀ {s : String} {pos : s.toSlice.Pos}, (String.Pos.ofToSlice pos).offset = pos.offset
-- Init.Data.Nat.Div.Basic
_private.Init.Data.Nat.Div.Basic.0.Nat.modCore.go.fuel_congr : ∀ (x y fuel1 fuel2 : ℕ) (hy : 0 < y) (h1 : x < fuel1) (h2 : x < fuel2),
  Nat.modCore.go y hy fuel1 x h1 = Nat.modCore.go y hy fuel2 x h2
-- Init.Data.String.Termination
String.Pos.Splits.remainingBytes_eq : ∀ {s : String} {p : s.Pos} {t₁ t₂ : String}, p.Splits t₁ t₂ → p.remainingBytes = t₂.utf8ByteSize
-- Mathlib.Topology.Instances.NNReal.Lemmas
Real.comap_toNNReal_atTop : Filter.comap Real.toNNReal Filter.atTop = Filter.atTop
-- Mathlib.Order.Atoms
Prop.isAtom_iff : ∀ {p : Prop}, IsAtom p ↔ p
-- Mathlib.Analysis.Fourier.Notation
/-- The Fourier transform as a continuous linear equivalence.  -/
FourierTransform.fourierCLE : (R : Type u_5) →
  (E : Type u_6) →
    {F : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : AddCommMonoid F] →
            [inst_3 : Module R E] →
              [inst_4 : Module R F] →
                [inst_5 : FourierTransform E F] →
                  [FourierAdd E F] →
                    [FourierSMul R E F] →
                      [inst_8 : FourierTransformInv F E] →
                        [FourierPair E F] →
                          [FourierInvPair F E] →
                            [inst_11 : TopologicalSpace E] →
                              [inst_12 : TopologicalSpace F] →
                                [ContinuousFourier E F] → [ContinuousFourierInv F E] → E ≃L[R] F
-- Mathlib.Algebra.GCDMonoid.Basic
dvd_lcm_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b : α), b ∣ lcm a b
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- Transport a `HasExactLimitsOfShape` along an equivalence of the shape.

Note: When `C` has finite colimits, this lemma holds with the equivalence replaced by an initial
functor, see `hasExactLimitsOfShape_of_initial` below.
 -/
CategoryTheory.HasExactLimitsOfShape.of_domain_equivalence : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {J' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : CategoryTheory.Category.{v_2, u_2} J'] (e : J ≌ J')
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.HasExactLimitsOfShape J C],
  CategoryTheory.HasExactLimitsOfShape J' C
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_sup : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  {s : Set M}, Submodule.span R s ⊔ p = Submodule.span R (s ∪ ↑p)
-- Mathlib.Order.CompleteLattice.Basic
iInf_le_iInf₂ : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (κ : ι → Sort u_8) (f : ι → α), ⨅ i, f i ≤ ⨅ i, ⨅ x, f i
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.isPositive_adjoint_comp_self : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (S : E →L[𝕜] F),
  (ContinuousLinearMap.adjoint S ∘SL S).IsPositive
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_all_iff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {ι : Sort u_4} [Countable ι] {p : α → ι → Prop},
  (∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i) ↔ ∀ (i : ι), ∀ᵐ (a : α) ∂μ, p a i
-- Mathlib.Algebra.Homology.Functor
HomologicalComplex.asFunctor_obj_X : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_3}
  {c : ComplexShape ι} (C : HomologicalComplex (CategoryTheory.Functor T V) c) (t : T) (i : ι),
  (C.asFunctor.obj t).X i = (C.X i).obj t
-- Lean.Meta.Sym.SymM
/-- Pre-shared expressions for commonly used terms.  -/
Lean.Meta.Sym.SharedExprs : Type
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.map_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (g : β →o γ) (f : α →o β),
  Topology.WithUpperSet.map (g.comp f) = (Topology.WithUpperSet.map g).comp (Topology.WithUpperSet.map f)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_zpow : ∀ (x : ℝ) (n : ℤ), Real.log (x ^ n) = ↑n * Real.log x
-- Mathlib.Data.Num.Basic
Num.instMod : Mod Num
-- Mathlib.RingTheory.FractionalIdeal.Basic
Nat.unaryCast.eq_1 : ∀ {R : Type u_1} [inst : One R] [inst_1 : Zero R] [inst_2 : Add R], Nat.unaryCast 0 = 0
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.MorphismProperty.relative_of_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {P : CategoryTheory.MorphismProperty C} [F.Faithful] [F.Full]
  [P.RespectsIso] {f : X ⟶ Y} (hf : F.relativelyRepresentable f),
  (∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), P (hf.snd g)) → CategoryTheory.MorphismProperty.relative F P f
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.epi_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : g ⟶ f)
  [CategoryTheory.Epi sq], CategoryTheory.Epi (CategoryTheory.Arrow.Hom.right sq)
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ_π_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q : ℕ) (i : ℤ) {Z : C}
  (h : L.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q).f i)
      (CategoryTheory.CategoryStruct.comp
        (((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).obj (Opposite.op q)).obj.π.f i) h) =
    CategoryTheory.CategoryStruct.comp ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.π✝ f n₀).f i) h
-- Mathlib.Analysis.ODE.ExistUnique
/-- A time-reversed version of `ODE_solution_unique_of_mem_Icc_right`. Uniqueness is shown in a
closed interval `Icc a b`, where `b` is the "initial" time.  -/
ODE_solution_unique_of_mem_Icc_left : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal}
  {f g : ℝ → E} {a b : ℝ},
  (∀ t ∈ Set.Ioc a b, LipschitzOnWith K (v t) (s t)) →
    ContinuousOn f (Set.Icc a b) →
      (∀ t ∈ Set.Ioc a b, HasDerivWithinAt f (v t (f t)) (Set.Iic t) t) →
        (∀ t ∈ Set.Ioc a b, f t ∈ s t) →
          ContinuousOn g (Set.Icc a b) →
            (∀ t ∈ Set.Ioc a b, HasDerivWithinAt g (v t (g t)) (Set.Iic t) t) →
              (∀ t ∈ Set.Ioc a b, g t ∈ s t) → f b = g b → Set.EqOn f g (Set.Icc a b)
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.Subcomplex.mem_nonDegenerate_iff : ∀ {X : SSet} (A : X.Subcomplex) {n : ℕ} (x : ↑(A.obj (Opposite.op { len := n }))),
  x ∈ A.toSSet.nonDegenerate n ↔ ↑x ∈ X.nonDegenerate n
-- Lean.Modifiers
Lean.isProtected : Lean.Environment → Lean.Name → Bool
-- Mathlib.Algebra.Homology.Opposite
/-- Auxiliary definition for `opEquivalence`.  -/
HomologicalComplex.opCounitIso : {ι : Type u_1} →
  (V : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} V] →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
          (HomologicalComplex.opInverse V c).comp (HomologicalComplex.opFunctor V c) ≅
            CategoryTheory.Functor.id (HomologicalComplex Vᵒᵖ c.symm)
-- Lean.Data.Lsp.Extra
/-- The latest RPC wire format supported by the server.
Defaults to `v0` when `none`.
 -/
Lean.Lsp.RpcOptions.rpcWireFormat? : Lean.Lsp.RpcOptions → Option Lean.Lsp.RpcWireFormat
-- Mathlib.Order.CompleteLattice.Basic
Pi.instCompleteLattice : {α : Type u_8} → {β : α → Type u_9} → [(i : α) → CompleteLattice (β i)] → CompleteLattice ((i : α) → β i)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.one_lt_mul_of_lt_of_le`.  -/
Right.one_lt_mul_of_lt_of_le : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightStrictMono α] {a b : α},
  1 < a → 1 ≤ b → 1 < a * b
-- Init.Data.AC
Lean.Data.AC.Context.evalList_removeNeutrals : ∀ {α : Sort u_1} (ctx : Lean.Data.AC.Context α) (e : List ℕ),
  Lean.Data.AC.evalList α ctx (Lean.Data.AC.removeNeutrals ctx e) = Lean.Data.AC.evalList α ctx e
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.div_le : ∀ {a b c : Ordinal.{u_4}}, b ≠ 0 → (a / b ≤ c ↔ a < b * Order.succ c)
-- Lean.Server.GoTo
Lean.Server.GoToContext : Type
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_union_of_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₁ → k ∈ t₁ ∪ t₂
-- Mathlib.Order.Interval.Finset.Defs
WithBot.instLocallyFiniteOrder.eq_1 : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : LocallyFiniteOrder α],
  WithBot.instLocallyFiniteOrder α =
    LocallyFiniteOrder.mk'
      (fun a b =>
        match a, b with
        | none, none => {⊥}
        | none, some b => ∅
        | some a, none => WithBot.insertBot (Finset.Iic a)
        | some a, some b => Finset.map Function.Embedding.coeWithBot (Finset.Icc b a))
      (fun a b =>
        match a, b with
        | none, x => ∅
        | some a, none => Finset.map Function.Embedding.coeWithBot (Finset.Iic a)
        | some a, some b => Finset.map Function.Embedding.coeWithBot (Finset.Ioc b a))
      (fun a b =>
        match a, b with
        | none, x => ∅
        | some a, none => WithBot.insertBot (Finset.Iio a)
        | some a, some b => Finset.map Function.Embedding.coeWithBot (Finset.Ico b a))
      (fun a b =>
        match a, b with
        | none, x => ∅
        | some a, none => Finset.map Function.Embedding.coeWithBot (Finset.Iio a)
        | some a, some b => Finset.map Function.Embedding.coeWithBot (Finset.Ioo b a))
      ⋯ ⋯ ⋯ ⋯
-- Mathlib.Topology.Homotopy.Basic
/-- Given a continuous function `f`, and a proof `h : P f`, we can define a `HomotopyWith f f P` by
`F (t, x) = f x`
 -/
ContinuousMap.HomotopyWith.refl : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {P : C(X, Y) → Prop} → (f : C(X, Y)) → P f → f.HomotopyWith f P
-- Mathlib.Order.Filter.Pointwise
Filter.pureAddMonoidHom.eq_1 : ∀ {α : Type u_2} [inst : AddZeroClass α],
  Filter.pureAddMonoidHom = { toFun := Filter.pureAddHom.toFun, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Continuous linear equivalences between domains and codomains
define an equivalence between the spaces of continuous alternating maps.  -/
ContinuousLinearEquiv.continuousAlternatingMapCongrEquiv : {R : Type u_1} →
  {M : Type u_2} →
    {M' : Type u_3} →
      {N : Type u_4} →
        {N' : Type u_5} →
          {ι : Type u_6} →
            [inst : Semiring R] →
              [inst_1 : AddCommMonoid M] →
                [inst_2 : Module R M] →
                  [inst_3 : TopologicalSpace M] →
                    [inst_4 : AddCommMonoid M'] →
                      [inst_5 : Module R M'] →
                        [inst_6 : TopologicalSpace M'] →
                          [inst_7 : AddCommMonoid N] →
                            [inst_8 : Module R N] →
                              [inst_9 : TopologicalSpace N] →
                                [inst_10 : AddCommMonoid N'] →
                                  [inst_11 : Module R N'] →
                                    [inst_12 : TopologicalSpace N'] →
                                      (M ≃L[R] M') → (N ≃L[R] N') → M [⋀^ι]→L[R] N ≃ M' [⋀^ι]→L[R] N'
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
/-- Non-unital star algebra homomorphisms commute with the non-unital continuous functional
calculus.  This version is specialized to `A →⋆ₙₐ[S] B` to allow for dot notation.  -/
NonUnitalStarAlgHom.map_cfcₙ : ∀ {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} {p : A → Prop} {q : B → Prop} [inst : CommSemiring R]
  [inst_1 : Nontrivial R] [inst_2 : StarRing R] [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R]
  [inst_5 : ContinuousStar R] [inst_6 : CommRing S] [inst_7 : Algebra R S] [inst_8 : NonUnitalRing A]
  [inst_9 : StarRing A] [inst_10 : TopologicalSpace A] [inst_11 : Module R A] [inst_12 : IsScalarTower R A A]
  [inst_13 : SMulCommClass R A A] [inst_14 : NonUnitalRing B] [inst_15 : StarRing B] [inst_16 : TopologicalSpace B]
  [inst_17 : Module R B] [inst_18 : IsScalarTower R B B] [inst_19 : SMulCommClass R B B] [inst_20 : Module S A]
  [inst_21 : Module S B] [IsScalarTower R S A] [IsScalarTower R S B]
  [inst_24 : NonUnitalContinuousFunctionalCalculus R A p] [inst_25 : NonUnitalContinuousFunctionalCalculus R B q]
  [ContinuousMapZero.UniqueHom R B] (φ : A →⋆ₙₐ[S] B) (f : R → R) (a : A),
  autoParam (ContinuousOn f (quasispectrum R a)) NonUnitalStarAlgHom.map_cfcₙ._auto_1 →
    autoParam (f 0 = 0) NonUnitalStarAlgHom.map_cfcₙ._auto_3 →
      autoParam (Continuous ⇑φ) NonUnitalStarAlgHom.map_cfcₙ._auto_5 →
        autoParam (p a) NonUnitalStarAlgHom.map_cfcₙ._auto_7 →
          autoParam (q (φ a)) NonUnitalStarAlgHom.map_cfcₙ._auto_9 → φ (cfcₙ f a) = cfcₙ f (φ a)
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- **Alias** of `WithAbs.algebraLeft`. -/
WithAbs.instAlgebra_left : {S : Type u_2} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {R : Type u_3} →
        (T : Type u_4) →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring T] → [Algebra R T] → (v : AbsoluteValue R S) → Algebra (WithAbs v) T
-- Mathlib.Algebra.Ring.Pi
/-- **Alias** of `RingHom.pi_injective`. -/
Pi.ringHom_injective : ∀ {I : Type u} {f : I → Type u_1} {γ : Type u_2} [Nonempty I] [inst : (i : I) → NonAssocSemiring (f i)]
  [inst_1 : NonAssocSemiring γ] (g : (i : I) → γ →+* f i),
  (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(RingHom.pi g)
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isBool.injEq : ∀ (val : Bool) (proof : Lean.Expr) (val_1 : Bool) (proof_1 : Lean.Expr),
  (Mathlib.Meta.NormNum.Result'.isBool val proof = Mathlib.Meta.NormNum.Result'.isBool val_1 proof_1) =
    (val = val_1 ∧ proof = proof_1)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (toStrictlyUnitaryPseudofunctor : CategoryTheory.StrictlyUnitaryPseudofunctor B C) →
          (map_comp :
              autoParam
                (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                  toStrictlyUnitaryPseudofunctor.map (CategoryTheory.CategoryStruct.comp f g) =
                    CategoryTheory.CategoryStruct.comp (toStrictlyUnitaryPseudofunctor.map f)
                      (toStrictlyUnitaryPseudofunctor.map g))
                CategoryTheory.StrictPseudofunctor.map_comp._autoParam) →
            autoParam
                (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                  toStrictlyUnitaryPseudofunctor.mapComp f g = CategoryTheory.eqToIso ⋯)
                CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso._autoParam →
              CategoryTheory.StrictPseudofunctor B C
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.exteriorPower.iso₁_hom_naturality_assoc : ∀ {R : Type u} [inst : CommRing R] {M N : ModuleCat R} (f : M ⟶ N) {Z : ModuleCat R} (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ModuleCat.exteriorPower.map f 1)
      (CategoryTheory.CategoryStruct.comp (ModuleCat.exteriorPower.iso₁ N).hom h) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.exteriorPower.iso₁ M).hom (CategoryTheory.CategoryStruct.comp f h)
-- Lean.Level
Lean.Level.PP.toResult : Lean.Level → Lean.Level.PP.M Lean.Level.PP.Result
-- Mathlib.Order.WithBot
WithTop.untopD_eq_untopD_iff : ∀ {α : Type u_1} {d : α} {x y : WithTop α},
  WithTop.untopD d x = WithTop.untopD d y ↔ x = y ∨ x = ↑d ∧ y = ⊤ ∨ x = ⊤ ∧ y = ↑d
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mrange_inl' : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mrange (AddMonoidHom.inl M N) = AddSubmonoid.comap (AddMonoidHom.snd M N) ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.mk' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z},
  CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g →
    (∀ ⦃T : C⦄ ⦃φ φ' : T ⟶ P⦄,
        CategoryTheory.CategoryStruct.comp φ fst = CategoryTheory.CategoryStruct.comp φ' fst →
          CategoryTheory.CategoryStruct.comp φ snd = CategoryTheory.CategoryStruct.comp φ' snd → φ = φ') →
      (∀ ⦃T : C⦄ (a : T ⟶ X) (b : T ⟶ Y),
          CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g →
            ∃ l, CategoryTheory.CategoryStruct.comp l fst = a ∧ CategoryTheory.CategoryStruct.comp l snd = b) →
        CategoryTheory.IsPullback fst snd f g
-- Mathlib.Topology.Inseparable
Inseparable.trans : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y z : X}, Inseparable x y → Inseparable y z → Inseparable x z
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.IsReduced.not_step : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.IsReduced L₁ → ¬FreeGroup.Red.Step L₁ L₂
-- Mathlib.Topology.Continuous
/-- The image of a dense set under a continuous map with dense range is a dense set.  -/
DenseRange.dense_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
  DenseRange f → Continuous f → Dense s → Dense (f '' s)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.monomial_pow : ∀ {R : Type u_2} [inst : CommSemiring R] (m : ℕ) (a : R) (n : ℕ),
  (PowerSeries.monomial m) a ^ n = (PowerSeries.monomial (n * m)) (a ^ n)
-- Lean.Environment
Lean.Kernel.Exception.thmTypeIsNotProp.inj : ∀ {env : Lean.Kernel.Environment} {name : Lean.Name} {type : Lean.Expr} {env_1 : Lean.Kernel.Environment}
  {name_1 : Lean.Name} {type_1 : Lean.Expr},
  Lean.Kernel.Exception.thmTypeIsNotProp env name type = Lean.Kernel.Exception.thmTypeIsNotProp env_1 name_1 type_1 →
    env = env_1 ∧ name = name_1 ∧ type = type_1
-- Mathlib.Order.Closure
/-- The underlying function is a lower adjoint.  -/
LowerAdjoint.gc' : ∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {u : β → α} (self : LowerAdjoint u),
  GaloisConnection self.toFun u
-- Std.Net.Addr
Std.Net.InterfaceAddress.mk.inj : ∀ {name : String} {physicalAddress : Std.Net.MACAddr} {isLoopback : Bool} {address netMask : Std.Net.IPAddr}
  {name_1 : String} {physicalAddress_1 : Std.Net.MACAddr} {isLoopback_1 : Bool} {address_1 netMask_1 : Std.Net.IPAddr},
  { name := name, physicalAddress := physicalAddress, isLoopback := isLoopback, address := address,
        netMask := netMask } =
      { name := name_1, physicalAddress := physicalAddress_1, isLoopback := isLoopback_1, address := address_1,
        netMask := netMask_1 } →
    name = name_1 ∧
      physicalAddress = physicalAddress_1 ∧ isLoopback = isLoopback_1 ∧ address = address_1 ∧ netMask = netMask_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.equiv_iff_toList_perm : ∀ {α : Type u} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β},
  t₁.Equiv t₂ ↔ (Std.DTreeMap.Internal.Impl.Const.toList t₁).Perm (Std.DTreeMap.Internal.Impl.Const.toList t₂)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.filter_key_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → Bool}, (Std.DHashMap.filter (fun k x => f k) m).Equiv m ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) = true
-- Mathlib.Order.Hom.Basic
OrderIsoClass.toOrderHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] [inst_2 : EquivLike F α β]
  [OrderIsoClass F α β], OrderHomClass F α β