mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Matroidᵣ.le_iff : ∀ {α : Type u_1} {M M' : Matroid.Matroidᵣ α}, M ≤ M' ↔ M.toMatroid.IsRestriction M'.toMatroid
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_eq_getD_back?_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α}, t.maxKeyD fallback = t.keysArray.back?.getD fallback
-- Mathlib.Data.Setoid.Basic
/-- Given a function `f : α → β` and equivalence relation `r` on `α`, the equivalence
closure of the relation on `f`'s image defined by '`x ≈ y` iff the elements of `f⁻¹(x)` are
related to the elements of `f⁻¹(y)` by `r`.'  -/
Setoid.map : {α : Type u_1} → {β : Type u_2} → Setoid α → (α → β) → Setoid β
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.mk.sizeOf_spec : ∀ {R : Type u_14} {S : Type u_15} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type u_16}
  {M₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂]
  [inst_6 : SizeOf R] [inst_7 : SizeOf S] [inst_8 : SizeOf M] [inst_9 : SizeOf M₂] (toAddHom : M →ₙ+ M₂)
  (map_smul' : ∀ (m : R) (x : M), toAddHom.toFun (m • x) = σ m • toAddHom.toFun x),
  sizeOf { toAddHom := toAddHom, map_smul' := map_smul' } = 1 + sizeOf toAddHom
-- Mathlib.Order.Closure
/-- An element is less than or equal its closure  -/
ClosureOperator.le_closure' : ∀ {α : Type u_1} [inst : Preorder α] (self : ClosureOperator α) (x : α), x ≤ self.toFun x
-- Lean.Parser.Term
/-- `inferInstanceAs α` synthesizes an instance of type `α` and then adjusts it to conform to the
expected type `β`, which must be inferable from context.

Example:
```
def D := Nat
instance : Inhabited D := inferInstanceAs (Inhabited Nat)
```

The adjustment will make sure that when the resulting instance will not "leak" the RHS `Nat` when
reduced at transparency levels below `semireducible`, i.e. where `D` would not be unfolded either,
preventing "defeq abuse".

More specifically, given the "source type" (the argument) and "target type" (the expected type),
`inferInstanceAs` synthesizes an instance for the source type and then unfolds and rewraps its
components (fields, nested instances) as necessary to make them compatible with the target type. The
individual steps are represented by the following options, which all default to enabled and can be
disabled to help with porting:

* `backward.inferInstanceAs.wrap`: master switch for instance adjustment in both `inferInstanceAs`
  and the default deriving handler
* `backward.inferInstanceAs.wrap.reuseSubInstances`: reuse existing instances for the target type
  for sub-instance fields to avoid non-defeq instance diamonds
* `backward.inferInstanceAs.wrap.instances`: wrap non-reducible instances in auxiliary definitions
* `backward.inferInstanceAs.wrap.data`: wrap data fields in auxiliary definitions (proof fields are
  always wrapped)

If you just need to synthesize an instance without transporting between types, use `inferInstance`
instead, potentially with a type annotation for the expected type.
 -/
Lean.Parser.Term.inferInstanceAs : Lean.Parser.Parser
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_pow_p_pow : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} (f : Perfection M p) (m n : ℕ),
  (Perfection.coeffMonoidHom M p (m + n)) (f ^ p ^ n) = (Perfection.coeffMonoidHom M p m) f
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpNatIso_hom_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [inst_5 : F'.Monoidal] (e : F ≅ F')
  (X : CategoryTheory.AddGrp C), ((CategoryTheory.Functor.mapAddGrpNatIso e).hom.app X).hom.hom = e.hom.app X.X
-- Mathlib.CategoryTheory.Abelian.RightDerived
/-- The right derived functors of an additive functor.  -/
CategoryTheory.Functor.rightDerived : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [CategoryTheory.HasInjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              (F : CategoryTheory.Functor C D) → [F.Additive] → ℕ → CategoryTheory.Functor C D
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  (Std.ExtDTreeMap.Const.alter t k f).getKey? k =
    if (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true then some k else none
-- Mathlib.Data.Set.Lattice
Set.iUnion_congr : ∀ {α : Type u_1} {ι : Sort u_5} {s t : ι → Set α}, (∀ (i : ι), s i = t i) → ⋃ i, s i = ⋃ i, t i
-- Mathlib.Control.Traversable.Equiv
Equiv.id_map : ∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Functor t] [LawfulFunctor t] {α : Type u}
  (x : t' α), Equiv.map eqv id x = x
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_eq_rpow_pi : ∀ {ι : Type u_2} {C : ι → Type u_3} [inst : (i : ι) → PartialOrder (C i)] [inst_1 : (i : ι) → Ring (C i)]
  [inst_2 : (i : ι) → StarRing (C i)] [inst_3 : (i : ι) → TopologicalSpace (C i)]
  [inst_4 : ∀ (i : ι), StarOrderedRing (C i)] [inst_5 : StarOrderedRing ((i : ι) → C i)]
  [inst_6 : (i : ι) → Algebra ℝ (C i)] [inst_7 : ∀ (i : ι), ContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint]
  [inst_8 : ContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint] [∀ (i : ι), IsSemitopologicalRing (C i)]
  [∀ (i : ι), T2Space (C i)] [inst_11 : NonnegSpectrumClass ℝ ((i : ι) → C i)]
  [inst_12 : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)] {c : (i : ι) → C i} {x : ℝ},
  (∀ (i : ι), IsUnit (c i)) → autoParam (∀ (i : ι), 0 ≤ c i) CFC.rpow_eq_rpow_pi._auto_1 → CFC.rpow c x = c ^ x
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateLet! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.LetDecl pu → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- If the summation filter is the trivial filter `⊥`, then the topological product is equal to the
finite product (which is taken to be 1 if the multiplicative support of `f` is infinite).

Note that in this case `HasProd f a` is satisfied for *every* element `a` of the target, so the
value assigned to the `tprod` is a question of conventions.  -/
tprod_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β},
  ¬L.NeBot → ∀ (f : β → α), ∏'[L] (b : β), f b = ∏ᶠ (b : β), f b
-- Mathlib.MeasureTheory.OuterMeasure.OfAddContent
/-- Construct a measure from a sigma-subadditive content on a semiring, assuming the semiring
generates a given measurable structure. The measure is defined on this measurable structure.  -/
MeasureTheory.AddContent.measure : {α : Type u_1} →
  {C : Set (Set α)} →
    [mα : MeasurableSpace α] →
      (m : MeasureTheory.AddContent ENNReal C) →
        MeasureTheory.IsSetSemiring C →
          mα ≤ MeasurableSpace.generateFrom C → m.IsSigmaSubadditive → MeasureTheory.Measure α
-- Std.Time.Time.HourMarker
Std.Time.instReprHourMarker.repr : Std.Time.HourMarker → ℕ → Std.Format
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.instAlgebraSubtypeMemIntermediateFieldAdjoinSingletonSetGenerator : {K : Type u_1} → [inst : Field K] → {E : IntermediateField K (RatFunc K)} → Algebra ↥K⟮RatFunc.Luroth.generator E⟯ ↥E
-- Mathlib.Topology.Order.IsLUB
IsClosed.upperClosure : ∀ {α : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {s : Set α}, IsClosed s → IsClosed ↑(upperClosure s)
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.instIsScalarTower : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {A : ι → Type u_2} [inst : SMul α β] [inst_1 : (i : ι) → SMul α (A i)]
  [inst_2 : (i : ι) → SMul β (A i)] [∀ (i : ι), IsScalarTower α β (A i)], IsScalarTower α β (GradedMonoid A)
-- Init.Data.List.ToArray
List.leftpad_toArray : ∀ {α : Type u_1} (n : ℕ) (a : α) (l : List α), Array.leftpad n a l.toArray = (List.leftpad n a l).toArray
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Two affine subspaces with nonempty intersection are equal if and only if their directions are
equal.  -/
AffineSubspace.eq_iff_direction_eq_of_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : AffineSubspace k P} {p : P},
  p ∈ s₁ → p ∈ s₂ → (s₁ = s₂ ↔ s₁.direction = s₂.direction)
-- Init.Data.Slice.Array.Lemmas
Subarray.toArray_mkSlice_rcc : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = (Std.Slice.toArray xs).extract lo (hi + 1)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.zero_def : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (S : Type u) [inst_5 : CommSemiring S] [inst_6 : Algebra R S],
  PolynomialLaw.toFun' 0 S = 0
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functorMapSrc_functorObjTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMapSrc f τ)
      (CategoryTheory.SmallObject.functorObjTop f πY) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.Arrow.Hom.left τ)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.mk : {d : ℤ} → ℤ → ℤ → ℤ√d
-- Init.MetaTypes
/-- Configures how to determine definitional equality between two structure instances.
See documentation for `Lean.Meta.EtaStructMode`.
 -/
Lean.Meta.Simp.Config.etaStruct : Lean.Meta.Simp.Config → Lean.Meta.EtaStructMode
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.coe_sInf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (S : Set (NonUnitalSubalgebra R A)),
  ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.Tactic.SplitIfs
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.SplitPosition.target : Mathlib.Tactic.SplitPosition✝
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.hom.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (self : F.DescentData f) ⦃Y : C⦄ (q q_1 : Y ⟶ S) (e_q : q = q_1) ⦃i₁ i₂ : ι⦄
  (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (_hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
  (_hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q), self.hom q f₁ f₂ _hf₁ _hf₂ = self.hom q_1 f₁ f₂ ⋯ ⋯
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_apply_of_notMem_of_notMem : ∀ {X : Type u_1} [inst : MeasurableSpace X] {x y : X} (p : ↑unitInterval) {s : Set X},
  MeasurableSet s → x ∉ s → y ∉ s → (ProbabilityTheory.bernoulliMeasure x y p) s = 0
-- Mathlib.Algebra.GroupWithZero.Defs
CommMonoidWithZero.toMonoidWithZero : {M₀ : Type u_2} → [self : CommMonoidWithZero M₀] → MonoidWithZero M₀
-- Mathlib.Order.OrderIsoNat
/-- Every infinite linear order contains either a strictly increasing or a strictly decreasing
sequence indexed by `ℕ`.  -/
Infinite.exists_strictMono_or_strictAnti : ∀ (α : Type u_2) [inst : LinearOrder α] [Infinite α], ∃ f, StrictMono f ∨ StrictAnti f
-- Mathlib.Order.BooleanAlgebra.Basic
compl_comp_compl : ∀ {α : Type u} [inst : BooleanAlgebra α], compl ∘ compl = id
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of a commutative semigroup by a congruence relation is a semigroup.  -/
Con.commSemigroup : {M : Type u_4} → [inst : CommSemigroup M] → (c : Con M) → CommSemigroup c.Quotient
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileSystemWatcher.mk.injEq : ∀ (globPattern : String) (kind? : Option ℕ) (globPattern_1 : String) (kind?_1 : Option ℕ),
  ({ globPattern := globPattern, kind? := kind? } = { globPattern := globPattern_1, kind? := kind?_1 }) =
    (globPattern = globPattern_1 ∧ kind? = kind?_1)
-- Mathlib.Topology.UniformSpace.Defs
/-- A map `f : α → β` between uniform spaces is called *uniform inducing* if the uniformity filter
on `α` is the pullback of the uniformity filter on `β` under `Prod.map f f`. If `α` is a separated
space, then this implies that `f` is injective, hence it is a `IsUniformEmbedding`.  -/
IsUniformInducing : {α : Type ua} → {β : Type ub} → [UniformSpace α] → [UniformSpace β] → (α → β) → Prop
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.hom_mul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon C) [inst_3 : CategoryTheory.IsCommMonObj M.X],
  CategoryTheory.MonObj.mul.hom = CategoryTheory.MonObj.mul
-- Mathlib.Data.Finset.Sups
Finset.image_sup_product : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] (s t : Finset α),
  Finset.image (Function.uncurry fun x1 x2 => x1 ⊔ x2) (s ×ˢ t) = s ⊻ t
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.mapRingHom_single`. -/
MonoidAlgebra.mapRangeRingHom_single : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (f : R →+* S) (a : M) (b : R),
  (MonoidAlgebra.mapRingHom M f) (MonoidAlgebra.single a b) = MonoidAlgebra.single a (f b)
-- Init.Data.Int.Linear
Int.Internal.Linear.OrOver.eq_2 : ∀ (p : ℕ → Prop) (fuel_1 : ℕ),
  Int.Internal.Linear.OrOver fuel_1.succ p = (p fuel_1 ∨ Int.Internal.Linear.OrOver fuel_1 p)
-- Init.Data.String.Basic
String.Pos.Raw.isValid_asString : ∀ {l : List Char} {p : String.Pos.Raw},
  String.Pos.Raw.IsValid (String.ofList l) p ↔ ∃ i, p.byteIdx = (String.ofList (List.take i l)).utf8ByteSize
-- Mathlib.Order.CompleteLattice.Finset
Finset.iInf_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] [inst_1 : DecidableEq α] (a : α) (s : Finset α) (t : α → β),
  ⨅ x ∈ insert a s, t x = t a ⊓ ⨅ x ∈ s, t x
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.insidePart_nest : ∀ {p : DyckWord}, p.nest.insidePart = p
-- Std.Time.DateTime.WallTime
/-- Subtracts a `Week.Offset` from the given `WallTime`.
 -/
Std.Time.WallTime.subWeeks : Std.Time.WallTime → Std.Time.Week.Offset → Std.Time.WallTime
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.liminf_add_gt_of_gt : ∀ {α : Type u_3} {f : Filter α} {u v : α → EReal} {a b : EReal},
  a < Filter.liminf u f → b < Filter.liminf v f → a + b < Filter.liminf (u + v) f
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.enumOrd_zero : ∀ {s : Set Ordinal.{u}}, Ordinal.enumOrd s 0 = sInf s
-- Mathlib.Analysis.Calculus.Deriv.Support
HasCompactSupport.deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E}, HasCompactSupport f → HasCompactSupport (deriv f)
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.smul_of_nonneg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E}, T.IsPositive → ∀ {c : 𝕜}, 0 ≤ c → (c • T).IsPositive
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor_map : ∀ {V : Type u'} [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {W : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} W] [inst_3 : CategoryTheory.MonoidalCategory W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.LaxMonoidal] (D : Type u) [inst_5 : CategoryTheory.EnrichedCategory V D]
  (e :
    (v : V) →
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v))
  (h :
    ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
      (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f))
  {X Y : CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D)} (f : X ⟶ Y),
  (CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor F D e h).map f =
    CategoryTheory.ForgetEnrichment.homOf W ((e (X ⟶[V] Y)) (CategoryTheory.ForgetEnrichment.homTo V f))
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.univ_add_univ : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] [inst_2 : Fintype α],
  Finset.univ + Finset.univ = Finset.univ
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `A` itself are linearly disjoint over `F`, then it is equal to `F`.  -/
IntermediateField.LinearDisjoint.eq_bot_of_self : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E},
  A.LinearDisjoint ↥A → A = ⊥
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instZPow : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Group β] → [IsTopologicalGroup β] → Pow C(α, β) ℤ
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_eq_rpow_iff : ∀ {x y : NNReal} {z : ℝ}, z ≠ 0 → (x ^ z = y ^ z ↔ x = y)
-- Mathlib.Geometry.Euclidean.Projection
/-- Reflection is involutive.  -/
EuclideanGeometry.reflection_involutive : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection],
  Function.Involutive ⇑(EuclideanGeometry.reflection s)
-- Init.Data.Iterators.Basic
Std.PlausibleIterStep.done.eq_1 : ∀ {α : Type u} {β : Type w} {IsPlausibleStep : Std.IterStep α β → Prop} (h : IsPlausibleStep Std.IterStep.done),
  Std.PlausibleIterStep.done h = ⟨Std.IterStep.done, h⟩
-- Mathlib.Data.Finite.Prod
Set.Infinite.prod_left : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s.Infinite → t.Nonempty → (s ×ˢ t).Infinite
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.casesPatterns.sizeOf_spec : ∀ (pats : Array Aesop.CasesPattern), sizeOf (Aesop.Frontend.BuilderOption.casesPatterns pats) = 1 + sizeOf pats
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  CategoryTheory.IsMonHom M.equivMonComonUnitIsoAppXAux.hom
-- Mathlib.Data.Nat.Factorial.Basic
/-- `n.ascFactorial k = n (n + 1) ⋯ (n + k - 1)`. This is closely related to `ascPochhammer`, but
much less general.  -/
Nat.ascFactorial : ℕ → ℕ → ℕ
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.toNonUnitalStarSubalgebra_inj : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {S U : StarSubalgebra R A},
  S.toNonUnitalStarSubalgebra = U.toNonUnitalStarSubalgebra ↔ S = U
-- Mathlib.Order.Bounds.Defs
/-- A set `s` is said to be coinitial for a set `t` if, for all `a ∈ s` there exists
`b ∈ t` such that `b ≤ a`.  -/
IsCoinitialFor : {α : Type u_1} → [LE α] → Set α → Set α → Prop
-- Mathlib.Analysis.PSeries
ENNReal.tsum_schlomilch_le : ∀ {u : ℕ → ℕ} {f : ℕ → ENNReal} {C : ℕ},
  (∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) →
    (∀ (n : ℕ), 0 < u n) →
      (∀ (n : ℕ), 0 ≤ f n) →
        Monotone u →
          SuccDiffBounded C u →
            ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k) ≤ (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑' (k : ℕ), f k
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
TopCat.instIsConnectedObjSSetToSSetOfPathConnectedSpaceCarrier : ∀ {X : TopCat} [PathConnectedSpace ↑X], (TopCat.toSSet.obj X).IsConnected
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- A class describing the property of preserving effective epimorphisms.
 -/
CategoryTheory.Functor.PreservesEffectiveEpis : {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] → CategoryTheory.Functor C D → Prop
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_mul_leadingCoeff_self_inv : ∀ {K : Type u_1} [inst : DivisionRing K] (p : Polynomial K), (p * Polynomial.C p.leadingCoeff⁻¹).natDegree = p.natDegree
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.C_mul_comp : ∀ {R : Type u} {a : R} [inst : Semiring R] {p r : Polynomial R}, (Polynomial.C a * p).comp r = Polynomial.C a * p.comp r
-- Init.Prelude
/-- `` `fieldIdx `` is the node kind of projection indices like the `2` in `x.2`.  -/
Lean.fieldIdxKind : Lean.SyntaxNodeKind
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.dirac_compProd_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [MeasurableSingletonClass α] {a : α} [ProbabilityTheory.IsSFiniteKernel κ] {s : Set (α × β)},
  MeasurableSet s → ((MeasureTheory.Measure.dirac a).compProd κ) s = (κ a) (Prod.mk a ⁻¹' s)
-- Mathlib.GroupTheory.CommutingProbability
commProb_pos : ∀ (M : Type u_1) [inst : Mul M] [Finite M] [h : Nonempty M], 0 < commProb M
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- A map `incl(X) ⟶ Y` is specified by an element of `Y`'s indexing set, and then a morphism
`X ⟶ Y.obj i` in the original category.  -/
CategoryTheory.Limits.FormalCoproduct.inclHomEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      (Y : CategoryTheory.Limits.FormalCoproduct C) →
        ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ Y) ≃ (i : Y.I) × (X ⟶ Y.obj i)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_le_prod_of_subset_of_le_one' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s t : Finset ι}
  [MulLeftMono N], s ⊆ t → (∀ i ∈ t, i ∉ s → f i ≤ 1) → ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i
-- 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.NumberTheory.DirichletCharacter.Basic
/-- The Dirichlet character at level `d` through which `χ` factors  -/
DirichletCharacter.FactorsThrough.χ₀ : {R : Type u_1} →
  [inst : CommMonoidWithZero R] →
    {n : ℕ} → {χ : DirichletCharacter R n} → {d : ℕ} → χ.FactorsThrough d → DirichletCharacter R d
-- Std.Time.Format.Modifier
Std.Time.instInhabitedZoneId.default : Std.Time.ZoneId
-- Mathlib.Order.Category.BddLat
bddLat_dual_comp_forget_to_semilatInfCat : BddLat.dual.comp (CategoryTheory.forget₂ BddLat SemilatInfCat) =
  (CategoryTheory.forget₂ BddLat SemilatSupCat).comp SemilatSupCat.dual
-- Mathlib.Topology.Connected.PathConnected
IsPathConnected.exists_path_through_family : ∀ {X : Type u_1} [inst : TopologicalSpace X] {n : ℕ} {s : Set X},
  IsPathConnected s →
    ∀ (p : Fin (n + 1) → X),
      (∀ (i : Fin (n + 1)), p i ∈ s) → ∃ γ, Set.range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ Set.range ⇑γ
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefInfo.instInhabitedLocation.default : Lean.Lsp.RefInfo.Location