mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.isoOfComponents_inv_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.LaxMonoidalFunctor C D} (e : (X : C) → F.obj X ≅ G.obj X)
  (naturality :
    autoParam
      (∀ {X Y : C} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom = CategoryTheory.CategoryStruct.comp (e X).hom (G.map f))
      CategoryTheory.LaxMonoidalFunctor.isoOfComponents._auto_1)
  (unit :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor)
          (e (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom =
        CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor)
      CategoryTheory.LaxMonoidalFunctor.isoOfComponents._auto_3)
  (tensor :
    autoParam
      (∀ (X Y : C),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y)
            (e (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom)
            (CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y))
      CategoryTheory.LaxMonoidalFunctor.isoOfComponents._auto_5)
  (X : C), (CategoryTheory.LaxMonoidalFunctor.isoOfComponents e naturality unit tensor).inv.hom.app X = (e X).inv
-- Init.Data.Nat.Fold
Nat.dfoldRev_congr : ∀ {n m : ℕ} (w : n = m) {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfoldRev_congr._auto_1 → Type u}
  (f : (i : ℕ) → (h : i < n) → α (i + 1) ⋯ → α i ⋯) (init : α n ⋯),
  n.dfoldRev f init = m.dfoldRev (fun i h => f i ⋯) (cast ⋯ init)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.MorphismProperty.LeftFraction₂.symm_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {W : CategoryTheory.MorphismProperty C} {X Y : C} (φ : W.LeftFraction₂ X Y), φ.symm.add = φ.add
-- Mathlib.Algebra.Group.Defs
/-- Despite the asymmetry of `neg_eq_of_add`, the symmetric version is true thanks to the
involutivity of negation.  -/
SubtractionMonoid.neg_eq_of_add : ∀ {G : Type u} [self : SubtractionMonoid G] (a b : G), a + b = 0 → -a = b
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.coe_substAlgHom : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} (ha : MvPowerSeries.HasSubst a),
  ⇑(MvPowerSeries.substAlgHom ha) = MvPowerSeries.subst a
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instTransVleVeq : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : ValuativeRel R] → Trans ValuativeRel.vle ValuativeRel.veq ValuativeRel.vle
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.mem_iff : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜]
  {R : HomogeneousSubsemiring 𝒜} {a : A}, a ∈ R.toSubsemiring ↔ a ∈ R
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- **Alias** of `CategoryTheory.MorphismProperty.HasPushouts.hasPushout`. -/
CategoryTheory.MorphismProperty.hasPushout : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} [self : P.HasPushouts]
  {X Y S : C} {f : S ⟶ X} (g : S ⟶ Y), P f → CategoryTheory.Limits.HasPushout f g
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.forall : ∀ {α : Type u} {p : WithZero α → Prop}, (∀ (x : WithZero α), p x) ↔ p 0 ∧ ∀ (a : α), p ↑a
-- Mathlib.Data.Set.Finite.Lattice
Set.iUnion_univ_pi_of_monotone : ∀ {ι : Type u_1} {ι' : Type u_2} [inst : LinearOrder ι'] [Nonempty ι'] [Finite ι] {α : ι → Type u_3}
  {s : (i : ι) → ι' → Set (α i)},
  (∀ (i : ι), Monotone (s i)) → (⋃ j, Set.univ.pi fun i => s i j) = Set.univ.pi fun i => ⋃ j, s i j
-- Mathlib.Algebra.Star.Basic
semiconjBy_star_star_star : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x y z : R}, SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.on_subset : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α}
  {t : Set α}, IsLocalMaxOn f t a → s ⊆ t → IsLocalMaxOn f s a
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.stmts₁.match_1.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4) (a : Γ → σ → Γ)
  (q : Turing.TM1.Stmt Γ Λ σ)
  (h_1 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.move a q → motive (Turing.TM1.Stmt.move a q))
  (h_2 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → Γ) →
        (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.write a q → motive (Turing.TM1.Stmt.write a q))
  (h_3 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.load a q → motive (Turing.TM1.Stmt.load a q))
  (h_4 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → Bool) →
        (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.branch a q₁ q₂ → motive (Turing.TM1.Stmt.branch a q₁ q₂))
  (h_5 : (Q : Turing.TM1.Stmt Γ Λ σ) → motive Q),
  (match Turing.TM1.Stmt.write a q with
    | Q@h:(Turing.TM1.Stmt.move a q) => h_1 Q a q h
    | Q@h:(Turing.TM1.Stmt.write a q) => h_2 Q a q h
    | Q@h:(Turing.TM1.Stmt.load a q) => h_3 Q a q h
    | Q@h:(Turing.TM1.Stmt.branch a q₁ q₂) => h_4 Q a q₁ q₂ h
    | Q => h_5 Q) =
    h_2 (Turing.TM1.Stmt.write a q) a q ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularMonoCategory.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.IsRegularMono f) →
    CategoryTheory.IsRegularMonoCategory C
-- Mathlib.Order.Filter.Bases.Basic
Filter.map_sigma_mk_comap : ∀ {α : Type u_1} {β : Type u_2} {π : α → Type u_6} {π' : β → Type u_7} {f : α → β},
  Function.Injective f →
    ∀ (g : (a : α) → π a → π' (f a)) (a : α) (l : Filter (π' (f a))),
      Filter.map (Sigma.mk a) (Filter.comap (g a) l) = Filter.comap (Sigma.map f g) (Filter.map (Sigma.mk (f a)) l)
-- Mathlib.NumberTheory.NumberField.AdeleRing
NumberField.instAlgebraAdeleRing : (R : Type u_2) →
  (K : Type u_1) →
    [inst : CommRing R] →
      [inst_1 : IsDedekindDomain R] →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → Algebra K (NumberField.AdeleRing R K)
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.congrLeft` as an `AlgEquiv`.  -/
LocallyConstant.congrLeftₐ : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {Z : Type u_6} →
          (R : Type u_7) →
            [inst_2 : CommSemiring R] →
              [inst_3 : Semiring Z] → [inst_4 : Algebra R Z] → X ≃ₜ Y → LocallyConstant X Z ≃ₐ[R] LocallyConstant Y Z
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.Finite.Rel.of_productive : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  {a b : Std.IterM.TerminationMeasures.Finite α m}, { it := a.it }.Rel { it := b.it } → a.Rel b
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.inv_hom_whiskerRight' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f] (Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.inv f) Z)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)
-- Mathlib.Topology.Category.Stonean.Basic
CompHaus.lift_lifts_assoc : ∀ {X Y : CompHaus} {Z : Stonean} (e : Z.compHaus ⟶ Y) (f : X ⟶ Y) [inst : CategoryTheory.Epi f] {Z_1 : CompHaus}
  (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CompHaus.lift e f) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp e h
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.lift_commutes_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z)
  (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.ProjectiveResolution.lift f P Q).f 0) (Q.π.f 0) =
    CategoryTheory.CategoryStruct.comp (P.π.f 0) f
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_right_Q : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ) (hpq : (c r).prev pq' = pq)
  (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') [inst_3 : X.HasSpectralSequence data]
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData X data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀
          i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).right.Q =
    X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.type.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.type = 1
-- Mathlib.Algebra.Group.Defs
ZSMul.mk : {G : Type u} → (ℤ → G → G) → ZSMul G
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.leadingCoeff_eq_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R},
  x.leadingCoeff = 0 ↔ x = 0
-- Std.Data.ExtDHashMap.Basic
/-- Removes all mappings of the hash map for which the given function returns `false`.  -/
Std.ExtDHashMap.filter : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [EquivBEq α] → [LawfulHashable α] → ((a : α) → β a → Bool) → Std.ExtDHashMap α β → Std.ExtDHashMap α β
-- Init.Data.Nat.Basic
Nat.sub_lt_left_of_lt_add : ∀ {n k m : ℕ}, n ≤ k → k < n + m → k - n < m
-- Mathlib.Order.Antichain
IsAntichain.to_dual_iff : ∀ {α : Type u_1} {s : Set α} [inst : LE α], IsAntichain (fun x1 x2 => x1 ≤ x2) s ↔ IsAntichain (fun x1 x2 => x1 ≤ x2) s
-- Init.Data.BitVec.Lemmas
/-- If a bitvec is different than zero the bits at indexes lower than `ctz x` are false.  -/
BitVec.getLsbD_false_of_lt_ctz : ∀ {w i : ℕ} {x : BitVec w}, i < x.ctz.toNat → x.getLsbD i = false
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.leadingCoeff_ne_zero : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A],
  Function.Injective D → (AddMonoidAlgebra.leadingCoeff D p ≠ 0 ↔ p ≠ 0)
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {cX cY : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X cX μ →
    ProbabilityTheory.HasSubgaussianMGF Y cY μ →
      ProbabilityTheory.IndepFun X Y μ → ProbabilityTheory.HasSubgaussianMGF (fun ω => X ω + Y ω) (cX + cY) μ
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceLErase_eq_balanceL! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size},
  Std.DTreeMap.Internal.Impl.balanceLErase k v l r hlb hrb hlr = Std.DTreeMap.Internal.Impl.balanceL! k v l r
-- Init.Data.UInt.IntToBitVec
UInt32.toBitVec64_toUSize : ∀ (n : UInt32) (h : System.Platform.numBits = 64), n.toUSize.toBitVec64 h = BitVec.setWidth 64 n.toBitVec
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.decidableLE : {α : Type u_1} →
  [inst : AddCommMonoid α] →
    [inst_1 : PartialOrder α] →
      [inst_2 : IsOrderedCancelAddMonoid α] → {s : AddSubmonoid α} → [DecidableLE α] → DecidableLE (AddLocalization s)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapRingEquiv_single : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (e : R ≃+* S) (r : R) (m : M),
  (MonoidAlgebra.mapRingEquiv M e) (MonoidAlgebra.single m r) = MonoidAlgebra.single m (e r)
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- The conditional kernel CDF of a kernel `κ : Kernel α (γ × ℝ)`, where `γ` is countably generated.
 -/
ProbabilityTheory.Kernel.condKernelCDF : {α : Type u_1} →
  {γ : Type u_3} →
    {mα : MeasurableSpace α} →
      {mγ : MeasurableSpace γ} →
        [MeasurableSpace.CountablyGenerated γ] →
          (κ : ProbabilityTheory.Kernel α (γ × ℝ)) → [ProbabilityTheory.IsFiniteKernel κ] → α × γ → StieltjesFunction ℝ
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p ≠ 0 → ∀ (n : ℕ), (p * Polynomial.X ^ n).natTrailingDegree = p.natTrailingDegree + n
-- Mathlib.Order.Hom.Lattice
LatticeHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {f g : LatticeHom α β},
  f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.closure_eq_top_of_mclosure_eq_top : ∀ {G : Type u_1} [inst : Group G] {S : Set G}, Submonoid.closure S = ⊤ → Subgroup.closure S = ⊤
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- Multiplication in the `Language.ring.Structure` is the same as the multiplication given by the
`Mul` instance  -/
FirstOrder.Ring.CompatibleRing.funMap_mul : ∀ {R : Type u_2} {inst : Add R} {inst_1 : Mul R} {inst_2 : Neg R} {inst_3 : One R} {inst_4 : Zero R}
  [self : FirstOrder.Ring.CompatibleRing R] (x : Fin 2 → R),
  FirstOrder.Language.Structure.funMap FirstOrder.Ring.mulFunc x = x 0 * x 1
-- Lean.Parser
Lean.PrettyPrinter.Formatter.interpretParserDescr : Lean.ParserDescr → Lean.CoreM Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_f : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J]
  [inst_4 : Small.{u, w} J] (j : J),
  (AlgebraicGeometry.Scheme.IsLocallyDirected.openCover F).f j = CategoryTheory.Limits.colimit.ι F j
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneRightOpOfCoconeEquiv_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C},
  CategoryTheory.Limits.coneRightOpOfCoconeEquiv.counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun c => Opposite.op (CategoryTheory.Limits.coconeOfConeRightOp c),
            map := fun {Y X} f => Opposite.op { hom := f.hom.unop, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp
        { obj := fun c => CategoryTheory.Limits.coneRightOpOfCocone (Opposite.unop c),
          map := fun {Y X} f => { hom := f.unop.hom.op, w := ⋯ }, map_id := ⋯, map_comp := ⋯ })
-- Mathlib.Algebra.Module.LocalizedModule.Basic
_private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.zero_smul_aux : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {T : Type u_1} [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : IsLocalization S T]
  (p : LocalizedModule S M), 0 • p = 0
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_le_pow : ∀ (n : ℕ), n.factorial ≤ n ^ n
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.bsup_lt_ord_of_isRegular : ∀ {o : Ordinal.{max u_1 u_2}} {f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}}
  {c : Cardinal.{max u_1 u_2}},
  c.IsRegular → o.card < c → (∀ (i : Ordinal.{max u_1 u_2}) (hi : i < o), f i hi < c.ord) → o.bsup f < c.ord
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k fallback : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter! f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)).getD fallback
-- Mathlib.Combinatorics.SimpleGraph.Ends.Properties
SimpleGraph.componentComplFunctor_nonempty_of_infinite : ∀ {V : Type} (G : SimpleGraph V) [Infinite V] (K : (Finset V)ᵒᵖ), Nonempty (G.componentComplFunctor.obj K)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.CategoryStruct.comp S.v₀₁.τ₁ S.v₁₂.τ₁ = 0
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgHom.map_adjoin : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A]
  [inst_2 : StarRing A] [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] [inst_10 : StarRing R]
  [inst_11 : IsScalarTower R A A] [inst_12 : SMulCommClass R A A] [inst_13 : StarModule R A]
  [inst_14 : IsScalarTower R B B] [inst_15 : SMulCommClass R B B] [inst_16 : StarModule R B] (f : F) (s : Set A),
  NonUnitalStarSubalgebra.map f (NonUnitalStarAlgebra.adjoin R s) = NonUnitalStarAlgebra.adjoin R (⇑f '' s)
-- Std.Time.Zoned
/-- Creates a new `DateTime` out of a `PlainDateTime` and a time zone identifier.
 -/
Std.Time.DateTime.of : Std.Time.PlainDateTime → String → IO Std.Time.DateTime
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.im_nnratCast : ∀ {K : Type u_1} [inst : Field K] {a b : K} (q : ℚ≥0), (NNRatCast.nnratCast q).im = 0
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Icc_sub_one_right_eq_Ico : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] [NoMinOrder α] (a b : α), Finset.Icc a (b - 1) = Finset.Ico a b
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.Ordinal.instDecidableLeOfDay : {x y : Std.Time.Nanosecond.Ordinal.OfDay} → Decidable (x ≤ y)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.div_mem_div : ∀ {α : Type u_2} [inst : Div α] {s t : Set α} {a b : α}, a ∈ s → b ∈ t → a / b ∈ s / t
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.toIntermediateField : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] →
      [inst_1 : Field K] → [inst_2 : Algebra k K] → FiniteGaloisIntermediateField k K → IntermediateField k K
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
/-- Constructor for the type of non degenerate simplices of a simplicial set.  -/
SSet.N.mk : {X : SSet} → {n : ℕ} → (x : X.obj (Opposite.op { len := n })) → x ∈ X.nonDegenerate n → X.N
-- Plausible.Sampleable
Plausible.NoShrink.inhabited : {α : Type u_1} → [inst : Inhabited α] → Inhabited (Plausible.NoShrink α)
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.toMulEquiv : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group E] →
          [inst_2 : Group G] →
            {S : GroupExtension N E G} →
              {E' : Type u_4} → [inst_3 : Group E'] → {S' : GroupExtension N E' G} → S.Equiv S' → E ≃* E'
-- Std.Async.Process
/-- Changes the current working directory to a new one.
 -/
Std.IO.Process.setCwd : System.FilePath → IO Unit
-- Std.Data.HashMap.Basic
/-- The notation `m[a]` or `m[a]'h` is preferred over calling this function directly.

Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of
`a ∈ m`.
 -/
Std.HashMap.get : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → (m : Std.HashMap α β) → (a : α) → a ∈ m → β
-- Mathlib.Combinatorics.SetFamily.Compression.Down
/-- `a` is in the down-compressed family iff it's in the original and its compression is in the
original, or it's not in the original but it's the compression of something in the original.  -/
Down.mem_compression : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α},
  s ∈ Down.compression a 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- Evaluation of a `ContinuousMultilinearMap` at a vector as an `AddMonoidHom`.  -/
ContinuousMultilinearMap.applyAddHom : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] →
                      [inst_7 : ContinuousAdd M₂] → ((i : ι) → M₁ i) → ContinuousMultilinearMap R M₁ M₂ →+ M₂
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
multipliable_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {L : SummationFilter β}
  [IsEmpty β], Multipliable f L
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.mk : {R : Type u_1} →
  [inst : CommRing R] →
    (toSubsemiring : Subsemiring R) →
      autoParam (∀ {x : R}, IsSquare x → x ∈ toSubsemiring.carrier) RingPreordering.mem_of_isSquare'._autoParam →
        autoParam (-1 ∉ toSubsemiring.carrier) RingPreordering.neg_one_notMem'._autoParam → RingPreordering R
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instIsBoundedSMulSubtypePreLpMemAddSubgroup : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedRing 𝕜] [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)]
  [inst_4 : Fact (1 ≤ p)], IsBoundedSMul 𝕜 ↥(lp E p)
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.instSMulRat : {M : Type u_2} → [inst : AddCommGroup M] → SMul ℚ (DivisibleHull M)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.instContractibleSpace : ContractibleSpace UpperHalfPlane
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.le_order_pow : ∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R) (n : ℕ), n • φ.order ≤ (φ ^ n).order
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.module : Lean.Lsp.SymbolKind
-- Mathlib.Data.Finmap
AList.singleton.eq_1 : ∀ {α : Type u} {β : α → Type v} (a : α) (b : β a), AList.singleton a b = { entries := [⟨a, b⟩], nodupKeys := ⋯ }