mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- Note that the identity is a cycle on any subsingleton set, but not a cycle.  -/
Equiv.Perm.IsCycleOn.subtypePerm : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α} (hf : f.IsCycleOn s), (f.subtypePerm ⋯).IsCycleOn Set.univ
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piFinTwo_apply : ∀ (α : Fin 2 → Type u_8) [inst : (i : Fin 2) → MeasurableSpace (α i)],
  ⇑(MeasurableEquiv.piFinTwo α) = fun f => (f 0, f 1)
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.liftRel_bind : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Stream'.WSeq α}
  {s2 : Stream'.WSeq β} {f1 : α → Stream'.WSeq γ} {f2 : β → Stream'.WSeq δ},
  Stream'.WSeq.LiftRel R s1 s2 →
    (∀ {a : α} {b : β}, R a b → Stream'.WSeq.LiftRel S (f1 a) (f2 b)) → Stream'.WSeq.LiftRel S (s1.bind f1) (s2.bind f2)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.Stmt.write.injEq : ∀ {Γ : Type u_1} (a a_1 : Γ), (Turing.TM0.Stmt.write a = Turing.TM0.Stmt.write a_1) = (a = a_1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α},
  Std.DTreeMap.Const.get! (t₁ ∩ t₂) k = if k ∈ t₂ then Std.DTreeMap.Const.get! t₁ k else default
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
/-- A multicoequalizer diagram in a complete lattice `T` consists of families of elements
`u : ι → T`, `v : ι → ι → T`, and an element `x : T` such that `x` is the supremum of `u`,
and for any `i` and `j`, `v i j` is the minimum of `u i` and `u j`.  -/
CompleteLattice.MulticoequalizerDiagram : {T : Type u} → [CompleteLattice T] → {ι : Type u_1} → T → (ι → T) → (ι → ι → T) → Prop
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverMincard_empty : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ}, Dynamics.coverMincard T ∅ U n = 0
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.restrict.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s s_1 : Set β} (e_s : s = s_1)
  (κ κ_1 : ProbabilityTheory.Kernel α β), κ = κ_1 → ∀ (hs : MeasurableSet s), κ.restrict hs = κ_1.restrict ⋯
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a b : α}, cmp a b = Ordering.eq → t[a]? = t[b]?
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.induction_on_pi : ∀ {ι : Type u_1} {motive : (ι → Cardinal.{v}) → Prop} (f : ι → Cardinal.{v}),
  (∀ (f : ι → Type v), motive fun i => Cardinal.mk (f i)) → motive f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {l : List α}, m.size ≤ (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).size
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → k ∉ m₁ \ m₂
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderivWithin_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {s : Set M} {g g' : M → F} {x : M},
  MDiffAt[s] g x → MDiffAt[s] g' x → UniqueMDiffAt[s] x → d[s] (g + g') x = d[s] g x + d[s] g' x
-- Mathlib.CategoryTheory.Limits.Preorder
/-- A family of colimiting binary cofans on a partial order induces a sup-semilattice structure on it.
 -/
Preorder.semilatticeSupOfIsColimitBinaryCofan : {C : Type u} →
  [inst : PartialOrder C] →
    (c : (X Y : C) → CategoryTheory.Limits.BinaryCofan X Y) →
      ((X Y : C) → CategoryTheory.Limits.IsColimit (c X Y)) → SemilatticeSup C
-- Mathlib.Data.Set.Prod
Set.pi_mono' : ∀ {ι : Type u_1} {α : ι → Type u_2} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)},
  (∀ i ∈ s₂, t₁ i ⊆ t₂ i) → s₂ ⊆ s₁ → s₁.pi t₁ ⊆ s₂.pi t₂
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.shrink : Lean.PArray ℚ → ℕ → Lean.PArray ℚ
-- Mathlib.Algebra.Order.Group.Basic
zpow_le_zpow_right : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {m n : ℤ} {a : α},
  1 ≤ a → m ≤ n → a ^ m ≤ a ^ n
-- Lean.Data.NameTrie
Lean.NameTrie.empty : {β : Type u_1} → Lean.NameTrie β
-- Mathlib.Order.Filter.Pointwise
Filter.eventually_neg : ∀ {α : Type u_2} [inst : Neg α] {f : Filter α} {p : α → Prop}, (∀ᶠ (x : α) in -f, p x) ↔ ∀ᶠ (x : α) in f, p (-x)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.mk.inj : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  {inst_3 : Finite σ} {toPreSubmersivePresentation : Algebra.PreSubmersivePresentation R S ι σ}
  {jacobian_isUnit : IsUnit toPreSubmersivePresentation.jacobian}
  {toPreSubmersivePresentation_1 : Algebra.PreSubmersivePresentation R S ι σ}
  {jacobian_isUnit_1 : IsUnit toPreSubmersivePresentation_1.jacobian},
  { toPreSubmersivePresentation := toPreSubmersivePresentation, jacobian_isUnit := jacobian_isUnit } =
      { toPreSubmersivePresentation := toPreSubmersivePresentation_1, jacobian_isUnit := jacobian_isUnit_1 } →
    toPreSubmersivePresentation = toPreSubmersivePresentation_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_of_mem_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β}, a ∈ t.insert k v → cmp k a ≠ Ordering.eq → a ∈ t
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.equiv_iff : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (e : M ≃ₗ[R] N), Module.Finite R M ↔ Module.Finite R N
-- Init.Data.Vector.Lemmas
Vector.replace_append_right : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n m : ℕ} {a b : α} {xs : Vector α n} {ys : Vector α m},
  a ∉ xs → (xs ++ ys).replace a b = xs ++ ys.replace a b
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- `spinGroup Q` forms a group where the inverse is `star`.  -/
spinGroup.instGroupSubtypeCliffordAlgebraMemSubmonoid : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {Q : QuadraticForm R M} → Group ↥(spinGroup Q)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.insertMany_list : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ (l : List (α × β)), m₁.Equiv m₂ → (m₁.insertMany l).Equiv (m₂.insertMany l)
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsBot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊥.IsClosedUnderIsomorphisms
-- Init.SizeOf
Lean.ParserDescr.trailingNode.sizeOf_spec : ∀ (kind : Lean.SyntaxNodeKind) (prec lhsPrec : ℕ) (p : Lean.ParserDescr),
  sizeOf (Lean.ParserDescr.trailingNode kind prec lhsPrec p) = 1 + sizeOf kind + sizeOf prec + sizeOf lhsPrec + sizeOf p
-- Mathlib.Topology.Constructions.SumProd
Filter.Eventually.curry_nhds : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X × Y → Prop} {x : X}
  {y : Y}, (∀ᶠ (x : X × Y) in nhds (x, y), p x) → ∀ᶠ (x' : X) in nhds x, ∀ᶠ (y' : Y) in nhds y, p (x', y')
-- Std.Time.Format.Modifier
Std.Time.Modifier.z.inj : ∀ {presentation presentation_1 : Std.Time.ZoneName},
  Std.Time.Modifier.z presentation = Std.Time.Modifier.z presentation_1 → presentation = presentation_1
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toIsometryEquiv_injective : ∀ {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₂], Function.Injective LinearIsometryEquiv.toIsometryEquiv
-- Aesop.Stats.Basic
Aesop.ForwardInstantiationStats.matches : Aesop.ForwardInstantiationStats → ℕ
-- Mathlib.RingTheory.RingInvo
/-- The equivalence of rings underlying a ring involution.  -/
RingInvo.toRingEquiv : {R : Type u_2} → [inst : Semiring R] → RingInvo R → R ≃+* Rᵐᵒᵖ
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- A constructor that assumes `‖z‖ < 1` instead of `dist z 0 < 1` and returns an element
of `𝕔𝔻` instead of `↥Metric.ball (0 : ℂ) 1`.  -/
Complex.UnitClosedDisc.mk : (z : ℂ) → ‖z‖ ≤ 1 → Complex.UnitClosedDisc
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- Any continuous bijection of light profinite spaces induces an isomorphism.  -/
LightProfinite.isIso_of_bijective : ∀ {X Y : LightProfinite} (f : X ⟶ Y),
  Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f) → CategoryTheory.IsIso f
-- Batteries.Data.Fin.Coding
Fin.encodeOption.eq_1 : ∀ {n : ℕ}, Fin.encodeOption none = 0
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.flag.inj : ∀ {name : Lean.Name} {default : Bool} {name_1 : Lean.Name} {default_1 : Bool},
  Lean.Doc.ArgSpec.flag✝ name default = Lean.Doc.ArgSpec.flag✝ name_1 default_1 → name = name_1 ∧ default = default_1
-- Mathlib.Order.Defs.LinearOrder
LinOrd.instCoeSortType : CoeSort LinOrd (Type u_2)
-- Mathlib.Data.Finset.Finsupp
Finsupp.card_pi : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (f : ι →₀ Finset α), f.pi.card = f.prod fun i => ↑(f i).card
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.lhom_ext'_iff : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ₁₂ : R →+* R₂}
  {φ ψ : (α →₀ M) →ₛₗ[σ₁₂] N}, φ = ψ ↔ ∀ (a : α), φ ∘ₛₗ Finsupp.lsingle a = ψ ∘ₛₗ Finsupp.lsingle a
-- Mathlib.Data.Num.Lemmas
Num.pred_to_nat : ∀ (n : Num), ↑n.pred = (↑n).pred
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ioo : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α},
  Filter.Tendsto a l Filter.atBot →
    Filter.Tendsto b l Filter.atTop →
      ∀ [NoMinOrder α] [NoMaxOrder α], MeasureTheory.AECover μ l fun i => Set.Ioo (a i) (b i)
-- Mathlib.Topology.MetricSpace.PiNat
/-- Given a type `X` and a sequence `Y` of metric spaces and a sequence `f : : ∀ i, X → Y i` of
separating functions, `PiNatEmbed X Y f` is a type synonym for `X` seen as a subset of `∀ i, Y i`.
 -/
Metric.PiNatEmbed : {ι : Type u_2} → (X : Type u_5) → (Y : ι → Type u_6) → ((i : ι) → X → Y i) → Type u_5
-- Init.Data.UInt.Bitwise
USize.or_self : ∀ {a : USize}, a ||| a = a
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.associator_hom_apply : ∀ {X Y Z : TopCat} {x : ↑X} {y : ↑Y} {z : ↑Z},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) ((x, y), z) =
    (x, y, z)
-- Mathlib.Order.Monotone.Odd
/-- An odd function on a linear ordered additive commutative group is strictly monotone on the whole
group provided that it is strictly monotone on `Set.Ici 0`.  -/
strictMono_of_odd_strictMonoOn_nonneg : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G]
  [inst_3 : AddCommGroup H] [inst_4 : PartialOrder H] [IsOrderedAddMonoid H] {f : G → H},
  (∀ (x : G), f (-x) = -f x) → StrictMonoOn f (Set.Ici 0) → StrictMono f
-- Init.Data.UInt.Bitwise
UInt16.not_zero : ~~~0 = -1
-- Mathlib.Data.FunLike.Group
FunLike.leftCancelSemigroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : LeftCancelSemigroup β]
  [inst_3 : IsMulApply F α β], FunLike.leftCancelSemigroup = Function.Injective.leftCancelSemigroup (fun f => ⇑f) ⋯ ⋯
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.getCastD : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [LawfulBEq α] → (a : α) → β a → Std.DHashMap.Internal.AssocList α β → β a
-- Mathlib.SetTheory.Ordinal.Notation
/-- Subtraction of ordinal notations (correct only for normal input)  -/
ONote.sub : ONote → ONote → ONote
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.equiv_empty_iff_isEmpty : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → (m.Equiv ∅ ↔ m.isEmpty = true)
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.IsocrystalHom.mk : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {k : Type u_1} →
      [inst_1 : CommRing k] →
        [inst_2 : CharP k p] →
          [inst_3 : PerfectRing k p] →
            {V : Type u_2} →
              [inst_4 : AddCommGroup V] →
                [inst_5 : WittVector.Isocrystal p k V] →
                  {V₂ : Type u_3} →
                    [inst_6 : AddCommGroup V₂] →
                      [inst_7 : WittVector.Isocrystal p k V₂] →
                        (toLinearMap : V →ₗ[FractionRing (WittVector p k)] V₂) →
                          (∀ (x : V),
                              (WittVector.Isocrystal.frobenius p k) (toLinearMap x) =
                                toLinearMap ((WittVector.Isocrystal.frobenius p k) x)) →
                            WittVector.IsocrystalHom p k V V₂
-- Mathlib.Data.Nat.Prime.Defs
Nat.monoid.primePow : {α : Type u_1} → [Monoid α] → Pow α Nat.Primes
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.IsGLPos.instSMulApply : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_2} [inst : SMul α ℂ] [inst_1 : IsScalarTower α ℂ ℂ]
  [inst_2 : Γ.HasDetOne], IsSMulApply α (CuspForm Γ k) UpperHalfPlane ℂ
-- Init.Data.UInt.Bitwise
UInt16.or_zero : ∀ {a : UInt16}, a ||| 0 = a
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIcc_right : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b), Set.projIcc a b h b = ⟨b, ⋯⟩
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι_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 : cc.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).inv
      (CategoryTheory.CategoryStruct.comp ι h) =
    CategoryTheory.CategoryStruct.comp S.homologyι
      (CategoryTheory.CategoryStruct.comp (S.isoOpcyclesOfIsColimit hcc).inv h)
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
ContMDiffMap.mdifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (f : ContMDiffMap I I' M M' ↑⊤) {x : M},
  MDiffAt ⇑f x
-- Mathlib.RingTheory.IsTensorProduct
/-- Let `R` be a commutative ring, `S` be an `R`-algebra, `M` be an `R`-module, `P` be an `S`
module, `N` be the base change of `M` to `S`, then `P ⊗[S] N` is isomorphic to `P ⊗[R] M`
as `S`-modules.  -/
IsBaseChange.tensorEquiv : {R : Type u_1} →
  {M : Type v₁} →
    {N : Type v₂} →
      {S : Type v₃} →
        [inst : AddCommMonoid M] →
          [inst_1 : AddCommMonoid N] →
            [inst_2 : CommSemiring R] →
              [inst_3 : CommSemiring S] →
                [inst_4 : Algebra R S] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      [inst_7 : Module S N] →
                        [inst_8 : IsScalarTower R S N] →
                          {f : M →ₗ[R] N} →
                            IsBaseChange S f →
                              (P : Type u_6) →
                                [inst_9 : AddCommGroup P] →
                                  [inst_10 : Module R P] →
                                    [inst_11 : Module S P] →
                                      [inst_12 : IsScalarTower R S P] → TensorProduct S P N ≃ₗ[S] TensorProduct R P M
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
Std.Iter.dropWhile_eq_dropWhile_toIterM : ∀ {α β : Type u_1} [Std.Iterator α Id β] {P : β → Bool} {it : Std.Iter β},
  Std.Iter.dropWhile P it = (Std.IterM.dropWhile P it.toIterM).toIter
-- Mathlib.Topology.Order.Category.AlexDisc
alexDiscEquivPreord_inverse_obj_str : ∀ (X : Preord), (alexDiscEquivPreord.inverse.obj X).str = Topology.WithUpperSet.instTopologicalSpace
-- Init.PropLemmas
/-- Excluded middle.  Added as alias for Decidable.em  -/
Decidable.or_not_self : ∀ (p : Prop) [Decidable p], p ∨ ¬p
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
/-- In 2D, the line defined by `s.orthRadius p` intersects `s` at exactly two points so long as `p`
lies strictly within `s` and not at its center.  -/
EuclideanGeometry.Sphere.ncard_inter_orthRadius_eq_two_of_dist_lt_radius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hf2 : Fact (Module.finrank ℝ V = 2)] {s : EuclideanGeometry.Sphere P} {p : P},
  dist p s.center < s.radius → p ≠ s.center → (Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)).ncard = 2
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddSemigroupOfContinuousAdd : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : AddSemigroup β] → [ContinuousAdd β] → AddSemigroup C(α, β)
-- Mathlib.Data.Multiset.Fintype
Multiset.mem_toEnumFinset : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α) (p : α × ℕ), p ∈ m.toEnumFinset ↔ p.2 < Multiset.count p.1 m
-- Mathlib.Analysis.Convex.StrictConvexBetween
/-- The strict triangle inequality.  -/
dist_lt_dist_add_dist_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {a b c : P}, dist a c < dist a b + dist b c ↔ ¬Wbtw ℝ a b c
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.Measure.hausdorffMeasure.congr_simp : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (d d_1 : ℝ),
  d = d_1 → MeasureTheory.Measure.hausdorffMeasure d = MeasureTheory.Measure.hausdorffMeasure d_1
-- Lean.Meta.Tactic.Grind.MatchCond
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go.replaceLhss : Array Lean.Expr → Array (Option Lean.Expr) → Lean.Expr → ℕ → Lean.Expr
-- Mathlib.Algebra.WithConv
WithConv.toConv_surjective : ∀ {A : Type u_2}, Function.Surjective WithConv.toConv
-- Lean.Meta.Diagnostics
Lean.Meta.mkDiagSummaryForUnfolded : Lean.PHashMap Lean.Name ℕ → optParam Bool false → Lean.MetaM Lean.Meta.DiagSummary
-- Batteries.Data.Vector.Lemmas
Vector.back_scanr : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {init : β} {f : α → β → β} {as : Vector α n},
  (Vector.scanr f init as).back = init
-- Mathlib.Order.OrderDual
/-- **Alias** of the reverse direction of `OrderDual.ofDual_le_ofDual`. -/
LE.le.ofDual : ∀ {α : Type u_1} [inst : LE α] {a b : αᵒᵈ}, b ≤ a → OrderDual.ofDual a ≤ OrderDual.ofDual b
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.finset_logSizeBallSeq_add_one_subset : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  (i : ℕ), (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset ⊆ (PairReduction.logSizeBallSeq J hJ a c i).finset
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.Const.alterKey_cons_perm.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (v : β) (h_1 : Unit → motive none) (h_2 : (v : β) → motive (some v)),
  (match some v with
    | none => h_1 ()
    | some v => h_2 v) =
    h_2 v
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_unsat_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℤ → ℤ → Bool
-- Mathlib.Topology.Bornology.BoundedOperation
BoundedMul.isBounded_mul : ∀ {R : Type u_1} {inst : Bornology R} {inst_1 : Mul R} [self : BoundedMul R] {s t : Set R},
  Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s * t)
-- Init.Data.Random
RandomGen.mk : {g : Type u} → (g → ℕ × ℕ) → (g → ℕ × g) → (g → g × g) → RandomGen g
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory C],
  CategoryTheory.SemiCartesianMonoidalCategory.toUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.SemiCartesianMonoidalCategory.fst_def : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.SemiCartesianMonoidalCategory C]
  (X Y : C),
  CategoryTheory.SemiCartesianMonoidalCategory.fst X Y =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X
        (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from Y))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
-- Init.SizeOf
Array.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (toList : List α), sizeOf { toList := toList } = 1 + sizeOf toList
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The coefficients `M →₀ R` of an element of the additive monoid algebra `R[M]`.  -/
AddMonoidAlgebra.coeff : {R : Type u_8} → {M : Type u_9} → [inst : Semiring R] → AddMonoidAlgebra R M → M →₀ R
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- Any monomorphism in `Type` is a coproduct injection.  -/
CategoryTheory.Limits.Types.isCoprodOfMono : {X Y : Type u} →
  (f : X ⟶ Y) →
    [CategoryTheory.Mono f] →
      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f (TypeCat.ofHom Subtype.val))