mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ConstMulAction
IsClosed.vadd : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] {s : Set α}, IsClosed s → ∀ (c : G), IsClosed (c +ᵥ s)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.zero_le_pairingIn_of_root_sub_mem : ∀ {ι : 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] {P : RootPairing ι R M N} [Finite ι]
  [CharZero R] [IsDomain R] {i j : ι} [inst_8 : P.IsNotG2],
  P.root i - P.root j ∈ Set.range ⇑P.root → 0 ≤ P.pairingIn ℤ i j
-- Lean.Meta.Match.SimpH
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.State.eqs : Lean.Meta.Match.SimpH.State✝ → List Lean.FVarId
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Continuous.aemeasurable2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
  [OpensMeasurableSpace α] [inst_3 : TopologicalSpace β] [inst_4 : MeasurableSpace β] [OpensMeasurableSpace β]
  [inst_6 : TopologicalSpace γ] [inst_7 : MeasurableSpace γ] [BorelSpace γ] [inst_9 : MeasurableSpace δ]
  [SecondCountableTopologyEither α β] {f : δ → α} {g : δ → β} {c : α → β → γ} {μ : MeasureTheory.Measure δ},
  (Continuous fun p => c p.1 p.2) → AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun a => c (f a) (g a)) μ
-- Mathlib.Algebra.Category.Grp.Basic
/-- Multiplicative equivalences between `CommGroup`s are the same as (isomorphic to) isomorphisms
in `CommGrpCat`.  -/
mulEquivIsoCommGroupIso : {X Y : CommGrpCat} → ↑X ≃* ↑Y ≅ X ≅ Y
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.measurableEmbedding_coe : MeasurableEmbedding Subtype.val
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.extend_eq : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C), s ∈ C → (MeasureTheory.AddContent.extend hC m) s = m s
-- Mathlib.Analysis.Convex.Between
sbtw_vadd_const_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : V} (p : P), Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_of_contains_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α},
  (t.insert k).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.Slice.intercalate.go.match_1.eq_1 : ∀ (motive : List String.Slice → Sort u_1) (a : String.Slice) (as : List String.Slice)
  (h_1 : (a : String.Slice) → (as : List String.Slice) → motive (a :: as)) (h_2 : Unit → motive []),
  (match a :: as with
    | a :: as => h_1 a as
    | [] => h_2 ()) =
    h_1 a as
-- Mathlib.Analysis.Calculus.Deriv.Shift
/-- The derivative of `x ↦ f (-x)` at `a` is the negative of the derivative of `f` at `-a`.  -/
deriv_comp_neg : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (f : 𝕜 → F) (x : 𝕜), deriv (fun x => f (-x)) x = -deriv f (-x)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivWithinAt.const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {s : Set M} {z : M} {f : M → E'} {f' : TangentSpace I z →L[𝕜] E'},
  HasMFDerivAt[s] f z f' → ∀ (a : 𝕜), HasMFDerivAt[s] (a • f) z (a • f')
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.mem_tail_support_append_iff : ∀ {V : Type u} {G : SimpleGraph V} {t u v w : V} (p : G.Walk u v) (p' : G.Walk v w),
  t ∈ (p.append p').support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail
-- Mathlib.Topology.Closure
interior_interior : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, interior (interior s) = interior s
-- Mathlib.Data.Nat.SuccPred
Nat.instSuccOrder : SuccOrder ℕ
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.toSublattice : {α : Type u_1} → [inst : CompleteLattice α] → CompleteSublattice α → Sublattice α
-- Mathlib.RingTheory.MvPowerSeries.Expand
/-- Expand the power series by a factor of p, so `∑ aₙ xⁿ` becomes `∑ aₙ xⁿᵖ`.

See also `PowerSeries.expand`.  -/
MvPowerSeries.expand : {σ : Type u_1} → {R : Type u_3} → [inst : CommRing R] → (p : ℕ) → p ≠ 0 → MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R
-- Mathlib.RingTheory.RingHom.Etale
RingHom.Etale.isStableUnderBaseChange : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => RingHom.Etale
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The identity map as an equivariant ring homomorphism.  -/
MulSemiringActionHom.id : (M : Type u_1) →
  [inst : Monoid M] → {R : Type u_10} → [inst_1 : Semiring R] → [inst_2 : MulSemiringAction M R] → R →+*[M] R
-- Mathlib.Order.ULift
ULift.instOrientedOrd_mathlib : ∀ {α : Type u} [inst : Ord α] [inst_1 : Std.OrientedOrd α], Std.OrientedOrd (ULift.{v, u} α)
-- Lean.Meta.AppBuilder
/-- Returns `a < b`  -/
Lean.Meta.mkLt : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.SupIndep
sSupIndep.mono : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sSupIndep s → ∀ {t : Set α}, t ⊆ s → sSupIndep t
-- Mathlib.Algebra.Algebra.Operations
Submodule.pow_succ : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A) {n : ℕ}, M ^ (n + 1) = M ^ n * M
-- Init.Data.String.Defs
String.toByteArray_append : ∀ {s t : String}, (s ++ t).toByteArray = s.toByteArray ++ t.toByteArray
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.mk.sizeOf_spec : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} [inst_6 : SizeOf A] [inst_7 : SizeOf B]
  [inst_8 : SizeOf C] [inst_9 : SizeOf A'] [inst_10 : SizeOf B'] [inst_11 : SizeOf C'] (left : ψ.left ⟶ ψ'.left)
  (right : ψ.right ⟶ ψ'.right) (base : ψ.base ⟶ ψ'.base)
  (left_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
          (CategoryTheory.Functor.whiskerRight left F') =
        CategoryTheory.CategoryStruct.comp (F.whiskerLeft base) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
      CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence._autoParam)
  (right_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
          (CategoryTheory.Functor.whiskerRight right G') =
        CategoryTheory.CategoryStruct.comp (G.whiskerLeft base)
          (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom)
      CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence._autoParam),
  sizeOf
      { left := left, right := right, base := base, left_coherence := left_coherence,
        right_coherence := right_coherence } =
    1 + sizeOf left + sizeOf right + sizeOf base + sizeOf left_coherence + sizeOf right_coherence
-- Mathlib.Algebra.Homology.ComplexShape
/-- The reverse of a `ComplexShape`.
 -/
ComplexShape.symm : {ι : Type u_1} → ComplexShape ι → ComplexShape ι
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.stdPart_map₂ : ∀ {x y : ℝ*} {r s : ℝ} {f : ℝ → ℝ → ℝ},
  Filter.Germ.Tendsto x (nhds r) →
    Filter.Germ.Tendsto y (nhds s) →
      ContinuousAt (Function.uncurry f) (r, s) → (Filter.Germ.map₂ f x y).Tendsto (nhds (f r s))
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigOWith_top : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F},
  Asymptotics.IsBigOWith c ⊤ f g ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Std.Internal.Do.Except.wpInst.match_1.splitter : {ε : Type u_1} →
  {α : Type u_2} →
    (motive : Except ε α → Sort u_3) →
      (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((el : ε) → motive (Except.error el)) → motive x
-- Init.Data.Range.Polymorphic.Basic
Std.Roc.le_upper_of_mem : ∀ {α : Type u} {r : Std.Roc α} {a : α} [inst : LE α] [inst_1 : LT α], a ∈ r → a ≤ r.upper
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.coeff_eval : ∀ {b : Ordinal.{u_1}},
  1 < b →
    ∀ {f : Ordinal.{u_1} →₀ Ordinal.{u_1}},
      (∀ (e : Ordinal.{u_1}), f e < b) → Ordinal.CNF.coeff b (Ordinal.CNF.eval b f) = f
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.HeightOneSpectrum.rankOne_hom'_def : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R],
  Valuation.RankLeOne.hom' Valued.v =
    (WithZeroMulInt.toNNReal ⋯).comp
      (Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt Valued.v).toMonoidWithZeroHom
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.mapPair_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C}
  (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.left })
  (g :
    F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.right }),
  (CategoryTheory.Limits.mapPair f g).app { as := CategoryTheory.Limits.WalkingPair.right } = g
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.pointwise_smul_eq_comap : ∀ {M : Type u_1} {R : Type u_3} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  (S : Ideal R), a • S = Ideal.comap (RingEquiv.symm ((MulSemiringAction.toRingAut M R) a)) S
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.hom_hom_rightUnitor : ∀ {R : Type u} [inst : CommSemiring R] {M : SemimoduleCat R},
  SemimoduleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom = ↑(TensorProduct.rid R ↑M)
-- Mathlib.RingTheory.Regular.RegularSequence
_private.Mathlib.RingTheory.Regular.RegularSequence.0.AddHom.map_smul_top_toAddSubgroup_of_surjective : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] {f : M →+ M₂}
  {as : List R} {bs : List S},
  Function.Surjective ⇑f →
    List.Forall₂ (fun r s => ∀ (x : M), f (r • x) = s • f x) as bs →
      AddSubgroup.map f (Ideal.ofList as • ⊤).toAddSubgroup = (Ideal.ofList bs • ⊤).toAddSubgroup
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Right.nsmul_nonneg : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddRightMono M] {x : M}, 0 ≤ x → ∀ {n : ℕ}, 0 ≤ n • x
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.Config.mk.injEq : ∀ (maxDepth : ℕ) (abstract debug : Bool) (maxDepth_1 : ℕ) (abstract_1 debug_1 : Bool),
  ({ maxDepth := maxDepth, abstract := abstract, debug := debug } =
      { maxDepth := maxDepth_1, abstract := abstract_1, debug := debug_1 }) =
    (maxDepth = maxDepth_1 ∧ abstract = abstract_1 ∧ debug = debug_1)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonCompletionClientCapabilities.fromJson : Lean.Json → Except String Lean.Lsp.CompletionClientCapabilities
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_inter_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ((t₁ ∩ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∉ t₂)
-- Init.Data.Nat.MinMax
Nat.zero_min : ∀ (a : ℕ), min 0 a = 0
-- Lean.Elab.Tactic.Monotonicity
Lean.Meta.Monotonicity.evalMonotonicity : Lean.Elab.Tactic.Tactic
-- Mathlib.Data.ENNReal.Operations
ENNReal.mem_Iio_self_add : ∀ {x ε : ENNReal}, x ≠ ⊤ → ε ≠ 0 → x ∈ Set.Iio (x + ε)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.rule_expr___ : Lean.ParserDescr
-- Mathlib.Data.Tree.Basic
instDecidableEqBinaryTree : {α : Type u_1} → [DecidableEq α] → DecidableEq (BinaryTree α)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.Hom.isComonHom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.Comon C} (self : M.Hom N), CategoryTheory.IsComonHom self.hom
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.beq.match_1.eq_3 : ∀ (motive : Lean.Name → Lean.Name → Sort u_1) (p₁ : Lean.Name) (n₁ : ℕ) (p₂ : Lean.Name) (n₂ : ℕ)
  (h_1 : Unit → motive Lean.Name.anonymous Lean.Name.anonymous)
  (h_2 : (p₁ : Lean.Name) → (s₁ : String) → (p₂ : Lean.Name) → (s₂ : String) → motive (p₁.str s₁) (p₂.str s₂))
  (h_3 : (p₁ : Lean.Name) → (n₁ : ℕ) → (p₂ : Lean.Name) → (n₂ : ℕ) → motive (p₁.num n₁) (p₂.num n₂))
  (h_4 : (x x_1 : Lean.Name) → motive x x_1),
  (match p₁.num n₁, p₂.num n₂ with
    | Lean.Name.anonymous, Lean.Name.anonymous => h_1 ()
    | p₁.str s₁, p₂.str s₂ => h_2 p₁ s₁ p₂ s₂
    | p₁.num n₁, p₂.num n₂ => h_3 p₁ n₁ p₂ n₂
    | x, x_1 => h_4 x x_1) =
    h_3 p₁ n₁ p₂ n₂
-- Mathlib.RingTheory.DividedPowers.Basic
/-- The exponential series of an element in the context of divided powers,
`Σ (dpow n a) X ^ n`  -/
DividedPowers.exp : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → DividedPowers I → A → PowerSeries A
-- Mathlib.CategoryTheory.Limits.Types.PreservesLimit
/-- Let `F : J ⥤ Cᵒᵖ` be a functor, `c'` a colimit cocone for `F.leftOp ⋙ shrinkYoneda.{w}`.
For any cone `c` for `F`, this is the canonical natural transformation
`c'.pt ⟶ shrinkYoneda.{w}.obj c.pt.unop`.  -/
CategoryTheory.Presheaf.coconePtToShrinkYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} J] →
        [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] →
          {F : CategoryTheory.Functor J Cᵒᵖ} →
            (c : CategoryTheory.Limits.Cone F) →
              {c' : CategoryTheory.Limits.Cocone (F.leftOp.comp CategoryTheory.shrinkYoneda.{w, v, u})} →
                CategoryTheory.Limits.IsColimit c' →
                  (c'.pt ⟶ CategoryTheory.shrinkYoneda.{w, v, u}.obj (Opposite.unop c.pt))
-- Mathlib.Computability.Ackermann
/-- The code for the partially applied Ackermann function.
This is used to prove that the Ackermann function is computable.  -/
Nat.Partrec.Code.pappAck : ℕ → Nat.Partrec.Code
-- Mathlib.Combinatorics.Enumerative.Bell
Multiset.bell_zero : Multiset.bell 0 = 1
-- Mathlib.Data.Fintype.BigOperators
Fintype.card_filter_piFinset_const_eq_of_mem : ∀ {ι : Type u_4} {κ : Type u_5} [inst : DecidableEq ι] [inst_1 : DecidableEq κ] [inst_2 : Fintype ι] (s : Finset κ)
  (i : ι) {x : κ}, x ∈ s → {f ∈ Fintype.piFinset fun x => s | f i = x}.card = s.card ^ (Fintype.card ι - 1)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.id_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.Mon C), (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- Bird's bordered minor `f[iα, jα]`.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.bminor : {R : Type u_1} → [CommRing R] → {n : ℕ} → Matrix (Fin n) (Fin n) R → {p : ℕ} → Fin n → Fin n → (Fin p → Fin n) → R
-- Mathlib.Data.PFun
PFun.lift_graph : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {b : β}, (a, b) ∈ (↑f).graph ↔ f a = b
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor_map_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) {X Y : CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G)}
  (f : X ⟶ Y),
  ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceFunctor F G c).map f).left =
    CategoryTheory.Under.homMk (CategoryTheory.StructuredArrow.Hom.right f).left ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_cons : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β},
  Std.Internal.List.getValue? a (⟨k, v⟩ :: l) = bif k == a then some v else Std.Internal.List.getValue? a l
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associatorNatIsoLeft_hom_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {b c d : B} (a : B) (g : b ⟶ c) (h : c ⟶ d) (X : a ⟶ b),
  (CategoryTheory.Bicategory.associatorNatIsoLeft a g h).hom.app X = (CategoryTheory.Bicategory.associator X g h).hom
-- Mathlib.Topology.Connected.Clopen
/-- In a preconnected set, if a symmetric transitive relation `P x y` is true for `y` close
enough to `x`, then it holds for all `x, y`. This is a version of the fact that, if an equivalence
relation has open classes, then it has a single equivalence class.  -/
IsPreconnected.induction₂ : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
  IsPreconnected s →
    ∀ (P : α → α → Prop),
      (∀ x ∈ s, ∀ᶠ (y : α) in nhdsWithin x s, P x y) →
        (∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z) →
          (∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x) → ∀ {x y : α}, x ∈ s → y ∈ s → P x y
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.ext : ∀ {p n : ℕ} {R : Type u_1} {x y : TruncatedWittVector p n R},
  (∀ (i : Fin n), TruncatedWittVector.coeff i x = TruncatedWittVector.coeff i y) → x = y
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.nhds_top' : nhds ⊤ = ⨅ a, Filter.principal (Set.Ioi ↑a)
-- Mathlib.Algebra.Category.Ring.Basic
/-- Ring equivalences are isomorphisms in category of semirings  -/
RingEquiv.toSemiRingCatIso : {R S : Type u} → [inst : Semiring R] → [inst_1 : Semiring S] → R ≃+* S → (SemiRingCat.of R ≅ SemiRingCat.of S)
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_ofNat : ∀ (α : Type u) [inst : AddMonoidWithOne α] {a : α} {n : ℕ}, ↑n = a → Mathlib.Meta.NormNum.IsNat a n
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_erase_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {k : α}, (m.erase k)[k]! = default
-- Mathlib.Data.Semiquot
/-- Replace `s` in a `q : Semiquot α` with a union `s ∪ q.s`  -/
Semiquot.blur : {α : Type u_1} → Set α → Semiquot α → Semiquot α
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ici_subset_Icc_union_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ici a ⊆ Set.Icc a b ∪ Set.Ici b
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.instFaithfulIncl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.WithInitial.incl.Faithful
-- Mathlib.SetTheory.ZFC.PSet
PSet.notMem_empty : ∀ (x : PSet.{u}), x ∉ ∅
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_le_iff : ∀ {R : Type u_1} [inst : CommRing R] {p : Ideal R} {n : ℕ} [p.IsPrime],
  p.height ≤ ↑n ↔ ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.empty_eq_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, Std.ExtDTreeMap.empty = ∅
-- Std.Net.Addr
/-- Obtain the port contained in a `SocketAddress`.
 -/
Std.Net.SocketAddress.port : Std.Net.SocketAddress → UInt16
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_iExsUnique : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {γ : Type u_3} [inst_1 : Finite γ]
  {φ : L.Formula (α ⊕ γ)} {v : α → M},
  (FirstOrder.Language.Formula.iExsUnique γ φ).Realize v ↔ ∃! i, φ.Realize (Sum.elim v i)
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The homotopy equivalence between `K.cylinder` and `K`.  -/
HomologicalComplex.cylinder.homotopyEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasCylinder] → (∀ (j : ι), ∃ i, c.Rel i j) → HomotopyEquiv K.cylinder K
-- Mathlib.Analysis.Normed.Lp.LpEquiv
/-- The canonical map between `lp (fun _ : α ↦ E) ∞` and `α →ᵇ E` as a `LinearIsometryEquiv`.  -/
lpBCFₗᵢ : {α : Type u_1} →
  (E : Type u_2) →
    (𝕜 : Type u_5) →
      [inst : TopologicalSpace α] →
        [DiscreteTopology α] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : NormedAddCommGroup E] →
              [inst_4 : NormedSpace 𝕜 E] → ↥(lp (fun x => E) ⊤) ≃ₗᵢ[𝕜] BoundedContinuousFunction α E
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.id_comp : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {X : Type u_2}
  {Y : Type u_3} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  (f : Convexity.ConvexSpace.AffineMap R X Y), (Convexity.ConvexSpace.AffineMap.id Y).comp f = f
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandParsedSnapshot.toSnapshot : Lean.Language.Lean.CommandParsedSnapshot → Lean.Language.Snapshot
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- The `AddSubsemigroup`s of an `AddMonoid` form a complete lattice.  -/
AddSubsemigroup.instCompleteLattice : {M : Type u_1} → [inst : Add M] → CompleteLattice (AddSubsemigroup M)
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.epiDesc.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f f_1 : X ⟶ Y)
  (e_f : f = f_1) [inst_2 : CategoryTheory.Epi f] {T : C} (g g_1 : X ⟶ T) (e_g : g = g_1)
  (hg : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) g = 0),
  CategoryTheory.Abelian.epiDesc f g hg = CategoryTheory.Abelian.epiDesc f_1 g_1 ⋯
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_sInf : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {s : Set (CategoryTheory.Subgroupoid C)}
  {p : (c : C) × (d : C) × (c ⟶ d)}, p ∈ sInf s ↔ ∀ S ∈ s, p ∈ S
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.exists_quotient_linearEquiv_submodule : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  (N : Submodule R M), ∃ P, Nonempty (↥N ≃ₗ[R] M ⧸ P)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Continuity from below: the measure of the union of an increasing sequence of (not necessarily
measurable) sets is the limit of the measures.  -/
MeasureTheory.tendsto_measure_iUnion_atTop : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder ι]
  [Filter.atTop.IsCountablyGenerated] {s : ι → Set α},
  Monotone s → Filter.Tendsto (⇑μ ∘ s) Filter.atTop (nhds (μ (⋃ n, s n)))
-- Mathlib.Algebra.CharP.Basic
/-- The characteristic of `F_p` is `p`.  -/
Fin.charP : ∀ (n : ℕ) [inst : NeZero n], CharP (Fin n) n