mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Producers.Range
/-- Returns an iterator over the given range. This iterator will emit the elements of the range
in increasing order.
 -/
Std.Rco.iter : {α : Type u_1} → Std.Rco α → Std.Iter α
-- Mathlib.Algebra.Notation.Defs
mul_ite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Mul α] (a b c : α),
  (a * if P then b else c) = if P then a * b else a * c
-- Init.Data.Array.MinMax
/-- Returns the smallest element of the array if it is not empty, or `none` if it is empty.

Examples:
* `#[].min? = none`
* `#[4].min? = some 4`
* `#[1, 4, 2, 10, 6].min? = some 1`
 -/
Array.min? : {α : Type u_1} → [Min α] → Array α → Option α
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.opEquiv_apply : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring R), Subring.opEquiv S = S.op
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.associator.inj : ∀ {e : Lean.Expr} {f g h : Mathlib.Tactic.BicategoryLike.Mor₁} {e_1 : Lean.Expr}
  {f_1 g_1 h_1 : Mathlib.Tactic.BicategoryLike.Mor₁},
  Mathlib.Tactic.BicategoryLike.StructuralAtom.associator e f g h =
      Mathlib.Tactic.BicategoryLike.StructuralAtom.associator e_1 f_1 g_1 h_1 →
    e = e_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1
-- Mathlib.Algebra.Group.Commute.Basic
Commute.mul_div_mul_comm : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b c d : G},
  Commute c d → Commute b c⁻¹ → a * b / (c * d) = a / c * (b / d)
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  M.equivMonComonUnitIsoAppXAux.inv = CategoryTheory.CategoryStruct.id M.X.X
-- Mathlib.RingTheory.Bialgebra.TensorProduct
/-- Representations of `a` and `b` yield a representation of `a ⊗ b`.  -/
Coalgebra.Repr.tmul : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {ι : Type u_4} →
        {κ : Type u_5} →
          [inst : CommSemiring R] →
            [inst_1 : Semiring A] →
              [inst_2 : Bialgebra R A] →
                [inst_3 : Semiring B] →
                  [inst_4 : Bialgebra R B] →
                    {a : A} →
                      {b : B} → Coalgebra.Repr R a ι → Coalgebra.Repr R b κ → Coalgebra.Repr R (a ⊗ₜ[R] b) (ι × κ)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.pushforward_I : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {D : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D}
  {S : CategoryTheory.Sheaf K RingCat} [inst_4 : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat]
  [inst_5 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_6 : ∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C)
  [inst_7 : G.IsContinuous K J] [inst_8 : G.IsCocontinuous K J]
  (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R)
  (η : (SheafOfModules.pushforward φ).obj (SheafOfModules.unit R) ≅ SheafOfModules.unit S)
  [inst_9 : ∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))]
  (h :
    ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
      CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂,
          max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
        (SheafOfModules.pushforward
          (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ)))
  {M : SheafOfModules R} (P : M.QuasicoherentData),
  (SheafOfModules.QuasicoherentData.pushforward G φ η h P).I = ((X : D) × (i : P.I) × (G.obj X ⟶ P.X i))
-- Init.Data.Vector.Zip
Vector.unzip_zip_right : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {as : Vector α n} {bs : Vector β n}, (as.zip bs).unzip.2 = bs
-- Mathlib.FieldTheory.KummerPolynomial
ne_zero_of_irreducible_X_pow_sub_C' : ∀ {K : Type u} [inst : Field K] {n : ℕ}, n ≠ 1 → ∀ {a : K}, Irreducible (Polynomial.X ^ n - Polynomial.C a) → a ≠ 0
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.of : {G : Type u_1} →
  {inst : CategoryTheory.Groupoid G} →
    [self : IsFreeGroupoid G] →
      {a b : IsFreeGroupoid.Generators G} →
        (a ⟶ b) →
          ((have this := a;
            this) ⟶
            b)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.empty_not_isBase : ∀ {α : Type u_1} {M : Matroid α} [h : M.RankPos], ¬M.IsBase ∅
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
/-- If `a : A` is not a unit, then some character takes the value zero at `a`. This is equivalent
to `gelfandTransform ℂ A a` takes the value zero at some character.  -/
WeakDual.CharacterSpace.exists_apply_eq_zero : ∀ {A : Type u_1} [inst : NormedCommRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] {a : A},
  ¬IsUnit a → ∃ f, f a = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.ext_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} {K K' : CategoryTheory.Limits.Multicofork I} (e : K.pt ≅ K'.pt)
  (h :
    autoParam (∀ (i : J.R), CategoryTheory.CategoryStruct.comp (K.π i) e.hom = K'.π i)
      CategoryTheory.Limits.Multicofork.ext._auto_1),
  (CategoryTheory.Limits.Multicofork.ext e h).inv.hom = e.inv
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.comm_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (f : K ⟶ L) (i₁ i₁' : I₁) (i₂ : I₂),
  CategoryTheory.CategoryStruct.comp ((f.f i₁).f i₂) ((L.d i₁ i₁').f i₂) =
    CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) ((f.f i₁').f i₂)
-- Lean.Message
/-- Set of message kinds that have been added to the log.
For example, we have the kind `unsafe.exponentiation.warning` for warning messages associated with
the configuration option `exponentiation.threshold`.
We don't produce a warning if the kind is already in the following set.
 -/
Lean.MessageLog.loggedKinds : Lean.MessageLog → Lean.NameSet
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] (ι : Type w)
  [inst_2 : CategoryTheory.Limits.HasFiniteProducts C] [inst_3 : Finite ι] (X : C) (j : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).inv
      (CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j) =
    CategoryTheory.Limits.Pi.π (fun x => X) j
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- Interpret `f : α → β` as an element of `C(α, β)₀`, falling back to the default value
`default : C(α, β)₀` if `f` is not continuous or does not map `0` to `0`.
This is mainly intended to be used for `C(α, β)₀`-valued integration. For example, if a family of
functions `f : ι → α → β` satisfies that `f i` is continuous and maps `0` to `0` for almost every
`i`, you can write the `C(α, β)₀`-valued integral "`∫ i, f i`" as
`∫ i, ContinuousMapZero.mkD (f i) 0`.
 -/
ContinuousMapZero.mkD : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero R] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] → [inst_3 : Zero X] → (X → R) → ContinuousMapZero X R → ContinuousMapZero X R
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toAlgHomHom_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (e : A ≃ₐ[R] A),
  (AlgEquiv.toAlgHomHom R A) e = ↑e
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.decidableIsCompl : {α : Type u_1} → {s t : Finset α} → [inst : Fintype α] → [DecidableEq α] → Decidable (IsCompl s t)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.instOfIsMultiplicativeOfRespectsIsoOfIsStableUnderFilteredColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.IsMultiplicative]
  [W.RespectsIso] [CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.{w, w, v, u} W],
  W.IsStableUnderTransfiniteComposition
-- Init.Data.Vector.OfFn
_private.Init.Data.Vector.OfFn.0.Vector.ofFnM.go.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] (f : Fin n → m α) (i : ℕ) (h' : i ≤ n)
  (acc : Array α) (w : acc.size = i),
  Vector.ofFnM.go✝ f i h' acc w =
    if h : i < n then do
      let __do_lift ← f ⟨i, h⟩
      Vector.ofFnM.go✝ f (i + 1) ⋯ (acc.push __do_lift) ⋯
    else pure (Vector.mk acc ⋯)
-- Mathlib.Data.Set.Lattice
Set.inter_iInter_nat_succ : ∀ {α : Type u_1} (u : ℕ → Set α), u 0 ∩ ⋂ i, u (i + 1) = ⋂ i, u i
-- Mathlib.AlgebraicGeometry.Scheme
/-- `PrimeSpectrum R` with the inclusion order is order isomorphic to the dual of `Spec R`.  -/
AlgebraicGeometry.primeSpectrumOrderIsoSpec : (R : Type u) → [inst : CommRing R] → PrimeSpectrum R ≃o (↥(AlgebraicGeometry.Spec (CommRingCat.of R)))ᵒᵈ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.comp_mapGrp_mul_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  (A : CategoryTheory.Grp C) {Z : E} (h : ((F.comp G).mapGrp.obj A).X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) A.X A.X)
        (G.map (F.map CategoryTheory.MonObj.mul)))
      h
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.ae_isProbabilityMeasure : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ι → Type u_8} {mβ : (i : ι) → MeasurableSpace (β i)}
  {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α}
  {f : (x : ι) → Ω → β x},
  ProbabilityTheory.Kernel.iIndepFun f κ μ → ∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)
-- Mathlib.Algebra.Order.Module.Synonym
Lex.instModule : {α : Type u_1} → {β : Type u_2} → [inst : Semiring α] → [inst_1 : AddCommMonoid β] → [Module α β] → Module (Lex α) β
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.dp_def : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ)
  (m : M), DividedPowerAlgebra.dp R n m = ↑(MvPolynomial.X (n, m))
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addRightCancelMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddRightCancelMonoid (f i)],
  Pi.addRightCancelMonoid =
    { toAddSemigroup := Pi.addRightCancelSemigroup.toAddSemigroup, toZero := Pi.addMonoid.toZero, zero_add := ⋯,
      add_zero := ⋯, toNSMul := Pi.addMonoid.toNSMul, nsmul_zero := ⋯, nsmul_succ := ⋯, toIsRightCancelAdd := ⋯ }
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.toList_eq_if_roc : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α],
  r.toList =
    have init := Std.PRange.UpwardEnumerable.least;
    if init ≤ r.upper then init :: (init<...=r.upper).toList else []
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
fderivWithin_cosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x →
    UniqueDiffWithinAt ℝ s x → fderivWithin ℝ (fun x => Real.cosh (f x)) s x = Real.sinh (f x) • fderivWithin ℝ f s x
-- Init.Data.List.Nat.Modify
List.modify_eraseIdx_of_ge : ∀ {α : Type u_1} (f : α → α) (i j : ℕ) (l : List α), j ≥ i → (l.eraseIdx i).modify j f = (l.modify (j + 1) f).eraseIdx i
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- The exponential map as a function `M → Mᵐ⁰`.  -/
WithZero.exp : {M : Type u_4} → M → WithZero (Multiplicative M)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_of_pos_of_le : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightStrictMono α] {a b c : α},
  0 < a → b ≤ c → b < a + c
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_pos_real' : ∀ {x : ENNReal}, 0 < x.toReal → x.log = ↑(Real.log x.toReal)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
CategoryTheory.Localization.essSurj_mapComposableArrows : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] (n : ℕ),
  (L.mapComposableArrows n).EssSurj
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [toSurjectiveOnStalks : AlgebraicGeometry.SurjectiveOnStalks f],
  Topology.IsClosedEmbedding ⇑f → AlgebraicGeometry.IsClosedImmersion f
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.doubleDualEmb_eq_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] {a : α} [Finite α], AddChar.doubleDualEmb a = 0 ↔ a = 0
-- Init.Data.Array.Lemmas
Array.map_filterMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ} {xs : Array α},
  Array.map g (Array.filterMap f xs) = Array.filterMap (fun x => Option.map g (f x)) xs
-- Mathlib.Data.Fin.Tuple.Curry
/-- Curry all the arguments of `Function.OfArity α β n` to get a function from a tuple.  -/
Function.OfArity.curry : {α β : Type u} → {n : ℕ} → ((Fin n → α) → β) → Function.OfArity α β n
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of `AffineSubspace.isConnected_setOfPred_wOppSide`. -/
AffineSubspace.isConnected_setOf_wOppSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} (x : P),
  (↑s).Nonempty → IsConnected {y | s.WOppSide x y}
-- Lean.Environment
Lean.Environment.instInhabitedVisibility : Inhabited Lean.Environment.Visibility
-- Mathlib.NumberTheory.Pell
/-- If `(x, y)` is a solution with `x` and `y` positive, then the `y` component of any power
has the same sign as the exponent.  -/
Pell.Solution₁.sign_y_zpow_eq_sign_of_x_pos_of_y_pos : ∀ {d : ℤ} {a : Pell.Solution₁ d}, 0 < a.x → 0 < a.y → ∀ (n : ℤ), (a ^ n).y.sign = n.sign
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwPos.mk : Lean.Name → Lean.Expr → Option Bool → Mathlib.Tactic.ClickSuggestions.GrwPos
-- Batteries.Data.List.Basic
List.replaceF.eq_2 : ∀ {α : Type u_1} (f : α → Option α) (a : α) (l : List α),
  List.replaceF f (a :: l) =
    match f a with
    | none => a :: List.replaceF f l
    | some a => a :: l
-- Mathlib.Data.Set.Card
Set.two_lt_ncard : ∀ {α : Type u_1} {s : Set α},
  autoParam s.Finite Set.two_lt_ncard._auto_1 → (2 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c)
-- Mathlib.Data.Nat.Factorization.Defs
Nat.ordProj_dvd_ordProj_iff_dvd : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → ((∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ a ∣ b)
-- Mathlib.Data.List.AList
AList.insertRec.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {C : AList β → Sort u_1} (H0 : C ∅)
  (IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (AList.insert a b l)) (nodupKeys : [].NodupKeys),
  AList.insertRec H0 IH { entries := [], nodupKeys := nodupKeys } = H0
-- Lean.Meta.Tactic.Grind.Types
/-- Performs (expensive) satisfiability checks in all registered solvers,
and returns the solver ids that made progress.
 -/
Lean.Meta.Grind.Solvers.check? : Lean.Meta.Grind.GoalM (Option (Array ℕ))
-- Init.Data.String.Lemmas.Basic
String.Slice.sliceTo_sliceFrom : ∀ {s : String.Slice} {pos : s.Pos} {pos' : (s.sliceFrom pos).Pos},
  (s.sliceFrom pos).sliceTo pos' = s.slice pos (String.Slice.Pos.ofSliceFrom pos') ⋯
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- If a linear map is injective on the span of a family of linearly independent vectors, then
the family stays linearly independent after composing with the linear map.
See `LinearIndependent.map` for the version with `Set.InjOn` replaced by `Disjoint`
when working over a ring.  -/
LinearIndependent.map_injOn : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'],
  LinearIndependent R v →
    ∀ (f : M →ₗ[R] M'), Set.InjOn ⇑f ↑(Submodule.span R (Set.range v)) → LinearIndependent R (⇑f ∘ v)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- Coercion to a function as an `AddMonoidHom`. Similar to `ContinuousMap.coeFnAddMonoidHom`.  -/
ContinuousMapZero.coeFnAddMonoidHom : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] →
          [inst_3 : CommSemiring R] → [inst_4 : IsTopologicalSemiring R] → ContinuousMapZero X R →+ X → R
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
NumberField.InfiniteAdeleRing.instNontrivial : ∀ (K : Type u_1) [inst : Field K] [NumberField K], Nontrivial (NumberField.InfiniteAdeleRing K)
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sum'_isBase_iff : ∀ {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {B : Set (ι × α)},
  (Matroid.sum' M).IsBase B ↔ ∀ (i : ι), (M i).IsBase (Prod.mk i ⁻¹' B)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- Coercion is an `AddMonoidHom`.  -/
MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → MeasureTheory.FiniteMeasure Ω →+ MeasureTheory.Measure Ω
-- Mathlib.Tactic.Variable
_private.Mathlib.Tactic.Variable.0.Mathlib.Command.Variable.completeBinders'.isVariableAlias : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Data.List.Basic
List.doubleton_eq : ∀ {α : Type u} [inst : DecidableEq α] {x y : α}, x ≠ y → {x, y} = [x, y]
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- Multiply a modular form of weight `k - 12` by the discriminant to get a cusp form of
weight `k`. Built directly as a `CuspForm` via `CuspForm.mulModularForm`.  -/
CuspForm.ofMulDiscriminant : {k : ℤ} →
  ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12) → CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {v : β}, (t.insert k v).maxKey! = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denoteAsIntModule.go : {α : Type u_1} → [Lean.Grind.CommRing α] → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Mon → α → α
-- Std.Data.DTreeMap.Raw.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.DTreeMap.Raw.Const.ofArray : {α : Type u} →
  {β : Type v} →
    Array (α × β) →
      (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.Const.ofArray._auto_1) → Std.DTreeMap.Raw α (fun x => β) cmp
-- Mathlib.Analysis.Normed.Group.Uniform
antilipschitzWith_iff_exists_mul_le_norm : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
  [inst_2 : FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] {f : 𝓕},
  (∃ K, AntilipschitzWith K ⇑f) ↔ ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ ‖f x‖
-- Mathlib.Data.Int.Range
Int.mem_range_iff : ∀ {m n r : ℤ}, r ∈ m.range n ↔ m ≤ r ∧ r < n
-- Mathlib.Analysis.Convex.Gauge
setOfPred_gauge_lt_eq : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Absorbent ℝ s → ∀ (a : ℝ), {x | gauge s x < a} = ⋃ r ∈ Set.Ioo 0 a, r • s
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.inter : ∀ {α : Type u_1} [inst : LE α] {s t : Set α}, IsLowerSet s → IsLowerSet t → IsLowerSet (s ∩ t)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolAux.range : {Self : Type} → Lean.Lsp.DocumentSymbolAux Self → Lean.Lsp.Range
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.OptionT.bind.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.Homotopy.Path
/-- The setoid on `Path`s defined by the equivalence relation `Path.Homotopic`. That is, two paths are
equivalent if there is a `Homotopy` between them.
 -/
Path.Homotopic.setoid : {X : Type u} → [inst : TopologicalSpace X] → (x₀ x₁ : X) → Setoid (Path x₀ x₁)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHomId : {F : Type u_3} →
  {R : Type u_4} →
    [inst : Monoid R] →
      {A : Type u_5} →
        {B : Type u_6} →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : DistribMulAction R A] →
              [inst_3 : NonUnitalNonAssocSemiring B] →
                [inst_4 : DistribMulAction R B] →
                  [inst_5 : FunLike F A B] → [NonUnitalAlgHomClass F R A B] → CoeTC F (A →ₙₐ[R] B)
-- Batteries.Data.Fin.Coding
Fin.encodeSubtype_zero_pos : ∀ {n : ℕ} {P : Fin (n + 1) → Prop} [inst : DecidablePred P] (h₀ : P 0), Fin.encodeSubtype P ⟨0, h₀⟩ = ⟨0, ⋯⟩
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- The *strong dual* of a topological vector space `M` over a ring `R`. This is the space of
continuous linear functionals and is equipped with the topology of uniform convergence
on bounded subsets. `StrongDual R M` is an abbreviation for `M →L[R] R`.  -/
StrongDual : (R : Type u_1) →
  [inst : Semiring R] →
    [TopologicalSpace R] →
      (M : Type u_2) → [TopologicalSpace M] → [inst_3 : AddCommMonoid M] → [Module R M] → Type (max u_1 u_2)
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.sub_sub_cancel_left : ∀ {α : Type u} [inst : SubtractionCommMonoid α] {a b : α}, IsAddUnit a → a - b - a = -b
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.instTopologicalSpace : {G : Type u_1} → [TopologicalSpace G] → [inst : Group G] → (N : Subgroup G) → TopologicalSpace (G ⧸ N)
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.map.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂],
  HomologicalComplex₂.total.map φ c₁₂ =
    { f := CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂), comm' := ⋯ }
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.instEssentiallySmallOpposite : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C],
  CategoryTheory.EssentiallySmall.{w, v, u} Cᵒᵖ
-- Init.MetaTypes
Lean.Meta.DSimp.instBEqConfig : BEq Lean.Meta.DSimp.Config
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.mapId'.eq_1 : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {b : B} (f : b ⟶ b) (hf : f = CategoryTheory.CategoryStruct.id b),
  F.mapId' f hf = CategoryTheory.CategoryStruct.comp (F.mapId b) (F.map₂ (CategoryTheory.eqToHom ⋯))