mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
CompleteLattice.MulticoequalizerDiagram.iSup_eq : ∀ {T : Type u} [inst : CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T},
  CompleteLattice.MulticoequalizerDiagram x u v → ⨆ i, u i = x
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- Constructor for isomorphisms between lax braided functors.  -/
CategoryTheory.LaxBraidedFunctor.isoOfComponents : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F G : CategoryTheory.LaxBraidedFunctor C D} →
                  (e : (X : C) → F.obj X ≅ G.obj X) →
                    autoParam
                        (∀ {X Y : C} (f : X ⟶ Y),
                          CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom =
                            CategoryTheory.CategoryStruct.comp (e X).hom (G.map f))
                        _auto_137✝ →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor)
                              (e (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom =
                            CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor)
                          _auto_139✝ →
                        autoParam
                            (∀ (X Y : C),
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y)
                                  (e (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom)
                                  (CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y))
                            _auto_141✝ →
                          (F ≅ G)
-- Mathlib.Order.Category.DistLat
DistLat.ofHom_id : ∀ {X : Type u} [inst : DistribLattice X],
  DistLat.ofHom (LatticeHom.id X) = CategoryTheory.CategoryStruct.id (DistLat.of X)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.instInhabitedAppImplicitArg.default : Lean.PrettyPrinter.Delaborator.AppImplicitArg
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.flipHom.eq_1 : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P},
  AddMonoidHom.flipHom = { toFun := AddMonoidHom.flip, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.trans_h₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ φ₃ : S₁ ⟶ S₂} (h₁₂ : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h₂₃ : CategoryTheory.ShortComplex.Homotopy φ₂ φ₃), (h₁₂.trans h₂₃).h₂ = h₁₂.h₂ + h₂₃.h₂
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
comap_nonZeroDivisors_le_of_injective : ∀ {F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [inst : MonoidWithZero M₀] [inst_1 : MonoidWithZero M₀']
  [inst_2 : FunLike F M₀ M₀'] [inst_3 : MonoidWithZeroHomClass F M₀ M₀'] {f : F},
  Function.Injective ⇑f → Submonoid.comap f (nonZeroDivisors M₀') ≤ nonZeroDivisors M₀
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- Suppose the sequence `stirlingSeq` (defined above) has the limit `a ≠ 0`.
Then the Wallis sequence `W n` has limit `a^2 / 2`.
 -/
Stirling.second_wallis_limit : ∀ (a : ℝ),
  a ≠ 0 →
    Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds a) →
      Filter.Tendsto Real.Wallis.W Filter.atTop (nhds (a ^ 2 / 2))
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- Curried `C^n` functions are `C^n` in the second coordinate.  -/
ContMDiff.curry_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {x : M},
  ContMDiff (I.prod I') J n (Function.uncurry f) → ContMDiff I' J n fun y => f x y
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.AuxGluingStruct.isom : ∀ {A : Type} [inst : MetricSpace A] (self : GromovHausdorff.AuxGluingStruct A), Isometry self.embed
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.ev_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} (f : I ⟶ J)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f]
  {X Y : CategoryTheory.Over I} (g : X ⟶ Y) {Z : CategoryTheory.Over I} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ChosenPullbacksAlong.pullback f).map
        ((CategoryTheory.ExponentiableMorphism.pushforward f).map g))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ExponentiableMorphism.ev f).app Y) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ExponentiableMorphism.ev f).app X)
      (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contSupp.eq_2 : ∀ (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.contSupp k.cons₂ =
    Turing.PartrecToTM2.trStmts₁
        (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)) ∪
      Turing.PartrecToTM2.contSupp k
-- Mathlib.Algebra.MonoidAlgebra.Support
MonoidAlgebra.of.eq_1 : ∀ (R : Type u_8) (M : Type u_9) [inst : Semiring R] [inst_1 : MulOneClass M],
  MonoidAlgebra.of R M = { toFun := (MonoidAlgebra.ofMagma R M).toFun, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.subset_toMeasurable : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α),
  s ⊆ MeasureTheory.toMeasurable μ s
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
/-- **Alias** of `Matroid.IsBase.cardinalMk_sdiff_comm`. -/
Matroid.IsBase.cardinalMk_diff_comm : ∀ {α : Type u} {M : Matroid α} {B B' : Set α} [M.InvariantCardinalRank],
  M.IsBase B → M.IsBase B' → Cardinal.mk ↑(B \ B') = Cardinal.mk ↑(B' \ B)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt64.reduceGT : Lean.Meta.Simp.Simproc
-- Std.Time.Date.Unit.Year
Std.Time.Year.instLEOffset : LE Std.Time.Year.Offset
-- Batteries.Lean.Expr
/-- Like `getRevArgD` but ignores metadata.  -/
Lean.Expr.getRevArgD' : Lean.Expr → ℕ → Lean.Expr → Lean.Expr
-- Mathlib.Data.Finsupp.Defs
/-- `Finsupp.mapRange` as an equiv.  -/
Finsupp.mapRange.equiv : {ι : Type u_3} →
  {M : Type u_4} → {N : Type u_5} → [inst : Zero M] → [inst_1 : Zero N] → (e : M ≃ N) → e 0 = 0 → (ι →₀ M) ≃ (ι →₀ N)
-- Mathlib.FieldTheory.SplittingField.Construction
/-- Embeds the splitting field into any other field that splits the polynomial.  -/
Polynomial.SplittingField.lift : {K : Type v} →
  {L : Type w} →
    [inst : Field K] →
      [inst_1 : Field L] →
        (f : Polynomial K) →
          [inst_2 : Algebra K L] → (Polynomial.map (algebraMap K L) f).Splits → f.SplittingField →ₐ[K] L
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.SplitCandidate.some : Lean.Meta.Grind.SplitInfo → ℕ → Bool → Bool → Lean.Meta.Grind.SplitCandidate✝
-- Mathlib.RingTheory.WittVector.Basic
WittVector.wittZSMul.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℤ), WittVector.wittZSMul p n = wittStructureInt p (n • MvPolynomial.X 0)
-- Mathlib.GroupTheory.Index
AddSubgroup.finite_iff_finite_and_finiteIndex : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), Finite G ↔ Finite ↥H ∧ H.FiniteIndex
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- Given an adjoint triple `F ⊣ G ⊣ H`, the left adjoint `F` is fully faithful if and only if the
right adjoint `H` is fully faithful.
 -/
CategoryTheory.Adjunction.Triple.fullyFaithfulEquiv : {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} →
          {G : CategoryTheory.Functor D C} →
            {H : CategoryTheory.Functor C D} →
              CategoryTheory.Adjunction.Triple F G H → F.FullyFaithful ≃ H.FullyFaithful
-- Mathlib.RingTheory.Ideal.Height
/-- A prime ideal of finite height is equal to any ideal that contains it with no greater height.  -/
Ideal.eq_of_le_of_height_le : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [I.IsPrime] [I.FiniteHeight] {J : Ideal R},
  I ≤ J → J.height ≤ I.height → I = J
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.fiberwise_right : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α}
  {f : α × β → E} {g : α × β → F} {l' : Filter β},
  f =Θ[l ×ˢ l'] g → ∀ᶠ (x : α) in l, (fun x_1 => f (x, x_1)) =Θ[l'] fun x_1 => g (x, x_1)
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.disjoint_supported_supported : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {s t : Set α}, Disjoint s t → Disjoint (Finsupp.supported M R s) (Finsupp.supported M R t)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.isBasis_iff_indep_encard_eq_of_finite : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  I.Finite →
    autoParam (X ⊆ M.E) Matroid.isBasis_iff_indep_encard_eq_of_finite._auto_1 →
      (M.IsBasis I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X)
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.nontriviality_proc : Lean.ParserDescr
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.eLpNorm_density_le : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν → ∀ (a : α) (s : Set β), MeasureTheory.eLpNorm (fun x => κ.density ν a x s) 1 (ν a) ≤ (ν a) Set.univ
-- Mathlib.Algebra.Group.Pi.Basic
Pi.group : {I : Type u} → {f : I → Type v₁} → [(i : I) → Group (f i)] → Group ((i : I) → f i)
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.instCompScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : AlgebraicGeometry.UniversallyOpen f]
  [hg : AlgebraicGeometry.UniversallyOpen g], AlgebraicGeometry.UniversallyOpen (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.NumberTheory.NumberField.DirichletDensity
_private.Mathlib.NumberTheory.NumberField.DirichletDensity.0.NumberField.Set.dirichletDensity.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))),
  NumberField.Set.dirichletDensity S = if h : ∃ δ, NumberField.Set.HasDirichletDensity S δ then h.choose else 0
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.if_lt : ∀ {n : ℕ} {a b f g : List.Vector ℕ n → ℕ},
  Nat.Primrec' a →
    Nat.Primrec' b → Nat.Primrec' f → Nat.Primrec' g → Nat.Primrec' fun v => if a v < b v then f v else g v
-- Mathlib.Algebra.MvPolynomial.Cardinal
/-- The cardinality of the multivariate polynomial ring, `MvPolynomial σ R` is at most the maximum
of `#R`, `#σ` and `ℵ₀`.

See `cardinalMk_le_max_lift` for the universe polymorphic version.  -/
MvPolynomial.cardinalMk_le_max : ∀ {σ R : Type u} [inst : CommSemiring R],
  Cardinal.mk (MvPolynomial σ R) ≤ max (max (Cardinal.mk R) (Cardinal.mk σ)) Cardinal.aleph0
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.instFromJsonModuleHierarchy : Lean.FromJson Lean.Lsp.Ipc.ModuleHierarchy
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- The image of one is zero.  -/
GroupSeminorm.map_one' : ∀ {G : Type u_6} [inst : Group G] (self : GroupSeminorm G), self.toFun 1 = 0
-- Mathlib.CategoryTheory.SingleObj
/-- Given a function `f : C → G` from a category to a group, we get a functor
`C ⥤ G` sending any morphism `x ⟶ y` to `f y * (f x)⁻¹`.  -/
CategoryTheory.SingleObj.differenceFunctor : {G : Type u} →
  [inst : Group G] →
    {C : Type v} →
      [inst_1 : CategoryTheory.Category.{w, v} C] → (C → G) → CategoryTheory.Functor C (CategoryTheory.SingleObj G)
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_then_not_ite'' : ∀ (c0 c1 : Bool) {a b : Bool}, (bif c0 then !bif c1 then b else !a else a) = bif c0 && c1 then !b else a
-- Mathlib.Order.Defs.Unbundled
/-- `Std.Irrefl` as a definition, suitable for use in proofs.  -/
Irreflexive : {α : Sort u_1} → (α → α → Prop) → Prop
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.Const.alter.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false}
  {hc : t.max he ∈ t}, t.get (t.max he) hc = t.max he
-- Mathlib.NumberTheory.LSeries.PrimesInAP
ArithmeticFunction.vonMangoldt.residueClass_apply_zero : ∀ {q : ℕ} (a : ZMod q), ArithmeticFunction.vonMangoldt.residueClass a 0 = 0
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.instQuasiCompactSubschemeι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), AlgebraicGeometry.QuasiCompact I.subschemeι
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.BalancedTree.mk.inj : ∀ {α : Type u} {β : α → Type v} {impl : Std.DTreeMap.Internal.Impl α β} {balanced_impl : impl.Balanced}
  {impl_1 : Std.DTreeMap.Internal.Impl α β} {balanced_impl_1 : impl_1.Balanced},
  { impl := impl, balanced_impl := balanced_impl } = { impl := impl_1, balanced_impl := balanced_impl_1 } →
    impl = impl_1
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateAddAct.mk_vadd : ∀ {α : Type u_1} {f : α → α} (n : ℕ) (x : α), { val := n } +ᵥ x = f^[n] x
-- Mathlib.Algebra.Group.Finsupp
AddEquiv.finsuppUnique.eq_1 : ∀ {M : Type u_3} [inst : AddZeroClass M] {ι : Type u_8} [inst_1 : Unique ι],
  AddEquiv.finsuppUnique = { toEquiv := Equiv.finsuppUnique, map_add' := ⋯ }
-- Mathlib.Order.CompactlyGenerated.Basic
CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup : ∀ {α : Type u} [inst : CompleteLattice α] (k : α),
  IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.disjoint_def : ∀ {M : Type u_1} [inst : MulOneClass M] {p₁ p₂ : Submonoid M}, Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
-- Mathlib.Algebra.Homology.Monoidal
/-- The tensor product of two morphisms of homological complexes.  -/
HomologicalComplex.tensorHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive] →
          [inst_4 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] →
            {I : Type u_2} →
              [inst_5 : AddMonoid I] →
                {c : ComplexShape I} →
                  [inst_6 : c.TensorSigns] →
                    [inst_7 : DecidableEq I] →
                      {K₁ K₂ L₁ L₂ : HomologicalComplex C c} →
                        (K₁ ⟶ L₁) →
                          (K₂ ⟶ L₂) →
                            [inst_8 : K₁.HasTensor K₂] → [inst_9 : L₁.HasTensor L₂] → K₁.tensorObj K₂ ⟶ L₁.tensorObj L₂
-- Mathlib.Topology.Inseparable
Topology.IsInducing.generalizingMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsInducing f → StableUnderGeneralization (Set.range f) → GeneralizingMap f
-- Init.Data.Array.Subarray
/-- Applies a monadic function to each element in a subarray in reverse order, stopping at the first
element for which the function succeeds by returning a value other than `none`. The succeeding value
is returned, or `none` if there is no success.

Example:
```lean example
#eval #["red", "green", "blue"].toSubarray.findSomeRevM? fun x => do
  IO.println x
  return Option.guard (· = 5) x.length
```
```output
blue
green
```
```output
some 5
```
 -/
Subarray.findSomeRevM? : {α : Type u} → {β : Type v} → {m : Type v → Type w} → [Monad m] → Subarray α → (α → m (Option β)) → m (Option β)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.forIn_mapWithPostcondition : ∀ {α β β₂ γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w}
  [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad o Pred EPred] [inst_8 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_10 : MonadLiftT n o] [LawfulMonadLiftT n o] [inst_12 : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_14 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β}
  {f : β → Std.Iterators.PostconditionT n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred}
  {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out).run
        g __do_lift acc ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.IterM.mapWithPostcondition f it) init g ⦃ Q; eQ ⦄
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorHom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X₁ X₂ : C}
  (f : X₁ ⟶ X₂) (Y : C),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id Y) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y
-- Std.Data.ExtTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.ExtTreeMap.entryAtIdx? : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → ℕ → Option (α × β)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.reindex_map : ∀ {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V₂] [inst_3 : Module k V] [inst_4 : Module k V₂] [inst_5 : AddTorsor V P]
  [inst_6 : AddTorsor V₂ P₂] {m n : ℕ} (s : Affine.Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) (f : P →ᵃ[k] P₂)
  (hf : Function.Injective ⇑f), (s.map f hf).reindex e = (s.reindex e).map f hf
-- Mathlib.Data.Seq.Basic
Stream'.Seq.get?_zipWith : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (s : Stream'.Seq α) (s' : Stream'.Seq β) (n : ℕ),
  (Stream'.Seq.zipWith f s s').get? n = Option.map₂ f (s.get? n) (s'.get? n)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limMap_mono : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (α : F ⟶ G) [∀ (j : J), CategoryTheory.Mono (α.app j)],
  CategoryTheory.Mono (CategoryTheory.Limits.limMap α)
-- Mathlib.AlgebraicGeometry.Limits
_private.Mathlib.AlgebraicGeometry.Limits.0.AlgebraicGeometry.isOpenImmersion_sigmaDesc_aux : ∀ {ι : Type u} (f : ι → AlgebraicGeometry.Scheme) {X : AlgebraicGeometry.Scheme} (α : (i : ι) → f i ⟶ X)
  [∀ (i : ι), AlgebraicGeometry.IsOpenImmersion (α i)],
  Pairwise (Function.onFun Disjoint fun x => Set.range ⇑(α x)) →
    AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.Sigma.desc α)
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
/-- [Stacks Tag 01S4](https://stacks.math.columbia.edu/tag/01S4) -/
AlgebraicGeometry.tfae_universallyInjective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  [AlgebraicGeometry.UniversallyInjective f,
      ∀ (K : Type u) [inst : Field K], Function.Injective fun g => CategoryTheory.CategoryStruct.comp g f,
      Function.Injective ⇑f ∧
        ∀ (x : ↥X), (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable,
      AlgebraicGeometry.Surjective (CategoryTheory.Limits.pullback.diagonal f)].TFAE
-- Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
IsPrimitiveRoot.pow_sub_one_eq_geom_sum_mul_geom_sum_inv_mul_pow_sub_one : ∀ {n i j : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [inst_1 : IsDomain A] (hζ : IsPrimitiveRoot ζ n) (hn : 2 ≤ n)
  (hi : i.Coprime n) (hj : j.Coprime n), ζ ^ j - 1 = ↑⋯.unit * ↑⋯.unit⁻¹ * (ζ ^ i - 1)
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.imp : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ φ' ψ' : L.BoundedFormula α n},
  T.Iff φ ψ → T.Iff φ' ψ' → T.Iff (φ.imp φ') (ψ.imp ψ')
-- Mathlib.Topology.Defs.Sequences
/-- A set `s` is sequentially closed if for any converging sequence `x n` of elements of `s`, the
limit belongs to `s` as well. Note that the sequential closure of a set is not guaranteed to be
sequentially closed.  -/
IsSeqClosed : {X : Type u_1} → [TopologicalSpace X] → Set X → Prop
-- Lean.Meta.Tactic.Grind.Types
/-- Returns a proof that `a = Bool.false`.
It assumes `a` and `Bool.false` are in the same equivalence class.
 -/
Lean.Meta.Grind.mkEqBoolFalseProof : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Data.Set.Order
Set.antitoneOn_iff_antitone : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  AntitoneOn f s ↔ Antitone fun a => f ↑a
-- Mathlib.RingTheory.Localization.Integral
/-- If `t` is integral in `S[1/t]`, then it is integral in `S`.  -/
IsLocalization.Away.isIntegral_of_isIntegral_map : ∀ {R : Type u_5} {S : Type u_6} {Sₘ : Type u_7} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing Sₘ]
  [inst_3 : Algebra R S] [inst_4 : Algebra S Sₘ] [inst_5 : Algebra R Sₘ] [IsScalarTower R S Sₘ] (x : S)
  [IsLocalization.Away x Sₘ], IsIntegral R ((algebraMap S Sₘ) x) → IsIntegral R x
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instIsRightAdjointPresheafOfModulesToPresheafOfModules : ∀ {X : AlgebraicGeometry.Scheme}, (AlgebraicGeometry.Scheme.Modules.toPresheafOfModules X).IsRightAdjoint
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.single_lt_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ((toDegLex fun₀ | b => 1) < toDegLex fun₀ | a => 1) ↔ a < b
-- Mathlib.Order.Filter.Pointwise
Filter.instSMulFilter.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β],
  Filter.instSMulFilter = { smul := fun a => Filter.map fun x => a • x }
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitHomIsoLimitYoneda'_hom_comp_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor Iᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)] (A : C) (i : I) {Z : Type u₂}
  (h : (CategoryTheory.yoneda.obj A).obj (F.rightOp.obj i) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π (F.rightOp.comp (CategoryTheory.yoneda.obj A)) i) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.yoneda.obj A).map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op) h