mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Lift a monoid homomorphism that maps polynomials `φ : R[X] →* S[X]`
to a `R⟮X⟯ →* S⟮X⟯`,
on the condition that `φ` maps non-zero-divisors to non-zero-divisors,
by mapping both the numerator and denominator and quotienting them.  -/
RatFunc.map : {R : Type u_3} →
  {S : Type u_4} →
    {F : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : FunLike F (Polynomial R) (Polynomial S)] →
            [inst_3 : MonoidHomClass F (Polynomial R) (Polynomial S)] →
              (φ : F) →
                nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S)) →
                  RatFunc R →* RatFunc S
-- Mathlib.Data.Finset.Image
Finset.attach_image_val : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α}, Finset.image Subtype.val s.attach = s
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.getAddFn : {m : Type → Type} →
  [MonadLiftT Lean.MetaM m] →
    [Lean.MonadError m] →
      [Monad m] → [Lean.Meta.Sym.Arith.MonadCanon m] → [Lean.Meta.Grind.Arith.CommRing.MonadRing m] → m Lean.Expr
-- Mathlib.Topology.Category.Profinite.Basic
Profinite.toTopCat.createsLimits : CategoryTheory.CreatesLimits Profinite.toTopCat
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.map_toOrderHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (c : OmegaCompletePartialOrder.Chain α)
  (f : α →o β), (c.map f).toOrderHom = f.comp c.toOrderHom
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.opEquiv_symm_apply : ∀ {M : Type u_2} [inst : MulOneClass M] (x : Submonoid Mᵐᵒᵖ), (RelIso.symm Submonoid.opEquiv) x = x.unop
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The identity affine map acts as the identity.  -/
AffineMap.id_apply : ∀ (k : Type u_1) {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p : P1), (AffineMap.id k P1) p = p
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_one : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R], MvPolynomial.expand 1 = AlgHom.id R (MvPolynomial σ R)
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Wedge.mk_ι : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (pt : C)
  (π : (j : J) → pt ⟶ (F.obj (Opposite.op j)).obj j)
  (hπ :
    ∀ ⦃i j : J⦄ (f : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (π i) ((F.obj (Opposite.op i)).map f) =
        CategoryTheory.CategoryStruct.comp (π j) ((F.map f.op).app j))
  (j : J), CategoryTheory.Limits.Multifork.ι (CategoryTheory.Limits.Wedge.mk pt π hπ) j = π j
-- Mathlib.Order.Partition.Finpartition
Finpartition.part.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) (a : α),
  P.part a = if ha : a ∈ s then Finset.choose (fun a_1 => a ∈ a_1) P.parts ⋯ else ∅
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf' : ∀ (R : Type u) [inst : CommRing R],
  (AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of R)).presheaf =
    (AlgebraicGeometry.Spec.structureSheaf R).obj
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The image under an `AddSemigroup` hom of the `AddSubsemigroup` generated by a set
equals the `AddSubsemigroup` generated by the image of the set.  -/
AddHom.map_mclosure : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (s : Set M),
  AddSubsemigroup.map f (AddSubsemigroup.closure s) = AddSubsemigroup.closure (⇑f '' s)
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.opNNNorm_eq_of_bounds : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  {φ : E →SL[σ₁₂] F} (M : NNReal),
  (∀ (x : E), ‖φ x‖₊ ≤ M * ‖x‖₊) → (∀ (N : NNReal), (∀ (x : E), ‖φ x‖₊ ≤ N * ‖x‖₊) → M ≤ N) → ‖φ‖₊ = M
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.lintEmptyNamed : Lean.Syntax → String → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.nonuniformWitness_spec : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α},
  s ≠ t →
    ¬G.IsUniform ε s t →
      ε ≤ ↑|G.edgeDensity (G.nonuniformWitness ε s t) (G.nonuniformWitness ε t s) - G.edgeDensity s t|
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- Construct `I`-adic Cauchy sequence from sequence satisfying the successive Cauchy condition.  -/
AdicCompletion.AdicCauchySequence.mk : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            (f : ℕ → M) → (∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]) → AdicCompletion.AdicCauchySequence I M
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isLocal.homEquiv_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {X Y : C}
  {f : X ⟶ Y} (hf : P.isLocal f) (Z : C) (hZ : P Z) (g : Y ⟶ Z),
  (hf.homEquiv Z hZ) g = CategoryTheory.CategoryStruct.comp f g
-- Init.Data.BitVec.Bootstrap
BitVec.setWidth_neg_of_le : ∀ {v w : ℕ} {x : BitVec v}, w ≤ v → BitVec.setWidth w (-x) = -BitVec.setWidth w x
-- Mathlib.CategoryTheory.GlueData
/-- If there is a forgetful functor into `Type` that preserves enough (co)limits, then `D.ι` will
be jointly surjective.  -/
CategoryTheory.GlueData.ι_jointly_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] (F : CategoryTheory.Functor C (Type v))
  [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F]
  [∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (x : F.obj D.glued), ∃ i y, (CategoryTheory.ConcreteCategory.hom (F.map (D.ι i))) y = x
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
/-- The tautological equivalence of categories between `C ⥤ V` and `C ⊛⥤ V`.  -/
CategoryTheory.MonoidalCategory.DayFunctor.equiv : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (V : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            CategoryTheory.MonoidalCategory.DayFunctor C V ≌ CategoryTheory.Functor C V
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getKey?ₘ : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → Option α
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  MeasureTheory.volume (ZSpan.fundamentalDomain (NumberField.mixedEmbedding.stdBasis K)) = 1
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.smulCommClass' : ∀ (α : Type u_1) {G : Type u_3} [inst : Group G] [inst_1 : SMul α G] [SMulCommClass G α G] [IsScalarTower α G G],
  SMulCommClass (ConjAct G) α G
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {x y : CategoryTheory.SimplicialObject.Split C},
  x = y ↔ x.X = y.X ∧ x.s ≍ y.s
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.correspondence.eq_1 : ∀ {M : Type u_1} [inst : Add M] {c : AddCon M},
  AddCon.correspondence =
    { toFun := fun d => AddCon.mapOfSurjective c.mkAddHom ⋯ ⋯,
      invFun := fun d => ⟨AddCon.comap AddCon.toQuotient ⋯ d, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_of_get_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m : Std.ExtHashSet α) {k v : α} {w : k ∈ m},
  m.get k w = v → k ∈ m
-- Mathlib.NumberTheory.JacobiSum.Basic
/-- If `χ` and `φ` are multiplicative characters on a finite field `F` with values in another
field `F'` such that `χ`, `φ` and `χφ` are all nontrivial and `char F' ≠ char F`, then
`J(χ,φ) * J(χ⁻¹,φ⁻¹) = #F` (in `F'`).  -/
jacobiSum_mul_jacobiSum_inv : ∀ {F : Type u_1} {F' : Type u_2} [inst : Fintype F] [inst_1 : Field F] [inst_2 : Field F'],
  ringChar F' ≠ ringChar F →
    ∀ {χ φ : MulChar F F'}, χ ≠ 1 → φ ≠ 1 → χ * φ ≠ 1 → jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = ↑(Fintype.card F)
-- Std.Data.ExtTreeMap.Lemmas
_private.Std.Data.ExtTreeMap.Lemmas.0.Std.ExtTreeMap.ext_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t t' : Std.ExtTreeMap α β cmp}, t = t' ↔ t.inner = t'.inner
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_insertMany_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} {ρ : Type w}
  [inst : ForIn Id ρ (α × β)] [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ} {k : α},
  k ∈ m → k ∈ m.insertMany l
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k : α}, t.WF → (Std.DTreeMap.Raw.map f t).contains k = t.contains k
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceOfNatAux : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.Decomposition.decompose'_eq : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ],
  DirectSum.Decomposition.decompose' = ⇑(DirectSum.decompose ℳ)
-- Std.Data.TreeMap.Raw.Basic
/-- Internal implementation detail of the tree map.  -/
Std.TreeMap.Raw.WF.out : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.WF → t.inner.WF
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_eq_foldr : ∀ {M : Type u_3} [inst : CommMonoid M] (s : Multiset M), s.prod = Multiset.foldr (fun x1 x2 => x1 * x2) 1 s
-- Std.Sat.AIG.RelabelNat
/-- The invariant carrying state structure for building the `HashMap` that translates from arbitrary
atom identifiers to `Nat`.
 -/
Std.Sat.AIG.RelabelNat.State : (α : Type) → [DecidableEq α] → [Hashable α] → Array (Std.Sat.AIG.Decl α) → ℕ → Type
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instMin : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] → [inst_1 : Field K] → [inst_2 : Algebra k K] → Min (FiniteGaloisIntermediateField k K)
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.prodμ_counitIso_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A] (X : (A × D) × C × E),
  (CategoryTheory.prod.prodμ C D E A).counitIso.hom.app X =
    CategoryTheory.Prod.mkHom
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1.1) (CategoryTheory.CategoryStruct.id X.1.2))
      (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.2.1) (CategoryTheory.CategoryStruct.id X.2.2))
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instMonoidOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : Monoid Mᵐᵒᵖ], DomMulAct.instMonoidOfMulOpposite = inst
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.ofNatCode.match_1.eq_2 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match false, true with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_2 ()
-- Lean.Parser.Term
Lean.Parser.Term.logNamedErrorAtMacro.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Sat.CNF.Basic
Std.Sat.CNF.empty.eq_1 : ∀ {α : Type u_1}, Std.Sat.CNF.empty = { clauses := #[] }
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- **Alias** of `MeasureTheory.Integrable.fun_neg`.

---

Eta-expanded form of `MeasureTheory.Integrable.neg`

---

If `f` is integrable, then so is `-f`.  -/
MeasureTheory.Integrable.neg' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun i => -f i) μ
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.IsLimit.lift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  {s : CategoryTheory.Limits.WidePullbackCone f} (hs hs_1 : CategoryTheory.Limits.IsLimit s),
  hs = hs_1 →
    ∀ {W : C} (b b_1 : W ⟶ X) (e_b : b = b_1) (a a_1 : (i : ι) → W ⟶ Y i) (e_a : a = a_1)
      (w : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a i) (f i) = b),
      CategoryTheory.Limits.WidePullbackCone.IsLimit.lift hs b a w =
        CategoryTheory.Limits.WidePullbackCone.IsLimit.lift hs_1 b_1 a_1 ⋯
-- Mathlib.CategoryTheory.Yoneda
/-- If `yoneda.map f` is an isomorphism, so was `f`.
 -/
CategoryTheory.Yoneda.isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.IsIso (CategoryTheory.yoneda.map f)], CategoryTheory.IsIso f
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- A 2-isomorphism between a partially-normalized 1-morphism in the free bicategory to the
fully-normalized 1-morphism.
 -/
CategoryTheory.FreeBicategory.normalizeIso : {B : Type u} →
  [inst : Quiver B] →
    {a b c : B} →
      (p : Quiver.Path a b) →
        (f : CategoryTheory.FreeBicategory.Hom b c) →
          CategoryTheory.CategoryStruct.comp ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p }) f ≅
            (CategoryTheory.FreeBicategory.preinclusion B).map { as := CategoryTheory.FreeBicategory.normalizeAux p f }
-- Mathlib.Combinatorics.Enumerative.Bell
_private.Mathlib.Combinatorics.Enumerative.Bell.0.Nat.sigmaPartitionWithPartEquiv : (n : ℕ) → (i : Fin n.succ) × { p // ↑i + 1 ∈ p.parts } ≃ (p : (n + 1).Partition) × ↥p.parts.toFinset
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.enorm_eq_one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → ∀ (i : ι), ‖v i‖ₑ = 1
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
/-- The homology functor on the derived category is induced by the homology
functor on the category of cochain complexes.  -/
DerivedCategory.homologyFunctorFactors : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        (n : ℤ) →
          DerivedCategory.Q.comp (DerivedCategory.homologyFunctor C n) ≅
            HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) n
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.instLeAtTopSymmetricIcc : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G], (SummationFilter.symmetricIcc G).LeAtTop
-- Mathlib.Algebra.Module.Submodule.Map
LinearMap.codRestrict.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (p : Submodule R₂ M₂) (f f_1 : M →ₛₗ[σ₁₂] M₂) (e_f : f = f_1) (h : ∀ (c : M), f c ∈ p),
  LinearMap.codRestrict p f h = LinearMap.codRestrict p f_1 ⋯
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.Raw.getEntryGED : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → (a : α) × β a → (a : α) × β a
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.ucs_eq_top_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (N : LieSubmodule R L M)
  [inst_6 : LieModule R L M] (k : ℕ), LieSubmodule.ucs k N = ⊤ ↔ LieModule.lowerCentralSeries R L M k ≤ N
-- Mathlib.Order.RelSeries
LTSeries.last_range : ∀ (n : ℕ), RelSeries.last (LTSeries.range n) = n
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.ofIso_diag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {Y : C} (e : X ≅ Y), (P.ofIso e).diag = P.diag
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal_uniformizer : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {ϖ : R},
  Irreducible ϖ → (IsDiscreteValuationRing.addVal R) ϖ = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Filter.Tendsto.arccos_nhdsLE : ∀ {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ},
  Filter.Tendsto f l (nhdsWithin x (Set.Iic x)) →
    Filter.Tendsto (fun x => Real.arccos (f x)) l (nhdsWithin (Real.arccos x) (Set.Ici (Real.arccos x)))
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instRespectsIsoPushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C), P.pushouts.RespectsIso
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorAlgebra.toDirectSum_comp_ofDirectSum : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorAlgebra.toDirectSum.comp TensorAlgebra.ofDirectSum = AlgHom.id R (DirectSum ℕ fun n => TensorPower R n M)
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_injective : ∀ {R : Type u}, Function.Injective Tropical.trop
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.coe_comp : ∀ {X Y Z : ProfiniteAddGrp.{u_1}} (f : X ⟶ Y) (g : Y ⟶ Z),
  ⇑(ProfiniteAddGrp.Hom.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(ProfiniteAddGrp.Hom.hom g) ∘ ⇑(ProfiniteAddGrp.Hom.hom f)
-- Mathlib.GroupTheory.Sylow
Sylow.instSubgroupClass : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], SubgroupClass (Sylow p G) G
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.ringInverse_eq_inverse : ∀ {R : Type u_1} {M : Type u_2} [inst : TopologicalSpace M] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M], Ring.inverse = ContinuousLinearMap.inverse
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddMonoid (f i)] → AddMonoid ((i : I) → f i)
-- Mathlib.CategoryTheory.Abelian.Exact
/-- A functor which preserves the exactness of short complexes preserves homology.  -/
CategoryTheory.Functor.preservesHomology_of_map_exact : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Abelian A] [inst_3 : CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B)
  [inst_4 : L.PreservesZeroMorphisms],
  (∀ (S : CategoryTheory.ShortComplex A), S.Exact → (S.map L).Exact) → L.PreservesHomology
-- Lean.Meta.Tactic.Contradiction
/-- When checking for empty types, `searchFuel` specifies the number of goals visited.  -/
Lean.Meta.Contradiction.Config.searchFuel : Lean.Meta.Contradiction.Config → ℕ
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The isomorphism (in `Type`) between
morphisms from the colimit object to a specified object `W`,
and an explicit componentwise description of cocones with cone point `W`.
 -/
CategoryTheory.Limits.colimit.homIso' : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            (W : C) →
              ULift.{u₁, v} (CategoryTheory.Limits.colimit F ⟶ W) ≅
                { p // ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (F.map f) (p j') = p j }
-- Mathlib.GroupTheory.Congruence.Defs
ConGen.Rel.trans : ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → ConGen.Rel r x z
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.paper_eq1 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) {p : ℕ}, BirdDet.Eq1✝ A p
-- Mathlib.MeasureTheory.Measure.Restrict
comap_subtype_coe_apply : ∀ {α : Type u_2} {_m0 : MeasurableSpace α} {s : Set α},
  MeasurableSet s →
    ∀ (μ : MeasureTheory.Measure α) (t : Set ↑s), (MeasureTheory.Measure.comap Subtype.val μ) t = μ (Subtype.val '' t)
-- Mathlib.Order.Bounds.Basic
IsGreatest.nonempty : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsGreatest s a → s.Nonempty
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.exists_inv : ∀ {R : Type u_3} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided] [hI : I.IsMaximal] {a : R ⧸ I},
  a ≠ 0 → ∃ b, a * b = 1
-- Init.Data.Array.Lemmas
Array.mem_push_of_mem : ∀ {α : Type u_1} {xs : Array α} {x : α} (y : α), x ∈ xs → x ∈ xs.push y
-- Init.Data.SInt.Lemmas
instLawfulOrderLTInt16 : Std.LawfulOrderLT Int16
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.getLsbD_extractAndExtend_of_lt : ∀ {w k v pos : ℕ} {x : BitVec w},
  k < v → (BitVec.extractAndExtend v x).getLsbD (pos * v + k) = (BitVec.extractAndExtendBit pos v x).getLsbD k
-- Mathlib.Algebra.Group.Subsemigroup.Membership
/-- An induction principle for elements of `⨆ i, S i`.
If `C` holds all elements of `S i` for all `i`, and is preserved under multiplication,
then it holds for all elements of the supremum of `S`.  -/
Subsemigroup.iSup_induction : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Mul M] (S : ι → Subsemigroup M) {C : M → Prop} {x₁ : M},
  x₁ ∈ ⨆ i, S i → (∀ (i : ι), ∀ x₂ ∈ S i, C x₂) → (∀ (x y : M), C x → C y → C (x * y)) → C x₁
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.le_maxKeyD_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.contains k = true → ∀ {fallback : α}, (cmp k (t.maxKeyD fallback)).isLE = true
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.filter_nsmul : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α) (n : ℕ),
  Multiset.filter p (n • s) = n • Multiset.filter p s
-- Mathlib.Algebra.Algebra.Equiv
AlgEquivClass.toRingEquivClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : Semiring A} {inst_2 : Semiring B} {inst_3 : Algebra R A} {inst_4 : Algebra R B} {inst_5 : EquivLike F A B}
  [self : AlgEquivClass F R A B], RingEquivClass F A B
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.isoOfHomeo_hom_hom_hom_apply : ∀ {P : TopCat → Prop} {X Y : CompHausLike P} (f : ↑X.toTop ≃ₜ ↑Y.toTop)
  (a : ↑((CompHausLike.compHausLikeToTop P).obj X)), (TopCat.Hom.hom (CompHausLike.isoOfHomeo f).hom.hom) a = f a
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree_eq_zero : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)], G.degree v = 0 ↔ G.IsIsolated v