mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Circular
/-- If `b` is between `a` and `c`, then `c` is between `b` and `a`.
This is motivated by imagining three points on a circle.  -/
CircularPreorder.btw_cyclic_left : ∀ {α : Type u_1} [self : CircularPreorder α] {a b c : α}, btw a b c → btw b c a
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn.go : {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
  {motive_2 :
      Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
        Sort u} →
    {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
      {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
        {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
          {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
            {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
              {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
                (t : Lean.Elab.Tactic.TacticParsedSnapshot) →
                  ((t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t) →
                    ((t :
                          Lean.Language.TransformedSnap
                            (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
                        Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t) →
                      ((t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                          Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t) →
                        ((t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
                            Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t) →
                          ((t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                              Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t) →
                            ((t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                                Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t) →
                              ((t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
                                  Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t) →
                                ((t : Task Lean.Elab.Tactic.TacticParsedSnapshot) →
                                    Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t) →
                                  motive_1 t ×' t.below
-- Mathlib.Analysis.InnerProductSpace.OfNorm
_private.Mathlib.Analysis.InnerProductSpace.OfNorm.0.term𝓚 : Lean.ParserDescr
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.IsCardinalFiltered.congr_simp : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (κ κ_1 : Cardinal.{w}) (e_κ : κ = κ_1)
  [inst_1 : Fact κ.IsRegular], CategoryTheory.IsCardinalFiltered J κ = CategoryTheory.IsCardinalFiltered J κ_1
-- Mathlib.Data.Finsupp.ToDFinsupp
sigmaFinsuppEquivDFinsupp_single : ∀ {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [inst : DecidableEq ι] [inst_1 : Zero N] (a : (i : ι) × η i) (n : N),
  (sigmaFinsuppEquivDFinsupp fun₀ | a => n) = fun₀ | a.fst => fun₀ | a.snd => n
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- The cofibrant resolution functor `HoCat.resolution`, as a localizer morphism.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.localizerMorphismResolution : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.LocalizerMorphism (HomotopicalAlgebra.weakEquivalences C)
        (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.CofibrantObject.HoCat C))
-- Lean.Elab.Do.PatternVar
_private.Lean.Elab.Do.PatternVar.0.Lean.Elab.Do.getLetEqnsDeclVars : Lean.TSyntax `Lean.Parser.Term.letEqnsDecl → Lean.Elab.TermElabM (Array Lean.Ident)
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.retracts_monotone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], Monotone CategoryTheory.MorphismProperty.retracts
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅} {km : α}, t.minKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Aesop.Stats.Basic
Aesop.instToJsonGoalStats.toJson : Aesop.GoalStats → Lean.Json
-- Mathlib.Computability.RegularExpressions
RegularExpression.map.eq_4 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (P Q : RegularExpression α),
  RegularExpression.map f (P.plus Q) = RegularExpression.map f P + RegularExpression.map f Q
-- Mathlib.Data.LawfulXor.Basic
instLawfulXorInt16 : LawfulXor Int16
-- Mathlib.Data.List.Lattice
List.inter_subset_left : ∀ {α : Type u_1} [inst : DecidableEq α] {l₁ l₂ : List α}, l₁ ∩ l₂ ⊆ l₁
-- Lean.Meta.Tactic.Grind.Types
/-- Combines all solver extensions into a single action using `Action.andAlso`.
Does not drain `newRawFacts`; use `Solvers.mkAction` (defined in `Intro.lean`) which
wraps this with `assertAll`.
 -/
Lean.Meta.Grind.Solvers.mkActionCore : IO Lean.Meta.Grind.Action
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `{ m_i }` is an `R`-basis of `M`, if `{ n_i }` is an `R`-basis of `N`,
such that the family `{ m_i * n_j }` in `S` is `R`-linearly independent
(in this result it is stated as the relevant `Finsupp.linearCombination` is injective),
then `M` and `N` are linearly disjoint.  -/
Submodule.LinearDisjoint.of_basis_mul' : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S)
  {κ : Type u_1} {ι : Type u_2} (m : Module.Basis κ R ↥M) (n : Module.Basis ι R ↥N),
  Function.Injective ⇑(Finsupp.linearCombination R fun i => ↑(m i.1) * ↑(n i.2)) → M.LinearDisjoint N
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_fn_inj : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {φ₁ φ₂ : A →ₐc[R] B}, ⇑φ₁ = ⇑φ₂ ↔ φ₁ = φ₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq)
  {v : β k} [inst_1 : Inhabited (β k')],
  List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (↑(t.insertMany l ⋯)).get! k' = cast ⋯ v
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.hasCoeToOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} →
            Coe (CategoryTheory.Oplax.StrongTrans.Modification η θ)
              ((CategoryTheory.Oplax.StrongTrans.toOplax η).Modification (CategoryTheory.Oplax.StrongTrans.toOplax θ))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdFstIsoProd_inv_snd_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Y Z] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z]
  [inst_3 : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f CategoryTheory.Limits.prod.fst)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h)) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
-- Mathlib.Algebra.Category.Grp.EpiMono
/-- Let `g : B ⟶ S(X')` be defined as such that, for any `β : B`, `g(β)` is the function sending
point at infinity to point at infinity and sending coset `y` to `β • y`.
 -/
GrpCat.SurjectiveOfEpiAuxs.g : {A B : GrpCat} → (f : A ⟶ B) → ↑B →* Equiv.Perm (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity f)
-- Mathlib.Algebra.Group.Equiv.Basic
/-- The equivalence `(M₁ →+ N) ≃ (M₂ →+ N)` obtained by postcomposition with
an additive equivalence `e : M₁ ≃+ M₂`.  -/
AddEquiv.addMonoidHomCongrLeftEquiv : {M₁ : Type u_5} →
  {M₂ : Type u_6} →
    {N : Type u_8} →
      [inst : AddZeroClass M₁] → [inst_1 : AddZeroClass M₂] → [inst_2 : AddMonoid N] → M₁ ≃+ M₂ → (M₁ →+ N) ≃ (M₂ →+ N)
-- Mathlib.Analysis.Normed.Operator.Banach
/-- The spectrum of a continuous linear map `f` over a Banach space is exactly the spectrum of `f`
viewed as a mere linear map.
 -/
ContinuousLinearMap.spectrum_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {f : E →L[𝕜] E}, spectrum 𝕜 f = spectrum 𝕜 ↑f
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Bicategory.associator_inv_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b) (β : b ⟶ c)
  (γ : c ⟶ d),
  (CategoryTheory.Bicategory.Adj.Bicategory.associator α β γ).inv.τl =
    (CategoryTheory.Bicategory.associator α.l β.l γ.l).inv
-- Init.Data.Fin.OverflowAware
Fin.addNat?_eq_none_iff : ∀ {n m : ℕ} {i : Fin n}, i.addNat? m = none ↔ n ≤ ↑i + m
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.vecMul_injective_of_invertible : ∀ {m : Type u} [inst : DecidableEq m] {K : Type u_3} [inst_1 : Field K] [inst_2 : Fintype m] (A : Matrix m m K)
  [Invertible A], Function.Injective fun v => Matrix.vecMul v A
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, t.getKey! a = t.getKeyD a default
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isHigherOrder : Lean.Expr → Lean.MetaM Bool
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.ae_neBot : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, (MeasureTheory.ae μ).NeBot ↔ μ ≠ 0
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instSemiring : {α : Type u} →
  {R : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : Semiring R] →
          [BoundedMul R] →
            [ContinuousMul R] → [BoundedAdd R] → [ContinuousAdd R] → Semiring (BoundedContinuousFunction α R)
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- The residue of `ζ(s)` at `s = 1` is equal to 1 expressed using `tsum` and for a
real variable.  -/
tendsto_sub_mul_tsum_nat_rpow : Filter.Tendsto (fun s => (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s) (nhdsWithin 1 (Set.Ioi 1)) (nhds 1)
-- Mathlib.Topology.UniformSpace.Ultra.Completion
IsUltraUniformity.completion : ∀ {X : Type u_1} [inst : UniformSpace X] [IsUltraUniformity X], IsUltraUniformity (UniformSpace.Completion X)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.distribMulAction' : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {R₁ : Type u_5} →
        {s : ι → Type u_7} →
          [inst_1 : (i : ι) → AddCommMonoid (s i)] →
            [inst_2 : (i : ι) → Module R (s i)] →
              [inst_3 : Monoid R₁] →
                [inst_4 : DistribMulAction R₁ R] →
                  [SMulCommClass R₁ R R] → DistribMulAction R₁ (PiTensorProduct R fun i => s i)
-- Mathlib.Topology.Instances.ENat
ENat.isOpenEmbedding_natCast : Topology.IsOpenEmbedding Nat.cast
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exsphere.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 → ∀ (signs signs_1 : Finset (Fin (n + 1))), signs = signs_1 → s.exsphere signs = s_1.exsphere signs_1
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.instSubsingleton : ∀ {R : Type u_1} [Semiring R] [Subsingleton R], Subsingleton (PowerSeries R)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.swapTR.go.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Array α → Sort u_2) (a : α) (xs : List α) (i : ℕ) (acc : Array α)
  (h_1 : (x x_1 : ℕ) → (x_2 : Array α) → motive [] x x_1 x_2)
  (h_2 : (head : α) → (tail : List α) → (x : Array α) → motive (head :: tail) 0 0 x)
  (h_3 : (a : α) → (xs : List α) → (i : ℕ) → (acc : Array α) → motive (a :: xs) 0 i.succ acc)
  (h_4 : (a : α) → (xs : List α) → (i : ℕ) → (acc : Array α) → motive (a :: xs) i.succ 0 acc)
  (h_5 : (a : α) → (xs : List α) → (i j : ℕ) → (acc : Array α) → motive (a :: xs) i.succ j.succ acc),
  (match a :: xs, 0, i.succ, acc with
    | [], x, x_1, x_2 => h_1 x x_1 x_2
    | head :: tail, 0, 0, x => h_2 head tail x
    | a :: xs, 0, i.succ, acc => h_3 a xs i acc
    | a :: xs, i.succ, 0, acc => h_4 a xs i acc
    | a :: xs, i.succ, j.succ, acc => h_5 a xs i j acc) =
    h_3 a xs i acc
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- `HasBiproduct F` expresses the mere existence of a bicone which is
simultaneously a limit and a colimit of the diagram `F`.  -/
CategoryTheory.Limits.HasBiproduct.exists_biproduct : ∀ {J : Type w} {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {F : J → C} [self : CategoryTheory.Limits.HasBiproduct F],
  Nonempty (CategoryTheory.Limits.LimitBicone F)
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.coe_ideal_span_singleton_div_self : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {x : R₁}, x ≠ 0 → ↑(Ideal.span {x}) / ↑(Ideal.span {x}) = 1
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Typecheck a `MonoidHom` as a morphism in `MonCat`.  -/
MonCat.ofHom : {X Y : Type u} → [inst : Monoid X] → [inst_1 : Monoid Y] → (X →* Y) → (MonCat.of X ⟶ MonCat.of Y)
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpaceCore.mk.inj : ∀ {H : Type u_5} {inst : TopologicalSpace H} {M : Type u_6} {atlas : Set (PartialEquiv M H)}
  {chartAt : M → PartialEquiv M H} {mem_chart_source : ∀ (x : M), x ∈ (chartAt x).source}
  {chart_mem_atlas : ∀ (x : M), chartAt x ∈ atlas}
  {open_source : ∀ (e e' : PartialEquiv M H), e ∈ atlas → e' ∈ atlas → IsOpen (e.symm.trans e').source}
  {continuousOn_toFun :
    ∀ (e e' : PartialEquiv M H), e ∈ atlas → e' ∈ atlas → ContinuousOn (↑(e.symm.trans e')) (e.symm.trans e').source}
  {atlas_1 : Set (PartialEquiv M H)} {chartAt_1 : M → PartialEquiv M H}
  {mem_chart_source_1 : ∀ (x : M), x ∈ (chartAt_1 x).source} {chart_mem_atlas_1 : ∀ (x : M), chartAt_1 x ∈ atlas_1}
  {open_source_1 : ∀ (e e' : PartialEquiv M H), e ∈ atlas_1 → e' ∈ atlas_1 → IsOpen (e.symm.trans e').source}
  {continuousOn_toFun_1 :
    ∀ (e e' : PartialEquiv M H),
      e ∈ atlas_1 → e' ∈ atlas_1 → ContinuousOn (↑(e.symm.trans e')) (e.symm.trans e').source},
  { atlas := atlas, chartAt := chartAt, mem_chart_source := mem_chart_source, chart_mem_atlas := chart_mem_atlas,
        open_source := open_source, continuousOn_toFun := continuousOn_toFun } =
      { atlas := atlas_1, chartAt := chartAt_1, mem_chart_source := mem_chart_source_1,
        chart_mem_atlas := chart_mem_atlas_1, open_source := open_source_1,
        continuousOn_toFun := continuousOn_toFun_1 } →
    atlas = atlas_1 ∧ chartAt = chartAt_1
-- Mathlib.Algebra.Order.Group.Abs
sub_lt_of_abs_sub_lt_right : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b c : G},
  |a - b| < c → a - c < b
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Verify that `grind?` suggestions actually work.  -/
linter.tacticAnalysis.verifyGrind : Lean.Option Bool
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.inter.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t₁ t₁_1 : Std.ExtTreeSet α cmp),
  t₁ = t₁_1 → ∀ (t₂ t₂_1 : Std.ExtTreeSet α cmp), t₂ = t₂_1 → t₁.inter t₂ = t₁_1.inter t₂_1
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.convex : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (C : PointedCone R E), Convex R ↑C
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α},
  k ∈ Std.ExtDTreeMap.filterMap f t ↔ ∃ (h : k ∈ t), (f (t.getKey k h) (Std.ExtDTreeMap.Const.get t k h)).isSome = true
-- Mathlib.RingTheory.Length
Module.length_of_free_of_finite : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Free R M] [Module.Finite R M], Module.length R M = ↑(Module.finrank R M) * Module.length R R
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.maxKey he ∈ t
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual : {α : Type u_1} → [LinearOrderedAddCommMonoidWithTop α] → LinearOrderedCommMonoidWithZero (Multiplicative αᵒᵈ)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.congr'_enorm : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {l : Filter α} {ε'' : Type u_7}
  [inst_2 : TopologicalSpace ε''] [inst_3 : ContinuousENorm ε''] {g : α → ε''},
  MeasureTheory.IntegrableAtFilter f l μ →
    MeasureTheory.AEStronglyMeasurable g μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) → MeasureTheory.IntegrableAtFilter g l μ
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.toListRev_iterFromIdx : ∀ {β : Type w} {n : ℕ} {xs : Vector β n} {pos : ℕ}, (xs.iterFromIdx pos).toListRev = (List.drop pos xs.toList).reverse
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.mk.sizeOf_spec : ∀ {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 : SizeOf C] [inst_3 : SizeOf D]
  (preimage : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y))
  (map_preimage :
    autoParam (∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage f) = f)
      CategoryTheory.Functor.FullyFaithful.map_preimage._autoParam)
  (preimage_map :
    autoParam (∀ {X Y : C} (f : X ⟶ Y), preimage (F.map f) = f)
      CategoryTheory.Functor.FullyFaithful.preimage_map._autoParam),
  sizeOf { preimage := preimage, map_preimage := map_preimage, preimage_map := preimage_map } = 1
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι] {Z : C} (h : H ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.homologyπ
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).inv h) =
    CategoryTheory.CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).inv (CategoryTheory.CategoryStruct.comp π h)
-- Mathlib.RingTheory.Extension.Generators
AlgHomClass.toAlgHom.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {F : Type u_5} [inst_5 : FunLike F A B] [inst_6 : AlgHomClass F R A B]
  (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_sdiff_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iio a \ Set.Iic b = Set.Ioo b a
-- Aesop.Tree.Data
Aesop.GoalId.instDecidableRelLt : DecidableRel fun x1 x2 => x1 < x2
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.algebraMap_dvd_iff_dvd : ∀ {R : Type u_1} {a b : R} [inst : CommSemiring R] {z w : R},
  (algebraMap R (QuadraticAlgebra R a b)) z ∣ (algebraMap R (QuadraticAlgebra R a b)) w ↔ z ∣ w
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.self_mem_flag_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  [Nontrivial R] (b : Module.Basis (Fin n) R M) {i : Fin n} {k : Fin (n + 1)}, b i ∈ b.flag k ↔ i.castSucc < k
-- Init.Data.Nat.Coprime
Nat.coprime_one_left_eq_true : ∀ (n : ℕ), Nat.Coprime 1 n = True
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.multiset_sum_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {m : Multiset A}, (∀ x ∈ m, x ∈ S) → m.sum ∈ S
-- Mathlib.Topology.LocallyFinsupp.Pushforward
Function.locallyFinsupp.map_id : ∀ {X : Type u_1} {R : Type u_3} [inst : TopologicalSpace X] (w : X → R) [inst_1 : Semiring R]
  (c : Function.locallyFinsupp X R) [inst_2 : PrespectralSpace X],
  (∀ (z : X), w z = 1) → Function.locallyFinsupp.map id w ⋯ c = c
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.role.closeMsg : String
-- Mathlib.Algebra.Group.Units.Equiv
AddEquiv.neg_symm : ∀ (G : Type u_6) [inst : SubtractionCommMonoid G], (AddEquiv.neg G).symm = AddEquiv.neg G
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.domCongr_apply : ∀ {G : Type u_2} {H : Type u_3} {A : Type u_4} [inst : AddCommMonoid A] (e : G ≃ H) (l : SkewMonoidAlgebra A G),
  (SkewMonoidAlgebra.domCongr e) l = SkewMonoidAlgebra.equivMapDomain e l
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {s : Set Ω},
  MeasurableSet s →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      (μ.tilted fun x => t * X x) s =
        ENNReal.ofReal (∫ (a : Ω) in s, Real.exp (t * X a - ProbabilityTheory.cgf X μ t) ∂μ)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.equiv_of_beq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.TreeMap α β cmp} [inst : BEq β] [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [LawfulBEq β], (m₁ == m₂) = true → m₁.Equiv m₂
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.ofList_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k : α},
  Std.ExtHashSet.ofList [k] = ∅.insert k
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.IsLimit.hom_ext : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g}
  (hs : CategoryTheory.Limits.IsLimit s) {W : C} {k l : W ⟶ s.pt},
  CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι → k = l
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertManyIfNewUnit l).getKey! k' = k