mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Condensed.Light.InternallyProjective
/-- Given a `P : LightProfinite`, the light free light condensed module `R[P]` is internally projective
if and only if, for all `A B : LightCondMod R`, for all epimorphisms `e : A ⟶ B`, for all
`S : LightProfinite` and all morphisms `g : R[P × S] ⟶ B`, there exists a `S' : LightProfinite`
with a surjection `π : S' ⟶ S` and a morphism `g' : R[P × S'] ⟶ A`, making the diagram
```
R[P × S'] --> A
  |           |
  v           v
R[P × S]  --> B
```
commute.
 -/
LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition : ∀ (R : Type u) [inst : CommRing R] (P : LightProfinite),
  CategoryTheory.InternallyProjective ((LightCondensed.free R).obj P.toCondensed) ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [CategoryTheory.Epi e] (S : LightProfinite)
      (g : (LightCondensed.free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj P S).toCondensed ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)),
          ∃ g',
            CategoryTheory.CategoryStruct.comp
                ((LightCondensed.free R).map
                  (lightProfiniteToLightCondSet.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P π)))
                g =
              CategoryTheory.CategoryStruct.comp g' e
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.neg_mk : ∀ {M : Type u_2} [inst : AddCommGroup M] (m : M) (s : ℕ+), -DivisibleHull.mk m s = DivisibleHull.mk (-m) s
-- Mathlib.Data.Fintype.Quotient
Quotient.listChoice.eq_def : ∀ {ι : Type u_1} [inst : DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)} {l : List ι}
  (q : (i : ι) → i ∈ l → Quotient (S i)),
  Quotient.listChoice q =
    match l, q with
    | [], q => ⟦fun a a_1 => nomatch a, a_1⟧
    | i :: tail, q =>
      (List.Pi.head q).liftOn₂ (Quotient.listChoice (List.Pi.tail q)) (fun x1 x2 => ⟦List.Pi.cons i tail x1 x2⟧) ⋯
-- Mathlib.RingTheory.FormalGroup.Basic
/-- A structure for a 1-dimensional formal group law over `R`.  -/
FormalGroup : (R : Type u_1) → [CommRing R] → Type u_1
-- Mathlib.Algebra.Group.Action.Defs
/-- The right and left actions of `M` on `α` are equal.  -/
IsCentralVAdd.op_vadd_eq_vadd : ∀ {M : Type u_9} {α : Type u_10} {inst : VAdd M α} {inst_1 : VAdd Mᵃᵒᵖ α} [self : IsCentralVAdd M α] (m : M) (a : α),
  AddOpposite.op m +ᵥ a = m +ᵥ a
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.SearchControl.stop.sizeOf_spec : sizeOf Lean.Server.FileWorker.SignatureHelp.SearchControl.stop = 1
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Coercion to a function for a scalar-valued continuous map multiplying a vector-valued one
(as opposed to `ContinuousMap.coe_smul` which is multiplication by a constant scalar).  -/
ContinuousMap.coe_smul' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_2} [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  [inst_6 : ContinuousSMul R M] (f : C(α, R)) (g : C(α, M)), ⇑(f • g) = ⇑f • ⇑g
-- Init.Data.List.Sublist
List.eq_nil_of_subset_nil : ∀ {α : Type u_1} {l : List α}, l ⊆ [] → l = []
-- Mathlib.Data.List.Permutation
List.perm_permutations'_iff : ∀ {α : Type u_1} {s t : List α}, s.permutations'.Perm t.permutations' ↔ s.Perm t
-- Init.Data.BitVec.Basic
/-- `NatCast` instance for `BitVec`.
 -/
BitVec.instNatCast : {w : ℕ} → NatCast (BitVec w)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.mk.sizeOf_spec : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜] [inst_6 : SizeOf ι]
  [inst_7 : SizeOf σ] [inst_8 : SizeOf A] (toSubsemiring : Subsemiring A)
  (is_homogeneous' : DirectSum.SetLike.IsHomogeneous 𝒜 toSubsemiring),
  sizeOf { toSubsemiring := toSubsemiring, is_homogeneous' := is_homogeneous' } = 1 + sizeOf toSubsemiring
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
ConcaveOn.condExp_map_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} (hm : m ≤ mα)
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  ConcaveOn ℝ s φ →
    UpperSemicontinuousOn φ s →
      (∀ᵐ (a : α) ∂μ, f a ∈ s) →
        IsClosed s → MeasureTheory.Integrable f μ → MeasureTheory.Integrable (φ ∘ f) μ → μ[φ ∘ f | m] ≤ᵐ[μ] φ ∘ μ[f | m]
-- Mathlib.MeasureTheory.Group.LIntegral
MeasurableEquiv.mulRight.congr_simp : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableMul G] (g g_1 : G),
  g = g_1 → MeasurableEquiv.mulRight g = MeasurableEquiv.mulRight g_1
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.W_isInvertedBy_presheafFiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A], J.W.IsInvertedBy Φ.presheafFiber
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Associate a `PartialEquiv` to an `Equiv`.  -/
Equiv.toPartialEquiv : {α : Type u_1} → {β : Type u_2} → α ≃ β → PartialEquiv α β
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
_private.Mathlib.Analysis.InnerProductSpace.Projection.Basic.0.termAbsR : Lean.ParserDescr
-- Mathlib.Topology.Category.CompactlyGenerated
/-- `CompactlyGenerated.{u, w}` is the type of `u`-compactly generated `w`-small topological spaces.
This should always be used with explicit universe parameters.  -/
CompactlyGenerated : Type (w + 1)
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.tensor_apply : ∀ {W X Y Z : Type u} (f : W ⟶ X) (g : Y ⟶ Z) (p : CategoryTheory.MonoidalCategoryStruct.tensorObj W Y),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) p =
    ((CategoryTheory.ConcreteCategory.hom f) p.1, (CategoryTheory.ConcreteCategory.hom g) p.2)
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.ExceptT.bindCont.match_1.splitter : {ε α : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((e : ε) → motive (Except.error e)) → motive x
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.deriv_cgf_zero : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  0 ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    deriv (ProbabilityTheory.cgf X μ) 0 = (∫ (x : Ω), X x ∂μ) / μ.real Set.univ
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β] (f : sSupHom α β), f.comp (sSupHom.id α) = f
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Arithmetic progressions of length three are unchanged under `2`-Freiman isomorphisms.  -/
IsAddFreimanIso.threeAPFree_congr : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {s : Set α} {t : Set β} {f : α → β},
  IsAddFreimanIso 2 s t f → (ThreeAPFree s ↔ ThreeAPFree t)
-- Mathlib.Algebra.GradedMonoid
SetLike.prod_pow_mem_graded : ∀ {ι : Type u_2} {R : Type u_3} {S : Type u_4} [inst : SetLike S R] [inst_1 : CommMonoid R] [inst_2 : AddCommMonoid ι]
  (A : ι → S) [SetLike.GradedMonoid A] {κ : Type u_5} (i : κ → ι) (g : κ → R) {F : Finset κ} (n : κ → ℕ),
  (∀ k ∈ F, g k ∈ A (i k)) → ∏ k ∈ F, g k ^ n k ∈ A (∑ k ∈ F, n k • i k)
-- Mathlib.Data.FP.Basic
FP.Float.instSub : [C : FP.FloatCfg] → Sub FP.Float
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_sdiff_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi a \ Set.Ici b = Set.Ioo a b
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- The Bessel potential `x ↦ (1 + ‖x‖ ^ 2) ^ r` has temperate growth.  -/
Function.hasTemperateGrowth_one_add_norm_sq_rpow : ∀ (H : Type u_8) [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℝ H] (r : ℝ),
  Function.HasTemperateGrowth fun x => (1 + ‖x‖ ^ 2) ^ r
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α] {f : α → β → γ} {k : α},
  m.WF → (Std.HashMap.Raw.map f m).getKey! k = m.getKey! k
-- Mathlib.Algebra.Notation.Lemmas
one_le_dite : ∀ {α : Type u_1} [inst : One α] {p : Prop} [inst_1 : Decidable p] {a : p → α} {b : ¬p → α} [inst_2 : LE α],
  (∀ (h : p), 1 ≤ a h) → (∀ (h : ¬p), 1 ≤ b h) → 1 ≤ dite p a b
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_le_one_iff : ∀ {a : Cardinal.{u}}, Cardinal.lift.{v, u} a ≤ 1 ↔ a ≤ 1
-- Mathlib.RingTheory.Polynomial.Ideal
Polynomial.ker_constantCoeff : ∀ {R : Type u_1} [inst : CommRing R], RingHom.ker Polynomial.constantCoeff = Ideal.span {Polynomial.X}
-- Mathlib.Topology.MetricSpace.Algebra
Submonoid.lipschitzMul : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : Monoid β] [LipschitzMul β] (s : Submonoid β), LipschitzMul ↥s
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.mul_apply : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] (f g : F →WOT[𝕜₂] F) (x : F), (f * g) x = f (g x)
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHom.restrictScalars : (R : Type u_1) →
  {S : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Semiring A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R S] →
                  [inst_5 : Algebra S A] →
                    [inst_6 : Algebra S B] →
                      [inst_7 : Algebra R A] →
                        [inst_8 : Algebra R B] →
                          [IsScalarTower R S A] →
                            [IsScalarTower R S B] → [inst_11 : Star A] → [inst_12 : Star B] → (A →⋆ₐ[S] B) → A →⋆ₐ[R] B
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∩ t₂)[k]! = default
-- Mathlib.Tactic.DuplicateDecls
Mathlib.Tactic.DuplicateDecls.Target.defs.sizeOf_spec : sizeOf Mathlib.Tactic.DuplicateDecls.Target.defs = 1
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.symm_self_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) (β : Y ≅ Z), α.symm ≪≫ α ≪≫ β = β
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.ofFaithful.eq_1 : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal]
  [inst_5 : F.Faithful] [inst_6 : CategoryTheory.BraidedCategory D]
  (β :
    (X Y : C) →
      CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X)
  (w :
    ∀ (X Y : C),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.map (β X Y).hom) =
        CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.Functor.LaxMonoidal.μ F Y X)),
  CategoryTheory.BraidedCategory.ofFaithful F β w =
    { braiding := β, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯,
      hexagon_reverse := ⋯ }
-- Std.Http.Data.Chunk
Std.Http.Chunk.instDecidableEqExtensionName : DecidableEq Std.Http.Chunk.ExtensionName
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.Hom.match_1.eq_2 : ∀ {C : Type u_1} (motive : CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Sort u_2) (a : C)
  (h_1 : (X Y : C) → motive (CategoryTheory.WithTerminal.of X) (CategoryTheory.WithTerminal.of Y))
  (h_2 : (a : C) → motive CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of a))
  (h_3 : (x : CategoryTheory.WithTerminal C) → motive x CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of a with
    | CategoryTheory.WithTerminal.of X, CategoryTheory.WithTerminal.of Y => h_1 X Y
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of a => h_2 a
    | x, CategoryTheory.WithTerminal.star => h_3 x) =
    h_2 a
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
/-- Conditional expectation of a function, with notation `μ[f | m]`.

It is defined as 0 if any one of the following conditions is true:
- `m` is not a sub-σ-algebra of `m₀`,
- `μ` is not σ-finite with respect to `m`,
- `f` is not integrable. 

[Wikidata Q772232](https://www.wikidata.org/wiki/Q772232) -/
MeasureTheory.condExp : {α : Type u_5} →
  {E : Type u_6} →
    MeasurableSpace α →
      {m₀ : MeasurableSpace α} →
        [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → MeasureTheory.Measure α → (α → E) → α → E
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- The canonical isomorphism between `(Fork.ofι ι w).unop` and `Cofork.ofπ ι.unop w.unop`.  -/
CategoryTheory.Limits.Fork.ofιUnopIsoOfπ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y P : Cᵒᵖ} →
      {f g : X ⟶ Y} →
        (ι ι' : P ⟶ X) →
          (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g) →
            (w' :
                CategoryTheory.CategoryStruct.comp f.unop ι'.unop = CategoryTheory.CategoryStruct.comp g.unop ι'.unop) →
              ι = ι' → ((CategoryTheory.Limits.Fork.ofι ι w).unop ≅ CategoryTheory.Limits.Cofork.ofπ ι'.unop w')
-- Mathlib.Analysis.Convex.Quasiconvex
QuasiconvexOn.convex_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder β] [inst_4 : SMul 𝕜 E] {s : Set E} {f : E → β},
  QuasiconvexOn 𝕜 s f → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ f x < r}
-- Mathlib.Tactic.NormNum.Core
/-- `norm_num1` normalizes numerical expressions in the goal. It is a basic version of `norm_num`
that does not call `simp`.

By default, it supports the operations `+` `-` `*` `/` `⁻¹` `^` and `%` over types with (at least)
an `AddMonoidWithOne` instance, such as `ℕ`, `ℤ`, `ℚ`, `ℝ`, `ℂ`. If the goal has the form `A = B`,
`A ≠ B`, `A < B` or `A ≤ B`, where `A` and `B` are numerical expressions, `norm_num1` will try to
close it. It also has a relatively simple primality prover.
:e
This tactic is extensible. Extensions can allow `norm_num1` to evaluate more kinds of expressions,
or to prove more kinds of propositions. See the `@[norm_num]` attribute for further information on
extending `norm_num1`.

* `norm_num1 at l` normalizes at location(s) `l`.

Examples:
```lean
example : 43 ≤ 74 + (33 : ℤ) := by norm_num1
example : ¬ (7-2)/(2*3) ≥ (1:ℝ) + 2/(3^2) := by norm_num1
```
 -/
Mathlib.Tactic.normNum1 : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
tangentMap_comp : ∀ {𝕜 : 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'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} {g : M' → M''}, MDiff g → MDiff f → tangentMap I I'' (g ∘ f) = tangentMap I' I'' g ∘ tangentMap I I' f