mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.pullbackSpecIso_inv_fst'_assoc : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of S) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
          (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))
        h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap S (TensorProduct R S T)))) h
-- Lean.Parser.Basic
Lean.Parser.checkStackTopFn : (Lean.Syntax → Bool) → String → Lean.Parser.ParserFn
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.length : {α : Type u} → {β : α → Type v} → Std.DHashMap.Internal.AssocList α β → ℕ
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opUnopEquiv_unitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Functor.opUnopEquiv C D).unitIso =
    CategoryTheory.NatIso.ofComponents (fun F => (Opposite.unop F).opUnopIso.op) ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- Extract an isomorphism between base components from an isomorphism in
`CatCospanTransform F G F' G'`.  -/
CategoryTheory.Limits.CatCospanTransform.baseIso : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {A' : Type u₄} →
        {B' : Type u₅} →
          {C' : Type u₆} →
            [inst : CategoryTheory.Category.{v₁, u₁} A] →
              [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                  {F : CategoryTheory.Functor A B} →
                    {G : CategoryTheory.Functor C B} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} →
                                  (ψ ≅ ψ') → (ψ.base ≅ ψ'.base)
-- Mathlib.Data.Finset.Prod
Finset.subset_product : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] {s : Finset (α × β)},
  s ⊆ Finset.image Prod.fst s ×ˢ Finset.image Prod.snd s
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- `seminormFromBounded' f` as a `RingNorm` on `R`, provided that `f` is nonnegative,
multiplicatively bounded and subadditive, that it preserves `0` and negation, and that `f` has
trivial kernel.  -/
normFromBounded : {R : Type u_1} →
  [inst : CommRing R] →
    {f : R → ℝ} →
      {c : ℝ} →
        f 0 = 0 →
          0 ≤ f →
            (∀ (x y : R), f (x * y) ≤ c * f x * f y) →
              (∀ (a b : R), f (a + b) ≤ f a + f b) → (∀ (x : R), f (-x) = f x) → f ⁻¹' {0} = {0} → RingNorm R
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₄_of_isCharThreeJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF], W.b₄ = 0
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.mem_support_of_mem_walk_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), ¬p.Nil → ∀ {w : V}, w ∈ p.support → w ∈ G.support
-- Mathlib.Data.Finsupp.Defs
Finsupp.instInhabited : {α : Type u_1} → {M : Type u_4} → [inst : Zero M] → Inhabited (α →₀ M)
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.«termλ_» : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- **Alias** of `Ordinal.CNF.coeff_of_notMem_CNF`. -/
Ordinal.CNF.coeff_of_not_mem_CNF : ∀ {b o e : Ordinal.{u_1}}, e ∉ List.map Prod.fst (Ordinal.CNF b o) → (Ordinal.CNF.coeff b o) e = 0
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Iic_sub_one_eq_Iio : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] [NoMinOrder α] (b : α),
  Set.Iic (b - 1) = Set.Iio b
-- Init.Data.Range.Polymorphic.Map
/-- Compatibility class for `Map` and `Least?`.  -/
Std.PRange.UpwardEnumerable.Map.PreservesLeast? : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : Std.PRange.UpwardEnumerable β] →
        [Std.PRange.Least? α] → [Std.PRange.Least? β] → Std.PRange.UpwardEnumerable.Map α β → Prop
-- Mathlib.Analysis.Convex.Deriv
/-- Reformulation of `ConvexOn.slope_le_of_hasDerivAt` using `deriv`.  -/
ConvexOn.slope_le_deriv : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  ConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → DifferentiableAt ℝ f y → slope f x y ≤ deriv f y
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toMultiplicativeLeft_symm_apply_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : AddZeroClass G] [inst_1 : MulOneClass H] (f : Multiplicative G ≃* H) (a : G),
  (AddEquiv.toMultiplicativeLeft.symm f) a = (MonoidHom.toAdditiveRight f.toMonoidHom) a
-- Mathlib.Algebra.Group.Even
instDecidablePredMulOppositeIsSquare.eq_1 : ∀ {α : Type u_2} [inst : Mul α] [inst_1 : DecidablePred IsSquare] (x : αᵐᵒᵖ),
  instDecidablePredMulOppositeIsSquare x = decidable_of_iff (IsSquare (MulOpposite.unop x)) ⋯
-- Std.Time.Date.Unit.Month
/-- Returns the number of days until the `month`.
 -/
Std.Time.Month.Ordinal.cumulativeDays : Bool → Std.Time.Month.Ordinal → Std.Time.Day.Offset
-- Mathlib.GroupTheory.Congruence.Hom
/-- The kernel of the natural homomorphism from a monoid to its quotient by a congruence
relation `c` equals `c`.  -/
Con.mk'_ker : ∀ {M : Type u_1} [inst : MulOneClass M] (c : Con M), Con.ker c.mk' = c
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U),
  F.germ U x hx =
    CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp F) (Opposite.op ⟨U, hx⟩)
-- Mathlib.Topology.VectorBundle.Hom
/-- Consider `C^n` maps `v : M → E₁` and `v : M → E₂` to vector bundles, over a basemap
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ  m` to `v m` and `w m`, and the resulting map is `C^n`.  -/
ContinuousAt.clm_bundle_apply₂ : ∀ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {F₃ : Type u_12} {M : Type u_13}
  [inst : NontriviallyNormedField 𝕜] {E₁ : B → Type u_14} [inst_1 : (x : B) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B) → TopologicalSpace (E₁ x)]
  {E₂ : B → Type u_15} [inst_7 : (x : B) → AddCommGroup (E₂ x)] [inst_8 : (x : B) → Module 𝕜 (E₂ x)]
  [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_16} [inst_13 : (x : B) → AddCommGroup (E₃ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₃ x)] [inst_15 : NormedAddCommGroup F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [inst_18 : (x : B) → TopologicalSpace (E₃ x)]
  [inst_19 : TopologicalSpace B] [inst_20 : TopologicalSpace M] [inst_21 : FiberBundle F₁ E₁]
  [inst_22 : VectorBundle 𝕜 F₁ E₁] [inst_23 : FiberBundle F₂ E₂] [inst_24 : VectorBundle 𝕜 F₂ E₂]
  [inst_25 : FiberBundle F₃ E₃] [inst_26 : VectorBundle 𝕜 F₃ E₃] {b : M → B} {v : (x : M) → E₁ (b x)} {x : M}
  [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₃ x)] [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₃ x)]
  {ψ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x) →L[𝕜] E₃ (b x)} {w : (x : M) → E₂ (b x)},
  ContinuousAt (fun m => ⟨b m, ψ m⟩) x →
    ContinuousAt (fun m => ⟨b m, v m⟩) x →
      ContinuousAt (fun m => ⟨b m, w m⟩) x → ContinuousAt (fun m => ⟨b m, ((ψ m) (v m)) (w m)⟩) x
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.toContinuousAffineMap_toContinuousMap : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), e.toContinuousAffineMap.toContinuousMap = ↑e.toHomeomorph
-- Std.Data.Iterators.Lemmas.Producers.Repeat
_private.Std.Data.Iterators.Lemmas.Producers.Repeat.0.Nat.repeat.match_1.eq_1 : ∀ {α : Type u_2} (motive : ℕ → α → Sort u_1) (a : α) (h_1 : (a : α) → motive 0 a)
  (h_2 : (n : ℕ) → (a : α) → motive n.succ a),
  (match 0, a with
    | 0, a => h_1 a
    | n.succ, a => h_2 n a) =
    h_1 a
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.coe_sSup_apply' : ∀ {E : Type u_3} [inst : AddGroup E] {s : Set (NonarchAddGroupSeminorm E)},
  BddAbove s → ∀ {x : E}, (sSup s) x = sSup ((fun x_1 => x_1 x) '' s)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.filter_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool},
  t.WF → ((Std.DTreeMap.Raw.filter f t).Equiv t ↔ ∀ (k : α) (h : k ∈ t), f k (t.get k h) = true)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblX_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  W.Equation P →
    P 2 ≠ 0 →
      W.dblX P =
        ((MvPolynomial.eval P) W.polynomialX ^ 2 - W.a₁ * (MvPolynomial.eval P) W.polynomialX * P 2 * (P 1 - W.negY P) -
                W.a₂ * P 2 ^ 2 * (P 1 - W.negY P) ^ 2 -
              2 * P 0 * P 2 * (P 1 - W.negY P) ^ 2) *
            (P 1 - W.negY P) /
          P 2
-- Mathlib.Topology.Algebra.Group.Matrix
Matrix.SpecialLinearGroup.isClosedEmbedding_mapGL : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : CommRing S] [inst_5 : TopologicalSpace S] [inst_6 : Algebra R S]
  [IsTopologicalRing S] [IsTopologicalRing R] [T1Space R] [T1Space S],
  Topology.IsClosedEmbedding ⇑(algebraMap R S) → Topology.IsClosedEmbedding ⇑(Matrix.SpecialLinearGroup.mapGL S)
-- Mathlib.CategoryTheory.Limits.IsConnected
CategoryTheory.isConnected_of_hasTerminal : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasTerminal C],
  CategoryTheory.IsConnected C
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.lt_mul_inv_iff_mul_lt : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] (a b : R) {c : R}, 0 < c → (a < b * c⁻¹ ↔ a * c < b)
-- Mathlib.Order.OmegaCompletePartialOrder
Prod.ωScottContinuous_snd : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β],
  OmegaCompletePartialOrder.ωScottContinuous Prod.snd
-- Mathlib.Algebra.Group.Units.Defs
Units.inv_mul_eq_iff_eq_mul : ∀ {α : Type u} [inst : Monoid α] (a : αˣ) {b c : α}, ↑a⁻¹ * b = c ↔ b = ↑a * c
-- Mathlib.Topology.Hom.ContinuousEvalConst
Continuous.coeFun : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} {Z : Type u_4} [inst : FunLike F α X] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X] [inst_4 : TopologicalSpace Z] {f : Z → F},
  Continuous f → Continuous fun z => ⇑(f z)
-- Mathlib.Topology.Algebra.Algebra.Equiv
/-- The composition of two continuous algebra equivalences.  -/
ContinuousAlgEquiv.trans : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : TopologicalSpace A] →
              [inst_3 : Semiring B] →
                [inst_4 : TopologicalSpace B] →
                  [inst_5 : Semiring C] →
                    [inst_6 : TopologicalSpace C] →
                      [inst_7 : Algebra R A] →
                        [inst_8 : Algebra R B] → [inst_9 : Algebra R C] → (A ≃A[R] B) → (B ≃A[R] C) → A ≃A[R] C
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Functor.sections_property : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w)} (s : ↑F.sections)
  {j j' : J} (f : j ⟶ j'), (CategoryTheory.ConcreteCategory.hom (F.map f)) (↑s j) = ↑s j'
-- Init.Data.Ord.Basic
Ordering.isLE_swap : ∀ {o : Ordering}, o.swap.isLE = o.isGE
-- Mathlib.LinearAlgebra.Prod
Submodule.sup_eq_range : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p q : Submodule R M),
  p ⊔ q = (p.subtype.coprod q.subtype).range
-- Mathlib.Data.Nat.Cast.Field
Nat.cast_div_div_div_cancel_right : ∀ {K : Type u_1} [inst : DivisionSemiring K] {d m n : ℕ} [CharZero K], d ∣ n → d ∣ m → ↑(m / d) / ↑(n / d) = ↑m / ↑n
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow.eq_def : ∀ (basis_hd : ℝ → ℝ) (basis_tl : Tactic.ComputeAsymptotics.Basis) (n : ℕ) (r : ℝ),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow basis_hd basis_tl n r =
    match n with
    | 0 =>
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons r
        Tactic.ComputeAsymptotics.MultiseriesExpansion.one
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
    | m.succ =>
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons 0
        (Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow basis_tl m r)
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.ModelTheory.Syntax
/-- An equivalence of bounded formulas given by an equivalence of terms and an equivalence of
relations.  -/
FirstOrder.Language.BoundedFormula.mapTermRelEquiv : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} →
    {α : Type u'} →
      {β : Type v'} →
        ((n : ℕ) → L.Term (α ⊕ Fin n) ≃ L'.Term (β ⊕ Fin n)) →
          ((n : ℕ) → L.Relations n ≃ L'.Relations n) → {n : ℕ} → L.BoundedFormula α n ≃ L'.BoundedFormula β n
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Remove the `i`th element of the set, by its index from left to right.

```
remove_nth {a, b, c, d} 2 = {a, b, d}
remove_nth {a, b, c, d} 5 = {a, b, c, d}
```  -/
Ordnode.removeNth : {α : Type u_1} → Ordnode α → ℕ → Ordnode α
-- Mathlib.Analysis.Calculus.LineDeriv.Measurable
aestronglyMeasurable_lineDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E]
  {F : Type u_3} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {v : E}
  [SecondCountableTopologyEither E F],
  Continuous f → ∀ (μ : MeasureTheory.Measure E), MeasureTheory.AEStronglyMeasurable (fun x => lineDeriv 𝕜 f x v) μ
-- Mathlib.Topology.Constructions
Pi.continuous_domRestrict₂_apply : ∀ {X : Type u} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Z] {s t : Set X} (hst : s ⊆ t)
  {f : ↑t → Z}, Continuous f → Continuous (Set.domRestrict₂ hst f)
-- Lean.Widget.Diff
/-- Add a tag to the diff at the positions given by `before` and `after`.  -/
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiff.withChange : Lean.SubExpr → Lean.SubExpr → optParam Lean.Widget.ExprDiffTag✝ Lean.Widget.ExprDiffTag.change✝ → Lean.Widget.ExprDiff✝
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
contMDiffAt_addInvariantVectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G]
  [inst_7 : LieAddGroup I (minSmoothness 𝕜 3) G] (v : AddGroupLieAlgebra I G) {g : G},
  ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun g => ⟨g, addInvariantVectorField v g⟩) g
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.mem_sup_left : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R} {x : R}, x ∈ I → x ∈ I ⊔ J
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `M` is finite free over a PID `R`, then any submodule `N` is free
and we can find a basis for `M` and `N` such that the inclusion map is a diagonal matrix
in Smith normal form.

See `Submodule.exists_smith_normal_form_of_le` for a version of this theorem that doesn't
need to map `N` into a submodule of `O`.

This is a strengthening of `Submodule.basisOfPidOfLe`.
 -/
Submodule.smithNormalFormOfLE : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [IsDomain R] →
              [IsPrincipalIdealRing R] →
                [Finite ι] →
                  Module.Basis ι R M →
                    (N O : Submodule R M) →
                      N ≤ O → (o : ℕ) × (n : ℕ) × Module.Basis.SmithNormalForm (Submodule.comap O.subtype N) (Fin o) n
-- Mathlib.Tactic.NormNum.Result
/-- Extract from a `Result` the rational value (as both a term and an expression),
and the proof that the original expression is equal to this rational number.
 -/
Mathlib.Meta.NormNum.Result.toNNRat' : {u : Lean.Level} →
  {α : Q(Type u)} →
    {e : Q(«$α»)} →
      (_i : autoParam Q(DivisionSemiring «$α») Mathlib.Meta.NormNum.Result.toNNRat'._auto_1) →
        Mathlib.Meta.NormNum.Result e →
          Option (ℚ × (n : Q(ℕ)) × (d : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNNRat «$e» «$n» «$d»))
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- Two 2-morphisms into a right Kan lift are equal if their compositions with
each triangle 2-morphism are equal.  -/
CategoryTheory.Bicategory.RightLift.IsKan.hom_ext : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {t : CategoryTheory.Bicategory.RightLift f g} (H : t.IsKan) {k : c ⟶ b} {τ τ' : k ⟶ t.lift},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight τ f) t.counit =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight τ' f) t.counit →
    τ = τ'
-- Init.Control.Lawful.Instances
ExceptT.run_controlAt : ∀ {m : Type u → Type u_1} {ε α : Type u} [inst : Monad m] [LawfulMonad m]
  (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m (stM m (ExceptT ε m) α)),
  (controlAt m f).run = f fun {β} x => x.run
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.mk_le_mk : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (x y : K)
  (hx : 0 ≤ ArchimedeanClass.mk x) (hy : 0 ≤ ArchimedeanClass.mk y),
  ArchimedeanClass.FiniteElement.mk x hx ≤ ArchimedeanClass.FiniteElement.mk y hy ↔ x ≤ y
-- Mathlib.CategoryTheory.Limits.Comma
/-- If `L` preserves the appropriate colimit, then given a colimit cocone for `F ⋙ fst L R : J ⥤ L` and
a cocone for `F ⋙ snd L R : J ⥤ R` we can build a cocone for `F` which will turn out to be a
colimit cocone.
 -/
CategoryTheory.Comma.coconeOfPreserves : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {A : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        {B : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
            {T : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} T] →
                {L : CategoryTheory.Functor A T} →
                  {R : CategoryTheory.Functor B T} →
                    (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) →
                      [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] →
                        {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} →
                          CategoryTheory.Limits.IsColimit c₁ →
                            CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R)) →
                              CategoryTheory.Limits.Cocone F
-- Lean.Elab.Calc
Lean.Elab.Term.CalcStepView.ref : Lean.Elab.Term.CalcStepView → Lean.Syntax
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULift.equivalence_unitIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.ULift.equivalence.unitIso.inv =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ULift.upFunctor.comp CategoryTheory.ULift.downFunctor)
-- Mathlib.Data.Vector.Defs
/-- Runs a function over a vector returning the intermediate results and a
final result.
 -/
List.Vector.mapAccumr : {α : Type u_1} → {β : Type u_2} → {σ : Type u_3} → {n : ℕ} → (α → σ → σ × β) → List.Vector α n → σ → σ × List.Vector β n
-- Lean.Expr
/-- Like `Lean.Expr.getAppArgs` but returns up to `maxArgs` arguments.

In particular, given `f a₁ a₂ ... aₙ`, returns `#[aₖ₊₁, ..., aₙ]`
where `k` is minimal such that the size of this array is at most `maxArgs`.
 -/
Lean.Expr.getBoundedAppArgs : ℕ → Lean.Expr → Array Lean.Expr
-- Mathlib.Analysis.Normed.Field.Krasner
/-- If `K` is a complete nontrivially normed field and `L` is an algebraic extension of `K`
such that the norm of `L` extends the norm on `K`, then `IsKrasner K L` holds.
This corresponds to the classical Krasner's lemma.
 -/
IsKrasner.of_completeSpace : ∀ (K : Type u_1) (L : Type u_2) [inst : NormedField L] [inst_1 : NontriviallyNormedField K] [CompleteSpace K]
  [IsUltrametricDist K] [inst_4 : NormedAlgebra K L] [Algebra.IsAlgebraic K L], IsKrasner K L
-- Lean.Parser.Types
Lean.Parser.ParserModuleContext.mk.sizeOf_spec : ∀ (env : Lean.Environment) (options : Lean.Options) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl),
  sizeOf { env := env, options := options, currNamespace := currNamespace, openDecls := openDecls } =
    1 + sizeOf env + sizeOf options + sizeOf currNamespace + sizeOf openDecls
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.transpose : ∀ {n : Type u_2} {R' : Type u_4} [inst : CommRing R'] [inst_1 : PartialOrder R'] [inst_2 : StarRing R']
  {M : Matrix n n R'}, M.PosDef → M.transpose.PosDef
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_insertMany_list : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {l : List ((a : α) × β a)},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑↑(m.insertMany l)).buckets).Perm
      (Std.Internal.List.insertList (Std.DHashMap.Internal.toListModel (↑m).buckets) l)
-- Init.Internal.Order.Basic
Lean.Order.lfp_monotone_fix : ∀ {α : Sort u} [inst : Lean.Order.CompleteLattice α] {f : α → α} {hm : Lean.Order.monotone f},
  Lean.Order.lfp_monotone f hm = f (Lean.Order.lfp_monotone f hm)
-- Mathlib.Algebra.Lie.Basic
LieRing.instLieAlgebra : {L : Type v} → [inst : LieRing L] → LieAlgebra ℤ L
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS'.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ), complEDS' b c d k 0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.ofIso_pt : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P P' Q Q' : C} (b : CategoryTheory.Limits.BinaryBicone P Q) (eP : P ≅ P') (eQ : Q ≅ Q'), (b.ofIso eP eQ).pt = b.pt