mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.RadonNikodym
/-- The singular part of `κ` with respect to `η` is mutually singular with `η`.  -/
ProbabilityTheory.Kernel.mutuallySingular_singularPart : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [inst : ProbabilityTheory.IsFiniteKernel κ] [inst_1 : ProbabilityTheory.IsFiniteKernel η] (a : α),
  ((κ.singularPart η) a).MutuallySingular (η a)
-- Mathlib.Data.Nat.Log
Nat.clog_mono_right : ∀ (b : ℕ) {n m : ℕ}, n ≤ m → Nat.clog b n ≤ Nat.clog b m
-- Init.Data.Array.Monadic
Array.forM_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [inst : Monad m] [LawfulMonad m] {xs : Array α} {g : α → β}
  {f : β → m PUnit.{u_1 + 1}}, forM (Array.map g xs) f = forM xs fun a => f (g a)
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.analyticOn : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_5} {Em : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (Em i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (Em i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em F)
  {s : Set ((i : ι) → Em i)}, AnalyticOn 𝕜 (⇑f) s
-- Mathlib.Topology.Homeomorph.Defs
/-- The unique homeomorphism between two empty types.  -/
Homeomorph.empty : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → [IsEmpty X] → [IsEmpty Y] → X ≃ₜ Y
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
det_fderivPiPolarCoordSymm : ∀ {ι : Type u_1} [inst : Fintype ι] (p : ι → ℝ × ℝ), (fderivPiPolarCoordSymm p).det = ∏ i, (p i).1
-- Mathlib.Algebra.Category.Semigrp.Basic
AddEquiv.toAddMagmaCatIso_hom : ∀ {X Y : Type u} [inst : Add X] [inst_1 : Add Y] (e : X ≃+ Y), e.toAddMagmaCatIso.hom = AddMagmaCat.ofHom e.toAddHom
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.RingTheory.Etale.StandardEtale
/-- The isomorphism to the standard etale algebra given a `StandardEtalePresentation`.  -/
StandardEtalePresentation.equivRing : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : StandardEtalePresentation R S) → S ≃ₐ[R] P.Ring
-- Mathlib.Analysis.Complex.AbelLimit
/-- The cone to the left of `1` with angle `2θ` such that `tan θ = s`.  -/
Complex.stolzCone : ℝ → Set ℂ
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
_private.Mathlib.CategoryTheory.Sites.Hypercover.Zero.0.CategoryTheory.PreZeroHypercover.sumLift.match_1.eq_1 : ∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} (motive : (E.sum F).I₀ → Sort u_5) (i : E.I₀)
  (h_1 : (i : E.I₀) → motive (Sum.inl i)) (h_2 : (i : F.I₀) → motive (Sum.inr i)),
  (match Sum.inl i with
    | Sum.inl i => h_1 i
    | Sum.inr i => h_2 i) =
    h_1 i
-- Lean.Meta.Instances
Lean.Meta.DefaultInstanceEntry.mk : Lean.Name → Lean.Name → ℕ → Lean.Meta.DefaultInstanceEntry
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
MeasureTheory.Measure.toBoxAdditive_apply : ∀ {ι : Type u_1} [inst : Finite ι] (μ : MeasureTheory.Measure (ι → ℝ)) [inst_1 : MeasureTheory.IsLocallyFiniteMeasure μ]
  (J : BoxIntegral.Box ι), μ.toBoxAdditive J = μ.real ↑J
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.EvenHom.compr₂_bilin : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} {B : Type u_4} [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (g : CliffordAlgebra.EvenHom Q A) (f : A →ₐ[R] B),
  (g.compr₂ f).bilin = g.bilin.compr₂ f.toLinearMap
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.nat_mul : ∀ {p x : ℝ} {n : ℕ}, LiouvilleWith p x → n ≠ 0 → LiouvilleWith p (↑n * x)
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.instMaxOfLinearOrder.eq_1 : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : LinearOrder α],
  AddUnits.instMaxOfLinearOrder = { max := fun a b => if a ≤ b then b else a }
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.coe_iSup_of_directed : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {ι : Sort u_2} [hι : Nonempty ι] {S : ι → NonUnitalSubsemiring R},
  Directed (fun x1 x2 => x1 ≤ x2) S → ↑(⨆ i, S i) = ⋃ i, ↑(S i)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.zero_domain : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F], LinearPMap.domain 0 = ⊤
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.transitive : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X}
  (J : CategoryTheory.GrothendieckTopology C),
  S ∈ J X →
    ∀ (R : CategoryTheory.Sieve X),
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ J Y) → R ∈ J X
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.coe_bot : ∀ {α : Type u_1} [inst : TopologicalSpace α], ↑⊥ = ∅
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_toArray_roo : ∀ {m n : ℕ}, (m<...n).toArray.toList = (m<...n).toList
-- Mathlib.Analysis.Complex.Periodic
/-- Key technical lemma: the function `cuspFunction h f` is differentiable at the images of
differentiability points of `f` (even if `invQParam` is not differentiable there).
 -/
Function.Periodic.differentiableAt_cuspFunction : ∀ {h : ℝ} {f : ℂ → ℂ},
  h ≠ 0 →
    Function.Periodic f ↑h →
      ∀ {z : ℂ},
        DifferentiableAt ℂ f z → DifferentiableAt ℂ (Function.Periodic.cuspFunction h f) (Function.Periodic.qParam h z)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Construct a morphism `A ⟶ B` of `Grp C` from a map `f : A.X ⟶ A.X` and a `IsMonHom f`
instance.  -/
CategoryTheory.Grp.homMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {A B : CategoryTheory.Grp C} → (f : A.X ⟶ B.X) → [CategoryTheory.IsMonHom f] → A ⟶ B
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.coe_inf : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (p p' : NonUnitalSubsemiring R), ↑(p ⊓ p') = ↑p ∩ ↑p'
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instSMul : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] → [inst_7 : ContMDiffMul I (↑⊤) G] → SMul 𝕜 (LeftInvariantDerivation I G)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
ExteriorAlgebra.ιMulti_family.eq_1 : ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ) {I : Type u_1}
  [inst_3 : LinearOrder I] (v : I → M) (s : ↑(Set.powersetCard I n)),
  ExteriorAlgebra.ιMulti_family R n v s = (ExteriorAlgebra.ιMulti R n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s))
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
tsum_eq_zero_of_not_summable : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  {f : β → α}, ¬Summable f L → ∑'[L] (b : β), f b = 0
-- Mathlib.Topology.Separation.Basic
instT1SpaceOfDiscreteTopology : ∀ {X : Type u_1} [inst : TopologicalSpace X] [DiscreteTopology X], T1Space X
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.refl : ∀ {α : Type u_1} {M : Matroid α}, M.IsRestriction M
-- Mathlib.Data.Num.ZNum
Num.decidableDvd : DecidableRel fun x1 x2 => x1 ∣ x2
-- Init.Data.Range.Polymorphic.UInt
UInt64.upwardEnumerableLT_ofBitVec : ∀ {x y : BitVec 64},
  Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y
-- Mathlib.RingTheory.Artinian.Module
instIsArtinianRingQuotientIdeal : ∀ (R : Type u_1) [inst : Ring R] [IsArtinianRing R] (I : Ideal R) [inst_2 : I.IsTwoSided], IsArtinianRing (R ⧸ I)
-- Lean.Parser.Do
Lean.Parser.Term.doSeqIndent : Lean.Parser.Parser
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indep_iSup_of_monotone : ∀ {α : Type u_1} {ι : Type u_3} {_mα : MeasurableSpace α} [inst : SemilatticeSup ι] {Ω : Type u_4}
  {m : ι → MeasurableSpace Ω} {m' m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  (∀ (i : ι), ProbabilityTheory.Kernel.Indep (m i) m' κ μ) →
    (∀ (i : ι), m i ≤ m0) → m' ≤ m0 → Monotone m → ProbabilityTheory.Kernel.Indep (⨆ i, m i) m' κ μ
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.continuous_toLp : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [inst_5 : OpensMeasurableSpace E]
  [inst_6 : SecondCountableTopologyEither E F] {p : ENNReal} [inst_7 : Fact (1 ≤ p)] {μ : MeasureTheory.Measure E}
  [hμ : μ.HasTemperateGrowth], Continuous fun f => f.toLp p μ
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
Matrix.val_planeConformalMatrix : ∀ {R : Type u_1} [inst : Field R] (a b : R) (hab : a ^ 2 + b ^ 2 ≠ 0),
  ↑(Matrix.planeConformalMatrix a b hab) = !![a, -b; b, a]
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instSub : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Sub (ModularForm Γ k)
-- Mathlib.Analysis.ODE.PicardLindelof
/-- Converse of `hasDerivWithinAt_picard_Icc`: if `f` is the derivative along `α`, then `α`
satisfies the integral equation.  -/
ODE.picard_eq_of_hasDerivAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {α : ℝ → E}
  {u : Set E} {t₀ t : ℝ},
  ContinuousOn (Function.uncurry f) (Set.uIcc t₀ t ×ˢ u) →
    (∀ t' ∈ Set.uIcc t₀ t, HasDerivWithinAt α (f t' (α t')) (Set.uIcc t₀ t) t') →
      Set.MapsTo α (Set.uIcc t₀ t) u → ODE.picard f t₀ (α t₀) α t = α t
-- Mathlib.Geometry.Manifold.WhitneyEmbedding
_private.Mathlib.Geometry.Manifold.WhitneyEmbedding.0.SmoothBumpCovering.embeddingPiTangent_injective_mfderiv : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_4 : TopologicalSpace M]
  [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (↑⊤) M] [inst_7 : T2Space M] [inst_8 : Fintype ι] {s : Set M}
  (f : SmoothBumpCovering ι I M s),
  ∀ x ∈ s, Function.Injective ⇑(mfderiv% ⇑(SmoothBumpCovering.embeddingPiTangent✝ f) x)
-- Mathlib.CategoryTheory.Generator.Presheaf
/-- Given `X : C` and `M : A`, this is the presheaf `Cᵒᵖ ⥤ A` which sends
`Y : Cᵒᵖ` to the coproduct of copies of `M` indexed by `Y.unop ⟶ X`.  -/
CategoryTheory.Presheaf.freeYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        [CategoryTheory.Limits.HasCoproducts A] → C → A → CategoryTheory.Functor Cᵒᵖ A
-- Init.Data.Stream
Std.instToStreamSubarray : {α : Type u_1} → Std.ToStream (Subarray α) (Subarray α)
-- Init.Data.Vector.Lemmas
Vector.any_reverse : ∀ {α : Type u_1} {n : ℕ} {f : α → Bool} {xs : Vector α n}, xs.reverse.any f = xs.any f
-- Mathlib.Algebra.Order.Quantale
Quantale.mul_sup_distrib : ∀ {α : Type u_1} {x y z : α} [inst : Semigroup α] [inst_1 : CompleteLattice α] [IsQuantale α],
  x * (y ⊔ z) = x * y ⊔ x * z
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.logDeriv_one_sub_cexp : ∀ (r : ℂ), (logDeriv fun z => 1 - r * Complex.exp z) = fun z => -r * Complex.exp z / (1 - r * Complex.exp z)
-- Mathlib.Algebra.Opposites
MulOpposite.instOne : {α : Type u_1} → [One α] → One αᵐᵒᵖ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α},
  (t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- Given an equivalence, there is an induced equivalence between colorings.  -/
SimpleGraph.recolorOfEquiv : {V : Type u} → (G : SimpleGraph V) → {α : Type u_4} → {β : Type u_5} → α ≃ β → G.Coloring α ≃ G.Coloring β
-- Mathlib.Analysis.CStarAlgebra.Basic
starₗᵢ_toContinuousLinearEquiv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : StarRing 𝕜] [inst_2 : SeminormedAddCommGroup E]
  [inst_3 : StarAddMonoid E] [inst_4 : NormedStarGroup E] [inst_5 : Module 𝕜 E] [inst_6 : StarModule 𝕜 E],
  ↑(starₗᵢ 𝕜) = starL 𝕜
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map_comp : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k K} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k G} (f : H →* K) (g : G →* H)
  (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) (n : ℕ),
  groupCohomology.map (f.comp g) (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor g).map φ) ψ) n =
    CategoryTheory.CategoryStruct.comp (groupCohomology.map f φ n) (groupCohomology.map g ψ n)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.drop.eq_def : ∀ {α : Type u} (s : Stream'.Seq α) (x : ℕ),
  s.drop x =
    match x with
    | 0 => s
    | n.succ => (s.drop n).tail
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- If `u` has a Fredholm package, it is Fredholm.  -/
ContinuousLinearMap.FredholmPackage.isFredholm : ∀ {𝕜 : 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] [CompleteSpace 𝕜] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space E] [T2Space F] {u : E →L[𝕜] F} (pkg : u.FredholmPackage),
  u.IsFredholm
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.typesWith_top : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w}, T.typesWith ⊤ = Set.univ
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.isPrimitive_one : ∀ {R : Type u_1} [inst : CommSemiring R], Polynomial.IsPrimitive 1
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.partSize_eq_one_of_range_emb_eq_singleton : ∀ {n : ℕ} (c : OrderedFinpartition n) {i : Fin c.length} {j : Fin n}, Set.range (c.emb i) = {j} → c.partSize i = 1
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop}
  (h : Manifold.LiftSourceTargetPropertyAt I J n f x P), h.codChart ∈ IsManifold.maximalAtlas J n N
-- Mathlib.RingTheory.Flat.Basic
/-- Tensor product of linearly independent families is linearly
independent under some flatness conditions.

The flatness condition could be removed over domains.
See `LinearIndepOn.tmul_of_isDomain`.  -/
TensorProduct.LinearIndepOn.tmul_of_flat_right : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {ι : Type u_6} {κ : Type u_7} {v : ι → M}
  {w : κ → N} {s : Set ι} {t : Set κ} [Module.Flat R N],
  LinearIndepOn R v s → LinearIndepOn R w t → LinearIndepOn R (fun i => v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t)
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.count_maximal : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v w : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Decidable (w = v)], FractionalIdeal.count K v ↑w.asIdeal = if w = v then 1 else 0
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The minimum of a measurable function is smaller than its integral.  -/
MeasureTheory.exists_le_lintegral : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal}
  [MeasureTheory.IsProbabilityMeasure μ], AEMeasurable f μ → ∃ x, f x ≤ ∫⁻ (a : α), f a ∂μ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.unitOfList_eq_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α},
  Std.ExtHashMap.unitOfList l = List.foldl (fun acc a => acc.insertIfNew a ()) ∅ l
-- Mathlib.Combinatorics.SetFamily.FourFunctions
/-- A slight generalisation of the **Marica-Schönheim Inequality**.  -/
Finset.le_card_diffs_mul_card_diffs : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] (s t : Finset α),
  s.card * t.card ≤ (s.diffs t).card * (t.diffs s).card
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Product of normed groups, using the sup norm.  -/
Prod.normedGroup : {E : Type u_2} → {F : Type u_3} → [NormedGroup E] → [NormedGroup F] → NormedGroup (E × F)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Relations.isUniversal_antisymmetric : ∀ {L : FirstOrder.Language} (r : L.Relations 2), FirstOrder.Language.BoundedFormula.IsUniversal r.antisymmetric
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.unfoldRule : Aesop.UnfoldRule → Aesop.BaseRuleSetMember
-- Init.Data.SInt.Lemmas
ISize.toInt_bmod_two_pow_numBits : ∀ (x : ISize), x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt
-- Mathlib.Data.List.Find
_private.Mathlib.Data.List.Find.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
OnePoint.map_smul : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] {L : Type u_2} [inst_2 : Field L] [inst_3 : DecidableEq L]
  (f : K →+* L) (g : GL (Fin 2) K) (c : OnePoint K),
  OnePoint.map (⇑f) (g • c) = (Matrix.GeneralLinearGroup.map f) g • OnePoint.map (⇑f) c
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.of_dvd : ∀ {R : Type u} [inst : CommSemiring R] {f g : Polynomial R}, f.Separable → g ∣ f → g.Separable
-- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
ConvexOn.comp_rnDeriv_trim_le : ∀ {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ} (hm : m ≤ m𝓧),
  μ.AbsolutelyContinuous ν →
    MeasureTheory.StronglyMeasurable f →
      ConvexOn ℝ (Set.Ici 0) f →
        ContinuousWithinAt f (Set.Ici 0) 0 →
          MeasureTheory.Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν →
            (fun x => f ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal) ≤ᵐ[ν.trim hm]
              ν[fun x => f (μ.rnDeriv ν x).toReal | m]
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.MorphismProperty.regularMono_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.MorphismProperty.regularMono C f ↔ CategoryTheory.IsRegularMono f
-- Init.System.ST
EST.pure : {α ε σ : Type} → α → EST ε σ α
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isRat_inv_neg : ∀ {α : Type u_1} [inst : DivisionRing α] [CharZero α] {a : α} {n d : ℕ},
  Mathlib.Meta.NormNum.IsRat a (Int.negOfNat n.succ) d → Mathlib.Meta.NormNum.IsRat a⁻¹ (Int.negOfNat d) n.succ
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.setLIntegral_const : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : β → ENNReal}
  {μ : MeasureTheory.Measure β} {a : α} {s : Set β},
  ∫⁻ (x : β) in s, f x ∂(ProbabilityTheory.Kernel.const α μ) a = ∫⁻ (x : β) in s, f x ∂μ
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.get?ₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [LawfulBEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → Option (β a)
-- Mathlib.GroupTheory.Perm.Option
Equiv.optionCongr_one : ∀ {α : Type u_1}, Equiv.optionCongr 1 = 1
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.equiv_of_both_ways : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C] {X Y : C} (f : X ⟶ Y) (g : Y ⟶ X), X ≈ Y
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.updateBinderName : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.FunDecl pu → Lean.Name → Lean.Compiler.LCNF.FunDecl pu
-- Init.Data.Nat.Div.Basic
Nat.one_mod_eq_zero_iff : ∀ {n : ℕ}, 1 % n = 0 ↔ n = 1
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_of_isEmpty : ∀ {α : Type u_4} [inst : MeasurableSpace α] [IsEmpty α] (μ : MeasureTheory.Measure α) (f : α → ENNReal),
  ∫⁻ (x : α), f x ∂μ = 0
-- Mathlib.RingTheory.Ideal.Maps
/-- `map` and `comap` are adjoint, and the composition `map f ∘ comap f` is the
identity  -/
Ideal.giMapComap : {R : Type u} →
  {S : Type v} →
    {F : Type u_1} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : FunLike F R S] →
            (f : F) →
              [inst_3 : RingHomClass F R S] → Function.Surjective ⇑f → GaloisInsertion (Ideal.map f) (Ideal.comap f)
-- Mathlib.Order.Sublattice
Sublattice.infClosed' : ∀ {α : Type u_2} [inst : Lattice α] (self : Sublattice α), InfClosed self.carrier
-- Init.Data.Array.Erase
Array.eraseP_eq_self_iff : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, xs.eraseP p = xs ↔ ∀ a ∈ xs, ¬p a = true
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mvPolynomialEquivMvPolynomial_symm_apply : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [inst : CommSemiring R] [inst_1 : CommSemiring S₃]
  (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃) (g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R)
  (hfgC : (f.comp g).comp MvPolynomial.C = MvPolynomial.C)
  (hfgX : ∀ (n : S₂), f (g (MvPolynomial.X n)) = MvPolynomial.X n)
  (hgfC : (g.comp f).comp MvPolynomial.C = MvPolynomial.C)
  (hgfX : ∀ (n : S₁), g (f (MvPolynomial.X n)) = MvPolynomial.X n) (a : MvPolynomial S₂ S₃),
  (MvPolynomial.mvPolynomialEquivMvPolynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX).symm a = g a
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
/-- The key that is used for sorting and deduplicating `apply at` lemmas.  -/
Mathlib.Tactic.ClickSuggestions.ApplyAtKey : Type