mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.coe_variableChange_Δ' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R)
  [inst_1 : W.IsElliptic], ↑(C • W).Δ' = ↑C.u⁻¹ ^ 12 * ↑W.Δ'
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearRupUnits : {n : ℕ} → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_inter_eq_false_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₂ = false → Std.DTreeMap.Internal.Impl.contains k (m₁.inter m₂ ⋯) = false
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.closure_range : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α), closure (Set.range pkg.coe) = Set.univ
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.whiskeringLeftCompEvaluation_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (a : A)
  (X : CategoryTheory.Functor B C),
  (CategoryTheory.whiskeringLeftCompEvaluation F a).inv.app X = CategoryTheory.CategoryStruct.id (X.obj (F.obj a))
-- Lean.Data.KVMap
Lean.KVMap.entries : Lean.KVMap → List (Lean.Name × Lean.DataValue)
-- Mathlib.Algebra.Group.ULift
ULift.leftCancelMonoid.eq_1 : ∀ {α : Type u} [inst : LeftCancelMonoid α],
  ULift.leftCancelMonoid = Function.Injective.leftCancelMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- The logarithmic derivative converts products into sums: away from a codiscrete subset of `U`, the
logarithmic derivative of a product of two meromorphic functions is the sum of the logarithmic
derivatives.
 -/
MeromorphicOn.logDeriv_mul_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'} {U : Set 𝕜},
  MeromorphicOn f U →
    MeromorphicOn g U →
      (∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤) →
        (∀ x ∈ U, meromorphicOrderAt g x ≠ ⊤) → logDeriv (f * g) =ᶠ[Filter.codiscreteWithin U] logDeriv f + logDeriv g
-- Aesop.RuleSet
/-- The simprocs used by the builtin norm simp rule.
 -/
Aesop.LocalRuleSet.simprocsArray : Aesop.LocalRuleSet → Array (Lean.Name × Lean.Meta.Simprocs)
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.WithGeneratedByTopology.instTopologicalSpace : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} → [inst_1 : TopologicalSpace Y] → TopologicalSpace (Topology.WithGeneratedByTopology X Y)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [P.IsClosedUnderLimitsOfShape J], P.op.IsClosedUnderColimitsOfShape Jᵒᵖ
-- Mathlib.Topology.Order.IntermediateValue
/-- This lemma characterizes when a subset `s` of a densely ordered conditionally complete linear
order is totally disconnected with respect to the order topology: between any two distinct points
of `s` must lie a point not in `s`.  -/
isTotallyDisconnected_iff_lt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {s : Set α}, IsTotallyDisconnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Set.Ioo x y
-- Lean.Parser.Syntax
Lean.Parser.Command.catBehaviorBoth : Lean.Parser.Parser
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.haveLebesgueDecomposition_add : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν],
  μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
-- Mathlib.Algebra.Lie.Weights.Chain
/-- The last weight in an `α`-chain through `β`.  -/
LieModule.chainTop : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {M : Type u_3} →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    [inst_7 : LieRing.IsNilpotent L] →
                      [IsAddTorsionFree R] →
                        [IsDomain R] →
                          [Module.IsTorsionFree R M] →
                            [IsNoetherian R M] → (L → R) → LieModule.Weight R L M → LieModule.Weight R L M
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add'_map : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₂ : X ⟶ Y),
  CategoryTheory.Localization.Preadditive.add' W (L.map f₁) (L.map f₂) = L.map (f₁ + f₂)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 0th differential in the complex of inhomogeneous chains of a `G`-representation `A` as a
linear map into the `k`-submodule of `A` spanned by elements of the form
`ρ(g)(x) - x, g ∈ G, x ∈ A`.  -/
groupHomology.chains₁ToCoinvariantsKer : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → ModuleCat.of k (G →₀ ↑A) ⟶ ModuleCat.of k ↥(Representation.Coinvariants.ker A.ρ)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.homRel.δ_comp_δ : ∀ {n : ℕ} {i j : Fin (n + 2)},
  i ≤ j →
    FreeSimplexQuiver.homRel
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i))
        ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ j.succ)))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ j))
        ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i.castSucc)))
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} (self : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j),
  CategoryTheory.CategoryStruct.comp self.f' p = CategoryTheory.CategoryStruct.comp (c.ι.app j) g
-- Std.Sync.CancellationToken
Std.CancellationToken.State.mk : Option Std.CancellationReason → Std.Queue Std.CancellationToken.Consumer → Std.CancellationToken.State
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_iteratedFDerivComponent_le : ∀ {𝕜 : Type u} {ι : Type v} {E₁ : ι → Type wE₁} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] {α : Type u_1}
  [inst_6 : Fintype α] (f : ContinuousMultilinearMap 𝕜 E₁ G) {s : Set ι} (e : α ≃ ↑s)
  [inst_7 : DecidablePred fun x => x ∈ s] (x : (i : ι) → E₁ i),
  ‖(f.iteratedFDerivComponent e) fun x_1 => x ↑x_1‖ ≤ ‖f‖ * ‖x‖ ^ (Fintype.card ι - Fintype.card α)
-- Mathlib.Logic.Small.Defs
small_iff : ∀ (α : Type v), Small.{w, v} α ↔ ∃ S, Nonempty (α ≃ S)
-- Mathlib.Data.Nat.MaxPowDiv
_private.Mathlib.Data.Nat.MaxPowDiv.0.Nat.pow_dvd_iff_le_of_spec : ∀ {p k n a b : ℕ}, 1 < p → n ≠ 0 → p ^ a * b = n → ¬p ∣ b → (p ^ k ∣ n ↔ k ≤ a)
-- Mathlib.Tactic.Widget.CommDiag
/-- Given a Hom type `α ⟶ β`, return `(α, β)`. Otherwise `none`.  -/
Mathlib.Tactic.Widget.homType? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
MulActionWithZero.toMulAction : {M₀ : Type u_2} →
  {A : Type u_7} → {inst : MonoidWithZero M₀} → {inst_1 : Zero A} → [self : MulActionWithZero M₀ A] → MulAction M₀ A
-- Mathlib.Data.Set.Card
Set.exists_ne_of_one_lt_ncard : ∀ {α : Type u_1} {s : Set α}, 1 < s.ncard → ∀ (a : α), ∃ b ∈ s, b ≠ a
-- Mathlib.Order.RelClasses
/-- Set notation form of `le_refl` -/
subset_refl : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] (a : α), a ⊆ a
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.mono_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜}, MeromorphicOn f U → ∀ {V : Set 𝕜}, V ⊆ U → MeromorphicOn f V
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.instInhabitedEqCnstr : Inhabited Lean.Meta.Grind.AC.EqCnstr
-- Lean.Meta.Basic
/-- By default synthetic opaque metavariables are not assigned by `isDefEq`. Motivation: we want to make
sure typing constraints resolved during elaboration should not "fill" holes that are supposed to be filled using tactics.
However, this restriction is too restrictive for tactics such as `exact t`. When elaborating `t`, we dot not fill
named holes when solving typing constraints or TC resolution. But, we ignore the restriction when we try to unify
the type of `t` with the goal target type. We claim this is not a hack and is defensible behavior because
this last unification step is not really part of the term elaboration.  -/
Lean.Meta.Config.assignSyntheticOpaque : Lean.Meta.Config → Bool
-- Init.System.IOError
IO.Error.permissionDenied.inj : ∀ {filename : Option String} {osCode : UInt32} {details : String} {filename_1 : Option String} {osCode_1 : UInt32}
  {details_1 : String},
  IO.Error.permissionDenied filename osCode details = IO.Error.permissionDenied filename_1 osCode_1 details_1 →
    filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1
-- Init.Data.Fin.Lemmas
Fin.natAdd_natAdd : ∀ (m n : ℕ) {p : ℕ} (i : Fin p), Fin.natAdd m (Fin.natAdd n i) = Fin.cast ⋯ (Fin.natAdd (m + n) i)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.instAddConstMapClass : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H},
  AddConstMapClass (AddConstMap G H a b) G H a b
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticWithinAt.exists_hasFTaylorSeriesUpToOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}
  {s : Set E} [CompleteSpace F] (n : WithTop ℕ∞),
  AnalyticWithinAt 𝕜 f s x →
    ∃ u ∈ nhdsWithin x (insert x s), ∃ p, HasFTaylorSeriesUpToOn n f p u ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_posPart : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : LinearOrder γ] [inst_3 : OrderClosedTopology γ] [inst_4 : Zero γ] (f : α →ₘ[μ] γ),
  ↑f.posPart =ᵐ[μ] fun a => max (↑f a) 0
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- The left unitor: `𝟙 a ≫ f ≅ f`  -/
CategoryTheory.Bicategory.leftUnitor : {B : Type u} →
  [self : CategoryTheory.Bicategory B] →
    {a b : B} → (f : a ⟶ b) → CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ≅ f
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'.eq_1 : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (i j k : A) (h : i + j = k),
  CategoryTheory.shiftFunctorAdd' C i j k h = CategoryTheory.eqToIso ⋯ ≪≫ CategoryTheory.shiftFunctorAdd C i j
-- Lean.DocString.Formatter
_private.Lean.DocString.Formatter.0.Lean.Doc.Parser.versoSyntaxToString : Lean.Syntax → String
-- Mathlib.FieldTheory.AbelRuffini
_private.Mathlib.FieldTheory.AbelRuffini.0.solvableByRad.eq_1 : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  solvableByRad F E = sInf {s | ∀ (x : E) (n : ℕ), n ≠ 0 → x ^ n ∈ s → x ∈ s}
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.mk_add_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] {m1 m2 : M} {s1 s2 : ℕ+},
  DivisibleHull.mk m1 s1 + DivisibleHull.mk m2 s2 = DivisibleHull.mk (↑s2 • m1 + ↑s1 • m2) (s1 * s2)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instCommSemiring : {M : Type u_2} →
  {N : Type u_3} →
    {X : Type u_4} →
      {Y : Type u_5} →
        {σ : M → N} →
          [inst : SMul M X] →
            [inst_1 : Monoid N] →
              [inst_2 : CommSemiring Y] → [inst_3 : MulSemiringAction N Y] → CommSemiring (X →ₑ[σ] Y)
-- Mathlib.Control.Bitraversable.Basic
LawfulBitraversable.mk : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] [toLawfulBifunctor : LawfulBifunctor t],
  (∀ {α β : Type u} (x : t α β), bitraverse pure pure x = pure x) →
    (∀ {F G : Type u → Type u} [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
        [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β')
        (x : t α α'),
        bitraverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
          Functor.Comp.mk (bitraverse f f' <$> bitraverse g g' x)) →
      (∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : t α α'),
          bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)) →
        (∀ {F G : Type u → Type u} [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
            [LawfulApplicative G] (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β)
            (f' : α' → F β') (x : t α α'),
            (fun {α} => η.app α) (bitraverse f f' x) =
              bitraverse ((fun {α} => η.app α) ∘ f) ((fun {α} => η.app α) ∘ f') x) →
          LawfulBitraversable t
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.ex_of_dvd : ∀ {α β a b d x : ℤ}, d > 1 → d ∣ a * x + b → α * a + β * d = 1 → ∃ k, x = k * d + -α * b % d
-- Mathlib.Data.List.Dedup
List.headI_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Inhabited α] (l : List α),
  l.dedup.headI = if l.headI ∈ l.tail then l.tail.dedup.headI else l.headI
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_dist_eq_of_L2 : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (x y : WithLp 2 (α × β)), dist x y = √(dist x.fst y.fst ^ 2 + dist x.snd y.snd ^ 2)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
/-- The unit isomorphism of the
equivalence `triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ` .  -/
CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ ≅
        (CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).comp
          (CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C)
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- `Matrix.vecMul` as a bilinear map.

When `A` is non-commutative, this can be instantiated as `vecMulBilin A Aᵐᵒᵖ`  -/
Matrix.vecMulBilin : {m : Type u_2} →
  {n : Type u_3} →
    (R : Type u_4) →
      (S : Type u_5) →
        {A : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [inst_3 : Module R A] →
                  [inst_4 : Module S A] →
                    [inst_5 : SMulCommClass S R A] →
                      [SMulCommClass S A A] →
                        [IsScalarTower R A A] → [Fintype m] → (m → A) →ₗ[R] Matrix m n A →ₗ[S] n → A
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Given an action `μ` of a Type `M` on a Type `N` and a relation `r` on `N`, informally, the
`ContravariantClass` says that "if the result of the action `μ` on a pair satisfies the
relation `r`, then the initial pair satisfied the relation `r`."

More precisely, the `ContravariantClass` is a class taking two Types `M N`, together with an
"action" `μ : M → N → N` and a relation `r : N → N → Prop`.  Its unique field `elim` is the
assertion that for all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the
pair `(μ m n₁, μ m n₂)` obtained from `(n₁, n₂)` by acting upon it by `m`, then, the relation
`r` also holds for the pair `(n₁, n₂)`.

If `m : M` and `h : r (μ m n₁) (μ m n₂)`, then `ContravariantClass.elim m h : r n₁ n₂`.
 -/
ContravariantClass : (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalRingHom.rangeRestrict_surjective : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S),
  Function.Surjective ⇑f.rangeRestrict
-- Mathlib.LinearAlgebra.Dimension.Free
/-- The rank of a free module `M` over `R` is the cardinality of `ChooseBasisIndex R M`.  -/
Module.Free.rank_eq_card_chooseBasisIndex : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [StrongRankCondition R], Module.rank R M = Cardinal.mk (Module.Free.ChooseBasisIndex R M)
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousOn_finite : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] [Finite ι]
  {F : ι → X → α} {S : Set X}, EquicontinuousOn F S ↔ ∀ (i : ι), ContinuousOn (F i) S
-- Mathlib.LinearAlgebra.Span.Basic
/-- Given a nonzero element `x` of a torsion-free module `M` over a ring `R`, the natural
isomorphism from the span of `x` to `R` given by $r \cdot x \mapsto r$.  -/
LinearEquiv.coord : (R : Type u_1) →
  (M : Type u_4) →
    [inst : Ring R] →
      [IsDomain R] →
        [inst_2 : AddCommGroup M] →
          [inst_3 : Module R M] → [Module.IsTorsionFree R M] → (x : M) → x ≠ 0 → ↥(R ∙ x) ≃ₗ[R] R
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length.congr_simp : ∀ {α : Type u} (s s_1 : Stream'.Seq α) (e_s : s = s_1) (h : s.Terminates), s.length h = s_1.length ⋯
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRci : {α : Type u_1} → [DecidableEq α] → DecidableEq (Std.Rci α)
-- Mathlib.Logic.Function.Basic
Function.LeftInverse.rightInverse_of_surjective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α},
  Function.LeftInverse f g → Function.Surjective g → Function.RightInverse f g
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.equivHom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (F G : CochainComplex C ℤ) (φ : F ⟶ G),
  (CochainComplex.HomComplex.Cocycle.equivHom F G) φ = CochainComplex.HomComplex.Cocycle.ofHom φ
-- Lean.Parser.Do
Lean.Parser.Term.doSeqItem : Lean.Parser.Parser
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.denote'_mul_combine_mul_addConst_eq : ∀ (ctx : Int.Internal.Linear.Context) (p q : Int.Internal.Linear.Poly) (a b c : ℤ),
  Int.Internal.Linear.Poly.denote' ctx (((p.mul b).combine (q.mul a)).addConst c) =
    b * Int.Internal.Linear.Poly.denote ctx p + a * Int.Internal.Linear.Poly.denote ctx q + c
-- Mathlib.Analysis.InnerProductSpace.Basic
real_inner_I_smul_self : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), inner ℝ x (RCLike.I • x) = 0
-- Mathlib.CategoryTheory.Yoneda
/-- A natural isomorphism between the sections functor `(C ⥤ Type) ⥤ Type` and the co-Yoneda
embedding of a terminal functor, specifically a constant functor on a given singleton type `X`.  -/
CategoryTheory.sectionsFunctorNatIsoCoyoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : Type (max u₁ u₂)) →
      [Unique X] →
        CategoryTheory.Functor.sectionsFunctor C ≅
          CategoryTheory.coyoneda.obj (Opposite.op ((CategoryTheory.Functor.const C).obj X))
-- Mathlib.Algebra.Group.WithOne.Defs
/-- Add an extra element `1` to a type  -/
WithOne : Type u_1 → Type u_1
-- Mathlib.Algebra.Group.Opposite
AddOpposite.unop_sub : ∀ {α : Type u_1} [inst : SubNegMonoid α] (x y : αᵃᵒᵖ),
  AddOpposite.unop (x - y) = -AddOpposite.unop y + AddOpposite.unop x
-- Mathlib.RepresentationTheory.Basic
/-- The representation on `α →₀ k[G]` defined pointwise by the left regular representation.  -/
Representation.free : (k : Type u_6) →
  (G : Type u_7) →
    [inst : CommSemiring k] → [inst_1 : Monoid G] → (α : Type u_8) → Representation k G (α →₀ MonoidAlgebra k G)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get?.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β), m = m_1 → ∀ (a a_1 : α), a = a_1 → m.get? a = m_1.get? a_1
-- Init.Grind.Interactive
/-- Adds new case-splits using model-based theory combination.
 -/
Lean.Parser.Tactic.Grind.mbtc : Lean.ParserDescr
-- Mathlib.Computability.Primrec.Basic
Primrec.subtype_val_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : β → Prop}
  [inst_2 : DecidablePred p] {hp : PrimrecPred p} {f : α → Subtype p}, (Primrec fun a => ↑(f a)) ↔ Primrec f
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMonC.go : ℤ → Lean.Grind.CommRing.Mon → ℕ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Topology.UniformSpace.Separation
IndiscreteTopology.eq_top_iff_indiscrete : ∀ {α : Type u_1} [u : UniformSpace α], u = ⊤ ↔ IndiscreteTopology α
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.all_eq_false_iff_exists_mem_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  {p : α → β → Bool}, m.WF → (m.all p = false ↔ ∃ a, ∃ (h : a ∈ m), p a (Std.DHashMap.Raw.Const.get m a h) = false)
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Result.motive : Lean.Elab.Tactic.ElimApp.Result → Lean.MVarId
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.continuousOn_coordChange : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
  (a : VectorPrebundle R F E) {e e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj}
  (he : e ∈ a.pretrivializationAtlas) (he' : e' ∈ a.pretrivializationAtlas),
  ContinuousOn (a.coordChange he he') (e.baseSet ∩ e'.baseSet)
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_nontrivial_iff : ∀ {α : Type u_1} [inst : Fintype α], Finset.univ.Nontrivial ↔ Nontrivial α
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι},
  TendstoLocallyUniformlyOn F f p s ↔ TendstoLocallyUniformly (fun i x => F i ↑x) (f ∘ Subtype.val) p
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.presheafHom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.Sheaf K (Type v)}
  [inst_2 : G.IsCoverDense K] [inst_3 : G.IsLocallyFull K] (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) (X : Dᵒᵖ),
  (CategoryTheory.Functor.IsCoverDense.Types.presheafHom α).app X =
    CategoryTheory.Functor.IsCoverDense.Types.appHom α (Opposite.unop X)