mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_eq_zero_of_dvd_of_eval_eq_zero : ∀ {R : Type u} [inst : CommSemiring R] {p q : Polynomial R} {x : R},
  p ∣ q → Polynomial.eval x p = 0 → Polynomial.eval x q = 0
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.preimage_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 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (f : P₁ ≃ᴬ[k] P₂) (s : Set P₁), ⇑f.symm ⁻¹' s = ⇑f '' s
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.str : (C : CategoryTheory.Cat) → CategoryTheory.Category.{v, u} ↑C
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
contentRegular_rieszContent : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  [inst_1 : T2Space X] [inst_2 : LocallyCompactSpace X], (rieszContent Λ).ContentRegular
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.AnalyzeResult.mk.sizeOf_spec : ∀ (maxS? : Option FBinopElab.SRec) (hasUncomparable : Bool),
  sizeOf { maxS? := maxS?, hasUncomparable := hasUncomparable } = 1 + sizeOf maxS? + sizeOf hasUncomparable
-- Mathlib.Topology.Algebra.Support
mulTSupport_comp_eq_preimage : ∀ {X : Type u_1} {α : Type u_2} [inst : One α] [inst_1 : TopologicalSpace X] {Y : Type u_9}
  [inst_2 : TopologicalSpace Y] (g : Y → α) (f : X ≃ₜ Y), mulTSupport (g ∘ ⇑f) = ⇑f ⁻¹' mulTSupport g
-- Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
WithTop.measurable_untopA : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  [inst_3 : MeasurableSpace ι] [BorelSpace ι] [inst_5 : Nonempty ι], Measurable WithTop.untopA
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params.extraInj : Lean.Meta.Grind.Params → Lean.PArray Lean.Meta.Grind.InjectiveTheorem
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.hom_comp : ∀ {M N T : CommMonCat} (f : M ⟶ N) (g : N ⟶ T),
  CommMonCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (CommMonCat.Hom.hom g).comp (CommMonCat.Hom.hom f)
-- Init.Data.SInt.Lemmas
Int32.ofNat_sub : ∀ (a b : ℕ), b ≤ a → Int32.ofNat (a - b) = Int32.ofNat a - Int32.ofNat b
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.finite : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S}, P.ker.FG → Module.Finite S P.Cotangent
-- Mathlib.LinearAlgebra.Projection
Submodule.prodEquivOfIsCompl_symm_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : E),
  (p.prodEquivOfIsCompl q hpq).symm x = ((p.projectionOnto q hpq) x, (q.projectionOnto p ⋯) x)
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
/-- This is an enumeration of the `p + 1` nondegenerate dimension-`(p + 1)`
simplices of `Δ[p] ⊗ Δ[1]`. It sends `i : Fin (p + 1)` to the nondegenerate
simplex consisting of the vertices
`(0, 0) ≤ (1,0) ≤ ... ≤ (i, 0) ≤ (i, 1) ≤ ... ≤ (p, 1)`.  -/
SSet.prodStdSimplex.nonDegenerateEquiv₁ : {p : ℕ} →
  Fin (p + 1) ≃
    ↑((CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
            (SSet.stdSimplex.obj { len := 1 })).nonDegenerate
        (p + 1))
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false → (m.insertMany l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.Analysis.SpecificLimits.Normed
tsum_geometric_of_norm_lt_one : ∀ {K : Type u_4} [inst : NormedDivisionRing K] {ξ : K}, ‖ξ‖ < 1 → ∑' (n : ℕ), ξ ^ n = (1 - ξ)⁻¹
-- Mathlib.Topology.DiscreteSubset
mem_codiscreteWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S T : Set X},
  S ∈ Filter.codiscreteWithin T ↔ ∀ x ∈ T, Disjoint (nhdsWithin x {x}ᶜ) (Filter.principal (T \ S))
-- Mathlib.RingTheory.PowerBasis
PowerBasis.lift_aeval : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (y : S')
  (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) (f : Polynomial A),
  (pb.lift y hy) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval y) f
-- Init.Data.List.MapIdx
List.mapFinIdx_cons : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {a : α} {f : (i : ℕ) → α → i < l.length + 1 → β},
  (a :: l).mapFinIdx f = f 0 a ⋯ :: l.mapFinIdx fun i a h => f (i + 1) a ⋯
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
/-- Expression for `hurwitzZeta a 1` as a limit. (Mathematically `hurwitzZeta a 1` is
undefined, but our construction assigns some value to it; this lemma is mostly of interest for
determining what that value is).  -/
HurwitzZeta.tendsto_hurwitzZeta_sub_one_div_nhds_one : ∀ (a : UnitAddCircle),
  Filter.Tendsto (fun s => HurwitzZeta.hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) (nhds 1)
    (nhds (HurwitzZeta.hurwitzZeta a 1))
-- Mathlib.Order.Types.Defs
OrderType.type_ne_zero_iff : ∀ {α : Type u} [inst : LinearOrder α], OrderType.type α ≠ 0 ↔ Nonempty α
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_sub : ∀ {f g : ℕ → ENNReal}, ∑' (i : ℕ), g i ≠ ⊤ → g ≤ f → ∑' (i : ℕ), (f i - g i) = ∑' (i : ℕ), f i - ∑' (i : ℕ), g i
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_ite : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f g : β → α}
  (p : β → Prop) [inst_2 : DecidablePred p],
  (s.inf fun i => if p i then f i else g i) = (Finset.filter p s).inf f ⊓ {i ∈ s | ¬p i}.inf g
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivWithinAt_ofNat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (n : ℕ) [inst_7 : OfNat F n] (x : E) (s : Set E),
  HasFDerivWithinAt (OfNat.ofNat n) 0 s x
-- Mathlib.Analysis.Fourier.LpSpace
MeasureTheory.Lp.instFourierInvAdd : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E],
  FourierInvAdd ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)
-- Mathlib.CategoryTheory.Category.Quiv
/-- The universal property of the path category of a quiver.  -/
CategoryTheory.Quiv.pathsEquiv : {V : Type u} →
  {C : Type u₁} →
    [inst : Quiver V] →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor (CategoryTheory.Paths V) C ≃ V ⥤q C
-- Mathlib.RingTheory.Smooth.Kaehler
sectionOfRetractionKerToTensorAux_algebraMap : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] (l : TensorProduct P S Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S)))
  (hl : l ∘ₗ KaehlerDifferential.kerToTensor R P S = LinearMap.id) (σ : S → P)
  (hσ : ∀ (x : S), (algebraMap P S) (σ x) = x) [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S]
  (hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥) (x : P),
  (sectionOfRetractionKerToTensorAux l hl σ hσ hf') ((algebraMap P S) x) =
    x - ↑(l (1 ⊗ₜ[P] (KaehlerDifferential.D R P) x))
-- Init.Data.Option.Attach
Option.unattach_attach : ∀ {α : Type u_1} (o : Option α), o.attach.unattach = o
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.erase_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α}, ∅.erase k = ∅
-- Mathlib.Topology.Separation.Regular
ULift.instT4Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T4Space X], T4Space (ULift.{u_3, u_1} X)
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.visitGoal : Lean.Environment → Aesop.Goal → Lean.MetaM (Option (Lean.MVarId × Array Aesop.RappRef × Lean.Environment))
-- Mathlib.Topology.Compactness.Lindelof
IsHereditarilyLindelof.isLindelof : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsHereditarilyLindelof s → IsLindelof s
-- Mathlib.Data.Finset.Lattice.Fold
Finset.le_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {b : β},
  b ∈ s → f b ≤ s.sup f
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.instLawfulMonadPostconditionT : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m], LawfulMonad (Std.Iterators.PostconditionT m)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_le_preAleph : ∀ {o₁ o₂ : Ordinal.{u_1}}, Cardinal.preAleph o₁ ≤ Cardinal.preAleph o₂ ↔ o₁ ≤ o₂
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.genWeightSpaceOf.congr_simp : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ χ_1 : R),
  χ = χ_1 → ∀ (x x_1 : L), x = x_1 → LieModule.genWeightSpaceOf M χ x = LieModule.genWeightSpaceOf M χ_1 x_1
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.removeNeutrals.loop.match_3.eq_2 : ∀ (motive : List ℕ → Sort u_1) (h_1 : (x : ℕ) → (xs : List ℕ) → motive (x :: xs)) (h_2 : Unit → motive []),
  (match [] with
    | x :: xs => h_1 x xs
    | [] => h_2 ()) =
    h_2 ()
-- Mathlib.Order.Partition.Basic
Partition.mem_top_iff : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α] {a : α}, a ∈ ⊤ ↔ a = s ∧ a ≠ ⊥
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf'_neg : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Neg α] [inst_2 : SemilatticeInf β] {s : Finset α}
  (hs : (-s).Nonempty) (f : α → β), (-s).inf' hs f = s.inf' ⋯ fun x => f (-x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termX₁_1 : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.norm_map' : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Semiring R] [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {E : Type u_11} {E₂ : Type u_12}
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (self : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E), ‖self.toLinearEquiv x‖ = ‖x‖
-- Mathlib.Topology.Algebra.Group.Torsor
Filter.Tendsto.vsub : ∀ {V : Type u_1} {P : Type u_2} {α : Type u_3} [inst : AddGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] {l : Filter α} {f g : α → P}
  {x y : P}, Filter.Tendsto f l (nhds x) → Filter.Tendsto g l (nhds y) → Filter.Tendsto (f -ᵥ g) l (nhds (x -ᵥ y))
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
LinearMap.mkContinuousOfExistsBound_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : Ring 𝕜₂]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜₂ F]
  {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (h : ∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) (x : E), (f.mkContinuousOfExistsBound h) x = f x
-- Mathlib.Algebra.Group.Pi.Lemmas
OneHom.coe_mulSingle : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → One (f i)] (i : I),
  ⇑(OneHom.mulSingle f i) = Pi.mulSingle i
-- Mathlib.Data.List.Sort
List.sortedLE_iff_isChain : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLE ↔ List.IsChain (fun x1 x2 => x1 ≤ x2) l
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_pointReflection : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x : P} (y : P), x ∈ s → s.WOppSide y ((AffineEquiv.pointReflection R x) y)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Disjoint union of two pre-`0`-hypercovers.  -/
CategoryTheory.PreZeroHypercover.sum : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      CategoryTheory.PreZeroHypercover X → CategoryTheory.PreZeroHypercover X → CategoryTheory.PreZeroHypercover X
-- Mathlib.NumberTheory.FactorisationProperties
/-- `abundancyIndex n` is the sum of the divisors of `n` divided by `n`.  -/
Nat.abundancyIndex : ℕ → ℚ
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.eq_1 : ∀ {G : Type u} [inst : AddGroup G] {A' A B' B : AddSubgroup G} [hAN : (A'.addSubgroupOf A).Normal]
  [hBN : (B'.addSubgroupOf B).Normal] (h' : A' = B') (h : A = B),
  QuotientAddGroup.equivQuotientAddSubgroupOfOfEq h' h =
    (QuotientAddGroup.quotientMapAddSubgroupOfOfLe ⋯ ⋯).toAddEquiv (QuotientAddGroup.quotientMapAddSubgroupOfOfLe ⋯ ⋯) ⋯
      ⋯
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.GeometricallyIntegral.of_geometricallyReduced_of_geometricallyIrreducible : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyReduced f]
  [AlgebraicGeometry.GeometricallyIrreducible f], AlgebraicGeometry.GeometricallyIntegral f
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.HasProjectiveResolution.out : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {Z : C} [self : CategoryTheory.HasProjectiveResolution Z],
  Nonempty (CategoryTheory.ProjectiveResolution Z)
-- Mathlib.Data.Finset.Preimage
Finset.preimage_union : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α → β} {s t : Finset β}
  (hst : Set.InjOn f (f ⁻¹' ↑(s ∪ t))), (s ∪ t).preimage f hst = s.preimage f ⋯ ∪ t.preimage f ⋯
-- Lean.DocString
/-- Finds the docstring for a name, taking tactic alternate forms and documentation extensions into
account.

Use `Lean.findSimpleDocString?` to look up the raw docstring without resolving alternate forms or
including extensions.
 -/
Lean.findDocString? : Lean.Environment →
  Lean.Name →
    optParam Bool true →
      optParam Lean.Options ∅ →
        optParam Lean.Name Lean.Name.anonymous → optParam (List Lean.OpenDecl) [] → IO (Option String)
-- Mathlib.Topology.MetricSpace.IsometricSMul
Pi.isIsometricSMul' : ∀ {ι : Type u_4} {M : ι → Type u_2} {X : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → SMul (M i) (X i)]
  [inst_2 : (i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsIsometricSMul (M i) (X i)],
  IsIsometricSMul ((i : ι) → M i) ((i : ι) → X i)
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_sum_le : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {ι : Type u_3} {s : Finset ι} {f : ι → α → E},
  (∀ i ∈ s, MeasureTheory.MemLp (f i) p μ) →
    1 ≤ p → MeasureTheory.lpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, MeasureTheory.lpNorm (f i) p μ
-- Mathlib.CategoryTheory.Skeletal
/-- Construct the skeleton category as the induced category on the isomorphism classes, and derive
its category structure.
 -/
CategoryTheory.Skeleton : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Type u₁
-- Mathlib.Data.Nat.MaxPowDiv
/-- Find largest `k : ℕ` such that `p ^ k ∣ n` for any `p : ℕ`, as well as the ratio `n / p ^ k`.

The implementation recurses from `(p, n)` to `(p * p, n)`,
so the recursion depth is $$O(\log(\nu_p(n)))$$, thus it is $$O(\log(\log(n)))$$.
 -/
Nat.maxPowDvdDiv : ℕ → ℕ → ℕ × ℕ
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin.stx.inj : ∀ {id : Lean.Name} {ref : Lean.Syntax} {id_1 : Lean.Name} {ref_1 : Lean.Syntax},
  Lean.Meta.Grind.Origin.stx id ref = Lean.Meta.Grind.Origin.stx id_1 ref_1 → id = id_1 ∧ ref = ref_1
-- Mathlib.LinearAlgebra.Finsupp.LSum
/-- A slight rearrangement from `lsum` gives us
the bijection underlying the free-forgetful adjunction for R-modules.
 -/
Finsupp.lift : (M : Type u_2) →
  (R : Type u_5) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (X : Type u_9) → (X → M) ≃+ ((X →₀ R) →ₗ[R] M)
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsion_int : ∀ {G : Type u_3} [inst : AddCommGroup G], (Submodule.torsion ℤ G).toAddSubgroup = AddCommGroup.torsion G
-- Mathlib.Combinatorics.Matroid.Basic
/-- create a copy of `M : Matroid α` with independence and base predicates and ground set defeq
to supplied arguments that are provably equal to those of `M`.  -/
Matroid.copy : {α : Type u_1} →
  (M : Matroid α) →
    (E : Set α) →
      (IsBase Indep : Set α → Prop) →
        E = M.E → (∀ (B : Set α), IsBase B ↔ M.IsBase B) → (∀ (I : Set α), Indep I ↔ M.Indep I) → Matroid α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.beq_iff_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α] [inst_3 : (k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)],
  (↑m₁).WF → (↑m₂).WF → (m₁.beq m₂ = true ↔ (↑m₁).Equiv ↑m₂)
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.AbelMode.term.sizeOf_spec : sizeOf Mathlib.Tactic.Abel.AbelMode.term = 1
-- Init.WF
Prod.lexAccessible : ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a : α},
  Acc ra a → (∀ (b : β), Acc rb b) → ∀ (b : β), Acc (Prod.Lex ra rb) (a, b)
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.map_ofLE : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}
  {A A' : DiscreteQuotient X} {B : DiscreteQuotient Y} (cond : DiscreteQuotient.LEComap f A B) (h : A' ≤ A)
  (c : Quotient A'.toSetoid), DiscreteQuotient.map f cond (DiscreteQuotient.ofLE h c) = DiscreteQuotient.map f ⋯ c
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.completeMultipartiteGraph.not_cliqueFree_of_le_enatCard : ∀ {n : ℕ} {ι : Type u_3} (V : ι → Type u_4) (f : (i : ι) → V i),
  ↑n ≤ ENat.card ι → ¬(SimpleGraph.completeMultipartiteGraph V).CliqueFree n
-- Mathlib.RingTheory.Flat.Basic
/-- Free `R`-modules over discrete types are flat.  -/
Module.Flat.finsupp : ∀ {R : Type u} [inst : CommSemiring R] (ι : Type v), Module.Flat R (ι →₀ R)
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.isUniformEmbedding_comp : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {δ : Type u_2}
  [inst_2 : UniformSpace δ] (g : C(β, δ)), IsUniformEmbedding ⇑g → IsUniformEmbedding g.comp
-- Mathlib.Order.Basic
Eq.not_gt : ∀ {α : Type u_2} [inst : Preorder α] {a b : α}, a = b → ¬b < a
-- Mathlib.Logic.Basic
exists_exists_and_exists_and_eq_and : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β → γ} {p : α → Prop} {q : β → Prop} {r : γ → Prop},
  (∃ c, (∃ a, p a ∧ ∃ b, q b ∧ f a b = c) ∧ r c) ↔ ∃ a, p a ∧ ∃ b, q b ∧ r (f a b)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₂₁.sq : (SSet.stdSimplex.face {1}).BicartSq (SSet.stdSimplex.face {0, 1}) (SSet.stdSimplex.face {1, 2}) (SSet.horn 2 1)
-- Mathlib.Order.Interval.Finset.Defs
Finset.map_subtype_embedding_Iio : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrderBot α]
  (a : Subtype p),
  (∀ ⦃a x : α⦄, x ≤ a → p a → p x) → Finset.map (Function.Embedding.subtype p) (Finset.Iio a) = Finset.Iio ↑a
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
SubmodulesRingBasis.mk : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {B : ι → Submodule R A},
  (∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j) →
    (∀ (a : A) (i : ι), ∃ j, a • B j ≤ B i) → (∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)) → SubmodulesRingBasis B
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The leftmost object of `F : ComposableArrows C n`.  -/
CategoryTheory.ComposableArrows.left : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {n : ℕ} → CategoryTheory.ComposableArrows C n → C
-- Mathlib.Data.List.Cycle
/-- The `s : Cycle α` contains no duplicates.  -/
Cycle.Nodup : {α : Type u_1} → Cycle α → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The comparison morphism for the kernel of `f`.
This is an isomorphism iff `G` preserves the kernel of `f`; see
`Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean`
 -/
CategoryTheory.Limits.kernelComparison : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          {D : Type u₂} →
            [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
              [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
                (G : CategoryTheory.Functor C D) →
                  [G.PreservesZeroMorphisms] →
                    [inst_5 : CategoryTheory.Limits.HasKernel f] →
                      [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)] →
                        G.obj (CategoryTheory.Limits.kernel f) ⟶ CategoryTheory.Limits.kernel (G.map f)
-- Mathlib.CategoryTheory.Functor.CurryingThree
/-- Currying a functor in three variables.  -/
CategoryTheory.Functor.curry₃ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_4} →
      {E : Type u_9} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] →
              [inst_3 : CategoryTheory.Category.{v_9, u_9} E] →
                CategoryTheory.Functor (CategoryTheory.Functor (C₁ × C₂ × C₃) E)
                  (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)))
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addZ_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P Q : Fin 3 → R) (u v : R),
  W'.addZ (u • P) (v • Q) = (u * v) ^ 2 * W'.addZ P Q
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.liftCLM_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : ContinuousAdd M] [inst_5 : ContinuousConstSMul R M]
  [inst_6 : Semiring S] [inst_7 : AddCommMonoid N] [inst_8 : Module S N] [inst_9 : TopologicalSpace N] {σ : R →+* S}
  (f : M →SL[σ] N) (hf : ∀ (x y : M), Inseparable x y → f x = f y) (a : SeparationQuotient M),
  (SeparationQuotient.liftCLM f hf) a = SeparationQuotient.lift (⇑f) hf a
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- The comparison map between two completions of the same uniform space.  -/
AbstractCompletion.compare : {α : Type uα} →
  [inst : UniformSpace α] →
    (pkg : AbstractCompletion.{vα, uα} α) → (pkg' : AbstractCompletion.{vα', uα} α) → pkg.space → pkg'.space
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderivWithin_zero_of_not_accPt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E},
  ¬AccPt x (Filter.principal s) → fderivWithin 𝕜 f s x = 0
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_one' : ∀ {α : Type u} [inst : Monoid α] {x : Invertible 1}, ⅟1 = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α},
  t.WF → Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.map f t) k = Option.map (f k) (Std.DTreeMap.Raw.Const.get? t k)