mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.congr_mono : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜},
  HasDerivWithinAt f f' s x → (∀ x ∈ t, f₁ x = f x) → f₁ x = f x → t ⊆ s → HasDerivWithinAt f₁ f' t x
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.id_F : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (S : CategoryTheory.SimplicialObject.Split C),
  (CategoryTheory.CategoryStruct.id S).F = CategoryTheory.CategoryStruct.id S.X
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.isDenseEmbedding_pureCauchy : ∀ {α : Type u} [inst : UniformSpace α], IsDenseEmbedding CauchyFilter.pureCauchy
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonianCycle.count_support_self : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a},
  p.IsHamiltonianCycle → List.count a p.support = 2
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.closure_sdiff_ssubset : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.Indep I → (I ∩ X).Nonempty → M.closure (I \ X) ⊂ M.closure I
-- Mathlib.AlgebraicGeometry.Group.Smooth
AlgebraicGeometry.pointEquivClosedPoint.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [inst_1 : IsAlgClosed K]
  (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [inst_2 : AlgebraicGeometry.LocallyOfFiniteType f],
  AlgebraicGeometry.pointEquivClosedPoint f =
    { toFun := fun p => ⟨↑p (IsLocalRing.closedPoint K), ⋯⟩,
      invFun := fun x => ⟨AlgebraicGeometry.pointOfClosedPoint f ↑x ⋯, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
/-- The precomposition of a spectral object with a functor.  -/
CategoryTheory.Triangulated.SpectralObject.precomp : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                [inst_6 : CategoryTheory.Pretriangulated C] →
                  CategoryTheory.Triangulated.SpectralObject C ι →
                    {ι' : Type u_4} →
                      [inst_7 : CategoryTheory.Category.{u_5, u_4} ι'] →
                        CategoryTheory.Functor ι' ι → CategoryTheory.Triangulated.SpectralObject C ι'
-- Lean.Meta.Sym.Arith.Poly
/-- `lcm m₁ m₂` returns the least common multiple of the given monomials.  -/
Lean.Grind.CommRing.Mon.lcm : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon
-- Mathlib.Order.UpperLower.Prod
UpperSet.instSProd : {α : Type u_1} →
  {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → SProd (UpperSet α) (UpperSet β) (UpperSet (α × β))
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.toOLeanEntry : Lean.Parser.ParserExtension.Entry → Lean.Parser.ParserExtension.OLeanEntry
-- Init.While
_private.Init.While.0.instNonemptySubtypePred : ∀ {α : Type u} {m : Type u → Type v} [inst : Monad m] {β : Type u} [Nonempty β] {f : α → m (α ⊕ β)} {a : α},
  Nonempty (Subtype (repeatM.Pred✝ f a))
-- Mathlib.Data.Set.Image
Set.forall_mem_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {p : β → Prop}, (∀ y ∈ f '' s, p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.parse.go : Lean.TSyntax `mcasesPat → Option Lean.Parser.Tactic.MCasesPat
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaMon_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] {X Y : CategoryTheory.Mon C} (f : X ⟶ Y),
  CategoryTheory.shrinkYonedaMon.{w, v, u}.map f = MonCat.shrinkFunctorMap (CategoryTheory.yonedaMon.map f)
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_succ_left : ∀ (R : Type u) [inst : Ring R] (n : ℕ),
  descPochhammer R (n + 1) = Polynomial.X * (descPochhammer R n).comp (Polynomial.X - 1)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RoiSliceData.mk : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.DTreeMap.Internal.Impl α β → Std.Roi α → Std.DTreeMap.Internal.RoiSliceData α β
-- Mathlib.GroupTheory.Finiteness
Subgroup.FG.finset_sup : ∀ {G : Type u_3} [inst : Group G] {ι : Type u_5} (s : Finset ι) (P : ι → Subgroup G), (∀ i ∈ s, (P i).FG) → (s.sup P).FG
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.top_ne_zero : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R], ⊤ ≠ 0
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_real_Icc_of_le : ∀ {a b : ℝ}, a ≤ b → MeasureTheory.volume.real (Set.Icc a b) = b - a
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.fixedField.algebra : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          (K : IntermediateField F E) → Algebra ↥K ↥(IntermediateField.fixedField K.fixingSubgroup)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.isUnit_iff_mul_inverse_cancel : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x : M₀}, IsUnit x ↔ x * Ring.inverse x = 1
-- Mathlib.Condensed.Solid
/-- The natural transformation `FintypeCat.toProfinite ⋙ profiniteSolid R ⟶ finFree R`
which is part of the assertion that `profiniteSolid R` is the (pointwise) right
Kan extension of `finFree R` along `FintypeCat.toProfinite`.  -/
Condensed.profiniteSolidCounit : (R : Type (u + 1)) → [inst : Ring R] → FintypeCat.toProfinite.comp (Condensed.profiniteSolid R) ⟶ Condensed.finFree R
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev.eq_1 : ∀ {s : String} (pos : s.Pos) (h : pos ≠ s.startPos), pos.prev h = String.Pos.ofToSlice (pos.toSlice.prev ⋯)
-- Mathlib.Algebra.Group.Action.Pi
Pi.addAction'.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {m : (i : ι) → AddMonoid (α i)}
  [inst : (i : ι) → AddAction (α i) (β i)], Pi.addAction' = { toVAdd := Pi.vadd', add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Combinatorics.Additive.SubsetSum
Finset.card_choose_two_lt_card_subsetSum_of_nonneg : ∀ {M : Type u_1} [inst : DecidableEq M] [inst_1 : AddCommMonoid M] {A : Finset M} [inst_2 : LinearOrder M]
  [IsOrderedCancelAddMonoid M], (∀ x ∈ A, 0 ≤ x) → A.card.choose 2 < A.subsetSum.card
-- Mathlib.Combinatorics.Quiver.Subquiver
/-- An `L`-labelling of a quiver assigns to every arrow an element of `L`.  -/
Quiver.Labelling : (V : Type u) → [Quiver V] → Sort u_1 → Sort (imax (u + 1) (u + 1) (u_2 + 1) u_1)
-- Mathlib.Algebra.Field.Basic
toLex_ratCast : ∀ {K : Type u_1} [inst : RatCast K] (n : ℚ), toLex ↑n = ↑n
-- Mathlib.Data.Multiset.Filter
Multiset.filter_filter : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (q : α → Prop) [inst_1 : DecidablePred q] (s : Multiset α),
  Multiset.filter p (Multiset.filter q s) = Multiset.filter (fun a => p a ∧ q a) s
-- Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
MeasureTheory.IsZeroOneMeasure.zero_one₀ : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.IsZeroOneMeasure μ]
  ⦃s : Set α⦄, MeasurableSet s → μ s = 0 ∨ μ s = 1
-- Mathlib.Data.ENat.Basic
ENat.WithBot.add_one_le_iff : ∀ {n : ℕ} {m : WithBot ℕ∞}, ↑n + 1 ≤ m ↔ ↑n < m
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabelPart.location? : Lean.Elab.InlayHintLabelPart → Option Lean.Elab.InlayHintLinkLocation
-- Mathlib.Algebra.Ring.Commute
sub_sq_comm : ∀ {R : Type u} [inst : CommRing R] (a b : R), (a - b) ^ 2 = (b - a) ^ 2
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Complex.betaIntegral_eq_Gamma_mul_div : ∀ (u v : ℂ), 0 < u.re → 0 < v.re → u.betaIntegral v = Complex.Gamma u * Complex.Gamma v / Complex.Gamma (u + v)
-- Mathlib.Analysis.Normed.Order.Lattice
HasSolidNorm.orderClosedTopology : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E],
  OrderClosedTopology E
-- Init.Data.AC
Lean.Data.AC.Context.evalList_sort_cons : ∀ {α : Sort u_1} (ctx : Lean.Data.AC.Context α),
  Std.Commutative ctx.op →
    ∀ (x : ℕ) (xs : List ℕ),
      Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort (x :: xs)) =
        Lean.Data.AC.evalList α ctx (x :: Lean.Data.AC.sort xs)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.eq : Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.Arith.Cutsat.UnsatProof
-- Mathlib.Order.Compare
ofDual_compares_ofDual : ∀ {α : Type u_1} [inst : LT α] {a b : αᵒᵈ} {o : Ordering},
  o.Compares (OrderDual.ofDual a) (OrderDual.ofDual b) ↔ o.Compares b a
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Under.preservesLimitsOfSize_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v, u} C]
  {Y : C} (f : X ⟶ Y),
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v, v, max u v, max u v} (CategoryTheory.Under.map f)
-- Mathlib.Analysis.Complex.Basic
/-- The module structure from `Module.complexToReal` is a normed space.  -/
NormedSpace.complexToReal : {E : Type u_1} → [inst : SeminormedAddCommGroup E] → [NormedSpace ℂ E] → NormedSpace ℝ E
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure.0.Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.match_3.eq_1 : ∀ (motive : Std.Tactic.BVDecide.Gate → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.Gate.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.Gate.xor) (h_3 : Unit → motive Std.Tactic.BVDecide.Gate.beq)
  (h_4 : Unit → motive Std.Tactic.BVDecide.Gate.or),
  (match Std.Tactic.BVDecide.Gate.and with
    | Std.Tactic.BVDecide.Gate.and => h_1 ()
    | Std.Tactic.BVDecide.Gate.xor => h_2 ()
    | Std.Tactic.BVDecide.Gate.beq => h_3 ()
    | Std.Tactic.BVDecide.Gate.or => h_4 ()) =
    h_1 ()
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- The property of morphisms in `SimplexCategory.Truncated 2` for
which `liftOfStrictSegal.app` is natural.  -/
SSet.Truncated.liftOfStrictSegal.naturalityProperty : {X Y : SSet.Truncated 2} →
  (f₀ :
      X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
        Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })) →
    (f₁ :
        X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
          Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })) →
      (∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
          f₀
              ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op))
                x) =
            (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op))
              (f₁ x)) →
        (∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
            f₀
                ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op))
                  x) =
              (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op))
                (f₁ x)) →
          Y.StrictSegal → CategoryTheory.MorphismProperty (SimplexCategory.Truncated 2)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.nonempty_support_finSuccEquiv : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R},
  f ≠ 0 → ((MvPolynomial.finSuccEquiv R n) f).support.Nonempty
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_1.eq_1 : ∀ {β β' : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (Option β')} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (h' : (f out).Property none)
  (h_1 : (h' : (f out).Property none) → motive ⟨none, h'⟩)
  (h_2 : (out' : β') → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩),
  (match ⟨none, h'⟩ with
    | ⟨none, h'⟩ => h_1 h'
    | ⟨some out', h'⟩ => h_2 out' h') =
    h_1 h'
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.row_map : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (A : Matrix m n α) (f : α → β) (i : m),
  (A.map f).row i = f ∘ A.row i
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsComplete.eq_1 : ∀ {α : Type u_1} (H : Hypergraph α), H.IsComplete = ∀ e ⊆ H.vertexSet, e ∈ H.edgeSet
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β}, MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → AEMeasurable f μa
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.minpoly_eq_X_pow_sub_C : ∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [ExpChar F q]
  [IsPurelyInseparable F E] (x : E), ∃ n y, minpoly F x = Polynomial.X ^ q ^ n - Polynomial.C y
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_le_smul : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {𝕜' : Type u_6} {c : 𝕜'} [inst_5 : NormedRing 𝕜'] [inst_6 : Module 𝕜' F]
  [inst_7 : SMulCommClass 𝕜 𝕜' F] [inst_8 : IsBoundedSMul 𝕜' F], p.radius ≤ (c • p).radius
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.apply.inj : ∀ {term : Aesop.RuleTerm} {md : Lean.Meta.TransparencyMode} {term_1 : Aesop.RuleTerm}
  {md_1 : Lean.Meta.TransparencyMode},
  Aesop.RuleTacDescr.apply term md = Aesop.RuleTacDescr.apply term_1 md_1 → term = term_1 ∧ md = md_1
-- Mathlib.Tactic.NormNum.Result
/-- Untyped version of `Result.isNNRat`.  -/
Mathlib.Meta.NormNum.Result'.isNNRat : Lean.Expr → ℚ → Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Meta.NormNum.Result'
-- Init.Data.Iterators.Basic
/-- Asserts that a certain iterator `it` could plausibly yield the value `out` after an arbitrary
number of steps.
 -/
Std.IterM.IsPlausibleIndirectOutput : {α β : Type w} → {m : Type w → Type w'} → [Std.Iterator α m β] → Std.IterM m β → β → Prop
-- Mathlib.Probability.Process.Filtration
MeasureTheory.measurableSet_of_filtration : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {s : Set Ω} {i : ι}, MeasurableSet s → MeasurableSet s
-- Aesop.RuleSet.Filter
Aesop.RuleFilter.matchesPhase : Aesop.RuleFilter → Aesop.PhaseName → Bool
-- Mathlib.Algebra.Free
Magma.AssocQuotient.instInhabited.eq_1 : ∀ {α : Type u} [inst : Mul α] [inst_1 : Inhabited α],
  Magma.AssocQuotient.instInhabited = { default := Magma.AssocQuotient.of default }
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- An embedding of complex shapes `e` satisfies `e.IsRelIff` if the implication
`e.rel` is an equivalence.  -/
ComplexShape.Embedding.IsRelIff : {ι : Type u_1} → {ι' : Type u_2} → {c : ComplexShape ι} → {c' : ComplexShape ι'} → c.Embedding c' → Prop
-- Mathlib.Order.UpperLower.Closure
IsAntichain.maximal_mem_lowerClosure_iff_mem : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {x : α},
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → (Maximal (fun x => x ∈ lowerClosure s) x ↔ x ∈ s)
-- Mathlib.MeasureTheory.Group.Arithmetic
instMeasurableEqOfMeasurableSingletonClassOfMeasurableSub₂ : ∀ {E : Type u_5} [inst : MeasurableSpace E] [inst_1 : AddGroup E] [MeasurableSingletonClass E] [MeasurableSub₂ E],
  MeasurableEq E
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.isClosedEmbedding : ∀ {α : Type u_4} {β : Type u_5} [inst : EMetricSpace α] [inst_1 : EMetricSpace β] {K : NNReal} {f : α → β}
  [CompleteSpace α], AntilipschitzWith K f → UniformContinuous f → Topology.IsClosedEmbedding f
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeries.StrictMonoOn : ∀ (G : Type u_1) [inst : AddGroup G],
  StrictMonoOn (AddSubgroup.upperCentralSeries G) (Set.Iic (AddGroup.nilpotencyClass G))
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.addTermInfoViews : Array Lean.Elab.Command.InductiveView → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
/-- The tautological section of `free I : SheafOfModules R` corresponding to `i : I`.  -/
SheafOfModules.freeSection : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] → {I : Type u} → I → (SheafOfModules.free I).sections
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- If `S / R` and `S' / R'` are algebras, `i : R' →+* R` and `j : S →+* S'` are injective ring
homomorphisms, such that `R' → R → S → S'` and `R' → S'` commute, then the rank of `S / R` is
smaller than or equal to the rank of `S' / R'`.  -/
Algebra.lift_rank_le_of_injective_injective : ∀ {R : Type w} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {R' : Type w'}
  {S' : Type v'} [inst_3 : CommSemiring R'] [inst_4 : Semiring S'] [inst_5 : Algebra R' S'] (i : R' →+* R)
  (j : S →+* S'),
  Function.Injective ⇑i →
    Function.Injective ⇑j →
      (j.comp (algebraMap R S)).comp i = algebraMap R' S' →
        Cardinal.lift.{v', v} (Module.rank R S) ≤ Cardinal.lift.{v, v'} (Module.rank R' S')
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.inclusion.coe_eq : ∀ {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst_1 : AddAction M α] (s : SubAddAction M α),
  ⇑s.inclusion = Subtype.val
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An additive subgroup of an additive group `G` is a subset containing 0, closed
under addition and additive inverse. 

[Wikidata Q466109](https://www.wikidata.org/wiki/Q466109) -/
AddSubgroup : (G : Type u_3) → [AddGroup G] → Type u_3
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
measurable_real_toNNReal : Measurable Real.toNNReal
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.balanceL_eq_balance : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size},
  Std.DTreeMap.Internal.Impl.balanceL k v l r hlb hrb hlr = Std.DTreeMap.Internal.Impl.balance k v l r hlb hrb ⋯
-- Mathlib.FieldTheory.FinTrdeg
FinTrdeg.exists_fg_isAlgebraic : ∀ (K : Type u_1) (L : Type u_2) {inst : Field K} {inst_1 : Field L} {inst_2 : Algebra K L} [self : FinTrdeg K L],
  ∃ E, E.FG ∧ Algebra.IsAlgebraic (↥E) L
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.opFunctor_obj : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R),
  (CategoryTheory.Comma.opFunctor L R).obj X =
    Opposite.op { left := Opposite.op X.right, right := Opposite.op X.left, hom := Opposite.op X.hom }
-- Aesop.Tracing
Aesop.ruleProvedEmoji : String
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.OplaxMonoidal]
  [inst_5 : G.LaxMonoidal] [adj.IsMonoidal] (X Y : D),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.LaxMonoidal.μ G X Y))
      (adj.counit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y))
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.ofConjAct_mul : ∀ {G : Type u_3} [inst : DivInvMonoid G] (x y : ConjAct G),
  ConjAct.ofConjAct (x * y) = ConjAct.ofConjAct x * ConjAct.ofConjAct y
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
SimpleGraph.card_edgeFinset_of_isExtremal_free : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V]
  [inst_1 : DecidableRel G.Adj], G.IsExtremal H.Free → G.edgeFinset.card = SimpleGraph.extremalNumber (Fintype.card V) H
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.pure_apply_of_ne : ∀ {α : Type u_1} (a a' : α), a' ≠ a → (PMF.pure a) a' = 0
-- Mathlib.CategoryTheory.Functor.FunctorHom
/-- Given a morphism `A' ⟶ A`, send a term of `HomObj F G A` to a term of `HomObj F G A'`.  -/
CategoryTheory.Functor.HomObj.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {F G : CategoryTheory.Functor C D} →
          {A A' : CategoryTheory.Functor C (Type w)} → (A' ⟶ A) → F.HomObj G A → F.HomObj G A'
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.DSmooth.isPlot : ∀ {X : Type u_1} [inst : DiffeologicalSpace X] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
  Diffeology.DSmooth p → Diffeology.IsPlot p
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.usize : UInt64 → Lean.Compiler.LCNF.LitValue
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphismClass.toTopHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : PartialOrder α] [inst_2 : OrderTop α]
  [inst_3 : Preorder β] [inst_4 : OrderTop β] [PseudoEpimorphismClass F α β], TopHomClass F α β
-- Init.Data.List.Erase
List.erase_append_left : ∀ {α : Type u_1} [inst : BEq α] {a : α} [LawfulBEq α] {l₁ : List α} (l₂ : List α),
  a ∈ l₁ → (l₁ ++ l₂).erase a = l₁.erase a ++ l₂
-- Mathlib.Algebra.Lie.AdjointAction.Derivation
/-- The adjoint action of a Lie algebra `L` on itself, seen as a morphism of Lie algebras from
`L` to its derivations.
Note the minus sign: this is chosen to so that `ad ⁅x, y⁆ = ⁅ad x, ad y⁆`.  -/
LieDerivation.ad : (R : Type u_1) →
  (L : Type u_2) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → L →ₗ⁅R⁆ LieDerivation R L L
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct.smulFn : Lean.Meta.Grind.Arith.Linear.NatStruct → Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_tensorObj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  Opposite.op (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (Opposite.op X) (Opposite.op Y)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.exists_pos : ∀ {M : Type u_1} [inst : CommMonoid M] {ζ : M} {k : ℕ}, ζ ^ k = 1 → k ≠ 0 → ∃ k' > 0, IsPrimitiveRoot ζ k'
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.comp_τ₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃) {Z : C} (h : S₃.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₂ h =
    CategoryTheory.CategoryStruct.comp φ₁₂.τ₂ (CategoryTheory.CategoryStruct.comp φ₂₃.τ₂ h)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.apply_one : ∀ {E : Type u_3} [inst : AddGroup E] [inst_1 : DecidableEq E] (x : E), 1 x = if x = 0 then 0 else 1
-- Init.Data.Vector.Lemmas
Vector.mapFinIdx_mk : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {f : (i : ℕ) → α → i < n → β} {xs : Array α} (h : xs.size = n),
  (Vector.mk xs h).mapFinIdx f = Vector.mk (xs.mapFinIdx fun i a h' => f i a ⋯) ⋯