mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mergeWith.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α]
  (mergeFn mergeFn_1 : (a : α) → β a → β a → β a),
  mergeFn = mergeFn_1 →
    ∀ (t₁ t₁_1 : Std.DTreeMap.Internal.Impl α β) (e_t₁ : t₁ = t₁_1) (t₂ t₂_1 : Std.DTreeMap.Internal.Impl α β),
      t₂ = t₂_1 →
        ∀ (ht₁ : t₁.Balanced),
          Std.DTreeMap.Internal.Impl.mergeWith mergeFn t₁ t₂ ht₁ =
            Std.DTreeMap.Internal.Impl.mergeWith mergeFn_1 t₁_1 t₂_1 ⋯
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_eq_singleton_iff : ∀ {k n : ℕ}, (*...n).toArray = #[k] ↔ n = 1 ∧ 0 = k
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_symm_toLinearEquiv : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ⇑e.symm = ⇑e.symm
-- Mathlib.Tactic.NormNum.BigOperators
/-- The set is empty.  -/
Mathlib.Meta.Finset.ProveEmptyOrConsResult.empty : {u : Lean.Level} → {α : Q(Type u)} → {s : Q(Finset «$α»)} → Q(«$s» = ∅) → Mathlib.Meta.Finset.ProveEmptyOrConsResult s
-- Mathlib.CategoryTheory.Limits.Types.Limits
/-- The equivalence between a limiting cone of `F` in `Type u` and the "concrete" definition as the
sections of `F`.  -/
CategoryTheory.Limits.Types.isLimitEquivSections : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    {F : CategoryTheory.Functor J (Type u)} →
      {c : CategoryTheory.Limits.Cone F} → CategoryTheory.Limits.IsLimit c → c.pt ≃ ↑F.sections
-- Mathlib.AlgebraicGeometry.AffineSpace
/-- `𝔸(n; S)` is the affine `n`-space over `S`.  -/
AlgebraicGeometry.«term𝔸(_;_)» : Lean.ParserDescr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.keysArray.size = t.size
-- Lean.Meta.Tactic.Cases
Lean.Meta.generalizeTargetsEq : Lean.MVarId → Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.MVarId
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Queue : Type
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.TwoPowShiftTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {w n : ℕ} {lhs : aig.RefVec w}
  {rhs : aig.RefVec n} {pow n_1 : ℕ} {lhs_1 : aig.RefVec w} {rhs_1 : aig.RefVec n_1} {pow_1 : ℕ},
  { n := n, lhs := lhs, rhs := rhs, pow := pow } = { n := n_1, lhs := lhs_1, rhs := rhs_1, pow := pow_1 } →
    n = n_1 ∧ lhs = lhs_1 ∧ rhs ≍ rhs_1 ∧ pow = pow_1
-- Mathlib.RepresentationTheory.Rep.Iso
/-- Functorially convert a representation of `G` into a module over `k[G]`.  -/
Rep.toModuleMonoidAlgebra : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Monoid G] → CategoryTheory.Functor (Rep.{w, u, v} k G) (ModuleCat (MonoidAlgebra k G))
-- Aesop.Script.TacticState
Aesop.Script.TacticState.eraseSolvedGoals : Aesop.Script.TacticState → Lean.MetavarContext → Lean.MetavarContext → Aesop.Script.TacticState
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → ∀ (s : R), p.scaleRoots s ≠ 0
-- Mathlib.Data.Sum.Interval
_private.Mathlib.Data.Sum.Interval.0.Finset.sumLift₂.match_1.eq_3 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (motive : α₁ ⊕ α₂ → β₁ ⊕ β₂ → Sort u_5) (val : α₂)
  (val_1 : β₁) (h_1 : (a : α₁) → (b : β₁) → motive (Sum.inl a) (Sum.inl b))
  (h_2 : (val : α₁) → (val_2 : β₂) → motive (Sum.inl val) (Sum.inr val_2))
  (h_3 : (val : α₂) → (val_2 : β₁) → motive (Sum.inr val) (Sum.inl val_2))
  (h_4 : (a : α₂) → (b : β₂) → motive (Sum.inr a) (Sum.inr b)),
  (match Sum.inr val, Sum.inl val_1 with
    | Sum.inl a, Sum.inl b => h_1 a b
    | Sum.inl val, Sum.inr val_2 => h_2 val val_2
    | Sum.inr val, Sum.inl val_2 => h_3 val val_2
    | Sum.inr a, Sum.inr b => h_4 a b) =
    h_3 val val_1
-- Lean.Meta.Basic
Lean.Meta.instInhabitedAbstractMVarsResult.default : Lean.Meta.AbstractMVarsResult
-- Mathlib.Data.Nat.Digits.Lemmas
/-- **Alias** of `Nat.le_length_digits_le`. -/
Nat.le_digits_len_le : ∀ (b n m : ℕ), n ≤ m → (b.digits n).length ≤ (b.digits m).length
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the largest key in the tree map, returning `fallback` if the tree map is empty.
 -/
Std.ExtTreeMap.maxKeyD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → α
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.GradesBy.decompose_single : ∀ {M : Type u_1} {ι : Type u_2} {R : Type u_3} [inst : AddMonoid M] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : CommSemiring R] (f : M →+ ι) (m : M) (r : R),
  (DirectSum.decompose (AddMonoidAlgebra.gradeBy R ⇑f)) (AddMonoidAlgebra.single m r) =
    (DirectSum.of (fun i => ↥(AddMonoidAlgebra.gradeBy R (⇑f) i)) (f m)) ⟨AddMonoidAlgebra.single m r, ⋯⟩
-- Mathlib.Order.CompleteLattice.Basic
sSup_eq_iSup' : ∀ {α : Type u_1} [inst : SupSet α] (s : Set α), sSup s = ⨆ a, ↑a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_eq_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a : α}, m.contains a = (m.getKey? a).isSome
-- Mathlib.Data.Setoid.Partition
/-- A collection `c : Set (Set α)` of sets is a partition of `α` into pairwise
disjoint sets if `∅ ∉ c` and each element `a : α` belongs to a unique set `b ∈ c`.  -/
Setoid.IsPartition : {α : Type u_1} → Set (Set α) → Prop
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.nnrealPart_coeFn_eq : ∀ {α : Type u} [inst : TopologicalSpace α] (f : BoundedContinuousFunction α ℝ), ⇑f.nnrealPart = Real.toNNReal ∘ ⇑f
-- Mathlib.Algebra.Tropical.Basic
Tropical.instMonoidTropical : {R : Type u} → [AddMonoid R] → Monoid (Tropical R)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarSpaceCoord_target' : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.mixedEmbedding.polarSpaceCoord K).target =
    (Set.univ.pi fun w => if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x => Set.Ioo (-Real.pi) Real.pi
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Restrict an open partial homeomorphism to the subsets of the source and target
that consist of points `x ∈ f.source`, `y = f x ∈ f.target`
such that `f` is `C^n` at `x` and `f.symm` is `C^n` at `y`.

Note that `n` is a natural number or `ω`, but not `∞`,
because the set of points of `C^∞`-smoothness of `f` is not guaranteed to be open.  -/
OpenPartialHomeomorph.restrContDiff : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type uE} →
      [inst_1 : NormedAddCommGroup E] →
        [NormedSpace 𝕜 E] →
          {F : Type uF} →
            [inst_3 : NormedAddCommGroup F] →
              [NormedSpace 𝕜 F] → OpenPartialHomeomorph E F → (n : WithTop ℕ∞) → n ≠ ↑⊤ → OpenPartialHomeomorph E F
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.baseChange_addX : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Jacobian R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P Q : Fin 3 → A), (W'.baseChange B).addX (⇑f ∘ P) (⇑f ∘ Q) = f ((W'.baseChange A).addX P Q)
-- Mathlib.Topology.ClusterPt
clusterPt_iff_nonempty : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X},
  ClusterPt x F ↔ ∀ ⦃U : Set X⦄, U ∈ nhds x → ∀ ⦃V : Set X⦄, V ∈ F → (U ∩ V).Nonempty
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Int.comap_cast_atBot : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R],
  Filter.comap Int.cast Filter.atBot = Filter.atBot
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.conesEquiv_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E),
  (CategoryTheory.Functor.Initial.conesEquiv F G).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun c =>
        CategoryTheory.Limits.Cone.ext
          (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone (F.comp G))).obj c).pt) ⋯)
      ⋯
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.comap_map_eq_self_of_injective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N},
  Function.Injective ⇑f → ∀ (H : Subgroup G), Subgroup.comap f (Subgroup.map f H) = H
-- Mathlib.Order.Disjoint
symm_disjoint : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α], Std.Symm Disjoint
-- Mathlib.Order.Interval.Set.Fin
Fin.image_val_uIoc : ∀ {n : ℕ} (i j : Fin n), Fin.val '' Set.uIoc i j = Set.uIoc ↑i ↑j
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.NatStruct : Type
-- Mathlib.Order.Fin.Basic
Fin.revOrderIso_apply : ∀ {n : ℕ} (a : (Fin n)ᵒᵈ), Fin.revOrderIso a = (OrderDual.ofDual a).rev
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_apply_of_countable : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [Countable ι] (f : ι → MeasureTheory.Measure α) (s : Set α),
  (MeasureTheory.Measure.sum f) s = ∑' (i : ι), (f i) s
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.toOpposite_apply : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (a : A),
  (AlgEquiv.toOpposite R A) a = MulOpposite.op a
-- Mathlib.Order.RelClasses
/-- Set notation form of `LE.le.eq_of_not_lt'` -/
LE.le.eq_of_not_ssubset' : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, b ⊆ a → ¬b ⊂ a → a = b
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.LinearWeights.map_lie : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  {inst_3 : AddCommGroup M} {inst_4 : Module R M} {inst_5 : LieRingModule L M} {inst_6 : LieModule R L M}
  {inst_7 : LieRing.IsNilpotent L} [self : LieModule.LinearWeights R L M] (χ : L → R),
  LieModule.genWeightSpace M χ ≠ ⊥ → ∀ (x y : L), χ ⁅x, y⁆ = 0
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
/-- The Grothendieck group is a group.  -/
Algebra.GrothendieckGroup.instCommGroup : {M : Type u_1} → [inst : CommMonoid M] → CommGroup (Algebra.GrothendieckGroup M)
-- Lean.Meta.Basic
/-- Resulting type for `abstractMVars`  -/
Lean.Meta.AbstractMVarsResult : Type
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.algebraMap_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] (ρ : Representation A G V) (a : A), (algebraMap A (ρ.IntertwiningMap ρ)) a = a • 1
-- Mathlib.Algebra.Algebra.Hom
/-- Reinterpret a `RingHom` as a `ℤ`-algebra homomorphism.  -/
RingHom.toIntAlgHom : {R : Type u_1} → {S : Type u_2} → [inst : Ring R] → [inst_1 : Ring S] → (R →+* S) → R →ₐ[ℤ] S
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.setLIntegral_tilted : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (f : α → ℝ)
  (g : α → ENNReal) (s : Set α),
  ∫⁻ (x : α) in s, g x ∂μ.tilted f =
    ∫⁻ (x : α) in s, ENNReal.ofReal (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) * g x ∂μ
-- Lean.Meta.Tactic.LibrarySearch
Lean.Meta.LibrarySearch.instOrdDeclMod : Ord Lean.Meta.LibrarySearch.DeclMod
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∉ t₁ → (t₁ ∪ t₂).getD k fallback = t₂.getD k fallback
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.sub : Int.Internal.Linear.Expr → Int.Internal.Linear.Expr → Int.Internal.Linear.Expr
-- Init.Data.String.Defs
String.Pos.Raw.isValid_iff_isValidUTF8_extract_zero : ∀ {s : String} {p : String.Pos.Raw},
  String.Pos.Raw.IsValid s p ↔ p ≤ s.rawEndPos ∧ (s.toByteArray.extract 0 p.byteIdx).IsValidUTF8
-- Mathlib.Topology.DiscreteSubset
Set.Finite.compl_mem_codiscrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {S : Set X}, S.Finite → Sᶜ ∈ Filter.codiscrete X
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
/-- A category is finitely accessible if it is `ℵ₀`-accessible.  -/
CategoryTheory.IsFinitelyAccessibleCategory : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.eq_succMany?_of_toArray_eq_append_append : ∀ {α : Type u} {r : Std.Rci α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxi.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff),
  cur = (Std.PRange.succMany? pref.size r.lower).get ⋯
-- Init.System.Uri
System.Uri.UriEscape.letterf : UInt8
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.trans_snd : ∀ {X Y : TopPair} {f₀ f₁ f₂ : X ⟶ Y} (F : TopPair.Homotopy f₀ f₁) (G : TopPair.Homotopy f₁ f₂),
  (F.trans G).snd = F.snd.trans G.snd
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m')
  (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 g)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
        (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm'))
      h
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp : ∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  {p : ENNReal} [inst_3 : BorelSpace E] {f : β → E} [hp : Fact (1 ≤ p)],
  p ≠ ⊤ →
    ∀ {μ : MeasureTheory.Measure β} (fmeas : Measurable f)
      [inst_4 : TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})] (hf : MeasureTheory.MemLp f p μ),
      Filter.Tendsto
        (fun n => MeasureTheory.MemLp.toLp ⇑(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) ⋯)
        Filter.atTop (nhds (MeasureTheory.MemLp.toLp f hf))
-- Mathlib.Data.Multiset.ZeroCons
Multiset.mem_cons : ∀ {α : Type u_1} {a b : α} {s : Multiset α}, a ∈ b ::ₘ s ↔ a = b ∨ a ∈ s
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.foldM_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w}
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n]
  [inst_5 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Monad o]
  [inst_9 : Std.Internal.Do.Assertion Pred] [inst_10 : Std.Internal.Do.Assertion EPred]
  [inst_11 : Std.Internal.Do.WPMonad o Pred EPred] [inst_12 : Std.IteratorLoop α m n] [inst_13 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o] [inst_16 : MonadLiftT m n] [inst_17 : MonadLiftT n o]
  [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → n γ} {g : δ → γ → o δ} {init : δ} {it : Std.IterM m β}
  {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.foldM
        (fun d b => do
          let c ← liftM (f b)
          g d c)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.IterM.mapM f it) ⦃ Q; eQ ⦄
-- Mathlib.SetTheory.Ordinal.Basic
/-- **Alias** of `Ordinal.type_ulift`. -/
Ordinal.type_uLift : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r],
  Ordinal.type (ULift.down ⁻¹'o r) = Ordinal.lift.{v, u} (Ordinal.type r)
-- Std.Internal.Do.Triple.SpecLemmas
/-- The type of loop invariants used by the specifications of `for ... in ...` loops.
A loop invariant maps the iteration cursor and accumulator state to an assertion.
The exception postcondition is specified separately as the spec's `epost` parameter.  -/
Std.Internal.Do.Invariant : {α : Type u₁} → List α → Type u₂ → Type (max u₁ u₂) → Type (max u₁ u₂)
-- Mathlib.Algebra.Group.Even
Even.eq_1 : ∀ {α : Type u_2} [inst : Add α] (a : α), Even a = ∃ r, a = r + r
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.Nat.div_add_eq_left_of_lt : ∀ {x y z : ℕ}, z ∣ x → y < z → 0 < z → (x + y) / z = x / z
-- Mathlib.RingTheory.Grassmannian
/-- The surjective `B`-linear map `B ⊗[R] M → B ⊗[A] ((A ⊗[R] M) ⧸ N)` obtained as the base change
of `N.mkQ` along `A → B`  -/
Module.Grassmannian.baseChangeMkQ : {R : Type u} →
  [inst : CommRing R] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {A : Type w} →
            [inst_3 : CommRing A] →
              [inst_4 : Algebra R A] →
                (B : Type w) →
                  [inst_5 : CommRing B] →
                    [inst_6 : Algebra R B] →
                      [inst_7 : Algebra A B] →
                        [IsScalarTower R A B] →
                          (N : Submodule A (TensorProduct R A M)) →
                            TensorProduct R B M →ₗ[B] TensorProduct A B (TensorProduct R A M ⧸ N)
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.instIterator : {α : Type u_1} → {β : Type u_2} → Std.Iterator (Lean.PersistentHashMap.Zipper α β) Id (α × β)
-- Mathlib.Algebra.Star.Subalgebra
/-- Range of a `StarAlgHom` as a star subalgebra.  -/
StarAlgHom.range : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R A] →
              [inst_4 : StarRing A] →
                [inst_5 : Semiring B] →
                  [inst_6 : Algebra R B] →
                    [inst_7 : StarRing B] → [inst_8 : StarModule R B] → (A →⋆ₐ[R] B) → StarSubalgebra R B
-- Init.Data.Vector.Count
Vector.countP_singleton : ∀ {α : Type u_1} {p : α → Bool} {a : α}, Vector.countP p #v[a] = if p a = true then 1 else 0
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.toCircle_zero : ∀ {T : ℝ}, AddCircle.toCircle 0 = 1
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.smul_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_3 : Semiring R] [inst_4 : CategoryTheory.Linear R C]
  [inst_5 : ∀ (n : ℤ), CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor C n)] (n : R) (f : T₁ ⟶ T₂),
  (n • f).hom₂ = n • f.hom₂
-- Mathlib.Data.Set.Lattice.Image
Set.mapsTo_iInter₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_8} {s : Set α} {t : (i : ι) → κ i → Set β} {f : α → β},
  Set.MapsTo f s (⋂ i, ⋂ j, t i j) ↔ ∀ (i : ι) (j : κ i), Set.MapsTo f s (t i j)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.coneOfHasLimitCurryCompLim.eq_1 : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)],
  CategoryTheory.Limits.coneOfHasLimitCurryCompLim G =
    { pt := CategoryTheory.Limits.limit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim),
      π :=
        {
          app := fun x =>
            CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) x.1)
              (((CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits (CategoryTheory.Functor.curry.obj G)).obj x.1).π.app
                x.2),
          naturality := ⋯ } }
-- Mathlib.Topology.DenseEmbedding
/-- If the domain of a `IsDenseInducing` map is a separable space, then so is the codomain.  -/
IsDenseInducing.separableSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [TopologicalSpace.SeparableSpace α], IsDenseInducing i → TopologicalSpace.SeparableSpace β
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.comp_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {φ' : S₂ ⟶ S₃} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  {h₃ : S₃.HomologyData} (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
  (ψ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₂ h₃), (ψ.comp ψ').left = ψ.left.comp ψ'.left
-- Mathlib.Probability.Martingale.BorelCantelli
/-- `leastGE f r` is the stopping time corresponding to the first time `f ≥ r`.  -/
MeasureTheory.leastGE : {ι : Type u_1} →
  {Ω : Type u_2} →
    {β : Type u_3} → [inst : Preorder ι] → [OrderBot ι] → [InfSet ι] → [Preorder β] → (ι → Ω → β) → β → Ω → WithTop ι
-- Init.Data.Array.Lemmas
Array.foldr_induction : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} (motive : ℕ → β → Prop) {init : β},
  motive as.size init →
    ∀ {f : α → β → β},
      (∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)) → motive 0 (Array.foldr f init as)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.coroot_coweightMap_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (i : ι₂) (f : P.Hom Q),
  f.coweightMap (Q.coroot i) = P.coroot (f.indexEquiv.symm i)
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.app_p_comm_assoc : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C]
  {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J) {Z : C}
  (h : Q.X.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.p.app X) (CategoryTheory.CategoryStruct.comp (f.f.app X) h) =
    CategoryTheory.CategoryStruct.comp (f.f.app X) (CategoryTheory.CategoryStruct.comp (Q.p.app X) h)
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.instIsCentralScalar : ∀ (R : Type u) (X : Type v) [inst : CommRing R] {S : Type u_1} [inst_1 : Monoid S] [inst_2 : DistribMulAction S R]
  [inst_3 : DistribMulAction Sᵐᵒᵖ R] [inst_4 : IsScalarTower S R R] [inst_5 : IsCentralScalar S R],
  IsCentralScalar S (FreeLieAlgebra R X)