mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.isoMk_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom))
      CategoryTheory.Lax.LaxTrans.isoMk._auto_1)
  (a : B), (CategoryTheory.Lax.LaxTrans.isoMk app naturality).inv.as.app a = (app a).inv
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.action_exchange : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {w x : D} {y z : C} (f : w ⟶ x) (g : y ⟶ z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight w g)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f z) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f y)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x g)
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
/-- A functor `G : C ⥤ D` is locally full w.r.t. a topology on `D` if for every `f : G.obj U ⟶ G.obj V`,
the set of `G.map fᵢ : G.obj Wᵢ ⟶ G.obj U` such that `G.map fᵢ ≫ f` is
in the image of `G` is a coverage of the topology on `D`.
 -/
CategoryTheory.Functor.IsLocallyFull : {C : Type uC} →
  [inst : CategoryTheory.Category.{vC, uC} C] →
    {D : Type uD} →
      [inst_1 : CategoryTheory.Category.{vD, uD} D] →
        CategoryTheory.Functor C D → CategoryTheory.GrothendieckTopology D → Prop
-- Init.Data.ToString.Extra
/-- Converts a list into a string, using `ToString.toString` to convert its elements.

The resulting string resembles list literal syntax, with the elements separated by `", "` and
enclosed in square brackets.

The resulting string may not be valid Lean syntax, because there's no such expectation for
`ToString` instances.

Examples:
* `[1, 2, 3].toString = "[1, 2, 3]"`
* `["cat", "dog"].toString = "[cat, dog]"`
* `["cat", "dog", ""].toString = "[cat, dog, ]"`
 -/
List.toString : {α : Type u_1} → [ToString α] → List α → String
-- Mathlib.Order.SymmDiff
symmDiff_sdiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), symmDiff a b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
-- Mathlib.NumberTheory.LSeries.ZMod
/-- The unique meromorphic function `ℂ → ℂ` which agrees with `∑' n : ℕ, Φ n / n ^ s` wherever the
latter is convergent. This is constructed as a linear combination of Hurwitz zeta functions.

Note that this is not the same as `LSeries Φ`: they agree in the convergence range, but
`LSeries Φ s` is defined to be `0` if `re s ≤ 1`.
 -/
ZMod.LFunction : {N : ℕ} → [NeZero N] → (ZMod N → ℂ) → ℂ → ℂ
-- Lean.Data.Lsp.Ipc
_private.Lean.Data.Lsp.Ipc.0.Lean.Lsp.Ipc.expandOutgoingCallHierarchy.go : ℕ →
  Lean.Lsp.CallHierarchyItem →
    Array Lean.Lsp.Range → Std.TreeSet String compare → Lean.Lsp.Ipc.IpcM (Lean.Lsp.Ipc.CallHierarchy × ℕ)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.eq_adjoint_iff_basis_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] {ι : Type u_5} (b : Module.Basis ι 𝕜 E)
  (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E),
  A = LinearMap.adjoint B ↔ ∀ (i : ι) (y : F), inner 𝕜 (A (b i)) y = inner 𝕜 (b i) (B y)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {a : α} {fallback : β},
  Std.DHashMap.Raw.Const.getD ∅ a fallback = fallback
-- Init.PropLemmas
exists_and_self : ∀ (P : Prop) (Q : P → Prop), (∃ (p : P), Q p) ∧ P ↔ ∃ (p : P), Q p
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
/-- representation function for dependent products  -/
MvQPF.Pi.repr : {n : ℕ} →
  {A : Type u} →
    (F : A → TypeVec.{u} n → Type u) →
      [inst : (α : A) → MvQPF (F α)] → ⦃α : TypeVec.{u} n⦄ → MvQPF.Pi F α → ↑(MvQPF.Pi.P F) α
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- See `AlgebraicGeometry.Morphisms.ClosedImmersion` for the closed immersion version.  -/
AlgebraicGeometry.Scheme.IdealSheafData.instIsPreimmersionSubschemeι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), AlgebraicGeometry.IsPreimmersion I.subschemeι
-- Mathlib.Analysis.CStarAlgebra.Unitization
Unitization.instCStarAlgebra : {A : Type u_3} → [NonUnitalCStarAlgebra A] → CStarAlgebra (Unitization ℂ A)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.id_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (A : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.CategoryStruct.id A).hom₂ = CategoryTheory.CategoryStruct.id A.obj₂
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  (t.erase k).get! k = default
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.eq_X_sub_C_of_single_root : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R],
  f.Splits → ∀ {x : R}, f.roots = {x} → f = Polynomial.C f.leadingCoeff * (Polynomial.X - Polynomial.C x)
-- Mathlib.Data.Sum.Order
Sum.Lex.noMaxOrder : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] [NoMaxOrder α] [NoMaxOrder β], NoMaxOrder (α ⊕ₗ β)
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.IsUniversallyEffectiveEquivalenceRelationCategory.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R A : C},
  (∀ (p₁ p₂ : R ⟶ A) [CategoryTheory.IsEquivalenceRelation p₁ p₂],
      CategoryTheory.IsUniversallyEffectiveEquivalenceRelation p₁ p₂) →
    CategoryTheory.IsUniversallyEffectiveEquivalenceRelationCategory C
-- Mathlib.GroupTheory.GroupAction.Hom
/-- For an additive monoid `M` acting on a type `X`, the `M`-equivariant functions
from `X` to itself form an additive monoid under composition.  -/
AddActionHom.End.instAddMonoidId : {M : Type u_2} → {X : Type u_4} → [inst : VAdd M X] → AddMonoid (X →ₑ[id] X)
-- Lean.Elab.Do.Basic
/-- The expected type of the current `do` block.
This can be different from `ReturnCont.resultType` in `for` loop `do` blocks, for example.
 -/
Lean.Elab.Do.Context.doBlockResultType : Lean.Elab.Do.Context → Lean.Expr
-- Mathlib.RingTheory.PowerSeries.Derivative
/-- Specialisation of `coeff_iterate_derivative` at `k = 0`: the constant term of the `n`-th formal
derivative recovers `n !` times the `n`-th coefficient, `constantCoeff (Dⁿ f) = n ! * coeff n f`.  -/
PowerSeries.constantCoeff_iterate_derivative : ∀ {R : Type u_1} [inst : CommSemiring R] (f : PowerSeries R) (n : ℕ),
  PowerSeries.constantCoeff ((⇑(PowerSeries.derivative R))^[n] f) = ↑n.factorial * (PowerSeries.coeff n) f
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.map.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (φ : R →+* S)
  (C : PrimeSpectrum.BasicConstructibleSetData R),
  PrimeSpectrum.BasicConstructibleSetData.map φ C = { f := φ C.f, n := C.n, g := ⇑φ ∘ C.g }
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.var.injEq : ∀ (a a_1 : Lean.FVarId), (Lean.Meta.Match.Example.var a = Lean.Meta.Match.Example.var a_1) = (a = a_1)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.compare_minKey!_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : β → β}, cmp (t.modify k f).minKey! t.minKey! = Ordering.eq
-- Std.Internal.UV.TCP
/-- Cancels the accept request of a socket.
 -/
Std.Internal.UV.TCP.Socket.cancelAccept : Std.Internal.UV.TCP.Socket → IO Unit
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.not_reachable_of_neighborSet_right_eq_empty : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, u ≠ v → G.neighborSet v = ∅ → ¬G.Reachable u v
-- Mathlib.Analysis.LConvolution
/-- The convolution of measurable functions is measurable.  -/
MeasureTheory.measurable_mlconvolution : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Mul G] [inst_1 : Inv G] [MeasurableMul₂ G] [MeasurableInv G]
  {f g : G → ENNReal} (μ : MeasureTheory.Measure G) [MeasureTheory.SFinite μ],
  Measurable f → Measurable g → Measurable (MeasureTheory.mlconvolution f g μ)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsRkFinite.indep_of_encard_le_eRk : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.IsRkFinite I → I.encard ≤ M.eRk I → M.Indep I
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isNat_lt_false : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {a b : α} {a' b' : ℕ},
  Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → b'.ble a' = true → ¬a < b
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.coe_zpow : ∀ {α : Type u_1} [inst : One α] [inst_1 : Pow α ℤ] (a : α) (n : ℤ), ↑(a ^ n) = ↑a ^ n
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
HasFDerivAt.tendsto_nhdsNE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E},
  HasFDerivAt f f' x → (∃ C, AntilipschitzWith C ⇑f') → Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhdsWithin (f x) {f x}ᶜ)
-- Mathlib.AlgebraicGeometry.Spec
/-- Under the isomorphisms `stalkIso`, the map `stalkMap (Spec.sheafedSpaceMap f) p` corresponds
to the induced local ring homomorphism `Localization.localRingHom`.
 -/
AlgebraicGeometry.localRingHom_comp_stalkIso : ∀ {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom
        (AlgebraicGeometry.StructureSheaf.stalkIso (↑R)
                (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).symm.toRingEquiv.toRingHom)
      (CategoryTheory.CategoryStruct.comp
        (CommRingCat.ofHom
          (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
            (CommRingCat.Hom.hom f) ⋯))
        (CommRingCat.ofHom (AlgebraicGeometry.StructureSheaf.stalkIso (↑S) p).toRingEquiv.toRingHom)) =
    AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom p
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.continuous : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂), Continuous ⇑f
-- Init.Data.Nat.Log2
/-- Base-two logarithm of natural numbers. Returns `⌊max 0 (log₂ n)⌋`.

This function is overridden at runtime with an efficient implementation. This definition is
the logical model.

Examples:
 * `Nat.log2 0 = 0`
 * `Nat.log2 1 = 0`
 * `Nat.log2 2 = 1`
 * `Nat.log2 4 = 2`
 * `Nat.log2 7 = 2`
 * `Nat.log2 8 = 3`
 -/
Nat.log2 : ℕ → ℕ
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.coe_equivMapOfInjective_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup M) (f : M →ₙ* N)
  (hf : Function.Injective ⇑f) (x : ↥S), ↑((S.equivMapOfInjective f hf) x) = f ↑x
-- Mathlib.Data.Finset.Sigma
Set.biInter_finsetSigma' : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i))
  (f : (i : ι) → α i → Set β), ⋂ i ∈ s, ⋂ j ∈ t i, f i j = ⋂ ij ∈ s.sigma t, f ij.fst ij.snd
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
/-- Compose two isomorphisms in a bicategorical category,
inserting unitors and associators between as necessary.  -/
CategoryTheory.bicategoricalIsoComp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} → {f g h i : a ⟶ b} → [CategoryTheory.BicategoricalCoherence g h] → (f ≅ g) → (h ≅ i) → (f ≅ i)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.toFiniteQuotientFunctor.eq_1 : ∀ (P : ProfiniteGrp.{u_1}),
  P.toFiniteQuotientFunctor =
    { obj := fun H => FiniteGrp.of (↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup),
      map := fun {X Y} fHK =>
        FiniteGrp.ofHom
          (QuotientGroup.map (↑X.toOpenSubgroup) (↑Y.toOpenSubgroup) (MonoidHom.id ↑P.toProfinite.toTop) ⋯),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.inf_eq_inter : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s t : { s // MeasurableSet s }), s ⊓ t = s ∩ t
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.keyAtIdx_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {i : ℕ}
  {h' : i < t₁.size} (h : t₁.Equiv t₂), t₁.keyAtIdx i h' = t₂.keyAtIdx i ⋯
-- Mathlib.Logic.Equiv.Option
/-- If we have a value on one side of an `Equiv` of `Option`
we also have a value on the other side of the equivalence
 -/
Equiv.removeNoneAux : {α : Type u_1} → {β : Type u_2} → Option α ≃ Option β → α → β
-- Mathlib.MeasureTheory.Function.EssSup
essSup_eq_iSup : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : CompleteLattice β],
  (∀ (a : α), μ {a} ≠ 0) → ∀ (f : α → β), essSup f μ = ⨆ i, f i
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.testBit.match_1.eq_2 : ∀ (motive : PosNum → ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive PosNum.one 0) (h_2 : (x : ℕ) → motive PosNum.one x)
  (h_3 : (a : PosNum) → motive a.bit0 0) (h_4 : (p : PosNum) → (n : ℕ) → motive p.bit0 n.succ)
  (h_5 : (a : PosNum) → motive a.bit1 0) (h_6 : (p : PosNum) → (n : ℕ) → motive p.bit1 n.succ),
  (x = 0 → False) →
    (match PosNum.one, x with
      | PosNum.one, 0 => h_1 ()
      | PosNum.one, x => h_2 x
      | a.bit0, 0 => h_3 a
      | p.bit0, n.succ => h_4 p n
      | a.bit1, 0 => h_5 a
      | p.bit1, n.succ => h_6 p n) =
      h_2 x
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeriesStep.hcongr_4 : ∀ (G G' : Type u_1),
  G = G' →
    ∀ (inst : Group G) (inst' : Group G'),
      inst ≍ inst' →
        ∀ (N : Subgroup G) (N' : Subgroup G'),
          N ≍ N' →
            ∀ (inst_1 : N.Normal) (inst'_1 : N'.Normal),
              inst_1 ≍ inst'_1 → N.upperCentralSeriesStep ≍ N'.upperCentralSeriesStep
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_app_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (j : J) (k : K) {Z : C}
  (h : CategoryTheory.Limits.colimit (F.comp ((CategoryTheory.evaluation K C).obj k)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.ι F j).app k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F k).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (F.comp ((CategoryTheory.evaluation K C).obj k)) j) h
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.isInternal_stratum' : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] (u : HahnEmbedding.ArchimedeanStrata K M),
  DirectSum.IsInternal u.stratum'
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.GrothendieckTopology.mem_toCoverage_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {S : CategoryTheory.Presieve X}
  (J : CategoryTheory.GrothendieckTopology C), S ∈ J.toCoverage.coverings X ↔ CategoryTheory.Sieve.generate S ∈ J X
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_support_of_injective : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : DecidableEq β] {f : α → β},
  Function.Injective f → ∀ (s : α →₀ M), (Finsupp.mapDomain f s).support = Finset.image f s.support
-- Mathlib.Geometry.Euclidean.Triangle
/-- The sine of the sum of two angles in a possibly degenerate
triangle (where two given sides are nonzero), vector angle form.  -/
_private.Mathlib.Geometry.Euclidean.Triangle.0.InnerProductGeometry.sin_angle_eq_sin_angle_add_add_angle_add : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  x ≠ 0 →
    y ≠ 0 →
      Real.sin (InnerProductGeometry.angle x y) =
        Real.sin (InnerProductGeometry.angle x (x + y) + InnerProductGeometry.angle y (y + x))
-- Batteries.Data.Fin.Fold
Fin.dfoldlM_zero : ∀ {m : Type u_1 → Type u_2} {α : Fin (0 + 1) → Type u_1} [inst : Monad m]
  (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x : α 0), Fin.dfoldlM 0 α f x = pure x
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getKey_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α}
  {h : Std.DHashMap.Internal.AssocList.contains a l = true},
  Std.DHashMap.Internal.AssocList.getKey a l h = Std.Internal.List.getKey a l.toList ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformlyOn.mono : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] {t : Set β},
  HasProdLocallyUniformlyOn f g t → s ⊆ t → HasProdLocallyUniformlyOn f g s
-- Mathlib.Algebra.Algebra.Prod
AlgEquiv.uniqueProd_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Unique B] (self : B × A), AlgEquiv.uniqueProd self = self.2
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.card_le_card_of_forall_subsingleton : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β},
  (∀ a ∈ s, ∃ b ∈ t, r a b) → (∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton) → s.card ≤ t.card
-- Mathlib.LinearAlgebra.AffineSpace.Ceva
/-- **Ceva's theorem** for a triangle, expressed using division.  -/
Affine.Triangle.prod_div_one_sub_eq_one_of_mem_line_point_lineMap : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {t : Affine.Triangle k P} {r : Fin 3 → k},
  (∀ (i : Fin 3), r i ≠ 0) →
    ∀ {p' : P},
      (∀ (i : Fin 3), p' ∈ line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]) →
        ∏ i, r i / (1 - r i) = 1
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
/-- A sequential limit of measurable `ℝ≥0∞`-valued functions is measurable.  -/
ENNReal.measurable_of_tendsto : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : ℕ → α → ENNReal} {g : α → ENNReal},
  (∀ (i : ℕ), Measurable (f i)) → Filter.Tendsto f Filter.atTop (nhds g) → Measurable g
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.objEquiv_symm_comp : ∀ {n n' : SimplexCategory} {m : SimplexCategoryᵒᵖ} (f : Opposite.unop m ⟶ n) (g : n ⟶ n'),
  SSet.stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.comp f g) =
    (CategoryTheory.ConcreteCategory.hom ((SSet.stdSimplex.map g).app m)) (SSet.stdSimplex.objEquiv.symm f)
-- Mathlib.CategoryTheory.IsConnected
/-- If `J` is connected, then given any function `F` such that the presence of a
morphism `j₁ ⟶ j₂` implies `F j₁ = F j₂`, there exists `a` such that `F j = a`
holds for any `j`. See `constant_of_preserves_morphisms` for a different
formulation of the fact that `F` is constant.
This can be thought of as a local-to-global property.

The converse is shown in `IsConnected.of_constant_of_preserves_morphisms`
 -/
CategoryTheory.constant_of_preserves_morphisms' : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsConnected J] {α : Type u₂} (F : J → α),
  (∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∃ a, ∀ (j : J), F j = a
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∉ m₂ → (m₁ ∪ m₂).get? k = m₁.get? k
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.coe_prodCongr : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] [inst_3 : UniformSpace δ] (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ), ⇑(h₁.prodCongr h₂) = Prod.map ⇑h₁ ⇑h₂
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.card_mulAut : ∀ (G : Type u_2) [inst : Group G] [Finite G] [h : IsCyclic G], Nat.card (MulAut G) = (Nat.card G).totient
-- Mathlib.Algebra.Colimit.Module
AddMonoidHom.toAddEquiv.congr_simp : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f f_1 : M →+ N) (e_f : f = f_1)
  (g g_1 : N →+ M) (e_g : g = g_1) (h₁ : g.comp f = AddMonoidHom.id M) (h₂ : f.comp g = AddMonoidHom.id N),
  f.toAddEquiv g h₁ h₂ = f_1.toAddEquiv g_1 ⋯ ⋯
-- Mathlib.Data.Finsupp.Single
Finsupp.equivFunOnFinite_single : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : DecidableEq α] [inst_2 : Finite α] (x : α) (m : M),
  (Finsupp.equivFunOnFinite fun₀ | x => m) = Pi.single x m
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_extendDomain : ∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} [inst_1 : DecidablePred P] (f : Subtype P →₀ M),
  Finsupp.subtypeDomain P f.extendDomain = f
-- Mathlib.Algebra.Module.LocalizedModule.Away
IsLocalizedModule.Away.isUnit_algebraMap : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : M →ₗ[R] N) (r : R)
  [IsLocalizedModule.Away r f], IsUnit ((algebraMap R (Module.End R N)) r)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.bounds_nonempty : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] {f : E [⋀^ι]→L[𝕜] F},
  ∃ c, c ∈ {c | 0 ≤ c ∧ ∀ (m : ι → E), ‖f m‖ ≤ c * ∏ i, ‖m i‖}
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_insertEntryIfNew_le_minKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k} {he : l.isEmpty = false},
      (compare (Std.Internal.List.minKey (Std.Internal.List.insertEntryIfNew k v l) ⋯)
            (Std.Internal.List.minKey l he)).isLE =
        true
-- Mathlib.MeasureTheory.Group.Arithmetic
AddSubgroup.instMeasurableVAdd : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace α] [inst_2 : AddGroup G]
  [inst_3 : AddAction G α] [MeasurableVAdd G α] (s : AddSubgroup G), MeasurableVAdd (↥s) α