mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtHashSet.Basic
/-- Retrieves the key from the set that matches `a`. Ensures that such a key exists by requiring a proof
of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the set.
 -/
Std.ExtHashSet.get : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      [inst : EquivBEq α] → [inst_1 : LawfulHashable α] → (m : Std.ExtHashSet α) → (a : α) → a ∈ m → α
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.prev.eq_1 : ∀ (x : String.Pos.Raw) (s : String) (b stopPos : String.Pos.Raw),
  { str := s, startPos := b, stopPos := stopPos }.prev x =
    if x.offsetBy b = b then x else { byteIdx := (String.Pos.Raw.prev s (x.offsetBy b)).byteIdx - b.byteIdx }
-- Mathlib.Algebra.GCDMonoid.Basic
NormalizationMonoid.normUnit_one : ∀ {α : Type u_2} {inst : MonoidWithZero α} [self : NormalizationMonoid α], normUnit 1 = 1
-- Mathlib.CategoryTheory.Sigma.Basic
/-- The functor `Sigma.map` applied to the identity function is just the identity functor.  -/
CategoryTheory.Sigma.mapId : (I : Type w₁) →
  (C : I → Type u₁) →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      CategoryTheory.Sigma.map C id ≅ CategoryTheory.Functor.id ((i : I) × C i)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- If two standard Borel spaces admit Borel measurable injections to one another,
then they are Borel isomorphic.  -/
PolishSpace.borelSchroederBernstein : {α : Type u_4} →
  {β : Type u_6} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] →
        [StandardBorelSpace α] →
          [StandardBorelSpace β] →
            {f : α → β} →
              {g : β → α} → Measurable f → Function.Injective f → Measurable g → Function.Injective g → α ≃ᵐ β
-- Mathlib.CategoryTheory.Monad.Limits
/-- If `C` has colimits of shape `J` then any coreflective subcategory has colimits of shape `J`.  -/
CategoryTheory.hasColimitsOfShape_of_coreflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasColimitsOfShape J C]
  (R : CategoryTheory.Functor D C) [CategoryTheory.Coreflective R], CategoryTheory.Limits.HasColimitsOfShape J D
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.of_forall_getElem?_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [LawfulBEq α],
  m₁.WF → m₂.WF → (∀ (k : α), m₁[k]? = m₂[k]?) → m₁.Equiv m₂
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.instNullSingletonClassElemRealVolume : MeasureTheory.NullSingletonClass MeasureTheory.volume
-- Init.Data.String.Lemmas.Modify
String.map_eq_internal : ∀ {f : Char → Char} {s : String}, String.map f s = String.ofList (List.map f s.toList)
-- Mathlib.Order.Monotone.Defs
Subsingleton.monotone : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] [Subsingleton α] (f : α → β), Monotone f
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_filter_eq_size_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool}, (Std.ExtDHashMap.filter f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f k (m.get k h) = true
-- Lean.Elab.BuiltinCommand
/-- If `id` is an identifier, return true if `ids` contains `id`.  -/
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.containsId : Array (Lean.TSyntax [`ident, `Lean.Parser.Term.hole]) → Lean.TSyntax [`ident, `Lean.Parser.Term.hole] → Bool
-- Mathlib.Data.Multiset.Defs
Multiset.leInductionOn : ∀ {α : Type u_1} {C : Multiset α → Multiset α → Prop} {s t : Multiset α},
  s ≤ t → (∀ {l₁ l₂ : List α}, l₁.Sublist l₂ → C ↑l₁ ↑l₂) → C s t
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
tendsto_zero_geometric_tsum_pnat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {r : 𝕜},
  ‖r‖ < 1 → Filter.Tendsto (fun m => ∑' (n : ℕ+), r ^ (↑n * ↑m)) Filter.atTop (nhds 0)
-- Mathlib.Geometry.Manifold.Bordism
/-- The manifold `M` of a singular `n`-manifold `(M, f)`  -/
SingularManifold.M : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {k : WithTop ℕ∞} →
      {E : Type u_2} →
        {H : Type u_3} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : FiniteDimensional ℝ E] →
                [inst_4 : TopologicalSpace H] → {I : ModelWithCorners ℝ E H} → SingularManifold X k I → Type u
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.posPart : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : AddGroup β] [inst_3 : Lattice β] [ContinuousSup β],
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => (f x)⁺
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instZero : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → Zero (WithVal v)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_sum : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {ι : Type u_1}
  (g : ι → Polynomial R) (s : Finset ι), Polynomial.map f (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.map f (g i)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_le_size_insertMany_list : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α}, m.size ≤ (m.insertMany l).size
-- Mathlib.Analysis.SumOverResidueClass
/-- A sequence `f` with values in an additive topological group `R` is summable on the
residue class of `k` mod `m` if and only if `f (m*n + k)` is summable.  -/
summable_indicator_mod_iff_summable : ∀ {R : Type u_1} [inst : AddCommGroup R] [inst_1 : TopologicalSpace R] [IsTopologicalAddGroup R] (m : ℕ) [hm : NeZero m]
  (k : ℕ) (f : ℕ → R), Summable ({n | ↑n = ↑k}.indicator f) ↔ Summable fun n => f (m * n + k)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Post-composition by a uniform embedding is a uniform embedding for the
uniform structures of `𝔖`-convergence.

More precisely, if `f : γ → β` is a uniform embedding, then
`(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)` is a uniform embedding.  -/
UniformOnFun.postcomp_isUniformEmbedding : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {𝔖 : Set (Set α)} [inst_1 : UniformSpace γ]
  {f : γ → β},
  IsUniformEmbedding f → IsUniformEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(UniformOnFun.toFun 𝔖))
-- Mathlib.RingTheory.Etale.Kaehler
/-- If `J ≃ Q ⊗ₚ I`, `S → T` is flat and `P → Q` is formally étale, then `T ⊗ H¹(L_P) ≃ H¹(L_Q)`.  -/
Algebra.Extension.tensorH1CotangentOfFormallyEtale : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] →
                  [IsScalarTower R S T] →
                    {P : Algebra.Extension R S} →
                      {Q : Algebra.Extension R T} →
                        (f : P.Hom Q) →
                          [alg : Algebra P.Ring Q.Ring] →
                            (halg : algebraMap P.Ring Q.Ring = f.toRingHom) →
                              [Module.Flat S T] →
                                f.toRingHom.FormallyEtale →
                                  Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) →
                                    TensorProduct S T P.H1Cotangent ≃ₗ[T] Q.H1Cotangent
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryGT? : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.mk.inj : ∀ {A : Type u_1} {inst : CommSemiring A} {I : Ideal A} {dpow : ℕ → A → A}
  {dpow_null : ∀ {n : ℕ} {x : A}, x ∉ I → dpow n x = 0} {dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1}
  {dpow_one : ∀ {x : A}, x ∈ I → dpow 1 x = x} {dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow n x ∈ I}
  {dpow_add :
    ∀ {n : ℕ} {x y : A},
      x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, dpow k.1 x * dpow k.2 y}
  {dpow_mul : ∀ {n : ℕ} {a x : A}, x ∈ I → dpow n (a * x) = a ^ n * dpow n x}
  {mul_dpow : ∀ {m n : ℕ} {x : A}, x ∈ I → dpow m x * dpow n x = ↑((m + n).choose m) * dpow (m + n) x}
  {dpow_comp : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow m (dpow n x) = ↑(m.uniformBell n) * dpow (m * n) x}
  {dpow_1 : ℕ → A → A} {dpow_null_1 : ∀ {n : ℕ} {x : A}, x ∉ I → dpow_1 n x = 0}
  {dpow_zero_1 : ∀ {x : A}, x ∈ I → dpow_1 0 x = 1} {dpow_one_1 : ∀ {x : A}, x ∈ I → dpow_1 1 x = x}
  {dpow_mem_1 : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow_1 n x ∈ I}
  {dpow_add_1 :
    ∀ {n : ℕ} {x y : A},
      x ∈ I → y ∈ I → dpow_1 n (x + y) = ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, dpow_1 k.1 x * dpow_1 k.2 y}
  {dpow_mul_1 : ∀ {n : ℕ} {a x : A}, x ∈ I → dpow_1 n (a * x) = a ^ n * dpow_1 n x}
  {mul_dpow_1 : ∀ {m n : ℕ} {x : A}, x ∈ I → dpow_1 m x * dpow_1 n x = ↑((m + n).choose m) * dpow_1 (m + n) x}
  {dpow_comp_1 : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow_1 m (dpow_1 n x) = ↑(m.uniformBell n) * dpow_1 (m * n) x},
  { dpow := dpow, dpow_null := dpow_null, dpow_zero := dpow_zero, dpow_one := dpow_one, dpow_mem := dpow_mem,
        dpow_add := dpow_add, dpow_mul := dpow_mul, mul_dpow := mul_dpow, dpow_comp := dpow_comp } =
      { dpow := dpow_1, dpow_null := dpow_null_1, dpow_zero := dpow_zero_1, dpow_one := dpow_one_1,
        dpow_mem := dpow_mem_1, dpow_add := dpow_add_1, dpow_mul := dpow_mul_1, mul_dpow := mul_dpow_1,
        dpow_comp := dpow_comp_1 } →
    dpow = dpow_1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.div_cert : Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.sub_comp : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {N₃ : Type u_13} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommGroup N₃] [inst_6 : Module R₁ M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ N₃] {σ₁₂ : R₁ →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂)
  (g h : M₂ →ₛₗ[σ₂₃] N₃), (g - h) ∘ₛₗ f = g ∘ₛₗ f - h ∘ₛₗ f
-- Mathlib.Analysis.Normed.Module.WeakDual
WeakDual.extendRCLikeL_apply : ∀ {𝕜 : Type u_5} {F : Type u_7} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (x : WeakDual ℝ F),
  WeakDual.extendRCLikeL x = StrongDual.toWeakDual (StrongDual.extendRCLikeₗ (WeakDual.toStrongDual x))
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.ιSigmaHorn_jointly_surjective : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] {d : ℕ} {j : ι} (a : (f.sigmaHorn j).obj (Opposite.op { len := d })),
  ∃ c x, (CategoryTheory.ConcreteCategory.hom (c.ιSigmaHorn.app (Opposite.op { len := d }))) x = a
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instFullPushforward : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f],
  (AlgebraicGeometry.Scheme.Modules.pushforward f).Full
-- Mathlib.Data.Set.Basic
Set.inter_isComm : ∀ {α : Type u}, Std.Commutative fun x1 x2 => x1 ∩ x2
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.valuation_coe_ratFunc : ∀ (K : Type u_2) [inst : Field K] (f : RatFunc K), Valued.v ((algebraMap (RatFunc K) (LaurentSeries K)) f) = Valued.v f
-- Mathlib.Order.Hom.Basic
/-- Reinterpret an order isomorphism as an order embedding.  -/
OrderIso.toOrderEmbedding : {α : Type u_2} → {β : Type u_3} → [inst : LE α] → [inst_1 : LE β] → α ≃o β → α ↪o β
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- If all elements of an infinite set have measure uniformly separated from zero,
then the set has infinite measure.  -/
Set.Infinite.meas_eq_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] {s : Set α},
  s.Infinite → (∃ ε, ε ≠ 0 ∧ ∀ x ∈ s, ε ≤ μ {x}) → μ s = ⊤
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_eq_tprod_of_hasProd_iff_hasProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [T2Space α]
  {f : β → α} {g : γ → α}, (∀ {a : α}, HasProd f a ↔ HasProd g a) → ∏' (b : β), f b = ∏' (c : γ), g c
-- Init.Data.List.MinMax
List.max_mem : ∀ {α : Type u_1} [inst : Max α] [Std.MaxEqOr α] {l : List α} (hl : l ≠ []), l.max hl ∈ l
-- Init.Data.List.Lemmas
List.head?_dropLast : ∀ {α : Type u_1} {xs : List α}, xs.dropLast.head? = if 1 < xs.length then xs.head? else none
-- Mathlib.CategoryTheory.Grothendieck
/-- If `F : C ⥤ Cat` is a functor and `t : c ⟶ d` is a morphism in `C`, then `transport` maps each
`c`-based element of `Grothendieck F` to a `d`-based element.
 -/
CategoryTheory.Grothendieck.transport : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      (x : CategoryTheory.Grothendieck F) → {c : C} → (x.base ⟶ c) → CategoryTheory.Grothendieck F
-- Lean.Parser.Level
Lean.Parser.Level.paren.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Binomial
/-- The multichoose function for integers.  -/
Int.multichoose : ℤ → ℕ → ℤ
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.submoduleMap_symm_apply_coe : ∀ {R : Type u_13} {R₂ : Type u_15} {M : Type u_16} {M₂ : Type u_17} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : SeminormedAddCommGroup M] [inst_3 : SeminormedAddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (p : Submodule R M)
  (e : M ≃ₛₗᵢ[σ₁₂] M₂) (y : ↥(Submodule.map (↑e.toLinearEquiv) p)),
  ↑((LinearIsometryEquiv.submoduleMap p e).symm y) = e.symm ↑y
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.copy_carrier : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (C : ConvexCone R M) (s : Set M) (hs : s = ↑C), ↑(C.copy s hs) = s
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_diagonal : ∀ {l : Type u_1} {m : Type u_2} {α : Type u_12} [inst : DecidableEq l] [inst_1 : DecidableEq m] [inst_2 : Zero α]
  (d₁ : l → α) (d₂ : m → α),
  Matrix.fromBlocks (Matrix.diagonal d₁) 0 0 (Matrix.diagonal d₂) = Matrix.diagonal (Sum.elim d₁ d₂)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.star.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C], sizeOf CategoryTheory.WithTerminal.star = 1
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.of_div : ∀ {m a b c : ℕ}, a / c ≡ b / c [MOD m / c] → c ∣ a → c ∣ b → c ∣ m → a ≡ b [MOD m]
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofZeros_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0),
  (CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg).right =
    CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- **Alias** of `CategoryTheory.Functor.PreservesMonomorphisms.of_iso`. -/
CategoryTheory.Functor.preservesMonomorphisms.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [F.PreservesMonomorphisms] (α : F ≅ G), G.PreservesMonomorphisms
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.ae_prod_iff_ae_ae : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {p : α × β → Prop},
  MeasurableSet {x | p x} → ((∀ᵐ (z : α × β) ∂μ.prod ν, p z) ↔ ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, p (x, y))
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α}, m.getKeyD a fallback = (m.getKey? a).getD fallback
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.projectMapAux.eq_8 : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (x x_1 Y : CategoryTheory.FreeMonoidalCategory C) (f_1 : x.Hom Y) (g : Y.Hom x_1),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f (f_1.comp g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeMonoidalCategory.projectMapAux f f_1)
      (CategoryTheory.FreeMonoidalCategory.projectMapAux f g)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc_exact : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' : κ),
  (c r).prev pq' = pq →
    ∀ (i₀ i₁ i₂ i₃ i₃' : ι) (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq')
      (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
      [X.HasSpectralSequence data]
      (hn₁ :
        autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc_exact._auto_1)
      (hn₂ :
        autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc_exact._auto_3),
      (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃
          i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).Exact
-- Mathlib.CategoryTheory.Limits.Skeleton
CategoryTheory.Limits.hasColimitsOfSize_thinSkeleton : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] [Quiver.IsThin C]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₂, u₂} C],
  CategoryTheory.Limits.HasColimitsOfSize.{w, w', u₂, u₂} (CategoryTheory.ThinSkeleton C)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableOn.mul : ∀ {𝕜 : 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] {s : Set M} {F' : Type u_21} [inst_6 : NormedRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'}, MDiff[s] p → MDiff[s] q → MDiff[s] (p * q)
-- Mathlib.Topology.Compactness.Paracompact
ParacompactSpace.of_hasBasis : ∀ {X : Type v} [inst : TopologicalSpace X] {ι : X → Sort u_1} {p : (x : X) → ι x → Prop} {s : (x : X) → ι x → Set X},
  (∀ (x : X), (nhds x).HasBasis (p x) (s x)) →
    (∀ (f : (x : X) → ι x),
        (∀ (x : X), p x (f x)) →
          ∃ β t, (∀ (b : β), IsOpen (t b)) ∧ ⋃ b, t b = Set.univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ x, t b ⊆ s x (f x)) →
      ParacompactSpace X
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.instDistribSMulOfIsScalarTower : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      (f : Polynomial R) → [inst_1 : DistribSMul S R] → [IsScalarTower S R R] → DistribSMul S (AdjoinRoot f)
-- Mathlib.Algebra.Group.TransferInstance
Equiv.mulEquiv_apply : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Mul β] (a : α), e.mulEquiv a = e a
-- Mathlib.Algebra.GroupWithZero.Action.Defs
smul_sub : ∀ {M : Type u_1} {A : Type u_7} [inst : AddGroup A] [inst_1 : DistribSMul M A] (r : M) (x y : A),
  r • (x - y) = r • x - r • y
-- Mathlib.Order.Filter.NAry
Filter.map_prod_eq_map₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (m : α → β → γ) (f : Filter α) (g : Filter β),
  Filter.map (fun p => m p.1 p.2) (f ×ˢ g) = Filter.map₂ m f g
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.IterM.length_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.submodule_eq_bot_iff : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {m : Submodule S M}
  {f : M →ₗ[S] M}, LinearMap.IsProj m f → (m = ⊥ ↔ f = 0)
-- Mathlib.Computability.Reduce
ManyOneEquiv.symm : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α → Prop} {q : β → Prop},
  ManyOneEquiv p q → ManyOneEquiv q p
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHom_comp : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  [ContinuousMap.UniqueHom R A] (f : C(↑(spectrum R a), R)) (f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))),
  (∀ (x : ↑(spectrum R a)), f x = ↑(f' x)) →
    ∀ (g : C(↑(spectrum R ((cfcHom ha) f)), R)), (cfcHom ha) (g.comp f') = (cfcHom ⋯) g
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
/-- The conditional cdf tends to 0 at -∞ for all `a : α`.  -/
ProbabilityTheory.tendsto_condCDF_atBot : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α),
  Filter.Tendsto (↑(ProbabilityTheory.condCDF ρ a)) Filter.atBot (nhds 0)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_eq_zero_iff : ∀ {A : Type u_2} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [CStarRing A] [inst_3 : NormedSpace ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] {a : A}, CFC.abs a = 0 ↔ a = 0
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_ne_zero : Cardinal.continuum ≠ 0
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instSemiring : (R : Type u_1) → (X : Type u_2) → [inst : CommSemiring R] → Semiring (FreeAlgebra R X)
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.instMin : {X : Type u_2} → [inst : TopologicalSpace X] → Min (DiscreteQuotient X)
-- Mathlib.Data.Multiset.Defs
Multiset.nodup_of_le : ∀ {α : Type u_1} {s t : Multiset α}, s ≤ t → t.Nodup → s.Nodup
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.mkExpectedDefEqMsg : Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.iff_exponent_eq_card : ∀ {α : Type u_1} [inst : CommGroup α] [Finite α], IsCyclic α ↔ Monoid.exponent α = Nat.card α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negAddY_of_X_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → W.negAddY P Q = (-WeierstrassCurve.Jacobian.addU P Q) ^ 3