mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.lintegral_prodMkLeft : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (ca : γ × α) (g : β → ENNReal),
  ∫⁻ (b : β), g b ∂(ProbabilityTheory.Kernel.prodMkLeft γ κ) ca = ∫⁻ (b : β), g b ∂κ ca.2
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_cancelVar' : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly)
  (c : ℤ) (x : Lean.Grind.CommRing.Var) (acc : Lean.Grind.CommRing.Poly),
  c ≠ 0 →
    ↑c * Lean.Grind.CommRing.Var.denote ctx x = 1 →
      Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.cancelVar' c x p acc) =
        Lean.Grind.CommRing.Poly.denote ctx p + Lean.Grind.CommRing.Poly.denote ctx acc
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.coe_neg : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β] (f : ZeroAtInftyContinuousMap α β), ⇑(-f) = -⇑f
-- Mathlib.Algebra.Group.Units.Basic
divp_eq_divp_iff : ∀ {α : Type u} [inst : CommMonoid α] {x y : α} {ux uy : αˣ}, x /ₚ ux = y /ₚ uy ↔ x * ↑uy = y * ↑ux
-- Mathlib.RingTheory.FreeCommRing
/-- The free commutative ring on the empty type is isomorphic to `ℤ`.  -/
freeCommRingPEmptyEquivInt : FreeCommRing PEmpty.{u + 1} ≃+* ℤ
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- the condition that `r` is a retraction of `S.f`  -/
CategoryTheory.ShortComplex.Splitting.f_r : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (self : S.Splitting),
  CategoryTheory.CategoryStruct.comp S.f self.r = CategoryTheory.CategoryStruct.id S.X₁
-- Mathlib.Algebra.Group.TransferInstance
Equiv.smul.eq_1 : ∀ (M : Type u_1) {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : SMul M β],
  Equiv.smul M e = { smul := fun n x => e.invFun (n • e.toFun x) }
-- Mathlib.Topology.Algebra.Valued.WithVal
Valuation.IsEquiv.uniformContinuous_equiv_symm : ∀ {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} [hval : Valued R Γ₀'],
  Valued.v = w → w.IsEquiv v → UniformContinuous ⇑(WithVal.equiv v).symm
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.generateFrom_singleton_empty : ∀ {α : Type u_1}, MeasurableSpace.generateFrom {∅} = ⊥
-- Init.Data.List.Basic
List.and_nil : [].and = true
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
/-- A transfinite composition of shape `J` induces a transfinite composition
of shape `Set.Ici j` for any `j : J`.  -/
CategoryTheory.TransfiniteCompositionOfShape.ici : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {X Y : C} →
            {f : X ⟶ Y} →
              [inst_3 : SuccOrder J] →
                [inst_4 : WellFoundedLT J] →
                  (c : CategoryTheory.TransfiniteCompositionOfShape J f) →
                    (j : J) → CategoryTheory.TransfiniteCompositionOfShape (↑(Set.Ici j)) (c.incl.app j)
-- Init.Data.BitVec.Bitblast
/-- A `DivModState` is lawful if the remainder width `wr` plus the numerator width `wn` equals `w`,
and the bitvectors `r` and `n` have values in the bounds given by bitwidths `wr`, resp. `wn`.

This is a proof engineering choice: an alternative world could have been
`r : BitVec wr` and `n : BitVec wn`, but this required much more dependent typing coercions.

Instead, we choose to declare all involved bitvectors as length `w`, and then prove that
the values are within their respective bounds.

We start with `wn = w` and `wr = 0`, and then in each step, we decrement `wn` and increment `wr`.
In this way, we grow a legal remainder in each loop iteration.
 -/
BitVec.DivModState.Lawful : {w : ℕ} → BitVec.DivModArgs w → BitVec.DivModState w → Prop
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.instRespectsSchemeIsOpenImmersion : CategoryTheory.MorphismProperty.Respects (@AlgebraicGeometry.Flat) AlgebraicGeometry.IsOpenImmersion
-- Mathlib.Algebra.Order.Monoid.Units
Units.instPartialOrderUnits.eq_1 : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : PartialOrder α],
  Units.instPartialOrderUnits = PartialOrder.lift Units.val ⋯
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_concat : ∀ {i w : ℕ} {b : Bool} {x : BitVec w}, (x.concat b).getMsbD i = if i < w then x.getMsbD i else decide (i = w) && b
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
iInf_ne_of_notMem : ∀ {α : Type u_5} [inst : CompleteLinearOrder α] {ι : Sort u_6} [Finite ι] {f : ι → α} {a : α},
  a ≠ ⊤ → (∀ (x : ι), f x ≠ a) → iInf f ≠ a
-- Lean.Elab.BuiltinTerm
/-- Recall that `mkTermInfo` does not create an `ofTermInfo` node in the info tree
if `e` corresponds to a hole that is going to be filled "later" by executing a tactic or resuming elaboration.
This behavior is problematic for auxiliary elaboration steps that are "almost" no-ops.
For example, consider the elaborator for
```
ensure_type_of% s msg e
```
It elaborates `s`, infers its type `t`, and then elaborates `e` ensuring the resulting type is `t`.
If the elaboration of `e` is postponed, then the result is just a metavariable, and an `ofTermInfo` would not be created.
This happens because `ensure_type_of%` is almost a no-op. The elaboration of `s` does not directly contribute to the
final result, just its type.
To make sure, we don't miss any information in the `InfoTree`, we can just create a "silent" annotation to force
`mTermInfo` to create a node for the `ensure_type_of% s msg e` even if `e` has been postponed.

Another possible solution is to elaborate `ensure_type_of% s msg e` as `ensureType s e` where `ensureType` has type
```
ensureType (s e : α) := e
```
We decided to use the silent notation because `ensure_type_of%` is heavily used in the `Do` elaborator, and the extra
overhead could be significant.
 -/
_private.Lean.Elab.BuiltinTerm.0.Lean.Elab.Term.mkSilentAnnotationIfHole : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.mk.inj : ∀ {α : Type u_5} {ι : Type u_6} {idxFun : ι → Option α} {proper : ∃ i, idxFun i = none} {idxFun_1 : ι → Option α}
  {proper_1 : ∃ i, idxFun_1 i = none},
  { idxFun := idxFun, proper := proper } = { idxFun := idxFun_1, proper := proper_1 } → idxFun = idxFun_1
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.VectorsProdEqOne.zero_eq : ∀ (G : Type u_2) [inst : Group G], Equiv.Perm.vectorsProdEqOne G 0 = {List.Vector.nil}
-- Mathlib.Combinatorics.HalesJewett
/-- **Alias** of the reverse direction of `Combinatorics.Line.toSubspaceUnit_isMono`. -/
Combinatorics.Line.IsMono.toSubspaceUnit : ∀ {α : Type u_2} {ι : Type u_3} {κ : Type u_4} {l : Combinatorics.Line α ι} {C : (ι → α) → κ},
  Combinatorics.Line.IsMono C l → Combinatorics.Subspace.IsMono C l.toSubspaceUnit
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorPreCore.map_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictPseudofunctorPreCore B C) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_left : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A] [inst_4 : Add B] [AddLeftStrictMono B]
  [AddRightStrictMono B],
  Function.Injective D →
    (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
      AddMonoidAlgebra.Monic D q → AddMonoidAlgebra.leadingCoeff D (p * q) = AddMonoidAlgebra.leadingCoeff D p
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDerivWithin_of_mem_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : E → F}
  {s : Set E} {x v : E}, s ∈ nhds x → lineDerivWithin 𝕜 f s x v = lineDeriv 𝕜 f x v
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Adjunction.toCat_ofCat : ∀ {C D : CategoryTheory.Cat} {F : C ⟶ D} {G : D ⟶ C} (adj : CategoryTheory.Bicategory.Adjunction F G),
  (CategoryTheory.Adjunction.ofCat adj).toCat = adj
-- Mathlib.Tactic.FieldSimp
/-- `field_simp` normalizes an expression in a (semi-)field by rewriting it to a common denominator,
i.e. to reduce it to an expression of the form `n / d` where neither `n` nor `d` contains any
division symbol.

The `field_simp` conv tactic is a variant of the main (i.e., not conv) `field_simp` tactic. The
latter operates recursively on subexpressions, bringing *every* field-expression encountered to the
form `n / d`.

The tactic will try discharge proofs of nonzeroness of denominators, and skip steps if discharging
fails. These denominators are made out of denominators appearing in the input expression,
by repeatedly taking products or divisors. The default discharger can be non-universal, i.e. can be
specific to the field at hand (order properties, explicit `≠ 0` hypotheses, `CharZero` if that is
known, etc). See `field_simp_discharge` for full details of the default discharger algorithm.

* `field_simp (disch := tac)` uses the tactic sequence `tac` to discharge nonzeroness/positivity
  proofs.
* `field_simp [t₁, ..., tₙ]` provides terms `t₁`, ..., `tₙ` to the discharger for
  nonzeroness/positivity proofs.

Examples:

```
-- `x / (1 - y) / (1 + y / (1 - y))` is reduced to `x / (1 - y + y)`:
example (x y z : ℚ) (hy : 1 - y ≠ 0) :
    ⌊x / (1 - y) / (1 + y / (1 - y))⌋ < 3 := by
  conv => enter [1, 1]; field_simp
  -- new goal: `⊢ ⌊x / (1 - y + y)⌋ < 3`
```
 -/
Mathlib.Tactic.FieldSimp.convField_simp__ : Lean.ParserDescr
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatIso.isIso_of_toNatTrans_isIso : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} (α : F ⟶ G)
  [CategoryTheory.IsIso α.toNatTrans], CategoryTheory.IsIso α
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- **Alias** of `CategoryTheory.Functor.ReflectsEpimorphisms.iso_iff`. -/
CategoryTheory.Functor.reflectsEpimorphisms.iso_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G), F.ReflectsEpimorphisms ↔ G.ReflectsEpimorphisms
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.instDiscreteTopology : ∀ {M : Type u_1} [inst : TopologicalSpace M] [DiscreteTopology M], DiscreteTopology Mᵃᵒᵖ
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.isScalarTower : ∀ {R : Type u_1} {R' : Type u_2} {E : Type u_3} [inst : AddGroup E] [inst_1 : SMul R ℝ] [inst_2 : SMul R NNReal]
  [inst_3 : IsScalarTower R NNReal ℝ] [inst_4 : SMul R' ℝ] [inst_5 : SMul R' NNReal]
  [inst_6 : IsScalarTower R' NNReal ℝ] [inst_7 : SMul R R'] [IsScalarTower R R' ℝ],
  IsScalarTower R R' (AddGroupSeminorm E)
-- Mathlib.Topology.Algebra.Valued.ValuedField
_private.Mathlib.Topology.Algebra.Valued.ValuedField.0.Valued.termHat : Lean.ParserDescr
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.autToPow_spec : ∀ (R : Type u_4) {S : Type u_5} [inst : CommRing S] [inst_1 : IsDomain S] {μ : S} {n : ℕ} (hμ : IsPrimitiveRoot μ n)
  [inst_2 : CommRing R] [inst_3 : Algebra R S] [inst_4 : NeZero n] (f : S ≃ₐ[R] S),
  μ ^ (↑((IsPrimitiveRoot.autToPow R hμ) f)).val = f μ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.instIsMultiplicativeFunctorCoequifibered : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C], CategoryTheory.NatTrans.Coequifibered.IsMultiplicative
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Lawfulness of `tensorHom`.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom_eq : ∀ {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} {D : Type u₃}
  {inst_4 : CategoryTheory.Category.{v₃, u₃} D}
  [self : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D]
  {d₁ d₂ d₁' d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂'),
  (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map
      (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom f f') =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObjIsoConvolution C V
          d₁ d₁').hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.DayConvolution.map
          ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map f)
          ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).map f'))
        (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObjIsoConvolution C
            V d₂ d₂').inv)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedStep.default : Lean.Meta.Simp.Step
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_diff_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑m₁).isEmpty = true → (↑(m₁.diff m₂)).isEmpty = true
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.nhdsWithin_basis_closedEBall`. -/
EMetric.nhdsWithin_basis_closed_eball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α},
  (nhdsWithin x s).HasBasis (fun ε => 0 < ε) fun ε => Metric.closedEBall x ε ∩ s
-- Mathlib.Data.Finset.Dedup
Finset.dedup_eq_self : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s.val.dedup = s.val
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_restrict : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), (π.restrict J).iUnion = ↑J ∩ π.iUnion
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.conj_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E) {T : E →L[𝕜] E},
  T.IsPositive → ∀ [inst_3 : U.HasOrthogonalProjection], (U.starProjection ∘SL T ∘SL U.starProjection).IsPositive
-- Mathlib.Algebra.Group.Subgroup.Map
AddMonoidHom.addSubgroupMap.eq_1 : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (f : G →+ G') (H : AddSubgroup G),
  f.addSubgroupMap H = f.addSubmonoidMap H.toAddSubmonoid
-- Mathlib.Order.Filter.Pointwise
/-- `a • f` is the map of `f` under `a •` in scope `Pointwise`.  -/
Filter.instSMulFilter : {α : Type u_2} → {β : Type u_3} → [SMul α β] → SMul α (Filter β)
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.ofIsTopCompl.eq_1 : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} {F : Type u_3} [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : TopologicalSpace F] [inst_6 : AddCommGroup F]
  [inst_7 : Module R F] [inst_8 : ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F)
  (ψ : ↥q →L[R] F), ContinuousLinearMap.ofIsTopCompl h φ ψ = φ.coprod ψ ∘SL ↑(p.prodEquivOfIsTopCompl q h).symm
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instMonoid : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [Monoid M] → Monoid (l.Germ M)
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.setIntegral_densityProcess_of_le : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] {n m : ℕ},
      n ≤ m →
        ∀ (a : α) {s : Set β},
          MeasurableSet s →
            ∀ {A : Set γ}, MeasurableSet A → ∫ (x : γ) in A, κ.densityProcess ν m a x s ∂ν a = (κ a).real (A ×ˢ s)
-- Mathlib.Algebra.Category.Grp.Basic
/-- Turn a morphism in `GrpCat` back into a `MonoidHom`.  -/
GrpCat.Hom.hom : {X Y : GrpCat} → X.Hom Y → ↑X →* ↑Y
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqResult : DecidableEq Std.Tactic.BVDecide.LRAT.Internal.Result
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- `X` is the colimit of its affine opens. See `isColimit_cocone` below.  -/
AlgebraicGeometry.Scheme.AffineZariskiSite.cocone : (X : AlgebraicGeometry.Scheme) →
  CategoryTheory.Limits.Cocone
    ((AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).comp
      ((CategoryTheory.Functor.rightOp X.presheaf).comp AlgebraicGeometry.Scheme.Spec))
-- Init.Data.List.FinRange
Fin.foldlM_eq_foldlM_finRange : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] (f : α → Fin n → m α) (x : α),
  Fin.foldlM n f x = List.foldlM f x (List.finRange n)
-- Mathlib.Algebra.GroupWithZero.Basic
/-- **Alias** of `pow_ne_zero`. -/
IsReduced.pow_ne_zero : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → a ^ n ≠ 0
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.toList_replace : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α} {b : β a},
  (Std.DHashMap.Internal.AssocList.replace a b l).toList = Std.Internal.List.replaceEntry a b l.toList
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory_associator_hom_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {a b c d : CategoryTheory.Bicategory.InducedBicategory C F} (x : a ⟶ b) (y : b ⟶ c) (z : c ⟶ d),
  (CategoryTheory.Bicategory.associator x y z).hom.hom = (CategoryTheory.Bicategory.associator x.hom y.hom z.hom).hom
-- Mathlib.Data.Finset.Erase
Finset.erase_subset : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), s.erase a ⊆ s
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- Variant of `NNReal.rpow_add'` that avoids having to prove `y + z = w` twice.  -/
NNReal.rpow_of_add_eq : ∀ {w y z : ℝ} (x : NNReal), w ≠ 0 → y + z = w → x ^ w = x ^ y * x ^ z
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.op_L₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.op.L₁ = S.L₂.op
-- Mathlib.CategoryTheory.Monoidal.Rigid.Braided
/-- If `C` is a braided and right rigid category, then it is a rigid category.
Not registered as an instance as this is not canonical enough.  -/
CategoryTheory.BraidedCategory.rigidCategoryOfRightRigidCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → [CategoryTheory.RightRigidCategory C] → CategoryTheory.RigidCategory C
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
/-- `PowerSeries.pentagonalSeries` as an infinite sum over integers  -/
PowerSeries.WithPiTopology.hasSum_pentagonalSeries : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R],
  HasSum (fun k => ↑↑k.negOnePow * PowerSeries.X ^ pentagonal k) (PowerSeries.pentagonalSeries R)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.graph_map_fst_eq_domain : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F),
  Submodule.map (LinearMap.fst R E F) f.graph = f.domain
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∈ t₂ → (t₁ ∩ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.Algebra.Module.Congruence.Defs
VAddCon.Quotient.eq_1 : ∀ {S : Type u_2} (M : Type u_3) [inst : VAdd S M] (c : VAddCon S M), VAddCon.Quotient M c = Quotient c.toSetoid
-- Lean.Elab.Binders
/-- Convert `stx` into an array of `BinderView`s.
`stx` must be an identifier, `_`, `explicitBinder`, `implicitBinder`, `strictImplicitBinder`, or `instBinder`.
 -/
_private.Lean.Elab.Binders.0.Lean.Elab.Term.toBinderViews : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Elab.Term.BinderView)
-- Mathlib.Topology.MetricSpace.Basic
MetricSpace.replaceDist_eq : ∀ {X : Type u_2} (m : MetricSpace X) (d : X → X → ℝ) (hd : d = dist), m.replaceDist d hd = m
-- Mathlib.Topology.MetricSpace.IsometricSMul
nndist_div_right : ∀ {M : Type u} [inst : DivInvMonoid M] [inst_1 : PseudoMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] (a b c : M),
  nndist (a / c) (b / c) = nndist a b
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeExtension.mapValueGroupWithZero_strictMono : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B] [inst_5 : ValuativeExtension A B],
  StrictMono ⇑(ValuativeExtension.mapValueGroupWithZero A B)
-- Mathlib.Algebra.Order.Hom.Basic
RingSeminormClass.toNonnegHomClass : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : NonUnitalNonAssocRing α]
  [inst_2 : Semiring β] [inst_3 : LinearOrder β] [IsOrderedAddMonoid β] [RingSeminormClass F α β], NonnegHomClass F α β
-- Mathlib.Data.Set.Lattice.Image
Set.surjOn_sUnion : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {T : Set (Set β)} {f : α → β},
  (∀ t ∈ T, Set.SurjOn f s t) → Set.SurjOn f s (⋃₀ T)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.instIsScalarTower : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  IsScalarTower R (MvPolynomial σ R) (MvPolynomial σ S)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add_subset_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t u : Finset α}, s + t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x + y ∈ u
-- Mathlib.Algebra.Homology.QuasiIso
HomologicalComplex.instHasTwoOutOfThreePropertyQuasiIso : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.CategoryWithHomology C], (HomologicalComplex.quasiIso C c).HasTwoOutOfThreeProperty
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.State : Type
-- Init.Grind.Util
Lean.Grind.markerUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_lt_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀},
  0 < b → (a / b < 1 ↔ a < b)