mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.HasPrimitives
Complex.wedgeIntegral_add_wedgeIntegral_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (z w : ℂ) (f : ℂ → E),
  z.wedgeIntegral w f + w.wedgeIntegral z f =
    (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) +
        Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) -
      Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_filter_not : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ι → Prop),
  (π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion
-- Mathlib.Data.Matrix.Mul
/-- `M * N` is the usual product of matrices `M` and `N`, i.e. we have that
`(M * N) i k` is the dot product of the `i`-th row of `M` by the `k`-th column of `N`.
This is currently only defined when `m` is finite.  -/
Matrix.instHMulOfFintypeOfMulOfAddCommMonoid : {l : Type u_1} →
  {m : Type u_2} →
    {n : Type u_3} →
      {α : Type v} → [Fintype m] → [Mul α] → [AddCommMonoid α] → HMul (Matrix l m α) (Matrix m n α) (Matrix l n α)
-- Init.Grind.Module.Basic
/-- A module over the natural numbers, i.e. a type with zero, addition, and scalar multiplication by natural numbers,
satisfying appropriate compatibilities.

Equivalently, an additive commutative monoid.

Use `IntModule` if the type has negation.
 -/
Lean.Grind.NatModule : Type u → Type u
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.sheafIso_hom_hom : ∀ {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} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ ℱ' : CategoryTheory.Sheaf K A} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj),
  (CategoryTheory.Functor.IsCoverDense.sheafIso i).hom.hom = (CategoryTheory.Functor.IsCoverDense.presheafIso i).hom
-- Mathlib.MeasureTheory.Function.Intersectivity
/-- **Bergelson Intersectivity Lemma**: In a finite measure space, a sequence of events that have
measure at least `r` has an infinite subset whose finite intersections all have positive volume.

TODO: The infinity of `t` should be strengthened to `t` having positive natural density.  -/
bergelson' : ∀ {α : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  {r : ENNReal} {s : ℕ → Set α},
  (∀ (n : ℕ), MeasurableSet (s n)) →
    r ≠ 0 → (∀ (n : ℕ), r ≤ μ (s n)) → ∃ t, t.Infinite ∧ ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → 0 < μ (⋂ n ∈ u, s n)
-- Mathlib.Algebra.Category.AlgCat.Basic
algEquivIsoAlgebraIso_hom : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : Ring X] [inst_2 : Ring Y] [inst_3 : Algebra R X]
  [inst_4 : Algebra R Y], algEquivIsoAlgebraIso.hom = TypeCat.ofHom fun e => e.toAlgebraIso
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.lift_ofList : ∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M] (f : α → M) (l : List α),
  (FreeMonoid.lift f) (FreeMonoid.ofList l) = (List.map f l).prod
-- Mathlib.Analysis.CStarAlgebra.Basic
NormedStarGroup.to_continuousStar : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : StarAddMonoid E] [NormedStarGroup E], ContinuousStar E
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.rTensor_baseChange : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : AddCommMonoid M]
  [inst_6 : AddCommMonoid N] [inst_7 : Module R M] [inst_8 : Module R N] (φ : A →ₐ[R] B) (t : TensorProduct R A M)
  (f : M →ₗ[R] N),
  (LinearMap.rTensor N φ.toLinearMap) ((LinearMap.baseChange A f) t) =
    (LinearMap.baseChange B f) ((LinearMap.rTensor M φ.toLinearMap) t)
-- Mathlib.Algebra.Algebra.Basic
LinearMap.extendScalarsOfSurjective_apply : ∀ {R : Type u_1} {S : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_2}
  {N : Type u_3} [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M] [inst_6 : Module S M]
  [inst_7 : IsScalarTower R S M] [inst_8 : Module R N] [inst_9 : Module S N] [inst_10 : IsScalarTower R S N]
  (h : Function.Surjective ⇑(algebraMap R S)) (l : M →ₗ[R] N) (x : M), (LinearMap.extendScalarsOfSurjective h l) x = l x
-- Std.Net.Addr
Std.Net.IPAddr.v6 : Std.Net.IPv6Addr → Std.Net.IPAddr
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Ref.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → (gate : ℕ) → Bool → gate < aig.decls.size → aig.Ref
-- Batteries.Linter.UnreachableTactic
/-- Adds a new syntax kind whose children will be ignored by the `unreachableTactic` linter.
This should be called from an `initialize` block.
 -/
Batteries.Linter.UnreachableTactic.addIgnoreTacticKind : Lean.SyntaxNodeKind → IO Unit
-- Mathlib.Topology.Order
continuous_sInf_dom : ∀ {α : Type u} {β : Type v} {f : α → β} {t₁ : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β}
  {t : TopologicalSpace α}, t ∈ t₁ → Continuous f → Continuous f
-- Std.Internal.Do.Triple.Basic
/-- Hoare triple notation without exception postcondition (defaults to `⊥`). An optional `(m := …)`
after the precondition ascribes the program to monad `…`.  -/
Std.Internal.Do.tripleNotation : Lean.ParserDescr
-- Mathlib.Algebra.Ring.IsFormallyReal
IsSumNonzeroSq.sq : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] {a : R}, a ≠ 0 → IsSumNonzeroSq (a * a)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.isPath_map_iff_of_injective`. -/
SimpleGraph.Walk.IsPath.map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v},
  Function.Injective ⇑f → p.IsPath → (SimpleGraph.Walk.map f p).IsPath
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.sub : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {s : Set α}
  {μ : MeasureTheory.Measure α} {f g : α → E},
  MeasureTheory.IntegrableOn f s μ → MeasureTheory.IntegrableOn g s μ → MeasureTheory.IntegrableOn (f - g) s μ
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.toEquiv_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), e.symm.toEquiv = e.symm
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureResult.script : Aesop.Script.DynStructureResult → List Aesop.Script.Step
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreHomEquiv.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
  (homEquiv_naturality_left_symm :
    autoParam
      (∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
        (homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (F.map f) ((homEquiv X Y).symm g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm._autoParam)
  (homEquiv_naturality_right :
    autoParam
      (∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
        (homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp ((homEquiv X Y) f) (G.map g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right._autoParam)
  (homEquiv_1 : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
  (homEquiv_naturality_left_symm_1 :
    autoParam
      (∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
        (homEquiv_1 X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (F.map f) ((homEquiv_1 X Y).symm g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm._autoParam)
  (homEquiv_naturality_right_1 :
    autoParam
      (∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
        (homEquiv_1 X Y') (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp ((homEquiv_1 X Y) f) (G.map g))
      CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right._autoParam),
  ({ homEquiv := homEquiv, homEquiv_naturality_left_symm := homEquiv_naturality_left_symm,
        homEquiv_naturality_right := homEquiv_naturality_right } =
      { homEquiv := homEquiv_1, homEquiv_naturality_left_symm := homEquiv_naturality_left_symm_1,
        homEquiv_naturality_right := homEquiv_naturality_right_1 }) =
    (homEquiv = homEquiv_1)
-- Init.Data.SInt.Lemmas
ISize.toInt8_mul : ∀ (a b : ISize), (a * b).toInt8 = a.toInt8 * b.toInt8
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddActionForall : {M : Type u_1} → {β : Type u_2} → {α : Type u_3} → [inst : AddMonoid M] → [AddAction M α] → AddAction Mᵈᵃᵃ (α → β)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
/-- **Alias** of `IsAddCyclic.isAddCommutative`. -/
IsAddCyclic.commutative : ∀ {α : Type u_1} [inst : AddGroup α] [IsAddCyclic α], IsAddCommutative α
-- Mathlib.Topology.Category.CompHausLike.EffectiveEpi
CompHausLike.precoherent : ∀ {P : TopCat → Prop} [CompHausLike.HasExplicitPullbacks P] [CompHausLike.HasExplicitFiniteCoproducts P],
  (∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
    CategoryTheory.Precoherent (CompHausLike P)
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.inter_cylinder_same : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (S₁ S₂ : Set ((i : ↥s) → α ↑i)),
  MeasureTheory.cylinder s S₁ ∩ MeasureTheory.cylinder s S₂ = MeasureTheory.cylinder s (S₁ ∩ S₂)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
ComplexShape.Embedding.truncGE'Functor.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e e_1 : c.Embedding c') (e_e : e = e_1)
  [inst : e.IsTruncGE] (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.CategoryWithHomology C],
  e.truncGE'Functor C = e_1.truncGE'Functor C
-- Mathlib.NumberTheory.LSeries.Basic
/-- If `s ≠ 0`, then the `if .. then .. else` construction in `LSeries.term` isn't needed, since
`0 ^ s = 0`.
 -/
LSeries.term_of_ne_zero' : ∀ {s : ℂ}, s ≠ 0 → ∀ (f : ℕ → ℂ) (n : ℕ), LSeries.term f s n = f n / ↑n ^ s
-- Init.Data.BitVec.Lemmas
BitVec.toInt_zero_length : ∀ (x : BitVec 0), x.toInt = 0
-- Mathlib.Topology.MetricSpace.Holder
/-- If a function is `r`-Hölder over a bounded set, then it is also `s`-Hölder when `s ≤ r`.  -/
HolderOnWith.of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {C D s : NNReal} {A : Set X},
  (∀ x ∈ A, ∀ y ∈ A, edist x y ≤ ↑D) → HolderOnWith C r f A → s ≤ r → HolderOnWith (C * D ^ (↑r - ↑s)) s f A
-- Mathlib.Algebra.GroupWithZero.Associated
associated_one_iff_isUnit : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, Associated a 1 ↔ IsUnit a
-- Mathlib.Topology.Maps.Proper.CompactlyGenerated
/-- Version of `isProperMap_iff_isCompact_preimage` in terms of `cocompact`.

There was an older version of this theorem which was changed to this one to make use
of the `CompactlyGeneratedSpace` typeclass. (since 2024-11-10)  -/
isProperMap_iff_tendsto_cocompact : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y]
  [CompactlyCoherentSpace Y] {f : X → Y},
  IsProperMap f ↔ Continuous f ∧ Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.instIsMulTorsionFree : ∀ {ι : Type u_1} {M : ι → Type u_3} [inst : (i : ι) → Monoid (M i)] [∀ (i : ι), IsMulTorsionFree (M i)],
  IsMulTorsionFree ((i : ι) → M i)
-- Mathlib.Data.List.Permutation
List.permutationsAux2.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (x : List α → β),
  List.permutationsAux2 t ts r [] x = (ts, r)
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- Noether's second isomorphism theorem: given two subgroups `H` and `N` of a group
`G`, where `N` is normal, defines an isomorphism between `H/(H ∩ N)` and `(H + N)/N`.  -/
QuotientAddGroup.quotientInfEquivSumNormalQuotient : {G : Type u} →
  [inst : AddGroup G] →
    (H N : AddSubgroup G) → [hN : N.Normal] → ↥H ⧸ N.addSubgroupOf H ≃+ ↥(H ⊔ N) ⧸ N.addSubgroupOf (H ⊔ N)
-- Batteries.Data.Fin.Lemmas
Fin.eq_false_of_find?_eq_none : ∀ {n : ℕ} {p : Fin n → Bool}, Fin.find? p = none → ∀ (i : Fin n), p i = false
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ComputedFieldView.modifiers : Lean.Elab.Command.ComputedFieldView → Lean.Syntax
-- Mathlib.RingTheory.Finiteness.Basic
_private.Mathlib.RingTheory.Finiteness.Basic.0.«termR≥0» : Lean.ParserDescr
-- Mathlib.Topology.Compactification.StoneCech
instCompactSpacePreStoneCech : ∀ {α : Type u} [inst : TopologicalSpace α], CompactSpace (PreStoneCech α)
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.dvd_gcd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Multiset α} {a : α},
  a ∣ s.gcd ↔ ∀ b ∈ s, a ∣ b
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
groupCohomology.IsMulCocycle₁.eq_1 : ∀ {G : Type u_1} {M : Type u_2} [inst : Mul G] [inst_1 : CommGroup M] [inst_2 : SMul G M] (f : G → M),
  groupCohomology.IsMulCocycle₁ f = ∀ (g h : G), f (g * h) = g • f h * f g
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The "left" map `W ⟶ X`.  -/
CategoryTheory.IsRegularEpi.left : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (f : X ⟶ Y) → [inst_1 : CategoryTheory.IsRegularEpi f] → CategoryTheory.IsRegularEpi.W f ⟶ X
-- Init.Data.UInt.Lemmas
UInt32.ofFin_bitVecToFin : ∀ (n : BitVec 32), UInt32.ofFin n.toFin = { toBitVec := n }
-- Batteries.Lean.IO.Process
/-- Pipe `input` into stdin of the spawned process,
then return the entire content of stdout as a `String` upon completion.
 -/
IO.Process.runCmdWithInput : String → Array String → optParam String "" → optParam Bool true → IO String
-- Mathlib.Data.List.ProdSigma
List.mem_map_swap : ∀ {α : Type u_1} {β : Type u_2} (x : α) (y : β) (xs : List (α × β)), (y, x) ∈ List.map Prod.swap xs ↔ (x, y) ∈ xs
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.mk.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7}
  (toMultilinearMap toMultilinearMap_1 : MultilinearMap R (fun x => M) N)
  (e_toMultilinearMap : toMultilinearMap = toMultilinearMap_1)
  (map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toMultilinearMap.toFun v = 0),
  { toMultilinearMap := toMultilinearMap, map_eq_zero_of_eq' := map_eq_zero_of_eq' } =
    { toMultilinearMap := toMultilinearMap_1, map_eq_zero_of_eq' := ⋯ }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_eq_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {he : t.isEmpty = false}, t.minKey he = t.minKey!
-- Mathlib.Data.List.AList
AList.instUnion : {α : Type u} → {β : α → Type v} → [DecidableEq α] → Union (AList β)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
PolynormableSpace.mk : ∀ {𝕜 : Type u_2} {E : Type u_6} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [topology : TopologicalSpace E], (WithSeminorms fun p => ↑p) → PolynormableSpace 𝕜 E
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- For a manifold `N` and a `C^n` homomorphism `φ` between `C^n` rings `R'`, `R''`, the
'left-composition-by-`φ`' ring homomorphism from `C^n⟮I, N; I', R'⟯` to `C^n⟮I, N; I'', R''⟯`.  -/
ContMDiffMap.compLeftRingHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    (I : ModelWithCorners 𝕜 E H) →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            (N : Type u_6) →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {E'' : Type u_7} →
                                    [inst_9 : NormedAddCommGroup E''] →
                                      [inst_10 : NormedSpace 𝕜 E''] →
                                        {H'' : Type u_8} →
                                          [inst_11 : TopologicalSpace H''] →
                                            {I'' : ModelWithCorners 𝕜 E'' H''} →
                                              {n : WithTop ℕ∞} →
                                                {R' : Type u_10} →
                                                  [inst_12 : Ring R'] →
                                                    [inst_13 : TopologicalSpace R'] →
                                                      [inst_14 : ChartedSpace H' R'] →
                                                        [inst_15 : ContMDiffRing I' n R'] →
                                                          {R'' : Type u_11} →
                                                            [inst_16 : Ring R''] →
                                                              [inst_17 : TopologicalSpace R''] →
                                                                [inst_18 : ChartedSpace H'' R''] →
                                                                  [inst_19 : ContMDiffRing I'' n R''] →
                                                                    (φ : R' →+* R'') →
                                                                      ContMDiff I' I'' n ⇑φ →
                                                                        ContMDiffMap I I' N R' n →+*
                                                                          ContMDiffMap I I'' N R'' n
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).toNNReal = OfNat.ofNat n
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
AddCommGrpCat.uliftZMultiplesAddEquiv_symm_apply_hom_apply : ∀ (G : AddCommGrpCat) (a : ↑G) (x : ULift.{u_1, 0} ℤ),
  (AddCommGrpCat.Hom.hom (G.uliftZMultiplesAddEquiv.symm a)) x = AddEquiv.ulift x • a
-- Mathlib.Data.Finset.Image
Finset.exists_mem_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {p : β → Prop},
  (∃ y ∈ Finset.image f s, p y) ↔ ∃ x ∈ s, p (f x)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- The characteristic predicate for localized module.
`IsLocalizedModule S f` describes that `f : M ⟶ M'` is the localization map identifying `M'` as
`LocalizedModule S M`.
 -/
IsLocalizedModule : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_2} →
      {M' : Type u_3} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M'] →
            [inst_3 : Module R M] → [inst_4 : Module R M'] → Submonoid R → (M →ₗ[R] M') → Prop
-- Init.Data.SInt.Lemmas
Int64.ofNat_toNatClampNeg : ∀ (x : Int64), 0 ≤ x → Int64.ofNat x.toNatClampNeg = x
-- Mathlib.Control.Bifunctor
Bifunctor.snd_fst : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α₀ α₁ : Type u₀} {β₀ β₁ : Type u₁}
  (f : α₀ → α₁) (f' : β₀ → β₁) (x : F α₀ β₀), Bifunctor.snd f' (Bifunctor.fst f x) = bimap f f' x
-- Init.Data.List.Sort.Basic
/-- Merges two lists, using `le` to select the first element of the resulting list if both are
non-empty.

If both input lists are sorted according to `le`, then the resulting list is also sorted according
to `le`. `O(|xs| + |ys|)`.

This implementation is not tail-recursive, but it is replaced at runtime by a proven-equivalent
tail-recursive merge.
 -/
List.merge : {α : Type u_1} → List α → List α → autoParam (α → α → Bool) List.merge._auto_1 → List α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_eq_getD_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {a : α}, t[a]! = t.getD a default
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
/-- Unlike categories, for graphs vertex equality is an important notion, so needing to be able to
work with equality of graph homomorphisms is a necessary evil.  -/
SimpleGraph.Walk.map_eq_of_eq : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v : V} (p : G.Walk u v) {f : G →g G'}
  (f' : G →g G') (h : f = f'), SimpleGraph.Walk.map f p = (SimpleGraph.Walk.map f' p).copy ⋯ ⋯
-- Mathlib.Data.Nat.Prime.Defs
/-- This instance is set up to work in the kernel (`by decide`) for small values.

Below (`decidablePrime'`) we will define a faster variant to be used by the compiler
(e.g. in `#eval` or `by native_decide`).

If you need to prove that a particular number is prime, in any case
you should not use `by decide`, but rather `by norm_num`, which is
much faster.
 -/
Nat.decidablePrime : (p : ℕ) → Decidable (Nat.Prime p)
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.Result.mk.injEq : ∀ {α : Type} (filtered : Option ProofWidgets.Html) (unfiltered : ProofWidgets.Html) (key : α)
  (pattern : ProofWidgets.Html) (filtered_1 : Option ProofWidgets.Html) (unfiltered_1 : ProofWidgets.Html) (key_1 : α)
  (pattern_1 : ProofWidgets.Html),
  ({ filtered := filtered, unfiltered := unfiltered, key := key, pattern := pattern } =
      { filtered := filtered_1, unfiltered := unfiltered_1, key := key_1, pattern := pattern_1 }) =
    (filtered = filtered_1 ∧ unfiltered = unfiltered_1 ∧ key = key_1 ∧ pattern = pattern_1)
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequence_comp_assoc : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological] [inst_9 : F.ShiftSequence ℤ],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ : ℤ) {Z : A} (h : (F.shift n₀).obj T.obj₃ ⟶ Z),
      CategoryTheory.CategoryStruct.comp ((F.shift n₀).map T.mor₁)
          (CategoryTheory.CategoryStruct.comp ((F.shift n₀).map T.mor₂) h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
/-- A morphism is scheme-theoretically dominant if its kernel is trivial.  -/
AlgebraicGeometry.IsSchemeTheoreticallyDominant : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop