mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.constVAdd_coe : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : ContinuousConstVAdd V₁ P₁] (v : V₁),
  ↑(ContinuousAffineEquiv.constVAdd k P₁ v) = AffineEquiv.constVAdd k P₁ v
-- Lean.Declaration
/-- Value for an opaque constant declaration `opaque x : t := e`  -/
Lean.OpaqueVal : Type
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.nonDegenerateEquivOfIso_symm_apply_coe : ∀ {X Y : SSet} (e : X ≅ Y) {n : ℕ} (x : ↑(Y.nonDegenerate n)),
  ↑((SSet.nonDegenerateEquivOfIso e).symm x) =
    (CategoryTheory.ConcreteCategory.hom (e.inv.app (Opposite.op { len := n }))) ↑x
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.asFiberHom_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X) (y : ↥(AlgebraicGeometry.Spec (X.residueField x))),
  (AlgebraicGeometry.Scheme.Hom.asFiberHom f x) y = AlgebraicGeometry.Scheme.Hom.asFiber f x
-- Mathlib.Order.CompleteLattice.Basic
sSup_inter_le : ∀ {α : Type u_1} [inst : CompleteLattice α] {s t : Set α}, sSup (s ∩ t) ≤ sSup s ⊓ sSup t
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- **Alias** of `Measurable.subtype_coe`. -/
Measurable.subtype_val : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : β → Prop} {f : α → Subtype p},
  Measurable f → Measurable fun a => ↑(f a)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.any_singleton : ∀ {α : Type u_1} {P : α → Prop} {x : α}, Ordnode.Any P {x} ↔ P x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → Bool} {k : α}, (Std.ExtDTreeMap.filter (fun k x => f k) t).getKey? k = Option.filter f (t.getKey? k)
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_sshiftRight : ∀ {w : ℕ} (x : BitVec w) (s i : ℕ),
  (x.sshiftRight s).getLsbD i = (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else x.msb)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGetEntryLE!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.getEntryLE! t₁ k = Std.DTreeMap.Raw.Const.getEntryLE! t₂ k
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Dᵒᵖ A)
  (x : Φ.fiber.Elementsᵒᵖ),
  (Φ.presheafFiberMapCocone F K P).ι.app x = Φ.toPresheafFiberMap F K P (Opposite.unop x).fst (Opposite.unop x).snd
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.smul_const : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : SMul M X] {m : MeasurableSpace α}
  {f : α → M} [inst_2 : MeasurableSpace M] [MeasurableSMul M X], Measurable f → ∀ (y : X), Measurable fun x => f x • y
-- Mathlib.NumberTheory.SmoothNumbers
/-- The product of the prime factors of `n` that are in `s` is an `s`-factored number.  -/
Nat.prod_mem_factoredNumbers : ∀ (s : Finset ℕ) (n : ℕ), (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod ∈ Nat.factoredNumbers s
-- Mathlib.MeasureTheory.Integral.Pi
/-- On a finite product space, a product of integrable functions depending on each coordinate is
integrable. Version with dependent target.  -/
MeasureTheory.Integrable.fintype_prod_dep : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : Fintype ι] [inst_1 : NormedCommRing 𝕜] {E : ι → Type u_3}
  {f : (i : ι) → E i → 𝕜} {mE : (i : ι) → MeasurableSpace (E i)} {μ : (i : ι) → MeasureTheory.Measure (E i)}
  [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)],
  (∀ (i : ι), MeasureTheory.Integrable (f i) (μ i)) →
    MeasureTheory.Integrable (fun x => ∏ i, f i (x i)) (MeasureTheory.Measure.pi μ)
-- Mathlib.Order.Basic
GE.ge.le : ∀ {α : Type u_2} [inst : LE α] {a b : α}, a ≥ b → b ≤ a
-- Mathlib.Algebra.Group.Center
Set.subset_centralizer_centralizer : ∀ {M : Type u_1} {S : Set M} [inst : Mul M], S ⊆ S.centralizer.centralizer
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Sheaf.isTerminalTerminal_from_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {X : A} (hX : CategoryTheory.Limits.IsTerminal X)
  (G : CategoryTheory.Sheaf J A),
  ((CategoryTheory.Sheaf.isTerminalTerminal J hX).from G).hom =
    (CategoryTheory.Functor.isTerminalConst Cᵒᵖ hX).from G.obj
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.mk.inj : ∀ {M : Type u_1} {inst : MulOneClass M} {toSubmonoid : Submonoid M} {mulSaturated : toSubmonoid.MulSaturated}
  {toSubmonoid_1 : Submonoid M} {mulSaturated_1 : toSubmonoid_1.MulSaturated},
  { toSubmonoid := toSubmonoid, mulSaturated := mulSaturated } =
      { toSubmonoid := toSubmonoid_1, mulSaturated := mulSaturated_1 } →
    toSubmonoid = toSubmonoid_1
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- Change of coefficients in mv power series, as an `AlgHom`  -/
MvPowerSeries.mapAlgHom : {σ : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            {B : Type u_4} →
              [inst_3 : Semiring B] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → MvPowerSeries σ A →ₐ[R] MvPowerSeries σ B
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ΨSq_even : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (m : ℤ),
  W.ΨSq (2 * m) =
    (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 * W.Ψ₂Sq
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.instFiniteIntAdditiveUnitsRingOfIntegers : ∀ (K : Type u_1) [inst : Field K] [NumberField K], Module.Finite ℤ (Additive (NumberField.RingOfIntegers K)ˣ)
-- Mathlib.RingTheory.Flat.IsBaseChange
IsBaseChange.of_left_exact : ∀ {R : Type u_1} [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S] {M₁ : Type u_3}
  {M₂ : Type u_4} {M₃ : Type u_5} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} [inst_3 : AddCommGroup M₁]
  [inst_4 : AddCommGroup M₂] [inst_5 : AddCommGroup M₃] [inst_6 : AddCommGroup N₁] [inst_7 : AddCommGroup N₂]
  [inst_8 : AddCommGroup N₃] [inst_9 : Module R M₁] [inst_10 : Module R M₂] [inst_11 : Module R M₃]
  [inst_12 : Module R N₁] [inst_13 : Module R N₂] [inst_14 : Module R N₃] [inst_15 : Module S N₁]
  [inst_16 : Module S N₂] [inst_17 : Module S N₃] [inst_18 : IsScalarTower R S N₁] [inst_19 : IsScalarTower R S N₂]
  [inst_20 : IsScalarTower R S N₃] (h₁ : M₁ →ₗ[R] N₁) (h₂ : M₂ →ₗ[R] N₂) (h₃ : M₃ →ₗ[R] N₃) {f : M₁ →ₗ[R] M₂}
  {g : M₂ →ₗ[R] M₃} {f' : N₁ →ₗ[S] N₂} {g' : N₂ →ₗ[S] N₃},
  h₂ ∘ₗ f = ↑R f' ∘ₗ h₁ →
    h₃ ∘ₗ g = ↑R g' ∘ₗ h₂ →
      ∀ [Module.Flat R S],
        IsBaseChange S h₂ →
          IsBaseChange S h₃ →
            Function.Exact ⇑f ⇑g →
              Function.Injective ⇑f → Function.Exact ⇑f' ⇑g' → Function.Injective ⇑f' → IsBaseChange S h₁
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- a `CatCommSq` bundling the natural isomorphism `F ⋙ base ≅ left ⋙ F'`.  -/
CategoryTheory.Limits.CatCospanTransform.squareLeft : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {A' : Type u₄} →
                  {B' : Type u₅} →
                    {C' : Type u₆} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                (self : CategoryTheory.Limits.CatCospanTransform F G F' G') →
                                  CategoryTheory.CatCommSq F self.left self.base F'
-- Init.Data.Option.Basic
Option.join_some : ∀ {α : Type u_1} {o : Option α}, (some o).join = o
-- Mathlib.Topology.UnitInterval
Set.Icc.abs_sub_addNSMul_le : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a ≤ b) {δ : α},
  0 ≤ δ →
    ∀ {t : ↑(Set.Icc a b)} (n : ℕ),
      t ∈ Set.Icc (Set.Icc.addNSMul h δ n) (Set.Icc.addNSMul h δ (n + 1)) → |↑t - ↑(Set.Icc.addNSMul h δ n)| ≤ δ
-- Mathlib.Analysis.SpecialFunctions.Arsinh
/-- The function `Real.arsinh` is real analytic.  -/
Real.analyticWithinAt_arsinh : ∀ {x : ℝ} {s : Set ℝ}, AnalyticWithinAt ℝ Real.arsinh s x
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ k ∉ m then some k else m.getKey? a
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- Right whiskering for morphisms of bimodule objects.  -/
Bimod.whiskerRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        [inst_3 :
            ∀ (X : C),
              CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                (CategoryTheory.MonoidalCategory.tensorLeft X)] →
          [inst_4 :
              ∀ (X : C),
                CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                  (CategoryTheory.MonoidalCategory.tensorRight X)] →
            {X Y Z : CategoryTheory.Mon C} →
              {M₁ M₂ : Bimod X Y} → (M₁ ⟶ M₂) → (N : Bimod Y Z) → M₁.tensorBimod N ⟶ M₂.tensorBimod N
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.emphLike : Lean.SyntaxNodeKind →
  Char →
    String →
      String →
        (Lean.Doc.Parser.InlineCtxt → Option ℕ) →
          (Lean.Doc.Parser.InlineCtxt → Option ℕ → Lean.Doc.Parser.InlineCtxt) →
            Lean.Doc.Parser.InlineCtxt → Lean.Parser.ParserFn
-- Mathlib.Data.Seq.Defs
Stream'.Seq.get?_mk : ∀ {α : Type u} (f : Stream' (Option α)) (hf : f.IsSeq), Stream'.Seq.get? ⟨f, hf⟩ = f
-- Init.Core
/-- `Refl r` means the binary relation `r` is reflexive, that is, `r x x` always holds.  -/
Std.Refl : {α : Sort u} → (α → α → Prop) → Prop
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.ae_mono : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ ≤ ν → MeasureTheory.ae μ ≤ MeasureTheory.ae ν
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_3.eq_2 : ∀ {n : ℕ} (motive : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) → Sort u_1)
  (h_1 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some (some c)))
  (h_2 : Unit → motive (some none)) (h_3 : Unit → motive none),
  (match some none with
    | some (some c) => h_1 c
    | some none => h_2 ()
    | none => h_3 ()) =
    h_2 ()
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MonotoneOn.memLp_top : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {f : X → E},
  MonotoneOn f s → ∀ {a b : X}, IsLeast s a → IsGreatest s b → MeasurableSet s → MeasureTheory.MemLp f ⊤ (μ.restrict s)
-- Mathlib.CategoryTheory.Shift.CommShift
/-- If a functor `F : C ⥤ D` is equipped with "commutation isomorphisms" with the
shifts by `a` and `b`, then there is a commutation isomorphism with the shift by `c` when
`a + b = c`.  -/
CategoryTheory.Functor.CommShift.isoAdd' : {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] →
        {F : CategoryTheory.Functor C D} →
          {A : Type u_4} →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                [inst_4 : CategoryTheory.HasShift D A] →
                  {a b c : A} →
                    a + b = c →
                      ((CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)) →
                        ((CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b)) →
                          ((CategoryTheory.shiftFunctor C c).comp F ≅ F.comp (CategoryTheory.shiftFunctor D c))
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.gcd_dvd_right : ∀ (a b : ℤ), Int.Internal.Linear.gcd✝ a b ∣ b
-- Mathlib.RingTheory.Spectrum.Prime.Topology
IsLocalRing.comap_closedPoint : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : IsLocalRing R] {S : Type v} [inst_2 : CommSemiring S]
  [inst_3 : IsLocalRing S] (f : R →+* S) [IsLocalHom f],
  PrimeSpectrum.comap f (IsLocalRing.closedPoint S) = IsLocalRing.closedPoint R
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.mulEquivProd_symm_apply_left : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] (x : N × G),
  (SemidirectProduct.mulEquivProd.symm x).left = x.1
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
/-- If `f` is a nontrivial countably generated filter, then there exists a sequence that converges
to `f`.  -/
Filter.exists_seq_tendsto : ∀ {α : Type u_1} (f : Filter α) [f.IsCountablyGenerated] [f.NeBot], ∃ x, Filter.Tendsto x Filter.atTop f
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- The jacobian of a presentation in the smaller coefficient ring, provided `P.HasCoeffs R₀`.  -/
Algebra.SubmersivePresentation.jacobianOfHasCoeffs : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] →
                (P : Algebra.SubmersivePresentation R S ι σ) →
                  (R₀ : Type u_5) →
                    [inst_4 : CommRing R₀] →
                      [inst_5 : Algebra R₀ R] →
                        [inst_6 : Algebra R₀ S] → [inst_7 : IsScalarTower R₀ R S] → [P.HasCoeffs R₀] → MvPolynomial ι R₀
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.d_comp_XIsoOfEq_inv : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₂ p₃ : ι}
  (h : p₃ = p₂) (p₁ : ι), CategoryTheory.CategoryStruct.comp (K.d p₁ p₂) (K.XIsoOfEq h).inv = K.d p₁ p₃
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLT_iff_pairwise`. -/
List.Pairwise.sortedLT : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], List.Pairwise (fun x1 x2 => x1 < x2) l → l.SortedLT
-- Mathlib.Order.Partition.Equipartition
/-- An equipartition of a finset with `n` elements into `k` parts has
`n - n % k` parts of size `n / k`.  -/
Finpartition.IsEquipartition.card_small_parts_eq_mod : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {P : Finpartition s},
  P.IsEquipartition → {p ∈ P.parts | p.card = s.card / P.parts.card}.card = P.parts.card - s.card % P.parts.card
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- The `AddSubgroup` defined by the class of `0` for an additive congruence relation
on an `AddGroup`.  -/
AddCon.addSubgroup : {G : Type u_1} → [inst : AddGroup G] → AddCon G → AddSubgroup G
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.preservesFiniteColimits_of_createsFiniteColimits_and_hasFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.CreatesFiniteColimits F]
  [CategoryTheory.Limits.HasFiniteColimits D], CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.mem_factors_of_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a p : α},
  a ≠ 0 → Irreducible p → p ∣ a → Associates.mk p ∈ (Associates.mk a).factors
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.mem_toAddSubmonoid : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : NonUnitalSubsemiring R} {x : R}, x ∈ s.toAddSubmonoid ↔ x ∈ s
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- Control of the variation of the vector measure which appears in the integral of scalar functions
with respect to a vector measure.  -/
MeasureTheory.VectorMeasure.variation_transpose_lsmul : ∀ {X : Type u_2} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  (μ : MeasureTheory.VectorMeasure X F), (μ.transpose (ContinuousLinearMap.lsmul ℝ ℝ)).variation = μ.variation
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- The carrier of `N ⊔ H` is just `↑N + ↑H` (pointwise set addition)
when `H` is a subgroup of the normalizer of `N` in `G`.  -/
AddSubgroup.coe_add_of_right_le_normalizer_left : ∀ {G : Type u_2} [inst : AddGroup G] (N H : AddSubgroup G), H ≤ AddSubgroup.normalizer ↑N → ↑(N ⊔ H) = ↑N + ↑H
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimInfo.mk.injEq : ∀ (elimExpr elimType : Lean.Expr) (motivePos : ℕ) (targetsPos : Array ℕ) (altsInfo : Array Lean.Meta.ElimAltInfo)
  (numComplexMotiveArgs : ℕ) (elimExpr_1 elimType_1 : Lean.Expr) (motivePos_1 : ℕ) (targetsPos_1 : Array ℕ)
  (altsInfo_1 : Array Lean.Meta.ElimAltInfo) (numComplexMotiveArgs_1 : ℕ),
  ({ elimExpr := elimExpr, elimType := elimType, motivePos := motivePos, targetsPos := targetsPos, altsInfo := altsInfo,
        numComplexMotiveArgs := numComplexMotiveArgs } =
      { elimExpr := elimExpr_1, elimType := elimType_1, motivePos := motivePos_1, targetsPos := targetsPos_1,
        altsInfo := altsInfo_1, numComplexMotiveArgs := numComplexMotiveArgs_1 }) =
    (elimExpr = elimExpr_1 ∧
      elimType = elimType_1 ∧
        motivePos = motivePos_1 ∧
          targetsPos = targetsPos_1 ∧ altsInfo = altsInfo_1 ∧ numComplexMotiveArgs = numComplexMotiveArgs_1)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosReflectLT.mk : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α]
  [toContravariantClass : ContravariantClass { x // 0 ≤ x } α (fun x y => y * ↑x) fun x1 x2 => x1 < x2],
  MulPosReflectLT α
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.ProbabilityMeasure.map_prod_map : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.ProbabilityMeasure β) {α' : Type u_3}
  [inst_2 : MeasurableSpace α'] {β' : Type u_4} [inst_3 : MeasurableSpace β'] {f : α → α'} {g : β → β'}
  (f_mble : Measurable f) (g_mble : Measurable g), (μ.map ⋯).prod (ν.map ⋯) = (μ.prod ν).map ⋯
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.final_of_initial_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.op.Initial], F.Final
-- Lean.Environment
Lean.Kernel.Exception.declTypeMismatch.inj : ∀ {env : Lean.Kernel.Environment} {decl : Lean.Declaration} {givenType : Lean.Expr} {env_1 : Lean.Kernel.Environment}
  {decl_1 : Lean.Declaration} {givenType_1 : Lean.Expr},
  Lean.Kernel.Exception.declTypeMismatch env decl givenType =
      Lean.Kernel.Exception.declTypeMismatch env_1 decl_1 givenType_1 →
    env = env_1 ∧ decl = decl_1 ∧ givenType = givenType_1
-- Mathlib.Algebra.Star.SelfAdjoint
skewAdjoint.instInhabitedSubtypeMemAddSubgroup : {R : Type u_1} → [inst : AddCommGroup R] → [inst_1 : StarAddMonoid R] → Inhabited ↥(skewAdjoint R)
-- Mathlib.FieldTheory.Relrank
Subfield.lift_relrank_comap_comap_eq_lift_relrank_of_le : ∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A B : Subfield E) (f : L →+* E),
  B ≤ f.fieldRange →
    Cardinal.lift.{v, w} ((Subfield.comap f A).relrank (Subfield.comap f B)) = Cardinal.lift.{w, v} (A.relrank B)
-- Mathlib.CategoryTheory.Monad.Products
/-- The equivalence from algebras for the coproduct monad to the under category.
 -/
CategoryTheory.algebraEquivUnder : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] →
        (CategoryTheory.coprodMonad X).Algebra ≌ CategoryTheory.Under X
-- Mathlib.Data.Finset.Preimage
Finset.sup_preimage_val_id : ∀ {α : Type u} [inst : Lattice α] [inst_1 : OrderBot α] {P : α → Prop} (Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t))
  (Pbot : P ⊥) {t : Finset α} (ht : ∀ x ∈ t, P x), (t.preimage Subtype.val ⋯).sup id = ⟨t.sup id, ⋯⟩
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.ofCompId_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  (t :
    CategoryTheory.Bicategory.LeftExtension f
      (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c))),
  t.ofCompId.right = t.extension
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.of_enorm_bound : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [MeasureTheory.IsFiniteMeasure μ] {f : α → ε},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {C : ENNReal}, C ≠ ⊤ → (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C) → MeasureTheory.MemLp f p μ
-- Batteries.Data.Char.Basic
Char.le_antisymm_iff : ∀ {x y : Char}, x = y ↔ x ≤ y ∧ y ≤ x
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.reduct_Carrier : ∀ {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} (φ : L →ᴸ L') (M : (φ.onTheory T).ModelType),
  ↑(FirstOrder.Language.Theory.ModelType.reduct φ M) = ↑M
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The pullback of `f` and `g` in `C` is isomorphic to the pushout of
`f.op` and `g.op` in `Cᵒᵖ`.  -/
CategoryTheory.Limits.pullbackIsoUnopPushout : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          [h : CategoryTheory.Limits.HasPullback f g] →
            CategoryTheory.Limits.pullback f g ≅ Opposite.unop (CategoryTheory.Limits.pushout f.op g.op)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.ofAddEquivOfDom_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {k : P ≃+ M}
  (H : AddSubmonoid.map k.toAddMonoidHom T = S) (x : P), (f.ofAddEquivOfDom H) x = f (k x)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_beq : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} (h' : k ∈ m), (m.getKey k h' == k) = true
-- Std.Data.DHashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.DHashMap.getKey? : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → α → Option α