mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.ext : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  {inst_5 : AddCommGroup M₂} {inst_6 : Module R M₂} {inst_7 : AddCommGroup N₂} {inst_8 : Module R N₂}
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {x y : P.Equiv Q},
  (↑x).weightMap = (↑y).weightMap → (↑x).coweightMap = (↑y).coweightMap → (↑x).indexEquiv = (↑y).indexEquiv → x = y
-- Mathlib.Logic.Embedding.Basic
Function.instCanLiftForallEmbeddingCoeInjective : ∀ {α : Sort u_1} {β : Sort u_2}, CanLift (α → β) (α ↪ β) DFunLike.coe Function.Injective
-- Mathlib.Analysis.Calculus.Rademacher
LipschitzWith.ae_exists_fderiv_of_countable : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  LipschitzWith C f → ∀ {s : Set E}, s.Countable → ∀ᵐ (x : E) ∂μ, ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ'_one : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.preΨ' 1 = 1
-- Mathlib.Algebra.Opposites
MulOpposite.instOne.eq_1 : ∀ {α : Type u_1} [inst : One α], MulOpposite.instOne = { one := MulOpposite.op 1 }
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
/-- Two algebra morphisms from the even subalgebra are equal if they agree on pairs of generators.

See note [partially-applied ext lemmas].  -/
CliffordAlgebra.even.algHom_ext : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A]
  ⦃f g : ↥(CliffordAlgebra.even Q) →ₐ[R] A⦄,
  (CliffordAlgebra.even.ι Q).compr₂ f = (CliffordAlgebra.even.ι Q).compr₂ g → f = g
-- Init.Data.Nat.Bitwise.Lemmas
Nat.xor_div_two_pow : ∀ {a b n : ℕ}, (a ^^^ b) / 2 ^ n = a / 2 ^ n ^^^ b / 2 ^ n
-- Init.Prelude
/-- The syntax which supplies the position of error messages.  -/
Lean.Macro.Context.ref : Lean.Macro.Context → Lean.Syntax
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H2Iso_inv_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : groupHomology.H2 A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.π
      (CategoryTheory.CategoryStruct.comp (groupHomology.H2Iso A).inv h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.H2π A) h
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex)
  (n : ℕ) (g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) (g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1))
  (w :
    f.f (n + 1) =
      CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' +
        CategoryTheory.CategoryStruct.comp g (J.cocomplex.d n (n + 1)))
  {Z_1 : C} (h : J.cocomplex.X (n + 2) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 2) (n + 3))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.descHomotopyZeroSucc f n g g' w) h) =
    CategoryTheory.CategoryStruct.comp
      (f.f (n + 2) - CategoryTheory.CategoryStruct.comp g' (J.cocomplex.d (n + 1) (n + 2))) h
-- Mathlib.Analysis.InnerProductSpace.Calculus
hasStrictFDerivAt_euclidean : ∀ {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H]
  [inst_2 : NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {f' : H →L[𝕜] EuclideanSpace 𝕜 ι} {y : H} [Finite ι],
  HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun x => (f x).ofLp i) (PiLp.proj 2 (fun x => 𝕜) i ∘SL f') y
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.submoduleOf_self : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (N : Submodule R M), N.submoduleOf N = ⊤
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.instInhabitedConfig : Inhabited Lean.Meta.Sym.DSimp.Config
-- Std.Time.Date.Basic
Std.Time.instHAddOffset_2 : HAdd Std.Time.Second.Offset Std.Time.Second.Offset Std.Time.Second.Offset
-- Init.BinderNameHint
binderNameHint.eq_1 : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (v : α) (binder : β) (e : γ), binderNameHint v binder e = e
-- Mathlib.Tactic.GuardGoalNums
/-- `guard_goal_nums n` succeeds if there are exactly `n` goals and fails otherwise.  -/
guardGoalNums : Lean.ParserDescr
-- Init.Data.Fin.Lemmas
Fin.subNat.congr_simp : ∀ {n : ℕ} (m : ℕ) (i i_1 : Fin (n + m)) (e_i : i = i_1) (h : m ≤ ↑i), Fin.subNat m i h = Fin.subNat m i_1 ⋯
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.FunPropDecl.mk.inj : ∀ {funPropName : Lean.Name} {path : Array Lean.Meta.DiscrTree.Key} {funArgId : ℕ} {funPropName_1 : Lean.Name}
  {path_1 : Array Lean.Meta.DiscrTree.Key} {funArgId_1 : ℕ},
  { funPropName := funPropName, path := path, funArgId := funArgId } =
      { funPropName := funPropName_1, path := path_1, funArgId := funArgId_1 } →
    funPropName = funPropName_1 ∧ path = path_1 ∧ funArgId = funArgId_1
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Given a function, there is a covariant induced map on graphs by pushing forward
the adjacency relation.

This is injective when the function is (see `SimpleGraph.map_injective`).  -/
SimpleGraph.map : {V : Type u_1} → {W : Type u_2} → (V → W) → SimpleGraph V → SimpleGraph W
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SemilatticeSup β] [inst_2 : Zero β]
  [inst_3 : TopologicalSpace β] [inst_4 : ContinuousSup β] (f g : CompactlySupportedContinuousMap α β),
  ⇑(f ⊔ g) = ⇑f ⊔ ⇑g
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l →
      ∀ {h : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).contains k' = true},
        (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).get k' h = cast ⋯ v
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.commRingEquiv_single_single : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N] (m : M)
  (n : N) (r : R),
  AddMonoidAlgebra.commRingEquiv (AddMonoidAlgebra.single m (AddMonoidAlgebra.single n r)) =
    AddMonoidAlgebra.single n (AddMonoidAlgebra.single m r)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α}, t.WF → (Std.TreeMap.Raw.map f t)[k]? = Option.map (f k) t[k]?
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.coe_centralizer : ∀ {R : Type u_1} [inst : NonUnitalRing R] (s : Set R), ↑(NonUnitalSubring.centralizer s) = s.centralizer
-- Mathlib.Order.Category.Semilat
SemilatInfCat.isOrderTop : (self : SemilatInfCat) → OrderTop self.X
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.endofunctorMonoidalCategory_tensorObj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C C) (X : C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).obj X = G.obj (F.obj X)
-- Mathlib.Geometry.Manifold.Notation
/-- The expression for the normed space's base field.  -/
Manifold.Elab.NormedSpaceInfo.baseField : Manifold.Elab.NormedSpaceInfo → Lean.Expr
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub_natCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIcoDiv hp (a - ↑m * p) b = toIcoDiv hp a b + ↑m
-- Lean.Elab.Term.TermElabM
/-- Return true iff `stx` is a `Syntax.ident`, and it is a local variable.  -/
Lean.Elab.Term.isLocalIdent? : Lean.Syntax → Lean.Elab.TermElabM (Option Lean.Expr)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.rightFunc_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {Y X : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)} (f : Y ⟶ X),
  CategoryTheory.Arrow.rightFunc.map f = f.right
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.instHasLimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [∀ (X : Cᵒᵖ),
      Small.{v, max u₂ v}
        ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections]
  {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.Limits.HasLimit
    (F.comp ((PresheafOfModules.evaluation R Y).comp (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))))
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar_extract_congr_of_le : ∀ {bytes : ByteArray} (i j j' : ℕ) {h : ((bytes.extract i j).utf8DecodeChar? 0).isSome = true}
  {h' : ((bytes.extract i j').utf8DecodeChar? 0).isSome = true},
  j ≤ j' → (bytes.extract i j).utf8DecodeChar 0 h = (bytes.extract i j').utf8DecodeChar 0 h'
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.fst.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β], OrderAddMonoidHom.fst α β = { toAddMonoidHom := AddMonoidHom.fst α β, monotone' := ⋯ }
-- Mathlib.Algebra.Group.Hom.Defs
/-- The proposition that the function preserves addition  -/
AddMonoidHom.map_add' : ∀ {M : Type u_10} {N : Type u_11} [inst : AddZero M] [inst_1 : AddZero N] (self : M →+ N) (x y : M),
  (↑self).toFun (x + y) = (↑self).toFun x + (↑self).toFun y
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.zero : {α : Type u} → [Zero α] → Zero (WithBot α)
-- Mathlib.Data.Sum.Order
/-- Lexicographical `Sum.inr`. Only used for pattern matching.  -/
Sum.inrₗ : {α : Type u_1} → {β : Type u_2} → β → α ⊕ₗ β
-- Mathlib.FieldTheory.Galois.Profinite
finGaloisGroupMap.map_comp : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  {L₁ L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ} (f : L₁ ⟶ L₂) (g : L₂ ⟶ L₃),
  finGaloisGroupMap (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (finGaloisGroupMap f) (finGaloisGroupMap g)
-- Init.Data.Vector.Lemmas
Vector.mem_append_left : ∀ {α : Type u_1} {n m : ℕ} {a : α} {xs : Vector α n} (ys : Vector α m), a ∈ xs → a ∈ xs ++ ys
-- Mathlib.Topology.MetricSpace.Bounded
Metric.ediam_univ_eq_top_iff_noncompact : ∀ {α : Type u} [inst : PseudoMetricSpace α] [ProperSpace α], Metric.ediam Set.univ = ⊤ ↔ NoncompactSpace α
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lim_mul_lim : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [inst_5 : CauSeq.IsComplete β abv]
  (f g : CauSeq β abv), f.lim * g.lim = (f * g).lim
-- Mathlib.RingTheory.Trace.Basic
Algebra.traceMatrix_of_matrix_mulVec : ∀ {κ : Type w} {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Fintype κ] (b : κ → B) (P : Matrix κ κ A),
  Algebra.traceMatrix A ((P.map ⇑(algebraMap A B)).mulVec b) = P * Algebra.traceMatrix A b * P.transpose
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- **Alias** of `CoxeterMatrix.D`.

---

The Coxeter matrix of type Dₙ.

The corresponding Coxeter-Dynkin diagram is:
```
    o
     \
      o --- o ⬝ ⬝ ⬝ ⬝ o --- o
     /
    o
```
 -/
CoxeterMatrix.Dₙ : (n : ℕ) → CoxeterMatrix (Fin n)
-- Mathlib.Data.Nat.Bitwise
/-- If `f` is a commutative operation on bools such that `f false false = false`, then `bitwise f`
is also commutative.  -/
Nat.bitwise_comm : ∀ {f : Bool → Bool → Bool}, (∀ (b b' : Bool), f b b' = f b' b) → ∀ (n m : ℕ), Nat.bitwise f n m = Nat.bitwise f m n
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ \ m₂).get? k = none
-- Mathlib.Data.Fintype.Basic
/-- See also `nonempty_encodable`, `nonempty_denumerable`.  -/
nonempty_fintype : ∀ (α : Type u_4) [Finite α], Nonempty (Fintype α)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.instIsRightAdjointFunctorLim : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C], CategoryTheory.Limits.lim.IsRightAdjoint
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_top_of_bound_enorm : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε},
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (C : NNReal), (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑C) → MeasureTheory.MemLp f ⊤ μ
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.ofScientific_nonneg : ∀ (m : ℕ) (s : Bool) (e : ℕ), 0 ≤ Rat.ofScientific m s e
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.injective_incl : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M), Function.Injective ⇑N.incl
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.AdditiveFunctor.ofExact_obj_fst : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : CategoryTheory.Limits.HasZeroObject D]
  [inst_6 : CategoryTheory.Limits.HasBinaryBiproducts C] (F : C ⥤ₑ D),
  ((CategoryTheory.AdditiveFunctor.ofExact C D).obj F).obj = F.obj
-- Mathlib.Data.Vector3
/-- A local infix notation for `Vector3.append`
 -/
_private.Mathlib.Data.Vector3.0.Vector3.«term_+-+_» : Lean.TrailingParserDescr
-- Mathlib.Data.Nat.ChineseRemainder
Nat.chineseRemainderOfFinset_lt_prod : ∀ {ι : Type u_1} (a s : ι → ℕ) {t : Finset ι} (hs : ∀ i ∈ t, s i ≠ 0)
  (pp : (↑t).Pairwise (Function.onFun Nat.Coprime s)), ↑(Nat.chineseRemainderOfFinset a s t hs pp) < ∏ i ∈ t, s i
-- Lean.Meta.AppBuilder
/-- Given proofs `hᵢ : pᵢ`, returns a proof for `p₁ ∧ ... ∧ pₙ`.
Roughly, `mkAndIntroN hs : mkAndN (← hs.mapM inferType)`.
 -/
Lean.Meta.mkAndIntroN : List Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.FunLike.Embedding
EmbeddingLike.apply_eq_iff_eq : ∀ {F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [inst : FunLike F α β] [i : EmbeddingLike F α β] (f : F) {x y : α},
  f x = f y ↔ x = y
-- Mathlib.Topology.ContinuousMap.Algebra
AddMonoidHom.compLeftContinuous.eq_1 : ∀ (α : Type u_1) {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {γ : Type u_3}
  [inst_2 : AddMonoid β] [inst_3 : ContinuousAdd β] [inst_4 : TopologicalSpace γ] [inst_5 : AddMonoid γ]
  [inst_6 : ContinuousAdd γ] (g : β →+ γ) (hg : Continuous ⇑g),
  AddMonoidHom.compLeftContinuous α g hg =
    { toFun := fun f => { toFun := ⇑g, continuous_toFun := hg }.comp f, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Data.Nat.Basic
Nat.dvd_sub_self_left : ∀ {n m : ℕ}, n ∣ n - m ↔ m = 0 ∨ n ≤ m
-- Mathlib.Algebra.Opposites
/-- The canonical bijection between `α` and `αᵐᵒᵖ`.  -/
MulOpposite.opEquiv : {α : Type u_1} → α ≃ αᵐᵒᵖ
-- Lean.Elab.Deriving.Basic
_private.Lean.Elab.Deriving.Basic.0.Lean.Elab.Term.MkInstResult.instVal : Lean.Elab.Term.MkInstResult✝ → Lean.Expr
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.IsReduced.infix : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.IsReduced L₂ → L₁ <:+: L₂ → FreeAddGroup.IsReduced L₁
-- Mathlib.Analysis.Meromorphic.Basic
/-- If a function is meromorphic at a point, then it is continuous at nearby points.  -/
MeromorphicAt.eventually_continuousAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E}, MeromorphicAt f x → ∀ᶠ (y : 𝕜) in nhdsWithin x {x}ᶜ, ContinuousAt f y
-- Mathlib.Algebra.Group.Action.Basic
MulAction.toPerm.eq_1 : ∀ {α : Type u_5} {β : Type u_6} [inst : Group α] [inst_1 : MulAction α β] (a : α),
  MulAction.toPerm a = { toFun := fun x => a • x, invFun := fun x => a⁻¹ • x, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.instSFiniteRestrict : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (s : Set α),
  MeasureTheory.SFinite (μ.restrict s)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_liftAt : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {n n' m : ℕ} {φ : L.BoundedFormula α n}
  {v : α → M} {xs : Fin (n + n') → M},
  m ≤ n →
    ((FirstOrder.Language.BoundedFormula.liftAt n' m φ).Realize v xs ↔
      φ.Realize v (xs ∘ fun i => if ↑i < m then Fin.castAdd n' i else i.addNat n'))
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_subset_neg : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] {s t : Finset α}, s ⊆ t → -s ⊆ -t
-- Lean.Meta.LazyDiscrTree
/-- Add an entry to the pre-discrimination tree. -/
Lean.Meta.LazyDiscrTree.PreDiscrTree.push : {α : Type} →
  Lean.Meta.LazyDiscrTree.PreDiscrTree α →
    Lean.Meta.LazyDiscrTree.Key → Lean.Meta.LazyDiscrTree.LazyEntry α → Lean.Meta.LazyDiscrTree.PreDiscrTree α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.w_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {j j' : J} (f : j ⟶ j') {Z : C}
  (h : F.obj j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (c.π.app j) (CategoryTheory.CategoryStruct.comp (F.map f) h) =
    CategoryTheory.CategoryStruct.comp (c.π.app j') h
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Two homomorphisms out of a free group are equal if they are equal on generators.

See note [partially-applied ext lemmas].  -/
FreeGroup.ext_hom : ∀ {α : Type u} {M : Type u_1} [inst : Monoid M] (f g : FreeGroup α →* M),
  (∀ (a : α), f (FreeGroup.of a) = g (FreeGroup.of a)) → f = g
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- In an `S` algebra `R`, the order of vanishing of `x : R` is equal to the order of vanishing
of `a • x` for `a` a unit in `S`.
 -/
Ring.ord_smul_of_isUnit : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_3} [inst_1 : CommRing S] [inst_2 : Algebra S R] {a : S},
  IsUnit a → ∀ (x : R), Ring.ord R (a • x) = Ring.ord R x
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.aleph0_lt_continuum : Cardinal.aleph0 < Cardinal.continuum
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.instMin : {V : Type u} → {G : SimpleGraph V} → Min G.Finsubgraph
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Filter.Tendsto.rpow_const_nhds_zero : ∀ {α : Type u_1} {l : Filter α} {f : α → ℝ} {p : ℝ},
  Filter.Tendsto f l (nhds 0) → 0 < p → Filter.Tendsto (fun t => f t ^ p) l (nhds 0)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.bot_lt_natCast : ∀ {α : Type u} [inst : AddMonoidWithOne α] [inst_1 : LT α] (n : ℕ), ⊥ < ↑n
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.instLawfulToBackwardSearcherModelCharDefaultBackwardSearcherForallBoolBeq : ∀ {c : Char}, String.Slice.Pattern.Model.LawfulToBackwardSearcherModel c
-- Mathlib.CategoryTheory.Limits.Connected
/-- (Impl). The obvious natural transformation from (X × K -) to K.  -/
CategoryTheory.ProdPreservesConnectedLimits.γ₂ : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] →
      {J : Type v₂} →
        [inst_2 : CategoryTheory.SmallCategory J] →
          {K : CategoryTheory.Functor J C} → (X : C) → K.comp (CategoryTheory.Limits.prod.functor.obj X) ⟶ K
-- Mathlib.Topology.Neighborhoods
isOpen_singleton_iff_nhds_eq_pure : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X), IsOpen {x} ↔ nhds x = pure x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.Cone.ofPullbackCone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
  (t :
    CategoryTheory.Limits.PullbackCone (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl)
      (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr)),
  (CategoryTheory.Limits.Cone.ofPullbackCone t).pt = t.pt
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.extractProofRapp : Lean.Environment → Lean.MVarId → Aesop.Rapp → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.LeibnizAdjunction.adj_counit_app_right : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) (adj₂ : F ⊣₂ G) (X₁ : CategoryTheory.Arrow C₁)
  [inst_3 : CategoryTheory.Limits.HasPullbacks C₂] [inst_4 : CategoryTheory.Limits.HasPushouts C₃]
  (X₃ : CategoryTheory.Arrow C₃),
  ((CategoryTheory.Functor.LeibnizAdjunction.adj F G adj₂ X₁).counit.app X₃).right =
    adj₂.homEquiv.symm
      (CategoryTheory.Limits.pullback.snd ((G.obj (Opposite.op X₁.left)).map X₃.hom) ((G.map X₁.hom.op).app X₃.right))
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.continuous_extend_one : ∀ {α' : Type u_3} {β : Type u_4} [inst : TopologicalSpace α'] [inst_1 : One β] [T2Space α']
  [inst_3 : TopologicalSpace β] {U : Set α'},
  IsOpen U → ∀ {f : ↑U → β}, Continuous f → HasCompactMulSupport f → Continuous (Function.extend Subtype.val f 1)
-- Mathlib.Algebra.Group.Action.Faithful
/-- `Monoid.toOppositeMulAction` is faithful on cancellative monoids.  -/
LeftCancelMonoid.to_faithfulSMul_mulOpposite : ∀ {α : Type u_3} [inst : LeftCancelMonoid α], FaithfulSMul αᵐᵒᵖ α
-- Mathlib.NumberTheory.Padics.Complex
/-- The norm on `ℂ_[p]` is compatible with the valuation.  -/
PadicComplex.norm_eq_norm : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ℂ_[p]), ‖x‖ = Valued.v.norm x
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousWithinAt.norm : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {s : Set α}
  {a : α}, ContinuousWithinAt f s a → ContinuousWithinAt (fun x => ‖f x‖) s a
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
/-- This shows `CStarAlgebra.approximateUnit` is a one-sided approximate unit, but this is marked
`private` because it is only used to prove `CStarAlgebra.increasingApproximateUnit`.  -/
_private.Mathlib.Analysis.CStarAlgebra.ApproximateUnit.0.CStarAlgebra.tendsto_mul_right_approximateUnit : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (m : A),
  Filter.Tendsto (fun x => x * m) (CStarAlgebra.approximateUnit A) (nhds m)