mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.Context.mk.inj : ∀ {level₂ level₁ : Lean.Level} {C : Q(Type level₁)} {instCat : Q(CategoryTheory.Category.{level₂, level₁} «$C»)}
  {instMonoidal? : Option Q(CategoryTheory.MonoidalCategory «$C»)} {level₂_1 level₁_1 : Lean.Level}
  {C_1 : Q(Type level₁_1)} {instCat_1 : Q(CategoryTheory.Category.{level₂_1, level₁_1} «$C_1»)}
  {instMonoidal?_1 : Option Q(CategoryTheory.MonoidalCategory «$C_1»)},
  { level₂ := level₂, level₁ := level₁, C := C, instCat := instCat, instMonoidal? := instMonoidal? } =
      { level₂ := level₂_1, level₁ := level₁_1, C := C_1, instCat := instCat_1, instMonoidal? := instMonoidal?_1 } →
    level₂ = level₂_1 ∧ level₁ = level₁_1 ∧ C = C_1 ∧ instCat = instCat_1 ∧ instMonoidal? = instMonoidal?_1
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- The canonical fan on `P : ι → Under R` given by `∀ i, P i`.  -/
CommRingCat.Under.piFan : {R : CommRingCat} → {ι : Type u} → (P : ι → CategoryTheory.Under R) → CategoryTheory.Limits.Fan P
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_erase_eq_of_not_compare_minKey!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, t.erase k ≠ ∅ → ¬cmp k t.minKey! = Ordering.eq → (t.erase k).minKey! = t.minKey!
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.smul_equiv : ∀ {R : Type r} [inst : CommRing R] (P : Fin 3 → R) {u : R}, IsUnit u → u • P ≈ P
-- Batteries.Data.Random.MersenneTwister
Batteries.Random.MersenneTwister.Config.mk : (wordSize stateSize : ℕ) →
  Fin stateSize →
    Fin wordSize →
      BitVec wordSize →
        ℕ × ℕ × ℕ × ℕ →
          BitVec wordSize × BitVec wordSize × BitVec wordSize →
            BitVec wordSize → BitVec wordSize → Batteries.Random.MersenneTwister.Config
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.whiskerOfIdCompIsoSelf_hom_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t : CategoryTheory.Bicategory.LeftLift f g),
  t.whiskerOfIdCompIsoSelf.hom.right = (CategoryTheory.Bicategory.leftUnitor t.lift).hom
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.instDecidableRelFinAdjCycleGraph : (n : ℕ) → DecidableRel (SimpleGraph.cycleGraph n).Adj
-- Mathlib.Probability.Independence.BoundedContinuousFunction
pi_indepFun_pi_of_prod_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  {F : T → Type u_5} [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)]
  [∀ (s : S), BorelSpace (E s)] [∀ (s : S), HasOuterApproxClosed (E s)] [inst_4 : (t : T) → TopologicalSpace (F t)]
  [inst_5 : (t : T) → MeasurableSpace (F t)] [∀ (t : T), BorelSpace (F t)] [∀ (t : T), HasOuterApproxClosed (F t)]
  {X : (s : S) → Ω → E s} {Y : (t : T) → Ω → F t} [inst_8 : Fintype S] [inst_9 : Fintype T]
  [MeasureTheory.IsFiniteMeasure P],
  (∀ (s : S), AEMeasurable (X s) P) →
    (∀ (t : T), AEMeasurable (Y t) P) →
      (∀ (f : (s : S) → BoundedContinuousFunction (E s) ℝ) (g : (t : T) → BoundedContinuousFunction (F t) ℝ),
          ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ∏ t, ⇑(g t) ∘ Y t) x ∂P =
            (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P) →
        ProbabilityTheory.IndepFun (fun ω s => X s ω) (fun ω t => Y t ω) P
-- Mathlib.Data.List.Permutation
List.mem_permutations' : ∀ {α : Type u_1} {s t : List α}, s ∈ t.permutations' ↔ s.Perm t
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Mon.coprime.eq_def : ∀ (x x_1 : Lean.Grind.CommRing.Mon),
  x.coprime x_1 =
    match x, x_1 with
    | Lean.Grind.CommRing.Mon.unit, x => true
    | x, Lean.Grind.CommRing.Mon.unit => true
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ =>
      match compare pw₁.x pw₂.x with
      | Ordering.eq => false
      | Ordering.lt => m₁.coprime (Lean.Grind.CommRing.Mon.mult pw₂ m₂)
      | Ordering.gt => (Lean.Grind.CommRing.Mon.mult pw₁ m₁).coprime m₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMapZero.toNNReal_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Zero X] (f : ContinuousMapZero X ℝ) (x : X),
  f.toNNReal x = (f x).toNNReal
-- Mathlib.Algebra.Lie.CartanSubalgebra
LieSubalgebra.IsCartanSubalgebra.nilpotent : ∀ {R : Type u} {L : Type v} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L} {H : LieSubalgebra R L}
  [self : H.IsCartanSubalgebra], LieRing.IsNilpotent ↥H
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
/-- This returns the multiset of irreducible factors of an associate as a `FactorSet`,
a multiset of irreducible associates `WithTop`.  -/
Associates.factors : {α : Type u_1} → [inst : CommMonoidWithZero α] → [UniqueFactorizationMonoid α] → Associates α → Associates.FactorSet α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
mulRightReflectLE_of_mulLeftReflectLE : ∀ (N : Type u_2) [inst : CommSemigroup N] [inst_1 : LE N] [MulLeftReflectLE N], MulRightReflectLE N
-- Mathlib.Topology.Connected.TotallyDisconnected
TotallyDisconnectedSpace.eq_of_continuous : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [PreconnectedSpace α]
  [TotallyDisconnectedSpace β] (f : α → β), Continuous f → ∀ (i j : α), f i = f j
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_natCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : NonAssocSemiring α] [inst_2 : StarRing α] (d : ℕ),
  (↑d).conjTranspose = ↑d
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.mem_Lp_iff_memLp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α →ₘ[μ] E}, f ∈ MeasureTheory.Lp E p μ ↔ MeasureTheory.MemLp (↑f) p μ
-- Mathlib.Data.Vector3
Fin2.insertPerm.eq_2 : ∀ (n : ℕ) (j : Fin2 n), Fin2.fz.insertPerm j.fs = j.fs
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMap.toNNReal_add_add_neg_add_neg_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] (f g : C(X, ℝ)),
  (f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal
-- Lean.Expr
_private.Lean.Expr.0.Lean.intAddFn : Lean.Expr
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidtNormed_unit_length' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] {f : ι → E}
  {n : ι}, InnerProductSpace.gramSchmidtNormed 𝕜 f n ≠ 0 → ‖InnerProductSpace.gramSchmidtNormed 𝕜 f n‖ = 1
-- Mathlib.RingTheory.RingHom.FaithfullyFlat
RingHom.FaithfullyFlat.iff_flat_and_comap_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.FaithfullyFlat ↔ f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSets.indep : ∀ {Ω : Type u_1} {m1 m2 _mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ] {p1 p2 : Set (Set Ω)},
  m1 ≤ _mΩ →
    m2 ≤ _mΩ →
      IsPiSystem p1 →
        IsPiSystem p2 →
          m1 = MeasurableSpace.generateFrom p1 →
            m2 = MeasurableSpace.generateFrom p2 → ProbabilityTheory.IndepSets p1 p2 μ → ProbabilityTheory.Indep m1 m2 μ
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.Fun.mk : {X : Type u_1} → {Y : Type u_2} → (X → Y) → TypeCat.Fun X Y
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_of_mono₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, CategoryTheory.Mono T.mor₃ → T.mor₂ = 0
-- Std.Http.Data.Request
/-- Creates a new HTTP CONNECT Request builder with the specified URI.
Typically used with `RequestTarget.authorityForm` for tunneling.
 -/
Std.Http.Request.connect : Std.Http.RequestTarget → Std.Http.Request.Builder
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.monic_integralNormalization : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → p.integralNormalization.Monic
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
strictAnti_mul_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] [ExistsAddOfLE R] [PosMulStrictMono R]
  [AddRightStrictMono R] [AddRightReflectLT R] {a : R}, a < 0 → StrictAnti fun x => a * x
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.div_subset_range : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (m : F) {s t : Set β}, s ⊆ Set.range ⇑m → t ⊆ Set.range ⇑m → s / t ⊆ Set.range ⇑m
-- Init.Data.Vector.Range
Vector.range_add : ∀ {n m : ℕ}, Vector.range (n + m) = Vector.range n ++ Vector.map (fun x => n + x) (Vector.range m)
-- Init.Grind.Config
/-- If `splitIte` is `true`, `grind` performs case-splitting on `if-then-else` expressions during the search.  -/
Lean.Grind.Config.splitIte : Lean.Grind.Config → Bool
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitesimal_def : ∀ {x : ℝ*}, x.Infinitesimal ↔ ∀ (r : ℝ), 0 < r → -↑r < x ∧ x < ↑r
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandInfo.mk : Lean.Elab.ElabInfo → Lean.Elab.CommandInfo
-- Mathlib.CategoryTheory.Filtered.Final
/-- The inclusion of an initial object is initial.  -/
CategoryTheory.Functor.initial_const_of_isInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsCofiltered C] {X : D} (hX : CategoryTheory.Limits.IsInitial X),
  ((CategoryTheory.Functor.const C).obj X).Initial
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first output of the iterator, or `none` if no such output is found.

`O(|it|)` since the iterator may skip an unknown number of times before returning a result.
Short-circuits upon encountering the first result. Only the first element of `it` is examined.

If the iterator is not productive, this function might run forever. The variant
`it.ensureTermination.first?` always terminates after finitely many steps.

Examples:
* `[7, 6].iter.first? = some 7`
* `[].iter.first? = none`
 -/
Std.Iter.first? : {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Iter β → Option β
-- Batteries.Tactic.Alias
Batteries.Tactic.Alias.AliasInfo.plain.sizeOf_spec : ∀ (n : Lean.Name), sizeOf (Batteries.Tactic.Alias.AliasInfo.plain n) = 1 + sizeOf n
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instHasOfPrecompPropertySchemeSurjective : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme),
  CategoryTheory.MorphismProperty.HasOfPrecompProperty (@AlgebraicGeometry.Surjective) P
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if `e` is in the equivalence class of `True`.  -/
Lean.Meta.Grind.isEqTrue : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.SetTheory.Ordinal.Notation
ONote.oadd.injEq : ∀ (a : ONote) (a_1 : ℕ+) (a_2 a_3 : ONote) (a_4 : ℕ+) (a_5 : ONote),
  (a.oadd a_1 a_2 = a_3.oadd a_4 a_5) = (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Ref.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} [inst_2 : SizeOf α] (gate : ℕ)
  (invert : Bool) (hgate : gate < aig.decls.size),
  sizeOf { gate := gate, invert := invert, hgate := hgate } = 1 + sizeOf gate + sizeOf invert + sizeOf hgate
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.homOfLE.congr_simp : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (e : U ≤ V), X.homOfLE e = X.homOfLE e
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.zero_rel : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (y : ↥S), (AddLocalization.r S) 0 (↑y, y)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_mul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Add M] [inst_2 : DecidableEq M]
  (x y : AddMonoidAlgebra R M) (m : M),
  (x * y).coeff m = x.coeff.sum fun m₁ r₁ => y.coeff.sum fun m₂ r₂ => if m₁ + m₂ = m then r₁ * r₂ else 0
-- Mathlib.Analysis.Complex.Norm
Complex.range_norm : (Set.range fun x => ‖x‖) = Set.Ici 0
-- Mathlib.CategoryTheory.Limits.Types.Equalizers
/-- Show that the subtype `{x : Y // g x = h x}` is an equalizer for the pair `(g,h)`.  -/
CategoryTheory.Limits.Types.equalizerLimit : {Y Z : Type u} → {g h : Y ⟶ Z} → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.parallelPair g h)
-- Mathlib.NumberTheory.Padics.Measure.Topology
/-- The weak topology on `AbstractMeasure G R E` (the weakest topology such that `μ ↦ μ f` is
continuous for all `f`).
 -/
AbstractMeasure.WeakTopology : {X : Type u_1} →
  {R : Type u_2} →
    {E : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : CommRing R] →
            [inst_3 : Module R E] →
              [inst_4 : TopologicalSpace R] → [inst_5 : IsTopologicalRing R] → TopologicalSpace (AbstractMeasure X R E)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A cone is a limit cone iff its extension by an isomorphism is.  -/
CategoryTheory.Limits.IsLimit.extendIsoEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {s : CategoryTheory.Limits.Cone F} →
            {X : C} →
              (i : X ⟶ s.pt) →
                [CategoryTheory.IsIso i] → CategoryTheory.Limits.IsLimit s ≃ CategoryTheory.Limits.IsLimit (s.extend i)
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- Given an equivalence of categories `F`, a projective presentation of `F(X)` induces a
projective presentation of `X.`  -/
CategoryTheory.Equivalence.projectivePresentationOfMapProjectivePresentation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        (F : C ≌ D) →
          (X : C) → CategoryTheory.ProjectivePresentation (F.functor.obj X) → CategoryTheory.ProjectivePresentation X
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toNonUnitalStarAlgHom_comp : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} [inst : Monoid R]
  [inst_1 : NonUnitalNonAssocSemiring A₁] [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁]
  [inst_4 : NonUnitalNonAssocSemiring A₂] [inst_5 : DistribMulAction R A₂] [inst_6 : Star A₂]
  [inst_7 : NonUnitalNonAssocSemiring A₃] [inst_8 : DistribMulAction R A₃] [inst_9 : Star A₃] (e₁ : A₁ ≃⋆ₐ[R] A₂)
  (e₂ : A₂ ≃⋆ₐ[R] A₃), e₂.toNonUnitalStarAlgHom.comp e₁.toNonUnitalStarAlgHom = (e₁.trans e₂).toNonUnitalStarAlgHom
-- Mathlib.Tactic.NormNum.Core
/-- Run each registered `norm_num` extension on an expression,
returning a `Simp.Result`.  -/
Mathlib.Meta.NormNum.eval : Lean.Expr → optParam Bool false → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.radius.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α), G.radius = ⨅ u, G.eccent u
-- Mathlib.Data.WSeq.Basic
/-- Monadic bind operator for weak sequences  -/
Stream'.WSeq.bind : {α : Type u} → {β : Type v} → Stream'.WSeq α → (α → Stream'.WSeq β) → Stream'.WSeq β
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.map_sub : ∀ {α β : Type u} (f : α → β) (x y : FreeAbelianGroup α), f <$> (x - y) = f <$> x - f <$> y
-- Mathlib.Data.Finset.Insert
/-- **Alias** of the reverse direction of `Finset.nontrivial_coe`. -/
Finset.Nontrivial.coe : ∀ {α : Type u_1} {s : Finset α}, s.Nontrivial → (↑s).Nontrivial
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove.eq_1 : ∀ {n : ℕ} (p : Fin n) (i : Fin (n + 1)), p.predAbove i = if h : p.castSucc < i then i.pred ⋯ else i.castPred ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_insertManyIfNew_impl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [inst : BEq α] [Std.LawfulBEqOrd α] [Std.TransOrd α]
  {t₁ : Std.DTreeMap.Internal.Impl α β} (h₁ : t₁.WF) {t₂ : Std.DTreeMap.Internal.Impl α β},
  (↑(t₁.insertManyIfNew t₂ ⋯)).toListModel.Perm (Std.Internal.List.insertListIfNew t₁.toListModel t₂.toListModel)
-- Mathlib.Algebra.Star.CentroidHom
/-- The canonical isomorphism from the center of a (non-associative) semiring onto its centroid.  -/
CentroidHom.starCenterIsoCentroid : {α : Type u_1} → [inst : NonAssocSemiring α] → [inst_1 : StarRing α] → ↥(StarSubsemiring.center α) ≃⋆+* CentroidHom α
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.dpow_comp : ∀ {A : Type u_3} {B : Type u_4} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  {hI : DividedPowers I} {hJ : DividedPowers J} (self : hI.DPMorphism hJ) {n : ℕ},
  ∀ a ∈ I, hJ.dpow n (self.toRingHom a) = self.toRingHom (hI.dpow n a)
-- Mathlib.Order.SuccPred.Basic
/-- Proof that `succ a` is the least element greater than `a`  -/
SuccOrder.succ_le_of_lt : ∀ {α : Type u_3} {inst : Preorder α} [self : SuccOrder α] {a b : α}, a < b → SuccOrder.succ a ≤ b
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.toAddCommMonoid.eq_1 : ∀ {M : Type u_5} [inst : AddCommMonoid M] (S : AddSubmonoid M), S.toAddCommMonoid = AddSubmonoidClass.toAddCommMonoid S
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Fold a function from left to right (in increasing order) across the tree.

```
foldl f z {1, 2, 4} = f (f (f z 1) 2) 4
```  -/
Ordnode.foldl : {α : Type u_1} → {β : Sort u_2} → (β → α → β) → β → Ordnode α → β
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.piCongrRight.eq_1 : ∀ {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} [inst : (j : η) → Add (Ms j)]
  [inst_1 : (j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j),
  AddEquiv.piCongrRight es =
    { toFun := fun x j => (es j) (x j), invFun := fun x j => (es j).symm (x j), left_inv := ⋯, right_inv := ⋯,
      map_add' := ⋯ }
-- Lean.Meta.Sym.Pattern
/-- Contains the index of the pattern variables that we must check whether its type
matches the type of the value assigned to it.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.State.tPending : Lean.Meta.Sym.UnifyM.State✝ → Array ℕ
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_insert_closure_eq_closure_insert : ∀ {α : Type u_2} (M : Matroid α) (e : α) (X : Set α), M.closure (insert e (M.closure X)) = M.closure (insert e X)
-- Mathlib.Computability.RegularExpressions
RegularExpression.zero_def : ∀ {α : Type u_1}, RegularExpression.zero = 0
-- Mathlib.Order.Lattice.Congruence
LatticeCon.inf : ∀ {α : Type u_2} [inst : Lattice α] (self : LatticeCon α) {w x y z : α},
  self.toSetoid w x → self.toSetoid y z → self.toSetoid (w ⊓ y) (x ⊓ z)
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Syntax.decodeScientificLitVal?.decodeExp : String → String.Pos.Raw → ℕ → ℕ → Option (ℕ × Bool × ℕ)
-- Mathlib.Logic.Basic
Ne.ite_ne_left_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {a b : α}, a ≠ b → ((if P then a else b) ≠ a ↔ ¬P)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.comap_mono : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (f : G →* H) {K L : FiniteIndexNormalSubgroup H},
  K ≤ L → FiniteIndexNormalSubgroup.comap f K ≤ FiniteIndexNormalSubgroup.comap f L
-- Mathlib.Tactic.Linter.Whitespace
/-- Given a `HashSet` of `Lean.Syntax.Range`s `rgs` and a further `Lean.Syntax.Range` `rg`,
`isOutside rgs rg` returns `false` if and only if `rgs` contains a range that completely contains
`rg`.

The linter uses this to figure out which nodes should be ignored.
 -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.Style.Whitespace.isOutside : Std.HashSet Lean.Syntax.Range → Lean.Syntax.Range → Bool
-- Lean.Parser.Level
Lean.Parser.levelParser.parenthesizer : optParam ℕ 0 → Lean.PrettyPrinter.Parenthesizer
-- Std.Do.Triple.Basic
/-- Observes a fact `Q` about the state by running a stateless program `obs`, then carries `Q` into the
proof of `prog`. A triple for `prog` follows from a triple for `obs` that assumes the postcondition
`Q` of the specification `h` and establishes the goal `wp⟦prog⟧ Post`. This requires `obs` to be
*stateless*: the premise `hp` states that its successful runs leave the state unchanged.
 -/
Std.Do.Triple.observe : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Std.Do.WP m ps] {α β : Type u} {obs : m α} {prog : m β}
  {Pre : Std.Do.Assertion ps} {Q : Std.Do.PostCond α ps} {Post : Std.Do.PostCond β ps},
  (∀ (C : Std.Do.Assertion ps), (Std.Do.wp obs).apply (Std.Do.PostCond.noThrow fun x => C) ⊢ₛ C) →
    ⦃Pre⦄ obs ⦃Q⦄ → ⦃Pre⦄ obs ⦃Q.imp (Std.Do.PostCond.noThrow fun x => (Std.Do.wp prog).apply Post)⦄ → ⦃Pre⦄ prog ⦃Post⦄
-- Init.Classical
Classical.not_imp : ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_def : ∀ {α : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ) (a : α) (x : γ),
  κ.rnDeriv η a x = ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- Given propositionally equal triplets `T₁` and `T₂` over `f` and `g`, the corresponding
`T₁.tensor` and `T₂.tensor` are isomorphic.  -/
AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr : {X Y S : AlgebraicGeometry.Scheme} →
  {f : X ⟶ S} →
    {g : Y ⟶ S} → {T₁ T₂ : AlgebraicGeometry.Scheme.Pullback.Triplet f g} → T₁ = T₂ → (T₁.tensor ≅ T₂.tensor)
-- Init.Data.Array.Bootstrap
_private.Init.Data.Array.Bootstrap.0.Array.foldlM.loop.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (i' : ℕ) (h_1 : Unit → motive 0) (h_2 : (i' : ℕ) → motive i'.succ),
  (match i'.succ with
    | 0 => h_1 ()
    | i'.succ => h_2 i') =
    h_2 i'
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
/-- Constructor for cocycles from `mappingCocone`.  -/
CochainComplex.mappingCocone.descCocycle : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (φ : K ⟶ L) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {M : CochainComplex C ℤ} →
              {n m : ℤ} →
                (α : CochainComplex.HomComplex.Cochain K M m) →
                  (β : CochainComplex.HomComplex.Cocycle L M n) →
                    m + 1 = n →
                      CochainComplex.HomComplex.δ m n α +
                            m.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ =
                          0 →
                        CochainComplex.HomComplex.Cocycle (CochainComplex.mappingCocone φ) M m
-- Batteries.Data.String.Lemmas
String.extract_of_valid : ∀ (l m r : List Char),
  String.Pos.Raw.extract (String.ofList (l ++ m ++ r)) { byteIdx := String.utf8Len l }
      { byteIdx := String.utf8Len l + String.utf8Len m } =
    String.ofList m
-- Mathlib.Algebra.Tropical.Basic
Tropical.instLTTropical : {R : Type u} → [LT R] → LT (Tropical R)
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.poly_eq_of_wittPolynomial_bind_eq' : ∀ (p : ℕ) {idx : Type u_1} [Fact (Nat.Prime p)] (f g : ℕ → MvPolynomial (idx × ℕ) ℤ),
  (∀ (n : ℕ), (MvPolynomial.bind₁ f) (wittPolynomial p ℤ n) = (MvPolynomial.bind₁ g) (wittPolynomial p ℤ n)) → f = g
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.mk'_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C}
  (s : X.Splitting), (CategoryTheory.SimplicialObject.Split.mk' s).s = s
-- Mathlib.Order.CompleteLattice.Basic
iInf_inf_eq : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f g : ι → α}, ⨅ x, f x ⊓ g x = (⨅ x, f x) ⊓ ⨅ x, g x