mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_eq_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = true → t.minKey! = default
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateUnboxImp : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu → Lean.FVarId → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.age.nonempty : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M], (L.age M).Nonempty
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.ProjectiveSpectrum.comapFun_asHomogeneousIdeal : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B] [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B]
  {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜] [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  (p : ProjectiveSpectrum ℬ),
  (AlgebraicGeometry.ProjectiveSpectrum.comapFun f hf p).asHomogeneousIdeal =
    HomogeneousIdeal.comap f p.asHomogeneousIdeal
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_mulHom_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β],
  Function.Injective fun f => ↑f
-- Mathlib.RingTheory.DedekindDomain.Different
/-- Transitivity of the different ideal.  -/
differentIdeal_eq_differentIdeal_mul_differentIdeal : ∀ (A : Type u_1) (B : Type u_4) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [IsIntegrallyClosed A] [inst_5 : IsDedekindDomain B] [inst_6 : Module.IsTorsionFree A B] (C : Type u_3)
  [inst_7 : IsDomain B] [inst_8 : CommRing C] [inst_9 : Algebra B C] [inst_10 : Algebra A C]
  [inst_11 : IsDedekindDomain C] [Module.Finite A B] [Module.Finite A C] [Module.Finite B C]
  [inst_15 : Module.IsTorsionFree A C] [inst_16 : Module.IsTorsionFree B C] [IsScalarTower A B C]
  [Algebra.IsSeparable (FractionRing A) (FractionRing C)],
  differentIdeal A C = differentIdeal B C * Ideal.map (algebraMap B C) (differentIdeal A B)
-- Mathlib.Algebra.Group.Action.Prod
Prod.mulAction : {M : Type u_1} →
  {α : Type u_5} → {β : Type u_6} → [inst : Monoid M] → [MulAction M α] → [MulAction M β] → MulAction M (α × β)
-- Init.Util
/-- Compares two objects for pointer equality.

Two objects are pointer-equal if, at runtime, they are allocated at exactly the same address. This
function is unsafe because it can distinguish between definitionally equal values.
 -/
ptrEq : {α : Type u_1} → α → α → Bool
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.IsocrystalHom.mk.sizeOf_spec : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {k : Type u_1} [inst_1 : CommRing k] [inst_2 : CharP k p]
  [inst_3 : PerfectRing k p] {V : Type u_2} [inst_4 : AddCommGroup V] [inst_5 : WittVector.Isocrystal p k V]
  {V₂ : Type u_3} [inst_6 : AddCommGroup V₂] [inst_7 : WittVector.Isocrystal p k V₂] [inst_8 : SizeOf k]
  [inst_9 : SizeOf V] [inst_10 : SizeOf V₂] (toLinearMap : V →ₗ[FractionRing (WittVector p k)] V₂)
  (frob_equivariant :
    ∀ (x : V),
      (WittVector.Isocrystal.frobenius p k) (toLinearMap x) = toLinearMap ((WittVector.Isocrystal.frobenius p k) x)),
  sizeOf { toLinearMap := toLinearMap, frob_equivariant := frob_equivariant } = 1 + sizeOf toLinearMap
-- Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
/-- **Alias** of `MeasureTheory.measure_setOfPred_frequently_eq_zero`.

---

A version of the **Borel-Cantelli lemma**: if `pᵢ` is a sequence of predicates such that
`∑' i, μ {x | pᵢ x}` is finite, then the measure of `x` such that `pᵢ x` holds frequently as `i → ∞`
(or equivalently, `pᵢ x` holds for infinitely many `i`) is equal to zero.  -/
MeasureTheory.measure_setOf_frequently_eq_zero : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {p : ℕ → α → Prop}, ∑' (i : ℕ), μ {x | p i x} ≠ ⊤ → μ {x | ∃ᶠ (n : ℕ) in Filter.atTop, p n x} = 0
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.instRingColimitType : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → Ring (RingCat.Colimits.ColimitType F)
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.add.injEq : ∀ (a b a_1 b_1 : Int.Internal.Linear.Expr), (a.add b = a_1.add b_1) = (a = a_1 ∧ b = b_1)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.lintegral_toKernel_mem : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → StieltjesFunction ℝ}
  [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) {s : Set (β × ℝ)},
  MeasurableSet s →
    ∫⁻ (b : β), ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' s) ∂ν a = (κ a) s
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor.mk.sizeOf_spec : ∀ (toPreprocessorBase : Mathlib.Tactic.Linarith.PreprocessorBase)
  (transform : Lean.MVarId → List Lean.Expr → Lean.MetaM (List Mathlib.Tactic.Linarith.Branch)),
  sizeOf { toPreprocessorBase := toPreprocessorBase, transform := transform } = 1 + sizeOf toPreprocessorBase
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.iSup_pow_natCast : ∀ {o : Ordinal.{u_1}}, 0 < o → ⨆ n, o ^ n = o ^ Ordinal.omega0
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
groupCohomology.inhomogeneousCochains.ext : ∀ {k G : Type u} [inst : CommRing k] {n : ℕ} [inst_1 : Group G] {A : Rep.{u, u, u} k G}
  {x y : ↑((groupCohomology.inhomogeneousCochains A).X n)}, (∀ (g : Fin n → G), x g = y g) → x = y
-- Lean.Server.GoTo
Lean.Server.instToJsonGoToKind.toJson : Lean.Server.GoToKind → Lean.Json
-- Mathlib.RingTheory.Bialgebra.Convolution
BialgHom.toLinearMap_convMul : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R C] [inst_5 : Coalgebra.IsCocomm R C] (f g : WithConv (C →ₐc[R] A)),
  WithConv.toConv (f * g).ofConv.toLinearMap =
    WithConv.toConv f.ofConv.toLinearMap * WithConv.toConv g.ofConv.toLinearMap
-- Mathlib.Data.Multiset.Dedup
Multiset.subset_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s ⊆ s.dedup
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instSubOfContinuousSub.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Sub β]
  [inst_3 : ContinuousSub β],
  ContinuousMap.instSubOfContinuousSub = { sub := fun f g => { toFun := ⇑f - ⇑g, continuous_toFun := ⋯ } }
-- Init.Data.Array.Set
/-- Replaces the element at a given index in an array.

No bounds check is performed, but the function requires a proof that the index is in bounds. This
proof can usually be omitted, and will be synthesized automatically.

The array is modified in-place if there are no other references to it.

Examples:
* `#[0, 1, 2].set 1 5 = #[0, 5, 2]`
* `#["orange", "apple"].set 1 "grape" = #["orange", "grape"]`
 -/
Array.set : {α : Type u_1} → (xs : Array α) → (i : ℕ) → α → autoParam (i < xs.size) Array.set._auto_1 → Array α
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasFDerivAt.const_cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E}
  {c : ℂ}, HasFDerivAt f f' x → c ≠ 0 ∨ f x ≠ 0 → HasFDerivAt (fun x => c ^ f x) ((c ^ f x * Complex.log c) • f') x
-- Mathlib.RingTheory.Ideal.Basic
Ring.exists_not_isUnit_of_not_isField : ∀ {R : Type u_5} [inst : CommSemiring R] [Nontrivial R], ¬IsField R → ∃ x, ∃ (_ : x ≠ 0), ¬IsUnit x
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.IsFredholm.finite_coker : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F}, u.IsFredholm → (↑u).range.CoFG
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
/-- If `d : MultispanIndex J C`, `c : Multicofork d` and `F : C ⥤ D`,
this is the induced multicofork of `d.map F`.  -/
CategoryTheory.Limits.Multicofork.map : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {J : CategoryTheory.Limits.MultispanShape} →
          {d : CategoryTheory.Limits.MultispanIndex J C} →
            CategoryTheory.Limits.Multicofork d →
              (F : CategoryTheory.Functor C D) → CategoryTheory.Limits.Multicofork (d.map F)
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.Comonad.comul_counit_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t]
  {Z : a ⟶ a} (h : CategoryTheory.CategoryStruct.comp t (CategoryTheory.CategoryStruct.id a) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.Comonad.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft t CategoryTheory.Bicategory.Comonad.counit) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor t).inv h
-- Mathlib.LinearAlgebra.TensorPower.Basic
/-- The tensor powers form a graded algebra.

Note that this instance implies `Algebra R (⨁ n : ℕ, ⨂[R]^n M)` via `DirectSum.Algebra`.  -/
TensorPower.galgebra : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → DirectSum.GAlgebra R fun i => TensorPower R i M
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
/-- The property of objects that are *equal* to `limit F` for some
functor `F : J ⥤ C` where all `F.obj j` satisfy `P`.  -/
CategoryTheory.ObjectProperty.strictLimitsOfShape : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C →
      (J : Type u') → [CategoryTheory.Category.{v', u'} J] → CategoryTheory.ObjectProperty C
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_basisOneIJK_repr : ∀ {R : Type u_3} (c₁ c₂ c₃ : R) [inst : CommRing R] (q : QuaternionAlgebra R c₁ c₂ c₃),
  ⇑((QuaternionAlgebra.basisOneIJK c₁ c₂ c₃).repr q) = ![q.re, q.imI, q.imJ, q.imK]
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.comap_comp_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {g : γ → α} (κ : ProbabilityTheory.Kernel α β) {f : δ → γ}
  (hf : Measurable f) (hg : Measurable g), κ.comap (g ∘ f) ⋯ = (κ.comap g hg).comap f hf
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_eq_biUnion_closedBall : ∀ {δ : ℝ} {α : Type u_2} [inst : PseudoMetricSpace α] [ProperSpace α] (E : Set α),
  0 ≤ δ → Metric.cthickening δ E = ⋃ x ∈ closure E, Metric.closedBall x δ
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.neg_τ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂), (-φ).τ₁ = -φ.τ₁
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom : ∀ {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).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η.inv) (α.app b))
      (CategoryTheory.CategoryStruct.comp (α.naturality f).hom
        (CategoryTheory.Bicategory.whiskerLeft (α.app a) (G.map₂ η.hom)))
-- Mathlib.Combinatorics.Quiver.Path
/-- Equality is decidable on paths in a quiver given decidable equality on the vertices and
arrows.  -/
Quiver.Path.instDecidableEq : {V : Type u_1} →
  [inst : Quiver V] → [DecidableEq V] → [(v w : V) → DecidableEq (v ⟶ w)] → (v w : V) → DecidableEq (Quiver.Path v w)
-- Std.Sync.Channel
/-- The central state structure for a zero buffer channel. Maintains the following invariants:
1. `producers = ∅ ∨ consumers = ∅`
2. `closed = true → consumers = ∅`
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.State : Type → Type
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_filter_containsKey_of_length_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.DistinctKeys l₂ →
      (∀ (a : α), Std.Internal.List.containsKey a l₂ = true → Std.Internal.List.containsKey a l₁ = true) →
        (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁).length = l₂.length
-- Aesop.Script.SScript
Aesop.Script.SScript.onGoal.inj : ∀ {goalPos : ℕ} {step : Aesop.Script.Step} {tail : Aesop.Script.SScript} {goalPos_1 : ℕ} {step_1 : Aesop.Script.Step}
  {tail_1 : Aesop.Script.SScript},
  Aesop.Script.SScript.onGoal goalPos step tail = Aesop.Script.SScript.onGoal goalPos_1 step_1 tail_1 →
    goalPos = goalPos_1 ∧ step = step_1 ∧ tail = tail_1
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Focus.rewrite_hyps : ∀ {σs : List (Type u_1)} {P Q R : Std.Do.SPred σs}, (P ⊣⊢ₛ Q) → (Q ⊢ₛ R) → P ⊢ₛ R
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.continuous_integral_continuousMap : ∀ {X : Type u_2} [inst : TopologicalSpace X] [CompactSpace X] [inst_2 : MeasurableSpace X]
  [inst_3 : OpensMeasurableSpace X] {F : Type u_3} [inst_4 : FunLike F X ℝ] [ContinuousMapClass F X ℝ] (f : F),
  Continuous fun μ => ∫ (x : X), f x ∂↑μ
-- Mathlib.Data.EReal.Inv
EReal.coe_div : ∀ (a b : ℝ), ↑(a / b) = ↑a / ↑b
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.ofIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.MonObj M] (e : M ≅ X),
  CategoryTheory.MonObj.ofIso e =
    { one := CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom,
      mul :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.inv e.inv)
          (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom),
      one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on a field `K`, the valuation
subring defined by `v` is clopen in the valuative topology.  -/
Valuation.isClopen_valuationSubring : ∀ {Γ₀ : Type u_3} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_4} [inst_1 : Field K] [inst_2 : ValuativeRel K]
  [inst_3 : TopologicalSpace K] [IsValuativeTopology K] (v : Valuation K Γ₀) [v.Compatible],
  IsClopen ↑v.valuationSubring
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.ringEquivOfRingEquivHom.congr_simp : ∀ (A : Type u_8) (K : Type u_9) [inst : CommRing A] [inst_1 : CommRing K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K], IsFractionRing.ringEquivOfRingEquivHom A K = IsFractionRing.ringEquivOfRingEquivHom A K
-- Mathlib.Algebra.Group.Action.Defs
/-- See also `AddMonoid.toAddAction`  -/
instVAddOfAdd : {α : Type u} → [Add α] → VAdd α α
-- Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
ModuleCat.hasProjectiveDimensionLE_of_semiLinearEquiv : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] {R' : Type u'} [inst_2 : Ring R'] [Small.{v', u'} R'] (e : R ≃+* R')
  {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) (n : ℕ) [CategoryTheory.HasProjectiveDimensionLE M n],
  CategoryTheory.HasProjectiveDimensionLE N n
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableWithinAt_neg_iff : ∀ {𝕜 : 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] {f : E → F}
  {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 (-f) s x ↔ DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.pointwise_central_scalar : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R]
  [inst_3 : MulSemiringAction Mᵐᵒᵖ R] [IsCentralScalar M R], IsCentralScalar M (Subsemiring R)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.findSome?.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive x
-- Init.Data.SInt.Lemmas
Int32.toNat_toBitVec_of_le : ∀ {x : Int32}, 0 ≤ x → x.toBitVec.toNat = x.toNatClampNeg
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
/-- The product formula for the infinite adele ring. This is the adelic version of
`NumberField.InfinitePlace.prod_eq_abs_norm`.  -/
NumberField.InfiniteAdeleRing.coe_norm_eq_abs_norm : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : K),
  ‖(algebraMap K (NumberField.InfiniteAdeleRing K)) x‖ = ↑|(Algebra.norm ℚ) x|
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- `mfderiv I I' f x`, given a function `f` between two manifolds, is the derivative of `f` at `x`,
as a continuous linear map from the tangent space at `x` to the tangent space at `f x`.  -/
mfderiv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                (I' : ModelWithCorners 𝕜 E' H') →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        (f : M → M') → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I' (f x)
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.comp_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {S : Type w}
  [inst_2 : CommSemiring S] [inst_3 : CategoryTheory.Linear S C] (X Y Z : C) (f : X ⟶ Y),
  (CategoryTheory.Linear.comp X Y Z) f = CategoryTheory.Linear.leftComp S Z f
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
/-- For a quasi-measure-preserving self-map `f`, if a null measurable set `s` is a.e. invariant,
then it is a.e. equal to a measurable invariant set.
 -/
MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → α},
  MeasureTheory.Measure.QuasiMeasurePreserving f μ μ →
    MeasureTheory.NullMeasurableSet s μ → f ⁻¹' s =ᵐ[μ] s → ∃ t, MeasurableSet t ∧ t =ᵐ[μ] s ∧ f ⁻¹' t = t
-- Lean.Meta.AppBuilder
_private.Lean.Meta.AppBuilder.0.Lean.Meta.mkAppMFinal : Lean.Name → Lean.Expr → Array Lean.Expr → Array Lean.MVarId → Lean.MetaM Lean.Expr
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_erase_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {fallback : β}, (m.erase k).getD k fallback = fallback
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.lt_def : ∀ {x y : ZFSet.{u}}, x ⊂ y ↔ x ⊂ y
-- Mathlib.Topology.Order.IsLUB
DenseRange.exists_seq_strictMono_tendsto_of_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {β : Type u_3}
  [inst_3 : LinearOrder β] [DenselyOrdered α] [FirstCountableTopology α] {f : β → α} {x y : α},
  DenseRange f →
    Monotone f →
      y < x → ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Set.Ioo y x) ∧ Filter.Tendsto (f ∘ u) Filter.atTop (nhds x)
-- Lean.Elab.Calc
Lean.Elab.Term.elabCalcSteps : Array Lean.Elab.Term.CalcStepView → Lean.Elab.TermElabM (Lean.Expr × Lean.Expr)
-- Mathlib.Order.Preorder.Chain
IsChain.singleton : ∀ {α : Type u_1} {r : α → α → Prop} {a : α}, IsChain r {a}
-- Mathlib.Combinatorics.Configuration
/-- A nondegenerate configuration in which every pair of points has a line through them.  -/
Configuration.HasLines : (P : Type u_1) → (L : Type u_2) → [Membership P L] → Type (max u_1 u_2)
-- Init.Data.Nat.Lemmas
/-- Variant of `Nat.lt_div_iff_mul_lt` that assumes `d ∣ n`.  -/
Nat.lt_div_iff_mul_lt' : ∀ {d n : ℕ}, d ∣ n → ∀ (a : ℕ), a < n / d ↔ d * a < n
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore_index : ∀ {m : ℕ} (k : Fin (m + 1)) (n : ℕ) (s : SSet.prodStdSimplex.pairingCore.Type₁ k n),
  (SSet.prodStdSimplex.pairingCore k n).index s = s.index.castSucc
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.HasCoreflexiveEqualizers.has_eq : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasCoreflexiveEqualizers C]
  ⦃A B : C⦄ (f g : A ⟶ B) [CategoryTheory.IsCoreflexivePair f g], CategoryTheory.Limits.HasEqualizer f g
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.pointwiseLeftKanExtension_obj : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasPointwiseLeftKanExtension F] (Y : D),
  (L.pointwiseLeftKanExtension F).obj Y =
    CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F)
-- Mathlib.Order.Filter.Bases.Basic
Filter.hasBasis_biInf_principal' : ∀ {α : Type u_1} {ι : Type u_6} {p : ι → Prop} {s : ι → Set α},
  (∀ (i : ι), p i → ∀ (j : ι), p j → ∃ k, p k ∧ s k ⊆ s i ∧ s k ⊆ s j) →
    (∃ i, p i) → (⨅ i, ⨅ (_ : p i), Filter.principal (s i)).HasBasis p s
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `g` is meromorphic at `x`, then `f - g` is meromorphic at `x` if and only if `f` is meromorphic
at `x`.
 -/
MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E},
  MeromorphicAt g x → (MeromorphicAt (fun z => f z - g z) x ↔ MeromorphicAt f x)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
max_mul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LinearOrder α] [MulRightMono α] (a b c : α), max a b * c = max (a * c) (b * c)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
/-- When $T$ is flat over $S$, the left bottom part of the snake lemma diagram used in
the construction of the connecting homomorphism `Algebra.Generators.H1Cotangent.δ`
naturally extends via a base change map.  -/
Algebra.Generators.H1Cotangent.exact_liftBaseChange_map_of_flat : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) [Module.Flat S T],
  Function.Exact ⇑(LinearMap.liftBaseChange T (Algebra.Extension.H1Cotangent.map (Q.toComp P).toExtensionHom))
    ⇑(Algebra.Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom)