mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Tactic.Omega.Frontend
Lean.Elab.Tactic.Omega.MetaProblem.mk.injEq : ∀ (problem : Lean.Elab.Tactic.Omega.Problem) (facts disjunctions : List Lean.Expr)
  (processedFacts : Std.HashSet Lean.Expr) (problem_1 : Lean.Elab.Tactic.Omega.Problem)
  (facts_1 disjunctions_1 : List Lean.Expr) (processedFacts_1 : Std.HashSet Lean.Expr),
  ({ problem := problem, facts := facts, disjunctions := disjunctions, processedFacts := processedFacts } =
      { problem := problem_1, facts := facts_1, disjunctions := disjunctions_1, processedFacts := processedFacts_1 }) =
    (problem = problem_1 ∧ facts = facts_1 ∧ disjunctions = disjunctions_1 ∧ processedFacts = processedFacts_1)
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.instContainsZeroOppositeOp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero],
  P.op.ContainsZero
-- Mathlib.Topology.Bornology.Constructions
Bornology.isBounded_prod_of_nonempty : ∀ {α : Type u_1} {β : Type u_2} [inst : Bornology α] [inst_1 : Bornology β] {s : Set α} {t : Set β},
  (s ×ˢ t).Nonempty → (Bornology.IsBounded (s ×ˢ t) ↔ Bornology.IsBounded s ∧ Bornology.IsBounded t)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasKernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).hom
      (CategoryTheory.Abelian.factorThruCoimage (F.map f)) =
    F.map (CategoryTheory.Abelian.factorThruCoimage f)
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.hom_id : ∀ {X : FinBddDistLat}, FinBddDistLat.Hom.hom (CategoryTheory.CategoryStruct.id X) = BoundedLatticeHom.id ↑X.toDistLat
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap_comp_map : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* M') (g : N →* N'),
  (Monoid.Coprod.swap M' N').comp (Monoid.Coprod.map f g) = (Monoid.Coprod.map g f).comp (Monoid.Coprod.swap M N)
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Specialize `isScalarTower_mid` to the common case where the top field is `L`.  -/
IntermediateField.isScalarTower_mid' : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  IsScalarTower K (↥S) L
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instAdd : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Add β] → Add (MeasureTheory.SimpleFunc α β)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.instNegTermRing : (α : Type u_2) → Neg (FirstOrder.Language.ring.Term α)
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.comp_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : P.IsMultiplicative] {X Y Z : CategoryTheory.WideSubcategory P} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Analysis.Real.Pi.Wallis
/-- The product of the first `k` terms in Wallis' formula for `π`.  -/
Real.Wallis.W : ℕ → ℝ
-- Init.Data.UInt.Bitwise
UInt64.not_ne_self : ∀ {a : UInt64}, ~~~a ≠ a
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_fin : ∀ (n : ℕ), Nat.card (Fin n) = n
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.fvar.sizeOf_spec : ∀ (moduleName id : String), sizeOf (Lean.Lsp.RefIdent.fvar moduleName id) = 1 + sizeOf moduleName + sizeOf id
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_lt_zero : ∀ {x : ℝ}, Real.arcsin x < 0 ↔ x < 0
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_one : ∀ {R : Type u} [inst : Zero R], Tropical.untrop 1 = 0
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_norm_add_const_of_dist_le' : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a b : E} {r : ℝ}, dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instSub : {K : Type u} → [inst : CommRing K] → Sub (RatFunc K)
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.IsPrincipal.sSup`. -/
Ordinal.Principal.sSup : ∀ {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}} {s : Set Ordinal.{u_1}},
  (∀ x ∈ s, Ordinal.IsPrincipal op x) → Ordinal.IsPrincipal op (sSup s)
-- Std.Do.SPred.SVal
/-- Gets the top-most state of type `σ` from an `SVal`.  -/
Std.Do.SVal.getThe : {σs : List (Type u)} → (σ : Type u) → [Std.Do.SVal.GetTy σ σs] → Std.Do.SVal σs σ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF →
    ∀ {a b : α}, (a == b) = true → Std.DHashMap.Internal.Raw₀.Const.get! m a = Std.DHashMap.Internal.Raw₀.Const.get! m b
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- Transfer `IsBigOWith` over an `OpenPartialHomeomorph`.  -/
OpenPartialHomeomorph.isBigOWith_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {E : Type u_3}
  [inst_2 : Norm E] {F : Type u_4} [inst_3 : Norm F] (e : OpenPartialHomeomorph α β) {b : β},
  b ∈ e.target →
    ∀ {f : β → E} {g : β → F} {C : ℝ},
      Asymptotics.IsBigOWith C (nhds b) f g ↔ Asymptotics.IsBigOWith C (nhds (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.nonzero_mul_comm : ∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a b : A),
  spectrum 𝕜 (a * b) \ {0} = spectrum 𝕜 (b * a) \ {0}
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.Suggestion.mk.sizeOf_spec : ∀ (suggestion : Lean.Meta.Tactic.TryThis.SuggestionText) (preInfo? postInfo? : Option String)
  (style? : Option Lean.Meta.Tactic.TryThis.SuggestionStyle) (messageData? : Option Lean.MessageData)
  (toCodeActionTitle? : Option (String → String)),
  sizeOf
      { suggestion := suggestion, preInfo? := preInfo?, postInfo? := postInfo?, style? := style?,
        messageData? := messageData?, toCodeActionTitle? := toCodeActionTitle? } =
    1 + sizeOf suggestion + sizeOf preInfo? + sizeOf postInfo? + sizeOf style? + sizeOf messageData? +
      sizeOf toCodeActionTitle?
-- Mathlib.Probability.Distributions.Exponential
ProbabilityTheory.exponentialPDF_of_neg : ∀ {r x : ℝ}, x < 0 → ProbabilityTheory.exponentialPDF r x = 0
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
/-- Express the value of `cosZeta` at a positive even integer as a value
of the Bernoulli polynomial.  -/
HurwitzZeta.cosZeta_two_mul_nat : ∀ {k : ℕ} {x : ℝ},
  k ≠ 0 →
    x ∈ Set.Icc 0 1 →
      HurwitzZeta.cosZeta (↑x) (2 * ↑k) =
        (-1) ^ (k + 1) * (2 * ↑Real.pi) ^ (2 * k) / 2 / ↑(2 * k).factorial *
          Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
-- Lean.Message
Lean.instToMessageDataOption : {α : Type} → [Lean.ToMessageData α] → Lean.ToMessageData (Option α)
-- Lean.Message
Lean.MessageDataContext.env : Lean.MessageDataContext → Lean.Environment
-- Mathlib.Logic.Equiv.Defs
Equiv.forall₂_congr : ∀ {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {p : α₁ → β₁ → Prop} {q : α₂ → β₂ → Prop}
  (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂),
  (∀ {x : α₁} {y : β₁}, p x y ↔ q (eα x) (eβ y)) → ((∀ (x : α₁) (y : β₁), p x y) ↔ ∀ (x : α₂) (y : β₂), q x y)
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.forget₂_preservesMonomorphisms : ∀ (C : Type u) (D : Type u') [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FC : C → C → Type u_2} {CC : C → Type w} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [inst_3 : CategoryTheory.ConcreteCategory C FC] {FD : D → D → Type u_3} {CD : D → Type w}
  [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [inst_6 : CategoryTheory.HasForget₂ C D] [(CategoryTheory.forget C).PreservesMonomorphisms],
  (CategoryTheory.forget₂ C D).PreservesMonomorphisms
-- Mathlib.GroupTheory.Congruence.Defs
Con.instPartialOrder.eq_1 : ∀ {M : Type u_1} [inst : Mul M],
  Con.instPartialOrder =
    { toLE := Con.instLE, lt := fun a b => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
      le_antisymm := ⋯ }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.toList_inj : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {t₁ t₂ : Std.ExtDTreeMap α β cmp},
  t₁.toList = t₂.toList ↔ t₁ = t₂
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.ContainsIdentities.eqToHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.ContainsIdentities]
  {x y : C} (h : x = y), W (CategoryTheory.eqToHom h)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- `ContinuousLinearMapClass F R M M₂` asserts `F` is a type of bundled continuous
`R`-linear maps `M → M₂`.  This is an abbreviation for
`ContinuousSemilinearMapClass F (RingHom.id R) M M₂`.  -/
ContinuousLinearMapClass : (F : Type u_1) →
  (R : outParam (Type u_2)) →
    [inst : Semiring R] →
      (M : outParam (Type u_3)) →
        [TopologicalSpace M] →
          [inst_2 : AddCommMonoid M] →
            (M₂ : outParam (Type u_4)) →
              [TopologicalSpace M₂] →
                [inst_4 : AddCommMonoid M₂] → [Module R M] → [Module R M₂] → [FunLike F M M₂] → Prop
-- Mathlib.Tactic.DepRewrite
_private.Mathlib.Tactic.DepRewrite.0.Mathlib.Tactic.DepRewrite.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Mathlib.Tactic.DepRewrite.Config
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for `Iso.inv η`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂.atomInvM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂ m] →
    Mathlib.Tactic.BicategoryLike.AtomIso → m Mathlib.Tactic.BicategoryLike.Atom
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.coe_copy_eq : ∀ {M : Type u_4} {N : Type u_5} {x : One M} {x_1 : One N} (f : OneHom M N) (f' : M → N) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Order.Atoms
isAtomic_dual_iff_isCoatomic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α], IsAtomic αᵒᵈ ↔ IsCoatomic α
-- Mathlib.LinearAlgebra.FreeModule.Basic
/-- A variation of `of_equiv`: the assumption `Module.Free R P` here is explicit rather than an
instance.  -/
Module.Free.of_equiv' : ∀ {R : Type u} {N : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N] {P : Type v}
  [inst_3 : AddCommMonoid P] [inst_4 : Module R P], Module.Free R P → ∀ (e : P ≃ₗ[R] N), Module.Free R N
-- Mathlib.Analysis.PSeries
Finset.le_sum_condensed : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M},
  (∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) →
    ∀ (n : ℕ), ∑ k ∈ Finset.range (2 ^ n), f k ≤ f 0 + ∑ k ∈ Finset.range n, 2 ^ k • f (2 ^ k)
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- Negating a matrix partitioned by rows is equivalent to negating each of the rows.  -/
Matrix.fromRows_neg : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [inst : Neg R] (A₁ : Matrix m₁ n R)
  (A₂ : Matrix m₂ n R), -A₁.fromRows A₂ = (-A₁).fromRows (-A₂)
-- Mathlib.Data.Rat.Cast.Defs
NNRat.commute_cast : ∀ {α : Type u_3} [inst : DivisionSemiring α] (a : α) (q : ℚ≥0), Commute a ↑q
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.exists_isBase_subset_spanning : ∀ {α : Type u_2} {M : Matroid α} {S I : Set α}, M.Indep I → M.Spanning S → I ⊆ S → ∃ B, M.IsBase B ∧ I ⊆ B ∧ B ⊆ S
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- The yoneda embedding of `FormalCoproduct.{v} C` into `v`-presheaves.  -/
CategoryTheory.Limits.FormalCoproduct.yoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.Limits.FormalCoproduct C) (CategoryTheory.Functor Cᵒᵖ (Type v))
-- Init.Data.Array.Monadic
Array.mapM_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → β}
  {g : β → m γ} {xs : Array α}, Array.mapM g (Array.map f xs) = Array.mapM (g ∘ f) xs
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prodMk_iff : ∀ {β : Type u_2} {mβ : MeasurableSpace β} {Ω : Type u_5} {F : Type u_6} {x : MeasurableSpace Ω}
  [inst : TopologicalSpace F] {X : Ω → β} {μ : MeasureTheory.Measure Ω},
  Measurable X →
    ∀ {f : Ω → F},
      MeasureTheory.AEStronglyMeasurable (fun x => f x.2) (MeasureTheory.Measure.map (fun ω => (X ω, ω)) μ) ↔
        MeasureTheory.AEStronglyMeasurable f μ
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable Int8
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {a : E},
  B.polar {a} = {y | ‖(B a) y‖ ≤ 1}
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_lieSubalgebra_mk_left : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (L' : LieSubalgebra R L) {x : L} (hx : x ∈ L') (y : ↥L'),
  ((LieModule.traceForm R (↥L') M) ⟨x, hx⟩) y = ((LieModule.traceForm R L M) x) ↑y
-- Std.Async.UDP
/-- Sends data through an UDP socket. The `addr` parameter specifies the destination address. If `addr`
is `none`, the data is sent to the default peer address set by `connect`.
 -/
Std.Async.UDP.Socket.send : Std.Async.UDP.Socket → ByteArray → optParam (Option Std.Net.SocketAddress) none → Std.Async.Async Unit
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_nil_eq_iff_false : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x : ℕ} (h : [] ≠ []),
  List.maxIdxOn f [] h = x ↔ False
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.instHasForget₂HomSubtypeObj : (S : Type u_1) →
  [inst : AddMonoidWithOne S] →
    (C : Type (u + 1)) →
      [inst_1 : CategoryTheory.LargeCategory C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          {FC : C → C → Type u_2} →
            {CC : C → Type u_3} →
              [inst_3 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
                [inst_4 : CategoryTheory.ConcreteCategory C FC] →
                  [inst_5 : CategoryTheory.HasShift C S] →
                    CategoryTheory.HasForget₂ (CategoryTheory.DifferentialObject S C) C
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.reduceUnary : Lean.Name → ℕ → (ℕ → ℕ) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictAntiOn.const_add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [AddLeftStrictMono α], StrictAntiOn f s → ∀ (c : α), StrictAntiOn (fun x => c + f x) s
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.comp_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ D₃ : F.DescentData f} (φ : D₁ ⟶ D₂) (φ' : D₂ ⟶ D₃) (i : ι)
  {Z : ↑(F.obj { as := Opposite.op (X i) })} (h : D₃.obj i ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp φ φ').hom i) h =
    CategoryTheory.CategoryStruct.comp (φ.hom i) (CategoryTheory.CategoryStruct.comp (φ'.hom i) h)
-- Mathlib.RingTheory.Localization.Module
IsLocalizedModule.map_injective_iff_localizedModuleMap_injective : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_4} {N' : Type u_5} [inst : CommSemiring R] {S : Submonoid R}
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid M'] [inst_6 : Module R M'] [inst_7 : AddCommMonoid N'] [inst_8 : Module R N']
  (g₁ : M →ₗ[R] M') (g₂ : N →ₗ[R] N') [inst_9 : IsLocalizedModule S g₁] [inst_10 : IsLocalizedModule S g₂]
  {l : M →ₗ[R] N},
  Function.Injective ⇑((IsLocalizedModule.map S g₁ g₂) l) ↔ Function.Injective ⇑((LocalizedModule.map S) l)
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.instReprTransitionRule.repr : Std.Time.TimeZone.TransitionRule → ℕ → Std.Format
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.ext : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] {𝔖 : Set (Set E)}
  {f g : UniformConvergenceCLM σ F 𝔖}, (∀ (x : E), f x = g x) → f = g
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.inr_injective : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0], Function.Injective ⇑(MonoidWithZeroHom.inr G₀ H₀)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.instInfinite : Infinite UpperHalfPlane
-- Mathlib.MeasureTheory.Order.Group.Lattice
Measurable.posPart : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : AddGroup α] [inst_2 : MeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} [MeasurableSup α], Measurable f → Measurable fun x => (f x)⁺
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- A functor to an `R`-linear category lifts to a functor from its `R`-linear completion.
 -/
CategoryTheory.Free.lift : (R : Type u_1) →
  [inst : CommRing R] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {D : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} D] →
            [inst_3 : CategoryTheory.Preadditive D] →
              [CategoryTheory.Linear R D] →
                CategoryTheory.Functor C D → CategoryTheory.Functor (CategoryTheory.Free R C) D
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.linearCoyoneda_obj_additive : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] (Y : Cᵒᵖ),
  ((CategoryTheory.linearCoyoneda R C).obj Y).Additive
-- Std.Data.DTreeMap.Internal.Operations
/-- A tree map obtained by inserting elements into `t` if they are new, bundled with an inductive principle.  -/
Std.DTreeMap.Internal.Impl.IteratedSlowNewInsertionInto : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → Type (max 0 u v)
-- Mathlib.Algebra.Order.Archimedean.Class
_private.Mathlib.Algebra.Order.Archimedean.Class.0.FiniteArchimedeanClass.lift.match_1.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  (motive : FiniteArchimedeanClass M → Sort u_2) (A : ArchimedeanClass M) (hA : A ≠ ⊤)
  (h_1 : (A : ArchimedeanClass M) → (hA : A ≠ ⊤) → motive ⟨A, hA⟩),
  (match ⟨A, hA⟩ with
    | ⟨A, hA⟩ => h_1 A hA) =
    h_1 A hA
-- Mathlib.Computability.NFA
NFA.Path.brecOn.go : {α : Type u} →
  {σ : Type v} →
    {M : NFA α σ} →
      {motive : (a a_1 : σ) → (a_2 : List α) → M.Path a a_1 a_2 → Sort u_1} →
        {a a_1 : σ} →
          {a_2 : List α} →
            (t : M.Path a a_1 a_2) →
              ((a a_3 : σ) → (a_4 : List α) → (t : M.Path a a_3 a_4) → NFA.Path.below t → motive a a_3 a_4 t) →
                motive a a_1 a_2 t ×' NFA.Path.below t
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- This lemma is superseded by `MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm` where we
allow `p = ∞` and only require `AEStronglyMeasurable`.  -/
MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  {f : ι → α → E} {g : α → E} [inst : SeminormedAddCommGroup E],
  p ≠ 0 →
    p ≠ ⊤ →
      (∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) →
        MeasureTheory.StronglyMeasurable g →
          ∀ {l : Filter ι},
            Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) l (nhds 0) →
              MeasureTheory.TendstoInMeasure μ f l g
-- Lean.Meta.Tactic.Rewrite
Lean.Meta.RewriteResult.eqProof : Lean.Meta.RewriteResult → Lean.Expr
-- Mathlib.Topology.Algebra.Support
/-- If a family of functions `f` has locally-finite support, subordinate to a family
of open sets, then for any point we can find a neighbourhood on which only finitely-many members of
`f` are non-zero.  -/
LocallyFinite.exists_finset_nhds_support_subset : ∀ {X : Type u_1} {R : Type u_8} {ι : Type u_9} [inst : TopologicalSpace X] {U : ι → Set X} [inst_1 : Zero R]
  {f : ι → X → R},
  (LocallyFinite fun i => Function.support (f i)) →
    (∀ (i : ι), tsupport (f i) ⊆ U i) →
      (∀ (i : ι), IsOpen (U i)) →
        ∀ (x : X), ∃ is, ∃ n ∈ nhds x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (Function.support fun i => f i z) ⊆ ↑is
-- Mathlib.Data.ENat.Basic
ENat.addLECancellable_of_lt_top : ∀ {a : ℕ∞}, a < ⊤ → AddLECancellable a
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.comp_iff_of_bijective_left : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] {f : M →ₗ[R] M'} (e : M' →ₗ[R] M''),
  Function.Bijective ⇑e → (IsLocalizedModule S (e ∘ₗ f) ↔ IsLocalizedModule S f)
-- Init.Data.List.Sublist
List.singleton_suffix_append_singleton_iff : ∀ {α : Type u_1} {a b : α} {l : List α}, [a] <:+ l ++ [b] ↔ a = b
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_toInt8 : ∀ (n : ISize) (h : System.Platform.numBits = 32), n.toInt8.toBitVec = BitVec.signExtend 8 (n.toBitVec32 h)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.zero_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A],
  (DoubleCentralizer.toProd 0).2 = 0
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.neg_add_eq_zero : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b : α}, IsAddUnit a → (-a + b = 0 ↔ a = b)
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem₀ : ∀ {G₀ : Type u_1} {A : Type u_4} [inst : GroupWithZero G₀] [inst_1 : AddGroup A] [inst_2 : DistribMulAction G₀ A]
  {a : G₀}, a ≠ 0 → ∀ (S : AddSubgroup A) (x : A), x ∈ a • S ↔ a⁻¹ • x ∈ S