mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- Naturality lemma for `ΓHomEquiv` analogous to `Adjunction.homEquiv_naturality_left_symm`.  -/
CategoryTheory.Sheaf.ΓHomEquiv_naturality_left_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] {X' X : A} {F : CategoryTheory.Sheaf J A} (f : X' ⟶ X)
  (g : X ⟶ (CategoryTheory.Sheaf.Γ J A).obj F),
  CategoryTheory.Sheaf.ΓHomEquiv.symm (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const Cᵒᵖ).map f)
      (CategoryTheory.Sheaf.ΓHomEquiv.symm g)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.trajMeasure.eq_1 : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)] (μ₀ : MeasureTheory.Measure (X 0))
  (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1)))
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)],
  ProbabilityTheory.Kernel.trajMeasure μ₀ κ =
    (MeasureTheory.Measure.map (⇑(MeasurableEquiv.piUnique fun i => X ↑i).symm) μ₀).bind
      ⇑(ProbabilityTheory.Kernel.traj κ 0)
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Composition on the left by a (continuous) homomorphism of topological semirings, as a
`RingHom`.  Similar to `RingHom.compLeft`.  -/
RingHom.compLeftContinuous : (α : Type u_1) →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] →
          [inst_2 : Semiring β] →
            [inst_3 : IsTopologicalSemiring β] →
              [inst_4 : TopologicalSpace γ] →
                [inst_5 : Semiring γ] →
                  [inst_6 : IsTopologicalSemiring γ] → (g : β →+* γ) → Continuous ⇑g → C(α, β) →+* C(α, γ)
-- Mathlib.Order.Hom.Set
/-- We can regard an order embedding as an order isomorphism to its range.  -/
OrderEmbedding.orderIso : {α : Type u_1} → {β : Type u_2} → [inst : LE α] → [inst_1 : LE β] → {f : α ↪o β} → α ≃o ↑(Set.range ⇑f)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.eq_C_of_degree_eq_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R},
  m.degree f = 0 → f = MvPolynomial.C (m.leadingCoeff f)
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.fvars : Lean.Meta.AbstractMVars.State → Array Lean.Expr
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_inj : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {p : ℕ},
  0 < p → ∀ {f g : MvPolynomial σ R}, (MvPolynomial.expand p) f = (MvPolynomial.expand p) g ↔ f = g
-- Init.Prelude
instInhabitedExcept : {ε : Type u} → {α : Type v} → [Inhabited ε] → Inhabited (Except ε α)
-- Mathlib.SetTheory.ZFC.Cardinal
ZFSet.lift_card_iUnion_le_sum_card : ∀ {α : Type u} [inst : Small.{v, u} α] {f : α → ZFSet.{v}},
  Cardinal.lift.{u, v} (ZFSet.iUnion fun i => f i).card ≤ Cardinal.sum fun i => (f i).card
-- Mathlib.CategoryTheory.Sites.Coherent.Basic
/-- The regular Grothendieck topology on a preregular category `C`.
 -/
CategoryTheory.regularTopology : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Preregular C] → CategoryTheory.GrothendieckTopology C
-- Init.Data.UInt.Bitwise
instAssociativeUSizeHXor : Std.Associative fun x1 x2 => x1 ^^^ x2
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Property ensuring that the model with corners `I` defines manifolds without boundary. This
differs from the more general `BoundarylessManifold`, which requires every point on the manifold
to be an interior point.  -/
ModelWithCorners.Boundaryless : {𝕜 : 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] → ModelWithCorners 𝕜 E H → Prop
-- Mathlib.Order.Interval.Finset.Defs
Set.fintypeUIcc : {α : Type u_1} → [inst : Lattice α] → [LocallyFiniteOrder α] → (a b : α) → Fintype ↑(Set.uIcc a b)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_erase : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {fallback : β},
  Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl a fallback =
    if compare k a = Ordering.eq then fallback else Std.DTreeMap.Internal.Impl.Const.getD t a fallback
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
sup_mul₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : SemilatticeSup G₀] [MulPosReflectLT G₀] {c : G₀},
  0 ≤ c → ∀ (a b : G₀), (a ⊔ b) * c = a * c ⊔ b * c
-- Lean.Meta.Basic
Lean.Meta.mkFreshExprMVarAt : Lean.LocalContext →
  Lean.LocalInstances →
    Lean.Expr →
      optParam Lean.MetavarKind Lean.MetavarKind.natural →
        optParam Lean.Name Lean.Name.anonymous → optParam ℕ 0 → Lean.MetaM Lean.Expr
-- Init.Core
/-- Heterogeneous equality is transitive.  -/
HEq.trans : ∀ {α β φ : Sort u} {a : α} {b : β} {c : φ}, a ≍ b → b ≍ c → a ≍ c
-- Mathlib.CategoryTheory.Limits.Final
/-- When `F : C ⥤ D` is final, and `G : D ⥤ E` has a colimit, then `F ⋙ G` has a colimit also and
`colimit (F ⋙ G) ≅ colimit G`.  -/
CategoryTheory.Functor.Final.colimitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : F.Final] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                (G : CategoryTheory.Functor D E) →
                  [inst_4 : CategoryTheory.Limits.HasColimit G] →
                    CategoryTheory.Limits.colimit (F.comp G) ≅ CategoryTheory.Limits.colimit G
-- Mathlib.Data.Holor
Holor.slice.eq_1 : ∀ {α : Type} {d : ℕ} {ds : List ℕ} (x : Holor α (d :: ds)) (i : ℕ) (h : i < d) (is : HolorIndex ds),
  x.slice i h is = x ⟨i :: ↑is, ⋯⟩
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.μ_δ : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.Monoidal] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
      (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.coe_mul : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] (x y : ↑(Set.Icc 0 1)),
  ↑(x * y) = ↑x * ↑y
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.le_comap_single_pi : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)] [inst_1 : DecidableEq ι]
  (S : (i : ι) → AddSubmonoid (M i)) {I : Set ι} {i : ι},
  S i ≤ AddSubmonoid.comap (AddMonoidHom.single M i) (AddSubmonoid.pi I S)
-- Mathlib.Algebra.GroupWithZero.Action.ConjAct
ConjAct.toConjAct_zero : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀], ConjAct.toConjAct 0 = 0
-- Mathlib.Data.Finset.NAry
Finset.card_image₂_singleton_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} (t : Finset β) {a : α},
  Function.Injective (f a) → (Finset.image₂ f {a} t).card = t.card
-- Mathlib.Data.Set.Operations
Set.sdiff_eq : ∀ {α : Type u} (s t : Set α), s \ t = s ∩ tᶜ
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
PartialOrder.mem_nerve_nonDegenerate_iff_injective : ∀ {X : Type u_1} [inst : PartialOrder X] {n : ℕ} (s : (CategoryTheory.nerve X).obj (Opposite.op { len := n })),
  s ∈ (CategoryTheory.nerve X).nonDegenerate n ↔ Function.Injective s.obj
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
MeasureTheory.integral_fintype : ∀ {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] {f : X → E}
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [MeasurableSingletonClass X] {μ : MeasureTheory.Measure X}
  [inst_4 : Fintype X], MeasureTheory.Integrable f μ → ∫ (x : X), f x ∂μ = ∑ x, μ.real {x} • f x
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.hasSum_symmetricIco_int_iff : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : ℤ → α} {a : α},
  HasSum f a (SummationFilter.symmetricIco ℤ) ↔
    Filter.Tendsto (fun N => ∑ n ∈ Finset.Ico (-↑N) ↑N, f n) Filter.atTop (nhds a)
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_pos : ∀ {x : ℝ}, x ∈ Set.Ioo 0 1 → 0 < Real.artanh x
-- Mathlib.Analysis.Normed.Group.Uniform
enorm_map : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
  [inst_2 : FunLike 𝓕 E F] [IsometryClass 𝓕 E F] [ZeroHomClass 𝓕 E F] (f : 𝓕) (x : E), ‖f x‖ₑ = ‖x‖ₑ
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUInt64HXorOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ^^^ x2) 0
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_filter_not_add_sum_filter : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] (s : Finset ι) (p : ι → Prop) [inst_1 : DecidablePred p]
  [inst_2 : (x : ι) → Decidable ¬p x] (f : ι → M), ∑ x ∈ s with ¬p x, f x + ∑ x ∈ s with p x, f x = ∑ x ∈ s, f x
-- Mathlib.Order.Category.BoolAlg
BoolAlg.ext_iff : ∀ {X Y : BoolAlg} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- `f` has the derivative `f'` at the point `x` in the sense of strict differentiability.

That is, `f y - f z = (y - z) • f' + o(y - z)` as `y, z → x`.  -/
HasStrictDerivAt : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type v} →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module 𝕜 F] → [inst_3 : TopologicalSpace F] → [ContinuousSMul 𝕜 F] → (𝕜 → F) → F → 𝕜 → Prop
-- Lean.Util.Recognizers
Lean.Expr.app2? : Lean.Expr → Lean.Name → Option (Lean.Expr × Lean.Expr)
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.degenerate_eq_univ_of_hasDimensionLT : ∀ (X : SSet) (d : ℕ) [X.HasDimensionLT d] (n : ℕ),
  autoParam (d ≤ n) SSet.degenerate_eq_univ_of_hasDimensionLT._auto_1 → X.degenerate n = Set.univ
-- Mathlib.CategoryTheory.Preadditive.Indization
CategoryTheory.instHasFiniteBiproductsInd : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteColimits C], CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Ind C)
-- Mathlib.Data.Set.Equitable
Set.Subsingleton.equitableOn : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring β] [inst_1 : PartialOrder β] [IsOrderedRing β] {s : Set α},
  s.Subsingleton → ∀ (f : α → β), s.EquitableOn f
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.mem_atBot_sets : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] [Nonempty α] {s : Set α},
  s ∈ Filter.atBot ↔ ∃ a, ∀ b ≤ a, b ∈ s
-- Mathlib.Data.Part
Part.mk.injEq : ∀ {α : Type u} (Dom : Prop) (get : Dom → α) (Dom_1 : Prop) (get_1 : Dom_1 → α),
  ({ Dom := Dom, get := get } = { Dom := Dom_1, get := get_1 }) = (Dom = Dom_1 ∧ get ≍ get_1)
-- Mathlib.Data.Nat.Find
Nat.findGreatest_is_greatest : ∀ {k : ℕ} {P : ℕ → Prop} [inst : DecidablePred P] {n : ℕ}, Nat.findGreatest P n < k → k ≤ n → ¬P k
-- Mathlib.RingTheory.DividedPowers.Basic
/-- The coercion from the divided powers structures to functions  -/
instCoeFunDividedPowersForallNatForall : {A : Type u_1} → [inst : CommSemiring A] → (I : Ideal A) → CoeFun (DividedPowers I) fun x => ℕ → A → A
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Functoriality of `yonedaCollectionPresheaf A F` in `F`.  -/
CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {F G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} →
        (F ⟶ G) →
          (CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F ⟶
            CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A G)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- **Alias** of `Matroid.eRk_eq_eRk_sdiff_eRk_le_zero`. -/
Matroid.eRk_eq_eRk_diff_eRk_le_zero : ∀ {α : Type u_1} {M : Matroid α} {Y : Set α} (X : Set α), M.eRk Y ≤ 0 → M.eRk (X \ Y) = M.eRk X
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.mkHom_hom : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  {s t : CategoryTheory.Limits.Cofork f g} (k : s.pt ⟶ t.pt) (w : CategoryTheory.CategoryStruct.comp s.π k = t.π),
  (CategoryTheory.Limits.Cofork.mkHom k w).hom = k
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
Finset.smul_prod_perm : ∀ {N : Type u_2} [inst : CommMonoid N] {G : Type u_4} [inst_1 : Group G] [inst_2 : MulDistribMulAction G N]
  [inst_3 : Fintype G] (b : N) (g : G), g • ∏ h, h • b = ∏ h, h • b
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_sub : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  {f g : E →SL[σ] F},
  ContinuousLinearMapWOT.ofCLM (f - g) = ContinuousLinearMapWOT.ofCLM f - ContinuousLinearMapWOT.ofCLM g
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.card_sphere_le_rothNumberNat : ∀ (n d k : ℕ), (Behrend.sphere n d k).card ≤ rothNumberNat ((2 * d - 1) ^ n)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_smul : ∀ {R : Type u_1} {A : Type u_3} {E : Type u_4} [inst : SMul R E] (c : R) (x : WithCStarModule A E),
  (WithCStarModule.equiv A E) (c • x) = c • (WithCStarModule.equiv A E) x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- The cosine of `π / 6` is `√3 / 2`.  -/
Real.cos_pi_div_six : Real.cos (Real.pi / 6) = √3 / 2
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuous_iff_limsup_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : CompleteLinearOrder γ] {f : α → γ},
  UpperSemicontinuous f ↔ ∀ (x : α), Filter.limsup f (nhds x) ≤ f x
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_inv : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (x : K),
  ArchimedeanClass.stdPart x⁻¹ = (ArchimedeanClass.stdPart x)⁻¹
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addIndex_union_le : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  (K₁ K₂ : TopologicalSpace.Compacts G) {V : Set G},
  (interior V).Nonempty →
    MeasureTheory.Measure.haar.addIndex (K₁.carrier ∪ K₂.carrier) V ≤
      MeasureTheory.Measure.haar.addIndex K₁.carrier V + MeasureTheory.Measure.haar.addIndex K₂.carrier V
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstr : Type
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.nil.hinj : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {V_1 : Type u} {G_1 : SimpleGraph V_1} {u_1 : V_1},
  V = V_1 → G ≍ G_1 → u ≍ u_1 → u ≍ u_1 → SimpleGraph.Walk.nil ≍ SimpleGraph.Walk.nil → V = V_1 ∧ G ≍ G_1 ∧ u ≍ u_1
-- Init.Sym.Simp.SimprocDSL
/-- Apply `a`, then apply `b` to the result.  -/
Lean.Parser.Sym.Simp.andThen : Lean.TrailingParserDescr
-- Lean.Meta.Tactic.Grind.Types
/-- Restore backtrackable parts of the state.  -/
Lean.Meta.Grind.SavedState.restore : Lean.Meta.Grind.SavedState → Lean.Meta.Grind.GrindM Unit
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- Constructor for morphisms to `X.opcycles`.  -/
CategoryTheory.Abelian.SpectralObject.liftOpcycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (fg : i ⟶ k) →
                    (h : CategoryTheory.CategoryStruct.comp f g = fg) →
                      {A : C} →
                        {n : ℤ} →
                          (x : A ⟶ (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg)) →
                            CategoryTheory.CategoryStruct.comp x
                                  ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) =
                                0 →
                              (A ⟶ X.opcycles f g n)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral_eq_of_subset : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal)
  {s : Finset ENNReal},
  (∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s) → f.lintegral μ = ∑ x ∈ s, x * μ (⇑f ⁻¹' {x})
-- Mathlib.Data.Set.Function
Set.LeftInvOn.surjOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α},
  Set.LeftInvOn f' f s → Set.MapsTo f s t → Set.SurjOn f' t s
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.coe_re : ∀ (z : UpperHalfPlane), (↑z).re = z.re
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- The left inverse of `f : E →ₗ[𝕜] F`.

If `f` is not injective, then we use the junk value `0`.  -/
LinearMap.leftInverse : {K : Type u_3} →
  {V : Type u_4} →
    {V' : Type u_5} →
      [inst : DivisionRing K] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : AddCommGroup V'] → [inst_3 : Module K V] → [inst_4 : Module K V'] → (V →ₗ[K] V') → V' →ₗ[K] V
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.PreDiscrTree.mk : {α : Type} →
  Std.HashMap Lean.Meta.LazyDiscrTree.Key ℕ →
    Array (Array (Lean.Meta.LazyDiscrTree.LazyEntry α)) → Lean.Meta.LazyDiscrTree.PreDiscrTree α
-- Mathlib.Order.Bounds.Basic
/-- When there is a global maximum, every set is bounded above.  -/
OrderTop.bddAbove : ∀ {α : Type u_1} [inst : Preorder α] [OrderTop α] (s : Set α), BddAbove s
-- Mathlib.Logic.Equiv.Nat
Equiv.natSumNatEquivNat_apply : ⇑Equiv.natSumNatEquivNat = Sum.elim (fun x => 2 * x) fun x => 2 * x + 1
-- Init.System.IO
IO.FS.FileType.dir.sizeOf_spec : sizeOf IO.FS.FileType.dir = 1
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.body : Lean.IR.Alt → Lean.IR.FnBody
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_insert_one : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Set R), Subsemiring.closure (insert 1 s) = Subsemiring.closure s
-- Mathlib.Order.CompleteLattice.Basic
iSup_congr : ∀ {α : Type u_1} {ι : Sort u_4} [inst : SupSet α] {f g : ι → α}, (∀ (i : ι), f i = g i) → ⨆ i, f i = ⨆ i, g i
-- Mathlib.Algebra.Module.Injective
Module.Injective.pi : ∀ (R : Type u) [inst : Ring R] {ι : Type w} (M : ι → Type v) [Small.{v, u} R] [inst_2 : (i : ι) → AddCommGroup (M i)]
  [inst_3 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Injective R (M i)], Module.Injective R ((i : ι) → M i)
-- Batteries.Logic
/-- **Alias** of `congrFun₃`. -/
congr_fun₃ : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4}
  {f g : (a : α) → (b : β a) → (c : γ a b) → δ a b c}, f = g → ∀ (a : α) (b : β a) (c : γ a b), f a b c = g a b c
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.isIso_prodComparison_of_preservesLimit_pair : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A B : C) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F],
  CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)
-- Mathlib.Data.List.Permutation
List.permutations.eq_1 : ∀ {α : Type u_1} (l : List α), l.permutations = l :: l.permutationsAux []
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.impFrom.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
CategoryTheory.Iso.toLinearEquiv.eq_1 : ∀ {R : Type u} [inst : Ring R] {X Y : ModuleCat R} (i : X ≅ Y),
  i.toLinearEquiv = LinearEquiv.ofLinearMap (ModuleCat.Hom.hom i.hom) (ModuleCat.Hom.hom i.inv) ⋯ ⋯
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_natCast_add : ∀ (r : ENNReal) (n : ℕ), ⌈↑n + r⌉ₑ = ↑n + ⌈r⌉ₑ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.mk_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W)
  (inr : Z ⟶ W) (eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr),
  (CategoryTheory.Limits.PushoutCocone.mk inl inr eq).inr = inr
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.mem_lpMeas_self : ∀ {α : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {p : ENNReal} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : ↥(MeasureTheory.Lp F p μ)),
  f ∈ MeasureTheory.lpMeas F 𝕜 m0 p μ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.anodyneExtensions_eq_retracts_transfiniteCompositionsOfShape : SSet.anodyneExtensions =
  ((CategoryTheory.MorphismProperty.coproducts.{u, u, u + 1}
            SSet.modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape
      ℕ).retracts
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_eq_toList_rco : ∀ {m n : ℤ}, (m<...n).toList = ((m + 1)...n).toList
-- Mathlib.Tactic.DeriveFintype
Mathlib.Deriving.Fintype.mkFintype : Lean.Name → Lean.Elab.Command.CommandElabM Bool
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- Interpret `Finsupp.restrictSupportEquiv` as a linear equivalence between
`supported M R s` and `s →₀ M`.  -/
AddMonoidAlgebra.supportedEquivFinsupp : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → [inst_2 : Module R S] → (s : Set M) → ↥(AddMonoidAlgebra.supported R S s) ≃ₗ[R] ↑s →₀ S
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_alter_of_not_compare_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β}, ¬cmp k k' = Ordering.eq → (k' ∈ t.alter k f ↔ k' ∈ t)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
isClosed_setOfPred_lipschitzOnWith : ∀ {α : Type u_4} {β : Type u_5} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (K : NNReal) (s : Set α),
  IsClosed {f | LipschitzOnWith K f s}
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α}
  (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ Std.DTreeMap.Const.insertMany t l},
  (Std.DTreeMap.Const.insertMany t l).getKey k h' = t.getKey k ⋯
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A B : CategoryTheory.Endofunctor.Coalgebra F} {f g : A ⟶ B},
  autoParam (f.f = g.f) CategoryTheory.Endofunctor.Coalgebra.ext._auto_1 → f = g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.compare_minKeyD_modify_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : β → β} {fallback : α},
      compare ((Std.DTreeMap.Internal.Impl.Const.modify k f t).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
-- Mathlib.Algebra.Order.Monoid.ToMulBot
WithZero.toMulBot_zero : ∀ {α : Type u} [inst : Add α], WithZero.toMulBot 0 = Multiplicative.ofAdd ⊥
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_right_inj : ∀ {M : Type u_1} [inst : Monoid M] {a b c : M}, IsUnit a → (a * b = a * c ↔ b = c)