mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (t.insertMany l).contains k = (t.contains k || (List.map Sigma.fst l).contains k)
-- Mathlib.Probability.Kernel.Irreducible
ProbabilityTheory.Kernel.IsIrreducible.irreducible : ∀ {α : Type u_1} {mα : MeasurableSpace α} {φ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α α}
  [self : ProbabilityTheory.Kernel.IsIrreducible φ κ] ⦃A : Set α⦄,
  MeasurableSet A → φ A > 0 → ∀ (a : α), ∃ n, ((κ ^ n) a) A > 0
-- Lean.Meta.Tactic.Grind.Main
/-- Checks whether any E-matching lemmas were activated but do not appear in the final proof term.
Controlled by `set_option grind.unusedLemmaThreshold`.
Uses grind's instance-marking infrastructure for precise tracking.
 -/
Lean.Meta.Grind.checkUnusedActivations : Lean.MVarId → Lean.Meta.Grind.Counters → Lean.Meta.Grind.GrindM Unit
-- Lean.Parser.Term
Lean.Parser.Term.byTactic'.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for monotonicity of addition on the right,
namely `a₁ < a₂ → a₁ + b < a₂ + b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedAddMonoid`.  -/
AddRightStrictMono : (M : Type u_1) → [Add M] → [LT M] → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Congr
fderivWithin_eventually_congr_set' : ∀ {𝕜 : 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 t : Set E} [T1Space E] (y : E),
  s =ᶠ[nhdsWithin x {y}ᶜ] t → fderivWithin 𝕜 f s =ᶠ[nhds x] fderivWithin 𝕜 f t
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.unitForward.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A) (X : C)
  (p : CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) X),
  CategoryTheory.OverPresheafAux.unitForward η X p = CategoryTheory.OverPresheafAux.OverArrows.val p.snd
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.toPartialOrder : {α : Type u_6} → [self : OmegaCompletePartialOrder α] → PartialOrder α
-- Mathlib.Algebra.Group.Int.Units
Int.eq_one_or_neg_one_of_mul_eq_neg_one : ∀ {u v : ℤ}, u * v = -1 → u = 1 ∨ u = -1
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.ξ_mulVec_eq_0 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {α : Type u_2} {β : Type u_3}
  (a : Matrix α β (NumberField.RingOfIntegers K)) (x : β × (K →+* ℂ) → ℤ),
  x ≠ 0 →
    ∀ [inst_2 : Fintype β], (NumberField.house.asiegel✝ K a).mulVec x = 0 → a.mulVec (NumberField.house.ξ✝ K x) = 0
-- Std.Sync.StreamMap
/-- Wait for the first value inside of the stream map.
 -/
Std.StreamMap.tryRecv : {α β : Type} → Std.StreamMap α β → Std.Async.Async (Option (α × β))
-- Mathlib.Algebra.BigOperators.Finsupp.Fin
/-- The space of finitely supported functions `Fin 2 →₀ α` is equivalent to `α × α`.
See also `finTwoArrowEquiv`.  -/
finTwoArrowEquiv' : (M : Type u_1) → [inst : Zero M] → (Fin 2 →₀ M) ≃ M × M
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_add_le_iff_le_add' : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, -c + a ≤ b ↔ a ≤ b + c
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.mem_specialOrthogonalGroup_fin_two_iff : ∀ {R : Type v} [inst : CommRing R] {M : Matrix (Fin 2) (Fin 2) R},
  M ∈ Matrix.specialOrthogonalGroup (Fin 2) R ↔ M 0 0 = M 1 1 ∧ M 0 1 = -M 1 0 ∧ M 0 0 ^ 2 + M 0 1 ^ 2 = 1
-- Init.Data.List.ToArray
Array.toList_set : ∀ {α : Type u_1} (xs : Array α) (i : ℕ) (x : α) (h : i < xs.size), (xs.set i x h).toList = xs.toList.set i x
-- Mathlib.Algebra.Group.TypeTags.Finite
Fintype.card_multiplicative : ∀ (α : Type u_1) [inst : Fintype α], Fintype.card (Multiplicative α) = Fintype.card α
-- Mathlib.Data.List.Permutation
_private.Mathlib.Data.List.Permutation.0.List.permutationsAux2.match_3.eq_1 : ∀ {α : Type u_1} {β : Type u_3} (motive : List α → (List α → β) → Sort u_2) (x : List α → β)
  (h_1 : (x : List α → β) → motive [] x) (h_2 : (y : α) → (ys : List α) → (f : List α → β) → motive (y :: ys) f),
  (match [], x with
    | [], x => h_1 x
    | y :: ys, f => h_2 y ys f) =
    h_1 x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.ofIsIso_presentation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N)
  [inst_3 : CategoryTheory.IsIso f] (σ : M.QuasicoherentData) (i : σ.I),
  (SheafOfModules.QuasicoherentData.ofIsIso f σ).presentation i =
    SheafOfModules.Presentation.ofIsIso (SheafOfModules.Hom.over f (σ.X i)) (σ.presentation i)
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Grothendieck.ιNatTrans.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.Grothendieck.ιNatTrans f =
    {
      app := fun d =>
        { base := f,
          fiber :=
            CategoryTheory.CategoryStruct.id
              ((F.map f).toFunctor.obj ((CategoryTheory.Grothendieck.ι F X).obj d).fiber) },
      naturality := ⋯ }
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.HoCat.localizerMorphismResolution_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.FibrantObject.HoCat.localizerMorphismResolution C).functor =
    HomotopicalAlgebra.FibrantObject.HoCat.resolution
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- The Fourier transform of the derivative is given by multiplication of
`(2 * π * Complex.I) • innerSL ℝ` with the Fourier transform.  -/
SchwartzMap.fourier_fderivCLM_eq : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℂ E]
  [inst_3 : NormedSpace 𝕜 E] [inst_4 : SMulCommClass ℂ 𝕜 E] {V : Type u_3} [inst_5 : NormedAddCommGroup V]
  [inst_6 : InnerProductSpace ℝ V] [inst_7 : FiniteDimensional ℝ V] [inst_8 : MeasurableSpace V] [inst_9 : BorelSpace V]
  (f : SchwartzMap V E),
  FourierTransform.fourier ((SchwartzMap.fderivCLM 𝕜 V E) f) =
    (2 * ↑Real.pi * Complex.I) • (SchwartzMap.smulRightCLM ℂ E (innerSL ℝ)) (FourierTransform.fourier f)
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation.eq_3 : ∀ (x : ℕ), hyperoperation 2 x 0 = 0
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- Lift a quadratic map on `M` to `M ⧸ N`, where `N` is contained in the radical.  -/
QuadraticMap.lift : {R : Type u_1} →
  {M : Type u_2} →
    {P : Type u_4} →
      [inst : AddCommGroup M] →
        [inst_1 : AddCommGroup P] →
          [inst_2 : CommRing R] →
            [inst_3 : Module R M] →
              [inst_4 : Module R P] →
                (Q : QuadraticMap R M P) → (N : Submodule R M) → N ≤ Q.radical → QuadraticMap R (M ⧸ N) P
-- Mathlib.Analysis.InnerProductSpace.Symmetric
InnerProductSpace.isSymmetric_rankOne_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), (↑(((InnerProductSpace.rankOne 𝕜) x) x)).IsSymmetric
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
/-- The coordinates of a representative of `2 • P` for a projective point representative `P` on a
Weierstrass curve.  -/
WeierstrassCurve.Projective.dblXYZ : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → Fin 3 → R
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.functor_ext : ∀ {J : CategoryTheory.Limits.MulticospanShape} {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Limits.WalkingMulticospan J) C}
  (left :
    ∀ (i : J.L),
      F.obj (CategoryTheory.Limits.WalkingMulticospan.left i) = G.obj (CategoryTheory.Limits.WalkingMulticospan.left i))
  (right :
    ∀ (i : J.R),
      F.obj (CategoryTheory.Limits.WalkingMulticospan.right i) =
        G.obj (CategoryTheory.Limits.WalkingMulticospan.right i)),
  (∀ (i : J.R),
      CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i))
          (CategoryTheory.eqToHom ⋯) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (G.map (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i))) →
    (∀ (i : J.R),
        CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i))
            (CategoryTheory.eqToHom ⋯) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (G.map (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i))) →
      F = G
-- Mathlib.Algebra.Category.AlgCat.Limits
/-- The forgetful functor from R-algebras to types preserves all limits.
 -/
AlgCat.forget_preservesLimitsOfSize : ∀ {R : Type u} [inst : CommRing R] [UnivLE.{v, w}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{t, v, w, w, max u (w + 1), w + 1} (CategoryTheory.forget (AlgCat R))
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
SimpleGraph.chromaticNumber_cycleGraph_of_odd : ∀ (n : ℕ), 2 ≤ n → Odd n → (SimpleGraph.cycleGraph n).chromaticNumber = 3
-- Mathlib.Topology.WithTopology
WithTopology.ofTopology_injective : ∀ {X : Type u_1} (t : TopologicalSpace X), Function.Injective WithTopology.ofTopology
-- Lean.Meta.RecExt
/-- Marks the given declaration as recursive.
 -/
Lean.Meta.markAsRecursive : Lean.Name → Lean.CoreM Unit
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instMulActionForall.eq_1 : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α],
  DomMulAct.instMulActionForall = { toSMul := DomMulAct.instSMulForall, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Analysis.Convex.Jensen
/-- A form of the **equality case of Jensen's equality** for the case of strict concave and positive
weights.  -/
StrictConcaveOn.map_sum_eq_iff_of_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConcaveOn 𝕜 s f →
    (∀ i ∈ t, 0 < w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) →
          (f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.isZero_X_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i : ℤ),
  CategoryTheory.Limits.IsZero ((CochainComplex.mappingCone φ).X i) ↔
    CategoryTheory.Limits.IsZero (F.X (i + 1)) ∧ CategoryTheory.Limits.IsZero (G.X i)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get!_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ ∩ t₂).get! k = t₁.get! k
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.δ_naturalityₗ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {m n m' : M}
  (f : m ⟶ m') (X : C) [inst_3 : F.OplaxMonoidal] {Z : C} (h : (F.obj n).obj ((F.obj m').obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app X)
      (CategoryTheory.CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) h) =
    CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f n)).app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m' n).app X) h)
-- Mathlib.Topology.FiberBundle.Basic
OpenPartialHomeomorph.mk.congr_simp : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (toPartialHomeomorph toPartialHomeomorph_1 : PartialHomeomorph X Y)
  (e_toPartialHomeomorph : toPartialHomeomorph = toPartialHomeomorph_1)
  (open_source : IsOpen toPartialHomeomorph.source) (open_target : IsOpen toPartialHomeomorph.target),
  { toPartialHomeomorph := toPartialHomeomorph, open_source := open_source, open_target := open_target } =
    { toPartialHomeomorph := toPartialHomeomorph_1, open_source := ⋯, open_target := ⋯ }
-- Mathlib.Order.Defs.Unbundled
Maximal.le_of_ge : ∀ {α : Type u_1} [inst : LE α] {P : α → Prop} {x y : α}, Maximal P x → P y → x ≤ y → y ≤ x
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_surjective : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f], Function.Surjective (Function.uncurry (IsLocalizedModule.mk' f))
-- Mathlib.Analysis.Convex.Body
/-- A convex body has non-empty carrier set  -/
ConvexBody.nonempty' : ∀ {V : Type u_2} [inst : TopologicalSpace V] [inst_1 : AddCommMonoid V] [inst_2 : SMul ℝ V] (self : ConvexBody V),
  self.carrier.Nonempty
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.map_isZero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X : C},
  CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsZero (F.obj X)
-- Mathlib.Topology.UnitInterval
/-- A point between two points in a closed interval
can be expressed as a convex combination of them.
 -/
Set.Icc.eq_convexComb : ∀ {a b : ℝ} {x y z : ↑(Set.Icc a b)} (hxy : x ≤ y) (hyz : y ≤ z), y = Set.Icc.convexComb x z ⟨(↑y - ↑x) / (↑z - ↑x), ⋯⟩
-- Mathlib.RingTheory.Filtration
/-- The trivial stable `I`-filtration of `N`.  -/
Ideal.stableFiltration : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (I : Ideal R) → Submodule R M → I.Filtration M
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.comap_asIdeal : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f)
  (v : IsDedekindDomain.HeightOneSpectrum S),
  (IsDedekindDomain.HeightOneSpectrum.comap f hf v).asIdeal = Ideal.comap f v.asIdeal
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.presheafEquivOfIso_unitIso_inv_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y)
  (X_1 : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) (X_2 : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  ((TopCat.Presheaf.presheafEquivOfIso C H).unitIso.inv.app X_1).app X_2 = X_1.map (CategoryTheory.eqToHom ⋯)
-- Mathlib.Probability.Kernel.Disintegration.Basic
MeasureTheory.Measure.disintegrate : ∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω))
  (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond], ρ.fst.compProd ρCond = ρ
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
WeakBilin.instTopologicalSpace : {𝕜 : Type u_2} →
  {E : Type u_4} →
    {F : Type u_5} →
      [TopologicalSpace 𝕜] →
        [inst : CommSemiring 𝕜] →
          [inst_1 : AddCommMonoid E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : AddCommMonoid F] →
                [inst_4 : Module 𝕜 F] → (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → TopologicalSpace (WeakBilin B)
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.full : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful), F.Full
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.ofHoms_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {X Y : ι → C} (f : (i : ι) → X i ⟶ Y i)
  (P : CategoryTheory.MorphismProperty C), CategoryTheory.MorphismProperty.ofHoms f ≤ P ↔ ∀ (i : ι), P (f i)
-- Mathlib.Probability.Kernel.Basic
/-- Because of the measurability field in `Kernel.deterministic`, `rw [h]` will not rewrite
`deterministic f hf` to `deterministic g ⋯`. Instead one can do `rw [deterministic_congr h]`.  -/
ProbabilityTheory.Kernel.deterministic_congr : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f g : α → β} {hf : Measurable f}
  (h : f = g), ProbabilityTheory.Kernel.deterministic f hf = ProbabilityTheory.Kernel.deterministic g ⋯
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.eq_singularPart_measure : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η ξ : ProbabilityTheory.Kernel α γ}
  {f : α → γ → ENNReal} [inst : ProbabilityTheory.IsFiniteKernel η],
  κ = η.withDensity f + ξ →
    Measurable (Function.uncurry f) → ∀ (a : α), (ξ a).MutuallySingular (η a) → ξ a = (κ a).singularPart (η a)
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_add_ofNat : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ)
  [inst_4 : n.AtLeastTwo], ⌈a + OfNat.ofNat n⌉ = ⌈a⌉ + OfNat.ofNat n
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.ClosureState.localDecls : Lean.Elab.Term.MutualClosure.ClosureState → Array Lean.LocalDecl
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.natCast_apply : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : ContinuousAdd M₁] (n : ℕ) (m : M₁), ↑n m = n • m
-- Mathlib.Algebra.Algebra.Tower
AlgHom.extendScalarsHomOfSurjective_apply : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : A →ₐ[R] A),
  (AlgHom.extendScalarsHomOfSurjective h) f = { toRingHom := ↑f, commutes' := ⋯ }
-- Mathlib.Logic.Function.Basic
Function.surjInv_eq : ∀ {α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f) (b : β), f (Function.surjInv h b) = b
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.generateFrom_sUnion : ∀ {X : Type u_1} {G : Set (Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X)))},
  DiffeologicalSpace.generateFrom (⋃₀ G) = ⨆ s ∈ G, DiffeologicalSpace.generateFrom s
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.hom_nsmul : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} (n : ℕ) (f : M ⟶ N),
  SemimoduleCat.Hom.hom (n • f) = n • SemimoduleCat.Hom.hom f
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddRightCancelSemigroupOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : AddRightCancelSemigroup Mᵃᵒᵖ], DomAddAct.instAddRightCancelSemigroupOfAddOpposite = inst
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The determinant of the change-of-basis matrix between two orthonormal bases `a`, `b` is ±1.  -/
OrthonormalBasis.det_to_matrix_orthonormalBasis_real : ∀ {ι : Type u_1} {F : Type u_5} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (a b : OrthonormalBasis ι ℝ F), a.toBasis.det ⇑b = 1 ∨ a.toBasis.det ⇑b = -1
-- Lean.Elab.InfoTree.Types
Lean.Elab.FieldInfo.stx : Lean.Elab.FieldInfo → Lean.Syntax
-- Mathlib.Topology.Connected.Clopen
Sum.isConnected_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set (α ⊕ β)},
  IsConnected s ↔ (∃ t, IsConnected t ∧ s = Sum.inl '' t) ∨ ∃ t, IsConnected t ∧ s = Sum.inr '' t
-- Mathlib.Topology.Algebra.UniformMulAction
IsAddUnit.vadd_uniformity : ∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : AddMonoid M] [inst_2 : AddAction M X]
  [UniformContinuousConstVAdd M X] {c : M}, IsAddUnit c → c +ᵥ uniformity X = uniformity X
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquiv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (Q : Type u_4) [inst_4 : CommSemiring Q] [inst_5 : Algebra R Q]
  [inst_6 : IsLocalization M Q] (a : S), (IsLocalization.algEquiv M S Q) a = (IsLocalization.map Q (RingHom.id R) ⋯) a
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.inclusion_right : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] {S T : NonUnitalStarSubalgebra R A} (h : S ≤ T) (x : ↥T) (m : ↑x ∈ S),
  (NonUnitalStarSubalgebra.inclusion h) ⟨↑x, m⟩ = x
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  {d : {X : Dᵒᵖ} → ↑(R.obj X) →+ ↑(M.obj X)}
  {d_mul :
    autoParam (∀ {X : Dᵒᵖ} (a b : ↑(R.obj X)), d (a * b) = a • d b + b • d a)
      PresheafOfModules.Derivation.d_mul._autoParam}
  {d_map :
    autoParam
      (∀ {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : ↑(R.obj X)),
        d ((CategoryTheory.ConcreteCategory.hom (R.map f)) x) = (CategoryTheory.ConcreteCategory.hom (M.map f)) (d x))
      PresheafOfModules.Derivation.d_map._autoParam}
  {d_app :
    autoParam (∀ {X : Cᵒᵖ} (a : ↑(S.obj X)), d ((CategoryTheory.ConcreteCategory.hom (φ.app X)) a) = 0)
      PresheafOfModules.Derivation.d_app._autoParam}
  {d_1 : {X : Dᵒᵖ} → ↑(R.obj X) →+ ↑(M.obj X)}
  {d_mul_1 :
    autoParam (∀ {X : Dᵒᵖ} (a b : ↑(R.obj X)), d_1 (a * b) = a • d_1 b + b • d_1 a)
      PresheafOfModules.Derivation.d_mul._autoParam}
  {d_map_1 :
    autoParam
      (∀ {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : ↑(R.obj X)),
        d_1 ((CategoryTheory.ConcreteCategory.hom (R.map f)) x) =
          (CategoryTheory.ConcreteCategory.hom (M.map f)) (d_1 x))
      PresheafOfModules.Derivation.d_map._autoParam}
  {d_app_1 :
    autoParam (∀ {X : Cᵒᵖ} (a : ↑(S.obj X)), d_1 ((CategoryTheory.ConcreteCategory.hom (φ.app X)) a) = 0)
      PresheafOfModules.Derivation.d_app._autoParam},
  { d := d, d_mul := d_mul, d_map := d_map, d_app := d_app } =
      { d := d_1, d_mul := d_mul_1, d_map := d_map_1, d_app := d_app_1 } →
    d = d_1
-- Batteries.Data.List.Lemmas
List.disjoint_singleton : ∀ {α : Type u_1} {l : List α} {a : α}, l.Disjoint [a] ↔ a ∉ l
-- Mathlib.Data.Vector.Basic
/-- Define `motive v` by case-analysis on `v : Vector α n`.  -/
List.Vector.casesOn : {α : Type u_1} →
  {m : ℕ} →
    {motive : {n : ℕ} → List.Vector α n → Sort u_8} →
      (v : List.Vector α m) →
        motive List.Vector.nil → ({n : ℕ} → (hd : α) → (tl : List.Vector α n) → motive (hd ::ᵥ tl)) → motive v
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_int_lt_one_iff_dvd : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℤ), ‖↑k‖ < 1 ↔ ↑p ∣ k
-- Std.Http.Data.Request
Std.Http.Request.instInhabitedHead : Inhabited Std.Http.Request.Head