mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.instPartialOrder : {R : Type u_2} →
  {E : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] →
            [inst_4 : TopologicalSpace E] → [inst_5 : Module R E] → PartialOrder (ProperCone R E)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₁.id.injEq : ∀ (e : Lean.Expr) (a : Mathlib.Tactic.BicategoryLike.Obj) (e_1 : Lean.Expr) (a_1 : Mathlib.Tactic.BicategoryLike.Obj),
  (Mathlib.Tactic.BicategoryLike.Mor₁.id e a = Mathlib.Tactic.BicategoryLike.Mor₁.id e_1 a_1) = (e = e_1 ∧ a = a_1)
-- Mathlib.GroupTheory.CommutingProbability
commProb_prod : ∀ (M : Type u_1) [inst : Mul M] (M' : Type u_2) [inst_1 : Mul M'], commProb (M × M') = commProb M * commProb M'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.Order.LatticeIntervals
Set.Ici.lattice : {α : Type u_1} → [inst : Lattice α] → {a : α} → Lattice ↑(Set.Ici a)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.Hom.ker_eq_bot_of_isIso : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f], AlgebraicGeometry.Scheme.Hom.ker f = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
_private.Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct.0.CategoryTheory.Limits.BinaryCoproductDisjoint.of_binaryCofan.match_1_3.splitter : (motive : (i j : CategoryTheory.Limits.WalkingPair) → i ≠ j → Sort u_1) →
  (i j : CategoryTheory.Limits.WalkingPair) →
    (hij : i ≠ j) →
      ((hij : CategoryTheory.Limits.WalkingPair.left ≠ CategoryTheory.Limits.WalkingPair.right) →
          motive CategoryTheory.Limits.WalkingPair.left CategoryTheory.Limits.WalkingPair.right hij) →
        ((hij : CategoryTheory.Limits.WalkingPair.right ≠ CategoryTheory.Limits.WalkingPair.left) →
            motive CategoryTheory.Limits.WalkingPair.right CategoryTheory.Limits.WalkingPair.left hij) →
          motive i j hij
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toMonComon_ofMonComon_obj_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) CategoryTheory.MonObj.one
-- ProofWidgets.Presentation.Expr
ProofWidgets.instRpcEncodableGetExprPresentationParams : Lean.Server.RpcEncodable ProofWidgets.GetExprPresentationParams
-- Mathlib.Algebra.Ring.Equiv
/-- The two paths coercion can take to an `AddMonoidHom` are equivalent  -/
RingEquiv.toAddMonoidMom_commutes : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S),
  (↑f).toAddMonoidHom = (↑f).toAddMonoidHom
-- Init.Data.Nat.Bitwise.Lemmas
Nat.instNeZeroHShiftLeft : ∀ {a n : ℕ} [NeZero a], NeZero (a <<< n)
-- Mathlib.Algebra.GroupWithZero.Defs
noZeroDivisors_iff_left_eq_zero_of_mul : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀], NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.dotId : Lean.Syntax → Lean.Name → Lean.LocalContext → Option Lean.Expr → Lean.Elab.CompletionInfo
-- Mathlib.Data.Finset.Card
Finset.card_sdiff_add_card : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s \ t).card + t.card = (s ∪ t).card
-- Init.Data.List.ToArray
Array.find?.eq_1 : ∀ {α : Type u} (p : α → Bool) (as : Array α),
  Array.find? p as =
    (do
        let __s ←
          forIn as (none, ()) fun a __s =>
              if p a = true then pure (ForInStep.done (some (some a), ())) else pure (ForInStep.yield (none, ()))
        have __r : Option (Option α) × Unit := __s
        match __r.1 with
          | some r => pure r
          | none => pure none).run
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I J : C} →
      {f : I ⟶ J} →
        [inst_1 : CategoryTheory.ChosenPullbacksAlong f] →
          (pushforward : CategoryTheory.Functor (CategoryTheory.Over I) (CategoryTheory.Over J)) →
            (CategoryTheory.ChosenPullbacksAlong.pullback f ⊣ pushforward) → CategoryTheory.ExponentiableMorphism f
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.map_sub : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [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]
  (D : LieDerivation R L M) (a b : L), D (a - b) = D a - D b
-- Mathlib.Tactic.ProxyType
/-- Given (constructor name, proxy constructor type, proxy constructor pattern) triples
constructed using `mkCtorProxyType`, return (1) the total proxy type (a `Type*`),
(2) patterns to use for each constructor, and (3) a proof to use to prove `left_inv` for
`proxy_type ≃ type` (this proof starts with `intro x`).  -/
Mathlib.ProxyType.ProxyEquivConfig.mkProxyType : Mathlib.ProxyType.ProxyEquivConfig →
  Array (Lean.Name × Lean.Expr × Lean.Term) → Lean.Elab.TermElabM (Lean.Expr × Array Lean.Term × Lean.TSyntax `tactic)
-- Mathlib.Data.Setoid.Basic
/-- The supremum of 2 equivalence relations r and s is the equivalence closure of the
supremum of the underlying binary operations.  -/
Setoid.sup_def : ∀ {α : Type u_1} {r s : Setoid α}, r ⊔ s = Relation.EqvGen.setoid (⇑r ⊔ ⇑s)
-- Mathlib.Order.CompleteLattice.Basic
le_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (f : ι → α) (i : ι), f i ≤ iSup f
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.CreatesColimits.createsFiniteColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.CreatesColimits F] → CategoryTheory.Limits.CreatesFiniteColimits F
-- Mathlib.Data.Finset.Max
Finset.isLeast_min' : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), IsLeast (↑s) (s.min' H)
-- Mathlib.Topology.Algebra.Group.Basic
Specializes.zpow : ∀ {G : Type u_1} [inst : DivInvMonoid G] [inst_1 : TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x y : G},
  x ⤳ y → ∀ (m : ℤ), (x ^ m) ⤳ (y ^ m)
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- This function is passed to `MVarId.gcongr` as the main discharger.
It doesn't try to prove the goal, but instead observes what the goal is,
to help determine which lemmas could work with `grw`.

If the selected grewrite position is valid, then `ref` is set, and a dummy error is thrown.
Note that this function will be called at most once,
so we don't lose information by throwing an error.  -/
_private.Mathlib.Tactic.ClickSuggestions.GRewrite.0.Mathlib.Tactic.ClickSuggestions.dummyDischarger : IO.Ref (Array Mathlib.Tactic.ClickSuggestions.GrwPos) → Bool → Lean.Expr → Lean.MVarId → Lean.MetaM Bool
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
csSup_image : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {s : Set β} {f : β → α},
  BddAbove (Set.range fun i => f ↑i) → sSup ∅ ≤ ⨆ i, f ↑i → sSup (f '' s) = ⨆ a ∈ s, f a
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.height.congr_simp : ∀ {ι : 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] {P : RootPairing ι R M N} (b b_1 : P.Base),
  b = b_1 → ∀ [inst_5 : CharZero R] (i i_1 : ι), i = i_1 → b.height i = b_1.height i_1
-- Mathlib.Data.Finset.SDiff
Finset.inter_sdiff_self : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ ∩ (s₂ \ s₁) = ∅
-- Mathlib.Analysis.Calculus.VectorField
/-- If a `C^2` map has an invertible derivative within a set at a point, then nearby derivatives
can be written as continuous linear equivs, which depend in a `C^1` way on the point, as well as
their inverse, and moreover one can compute the derivative of the inverse.  -/
exists_continuousLinearEquiv_fderivWithin_symm_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace E]
  {f : E → F} {s : Set E} {x : E},
  ContDiffWithinAt 𝕜 2 f s x →
    (fderivWithin 𝕜 f s x).IsInvertible →
      UniqueDiffOn 𝕜 s →
        x ∈ s →
          ∃ N,
            ContDiffWithinAt 𝕜 1 (fun y => ↑(N y)) s x ∧
              ContDiffWithinAt 𝕜 1 (fun y => ↑(N y).symm) s x ∧
                (∀ᶠ (y : E) in nhdsWithin x s, ↑(N y) = fderivWithin 𝕜 f s y) ∧
                  ∀ (v : E),
                    (fderivWithin 𝕜 (fun y => ↑(N y).symm) s x) v =
                      -↑(N x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(N x).symm
-- Init.Data.UInt.Lemmas
UInt8.le_iff_toBitVec_le : ∀ {a b : UInt8}, a ≤ b ↔ a.toBitVec ≤ b.toBitVec
-- Std.Time.Duration
Std.Time.Duration.instCoeOffset : Coe Std.Time.Nanosecond.Offset Std.Time.Duration
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
contDiffOn_ext_coord_change : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {n : WithTop ℕ∞} {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] [IsManifold I n M] (x x' : M),
  ContDiffOn 𝕜 n (↑(extChartAt I x) ∘ ↑(extChartAt I x').symm) ((extChartAt I x').symm.trans (extChartAt I x)).source
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- A non-unital subring of a `NonUnitalCommRing` is a `NonUnitalCommRing`.  -/
NonUnitalSubring.toNonUnitalCommRing : {R : Type u_1} → [inst : NonUnitalCommRing R] → (s : NonUnitalSubring R) → NonUnitalCommRing ↥s
-- Init.Data.Nat.Basic
Nat.mul_eq : ∀ {x y : ℕ}, x.mul y = x * y
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_add_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ ν : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G),
  (μ + ν).transpose B = μ.transpose B + ν.transpose B
-- Mathlib.CategoryTheory.Monad.Limits
/-- The coalgebra structure which will be the point of the new colimit cone for `D`.  -/
CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {T : CategoryTheory.Comonad C} →
          (D : CategoryTheory.Functor J T.Coalgebra) →
            (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) → CategoryTheory.Limits.IsColimit c → T.Coalgebra
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
CochainComplex.homologyMap_homologyδOfTriangle : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)),
  DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    ∀ (n₀ n₁ : ℤ) (h : autoParam (n₀ + 1 = n₁) CochainComplex.homologyMap_homologyδOfTriangle._auto_1),
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap T.mor₂ n₀)
          (CochainComplex.homologyδOfTriangle T n₀ n₁ h) =
        0
-- Mathlib.Order.NonemptyFiniteChains
/-- The image of a nonempty finite chain by a monotone map.  -/
PartialOrder.NonemptyFiniteChains.map : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : PartialOrder X] →
      [inst_1 : PartialOrder Y] → PartialOrder.NonemptyFiniteChains X → (X →o Y) → PartialOrder.NonemptyFiniteChains Y
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftAlgHom_apply_div : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} {S : Type u_3} [inst_2 : Field L]
  [inst_3 : CommSemiring S] [inst_4 : Algebra S (Polynomial K)] [inst_5 : Algebra S L] (φ : Polynomial K →ₐ[S] L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p q : Polynomial K),
  (RatFunc.liftAlgHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) =
    φ p / φ q
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_mk : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (a : Continuous (↑e).toFun)
  (b : Continuous e.invFun), ⇑{ toLinearEquiv := e, continuous_toFun := a, continuous_invFun := b } = ⇑e
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint32.injEq : ∀ (val val_1 : UInt32),
  (Lean.Compiler.LCNF.LitValue.uint32 val = Lean.Compiler.LCNF.LitValue.uint32 val_1) = (val = val_1)
-- Mathlib.Analysis.Analytic.Constructions
AnalyticWithinAt.neg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E},
  AnalyticWithinAt 𝕜 f s x → AnalyticWithinAt 𝕜 (-f) s x
-- Init.Data.UInt.Bitwise
UInt32.ofBitVec_xor : ∀ (a b : BitVec 32), { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }
-- Mathlib.Topology.MetricSpace.Polish
PolishSpace.IsClopenable.iUnion : ∀ {α : Type u_1} [t : TopologicalSpace α] [PolishSpace α] {s : ℕ → Set α},
  (∀ (n : ℕ), PolishSpace.IsClopenable (s n)) → PolishSpace.IsClopenable (⋃ n, s n)
-- Mathlib.Order.Minimal
minimal_and_iff_right_of_imp : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : LE α],
  (∀ ⦃x : α⦄, P x → Q x) → (Minimal (fun x => P x ∧ Q x) x ↔ Minimal P x ∧ Q x)
-- Mathlib.Algebra.Exact.Basic
AddMonoidHom.exact_iff : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : AddGroup M] [inst_1 : AddGroup N] [inst_2 : AddGroup P]
  {f : M →+ N} {g : N →+ P}, Function.Exact ⇑f ⇑g ↔ g.ker = f.range
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.Heart.full_ι : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Preadditive C}
  {inst_2 : CategoryTheory.Limits.HasZeroObject C} {inst_3 : CategoryTheory.HasShift C ℤ}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  {t : CategoryTheory.Triangulated.TStructure C} {H : Type u'} {inst_6 : CategoryTheory.Category.{v', u'} H}
  {inst_7 : CategoryTheory.Preadditive H} [self : t.Heart H], (CategoryTheory.Triangulated.TStructure.Heart.ι t).Full
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntryD_cons_of_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  {fallback : (a : α) × β a},
  (k == a) = false → Std.Internal.List.getEntryD a fallback (⟨k, v⟩ :: l) = Std.Internal.List.getEntryD a fallback l
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuous_iff_isOpen_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} [inst_1 : Preorder β],
  LowerSemicontinuous f ↔ ∀ (y : β), IsOpen (f ⁻¹' Set.Ioi y)
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.Ψ.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ)
  (hn₁ : n₀ + 1 = n₁),
  X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ =
    X.descCycles f₂ f₃ (CategoryTheory.CategoryStruct.comp f₂ f₃) ⋯
      (CategoryTheory.CategoryStruct.comp (X.δ f₁ (CategoryTheory.CategoryStruct.comp f₂ f₃) n₀ n₁ hn₁)
        (X.pOpcycles f₁ f₂ n₁))
      ⋯
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.liftEquiv_trans : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing K] [inst_1 : CommRing L]
  [inst_2 : CommRing M] [inst_3 : CommRing N] (i : K →+* L) (g : L →+* N) (p : ℕ) [inst_4 : ExpChar M p]
  [inst_5 : ExpChar K p] [inst_6 : PerfectRing M p] [inst_7 : IsPRadical i p] [inst_8 : ExpChar L p]
  [inst_9 : ExpChar N p] [inst_10 : IsPRadical g p] [inst_11 : IsPRadical (g.comp i) p],
  (PerfectRing.liftEquiv M i p).trans (PerfectRing.liftEquiv M g p) = PerfectRing.liftEquiv M (g.comp i) p
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.forall_toScheme : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} {P : ↥↑U → Prop}, (∀ (x : ↥↑U), P x) ↔ ∀ (x : ↥X) (hx : x ∈ U), P ⟨x, hx⟩
-- Qq.MetaM
Qq.MaybeLevelDefEq.defEq : {u v : Lean.Level} → u =QL v → Qq.MaybeLevelDefEq u v
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.isLUB_range_ωSup : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] (c : OmegaCompletePartialOrder.Chain α),
  IsLUB (Set.range ⇑c) (OmegaCompletePartialOrder.ωSup c)
-- Mathlib.Analysis.CStarAlgebra.Unitary.Span
selfAdjoint.star_coe_unitarySelfAddISMul : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (a : ↥(selfAdjoint A))
  (ha_norm : ‖a‖ ≤ 1), star ↑(selfAdjoint.unitarySelfAddISMul a ha_norm) = ↑a - Complex.I • CFC.sqrt (1 - ↑a ^ 2)
-- Init.Data.Repr
/-- The standard way of turning values of some type into `Format`.

When rendered this `Format` should be as close as possible to something that can be parsed as the
input value.
 -/
Repr : Type u → Type u
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
/-- `AddMonoidAlgebra.toDirectSum` and `DirectSum.toAddMonoidAlgebra` together form an
equiv.  -/
addMonoidAlgebraEquivDirectSum : {ι : Type u_1} →
  {M : Type u_3} →
    [DecidableEq ι] →
      [inst : Semiring M] → [(m : M) → Decidable (m ≠ 0)] → AddMonoidAlgebra M ι ≃ DirectSum ι fun x => M
-- Mathlib.Algebra.Module.Submodule.Defs
/-- Construct a submodule from closure under two-element linear combinations.
I.e., a nonempty set closed under two-element linear combinations is a submodule.  -/
Submodule.ofLinearComb : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (C : Set M) → C.Nonempty → (∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C) → Submodule R M
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_eq_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulBEq α] {k fallback : α},
  k ∈ m → m.getD k fallback = k
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.reindex_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι) (i' : ι'),
  (c.reindex e).π i' = c.π (e i')
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_filterMapM_filterMapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → n (Option γ)} {g : γ → o (Option δ)} {it : Std.IterM m β},
  (Std.IterM.filterMapM g (Std.IterM.filterMapM f it)).toArray =
    (Std.IterM.filterMapM
        (fun b => do
          let __do_lift ← liftM (f b)
          match __do_lift with
            | none => pure none
            | some fb => g fb)
        it).toArray
-- Init.Data.Array.Basic
/-- Applies a function that returns an array to each element of an array. The resulting arrays are
appended.

Examples:
* `#[2, 3, 2].flatMap Array.range = #[0, 1, 0, 1, 2, 0, 1]`
* `#[['a', 'b'], ['c', 'd', 'e']].flatMap List.toArray = #['a', 'b', 'c', 'd', 'e']`
 -/
Array.flatMap : {α : Type u} → {β : Type u_1} → (α → Array β) → Array α → Array β
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.instIsSolvableTensorProduct : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {A : Type u_1}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] [LieAlgebra.IsSolvable L], LieAlgebra.IsSolvable (TensorProduct R A L)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_right_le_mk_div : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk b ≤ MulArchimedeanClass.mk a → MulArchimedeanClass.mk b ≤ MulArchimedeanClass.mk (a / b)
-- Mathlib.Probability.Distributions.Uniform
/-- Given a non-empty multiset `s` we construct the `PMF` which sends `a` to the fraction of
elements in `s` that are `a`.  -/
PMF.ofMultiset : {α : Type u_1} → (s : Multiset α) → s ≠ 0 → PMF α
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pattern.ForwardSliceSearcher.startsWith.eq_1 : ∀ (pat s : String.Slice),
  String.Slice.Pattern.ForwardSliceSearcher.startsWith pat s =
    if h : pat.utf8ByteSize ≤ s.utf8ByteSize then
      have hs := ⋯;
      have hp := ⋯;
      String.Slice.Pattern.Internal.memcmpSlice s pat s.startPos.offset pat.startPos.offset pat.rawEndPos hs hp
    else false
-- Std.Http.Data.Body.Stream
/-- Non-blocking receive for the `Body` typeclass. Returns `none` when no producer is
waiting and the channel is still open, `some (some chunk)` when data is ready,
or `some none` at end-of-stream (channel closed with no pending producer).
 -/
Std.Http.Body.Stream.tryRecvBody : Std.Http.Body.Stream → Std.Async.Async (Option (Option Std.Http.Chunk))
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.startsWith.match_1.eq_2 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (x y : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq)
  (h_1 : (x y : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.var y))
  (h_2 :
    (x y : Lean.Grind.AC.Var) → (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.cons y s))
  (h_3 :
    (x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) →
        (x_1 : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x_1))
  (h_4 :
    (x : Lean.Grind.AC.Var) →
      (s₂ : Lean.Grind.AC.Seq) →
        (y : Lean.Grind.AC.Var) →
          (s₁ : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x s₂) (Lean.Grind.AC.Seq.cons y s₁)),
  (match Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.cons y s with
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.var y => h_1 x y
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.cons y s => h_2 x y s
    | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x_1 => h_3 x s x_1
    | Lean.Grind.AC.Seq.cons x s₂, Lean.Grind.AC.Seq.cons y s₁ => h_4 x s₂ y s₁) =
    h_2 x y s
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.hom_base_inv_base : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y),
  CategoryTheory.CategoryStruct.comp e.hom.base e.inv.base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace