mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.is_cover : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {G : CategoryTheory.Functor C D}
  {K : CategoryTheory.GrothendieckTopology D} [self : G.IsCoverDense K] (U : D),
  CategoryTheory.Sieve.coverByImage G U ∈ K U
-- Mathlib.Data.Finset.Sups
Finset.forall_infs_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t : Finset α} {p : α → Prop},
  (∀ c ∈ s ⊼ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊓ b)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- For `Unique one`, the equivariant map from `one ↪ α` to `α`  -/
AddActionHom.zeroEmbeddingMap : {G : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup G] → [inst_1 : AddAction G α] → {zero : Type u_5} → [Unique zero] → (zero ↪ α) →ₑ[id] α
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.denote_mkConst : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {val : Bool} {aig : Std.Sat.AIG α},
  ⟦assign, aig.mkConst val⟧ = val
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.subgroupMap_symm_apply : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (e : G ≃* G') (H : Subgroup G)
  (g : ↥(Subgroup.map (↑e) H)), (e.subgroupMap H).symm g = ⟨e.symm ↑g, ⋯⟩
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- Corollary of Chinese Remainder Theorem: if `Iᵢ` are pairwise coprime ideals in a
commutative ring then given elements `xᵢ` you can find `r` with `r - xᵢ ∈ Iᵢ` for all `i`.  -/
Ideal.exists_forall_sub_mem_ideal : ∀ {R : Type u_2} [inst : CommRing R] {ι : Type u_3} [Finite ι] {I : ι → Ideal R},
  Pairwise (Function.onFun IsCoprime I) → ∀ (x : ι → R), ∃ r, ∀ (i : ι), r - x i ∈ I i
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eccent_eq_zero_of_subsingleton : ∀ {α : Type u_1} {G : SimpleGraph α} [Subsingleton α] (u : α), G.eccent u = 0
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.commSemigroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst_1 : CommSemigroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f)
  (mul : ∀ (x y : M₁), f (x * y) = f x * f y),
  Function.Surjective.commSemigroup f hf mul = { toSemigroup := Function.Surjective.semigroup f hf mul, mul_comm := ⋯ }
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- If `2` is invertible in the coefficient ring,
a quadratic map is nondegenerate iff its radical is 0.
(Use `QuadraticMap.Nondegenerate.radical_eq_bot`
for the one-way implication in all characteristics.)
 -/
QuadraticMap.nondegenerate_iff_radical_eq_bot : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] {Q : QuadraticMap R M P} [Invertible 2],
  QuadraticMap.Nondegenerate ↔ Q.radical = ⊥
-- Batteries.Recycling.MonadSatisfying.Array
_private.Batteries.Recycling.MonadSatisfying.Array.0.Array.SatisfiesM_anyM.go : ∀ {m : Type → Type u_1} {α : Type u_2} {start stop : ℕ} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α}
  (tru : Prop) (fal : ℕ → Prop) {stop_1 j : ℕ},
  j ≤ stop_1 →
    ∀ (hstop : stop_1 ≤ as.size),
      fal j →
        (∀ (i : Fin as.size), ↑i < stop_1 → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])) →
          SatisfiesM (fun res => bif res then tru else fal stop_1) (Array.anyM.loop p as stop_1 hstop j)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.rightHomologyFunctor_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C],
  (CategoryTheory.ShortComplex.rightHomologyFunctor C).Additive
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
/-- **Alias** of `SkewMonoidAlgebra.coeff_update`. -/
SkewMonoidAlgebra.update_toFinsupp : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (f : SkewMonoidAlgebra M α) (a : α) (b : M),
  (f.update a b).coeff = f.coeff.update a b
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.Functor.instPreservesMonomorphisms : ∀ {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] (F : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [inst_6 : F.PreservesZeroMorphisms]
  [F.PreservesHomology], F.PreservesMonomorphisms
-- Init.Data.Rat.Lemmas
Rat.add_zero : ∀ (a : ℚ), a + 0 = a
-- Mathlib.Data.Complex.Basic
Complex.mk : ℝ → ℝ → ℂ
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- `a` is less than `b` if and only if `b` is a proper transitive successor of `a`.
 -/
Std.PRange.LawfulUpwardEnumerableLT.lt_iff : ∀ {α : Type u} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : LT α} [self : Std.PRange.LawfulUpwardEnumerableLT α]
  (a b : α), a < b ↔ Std.PRange.UpwardEnumerable.LT a b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ofList_eq_insertMany_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {l : List (α × β)},
  Std.ExtDTreeMap.Const.ofList l cmp = Std.ExtDTreeMap.Const.insertMany ∅ l
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_eq_default : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, a ∉ m → m.getKey! a = default
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.MorphismProperty.IsMonoidalStable.toIsStableUnderUnitor : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P : CategoryTheory.MorphismProperty C}
  {inst_1 : CategoryTheory.MonoidalCategory C} [self : P.IsMonoidalStable], P.IsStableUnderUnitor
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- `Multiseries`-part of `MultiseriesExpansion.monomialRpow`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow : (basis_hd : ℝ → ℝ) →
  (basis_tl : Tactic.ComputeAsymptotics.Basis) →
    ℕ → ℝ → Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl
-- Mathlib.RingTheory.AdjoinRoot
/-- **Alias** of `AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk`.

---

The natural isomorphism `R[α]/((I[x] ⊔ (f)) / (f)) ≅ (R[x]/I[x])/((f) ⊔ I[x] / I[x])`
for `α` a root of `f : R[X]` and `I : Ideal R`  -/
AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (f : Polynomial R) →
        AdjoinRoot f ⧸ Ideal.map (AdjoinRoot.mk f) (Ideal.map Polynomial.C I) ≃+*
          (Polynomial R ⧸ Ideal.map Polynomial.C I) ⧸
            Ideal.map (Ideal.Quotient.mk (Ideal.map Polynomial.C I)) (Ideal.span {f})
-- Mathlib.Order.Heyting.Basic
compl_iff_not : ∀ (p : Prop), pᶜ ↔ ¬p
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opEquivalence_counitIso : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V],
  (HomologicalComplex.opEquivalence V c).counitIso = HomologicalComplex.opCounitIso V c
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
/-- The functor `F` is Cartesian closed (i.e. preserves exponentials) if each natural transformation
`expComparison F A` is an isomorphism
 -/
CategoryTheory.MonoidalClosedFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v, u'} D] →
        [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [CategoryTheory.MonoidalClosed C] →
                [CategoryTheory.MonoidalClosed D] →
                  [CategoryTheory.Limits.PreservesLimitsOfShape
                        (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] →
                    Prop
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom'_assoc : ∀ {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] (x : D) {y z : C} (f : y ⟶ z)
  [inst_4 : CategoryTheory.IsIso f] {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x z ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x (CategoryTheory.inv f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f)
        h) =
    h
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mu_self : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (a : α), (IncidenceAlgebra.mu 𝕜) a a = 1
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
/-- the vertices in each face are affine independent: this is an implementation detail  -/
Geometry.SimplicialComplex.indep : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] (self : Geometry.SimplicialComplex 𝕜 E) {s : Finset E},
  s ∈ self.faces → AffineIndependent 𝕜 Subtype.val
-- Init.Data.String.Decode
ByteArray.isUTF8FirstByte_of_validateUTF8At : ∀ {b : ByteArray} {i : ℕ} (h : b.validateUTF8At i = true), b[i].IsUTF8FirstByte
-- Lean.Meta.Tactic.Acyclic
/-- Close the given goal if `h` is a proof for an equality such as `as = a :: as`.
Inductive datatypes in Lean are acyclic.
 -/
Lean.MVarId.acyclic : Lean.MVarId → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Order.Heyting.Basic
hnot_le_hnot : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, b ≤ a → ￢a ≤ ￢b
-- Mathlib.Algebra.Group.Units.Equiv
/-- A multiplicative equivalence of monoids defines a multiplicative equivalence
of their groups of units.  -/
Units.mapEquiv : {M : Type u_3} → {N : Type u_4} → [inst : Monoid M] → [inst_1 : Monoid N] → M ≃* N → Mˣ ≃* Nˣ
-- Mathlib.Order.Filter.Subsingleton
Filter.HasBasis.subsingleton_iff : ∀ {α : Type u_1} {l : Filter α} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → (l.Subsingleton ↔ ∃ i, p i ∧ (s i).Subsingleton)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.X_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {φ : MvPowerSeries σ R} {s : σ},
  MvPowerSeries.X s * φ = φ * MvPowerSeries.X s
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ico_sub_bot : ∀ {M : Type u_4} (f : ℕ → M) {m n : ℕ} [inst : AddCommGroup M],
  m < n → ∑ i ∈ Finset.Ico m n, f i - f m = ∑ i ∈ Finset.Ico (m + 1) n, f i
-- Init.Data.Rat.Basic
Rat.pow : ℚ → ℕ → ℚ
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.toAlgebra : {R : Type u} → {A : Type v} → {inst : CommSemiring R} → {inst_1 : Semiring A} → [self : Bialgebra R A] → Algebra R A
-- Init.Data.Array.Monadic
List.flatMapM_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α}
  {f : α → m (Array β)}, Array.flatMapM f l.toArray = List.toArray <$> List.flatMapM (fun a => Array.toList <$> f a) l
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHomLeft : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᵒᵖ Dᵒᵖ] {c c' : D} (f : c ⟶ c') (d : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f d =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f.op (Opposite.op d)).unop
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_of_mem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  l.contains k = false → k ∈ Std.ExtDTreeMap.Const.insertManyIfNewUnit t l → k ∈ t
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- If `f` is real-meromorphic on a compact interval, then `log ‖f ·‖` is interval integrable on this
interval.
 -/
MeromorphicOn.intervalIntegrable_log_norm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ},
  MeromorphicOn f (Set.uIcc a b) → IntervalIntegrable (fun x => Real.log ‖f x‖) MeasureTheory.volume a b
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- Composition of a group seminorm with a monoid homomorphism as a group seminorm.  -/
GroupSeminorm.comp : {E : Type u_3} → {F : Type u_4} → [inst : Group E] → [inst_1 : Group F] → GroupSeminorm E → (F →* E) → GroupSeminorm F
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
Lean.Meta.Grind.Arith.Cutsat.getAssignment? : Lean.Meta.Grind.Goal → Lean.Expr → Lean.MetaM (Option ℚ)
-- Mathlib.Data.ZMod.QuotientGroup
/-- Partition `G ⧸ H` into orbits of the action of `g : G`.  -/
Subgroup.quotientEquivSigmaZMod : {G : Type u_3} →
  [inst : Group G] →
    (H : Subgroup G) →
      (g : G) →
        G ⧸ H ≃
          (q : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers g)) (G ⧸ H)) ×
            ZMod (Function.minimalPeriod (fun x => g • x) (Quotient.out q))
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag_zero : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : Zero α], Matrix.blockDiag 0 = 0
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.null_iff_toMeasure_null : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω), ν s = 0 ↔ ↑ν s = 0
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.size_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.size = t₂.size
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.const_mul_right' : ∀ {α : Type u_1} {E : Type u_3} {R : Type u_13} [inst : Norm E] [inst_1 : SeminormedRing R] {f : α → E} {l : Filter α}
  {g : α → R} {u : Rˣ} {c' : ℝ},
  0 ≤ c' → Asymptotics.IsBigOWith c' l f g → Asymptotics.IsBigOWith (c' * ‖↑u⁻¹‖) l f fun x => ↑u * g x
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.isClosed_preimage_ofLawson : ∀ {α : Type u_1} [inst : Preorder α] {S : Set α}, IsClosed (⇑Topology.WithLawson.ofLawson ⁻¹' S) ↔ IsClosed S
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.id_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) (x : M), (LinearMap.BilinForm.Isometry.id B) x = x
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapLeftHomologyIso_hom_naturality : ∀ {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₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasLeftHomology]
  [inst_6 : S₂.HasLeftHomology] [inst_7 : F.PreservesLeftHomologyOf S₁] [inst_8 : F.PreservesLeftHomologyOf S₂],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap (F.mapShortComplex.map φ))
      (S₂.mapLeftHomologyIso F).hom =
    CategoryTheory.CategoryStruct.comp (S₁.mapLeftHomologyIso F).hom
      (F.map (CategoryTheory.ShortComplex.leftHomologyMap φ))
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.ofUnits_units_le : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M), S.units.ofUnits ≤ S
-- Init.Data.SInt.Lemmas
Int16.toUInt16_ofNat : ∀ {n : ℕ}, Int16.toUInt16 (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Analysis.Calculus.Deriv.Abs
HasFDerivWithinAt.abs : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {s : Set E}
  {x : E}, HasFDerivWithinAt f f' s x → f x ≠ 0 → HasFDerivWithinAt (fun x => |f x|) (↑(SignType.sign (f x)) • f') s x
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.SimpleFunc.coe_toLargerSpace_eq : ∀ {β : Type u_6} {γ : Type u_7} {m m0 : MeasurableSpace β} (hm : m ≤ m0) (f : MeasureTheory.SimpleFunc β γ),
  ⇑(MeasureTheory.SimpleFunc.toLargerSpace hm f) = ⇑f
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Revert.revert : ∀ {σs : List (Type u)} {P Q H T : Std.Do.SPred σs}, (P ⊣⊢ₛ Q ∧ H) → (Q ⊢ₛ H → T) → P ⊢ₛ T
-- Mathlib.Tactic.DuplicateDecls
Mathlib.Tactic.DuplicateDecls.Target.instances.sizeOf_spec : sizeOf Mathlib.Tactic.DuplicateDecls.Target.instances = 1
-- Init.Data.NeZero
/-- The proposition that `n` is not zero.  -/
NeZero.out : ∀ {R : Type u_1} {inst : Zero R} {n : R} [self : NeZero n], n ≠ 0
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinAt.mono_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s t : Set E} {x : E},
  HasFPowerSeriesWithinAt f p s x → s ∈ nhdsWithin x t → HasFPowerSeriesWithinAt f p t x
-- Mathlib.Algebra.Algebra.Unitization
Unitization.toAddEquiv_linearEquiv : ∀ {S : Type u_2} {R : Type u_3} {A : Type u_4} [inst : Semiring S] [inst_1 : AddCommMonoid R] [inst_2 : AddCommMonoid A]
  [inst_3 : Module S R] [inst_4 : Module S A], (Unitization.linearEquiv S R A).toAddEquiv = Unitization.addEquiv R A
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_sq_eq_def_ax : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K] (z : K),
  ‖z‖ ^ 2 = RCLike.re z * RCLike.re z + RCLike.im z * RCLike.im z
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instLawfulBEqPoly : LawfulBEq Lean.Grind.Linarith.Poly
-- Mathlib.Order.Monotone.Defs
/-- **Alias** of the reverse direction of `antitone_iff_apply₂`. -/
Antitone.of_apply₂ : ∀ {ι : Type u_1} {α : Type u} {β : ι → Type u_4} [inst : (i : ι) → Preorder (β i)] [inst_1 : Preorder α]
  {f : α → (i : ι) → β i}, (∀ (i : ι), Antitone fun x => f x i) → Antitone f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemTag.deprecated : Lean.Lsp.CompletionItemTag
-- Lean.Meta.Tactic.SolveByElim
Lean.Meta.SolveByElim.ApplyRulesConfig.mk : Lean.Meta.Tactic.Backtrack.BacktrackConfig →
  Lean.Meta.ApplyConfig → Lean.Meta.TransparencyMode → Bool → Bool → Lean.Meta.SolveByElim.ApplyRulesConfig
-- Mathlib.CategoryTheory.Adjunction.Lifting.Right
/-- Suppose we have a commutative square of functors

```
      Q
    A → B
  U ↓   ↓ V
    C → D
      L
```

where `U` has a right adjoint, `A` has coreflexive equalizers and `V` has a right adjoint such that
each component of the counit is a regular mono.
Then `Q` has a right adjoint if `L` has a right adjoint.

See https://ncatlab.org/nlab/show/adjoint+lifting+theorem
 -/
CategoryTheory.isLeftAdjoint_square_lift : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (Q : CategoryTheory.Functor A B) (V : CategoryTheory.Functor B D)
  (U : CategoryTheory.Functor A C) (L : CategoryTheory.Functor C D) (comm : U.comp L ≅ Q.comp V) [U.IsLeftAdjoint]
  [inst_5 : V.IsLeftAdjoint] [L.IsLeftAdjoint]
  (h : (X : B) → CategoryTheory.RegularMono ((CategoryTheory.Adjunction.ofIsLeftAdjoint V).unit.app X))
  [CategoryTheory.Limits.HasCoreflexiveEqualizers A], Q.IsLeftAdjoint
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.injective_isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Injective)
-- Mathlib.Topology.MetricSpace.Dilation
Isometry.toDilation.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (f f_1 : α → β)
  (e_f : f = f_1) (hf : Isometry f), Isometry.toDilation f hf = Isometry.toDilation f_1 ⋯
-- Init.Data.List.Perm
/-- Similar to `Perm.recOn`, but the `swap` case is generalized to `Perm.swap'`,
where the tail of the lists are not necessarily the same.
 -/
List.Perm.recOnSwap' : ∀ {α : Type u_1} {motive : (l₁ l₂ : List α) → l₁.Perm l₂ → Prop} {l₁ l₂ : List α} (p : l₁.Perm l₂),
  motive [] [] ⋯ →
    (∀ (x : α) {l₁ l₂ : List α} (h : l₁.Perm l₂), motive l₁ l₂ h → motive (x :: l₁) (x :: l₂) ⋯) →
      (∀ (x y : α) {l₁ l₂ : List α} (h : l₁.Perm l₂), motive l₁ l₂ h → motive (y :: x :: l₁) (x :: y :: l₂) ⋯) →
        (∀ {l₁ l₂ l₃ : List α} (h₁ : l₁.Perm l₂) (h₂ : l₂.Perm l₃),
            motive l₁ l₂ h₁ → motive l₂ l₃ h₂ → motive l₁ l₃ ⋯) →
          motive l₁ l₂ p
-- Init.Internal.Order.Basic
/-- A “less-or-equal-to” or “approximates” relation.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.PartialOrder.rel : {α : Sort u} → [self : Lean.Order.PartialOrder α] → α → α → Prop
-- Mathlib.Lean.Expr.Basic
/-- Invariant: `i : ℕ` should be less than the size of `as : Array Expr`.  -/
_private.Mathlib.Lean.Expr.Basic.0.Lean.Expr.getAppAppsAux : Lean.Expr → Array Lean.Expr → ℕ → Array Lean.Expr
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureResult.postState : Aesop.Script.DynStructureResult → Lean.Meta.SavedState
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ}
  (A B : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ),
  B ≠ A →
    ∀ {Z : C} (h : s.N (Opposite.unop B.fst).len ⟶ Z),
      CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp (s.πSummand B) h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.RepresentationTheory.Maschke
MonoidAlgebra.Submodule.exists_isCompl : ∀ {k : Type u_1} [inst : Field k] {G : Type u_2} [Finite G] [NeZero ↑(Nat.card G)] [inst_3 : Group G] {V : Type u_3}
  [inst_4 : AddCommGroup V] [inst_5 : Module (MonoidAlgebra k G) V] (p : Submodule (MonoidAlgebra k G) V),
  ∃ q, IsCompl p q
-- Aesop.Builder.NormSimp
Aesop.PhaseSpec.getSimpPrio : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Aesop.PhaseSpec → m ℕ
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.const.injEq : ∀ (a : Lean.Name) (a_1 : ℕ) (a_2 : Lean.Name) (a_3 : ℕ),
  (Lean.Meta.LazyDiscrTree.Key.const a a_1 = Lean.Meta.LazyDiscrTree.Key.const a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- If `f f' : X ⟶ Y`, `g : Y ⟶ Z` forms a pushout square, then `g` is the coequalizer of
`f` and `f'`.  -/
CategoryTheory.IsPushout.isLimitFork : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      {f f' : X ⟶ Y} →
        {g : Y ⟶ Z} →
          (H : CategoryTheory.IsPushout f f' g g) →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ g ⋯)
-- Mathlib.NumberTheory.Multiplicity
Int.emultiplicity_pow_add_pow : ∀ {p : ℕ},
  Nat.Prime p →
    Odd p →
      ∀ {x y : ℤ},
        ↑p ∣ x + y →
          ¬↑p ∣ x →
            ∀ {n : ℕ}, Odd n → emultiplicity (↑p) (x ^ n + y ^ n) = emultiplicity (↑p) (x + y) + emultiplicity p n
-- Mathlib.Algebra.Order.SuccPred
Order.not_isSuccPrelimit_add_one : ∀ {α : Type u_1} [inst : PartialOrder α] (a : α) [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α] [NoMaxOrder α],
  ¬Order.IsSuccPrelimit (a + 1)
-- Mathlib.Algebra.Regular.SMul
IsSMulRegular.right_eq_zero_of_smul : ∀ {R : Type u_1} {M : Type u_3} [inst : Zero M] [inst_1 : SMulZeroClass R M] {r : R} {x : M},
  IsSMulRegular M r → r • x = 0 → x = 0