mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Internalize
/-- Returns `true` if we can ignore `ext` for functions occurring as arguments of a `declName`-application.  -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.extParentsToIgnore : Lean.Name → Bool
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal.0.AugmentedSimplexCategory.leftUnitor.match_1.splitter : (motive : AugmentedSimplexCategory → Sort u_1) →
  (x : AugmentedSimplexCategory) →
    ((a : SimplexCategory) → motive (CategoryTheory.WithInitial.of a)) →
      (Unit → motive CategoryTheory.WithInitial.star) → motive x
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isTopologicalBasis_basic_opens : ∀ {R : Type u} [inst : CommSemiring R],
  TopologicalSpace.IsTopologicalBasis (Set.range fun r => ↑(PrimeSpectrum.basicOpen r))
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation of a product equals the product of the valuations.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x y : R),
  v.intValuationDef (x * y) = v.intValuationDef x * v.intValuationDef y
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.map_sub : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x y : E), e (x - y) = e x - e y
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.rightUnitorImpl_inv_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  X.rightUnitorImpl.inv.F =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
-- Lean.Elab.MutualDef
/-- Elaborates only the declaration view headers. We have to elaborate the headers first because we
support mutually recursive declarations in Lean 4.
 -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabHeaders : Array Lean.Elab.DefView →
  Array Lean.Elab.ExpandDeclIdResult →
    Array (IO.Promise (Option Lean.Elab.BodyProcessedSnapshot)) →
      Array (IO.Promise Lean.Elab.Tactic.TacticParsedSnapshot) → Lean.Elab.TermElabM (Array Lean.Elab.DefViewElabHeader)
-- Lean.Meta.Tactic.Grind.EMatchAction
Lean.Meta.Grind.Action.instantiate' : Lean.Meta.Grind.Action
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.setIntegral_condExpIndSMul : ∀ {α : Type u_1} {G' : Type u_6} [inst : NormedAddCommGroup G'] [inst_1 : NormedSpace ℝ G'] [CompleteSpace G']
  {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} {hm : m ≤ m0},
  MeasurableSet s →
    ∀ (ht : MeasurableSet t),
      μ s ≠ ⊤ →
        ∀ (hμt : μ t ≠ ⊤) (x : G'),
          ∫ (a : α) in s, ↑↑(MeasureTheory.condExpIndSMul hm ht hμt x) a ∂μ = μ.real (t ∩ s) • x
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.descFunLift.eq_6 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (s : CategoryTheory.Limits.Cocone F) (x_1 y : RingCat.Colimits.Prequotient F),
  RingCat.Colimits.descFunLift F s (x_1.mul y) =
    RingCat.Colimits.descFunLift F s x_1 * RingCat.Colimits.descFunLift F s y
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- The multiplicative equivalence between the `valueGroup` of the valuation on `WithVal v`
and the valuation `v`.  -/
WithVal.valueGroupEquiv : {Γ₀ : Type u_2} →
  [inst : LinearOrderedCommGroupWithZero Γ₀] →
    {R : Type u_3} →
      [inst_1 : Ring R] →
        (v : Valuation R Γ₀) →
          ↥(MonoidWithZeroHom.ofClass Valued.v).valueGroup ≃* ↥(MonoidWithZeroHom.ofClass v).valueGroup
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_apply_eq : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] (d : n → α) (i : n), Matrix.diagonal d i i = d i
-- Init.Data.SInt.Lemmas
Int64.le_maxValue : ∀ (a : Int64), a ≤ Int64.maxValue
-- Mathlib.Algebra.Torsor.Defs
/-- A `Torsor G P` gives a structure to the nonempty type `P`,
acted on by a `Group G` with a transitive and free action given
by the `•` operation and a corresponding division given by the
`/ₛ` operation.  -/
Torsor : (G : outParam (Type u_1)) → Type u_2 → [Group G] → Type (max u_1 u_2)
-- Mathlib.RingTheory.FiniteType
AlgHom.FiniteType.of_comp_finiteType : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : CommRing C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  {f : A →ₐ[R] B} {g : B →ₐ[R] C}, (g.comp f).FiniteType → g.FiniteType
-- Mathlib.Algebra.GroupWithZero.Units.Basic
IsUnit.ne_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [Nontrivial M₀] {a : M₀}, IsUnit a → a ≠ 0
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.associatorNatIsoRightCat_hom_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) (X : c ⟶ d),
  (CategoryTheory.Bicategory.associatorNatIsoRightCat f g d).hom.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator f g X).hom
-- Mathlib.CategoryTheory.Whiskering
/-- The obvious functor
`(C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (C₃ ⥤ D₃) ⥤ (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E)`.  -/
CategoryTheory.Functor.whiskeringLeft₃ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_4} →
        {D₂ : Type u_5} →
          {D₃ : Type u_6} →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] →
                        (E : Type u_7) →
                          [inst_6 : CategoryTheory.Category.{v_7, u_7} E] →
                            CategoryTheory.Functor (CategoryTheory.Functor C₁ D₁)
                              (CategoryTheory.Functor (CategoryTheory.Functor C₂ D₂)
                                (CategoryTheory.Functor (CategoryTheory.Functor C₃ D₃)
                                  (CategoryTheory.Functor
                                    (CategoryTheory.Functor D₁
                                      (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E)))
                                    (CategoryTheory.Functor C₁
                                      (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))))))
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
summable_prod_mul_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜] (k : ℕ) {r : 𝕜},
  ‖r‖ < 1 → Summable fun c => ↑↑c.2 ^ k * r ^ (↑c.1 * ↑c.2)
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.IsSeparated.subset : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s t : Set X} {ε : ENNReal},
  s ⊆ t → Metric.IsSeparated ε t → Metric.IsSeparated ε s
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
ContinuousLinearEquiv.unitsEquivAut.congr_simp : ∀ (R : Type u_1) [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : ContinuousMul R],
  ContinuousLinearEquiv.unitsEquivAut R = ContinuousLinearEquiv.unitsEquivAut R
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_iInf : ∀ {ι : Sort u_3} [Nonempty ι] (f : ι → NNReal), ↑(iInf f) = ⨅ a, ↑(f a)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_sub_of_right_eq_zero : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R}, v y = 0 → v (x - y) = v x
-- Mathlib.Order.Grade
grade_ofDual : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : Preorder α] [inst_2 : GradeOrder 𝕆 α] (a : αᵒᵈ),
  grade 𝕆 (OrderDual.ofDual a) = OrderDual.ofDual (grade 𝕆ᵒᵈ a)
-- Mathlib.RingTheory.WittVector.Identities
WittVector.FractionRing.p_nonzero : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] [Nontrivial R] [CharP R p], ↑p ≠ 0
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.pairingIn_threeShortAddLong_right : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι),
  P.pairingIn ℤ i (RootPairing.EmbeddedG2.threeShortAddLong P) =
    P.pairingIn ℤ i (RootPairing.EmbeddedG2.short P) + P.pairingIn ℤ i (RootPairing.EmbeddedG2.long P)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.eventually_nonpos : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] {u v : α → β}
  {l : Filter α} [ClosedIicTopology β],
  Asymptotics.IsEquivalent l u v → (∀ᶠ (t : α) in l, v t ≤ 0) → ∀ᶠ (x : α) in l, u x ≤ 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.length_nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.length = 0
-- Init.Grind.ToInt
Lean.Grind.ToInt.Mod.mk : ∀ {α : Type u} [inst : Mod α] {I : outParam Lean.Grind.IntInterval} [inst_1 : Lean.Grind.ToInt α I],
  (∀ (x y : α), ↑(x % y) = ↑x % ↑y) → Lean.Grind.ToInt.Mod α I
-- Init.Data.String.Lemmas.TakeDrop
String.Slice.drop_eq_sliceFrom : ∀ {s : String.Slice} {n : ℕ}, s.drop n = s.sliceFrom (s.startPos.nextn n)
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_fromBlocks : ∀ {X : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace R] {A : X → Matrix n l R} {B : X → Matrix n m R} {C : X → Matrix p l R}
  {D : X → Matrix p m R},
  Continuous A →
    Continuous B → Continuous C → Continuous D → Continuous fun x => Matrix.fromBlocks (A x) (B x) (C x) (D x)
-- Mathlib.Analysis.LocallyConvex.PointwiseConvergence
PointwiseConvergenceCLM.tendsto_nhds_atTop : ∀ {α : Type u_1} {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂}
  {E : Type u_7} {F : Type u_8} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜₂ F] [inst_7 : SemilatticeSup α] [Nonempty α]
  (u : α → E →SLₚₜ[σ] F) (y₀ : E →SLₚₜ[σ] F),
  Filter.Tendsto u Filter.atTop (nhds y₀) ↔ ∀ (x : E) (ε : ℝ), 0 < ε → ∃ k₀, ∀ (k : α), k₀ ≤ k → ‖(u k) x - y₀ x‖ < ε
-- Mathlib.Data.Stream.Init
Stream'.append_take : ∀ {α : Type u} (n : ℕ) (x : List α) (a : Stream' α), x ++ Stream'.take n a = Stream'.take (x.length + n) (x ++ₛ a)
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
OrderDual.instSemigroupWithZero : {α : Type u_1} → [SemigroupWithZero α] → SemigroupWithZero αᵒᵈ
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_unique : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G}
  [inst_6 : Unique X] [CompleteSpace G], ∫ᵛ (x : X), f x ∂[B; μ] = (B (f default)) (μ Set.univ)
-- Mathlib.Data.Multiset.MapFold
Multiset.foldr_cons : ∀ {α : Type u_1} {β : Type v} (f : α → β → β) [inst : LeftCommutative f] (b : β) (a : α) (s : Multiset α),
  Multiset.foldr f b (a ::ₘ s) = f a (Multiset.foldr f b s)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.instFaithfulCompPre : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (S : D) [F.Faithful], (CategoryTheory.CostructuredArrow.pre F G S).Faithful
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Empty.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m β] →
      {it : Std.IterM m β} →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.ofCocone_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type v} [inst_1 : CategoryTheory.SmallCategory I]
  [inst_2 : CategoryTheory.IsFiltered I] {F : CategoryTheory.Functor I C}
  (c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)) (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.Limits.IndObjectPresentation.ofCocone c hc).ι = c.ι
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedCancelVAdd.le_of_vadd_le_vadd_right : ∀ {G : Type u_3} {P : Type u_4} {inst : LE G} {inst_1 : LE P} {inst_2 : VAdd G P} [self : IsOrderedCancelVAdd G P]
  (a b : G) (c : P), a +ᵥ c ≤ b +ᵥ c → a ≤ b
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.uniformSpace : {α : Type u_1} → [inst : UniformSpace α] → UniformSpace (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
ContinuousMultilinearMap.iteratedFDeriv_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) (n : ℕ),
  iteratedFDeriv 𝕜 n ⇑f = f.iteratedFDeriv n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Over.coprodObj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] {A : C}
  (a g : CategoryTheory.Over A),
  a.coprodObj.obj g = CategoryTheory.Over.mk (CategoryTheory.Limits.coprod.desc a.hom g.hom)
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypic.linearEquiv_finsupp : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  [Nontrivial M], IsIsotypic R M → ∃ ι, ∃ (_ : Nonempty ι), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] ι →₀ ↥S)
-- Mathlib.Algebra.Homology.Augment
CochainComplex.augmentTruncate_hom_f_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : CochainComplex V ℕ), C.augmentTruncate.hom.f 0 = CategoryTheory.CategoryStruct.id (C.X 0)
-- Lean.Level
Lean.Level.updateIMax! : Lean.Level → Lean.Level → Lean.Level → Lean.Level
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.computeFixedIndexBitMask.go : ℕ → Array Lean.Expr → ℕ → IO.Ref (Array Bool) → List Lean.Constructor → Lean.MetaM (Array Bool)
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_mul_cancel_of_tmod_eq_zero : ∀ {a b : ℤ}, a.tmod b = 0 → a.tdiv b * b = a
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_const_sub_id' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (c : 𝕜), (deriv fun x => c - x) = fun x => -1
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.max_eq_zero : ∀ {a b : Ordinal.{u_1}}, max a b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), f.toFun = ⇑f
-- Init.Data.String.Defs
String.size_toByteArray : ∀ {s : String}, s.toByteArray.size = s.utf8ByteSize
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- If `M / R` and `M' / R'` are modules, `i : R' → R` is an injective map
non-zero elements, `j : M →+ M'` is an injective monoid homomorphism, such that the scalar
multiplications on `M` and `M'` are compatible, then the rank of `M / R` is smaller than or equal to
the rank of `M' / R'`. As a special case, taking `R = R'` it is
`LinearMap.lift_rank_le_of_injective`.  -/
lift_rank_le_of_injective_injectiveₛ : ∀ {R : Type u} {R' : Type u'} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M'] [inst_5 : Module R' M'] (i : R' → R)
  (j : M →+ M'),
  Function.Injective i →
    Function.Injective ⇑j →
      (∀ (r : R') (m : M), j (i r • m) = r • j m) →
        Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R' M')
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Icc_succ_left_eq_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] {a b : α},
  a ≤ b → insert a (Finset.Icc (Order.succ a) b) = Finset.Icc a b
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- If `‖pₙ‖ rⁿ` is bounded in `n`, then the radius of `p` is at least `r`.  -/
FormalMultilinearSeries.le_radius_of_bound_nnreal : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (C : NNReal) {r : NNReal}, (∀ (n : ℕ), ‖p n‖₊ * r ^ n ≤ C) → ↑r ≤ p.radius
-- Mathlib.Logic.Function.Basic
/-- If the co-domain `β` of an injective function `f : α → β` has decidable equality, then
the domain `α` also has decidable equality.  -/
Function.Injective.decidableEq : {α : Sort u_1} → {β : Sort u_2} → {f : α → β} → [DecidableEq β] → Function.Injective f → DecidableEq α
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_mkNormedAddGroupHom : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (f : V₁ →+ V₂)
  (C : ℝ) (hC : ∀ (v : V₁), ‖f v‖ ≤ C * ‖v‖), ⇑(f.mkNormedAddGroupHom C hC) = ⇑f
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.findAux_s : ∀ {self : Batteries.UnionFind} {x : Fin self.size},
  (self.findAux x).s =
    if self.arr[↑x].parent = ↑x then self.arr
    else (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.verticalIntegral_norm_le : ∀ {b : ℂ},
  0 < b.re →
    ∀ (c : ℝ) {T : ℝ},
      0 ≤ T →
        ‖GaussianFourier.verticalIntegral b c T‖ ≤
          2 * |c| * Real.exp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.re_inv : ∀ {K : Type u_1} [inst : Field K] {a b : K} (z : QuadraticAlgebra K a b),
  z⁻¹.re = (QuadraticAlgebra.norm z)⁻¹ * (z.re + b * z.im)
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.hasLimits : CategoryTheory.Limits.HasLimits GrpCat
-- Mathlib.Logic.Relator
Relator.BiTotal.symm : ∀ {α : Type u_1} {β : Type u_2} {r₁₂ : α → β → Prop} {r₂₁ : β → α → Prop},
  (∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) → Relator.BiTotal r₁₂ → Relator.BiTotal r₂₁
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (d : D) (c : Cᴹᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c.unmop d
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- If `m u = ∞` for any set `u` that has nonempty intersection both with `s` and `t`, then
`μ (s ∪ t) = μ s + μ t`, where `μ = MeasureTheory.OuterMeasure.ofFunction m m_empty`.

E.g., if `α` is an (e)metric space and `m u = ∞` on any set of diameter `≥ r`, then this lemma
implies that `μ (s ∪ t) = μ s + μ t` on any two sets such that `r ≤ edist x y` for all `x ∈ s`
and `y ∈ t`.  -/
MeasureTheory.OuterMeasure.ofFunction_union_of_top_of_nonempty_inter : ∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {s t : Set α},
  (∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤) →
    (MeasureTheory.OuterMeasure.ofFunction m m_empty) (s ∪ t) =
      (MeasureTheory.OuterMeasure.ofFunction m m_empty) s + (MeasureTheory.OuterMeasure.ofFunction m m_empty) t
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.instIsMultiplicativeInnerAnodyneExtensions : SSet.innerAnodyneExtensions.IsMultiplicative
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.invalidExtMsg : String
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.rowLen_anti : ∀ (μ : YoungDiagram) (i1 i2 : ℕ), i1 ≤ i2 → μ.rowLen i2 ≤ μ.rowLen i1
-- Mathlib.Order.Defs.Unbundled
LowerSet.mk.inj : ∀ {α : Type u_1} {inst : LE α} {carrier : Set α} {lower' : IsLowerSet carrier} {carrier_1 : Set α}
  {lower'_1 : IsLowerSet carrier_1},
  { carrier := carrier, lower' := lower' } = { carrier := carrier_1, lower' := lower'_1 } → carrier = carrier_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a b : α}, cmp a b = Ordering.eq → Std.ExtDTreeMap.Const.get? t a = Std.ExtDTreeMap.Const.get? t b
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.mk.injEq : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra S S']
  (val : ι → P'.Ring) (aeval_val : ∀ (i : ι), (MvPolynomial.aeval P'.val) (val i) = (algebraMap S S') (P.val i))
  (val_1 : ι → P'.Ring) (aeval_val_1 : ∀ (i : ι), (MvPolynomial.aeval P'.val) (val_1 i) = (algebraMap S S') (P.val i)),
  ({ val := val, aeval_val := aeval_val } = { val := val_1, aeval_val := aeval_val_1 }) = (val = val_1)
-- Mathlib.GroupTheory.Index
AddSubgroup.index_ne_zero_of_finite : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} [hH : Finite (G ⧸ H)], H.index ≠ 0
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The lower topology is the topology generated by the complements of the left-closed right-infinite
intervals.
 -/
Topology.IsLower : (α : Type u_3) → [t : TopologicalSpace α] → [Preorder α] → Prop
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_map_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w))
  {X Y : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)} (f : X ⟶ Y),
  ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.map f) = f.base
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.fvar.sizeOf_spec : ∀ (a : Lean.FVarId) (a_1 : ℕ), sizeOf (Lean.Meta.DiscrTree.Key.fvar a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Topology.Algebra.IsOpenUnits
isOpenUnits_iff : ∀ (M : Type u_1) [inst : Monoid M] [inst_1 : TopologicalSpace M], IsOpenUnits M ↔ Topology.IsOpenEmbedding Units.val
-- Mathlib.Data.Finset.Image
Finset.coe_image_subset_range : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α}, ↑(Finset.image f s) ⊆ Set.range f