mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.MeasurePreserving.integrableOn_comp_preimage : ∀ {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : MeasurableSpace β] {e : α → β}
  {ν : MeasureTheory.Measure β},
  MeasureTheory.MeasurePreserving e μ ν →
    MeasurableEmbedding e →
      ∀ {f : β → ε} {s : Set β}, MeasureTheory.IntegrableOn (f ∘ e) (e ⁻¹' s) μ ↔ MeasureTheory.IntegrableOn f s ν
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instIsOrderedAddMonoid : ∀ {α : Type u_3}, IsOrderedAddMonoid (MeasureTheory.OuterMeasure α)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.instEssSurjObjCompPostOfFull : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) [G.Full], (CategoryTheory.StructuredArrow.post S F G).EssSurj
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.addZ_neg : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.addZ P (W'.neg P) = 0
-- Mathlib.Algebra.Module.ZLattice.Basic
Module.Basis.ofZLatticeComap_apply : ∀ (K : Type u_1) [inst : NormedField K] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace K F] (L : Submodule ℤ E)
  (e : F ≃ₗ[K] E) {ι : Type u_4} (b : Module.Basis ι ℤ ↥L) (i : ι),
  ↑((Module.Basis.ofZLatticeComap K L e b) i) = e.symm ↑(b i)
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.degree_le : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G.Copy H) (v : V)
  [inst : Fintype ↑(G.neighborSet v)] [inst_1 : Fintype ↑(H.neighborSet (f v))], G.degree v ≤ H.degree (f v)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {R₁ R₂ : CategoryTheory.RingObjCat C} {x y : R₁.Hom R₂},
  x = y ↔ x.hom = y.hom
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.proj_toFun : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {proj : Z → B} (self : Bundle.Trivialization F proj),
  ∀ p ∈ self.source, (↑self.toOpenPartialHomeomorph p).1 = proj p
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.mk'_f : ∀ {ι : Type u_1} {ι' : Type u_2} (c : ComplexShape ι) (c' : ComplexShape ι') (f : ι → ι') (hf : Function.Injective f)
  (iff : ∀ (i₁ i₂ : ι), c.Rel i₁ i₂ ↔ c'.Rel (f i₁) (f i₂)) (a : ι),
  (ComplexShape.Embedding.mk' c c' f hf iff).f a = f a
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.zpow : ∀ {α : Type u_1} {M : Type u_3} [inst : DivisionMonoid M] {f : α → M},
  Function.HasFiniteMulSupport f → ∀ (n : ℤ), Function.HasFiniteMulSupport (f ^ n)
-- Init.SimpLemmas
or_iff_right_of_imp : ∀ {a b : Prop}, (a → b) → (a ∨ b ↔ b)
-- Batteries.Data.HashMap.Basic
/-- Folds a function over the elements in the map (in arbitrary order).
```
fold (fun sum _ v => sum + v) 0 (ofList [("one", 1), ("two", 2)]) = 3
```
 -/
Batteries.HashMap.fold : {α : Type u_1} →
  {x : BEq α} → {x_1 : Hashable α} → {δ : Type u_2} → {β : Type u_3} → (δ → α → β → δ) → δ → Batteries.HashMap α β → δ
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
ContinuousLinearMap.compLpL.congr_simp : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_6} {𝕜' : Type u_7}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_6 : RingHomIsometric σ] [inst_7 : Fact (1 ≤ p)] (L L_1 : E →SL[σ] F),
  L = L_1 → ContinuousLinearMap.compLpL p μ L = ContinuousLinearMap.compLpL p μ L_1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.smulRight_one_eq_toSpanSingleton : ∀ (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 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₁] (x : M₁),
  ContinuousLinearMap.smulRight 1 x = ContinuousLinearMap.toSpanSingleton R₁ x
-- Mathlib.Data.PEquiv
PEquiv.eq_some_iff : ∀ {α : Type u} {β : Type v} (f : α ≃. β) {a : α} {b : β}, f.symm b = some a ↔ f a = some b
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.coequalizer_isOpen_iff : ∀ {X Y : TopCat} {f g : X ⟶ Y} (U : Set ↑(CategoryTheory.Limits.coequalizer f g)),
  IsOpen U ↔ IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.coequalizer.π f g)) ⁻¹' U)
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- Characterisation of `2`-Freiman homomorphisms.  -/
isMulFreimanHom_two : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsMulFreimanHom 2 A B f ↔ Set.MapsTo f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a * b = c * d → f a * f b = f c * f d
-- Mathlib.Algebra.Group.WithOne.Basic
MulEquiv.withOneCongr_symm : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : Mul β] (e : α ≃* β), e.withOneCongr.symm = e.symm.withOneCongr
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_map : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.map f m).get? k = Option.map (f k) (m.get? k)
-- Lean.Server.References
/-- Converts an `Import` to its LSP-internal representation.  -/
Lean.Server.ImportInfo.ofImport : Lean.Import → Lean.Lsp.ImportInfo
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffAt.congr_of_eventuallyEq : ∀ {𝕜 : 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 f₁ : M → M'} {x : M}
  {n : WithTop ℕ∞}, ContMDiffAt I I' n f x → f₁ =ᶠ[nhds x] f → ContMDiffAt I I' n f₁ x
-- Mathlib.Data.List.Lookmap
List.lookmap.eq_1 : ∀ {α : Type u_1} (f : α → Option α) (l : List α), List.lookmap f l = List.lookmap.go f l #[]
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Restriction from `R`-linear automorphisms of `M` to `R`-linear endomorphisms of `M`,
promoted to a monoid hom.  -/
LinearEquiv.automorphismGroup.toLinearMapMonoidHom : {R : Type u_1} →
  {M : Type u_5} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (M ≃ₗ[R] M) →* M →ₗ[R] M
-- Mathlib.InformationTheory.Hamming
hammingDist_comp_le_hammingDist : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {γ : ι → Type u_4}
  [inst_2 : (i : ι) → DecidableEq (γ i)] (f : (i : ι) → γ i → β i) {x y : (i : ι) → γ i},
  (hammingDist (fun i => f i (x i)) fun i => f i (y i)) ≤ hammingDist x y
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.one_smul : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] (x : OreLocalization S X), 1 • x = x
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeQuotientEquivQuotientSubtype_mk : ∀ {α : Sort u_1} (p₁ : α → Prop) [s₁ : Setoid α] [s₂ : Setoid (Subtype p₁)] (p₂ : Quotient s₁ → Prop)
  (hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧) (h : ∀ (x y : Subtype p₁), s₂ x y ↔ ↑x ≈ ↑y) (x : α) (hx : p₂ ⟦x⟧),
  (Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h) ⟨⟦x⟧, hx⟩ = ⟦⟨x, ⋯⟩⟧
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- The function `Spec A⁰_f → Proj|D(f)` sending `q` to `{a | aᵢᵐ/fⁱ ∈ q}`.  -/
AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          {𝒜 : ℕ → σ} →
            [inst_3 : GradedRing 𝒜] →
              {f : A} →
                {m : ℕ} →
                  f ∈ 𝒜 m →
                    0 < m →
                      ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj
                                (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace →
                        ↑↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toPresheafedSpace
-- Lean.Meta.Tactic.NormCast
/-- move lemma: LHS has 1 head coe and 0 internal coes,
RHS has 0 head coes and ≥ 1 internal coes  -/
Lean.Meta.NormCast.Label.move : Lean.Meta.NormCast.Label
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.le_orderTop_iff_forall : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] {x : HahnSeries Γ R} {i : WithTop Γ},
  i ≤ x.orderTop ↔ ∀ (j : Γ), ↑j < i → x.coeff j = 0
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
/-- The category whose objects are denoted `⦋n⦌ₛ` for `n : ℕ` and
morphisms `⦋n⦌ₛ ⟶ ⦋m⦌ₛ` are order embeddings `Fin (n.len + 1) ↪o Fin (m.len + 1)`.
(This identifies to a wide subcategory of the category `SemiSimplex`, which
has the "same" objects, and morphisms `Fin (n.len + 1) →o Fin (m.len + 1)`,
see the faithful functor `SemiSimplexCategory.toSimplexCategory`.)  -/
SemiSimplexCategory : Type
-- Lean.InternalExceptionId
Lean.instInhabitedInternalExceptionId.default : Lean.InternalExceptionId
-- Mathlib.Data.W.Constructions
WType.toList.eq_1 : ∀ (γ : Type u) (f : WType.Listβ γ WType.Listα.nil → WType (WType.Listβ γ)),
  WType.toList γ (WType.mk WType.Listα.nil f) = []
-- Mathlib.Data.Finset.Functor
Finset.id_traverse : ∀ {α : Type u} [inst : DecidableEq α] (s : Finset α), Finset.traverse pure s = pure s
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.smul_coe : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_3)
  [inst_3 : CommMonoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M] (s : S)
  (x : ↥(Submodule.torsion' R M S)), ↑(s • x) = s • ↑x
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerivedNatTrans_comp : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (LF'' LF' LF : CategoryTheory.Functor D H) {F F' F'' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α'' : L.comp LF'' ⟶ F'') (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C)
  [inst_3 : L.IsLocalization W] [inst_4 : LF.IsLeftDerivedFunctor α W] [inst_5 : LF'.IsLeftDerivedFunctor α' W]
  (τ' : F'' ⟶ F') (τ : F' ⟶ F),
  CategoryTheory.CategoryStruct.comp (LF''.leftDerivedNatTrans LF' α'' α' W τ') (LF'.leftDerivedNatTrans LF α' α W τ) =
    LF''.leftDerivedNatTrans LF α'' α W (CategoryTheory.CategoryStruct.comp τ' τ)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_constVSub : ∀ (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₁] (p : P₁), (AffineEquiv.constVSub k p).linear = LinearEquiv.neg k
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castSucc_Ici : ∀ {n : ℕ} (i : Fin n), Fin.castSucc '' Set.Ici i = Set.Ico i.castSucc (Fin.last n)
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.span_basisOfIsMaxRank : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ} (hu : NumberField.Units.IsMaxRank u),
  (Submodule.span ℤ (Set.range ⇑(NumberField.Units.basisOfIsMaxRank hu))).toAddSubgroup =
    AddSubgroup.map (NumberField.Units.logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)))
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.toCoalgHom_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₐc[R] B) (a : A), f.toCoalgHom a = f a
-- Mathlib.Topology.Instances.ENNReal.Lemmas
continuous_edist : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α], Continuous fun p => edist p.1 p.2
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
Measurable.of_union₃_range_cover : ∀ {α : Type u_1} {β : Type u_2} {α₁ : Type u_6} {α₂ : Type u_7} {α₃ : Type u_8} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mα₁ : MeasurableSpace α₁} {mα₂ : MeasurableSpace α₂} {mα₃ : MeasurableSpace α₃}
  {i₁ : α₁ → α} {i₂ : α₂ → α} {i₃ : α₃ → α} {f : α → β},
  MeasurableEmbedding i₁ →
    MeasurableEmbedding i₂ →
      MeasurableEmbedding i₃ →
        Set.univ ⊆ Set.range i₁ ∪ Set.range i₂ ∪ Set.range i₃ →
          Measurable (f ∘ i₁) → Measurable (f ∘ i₂) → Measurable (f ∘ i₃) → Measurable f
-- Mathlib.Analysis.Fourier.ZMod
/-- Fourier inversion formula, discrete case.  -/
_private.Mathlib.Analysis.Fourier.ZMod.0.ZMod.auxDFT_auxDFT : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Φ : ZMod N → E),
  ZMod.auxDFT✝ (ZMod.auxDFT✝ Φ) = fun j => ↑N • Φ (-j)
-- Mathlib.Topology.Sheaves.Sheaf
TopCat.instCategorySheaf : (C : Type u_3) →
  [inst : CategoryTheory.Category.{u_1, u_3} C] →
    (X : TopCat) → CategoryTheory.Category.{max u_1 u_2, max (max u_3 u_1) u_2} (TopCat.Sheaf C X)
-- Mathlib.Algebra.Order.Monovary
/-- Two functions antivary iff the rearrangement inequality holds.  -/
antivary_iff_mul_rearrangement : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α},
  Antivary f g ↔ ∀ (i j : ι), f i * g i + f j * g j ≤ f i * g j + f j * g i
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The linear map that makes `canonicalEmbedding` and `mixedEmbedding` commute, see
`commMap_canonical_eq_mixed`.  -/
NumberField.mixedEmbedding.commMap : (K : Type u_1) → [inst : Field K] → ((K →+* ℂ) → ℂ) →ₗ[ℝ] NumberField.mixedEmbedding.mixedSpace K
-- Mathlib.Control.Monad.Cont
ContT.run_throw : ∀ {r : Type u} {m : Type u → Type v} {α : Type w} {ε : Type u_1} [inst : MonadExceptOf ε m] (e : ε) (f : α → m r),
  (throw e).run f = throw e
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.FinMeasSupp.add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : AddZeroClass β]
  {f g : MeasureTheory.SimpleFunc α β}, f.FinMeasSupp μ → g.FinMeasSupp μ → (f + g).FinMeasSupp μ
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv_subset_sdiv_right : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s₁ s₂ t : Set β}, s₁ ⊆ s₂ → s₁ /ₛ t ⊆ s₂ /ₛ t
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.sectionsAddSubmonoid.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat),
  AddMonCat.sectionsAddSubmonoid F =
    { carrier := (F.comp (CategoryTheory.forget AddMonCat)).sections, add_mem' := ⋯, zero_mem' := ⋯ }
-- ProofWidgets.Component.PenroseDiagram
/-- Components to display as labels in the diagram,
stored in the map as name ↦ (type, html).  -/
ProofWidgets.Penrose.DiagramState.embeds : ProofWidgets.Penrose.DiagramState → Std.HashMap String (String × ProofWidgets.Html)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
NonUnitalContinuousFunctionalCalculus.predicate_zero : ∀ (R : Type u_1) {A : Type u_2} {p : outParam (A → Prop)} {inst : CommSemiring R} {inst_1 : Nontrivial R}
  {inst_2 : StarRing R} {inst_3 : MetricSpace R} {inst_4 : IsTopologicalSemiring R} {inst_5 : ContinuousStar R}
  {inst_6 : NonUnitalRing A} {inst_7 : StarRing A} {inst_8 : TopologicalSpace A} {inst_9 : Module R A}
  {inst_10 : IsScalarTower R A A} {inst_11 : SMulCommClass R A A} [self : NonUnitalContinuousFunctionalCalculus R A p],
  p 0
-- Mathlib.Topology.Subpath
/-- **Alias** of `Set.Icc.convexComb`. -/
Path.subpathAux : {a b : ℝ} → ↑(Set.Icc a b) → ↑(Set.Icc a b) → ↑unitInterval → ↑(Set.Icc a b)
-- Mathlib.Topology.CWComplex.Classical.Basic
_private.Mathlib.Topology.CWComplex.Classical.Basic.0.Topology.CWComplex.OfDiscreteClosed.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive n
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- A cokernel cofork for `f` is mapped to a cokernel cofork for `G.map f` if `G` is a functor
which preserves zero morphisms.  -/
CategoryTheory.Limits.CokernelCofork.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {X Y : C} →
              {f : X ⟶ Y} →
                CategoryTheory.Limits.CokernelCofork f →
                  (G : CategoryTheory.Functor C D) →
                    [G.PreservesZeroMorphisms] → CategoryTheory.Limits.CokernelCofork (G.map f)
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
/-- `f z ^ g z` is analytic if `f z` avoids nonpositive reals  -/
AnalyticOnNhd.cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : E → ℂ} {s : Set E},
  AnalyticOnNhd ℂ f s →
    AnalyticOnNhd ℂ g s → (∀ z ∈ s, f z ∈ Complex.slitPlane) → AnalyticOnNhd ℂ (fun z => f z ^ g z) s
-- Mathlib.NumberTheory.LSeries.Convergence
LSeriesSummable_of_abscissaOfAbsConv_lt_re : ∀ {f : ℕ → ℂ} {s : ℂ}, LSeries.abscissaOfAbsConv f < ↑s.re → LSeriesSummable f s
-- Mathlib.GroupTheory.Perm.DomMulAct
DomMulAct.stabilizerMulEquiv_apply : ∀ {α : Type u_1} {ι : Type u_2} {f : α → ι} (g : (↥(MulAction.stabilizer (Equiv.Perm α)ᵈᵐᵃ f))ᵐᵒᵖ) {a : α} {i : ι}
  (h : f a = i), ↑(((DomMulAct.stabilizerMulEquiv f) g i) ⟨a, h⟩) = (DomMulAct.mk.symm ↑(MulOpposite.unop g)) a
-- Mathlib.Order.PartialSups
/-- Version of `ciSup_partialSups_eq` without boundedness assumptions, but requiring a
`CompleteLattice` rather than just a `ConditionallyCompleteLattice`.  -/
iSup_partialSups_eq : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι] [inst_2 : CompleteLattice α]
  (f : ι → α), ⨆ i, (partialSups f) i = ⨆ i, f i
-- Mathlib.Data.Set.Prod
Set.disjoint_prod : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β},
  Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
-- Mathlib.Logic.Equiv.PartialEquiv
/-- A lemma commonly useful when `e` and `e'` are charts of a manifold.  -/
PartialEquiv.mem_symm_trans_source : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) {e' : PartialEquiv α γ} {x : α},
  x ∈ e.source → x ∈ e'.source → ↑e x ∈ (e.symm.trans e').source
-- Mathlib.CategoryTheory.MorphismProperty.CommaSites
CategoryTheory.MorphismProperty.coverPreserving_comap_forget : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} {S : C}
  [P.IsStableUnderComposition] (K : CategoryTheory.Precoverage C) [K.HasIsos] [K.IsStableUnderBaseChange]
  [K.IsStableUnderComposition] [K.HasPullbacks],
  K ≤ P.precoverage →
    CategoryTheory.CoverPreserving
      (CategoryTheory.Precoverage.comap
          ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp (CategoryTheory.Over.forget S)) K).toGrothendieck
      (K.toGrothendieck.over S) (CategoryTheory.MorphismProperty.Over.forget P ⊤ S)
-- Mathlib.Order.Atoms
exists_covBy_le_of_lt : ∀ {α : Type u_4} {a b : α} [inst : Preorder α] [IsStronglyAtomic α], a < b → ∃ x, a ⋖ x ∧ x ≤ b
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_interval : ∀ {a b : ℝ}, MeasureTheory.volume (Set.uIcc a b) = ENNReal.ofReal |b - a|
-- Mathlib.Order.Filter.Bases.Basic
/-- Index of a basis set such that `s i ⊆ t` as an element of `Subtype p`.  -/
Filter.HasBasis.index : {α : Type u_1} →
  {ι : Sort u_4} →
    {l : Filter α} → {p : ι → Prop} → {s : ι → Set α} → l.HasBasis p s → (t : Set α) → t ∈ l → { i // p i }
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_norm_quasispectrum : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A),
  autoParam (p a) NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_norm_quasispectrum._auto_1 →
    IsGreatest ((fun x => ‖x‖) '' quasispectrum 𝕜 a) ‖a‖
-- Mathlib.Algebra.Order.Star.Basic
instIsOrderedModule : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : NonUnitalSemiring A] [inst_5 : StarRing A] [inst_6 : PartialOrder A] [StarOrderedRing A]
  [inst_8 : Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A], IsOrderedModule R A
-- Mathlib.Order.UpperLower.Prod
LowerSet.prod_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s₁ s₂ : LowerSet α} {t₁ t₂ : LowerSet β},
  s₁ ≤ s₂ → t₁ ≤ t₂ → s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.bijective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), Function.Bijective ⇑f
-- Mathlib.Data.ENNReal.Operations
ENNReal.image_coe_Icc : ∀ (x y : NNReal), ENNReal.ofNNReal '' Set.Icc x y = Set.Icc ↑x ↑y
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.mem_nhds_zero : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (U : OpenAddSubgroup G), ↑U ∈ nhds 0
-- Mathlib.Probability.Kernel.Disintegration.Basic
/-- Auxiliary lemma for `IsCondKernel.apply_of_ne_zero`.  -/
_private.Mathlib.Probability.Kernel.Disintegration.Basic.0.MeasureTheory.Measure.IsCondKernel.apply_of_ne_zero_of_measurableSet : ∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω))
  (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] [MeasureTheory.IsFiniteMeasure ρ]
  [MeasurableSingletonClass α] {x : α},
  ρ.fst {x} ≠ 0 → ∀ {s : Set Ω}, MeasurableSet s → (ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.openPartialHomeomorphCoe_symm_apply : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [inst_5 : OrderTopology 𝕜]
  [inst_6 : DiscreteTopology ↥(AddSubgroup.zmultiples p)] (x : AddCircle p),
  ↑(AddCircle.openPartialHomeomorphCoe p a).symm x = ↑((AddCircle.equivIco p a) x)
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_single : ∀ {M : Type u_2} {α : Sort u_4} [inst : CommMonoid M] (f : α → M) (a : α),
  (∀ (x : α), x ≠ a → f x = 1) → ∏ᶠ (x : α), f x = f a
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg.eq_1 : ∀ {α : Type u_2} [inst : Neg α], Set.neg = { neg := Set.preimage Neg.neg }
-- Mathlib.Probability.Moments.CovarianceBilinDual
/-- Linear map from the dual to `Lp` equal to `MemLp.toLp` if `MemLp id p μ` and to 0 otherwise.  -/
StrongDual.toLpₗ : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {mE : MeasurableSpace E} →
      {𝕜 : Type u_2} →
        [inst_1 : NontriviallyNormedField 𝕜] →
          [inst_2 : NormedSpace 𝕜 E] →
            (μ : MeasureTheory.Measure E) → (p : ENNReal) → StrongDual 𝕜 E →ₗ[𝕜] ↥(MeasureTheory.Lp 𝕜 p μ)