mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Finite.Basic
/-- **Alias** of `Set.Finite.toFinset_ofPred`. -/
Set.Finite.toFinset_setOf : ∀ {α : Type u} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p] (h : {x | p x}.Finite),
  h.toFinset = {x | p x}
-- Mathlib.Analysis.Meromorphic.Order
/-- On a connected set, there exists a point where a meromorphic function `f` has finite order iff `f`
has finite order at every point.

See `Meromorphic.exists_meromorphicOrderAt_ne_top_iff_forall` in file
`Mathlib/Analysis/Meromorphic/RCLike` for a related result assuming that `f` is meromorphic on all
of `𝕜`.
 -/
MeromorphicOn.exists_meromorphicOrderAt_ne_top_iff_forall : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → IsConnected U → ((∃ u, meromorphicOrderAt f ↑u ≠ ⊤) ↔ ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤)
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- Closure of a submonoid `S` equals `S`.  -/
Submonoid.closure_eq : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), Submonoid.closure ↑S = S
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_zero : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ), (MvPolynomial.rename f) 0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.IsInitial.strict_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C}
  (hI : CategoryTheory.Limits.IsInitial I) {A : C} (f g : A ⟶ I), f = g
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- The composition of `C^n` functions on domains is `C^n`.  -/
ContMDiffOn.comp' : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] {E'' : Type u_8} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E'']
  {H'' : Type u_9} [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10}
  [inst_12 : TopologicalSpace M''] [inst_13 : ChartedSpace H M] [inst_14 : ChartedSpace H' M']
  [inst_15 : ChartedSpace H'' M''] {f : M → M'} {s : Set M} {n : WithTop ℕ∞} {t : Set M'} {g : M' → M''},
  ContMDiffOn I' I'' n g t → ContMDiffOn I I' n f s → ContMDiffOn I I'' n (g ∘ f) (s ∩ f ⁻¹' t)
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate : ∀ {α : Type u_1} {f : α → α} {x : α} {m n : ℕ},
  x ∈ Function.periodicPts f → Function.IsPeriodicPt f m (f^[n] x) → Function.IsPeriodicPt f m x
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `NonUnitalNonAssocCommRing` instance along a surjective function.  -/
Function.Surjective.nonUnitalNonAssocCommRing : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : Neg S] →
                [inst_4 : Sub S] →
                  [inst_5 : SMul ℕ S] →
                    [inst_6 : SMul ℤ S] →
                      [inst_7 : NonUnitalNonAssocCommRing R] →
                        f 0 = 0 →
                          (∀ (x y : R), f (x + y) = f x + f y) →
                            (∀ (x y : R), f (x * y) = f x * f y) →
                              (∀ (x : R), f (-x) = -f x) →
                                (∀ (x y : R), f (x - y) = f x - f y) →
                                  (∀ (n : ℕ) (x : R), f (n • x) = n • f x) →
                                    (∀ (n : ℤ) (x : R), f (n • x) = n • f x) → NonUnitalNonAssocCommRing S
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.invRotate_map_hom₂ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y),
  ((CategoryTheory.Pretriangulated.invRotate C).map f).hom₂ = f.hom₁
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The even Hurwitz completed zeta is differentiable away from `s = 0` and `s = 1` (and also at
`s = 0` if `a ≠ 0`)
 -/
HurwitzZeta.differentiableAt_completedHurwitzZetaEven : ∀ (a : UnitAddCircle) {s : ℂ}, s ≠ 0 ∨ a ≠ 0 → s ≠ 1 → DifferentiableAt ℂ (HurwitzZeta.completedHurwitzZetaEven a) s
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_eq_insertListIfNewUnitₘ : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) (l : List α),
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l) =
    Std.DHashMap.Internal.Raw₀.Const.insertListIfNewUnitₘ m l
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.coind_toMonoidHom_apply_apply_coe : ∀ {R : Type u_1} {V : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] {G : Type u_7} {H : Type u_8} [inst_5 : Group G]
  [inst_6 : TopologicalSpace G] [inst_7 : TopologicalSpace R] [inst_8 : ContinuousSMul R V] [inst_9 : Group H]
  [inst_10 : TopologicalSpace H] (φ : G →ₜ* H) [inst_11 : IsTopologicalGroup H] (π : ContRepresentation R G V) (h : H)
  (x : ↥(ContRepresentation.coindV φ π)),
  ↑(((ContRepresentation.coind φ π).toMonoidHom h) x) = (↑x).comp (ContinuousMap.mulRight h)
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.replace : {α : Type u} →
  {β : α → Type v} → [BEq α] → (a : α) → β a → Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewRawFact.mk : Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Grind.SplitSource → Lean.Meta.Grind.EMatchDiagSource → Lean.Meta.Grind.NewRawFact
-- Mathlib.GroupTheory.Coset.Basic
/-- Equality of two left cosets `a * s` and `b * s`.  -/
LeftCosetEquivalence : {α : Type u_1} → [Mul α] → Set α → α → α → Prop
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- `G.support` is the set of vertices that form edges in `G`.  -/
SimpleGraph.support : {V : Type u} → SimpleGraph V → Set V
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsAlt.smul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_8}
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α R] [inst_5 : SMulCommClass R α R] (a : α)
  {B : LinearMap.BilinForm R M}, B.IsAlt → (a • B).IsAlt
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.flatten_splitByLoop : ∀ {α : Type u_1} {r : α → α → Bool} {l : List α} {a : α} {g : List α},
  (List.splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
-- Lean.Compiler.LCNF.Types
Lean.Compiler.LCNF.erasedExpr : Lean.Expr
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.instProdNormSMulClass : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] [inst_2 : SeminormedRing 𝕜] [inst_3 : Module 𝕜 α] [inst_4 : Module 𝕜 β]
  [NormSMulClass 𝕜 α] [NormSMulClass 𝕜 β], NormSMulClass 𝕜 (WithLp p (α × β))
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Submodule.orthogonal_le_orthogonal_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K₀ K₁ : Submodule 𝕜 E} [K₀.HasOrthogonalProjection] [K₁.HasOrthogonalProjection], K₀ᗮ ≤ K₁ᗮ ↔ K₁ ≤ K₀
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.isCompl_opensRange_inl_inr : ∀ (X Y : AlgebraicGeometry.Scheme),
  IsCompl (AlgebraicGeometry.Scheme.Hom.opensRange CategoryTheory.Limits.coprod.inl)
    (AlgebraicGeometry.Scheme.Hom.opensRange CategoryTheory.Limits.coprod.inr)
-- Mathlib.Logic.Denumerable
Denumerable.sigma_ofNat_val : ∀ {α : Type u_1} [inst : Denumerable α] {γ : α → Type u_3} [inst_1 : (a : α) → Denumerable (γ a)] (n : ℕ),
  Denumerable.ofNat (Sigma γ) n =
    ⟨Denumerable.ofNat α (Nat.unpair n).1,
      Denumerable.ofNat (γ (Denumerable.ofNat α (Nat.unpair n).1)) (Nat.unpair n).2⟩
-- Mathlib.Order.Preorder.Finite
Set.finite_isTop : ∀ (α : Type u_2) [inst : PartialOrder α], {a | IsTop a}.Finite
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.processPendingExpr : Array Lean.MVarId → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Lex.completeLattice : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [(i : ι) → CompleteLinearOrder (α i)] → [WellFoundedLT ι] → CompleteLattice (Lex ((i : ι) → (fun i => α i) i))
-- Mathlib.Data.Matrix.Mul
/-- The `i`th row of the multiplication is the same as the `vecMul` with the `i`th row of `A`.  -/
Matrix.mul_apply_eq_vecMul : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  (A : Matrix m n α) (B : Matrix n o α) (i : m), (A * B) i = Matrix.vecMul (A i) B
-- Mathlib.Tactic.Simproc.FinsetInterval
/-- Given integers `m` and `n` and corresponding integer literals `em` and `en`,
returns `(s, ⊢ Finset.Icc m n = s)`.

This cannot be easily merged with `evalFinsetIccNat` since they require different
handling of numerals for `ℕ` and `ℤ`.  -/
Mathlib.Tactic.Simp.evalFinsetIccInt : ℤ → ℤ → (em en : Q(ℤ)) → Lean.MetaM ((s : Q(Finset ℤ)) × Q(Finset.Icc «$em» «$en» = «$s»))
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- **Alias** of the forward direction of `SimpleGraph.neighborSet_eq_empty`. -/
SimpleGraph.IsIsolated.of_neighborSet_eq_empty : ∀ {V : Type u} (G : SimpleGraph V) {v : V}, G.neighborSet v = ∅ → G.IsIsolated v
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∈ t₂ → (t₁ ∩ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.Topology.MetricSpace.Kuratowski
KuratowskiEmbedding.embeddingOfSubset_coe : ∀ {α : Type u} {n : ℕ} [inst : MetricSpace α] (x : ℕ → α) (a : α),
  ↑(KuratowskiEmbedding.embeddingOfSubset x a) n = dist a (x n) - dist (x 0) (x n)
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
_private.Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric.0.Complex.tendsto_multiset_prod_div_multiset_prod_mul : ∀ (a b : Multiset ℂ),
  Filter.Tendsto
    (fun n =>
      (Multiset.map (fun x => x / ↑n + 1) a).prod / ((Multiset.map (fun x => x / ↑n + 1) b).prod * (1 + (↑n)⁻¹)))
    Filter.atTop (nhds 1)
-- Batteries.Tactic.Lint.Basic
Batteries.Tactic.Lint.NamedLinter.mk.injEq : ∀ (toLinter : Batteries.Tactic.Lint.Linter) (name declName : Lean.Name) (toLinter_1 : Batteries.Tactic.Lint.Linter)
  (name_1 declName_1 : Lean.Name),
  ({ toLinter := toLinter, name := name, declName := declName } =
      { toLinter := toLinter_1, name := name_1, declName := declName_1 }) =
    (toLinter = toLinter_1 ∧ name = name_1 ∧ declName = declName_1)
-- Init.Data.Vector.OfFn
Vector.ofFnM_succ' : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α},
  Vector.ofFnM f = do
    let a ← f 0
    let as ← Vector.ofFnM fun i => f i.succ
    pure (Vector.cast ⋯ (#v[a] ++ as))
-- Lean.Environment
/-- Construct a mapping from persistent extension name to extension index at the array of persistent extensions.
We only consider extensions starting with index `>= startingAt`.
 -/
Lean.mkExtNameMap : ℕ → IO (Std.HashMap Lean.Name ℕ)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.symm : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) {x y : R}, c x y → c y x
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.inv_mem' : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (self : IntermediateField K L), ∀ x ∈ self.carrier, x⁻¹ ∈ self.carrier
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for the modulo operation on `BitVec`s.  -/
BitVec.reduceMod : Lean.Meta.Simp.DSimproc
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The weights for the circumcenter of a simplex, in terms of `pointsWithCircumcenter`.  -/
Affine.Simplex.circumcenterWeightsWithCircumcenter : (n : ℕ) → Affine.Simplex.PointsWithCircumcenterIndex n → ℝ
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.algHom_ext_iff : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] {C : Type u_5} [inst_10 : Ring C] [inst_11 : Algebra R C]
  {f g : GradedTensorProduct R 𝒜 ℬ →ₐ[R] C},
  f = g ↔
    f.comp (GradedTensorProduct.includeLeft 𝒜 ℬ) = g.comp (GradedTensorProduct.includeLeft 𝒜 ℬ) ∧
      f.comp (GradedTensorProduct.includeRight 𝒜 ℬ) = g.comp (GradedTensorProduct.includeRight 𝒜 ℬ)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.coeSubgraph : ∀ {V : Type u_1} {G : SimpleGraph V} {G' : G.Subgraph} {M : G'.coe.Subgraph},
  M.IsMatching → (SimpleGraph.Subgraph.coeSubgraph M).IsMatching
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
/-- The canonical morphism `i : coimage f ⟶ Q` is a monomorphism  -/
CategoryTheory.NonPreadditiveAbelian.instMonoFactorThruCoimage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {P Q : C}
  (f : P ⟶ Q), CategoryTheory.Mono (CategoryTheory.Abelian.factorThruCoimage f)
-- Mathlib.Algebra.Order.Monoid.Units
Units.instPreorder.eq_1 : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : Preorder α], Units.instPreorder = Preorder.lift Units.val
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.Ioi_add_bij : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a d : M), Set.BijOn (fun x => x + d) (Set.Ioi a) (Set.Ioi (a + d))
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.forIn'_eq_match_step.match_1.splitter : {γ : Type u_1} →
  (motive : ForInStep γ → Sort u_2) →
    (__do_lift : ForInStep γ) →
      ((c : γ) → motive (ForInStep.yield c)) → ((c : γ) → motive (ForInStep.done c)) → motive __do_lift
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.blockSep : Lean.Parser.ParserFn
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrX_mapHomologicalComplexObjXIso_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {D : Type u_3} [inst_4 : CategoryTheory.Category.{v_2, u_3} D]
  [inst_5 : CategoryTheory.Preadditive D] (H : CategoryTheory.Functor C D) [inst_6 : H.Additive]
  [inst_7 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)] (i : ι) {Z : D}
  (h : H.obj ((HomologicalComplex.homotopyCofiber φ).X i) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX ((H.mapHomologicalComplex c).map φ) i)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjXIso φ H i).inv
        h) =
    CategoryTheory.CategoryStruct.comp (H.map (HomologicalComplex.homotopyCofiber.inrX φ i)) h
-- Mathlib.Data.Seq.Basic
Stream'.Seq.Pairwise_cons_nil : ∀ {α : Type u} {R : α → α → Prop} {hd : α}, Stream'.Seq.Pairwise R (Stream'.Seq.cons hd Stream'.Seq.nil)
-- Mathlib.Topology.UniformSpace.Closeds
UniformContinuous.prod_nonemptyCompacts : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] {f : α → TopologicalSpace.NonemptyCompacts β} {g : α → TopologicalSpace.NonemptyCompacts γ},
  UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x ×ˢ g x
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.instNNRatCast : {K : Type u} →
  [inst : DivisionRing K] → {S : Type u_1} → [inst_1 : SetLike S K] → [h : SubfieldClass S K] → (s : S) → NNRatCast ↥s
-- Batteries.Data.List.Interleave
List.interleave_ofFn_ofFn_even : ∀ {α : Type u_1} {n : ℕ} {f g : Fin n → α},
  (List.ofFn f).interleave (List.ofFn g) = List.ofFn fun i => if ↑i % 2 = 0 then f ⟨↑i / 2, ⋯⟩ else g ⟨↑i / 2, ⋯⟩
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.trans_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : AddCommMonoid C] [inst_4 : Module R A] [inst_5 : Module R B]
  [inst_6 : Module R C] [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C]
  (e₁₂ : A ≃ₗc[R] B) (e₂₃ : B ≃ₗc[R] C) (a : C), (e₁₂.trans e₂₃).symm a = e₁₂.symm (e₂₃.symm a)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j),
  CategoryTheory.CategoryStruct.comp c.ιSigmaHorn (f.t j) = SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn f c
-- Init.Meta.Defs
Lean.Name.appendAfter : Lean.Name → String → Lean.Name
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.mapNatIso_inv : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  {F G : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms]
  (τ : F ≅ G), (S.mapNatIso τ).inv = S.mapNatTrans τ.inv
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [Inhabited α],
  t.WF →
    ∀ {k fallback : α} {f : Option β → Option β},
      (t.alter k f).getKeyD k fallback = if (f t[k]?).isSome = true then k else fallback
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instAddCommGroup : {q : ℕ} → AddCommGroup (LucasLehmer.X q)
-- Mathlib.Analysis.Normed.Module.Basic
SeminormedSpace.Core.mk : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Norm E]
  [inst_3 : Module 𝕜 E],
  (∀ (x : E), 0 ≤ ‖x‖) →
    (∀ (c : 𝕜) (x : E), ‖c • x‖ = ‖c‖ * ‖x‖) → (∀ (x y : E), ‖x + y‖ ≤ ‖x‖ + ‖y‖) → SeminormedSpace.Core 𝕜 E
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The object underlying `⊥ : Subobject B` is (up to isomorphism) the zero object.  -/
CategoryTheory.Subobject.botCoeIsoZero : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] → {B : C} → CategoryTheory.Subobject.underlying.obj ⊥ ≅ 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_erase_eq_of_not_compare_eq_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).maxKey? = t.maxKey?
-- Mathlib.Data.Nat.Log
/-- `(b ^ ·)` and `log b` (almost) form a Galois connection. See also `Nat.pow_le_of_le_log` and
`Nat.le_log_of_pow_le` for individual implications under weaker assumptions.  -/
Nat.le_log_iff_pow_le : ∀ {b : ℕ}, 1 < b → ∀ {x y : ℕ}, y ≠ 0 → (x ≤ Nat.log b y ↔ b ^ x ≤ y)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.neighborSet_subgraphOfAdj_of_ne_of_ne : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (hvw : G.Adj v w),
  u ≠ v → u ≠ w → (G.subgraphOfAdj hvw).neighborSet u = ∅
-- Mathlib.LinearAlgebra.Dimension.Finite
LinearIndependent.lt_aleph0_of_finite : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type w} [Module.Finite R M] {v : ι → M}, LinearIndependent R v → Cardinal.mk ι < Cardinal.aleph0
-- Init.Data.Array.Basic
/-- Swaps two elements of an array. The modification is performed in-place when the reference to the
array is unique.

Examples:
* `#["red", "green", "blue", "brown"].swap 0 3 = #["brown", "green", "blue", "red"]`
* `#["red", "green", "blue", "brown"].swap 0 2 = #["blue", "green", "red", "brown"]`
* `#["red", "green", "blue", "brown"].swap 1 2 = #["red", "blue", "green", "brown"]`
* `#["red", "green", "blue", "brown"].swap 3 0 = #["brown", "green", "blue", "red"]`
 -/
Array.swap : {α : Type u} →
  (xs : Array α) →
    (i j : ℕ) → autoParam (i < xs.size) Array.swap._auto_1 → autoParam (j < xs.size) Array.swap._auto_3 → Array α
-- Init.Data.String.Lemmas.Splits
String.splits_prev_endPos : ∀ {s : String} {h : s.endPos ≠ s.startPos},
  (s.endPos.prev h).Splits (s.sliceTo (s.endPos.prev h)).copy (String.singleton ((s.endPos.prev h).get ⋯))
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.lt_one : ∀ {R : Type u} [inst : EuclideanDomain R] (a : R), EuclideanDomain.r a 1 → a = 0
-- Mathlib.Topology.UniformSpace.Separation
isClosed_range_of_spaced_out : ∀ {α : Type u} [inst : UniformSpace α] {ι : Type u_1} [T0Space α] {V₀ : Set (α × α)},
  V₀ ∈ uniformity α → ∀ {f : ι → α}, (Pairwise fun x y => (f x, f y) ∉ V₀) → IsClosed (Set.range f)
-- Mathlib.Algebra.Regular.Basic
IsDedekindFiniteAddMonoid.iff_isAddLeftRegular_of_add_eq_zero : ∀ {R : Type u_1} [inst : AddMonoid R], IsDedekindFiniteAddMonoid R ↔ ∀ (x y : R), x + y = 0 → IsAddLeftRegular x
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mem_top : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, J ∈ ⊤ ↔ J = I
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.toWord_inj : ∀ {α : Type u_1} [inst : DecidableEq α] {x y : FreeAddGroup α}, x.toWord = y.toWord ↔ x = y
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_zpow : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Group G]
  [inst_2 : DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) (n : ℤ), ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.sinPartialEquiv.eq_1 : Real.sinPartialEquiv =
  { toFun := Real.sin, invFun := Real.arcsin, source := Set.Icc (-(Real.pi / 2)) (Real.pi / 2),
    target := Set.Icc (-1) 1, map_source' := ⋯, map_target' := ⋯, left_inv' := Real.sinPartialEquiv._proof_1,
    right_inv' := Real.sinPartialEquiv._proof_3 }
-- Lean.Widget.UserWidget
/-- Construct a widget instance by finding a widget module
in the current environment.

`hash` must be `hash (toModule c).javascript`
where `c` is some global constant annotated with `@[widget_module]`,
or the name of a builtin widget module.  -/
Lean.Widget.WidgetInstance.ofHash : UInt64 → StateM Lean.Server.RpcObjectStore Lean.Json → Lean.CoreM Lean.Widget.WidgetInstance
-- Mathlib.Analysis.Analytic.Constructions
hasFPowerSeriesOnBall_inverse_one_sub : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [HasSummableGeomSeries A],
  HasFPowerSeriesOnBall (fun x => Ring.inverse (1 - x)) (formalMultilinearSeries_geometric 𝕜 A) 0 1
-- Mathlib.Data.Matrix.DMatrix
/-- The transpose of a dmatrix.  -/
DMatrix.«term_ᵀ» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.Perm.Fin
Equiv.Perm.decomposeFin.eq_1 : ∀ {n : ℕ},
  Equiv.Perm.decomposeFin =
    ((finSuccEquiv n).permCongr.trans Equiv.Perm.decomposeOption).trans
      ((finSuccEquiv n).symm.prodCongr (Equiv.refl (Equiv.Perm (Fin n))))
-- Mathlib.Data.Finsupp.Weight
Finsupp.degree_preimage_add : ∀ {σ : Type u_5} (s t : Set ℕ), ⇑Finsupp.degree ⁻¹' (s + t) = ⇑Finsupp.degree ⁻¹' s + ⇑Finsupp.degree ⁻¹' t