mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.toSubmodule_injective : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M], Function.Injective ClosedSubmodule.toSubmodule
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_I₀ : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfRight 𝒰 f g).I₀ = 𝒰.I₀
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- In an s-finite space, among disjoint null-measurable sets, only countably many can have positive
measure.  -/
MeasureTheory.Measure.countable_meas_pos_of_disjoint_iUnion₀ : ∀ {α : Type u_1} {ι : Type u_4} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ]
  {As : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) →
    Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) As) → {i | 0 < μ (As i)}.Countable
-- Mathlib.Order.Filter.CountableSeparatingOn
Filter.EventuallyEq.of_forall_separating_preimage : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → β} (p : Set β → Prop)
  [HasCountableSeparatingOn β p Set.univ], (∀ (U : Set β), p U → f ⁻¹' U =ᶠ[l] g ⁻¹' U) → f =ᶠ[l] g
-- Mathlib.Topology.Compactification.StoneCech
ultrafilterBasis_is_basis : ∀ {α : Type u}, TopologicalSpace.IsTopologicalBasis (ultrafilterBasis α)
-- Mathlib.Analysis.Calculus.Deriv.AffineMap
AffineMap.hasDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {s : Set 𝕜} {x : 𝕜}, HasDerivWithinAt (⇑f) (f.linear 1) s x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_of_mul_le_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulRightMono α] {a b c d : α}, a * b ≤ c → d ≤ a → d * b ≤ c
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.instInitialCostructuredArrowOverToOver : ∀ {C₀ : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] (F : CategoryTheory.Functor C₀ C) (X : C) [F.Initial],
  (CategoryTheory.CostructuredArrow.toOver F X).Initial
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.RpcSession.keptAlive : ℕ → Lean.Server.FileWorker.RpcSession → Lean.Server.FileWorker.RpcSession
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The replacement expression obtained from the rewrite  -/
Mathlib.Tactic.LibraryRewrite.Rewrite.replacement : Mathlib.Tactic.LibraryRewrite.Rewrite → Lean.Expr
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor.obj S = S.composableArrows
-- Init.Data.SInt.Lemmas
Int64.toInt_ofIntLE : ∀ {x : ℤ} {h₁ : Int64.minValue.toInt ≤ x} {h₂ : x ≤ Int64.maxValue.toInt}, (Int64.ofIntLE x h₁ h₂).toInt = x
-- Mathlib.Algebra.Module.LinearMap.Basic
DomMulAct.smul_linearMap_apply : ∀ {R : Type u_1} {R' : Type u_2} {M : Type u_4} {M' : Type u_5} [inst : Semiring R] [inst_1 : Semiring R']
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M] [inst_5 : Module R' M'] {σ₁₂ : R →+* R'}
  {S' : Type u_6} [inst_6 : Monoid S'] [inst_7 : DistribMulAction S' M] [inst_8 : SMulCommClass R S' M] (a : S'ᵈᵐᵃ)
  (f : M →ₛₗ[σ₁₂] M') (x : M), (a • f) x = f (DomMulAct.mk.symm a • x)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.foldM_filterMapWithPostcondition.match_1.eq_2 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (x : Option γ) (h_1 : (c : γ) → motive (some c))
  (h_2 : (x : Option γ) → motive x),
  (∀ (c : γ), x = some c → False) →
    (match x with
      | some c => h_1 c
      | x => h_2 x) =
      h_2 x
-- Mathlib.Topology.Clopen
IsClopen.isOpen : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClopen s → IsOpen s
-- Std.Data.DHashMap.Internal.RawLemmas
/-- Variant of `get_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.DHashMap.Internal.Raw₀.Const.get_map' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → γ}
  {k : α} (h : (↑m).WF) {h' : (Std.DHashMap.Internal.Raw₀.map f m).contains k = true},
  Std.DHashMap.Internal.Raw₀.Const.get (Std.DHashMap.Internal.Raw₀.map f m) k h' =
    f (m.getKey k ⋯) (Std.DHashMap.Internal.Raw₀.Const.get m k ⋯)
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.one_le_prod_of_one_le : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] {l : List M}, (∀ x ∈ l, 1 ≤ x) → 1 ≤ l.prod
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.lineDerivOp_sum : ∀ {ι : Type u_1} {V : Type u_5} {E : Type u_6} {F : Type u_7} [inst : AddCommGroup V] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : LineDeriv V E F] [LineDerivAdd V E F] (v : V) (f : ι → E) (s : Finset ι),
  LineDeriv.lineDerivOp v (∑ i ∈ s, f i) = ∑ i ∈ s, LineDeriv.lineDerivOp v (f i)
-- Lean.Widget.UserWidget
Lean.Widget.instInhabitedUserWidgetDefinition : Inhabited Lean.Widget.UserWidgetDefinition
-- Mathlib.Topology.Connected.LocallyConnected
locallyConnectedSpace_iff_hasBasis_isOpen_isConnected : ∀ {α : Type u} [inst : TopologicalSpace α],
  LocallyConnectedSpace α ↔ ∀ (x : α), (nhds x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.rejected.injEq : ∀ {s : String.Slice} (startPos endPos startPos_1 endPos_1 : s.Pos),
  (String.Slice.Pattern.SearchStep.rejected startPos endPos =
      String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1) =
    (startPos = startPos_1 ∧ endPos = endPos_1)
-- Lean.Parser.Term
Lean.Parser.Term.debugAssert.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
/-- An auxiliary lemma en route to `RootPairing.finrank_corootSpan_eq`.  -/
_private.Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate.0.RootPairing.finrank_corootSpan_le : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  (S : Type u_5) [inst_6 : CommRing S] [IsDomain R] [IsDomain S] [inst_9 : Algebra S R] [FaithfulSMul S R]
  [P.IsValuedIn S] [inst_12 : Module S M] [IsScalarTower S R M] [inst_14 : Module S N] [IsScalarTower S R N]
  [P.IsAnisotropic], Module.finrank S ↥(P.corootSpan S) ≤ Module.finrank S ↥(P.rootSpan S)
-- Mathlib.Computability.TuringMachine.Tape
/-- Move the tape in response to a motion of the Turing machine. Note that `T.move Dir.left` makes
`T.left` smaller; the Turing machine is moving left and the tape is moving right.  -/
Turing.Tape.move : {Γ : Type u_1} → [inst : Inhabited Γ] → Turing.Dir → Turing.Tape Γ → Turing.Tape Γ
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.rootSystem_pairing_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] (H : LieSubalgebra K L)
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : ↥LieSubalgebra.root),
  (LieAlgebra.IsKilling.rootSystem H).pairing β α = ↑β (LieAlgebra.IsKilling.coroot ↑α)
-- Lean.Meta.Tactic.Simp.Main
/-- Unfold definition even if it is not marked as `@[reducible]`.
Remark: We never unfold irreducible definitions. Mathlib relies on that in the implementation of the
command `irreducible_def`.
 -/
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.unfoldDefinitionAny? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.ins_toList : ∀ {α : Type u_1} {t : RBTree.RBNode α} {p : RBTree.RBNode.Path α}, (p.ins t).toList = p.withList t.toList
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.congr_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) {T : Type u_3} [inst_3 : Semiring T] (w : AbsoluteValue T S) (f : R ≃+* T) (x : WithAbs v),
  (WithAbs.congr v w f) x = WithAbs.toAbs w (f x.ofAbs)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_alter_of_beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (k == k') = true → (k' ∈ Std.DHashMap.Const.alter m k f ↔ (f (Std.DHashMap.Const.get? m k)).isSome = true)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin_toMatrix : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂),
  (Matrix.toLin v₁ v₂) ((LinearMap.toMatrix v₁ v₂) f) = f
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_fun_neg_iff : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {s : Set α}
  {μ : MeasureTheory.Measure α} {f : α → E},
  MeasureTheory.IntegrableOn (fun x => -f x) s μ ↔ MeasureTheory.IntegrableOn f s μ
-- Aesop.Frontend.Tactic
_private.Aesop.Frontend.Tactic.0.Aesop.Frontend.TacticConfig.parse.go : Lean.MVarId → Bool → Array (Lean.TSyntax `Aesop.tactic_clause) → Lean.Elab.TermElabM Aesop.Frontend.TacticConfig
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.insertMany_list_singleton : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {k : α} {v : β},
  t.insertMany [(k, v)] = t.insert k v
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.lit.inj : ∀ {a a_1 : Lean.Literal}, Lean.Meta.LazyDiscrTree.Key.lit a = Lean.Meta.LazyDiscrTree.Key.lit a_1 → a = a_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_eq_of_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) (h : (↑m₁).Equiv ↑m₂) {k : α}
  (h' : m₁.contains k = true), m₁.getKey k h' = m₂.getKey k ⋯
-- Mathlib.Algebra.Star.Conjneg
conjneg_zero : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R], conjneg 0 = 0
-- Init.Prelude
/-- Converts a `String` to a `Name` without performing any parsing. `mkSimple s` is short for `.str .anonymous s`.

This means that `mkSimple "a.b"` is the name `«a.b»`, not `a.b`.
 -/
Lean.Name.mkSimple : String → Lean.Name
-- Mathlib.Analysis.Asymptotics.Lemmas
ContinuousOn.isBigOWith_rev_principal : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : TopologicalSpace α] {s : Set α} {f : α → E}
  [inst_1 : NormedAddGroup E] [inst_2 : SeminormedAddGroup F],
  ContinuousOn f s →
    IsCompact s →
      (∀ i ∈ s, f i ≠ 0) →
        ∀ (c : F), Asymptotics.IsBigOWith (‖c‖ / sInf (norm '' f '' s)) (Filter.principal s) (fun x => c) f
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.hasColimits_monCat : CategoryTheory.Limits.HasColimits MonCat
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.isBase_compl_iff_maximal_disjoint_isBase : ∀ {α : Type u_1} {M : Matroid α} {B : Set α},
  autoParam (B ⊆ M.E) Matroid.isBase_compl_iff_maximal_disjoint_isBase._auto_1 →
    (M.IsBase (M.E \ B) ↔ Maximal (fun I => I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) B)
-- Mathlib.RingTheory.PicardGroup
/-- When a flat `R`-module `M` is embedded as a submodule of a faithful `R`-algebra `A`,
the multiplication map induces an isomorphism `A ⊗[R] M ≃ₗ[A] A`.  -/
Module.Flat.tensorSubmoduleAlgebraEquiv : {R : Type u} →
  {M : Type v} →
    {A : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] →
                (e : TensorProduct R A M ≃ₗ[A] A) →
                  [Module.Flat R M] → [FaithfulSMul R A] → TensorProduct R A ↥(Module.Flat.submoduleAlgebra e) ≃ₗ[A] A
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_add_left_image : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, ⋃ a ∈ s, (fun x => a + x) '' t = s + t
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.symm_bijective : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β], Function.Bijective OrderRingIso.symm
-- Mathlib.Algebra.Group.Hom.Defs
/-- `AddMonoidHom` down-cast to an `AddHom`, forgetting the 0-preserving property.  -/
AddMonoidHom.coeToAddHom : {M : Type u_4} → {N : Type u_5} → [inst : AddZero M] → [inst_1 : AddZero N] → Coe (M →+ N) (M →ₙ+ N)
-- Mathlib.Topology.Order.IsLUB
/-- This is an analogue of `Dense.continuous_inf` for functions taking values in a conditionally
complete linear order. The assumption of `BddBelow (range f)` is not needed in this theorem.  -/
Dense.ciInf' : ∀ {γ : Type u_2} {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α]
  [ClosedIciTopology α] {f : γ → α} [inst_3 : TopologicalSpace γ] {S : Set γ},
  Dense S → Continuous f → ⨅ s, f ↑s = ⨅ i, f i
-- Mathlib.Algebra.Lie.TraceForm
LieModule.traceForm_apply_apply : ∀ (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] (x y : L),
  ((LieModule.traceForm R L M) x) y = (LinearMap.trace R M) ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y)
-- Mathlib.Algebra.Group.Basic
add_eq_left : ∀ {M : Type u_4} [inst : AddMonoid M] [IsLeftCancelAdd M] {a b : M}, a + b = a ↔ b = 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.insertManyIfNewUnit_list_equiv_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} {l : List α},
  (m.insertManyIfNewUnit l).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) m l)
-- Mathlib.Topology.Algebra.AffineSubspace
ContinuousAffineEquiv.affineSubspaceMap_apply_symm_apply : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] (e : P ≃ᴬ[R] Q) (s : AffineSubspace R P)
  [inst_9 : Nonempty ↥s] (x : ↥(AffineSubspace.map (↑↑e) s)), e ↑((e.affineSubspaceMap s).symm x) = ↑x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_erase_le_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k km kme : α} (hkme : (t.erase k).maxKey? = some kme), t.maxKey?.get ⋯ = km → (cmp kme km).isLE = true
-- Init.Data.String.Legacy
/-- Auxiliary for `splitOn`. Preconditions:
* `sep` is not empty
* `b <= i` are indexes into `s`
* `j` is an index into `sep`, and not at the end

It represents the state where we have currently parsed some split parts into `r` (in reverse order),
`b` is the beginning of the string / the end of the previous match of `sep`, and the first `j` bytes
of `sep` match the bytes `i-j .. i` of `s`.
 -/
String.splitOnAux : String → String → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw → List String → List String
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} {fallback : β a}, t.contains a = false → t.getD a fallback = fallback
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.mkHom.congr_simp : ∀ {M N : Type u} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N] (f f_1 : NormedAddGroupHom M N)
  (e_f : f = f_1) (i : f.NormNoninc), SemiNormedGrp₁.mkHom f i = SemiNormedGrp₁.mkHom f_1 ⋯
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Comma.mk.congr_simp : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  (toComma toComma_1 : CategoryTheory.Comma L R) (e_toComma : toComma = toComma_1) (prop : P toComma.hom),
  { toComma := toComma, prop := prop } = { toComma := toComma_1, prop := ⋯ }
-- Mathlib.Algebra.Group.Defs
IsMulCommutative.instCommGroup.eq_1 : ∀ {G : Type u_2} [inst : Group G] [inst_1 : IsMulCommutative G],
  IsMulCommutative.instCommGroup = { toGroup := inst, mul_comm := ⋯ }
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.lift_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] {i : R →+* T} {x : T} (hx : Polynomial.eval₂ i x f = 0),
  (h.lift i x hx) h.root = x
-- Aesop.Rule.Name
Aesop.PhaseName.instOrd : Ord Aesop.PhaseName
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- The ring homomorphism of additive monoid algebras induced by a homomorphism of the base rings.
 -/
AddMonoidAlgebra.mapRingHom : {R : Type u_3} →
  {S : Type u_4} →
    (M : Type u_6) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → [inst_2 : AddMonoid M] → (R →+* S) → AddMonoidAlgebra R M →+* AddMonoidAlgebra S M
-- Init.Data.UInt.Bitwise
UInt32.not_ne_self : ∀ {a : UInt32}, ~~~a ≠ a
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- If two functions differ only on a discrete set, then their characteristic functions agree, except
perhaps at radius 0.
 -/
ValueDistribution.characteristic_congr_codiscrete : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {a : WithTop E} {r : ℝ},
  f =ᶠ[Filter.codiscrete ℂ] g → r ≠ 0 → ValueDistribution.characteristic f a r = ValueDistribution.characteristic g a r
-- Init.Data.Nat.Lemmas
Nat.le_pow : ∀ {a b : ℕ}, 0 < b → a ≤ a ^ b
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivary_iff_forall_smul_nonpos`. -/
Antivary.sub_smul_sub_nonpos : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β}, Antivary f g → ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0
-- Mathlib.Data.Fin.Embedding
Function.Embedding.setValue.congr_simp : ∀ {α : Sort u_1} {β : Sort u_2} (f f_1 : α ↪ β),
  f = f_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (b b_1 : β),
          b = b_1 →
            ∀ {inst : (a' : α) → Decidable (a' = a)} [inst_1 : (a' : α) → Decidable (a' = a_1)]
              {inst_2 : (a' : α) → Decidable (f a' = b)} [inst_3 : (a' : α) → Decidable (f_1 a' = b_1)],
              f.setValue a b = f_1.setValue a_1 b_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Group.covariant_swap_iff_contravariant_swap : ∀ {N : Type u_2} {r : N → N → Prop} [inst : Group N],
  Covariant N N (Function.swap fun x1 x2 => x1 * x2) r ↔ Contravariant N N (Function.swap fun x1 x2 => x1 * x2) r
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_conj_eq : ∀ (f : CircleDeg1Liftˣ) (g : CircleDeg1Lift), (↑f * g * ↑f⁻¹).translationNumber = g.translationNumber
-- Lean.Parser.Command
Lean.Parser.Command.abbrev : Lean.Parser.Parser
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.OneLine.State.tags : Lean.PrettyPrinter.OneLine.State → List (ℕ × Std.Format)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_add_left : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → ∀ (g : α → ENNReal), μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `sInf s = 0` when `s` is an empty set of reals, it suffices to show that all elements of `s`
are at least some nonpositive number `a` to show that `a ≤ sInf s`.

See also `le_csInf`.  -/
Real.le_sInf : ∀ {s : Set ℝ} {a : ℝ}, (∀ x ∈ s, a ≤ x) → a ≤ 0 → a ≤ sInf s
-- Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots
/-- Adjoining all `p`-th root to a field of (exponential) characteristic `p`.  -/
AdjoinPthRoots : Type u_1 → Type u_1
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_eq_zero : ∀ {V : Type u_1} {G : SimpleGraph V}, G.vertexCoverNum = 0 ↔ G = ⊥
-- Init.Grind.Lemmas
Lean.Grind.Semiring.mul_one_congr : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] {a b : α}, b = 1 → a * b = a
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.SmallCategoryOfSet.mk : {Ω : Type w} →
  (obj : Set Ω) →
    (hom : ↑obj → ↑obj → Set Ω) →
      (id : (X : ↑obj) → ↑(hom X X)) →
        (comp : {X Y Z : ↑obj} → ↑(hom X Y) → ↑(hom Y Z) → ↑(hom X Z)) →
          autoParam (∀ {X Y : ↑obj} (f : ↑(hom X Y)), comp (id X) f = f)
              CategoryTheory.SmallCategoryOfSet.id_comp._autoParam →
            autoParam (∀ {X Y : ↑obj} (f : ↑(hom X Y)), comp f (id Y) = f)
                CategoryTheory.SmallCategoryOfSet.comp_id._autoParam →
              autoParam
                  (∀ {X Y Z T : ↑obj} (f : ↑(hom X Y)) (g : ↑(hom Y Z)) (h : ↑(hom Z T)),
                    comp (comp f g) h = comp f (comp g h))
                  CategoryTheory.SmallCategoryOfSet.assoc._autoParam →
                CategoryTheory.SmallCategoryOfSet Ω
-- Mathlib.Util.Notation3
/-- Represents a key to use when registering the `delab` attribute for a delaborator.
We use this to handle overapplication.
 -/
Mathlib.Notation3.DelabKey : Type
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given two points in an affine subspace, the angles between those two points at two other
points on the same side of that subspace have the same sign.  -/
AffineSubspace.SSameSide.oangle_sign_eq : ∀ {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)]
  {s : AffineSubspace ℝ P} {p₁ p₂ p₃ p₄ : P},
  p₁ ∈ s →
    p₂ ∈ s → s.SSameSide p₃ p₄ → (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₁ p₃ p₂).sign
-- Init.Data.Array.Lemmas
Array.all_flatMap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {p : β → Bool},
  (Array.flatMap f xs).all p = xs.all fun a => (f a).all p
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.IsProper.mk : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore},
  (∀ (s : h.ι), (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS) → h.IsProper
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.forget₂_module_map : ∀ (R : Type u) [inst : CommRing R] {X Y : AlgCat R} (f : X ⟶ Y),
  (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)).map f = ModuleCat.ofHom (AlgCat.Hom.hom f).toLinearMap