mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.w : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} (g : F.obj a ⟶ Y),
  CategoryTheory.CategoryStruct.comp (hf.fst g) f = CategoryTheory.CategoryStruct.comp (F.map (hf.snd g)) g
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.zero_smul_set_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] (s : Set β), 0 • s ⊆ 0
-- Mathlib.RingTheory.Unramified.Basic
/-- This holds in general for epimorphisms.  -/
Algebra.FormallyUnramified.of_surjective : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} {B : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallyUnramified R A] (f : A →ₐ[R] B),
  Function.Surjective ⇑f → Algebra.FormallyUnramified R B
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_eq_self_sub_bdiv_mul : ∀ (x : ℤ) (m : ℕ), x.bmod m = x - x.bdiv m * ↑m
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instVAddCommClassForall : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} {N : Type u_4} [inst : VAdd M α] [inst_1 : VAdd N β],
  VAddCommClass Mᵈᵃᵃ N (α → β)
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
LieAdmissibleAlgebra.toModule : {R : Type u_1} →
  {L : Type u_2} → {inst : CommRing R} → {inst_1 : LieAdmissibleRing L} → [self : LieAdmissibleAlgebra R L] → Module R L
-- Mathlib.CategoryTheory.CommSq
/-- The lift.  -/
CategoryTheory.CommSq.LiftStruct.l : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A B X Y : C} →
      {f : A ⟶ X} →
        {i : A ⟶ B} → {p : X ⟶ Y} → {g : B ⟶ Y} → {sq : CategoryTheory.CommSq f i p g} → sq.LiftStruct → (B ⟶ X)
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Delaborates a function application in explicit mode.
* If `insertExplicit` is true, then ensures the head syntax is wrapped with `@`.
* If `fieldNotation` is true, then allows the application to be pretty printed using field notation.
  Field notation will not be used when `insertExplicit` is true.
 -/
Lean.PrettyPrinter.Delaborator.delabAppExplicitCore : Bool →
  ℕ →
    (Bool → Lean.PrettyPrinter.Delaborator.Delab) →
      Array Lean.PrettyPrinter.Delaborator.ParamKind → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.card_support_trinomial : ∀ {R : Type u} [inst : Semiring R] {k m n : ℕ},
  k < m →
    m < n →
      ∀ {x y z : R},
        x ≠ 0 →
          y ≠ 0 →
            z ≠ 0 →
              (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m +
                      Polynomial.C z * Polynomial.X ^ n).support.card =
                3
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- Given two triples of non-collinear points, if the lines determined by corresponding pairs of
points are parallel, then the vectors between corresponding pairs of points are all related by the
same nonzero scale factor. (The formal statement is slightly more general.)  -/
exists_eq_smul_of_parallel : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ p₄ p₅ p₆ : P},
  p₂ ∉ line[k, p₁, p₃] →
    line[k, p₁, p₂].Parallel line[k, p₄, p₅] →
      line[k, p₅, p₆].direction ≤ line[k, p₂, p₃].direction →
        line[k, p₆, p₄].direction ≤ line[k, p₃, p₁].direction →
          ∃ r, r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0to1.tr.match_3.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} (motive : Turing.TM0to1.Λ' Γ Λ → Sort u_3) (q : Λ)
  (h_1 : (q : Λ) → motive (Turing.TM0to1.Λ'.normal q))
  (h_2 : (d : Turing.Dir) → (q : Λ) → motive (Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.move d) q))
  (h_3 : (a : Γ) → (q : Λ) → motive (Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.write a) q)),
  (match Turing.TM0to1.Λ'.normal q with
    | Turing.TM0to1.Λ'.normal q => h_1 q
    | Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.move d) q => h_2 d q
    | Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.write a) q => h_3 a q) =
    h_1 q
-- Mathlib.Algebra.Notation.Support
Function.support_comp_eq_preimage : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Zero M] (g : κ → M) (f : ι → κ),
  Function.support (g ∘ f) = f ⁻¹' Function.support g
-- Mathlib.Order.Interval.Finset.Floor
Nat.cast_mem_Ioo_iff : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [inst_2 : FloorSemiring α] {a b : α} {n : ℕ},
  0 ≤ a → (↑n ∈ Set.Ioo a b ↔ n ∈ Finset.Ioo ⌊a⌋₊ ⌈b⌉₊)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_le_max?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k km kmi : α},
  t.max? = some km → (t.insert k).max?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.integral_eq' : ∀ {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [inst : NormedAddCommGroup E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_1 : NormedSpace ℝ E] [inst_2 : NormedRing 𝕜] [inst_3 : Module 𝕜 E]
  [inst_4 : IsBoundedSMul 𝕜 E] [inst_5 : SMulCommClass ℝ 𝕜 E] [inst_6 : CompleteSpace E]
  (f : ↥(MeasureTheory.Lp E 1 μ)), MeasureTheory.L1.integral f = (MeasureTheory.L1.integralCLM' 𝕜) f
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.op_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (h : f.MulStruct g fg i) {j : Fin n} (hij : autoParam (i.rev = j) SSet.PtSimplex.MulStruct.op._auto_1),
  (h.op hij).map = SSet.yonedaEquiv.symm (SSet.opObjEquiv.symm (SSet.yonedaEquiv h.map))
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'_zero : ∀ {α : Type u_1}, RegularExpression.matches' 0 = 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ContinuousOn.cpow : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f g : α → ℂ} {s : Set α},
  ContinuousOn f s → ContinuousOn g s → (∀ a ∈ s, f a ∈ Complex.slitPlane) → ContinuousOn (fun x => f x ^ g x) s
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- The equivalence between `AddCircle p` and the half-open interval `[a, a + p)`, whose inverse
is the natural quotient map.  -/
AddCircle.equivIco : {𝕜 : Type u_1} →
  [inst : AddCommGroup 𝕜] →
    (p : 𝕜) →
      [inst_1 : LinearOrder 𝕜] →
        [IsOrderedAddMonoid 𝕜] → [hp : Fact (0 < p)] → (a : 𝕜) → [Archimedean 𝕜] → AddCircle p ≃ ↑(Set.Ico a (a + p))
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.hasCoeToOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → Coe (CategoryTheory.Pseudofunctor B C) (CategoryTheory.OplaxFunctor B C)
-- Init.Data.SInt.Bitwise
Int32.toInt_not : ∀ (a : Int32), (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 32)
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.coe_of : ∀ (M : Type u) [inst : AddMonoid M], ↑(AddMonCat.of M) = M
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.subtype_eq_val : ∀ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M), ⇑p.subtype = Subtype.val
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.State.mk.injEq : ∀ (levelNames : List Lean.Name) (syntheticMVars : Lean.MVarIdMap Lean.Elab.Term.SyntheticMVarDecl)
  (pendingMVars : List Lean.MVarId) (mvarErrorInfos : List Lean.Elab.Term.MVarErrorInfo)
  (levelMVarErrorInfos : List Lean.Elab.Term.LevelMVarErrorInfo) (mvarArgNames : Lean.MVarIdMap Lean.Name)
  (letRecsToLift : List Lean.Elab.Term.LetRecToLift) (levelNames_1 : List Lean.Name)
  (syntheticMVars_1 : Lean.MVarIdMap Lean.Elab.Term.SyntheticMVarDecl) (pendingMVars_1 : List Lean.MVarId)
  (mvarErrorInfos_1 : List Lean.Elab.Term.MVarErrorInfo)
  (levelMVarErrorInfos_1 : List Lean.Elab.Term.LevelMVarErrorInfo) (mvarArgNames_1 : Lean.MVarIdMap Lean.Name)
  (letRecsToLift_1 : List Lean.Elab.Term.LetRecToLift),
  ({ levelNames := levelNames, syntheticMVars := syntheticMVars, pendingMVars := pendingMVars,
        mvarErrorInfos := mvarErrorInfos, levelMVarErrorInfos := levelMVarErrorInfos, mvarArgNames := mvarArgNames,
        letRecsToLift := letRecsToLift } =
      { levelNames := levelNames_1, syntheticMVars := syntheticMVars_1, pendingMVars := pendingMVars_1,
        mvarErrorInfos := mvarErrorInfos_1, levelMVarErrorInfos := levelMVarErrorInfos_1,
        mvarArgNames := mvarArgNames_1, letRecsToLift := letRecsToLift_1 }) =
    (levelNames = levelNames_1 ∧
      syntheticMVars = syntheticMVars_1 ∧
        pendingMVars = pendingMVars_1 ∧
          mvarErrorInfos = mvarErrorInfos_1 ∧
            levelMVarErrorInfos = levelMVarErrorInfos_1 ∧
              mvarArgNames = mvarArgNames_1 ∧ letRecsToLift = letRecsToLift_1)
-- Lean.Environment
_private.Lean.Environment.0.Lean.mkIRData : Lean.Environment → Lean.ModuleData
-- Mathlib.Logic.Encodable.Basic
/-- **Alias** of `Encodable.decode₂_isPartialInv`. -/
Encodable.decode₂_is_partial_inv : ∀ {α : Type u_1} [inst : Encodable α], Function.IsPartialInv Encodable.encode (Encodable.decode₂ α)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.alterKey.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (k : α) (f : Option (β k) → Option (β k))
  (l : List ((a : α) × β a)),
  Std.Internal.List.alterKey k f l =
    match f (Std.Internal.List.getValueCast? k l) with
    | none => Std.Internal.List.eraseKey k l
    | some v => Std.Internal.List.insertEntry k v l
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.degree_le_zero_iff_eq_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → (p.degree ≤ 0 ↔ p = 1)
-- Mathlib.Order.Interval.Finset.Defs
/-- A `LocallyFiniteOrder` can be transferred across an order isomorphism.  -/
LocallyFiniteOrder.ofOrderIsoClass : {F : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : Preorder M] →
        [inst_1 : Preorder N] →
          [inst_2 : EquivLike F M N] → [OrderIsoClass F M N] → F → [LocallyFiniteOrder N] → LocallyFiniteOrder M
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prodH : {ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    {L₁ : Type u_3} →
      {L₂ : Type u_4} →
        [inst : Finite ι₁] →
          [inst_1 : Finite ι₂] →
            (eι : ι₁ ≃ ι₂) →
              [inst_2 : LieRing L₁] →
                [inst_3 : LieRing L₂] →
                  {R : Type u_5} →
                    [inst_4 : CommRing R] →
                      [inst_5 : LieAlgebra R L₁] →
                        {H₁ : LieSubalgebra R L₁} →
                          (b₁ : LieAlgebra.Basis ι₁ H₁) →
                            [inst_6 : LieAlgebra R L₂] →
                              {H₂ : LieSubalgebra R L₂} →
                                (b₂ : LieAlgebra.Basis ι₂ H₂) → ι₁ → ↥(LieAlgebra.Basis.prod✝ eι b₁ b₂)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_mul_eq_opow_omega0 : ∀ {a b : Ordinal.{u_1}}, 0 < b → b ≤ a ^ Ordinal.omega0 → Ordinal.nfp (fun x => a * x) b = a ^ Ordinal.omega0
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- A functor reflecting larger cofiltered limits also reflects smaller cofiltered limits.  -/
CategoryTheory.Limits.reflectsCofilteredLimitsOfSize_of_univLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
  [CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
-- Mathlib.CategoryTheory.UnivLE
instFullWitness : ∀ [inst : UnivLE.{max u v, v}], UnivLE.witness.Full
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The map induced on `G`-invariant elements by a continuous intertwining map.  -/
ContIntertwiningMap.mapInvariants : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π : ContRepresentation R G V} →
                              {π' : ContRepresentation R G W} →
                                ContIntertwiningMap π π' → ↥π.invariants →L[R] ↥π'.invariants
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.category.sizeOf_spec : ∀ (catName declName : Lean.Name) (behavior : Lean.Parser.LeadingIdentBehavior),
  sizeOf (Lean.Parser.ParserExtension.Entry.category catName declName behavior) =
    1 + sizeOf catName + sizeOf declName + sizeOf behavior
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.Key.w : Std.Tactic.BVDecide.BVExpr.Cache.Key → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- The restriction of a morphism of graphs to induced subgraphs.  -/
SimpleGraph.induceHom : {V : Type u_1} →
  {W : Type u_2} →
    {G : SimpleGraph V} →
      {G' : SimpleGraph W} →
        {s : Set V} →
          {t : Set W} → (φ : G →g G') → Set.MapsTo (⇑φ) s t → SimpleGraph.induce s G →g SimpleGraph.induce t G'
-- Mathlib.GroupTheory.GroupAction.Pointwise
Set.MapsTo.vadd_set : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β]
  [inst_2 : FunLike F α β] [AddActionHomClass F M α β] {f : F} {s : Set α} {t : Set β},
  Set.MapsTo (⇑f) s t → ∀ (c : M), Set.MapsTo (⇑f) (c +ᵥ s) (c +ᵥ t)
-- Mathlib.Order.Hom.BoundedLattice
Codisjoint.map : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : FunLike F α β]
  [inst_3 : OrderTop α] [inst_4 : OrderTop β] [TopHomClass F α β] [SupHomClass F α β] {a b : α} (f : F),
  Codisjoint a b → Codisjoint (f a) (f b)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- Transport a non-unital star subalgebra via a non-unital star algebra homomorphism.  -/
NonUnitalStarSubalgebra.map : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalNonAssocSemiring B] →
                  [inst_5 : Module R B] →
                    [inst_6 : Star B] →
                      [inst_7 : FunLike F A B] →
                        [NonUnitalAlgHomClass F R A B] →
                          [StarHomClass F A B] → F → NonUnitalStarSubalgebra R A → NonUnitalStarSubalgebra R B
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.instNonemptyOfNontrivial : ∀ {R : Type u} [inst : CommSemiring R] [Nontrivial R], Nonempty (PrimeSpectrum R)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_two_nsmul_eq_neg_sign_iff : ∀ {θ : Real.Angle}, (2 • θ).sign = -θ.sign ↔ θ = 0 ∨ Real.pi / 2 < |θ.toReal|
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- This lemma will be immediately superseded by `ext`, below.  -/
_private.Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms.0.CategoryTheory.Limits.HasZeroMorphisms.ext_aux : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I J : CategoryTheory.Limits.HasZeroMorphisms C),
  (∀ (X Y : C), Zero.zero = Zero.zero) → I = J
-- Lean.Linter.Init
/-- State of `linterSetsExt`.

`merged` is the queryable union of all sources (builtins folded in at env creation,
imported entries from oleans, and locally added entries). `localEntries` tracks entries
added in the current module so they can be exported into the olean.
 -/
Lean.Linter.LinterSetsState : Type
-- Mathlib.Data.List.Sort
List.Perm.eq_reverse_of_sortedLE_of_sortedGE : ∀ {α : Type u_1} [inst : PartialOrder α] {l₁ l₂ : List α}, l₁.Perm l₂ → l₁.SortedLE → l₂.SortedGE → l₁ = l₂.reverse
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instMonoid.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Monoid M],
  Filter.Germ.instMonoid =
    { toSemigroup := Filter.Germ.instSemigroup, toOne := Filter.Germ.instOne, one_mul := ⋯, mul_one := ⋯,
      npow := fun n a => a ^ n, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Two vector spaces are isomorphic if they have the same dimension.  -/
nonempty_linearEquiv_of_lift_rank_eq : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M] [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [Module.Free R M'] [StrongRankCondition R],
  Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M') → Nonempty (M ≃ₗ[R] M')
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.comp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F G H : CategoryTheory.LaxBraidedFunctor C D} (α : F ⟶ G) (β : G ⟶ H),
  (CategoryTheory.CategoryStruct.comp α β).hom = CategoryTheory.CategoryStruct.comp α.hom β.hom
-- Aesop.Main
Aesop.evalAesop : Lean.Elab.Tactic.Tactic
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_sdiff_le_iff_le_add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ → s ⊆ t → μ s ≠ ⊤ → ∀ {ε : ENNReal}, μ (t \ s) ≤ ε ↔ μ t ≤ μ s + ε
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_g : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₁.g = CategoryTheory.Limits.biprod.snd
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_transpose_iff : ∀ {α : Type u_1} {n : Type u_3} {A : Matrix n n α}, A.transpose.IsSymm ↔ A.IsSymm
-- Mathlib.Order.Cover
WCovBy.Ioo_eq : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⩿ b → Set.Ioo a b = ∅
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
/-- Coercion from `E →SLₚₜ[σ] F` to `E →ₛₗ[σ] F` as a `𝕜₂`-linear map.  -/
PointwiseConvergenceCLM.coeLMₛₗ : {𝕜₁ : Type u_4} →
  {𝕜₂ : Type u_5} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          (E : Type u_7) →
            (F : Type u_8) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : TopologicalSpace F] →
                      [inst_6 : IsTopologicalAddGroup F] →
                        [inst_7 : Module 𝕜₁ E] →
                          [inst_8 : Module 𝕜₂ F] →
                            [inst_9 : ContinuousConstSMul 𝕜₂ F] → (E →SLₚₜ[σ] F) →ₗ[𝕜₂] E →ₛₗ[σ] F
-- Std.Time.Zoned.RecurringRule
/-- `n` form: zero-based day 0–365 (Feb 29 counted in leap years).
 -/
Std.Time.TimeZone.TransitionSpec.julian0 : Std.Time.Internal.Bounded.LE 0 365 → Std.Time.TimeZone.TransitionSpec
-- Mathlib.AlgebraicGeometry.Scheme
/-- A morphism between schemes is a morphism between the underlying locally ringed spaces.  -/
AlgebraicGeometry.Scheme.Hom : AlgebraicGeometry.Scheme → AlgebraicGeometry.Scheme → Type u_1
-- Lean.Data.DeclarationRange
Lean.DeclarationRanges.mk.inj : ∀ {range selectionRange range_1 selectionRange_1 : Lean.DeclarationRange},
  { range := range, selectionRange := selectionRange } = { range := range_1, selectionRange := selectionRange_1 } →
    range = range_1 ∧ selectionRange = selectionRange_1
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.map_of : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N) (x : M),
  (AdicCompletion.map I f) ((AdicCompletion.of I M) x) = (AdicCompletion.of I N) (f x)
-- Mathlib.Data.ENNReal.Real
ENNReal.le_toNNReal_of_coe_le : ∀ {a : ENNReal} {p : NNReal}, ↑p ≤ a → a ≠ ⊤ → p ≤ a.toNNReal
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.toList_rci : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.toList_rci._auto_1) [Std.TransCmp cmp]
  {t : Std.DTreeMap α β cmp} {bound : α},
  Std.Slice.toList (Std.Rci.Sliceable.mkSlice t bound...*) = List.filter (fun e => (cmp e.fst bound).isGE) t.toList
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₁ : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} →
      {hζ : IsPrimitiveRoot ζ 3} →
        FermatLastTheoremForThreeGen.Solution✝ hζ →
          [inst_1 : NumberField K] → [IsCyclotomicExtension {3} ℚ K] → (NumberField.RingOfIntegers K)ˣ
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- Given a functor `F : C ⥤ D`, if `F.map p₁` and `F.map p₂` form a jointly monic pair of
morphisms, then `F` preserves reflexive relations.  -/
CategoryTheory.ReflexiveRelation.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {R X : C} →
          {p₁ p₂ : R ⟶ X} →
            CategoryTheory.ReflexiveRelation p₁ p₂ →
              (F : CategoryTheory.Functor C D) →
                [CategoryTheory.JointlyMono₂ (F.map p₁) (F.map p₂)] →
                  CategoryTheory.ReflexiveRelation (F.map p₁) (F.map p₂)
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiff.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {H'' : Type u_6} [inst_7 : TopologicalSpace H''] {E'' : Type u_7}
  [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {I'' : ModelWithCorners 𝕜 E'' H''} {G : Type u_8}
  [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H G] {M : Type u_9} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace H'' N]
  [inst_16 : SMul G M] {n : WithTop ℕ∞} [ContMDiffSMul I I' n G M] {f : N → G} {g : N → M},
  ContMDiff I'' I n f → ContMDiff I'' I' n g → ContMDiff I'' I' n (f • g)
-- Mathlib.CategoryTheory.Products.Basic
/-- The equivalence, given by swapping factors, between `C × D` and `D × C`.
 -/
CategoryTheory.Prod.braiding : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → C × D ≌ D × C
-- Mathlib.LinearAlgebra.Dimension.Basic
LinearMap.lift_rank_le_of_surjective : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  Function.Surjective ⇑f → Cardinal.lift.{v, v'} (Module.rank R M') ≤ Cardinal.lift.{v', v} (Module.rank R M)
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_aux.fwdDiffₗ_apply : ∀ (M : Type u_1) (G : Type u_2) [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) (f : M → G) (a : M),
  (fwdDiff_aux.fwdDiffₗ M G h) f a = fwdDiff h f a
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.existsN : ∀ {X : SSet} {n : ℕ} (s : X.obj (Opposite.op { len := n })) {A : X.Subcomplex},
  s ∉ A.obj (Opposite.op { len := n }) →
    ∃ x f, CategoryTheory.Epi f ∧ (CategoryTheory.ConcreteCategory.hom (X.map f.op)) x.simplex = s