mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Language.Lean.Types
/-- Resulting elaboration state.  -/
Lean.Language.Lean.CommandResultSnapshot.cmdState : Lean.Language.Lean.CommandResultSnapshot → Lean.Elab.Command.State
-- Init.Prelude
/-- Given `a : α`, then `pure a : f α` represents an action that does nothing and returns `a`.

Examples:
* `(pure "hello" : Option String) = some "hello"`
* `(pure "hello" : Except (Array String) String) = Except.ok "hello"`
* `(pure "hello" : StateM Nat String).run 105 = ("hello", 105)`
 -/
Pure.pure : {f : Type u → Type v} → [self : Pure f] → {α : Type u} → α → f α
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnCommRing.sizeOf_spec : ∀ (e : Lean.Expr) (p : Int.Internal.Linear.Poly) (re : Lean.Meta.Grind.Arith.CommRing.RingExpr)
  (rp : Lean.Grind.CommRing.Poly) (p' : Int.Internal.Linear.Poly),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnCommRing e p re rp p') =
    1 + sizeOf e + sizeOf p + sizeOf re + sizeOf rp + sizeOf p'
-- Mathlib.Tactic.Clean
/-- (Deprecated) `clean t` is a macro for `exact clean% t`.  -/
Mathlib.Tactic.tacticClean_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.Preserves
/-- If `F` is a presheaf which satisfies the sheaf condition with respect to the empty presieve on any
object, then `F` takes that object to the terminal object.
 -/
CategoryTheory.Presieve.isTerminal_of_isSheafFor_empty_presieve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : C) →
      (F : CategoryTheory.Functor Cᵒᵖ (Type w)) →
        CategoryTheory.Presieve.IsSheafFor F
            (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a) →
          CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op I))
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.Context.mctx₁ : Aesop.EqualUpToIdsM.Context → Lean.MetavarContext
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.ofIsTopCompl_add : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} {F : Type u_3} [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : TopologicalSpace F] [inst_6 : AddCommGroup F]
  [inst_7 : Module R F] [inst_8 : ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q)
  (φ₁ φ₂ : ↥p →L[R] F) (ψ₁ ψ₂ : ↥q →L[R] F),
  ContinuousLinearMap.ofIsTopCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) =
    ContinuousLinearMap.ofIsTopCompl h φ₁ ψ₁ + ContinuousLinearMap.ofIsTopCompl h φ₂ ψ₂
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.reindex_comp_tprod : ∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (e : ι ≃ ι₂),
  (↑(PiTensorProduct.reindex R s e)).compMultilinearMap (PiTensorProduct.tprod R) =
    (MultilinearMap.domDomCongrLinearEquiv' R R s (PiTensorProduct R fun i => s (e.symm i)) e).symm
      (PiTensorProduct.tprod R)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso_inv_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C)
  (X_1 : CategoryTheory.Discrete PUnit.{w + 1}),
  (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.unitIso.inv.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id
      (X.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1})))
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.WalkingParallelPair.zero : CategoryTheory.Limits.WalkingParallelPair
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.degree_map_eq_of_leadingCoeff_ne_zero : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {p : Polynomial R} (f : R →+* S),
  f p.leadingCoeff ≠ 0 → (Polynomial.map f p).degree = p.degree
-- Init.Data.Array.Erase
Array.mem_eraseP_of_neg : ∀ {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α}, ¬p a = true → (a ∈ xs.eraseP p ↔ a ∈ xs)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂).get k h_mem = m₁.get k ⋯
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
/-- Given a short complex `S` of modules, this is the isomorphism between the abstract `S.opcycles`
of the homology API and the more concrete description as `S.X₂ ⧸ LinearMap.range S.f.hom`.  -/
CategoryTheory.ShortComplex.moduleCatOpcyclesIso : {R : Type u} →
  [inst : Ring R] →
    (S : CategoryTheory.ShortComplex (ModuleCat R)) →
      S.opcycles ≅ ModuleCat.of R (↑S.X₂ ⧸ (ModuleCat.Hom.hom S.f).range)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.instCategory : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Category.{v, max u v} (CategoryTheory.CosimplicialObject C)
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.kerParam_range_eq : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α},
  (Equiv.Perm.OnCycleFactors.kerParam g).range =
    Subgroup.map (Subgroup.centralizer {g}).subtype (Equiv.Perm.OnCycleFactors.toPermHom g).ker
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.quasiCompactCover_iff : ∀ {S : AlgebraicGeometry.Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S),
  AlgebraicGeometry.QuasiCompactCover 𝒰 ↔
    ∀ {U : S.Opens}, AlgebraicGeometry.IsAffineOpen U → IsCompactOpenCovered (fun x => ⇑(𝒰.f x)) ↑U
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_zero_right : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (y : M), QuadraticMap.polar (⇑Q) y 0 = 0
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHomClass.eq_1 : ∀ (F : Type u_10) (M : Type u_11) (A : Type u_12) (B : Type u_13) [inst : Monoid M] [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : DistribMulAction M A] [inst_4 : DistribMulAction M B] [inst_5 : FunLike F A B],
  DistribMulActionHomClass F M A B = DistribMulActionSemiHomClass F (⇑(MonoidHom.id M)) A B
-- Init.Data.UInt.Lemmas
UInt64.sub_le : ∀ {a b : UInt64}, b ≤ a → a - b ≤ a
-- Mathlib.Analysis.Calculus.Deriv.Comp
fderiv_comp_deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F} (x : 𝕜)
  {l : F → E}, DifferentiableAt 𝕜 l (f x) → DifferentiableAt 𝕜 f x → deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.norm_le_seminorm : ∀ (𝕜 : Type u_2) {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (x₀ : E), ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 0) f
-- Mathlib.Topology.Separation.Basic
/-- Removing a finite set from a dense set in a space without isolated points, one still
obtains a dense set.  -/
Dense.sdiff_finite : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X},
  Dense s → ∀ {t : Set X}, t.Finite → Dense (s \ t)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_attach_eq_sum_dite : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Fintype ι] (s : Finset ι) (f : ↥s → M)
  [inst_2 : DecidablePred fun x => x ∈ s], ∑ i ∈ s.attach, f i = ∑ i, if h : i ∈ s then f ⟨i, h⟩ else 0
-- Mathlib.Logic.Function.Basic
/-- Involuting an `ite` of an involuted value `x : α` negates the `Prop` condition in the `ite`.  -/
Function.Involutive.ite_not : ∀ {α : Sort u} {f : α → α},
  Function.Involutive f → ∀ (P : Prop) [inst : Decidable P] (x : α), f (if P then x else f x) = if ¬P then x else f x
-- Mathlib.Computability.PartrecCode
PFun.pure.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (x : β) (x_1 : α), PFun.pure x x_1 = Part.some x
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- One can bound the `k`-th derivative of the Fourier integral of `f`, multiplied by `(L v w) ^ n`,
in terms of integrals of iterated derivatives of `f` (of order up to `n`) multiplied by `‖v‖ ^ i`
(for `i ≤ k`).
Auxiliary version in terms of the operator norm of `fourierPowSMulRight (-L.flip) ⬝`. For a version
in terms of `|L v w| ^ n * ⬝`, see `pow_mul_norm_iteratedFDeriv_fourierIntegral_le`.
 -/
VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V]
  {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] {K N : ℕ∞},
  ContDiff ℝ (↑N) f →
    (∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ) →
      ∀ {k n : ℕ},
        ↑k ≤ K →
          ↑n ≤ N →
            ∀ {w : W},
              ‖VectorFourier.fourierPowSMulRight (-L.flip)
                    (iteratedFDeriv ℝ k
                      (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f))
                    w n‖ ≤
                (2 * Real.pi) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k *
                  ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
                    ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : Type w} {inst_2 : CategoryTheory.Category.{w', w} J} {F : CategoryTheory.Functor C D}
  [self : CategoryTheory.Limits.PreservesLimitsOfShape J F] {K : CategoryTheory.Functor J C},
  CategoryTheory.Limits.PreservesLimit K F
-- Mathlib.Topology.PartitionOfUnity
/-- If `X` is a normal topological space and `U` is a locally finite open covering of a closed set
`s`, then there exists a `PartitionOfUnity ι X s` that is subordinate to `U`. If `X` is a
paracompact space, then the assumption `hf : LocallyFinite U` can be omitted, see
`BumpCovering.exists_isSubordinate`.  -/
PartitionOfUnity.exists_isSubordinate_of_locallyFinite : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [NormalSpace X],
  IsClosed s → ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → LocallyFinite U → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U
-- Batteries.Data.DList.Lemmas
_private.Batteries.Data.DList.Lemmas.0.Batteries.DList.push.match_1.splitter : {α : Type u_1} →
  (motive : Batteries.DList α → α → Sort u_2) →
    (x : Batteries.DList α) →
      (x_1 : α) →
        ((f : List α → List α) →
            (h : ∀ (l : List α), f l = f [] ++ l) → (a : α) → motive { apply := f, invariant := h } a) →
          motive x x_1
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.exists_pos_ball : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoMetricSpace α] (x : α),
  μ ≠ 0 → ∃ n, 0 < μ (Metric.ball x ↑n)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.desc_inl_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr =
    CategoryTheory.CategoryStruct.id (X ⨿ Y)
-- Mathlib.RingTheory.Artinian.Module
/-- **Alias** of `IsArtinianRing.setOfPred_isMaximal_finite`.

---

[Stacks Tag 00J7](https://stacks.math.columbia.edu/tag/00J7) -/
IsArtinianRing.setOf_isMaximal_finite : ∀ (R : Type u_1) [inst : CommSemiring R] [IsArtinianRing R], {I | I.IsMaximal}.Finite
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_add_iff_add_lt_ne_self`. -/
Ordinal.principal_add_iff_add_lt_ne_self : ∀ {a : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) a ↔ ∀ b < a, ∀ c < a, b + c ≠ a
-- Init.Data.Order.Ord
Array.instTransOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.TransOrd α], Std.TransOrd (Array α)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_diff_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∈ m₁ \ m₂ ↔ k ∈ m₁ ∧ k ∉ m₂
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.instInhabitedRelevantArg.default : Mathlib.Tactic.Translate.RelevantArg
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- A Bézout ring is a ring whose finitely generated ideals are principal.  -/
IsBezout : (R : Type u) → [Semiring R] → Prop
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m.erase k).size = if k ∈ m then m.size - 1 else m.size
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.instHasCoeffsSubtypeMemSubalgebraAdjoin : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [P.HasCoeffs R₀] (s : Set R),
  P.HasCoeffs ↥(Algebra.adjoin R₀ s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The (not necessarily limiting) `PullbackCone h i` implicit in the statement
that we have `CommSq f g h i`.
 -/
CategoryTheory.CommSq.cone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W X Y Z : C} →
      {f : W ⟶ X} →
        {g : W ⟶ Y} → {h : X ⟶ Z} → {i : Y ⟶ Z} → CategoryTheory.CommSq f g h i → CategoryTheory.Limits.PullbackCone h i
-- Mathlib.Topology.Order
/-- **Alias** of `TopologicalSpace.generateFrom_setOfPred_isOpen`. -/
TopologicalSpace.generateFrom_setOf_isOpen : ∀ {α : Type u} (t : TopologicalSpace α), TopologicalSpace.generateFrom {s | IsOpen s} = t
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.map_constants : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (φ : L.ElementaryEmbedding M N) (c : L.Constants), φ ↑c = ↑c
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.toArray_keysIter : ∀ {α : Type u} {β : α → Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m.keysIter.toArray = m.keysArray
-- Mathlib.RingTheory.MvPowerSeries.Equiv
PowerSeries.toMvPowerSeries_X : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] (i : σ),
  (PowerSeries.toMvPowerSeries i) PowerSeries.X = MvPowerSeries.X i
-- Std.Sat.AIG.Basic
/-- An empty `Cache` is valid for any `Array Decl` as it never has a hit.
 -/
Std.Sat.AIG.Cache.WF.empty : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {decls : Array (Std.Sat.AIG.Decl α)},
  Std.Sat.AIG.Cache.WF decls ∅
-- Mathlib.RingTheory.Coalgebra.Basic
/-- The comultiplication of the coalgebra  -/
CoalgebraStruct.comul : {R : Type u} →
  {A : Type v} →
    {inst : CommSemiring R} →
      {inst_1 : AddCommMonoid A} → {inst_2 : Module R A} → [self : CoalgebraStruct R A] → A →ₗ[R] TensorProduct R A A
-- Init.System.Platform
System.Platform.eight_dvd_numBits : 8 ∣ System.Platform.numBits
-- Init.Data.String.PosRaw
String.Pos.Raw.Internal.minImpl : String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
_private.Lean.Meta.Tactic.Simp.Arith.Int.Basic.0.Lean.Meta.Simp.Arith.Int.adapter : Lean.Expr →
  (Lean.Expr → Lean.Meta.Simp.Arith.Int.ToLinear.M (Option (Int.Internal.Linear.Expr × Int.Internal.Linear.Expr))) →
    Lean.MetaM (Option (Int.Internal.Linear.Expr × Int.Internal.Linear.Expr × Array Lean.Expr))
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- The L-series of the von Mangoldt function restricted to the prime residue class `a` mod `q`
is continuous on `re s ≥ 1` except for a simple pole at `s = 1` with residue `(q.totient)⁻¹`.
The statement as given here in terms of `ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux`
is equivalent.  -/
ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux : ∀ {q : ℕ} (a : ZMod q) [inst : NeZero q],
  ContinuousOn (ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux a) {s | 1 ≤ s.re}
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- If a subalgebra is contained in a finite-dimensional
subalgebra with the same dimension, they are equal.  -/
Subalgebra.eq_of_le_of_finrank_eq : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Ring L] [inst_2 : Algebra K L] {F E : Subalgebra K L}
  [hfin : FiniteDimensional K ↥E], F ≤ E → Module.finrank K ↥F = Module.finrank K ↥E → F = E
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.UseImplicitLambdaResult.yes : Lean.Expr → Lean.Elab.Term.UseImplicitLambdaResult
-- Mathlib.RingTheory.Perfection
PreTilt.val.congr_simp : ∀ (K : Type u₁) [inst : Field K] (v v_1 : Valuation K NNReal) (e_v : v = v_1) (O : Type u₂) [inst_1 : CommRing O]
  [inst_2 : Algebra O K] (hv : v.Integers O) (p : ℕ) [inst_3 : Fact (Nat.Prime p)] [inst_4 : Fact ¬IsUnit ↑p],
  PreTilt.val K v O hv p = PreTilt.val K v_1 O ⋯ p
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Naturality of the lax functoriality constraint, on the right.  -/
CategoryTheory.LaxFunctor.mapComp_naturality_right_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.LaxFunctor B C) {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g')
  {Z : self.obj a ⟶ self.obj c} (h : self.map (CategoryTheory.CategoryStruct.comp f g') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.mapComp f g)
      (CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η))
      (CategoryTheory.CategoryStruct.comp (self.mapComp f g') h)
-- Init.SimpLemmas
Bool.false_and : ∀ (b : Bool), (false && b) = false
-- Mathlib.Order.RelSeries
RelSeries.last.eq_1 : ∀ {α : Type u_1} {r : SetRel α α} (x : RelSeries r), x.last = x.toFun (Fin.last x.length)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.getDₘ_eq_getValueD : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α fun x => β} {fallback : β},
  t.Ordered → Std.DTreeMap.Internal.Impl.Const.getDₘ t k fallback = Std.Internal.List.getValueD k t.toListModel fallback
-- Aesop.Stats.Extension
Aesop.StatsExtension.importedEntries : Lean.Environment → Aesop.StatsExtension → Array (Array Aesop.StatsExtensionEntry)
-- Init.Data.Order.Classes
/-- This typeclass states that `Min.min a b` returns one of its arguments, either `a` or `b`.
 -/
Std.MinEqOr : (α : Type u) → [Min α] → Prop
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseWeekdayText : (Std.Time.Text → Std.Time.Modifier) → String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.IterM.step_take.match_1.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.IsLocallyFiniteMeasure.withDensity_coe : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α]
  [OpensMeasurableSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → NNReal},
  Continuous f → MeasureTheory.IsLocallyFiniteMeasure (μ.withDensity fun x => ↑(f x))
-- Mathlib.Data.Set.Lattice
Set.biInter_pair : ∀ {α : Type u_1} {β : Type u_2} (a b : α) (s : α → Set β), ⋂ x ∈ {a, b}, s x = s a ∩ s b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKeyGT?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyGT? k = t₂.getKeyGT? k
-- Init.Data.Array.Attach
Array.pmap_eq_pmapImpl : @Array.pmap = @Array.pmapImpl
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.naturality_id_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.StrongTrans F G) (a : B) {Z : F.obj a ⟶ G.obj a}
  (h : CategoryTheory.CategoryStruct.comp (self.app a) (CategoryTheory.CategoryStruct.id (G.obj a)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.app a)).inv h))
-- Aesop.Forward.Substitution
/-- Merge two substitutions. Precondition: the substitutions are compatible, so
they must have the same size and if `s₁[x]` and `s₂[x]` are both defined, they
must be defeq.  -/
Aesop.Substitution.mergeCompatible : Aesop.Substitution → Aesop.Substitution → Aesop.Substitution
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_iInf : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {ι : Sort u_7} [Nonempty ι] (f : G →* N),
  Function.Injective ⇑f → ∀ (s : ι → Subgroup G), Subgroup.map f (iInf s) = ⨅ i, Subgroup.map f (s i)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.mapRange_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {N : Type u_4} [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N] {f : M →+ N} (hf : Continuous ⇑f),
  MeasureTheory.VectorMeasure.mapRange 0 f hf = 0
-- Init.Data.Stream
Std.ToStream.mk : {collection : Type u} → {stream : outParam (Type u)} → (collection → stream) → Std.ToStream collection stream
-- Mathlib.Algebra.Module.PID
/-- A finitely generated torsion module over a PID is an internal direct sum of its
`p i ^ e i`-torsion submodules for some primes `p i` and numbers `e i`.  -/
Submodule.exists_isInternal_prime_power_torsion_of_pid : ∀ {R : Type u} [inst : CommRing R] [IsPrincipalIdealRing R] {M : Type v} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [IsDomain R] [Module.Finite R M],
  Module.IsTorsion R M →
    ∃ ι x x p,
      ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, DirectSum.IsInternal fun i => Submodule.torsionBy R M (p i ^ e i)
-- Mathlib.Algebra.Ring.SumsOfSquares
Nat.isSumSq : ∀ (n : ℕ), IsSumSq n
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.orderIsoRpow.eq_1 : ∀ (y : ℝ) (hy : 0 < y),
  NNReal.orderIsoRpow y hy = StrictMono.orderIsoOfRightInverse (fun x => x ^ y) ⋯ (fun x => x ^ (1 / y)) ⋯
-- Mathlib.Analysis.Complex.Isometry
/-- An element of the unit circle defines a `LinearIsometryEquiv` from `ℂ` to itself, by
rotation.  -/
rotation : Circle →* ℂ ≃ₗᵢ[ℝ] ℂ