mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.isoInv.inj : ∀ {e : Lean.Expr} {isoLift : Mathlib.Tactic.BicategoryLike.IsoLift} {iso : Mathlib.Tactic.BicategoryLike.Mor₂Iso}
  {e_1 : Lean.Expr} {isoLift_1 : Mathlib.Tactic.BicategoryLike.IsoLift} {iso_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso},
  Mathlib.Tactic.BicategoryLike.Mor₂.isoInv e isoLift iso =
      Mathlib.Tactic.BicategoryLike.Mor₂.isoInv e_1 isoLift_1 iso_1 →
    e = e_1 ∧ isoLift = isoLift_1 ∧ iso = iso_1
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin'_apply' : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (M : Matrix m n R), Matrix.toLin' M = M.mulVecLin
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- Multiple transitivity of a pretransitive action
is equivalent to one less transitivity of stabilizer of a point
[Wielandt, th. 9.1, 1st part][Wielandt-1964].  -/
SubAddAction.ofStabilizer.isMultiplyPretransitive : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] [AddAction.IsPretransitive G α] {n : ℕ}
  {a : α},
  AddAction.IsMultiplyPretransitive G α n.succ ↔
    AddAction.IsMultiplyPretransitive (↥(AddAction.stabilizer G a)) (↥(SubAddAction.ofStabilizer G a)) n
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.instLEValueGroup : (A : Type u) →
  [inst : CommRing A] → (K : Type v) → [inst_1 : Field K] → [inst_2 : Algebra A K] → LE (ValuationRing.ValueGroup A K)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.inductiveElabAttr.unsafe_1 : IO (Lean.KeyedDeclsAttribute Lean.Elab.Command.InductiveElabDescr)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_iso : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (α : F ⟶ G) {a b : B} {f g : a ⟶ b} (η : f ≅ g),
  α.naturality g =
    CategoryTheory.Bicategory.whiskerRightIso (F.map₂Iso η.symm) (α.app b) ≪≫
      α.naturality f ≪≫ CategoryTheory.Bicategory.whiskerLeftIso (α.app a) (G.map₂Iso η)
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidalFunctorComp.eq_1 : ∀ {M : Type u} [inst : Monoid M] {N : Type u'} [inst_1 : Monoid N] {K : Type u} [inst_2 : Monoid K] (F : M →* N)
  (G : N →* K),
  CategoryTheory.Discrete.monoidalFunctorComp F G =
    CategoryTheory.Iso.refl
      ((CategoryTheory.Discrete.monoidalFunctor F).comp (CategoryTheory.Discrete.monoidalFunctor G))
-- Init.Prelude
/-- The "one" element of the type.  -/
One.one : {α : Type u} → [self : One α] → α
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_eq_zero_of_lt_natDegree : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (n : ℕ), p.natDegree < n → (Polynomial.hasseDeriv n) p = 0
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.mul_add_div_right : ∀ {R : Type u} [inst : EuclideanDomain R] (x y z : R), z ≠ 0 → z ∣ y → (x * z + y) / z = x + y / z
-- Mathlib.Data.Num.Lemmas
Num.toNat_injective : Function.Injective castNum
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
/-- The `I`-primaryComponent component of a module `M` where `I` is an ideal of `A`.  -/
Ideal.primaryComponent : {A : Type u_1} →
  (M : Type u_2) → [inst : CommRing A] → Ideal A → [inst_1 : AddCommMonoid M] → [inst_2 : Module A M] → Submodule A M
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
/-- If `|f|` is bounded almost everywhere by `R`, then so is its conditional expectation.  -/
MeasureTheory.ae_bdd_abs_condExp_of_ae_bdd_abs : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E]
  [IsOrderedModule ℝ E] {R : E} {f : α → E}, (∀ᵐ (x : α) ∂μ, |f x| ≤ R) → ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ R
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheorem.mk.injEq : ∀ (levelParams : Array Lean.Name) (proof : Lean.Expr) (numParams : ℕ) (patterns : List Lean.Expr)
  (symbols : List Lean.HeadIndex) (origin : Lean.Meta.Grind.Origin) (kind : Lean.Meta.Grind.EMatchTheoremKind)
  (minIndexable : Bool) (cnstrs : List Lean.Meta.Grind.EMatchTheoremConstraint) (levelParams_1 : Array Lean.Name)
  (proof_1 : Lean.Expr) (numParams_1 : ℕ) (patterns_1 : List Lean.Expr) (symbols_1 : List Lean.HeadIndex)
  (origin_1 : Lean.Meta.Grind.Origin) (kind_1 : Lean.Meta.Grind.EMatchTheoremKind) (minIndexable_1 : Bool)
  (cnstrs_1 : List Lean.Meta.Grind.EMatchTheoremConstraint),
  ({ levelParams := levelParams, proof := proof, numParams := numParams, patterns := patterns, symbols := symbols,
        origin := origin, kind := kind, minIndexable := minIndexable, cnstrs := cnstrs } =
      { levelParams := levelParams_1, proof := proof_1, numParams := numParams_1, patterns := patterns_1,
        symbols := symbols_1, origin := origin_1, kind := kind_1, minIndexable := minIndexable_1,
        cnstrs := cnstrs_1 }) =
    (levelParams = levelParams_1 ∧
      proof = proof_1 ∧
        numParams = numParams_1 ∧
          patterns = patterns_1 ∧
            symbols = symbols_1 ∧ origin = origin_1 ∧ kind = kind_1 ∧ minIndexable = minIndexable_1 ∧ cnstrs = cnstrs_1)
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
IsBoundedBilinearMap.hasStrictFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {b : E × F → G} (h : IsBoundedBilinearMap 𝕜 b) (p : E × F),
  HasStrictFDerivAt b (h.deriv p) p
-- Init.Data.SInt.Lemmas
Int32.toInt_inj : ∀ {x y : Int32}, x.toInt = y.toInt ↔ x = y
-- Std.Data.DTreeMap.Raw.Iterator
Std.DTreeMap.Raw.valuesIter_toList : ∀ {α β : Type u_1} {cmp : α → α → Ordering} (m : Std.DTreeMap.Raw α (fun x => β) cmp), m.valuesIter.toList = m.values
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.desc_inr : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {X : ι → Type u_5}
  (x₁ : (i₁ : ι₁) → X (e₁.f i₁)) (x₂ : (i₂ : ι₂) → X (e₂.f i₂)) (i₂ : ι₂), ac.desc x₁ x₂ (e₂.f i₂) = x₂ i₂
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
LinearMap.finrank_le_finrank_of_injective : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {M' : Type u_2} [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [Module.Finite R M'] {f : M →ₗ[R] M'},
  Function.Injective ⇑f → Module.finrank R M ≤ Module.finrank R M'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_le_size_insertMany : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {ρ : Type w}
  [inst : ForIn Id ρ ((a : α) × β a)] [EquivBEq α] [LawfulHashable α] {l : ρ}, m.size ≤ (m.insertMany l).size
-- Mathlib.Logic.Nonempty
Nonempty.map2 : ∀ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (f : α → β → γ), Nonempty α → Nonempty β → Nonempty γ
-- Mathlib.Data.ENNReal.Basic
/-- **Alias** of the reverse direction of `ENNReal.coe_le_coe`. -/
ENNReal.coe_le_coe_of_le : ∀ {r q : NNReal}, r ≤ q → ↑r ≤ ↑q
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.inv_val_mem_of_mem_units : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) {x : Mˣ}, x ∈ S.units → ↑x⁻¹ ∈ S
-- Lean.Data.Lsp.Basic
Lean.Lsp.SnippetString.mk : String → Lean.Lsp.SnippetString
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.compPartialSumTargetSet_image_compPartialSumSource : ∀ (m M N : ℕ),
  ∀ i ∈ FormalMultilinearSeries.compPartialSumTargetSet m M N,
    ∃ j,
      ∃ (hj : j ∈ FormalMultilinearSeries.compPartialSumSource m M N),
        FormalMultilinearSeries.compChangeOfVariables m M N j hj = i
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegal.mk.sizeOf_spec : ∀ {X : SSet} (spineToSimplex : {n : ℕ} → X.Path n → X.obj (Opposite.op { len := n }))
  (spine_spineToSimplex : ∀ (n : ℕ), X.spine n ∘ spineToSimplex = id)
  (spineToSimplex_spine : ∀ (n : ℕ), spineToSimplex ∘ X.spine n = id),
  sizeOf
      { spineToSimplex := spineToSimplex, spine_spineToSimplex := spine_spineToSimplex,
        spineToSimplex_spine := spineToSimplex_spine } =
    1
-- Std.Tactic.Do.Syntax
/-- `mvcgen_trivial` is the tactic automatically called by `mvcgen` to discharge VCs.
It tries to discharge the VC by applying `(try mpure_intro); trivial` and otherwise delegates to
`mvcgen_trivial_extensible`.
Users are encouraged to extend `mvcgen_trivial_extensible` instead of this tactic in order not to
override the default `(try mpure_intro); trivial` behavior.
 -/
Lean.Parser.Tactic.tacticMvcgen_trivial : Lean.ParserDescr
-- Mathlib.Analysis.Distribution.FourierMultiplier
SchwartzMap.fourierMultiplierCLM_const : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace ℝ E] [inst_4 : NormedSpace ℂ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℂ 𝕜 F] [inst_7 : FiniteDimensional ℝ E] [inst_8 : MeasurableSpace E] [inst_9 : BorelSpace E]
  [CompleteSpace F] (c : 𝕜),
  (SchwartzMap.fourierMultiplierCLM F fun x => c) = c • ContinuousLinearMap.id 𝕜 (SchwartzMap E F)
-- Mathlib.Control.Basic
Sum.instLawfulMonad_mathlib : ∀ {e : Type v}, LawfulMonad (Sum e)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_uniqueRingEquiv_symm : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Subsingleton M] (r : R) (m : M),
  ((MonoidAlgebra.uniqueRingEquiv M).symm r).coeff m = r
-- Init.Data.Nat.Compare
Nat.compare_eq_ite_le : ∀ (a b : ℕ), compare a b = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y),
  ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).map f).fiber =
    CategoryTheory.AsSmall.up.map f.fiber
-- Mathlib.RingTheory.LaurentSeries
PowerSeries.coe_pow : ∀ {R : Type u_1} [inst : Semiring R] (f : PowerSeries R) (n : ℕ),
  (HahnSeries.ofPowerSeries ℤ R) (f ^ n) = (HahnSeries.ofPowerSeries ℤ R) f ^ n
-- Std.Do.WP.Basic
Std.Do.ExceptT.instWP : {m : Type u → Type v} →
  {ps : Std.Do.PostShape} → {ε : Type u} → [Std.Do.WP m ps] → Std.Do.WP (ExceptT ε m) (Std.Do.PostShape.except ε ps)
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.dirac.instSigmaFinite : ∀ {α : Type u_1} [inst : MeasurableSpace α] {a : α}, MeasureTheory.SigmaFinite (MeasureTheory.Measure.dirac a)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.toNormalization_inl_normalizationCoprodIso_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV],
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp iU f))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
        (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).hom) =
    CategoryTheory.CategoryStruct.comp iU (AlgebraicGeometry.Scheme.Hom.toNormalization f)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_eq_cons_iff : ∀ {xs : List ℤ} {m n a : ℤ}, (m...n).toList = a :: xs ↔ m = a ∧ m < n ∧ ((m + 1)...n).toList = xs
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.toDeleteEdges : ∀ {V : Type u} (G : SimpleGraph V) {v w : V} (s : Set (Sym2 V)) {p : G.Walk v w},
  p.IsPath → ∀ (hp : ∀ e ∈ p.edges, e ∉ s), (SimpleGraph.Walk.toDeleteEdges s p hp).IsPath
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
spectrum.pow_mem_pow : ∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A) (n : ℕ) {k : 𝕜},
  k ∈ spectrum 𝕜 a → k ^ n ∈ spectrum 𝕜 (a ^ n)
-- Mathlib.NumberTheory.PrimeCounting
Nat.mem_primesLE : ∀ {p n : ℕ}, p ∈ n.primesLE ↔ p ≤ n ∧ Nat.Prime p
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.ιMulti_family_apply_coe : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Type u_4}
  [inst_3 : LinearOrder I] (v : I → M) (s : ↑(Set.powersetCard I n)),
  ↑(exteriorPower.ιMulti_family R n v s) = ExteriorAlgebra.ιMulti_family R n v s
-- Mathlib.Analysis.Complex.Poisson
/-- The Herglotz–Riesz kernel `herglotzRieszKernel c w` is continuous on the circle `sphere c |R|`
whenever `w ∈ ball c R`.
 -/
continuousOn_herglotzRieszKernel_sphere : ∀ {R : ℝ} {w c : ℂ}, w ∈ Metric.ball c R → ContinuousOn (herglotzRieszKernel c w) (Metric.sphere c |R|)
-- Std.Data.ExtTreeMap.Lemmas
/-- Variant of `getD_map` that holds without `LawfulEqCmp`.  -/
Std.ExtTreeMap.getD_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k : α} {fallback : γ},
  (Std.ExtTreeMap.map f t).getD k fallback = (Option.pmap (fun v h => f (t.getKey k h) v) t[k]? ⋯).getD fallback
-- Mathlib.Tactic.NormNum.OfScientific
Mathlib.Meta.NormNum.isNat_ofScientific_of_false : ∀ {α : Type u_1} [inst : DivisionSemiring α] {m e nm ne n : ℕ},
  Mathlib.Meta.NormNum.IsNat m nm →
    Mathlib.Meta.NormNum.IsNat e ne →
      n = nm.mul (10 ^ ne) → Mathlib.Meta.NormNum.IsNat (OfScientific.ofScientific m false e) n
-- Mathlib.Probability.Kernel.Disintegration.Basic
MeasureTheory.Measure.IsCondKernel.isSFiniteKernel : ∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω))
  (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond], ρ ≠ 0 → ProbabilityTheory.IsSFiniteKernel ρCond
-- Lean.Meta.IndPredBelow
Lean.Meta.IndPredBelow.RecursionContext.mk.injEq : ∀ (belows : Lean.FVarIdMap (Lean.Name × Lean.Expr)) (motives : Lean.FVarIdMap (ℕ × Lean.Expr))
  (belows_1 : Lean.FVarIdMap (Lean.Name × Lean.Expr)) (motives_1 : Lean.FVarIdMap (ℕ × Lean.Expr)),
  ({ belows := belows, motives := motives } = { belows := belows_1, motives := motives_1 }) =
    (belows = belows_1 ∧ motives = motives_1)
-- Mathlib.Algebra.Notation.Indicator
Set.piecewise_eq_mulIndicator : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f : α → M} [inst_1 : DecidablePred fun x => x ∈ s],
  s.piecewise f 1 = s.mulIndicator f
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_add : ∀ {a b : USize} (h : System.Platform.numBits = 64), (a + b).toBitVec64 h = a.toBitVec64 h + b.toBitVec64 h
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorAlgebra.ofDirectSum_of_tprod : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (x : Fin n → M),
  TensorAlgebra.ofDirectSum ((DirectSum.of (fun n => TensorPower R n M) n) ((PiTensorProduct.tprod R) x)) =
    (TensorAlgebra.tprod R M n) x
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.functor_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) {X : T} (Y : CategoryTheory.Over X)
  (Z : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.toOver F X) Y),
  (CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.functor F Y).obj Z =
    CategoryTheory.CostructuredArrow.mk (CategoryTheory.Over.Hom.left Z.hom)
-- Mathlib.Order.BoundedOrder.Monotone
Antitone.ball : ∀ {α : Type u} {β : Type v} [inst : Preorder α] {P : β → α → Prop} {s : Set β},
  (∀ x ∈ s, Antitone (P x)) → Antitone fun y => ∀ x ∈ s, P x y
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.hasLeftHomology_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [S₁.HasLeftHomology], S₂.HasLeftHomology
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  (t.insertManyIfNewUnit l)[k]? = if k ∈ t ∨ l.contains k = true then some () else none
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.isBasis_iff_isBasis_closure_of_subset' : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, I ⊆ X → (M.IsBasis I X ↔ M.IsBasis I (M.closure X) ∧ X ⊆ M.E)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDocumentColorParams.fromJson : Lean.Json → Except String Lean.Lsp.DocumentColorParams
-- Mathlib.Analysis.Convex.Topology
Convex.combo_interior_closure_mem_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s →
    ∀ {x y : E}, x ∈ interior s → y ∈ closure s → ∀ {a b : 𝕜}, 0 < a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ interior s
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.ArrayStxBuilder.build : Lean.Elab.Term.Quotation.ArrayStxBuilder → Lean.Term
-- Mathlib.LinearAlgebra.Dimension.Free
Module.Free.exists_linearMap_injective_of_rank_lt : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  {N : Type v} [inst_4 : AddCommMonoid N] [inst_5 : Module R N],
  Module.rank R M < Module.rank R N → ∃ f, Function.Injective ⇑f
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Expr.instantiateBetaRevRange.visitWithoutBeta : ℕ → ℕ → Array Lean.Expr → Lean.Expr → ℕ → Lean.MonadStateCacheT (Lean.ExprStructEq × ℕ) Lean.Expr Id Lean.Expr
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instDecidableMem : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [inst : EquivBEq α] → [inst_1 : LawfulHashable α] → {m : Std.ExtDHashMap α β} → {a : α} → Decidable (a ∈ m)
-- Init.Data.List.Lemmas
List.insert_append_of_mem_left : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α}, a ∈ l₂ → List.insert a (l₁ ++ l₂) = l₁ ++ l₂
-- Init.Data.UInt.Lemmas
UInt32.toNat_mod : ∀ (a b : UInt32), (a % b).toNat = a.toNat % b.toNat
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Cofix.bisim : ∀ {F : Type u → Type u} [q : QPF F] (r : QPF.Cofix F → QPF.Cofix F → Prop),
  (∀ (x y : QPF.Cofix F), r x y → Functor.Liftr r x.dest y.dest) → ∀ (x y : QPF.Cofix F), r x y → x = y
-- Mathlib.Data.Set.Operations
Set.comp_rangeSplitting : ∀ {α : Type u} {β : Type v} (f : α → β), f ∘ Set.rangeSplitting f = Subtype.val
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.comp_apply : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {FC : outParam (C → C → Type u_1)} {CC : outParam (C → Type w)}
  {inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))} [self : CategoryTheory.ConcreteCategory C FC]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.mem_of_mem_sdiff`. -/
Set.mem_of_mem_diff : ∀ {α : Type u_1} {s t : Set α} {x : α}, x ∈ s \ t → x ∈ s
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
/-- If `q < p` are prime ideals such that `p` is minimal over `span (s ∪ {x})` and
`t` is a set contained in `q` such that `s ⊆ √span (t ∪ {x})`, then `q` is minimal over `span t`.
This is used in the induction step for the proof of Krull's height theorem.  -/
Ideal.mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {q p : Ideal R} [q.IsPrime],
  q < p →
    ∀ (x : R) (s : Set R),
      p ∈ (Ideal.span (insert x s)).minimalPrimes →
        ∀ t ⊆ ↑q, s ⊆ ↑(Ideal.span (insert x t)).radical → q ∈ (Ideal.span t).minimalPrimes
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.vsub_self_of_zero_mem : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  {s : AffineSubspace k V}, 0 ∈ s → ↑s -ᵥ ↑s = ↑s
-- Mathlib.Data.Int.ModEq
Int.existsUnique_equiv_nat : ∀ (a : ℤ) {b : ℤ}, 0 < b → ∃ z, ↑z < b ∧ ↑z ≡ a [ZMOD b]
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.of_sub_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t : Finset α}, (s - t).Nonempty → s.Nonempty
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_bot_ae_eq : ∀ {Ω : Type u_1} {mΩ₀ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (X : Ω → ENNReal),
  P⁻[X | ⊥] =ᵐ[P] fun x => (P Set.univ)⁻¹ • ∫⁻ (ω : Ω), X ω ∂P
-- Mathlib.Analysis.Calculus.Monotone
/-- A real function which is monotone on a set is differentiable Lebesgue-almost everywhere on
this set. This version does not assume that `s` is measurable. For a formulation with
`volume.restrict s` assuming that `s` is measurable, see `MonotoneOn.ae_differentiableWithinAt`.
 -/
MonotoneOn.ae_differentiableWithinAt_of_mem : ∀ {f : ℝ → ℝ} {s : Set ℝ}, MonotoneOn f s → ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardCongr₂_inv_app_val_app_hom_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] [inst_3 : G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S)
  {ψ : T ⟶ (F.sheafPushforwardContinuous RingCat J K).obj S} (e : F ≅ G)
  (he :
    CategoryTheory.CategoryStruct.comp φ
        ((CategoryTheory.Functor.sheafPushforwardContinuousNatTrans e.hom RingCat J K).app S) =
      ψ)
  (X : SheafOfModules S) (x : Cᵒᵖ) (x_1 : ↑(((SheafOfModules.pushforward ψ).obj X).val.obj x)),
  (ModuleCat.Hom.hom (((SheafOfModules.pushforwardCongr₂ φ e he).inv.app X).val.app x)) x_1 =
    (CategoryTheory.CategoryStruct.comp
          (((SheafOfModules.pushforwardNatTrans
                      (CategoryTheory.CategoryStruct.comp φ
                        ((CategoryTheory.Functor.sheafPushforwardContinuousNatTrans e.hom RingCat J K).app S))
                      e.inv).app
                  X).val.app
            x)
          (((SheafOfModules.pushforwardCongr ⋯).hom.app X).val.app x)).hom'
      ((((SheafOfModules.pushforwardCongr he).inv.app X).val.app x).hom' x_1)
-- Mathlib.Algebra.Order.Field.Basic
div_le_div_right_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  c < 0 → (a / c ≤ b / c ↔ b ≤ a)
-- Init.Data.String.Lemmas.StringOrder
String.le_refl : ∀ (a : String), a ≤ a
-- Mathlib.Data.Complex.Basic
Complex.real_smul : ∀ {x : ℝ} {z : ℂ}, x • z = ↑x * z
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The canonical cone over `diagram P` is a limit cone.  -/
ProfiniteGrp.isLimitCone : (P : ProfiniteGrp.{u}) → CategoryTheory.Limits.IsLimit P.cone
-- Mathlib.Algebra.Category.ModuleCat.Localization
ModuleCat.localizedModule.congr_simp : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (M M_1 : ModuleCat R),
  M = M_1 → ∀ (S : Submonoid R), M.localizedModule S = M_1.localizedModule S