mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Weights.Linear
/-- Forgetting the action of `L`,
the spaces `genWeightSpace M χ` and `shiftedGenWeightSpace R L M χ` are equivalent.  -/
LieModule.shiftedGenWeightSpace.shift : (R : Type u_2) →
  (L : Type u_3) →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    [inst_7 : LieRing.IsNilpotent L] →
                      (χ : L → R) → ↥(LieModule.genWeightSpace M χ) ≃ₗ[R] ↥(LieModule.shiftedGenWeightSpace R L M χ)
-- Mathlib.Order.Partition.Finpartition
Finpartition.equivSigmaParts.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s),
  P.equivSigmaParts =
    { toFun := fun x => ⟨⟨P.part ↑x, ⋯⟩, ⟨↑x, ⋯⟩⟩, invFun := fun x => ⟨↑x.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Descr.mk.injEq : ∀ {α β σ : Type} (name : autoParam Lean.Name Lean.ScopedEnvExtension.Descr.name._autoParam) (mkInitial : IO σ)
  (ofOLeanEntry : σ → α → Lean.ImportM β) (toOLeanEntry : β → α) (addEntry : σ → β → σ) (finalizeImport : σ → σ)
  (exportEntry? : Lean.Environment → α → Lean.OLeanEntries (Option α))
  (name_1 : autoParam Lean.Name Lean.ScopedEnvExtension.Descr.name._autoParam) (mkInitial_1 : IO σ)
  (ofOLeanEntry_1 : σ → α → Lean.ImportM β) (toOLeanEntry_1 : β → α) (addEntry_1 : σ → β → σ) (finalizeImport_1 : σ → σ)
  (exportEntry?_1 : Lean.Environment → α → Lean.OLeanEntries (Option α)),
  ({ name := name, mkInitial := mkInitial, ofOLeanEntry := ofOLeanEntry, toOLeanEntry := toOLeanEntry,
        addEntry := addEntry, finalizeImport := finalizeImport, exportEntry? := exportEntry? } =
      { name := name_1, mkInitial := mkInitial_1, ofOLeanEntry := ofOLeanEntry_1, toOLeanEntry := toOLeanEntry_1,
        addEntry := addEntry_1, finalizeImport := finalizeImport_1, exportEntry? := exportEntry?_1 }) =
    (name = name_1 ∧
      mkInitial = mkInitial_1 ∧
        ofOLeanEntry = ofOLeanEntry_1 ∧
          toOLeanEntry = toOLeanEntry_1 ∧
            addEntry = addEntry_1 ∧ finalizeImport = finalizeImport_1 ∧ exportEntry? = exportEntry?_1)
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable, then
for any intermediate field `S` of `K / F` such that `S / F` is algebraic, the `E(S) / E` and
`S / F` have the same separable degree.  -/
IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable' : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] (S : IntermediateField F K)
  [Algebra.IsAlgebraic F ↥S] [IsPurelyInseparable F E],
  Field.sepDegree E ↥(IntermediateField.adjoin E ↑S) = Field.sepDegree F ↥S
-- Init.Data.Array.Basic
Array.reverse.loop : {α : Type u} → (as : Array α) → ℕ → Fin as.size → Array α
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_eq_empty_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioc b a = ∅ ↔ ¬b < a
-- Mathlib.Data.Set.Card
Set.encard_coe_eq_coe_finsetCard : ∀ {α : Type u_1} (s : Finset α), (↑s).encard = ↑s.card
-- Init.GrindInstances.ToInt
Lean.Grind.instLEISizeSintNumBits : Lean.Grind.ToInt.LE ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
-- Mathlib.Data.TypeVec
TypeVec.prod_map_id : ∀ {n : ℕ} {α β : TypeVec.{u_1} n}, TypeVec.prod.map TypeVec.id TypeVec.id = TypeVec.id
-- Std.Http.Protocol.H1
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.BodyMode.chunked : Std.Http.Protocol.H1.Machine.BodyMode✝
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiff.sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : SubNegMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G]
  {E' : Type u_5} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6}
  [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H' M] {f : M → G} (c : G), ContMDiff I' I n f → ContMDiff I' I n fun x => f x - c
-- Mathlib.Topology.List
List.Vector.insertIdx.eq_1 : ∀ {α : Type u_1} {n : ℕ} (a : α) (i : Fin (n + 1)) (v : List.Vector α n),
  List.Vector.insertIdx a i v = ⟨(↑v).insertIdx (↑i) a, ⋯⟩
-- Mathlib.Algebra.QuadraticDiscriminant
/-- Root of a quadratic when its discriminant equals zero  -/
quadratic_eq_zero_iff_of_discrim_eq_zero : ∀ {K : Type u_1} [inst : Field K] [NeZero 2] {a b c : K},
  a ≠ 0 → discrim a b c = 0 → ∀ (x : K), a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a)
-- Mathlib.RingTheory.Nilpotent.Defs
nilpotencyClass.eq_1 : ∀ {R : Type u_1} (x : R) [inst : Zero R] [inst_1 : Pow R ℕ], nilpotencyClass x = sInf {k | x ^ k = 0}
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instSub.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Sub G] [inst_2 : ContinuousSub G],
  SeparationQuotient.instSub = { sub := Quotient.map₂ (fun x1 x2 => x1 - x2) ⋯ }
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwKey.mk.inj : ∀ {numGoals nameLength replacementSize : ℕ} {name : String} {replacement : Lean.Meta.AbstractMVarsResult}
  {numGoals_1 nameLength_1 replacementSize_1 : ℕ} {name_1 : String} {replacement_1 : Lean.Meta.AbstractMVarsResult},
  { numGoals := numGoals, nameLength := nameLength, replacementSize := replacementSize, name := name,
        replacement := replacement } =
      { numGoals := numGoals_1, nameLength := nameLength_1, replacementSize := replacementSize_1, name := name_1,
        replacement := replacement_1 } →
    numGoals = numGoals_1 ∧
      nameLength = nameLength_1 ∧ replacementSize = replacementSize_1 ∧ name = name_1 ∧ replacement = replacement_1
-- Init.Data.Iterators.Lemmas.Combinators.Attach
Std.Iter.count_attachWith : ∀ {α β : Type u_1} {P : β → Prop} [inst : Std.Iterator α Id β] {it : Std.Iter β}
  {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id], (it.attachWith P hP).length = it.length
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.superposeC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon)
  (p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.superpose_certC k₁ m₁ p₁ k₂ m₂ p₂ p c = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ = 0 →
      Lean.Grind.CommRing.Poly.denote ctx p₂ = 0 → Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Init.Data.String.Subslice
String.Slice.Subslice.endExclusive_extendLeft : ∀ {s : String.Slice} {sl : s.Subslice} {newStart : s.Pos} {h : newStart ≤ sl.startInclusive},
  (sl.extendLeft newStart h).endExclusive = sl.endExclusive
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH2_id : ∀ {k H : Type u} [inst : CommRing k] [inst_1 : Group H] {A : Rep.{u_1, u, u} k H},
  groupCohomology.mapShortComplexH2 (MonoidHom.id H) (CategoryTheory.CategoryStruct.id A) =
    CategoryTheory.CategoryStruct.id (groupCohomology.shortComplexH2 A)
-- Mathlib.Analysis.Complex.Poisson
_private.Mathlib.Analysis.Complex.Poisson.0.poissonKernel.eq_1 : ∀ (c w z : ℂ), poissonKernel c w z = (‖z - c‖ ^ 2 - ‖w - c‖ ^ 2) / ‖z - c - (w - c)‖ ^ 2
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- The Jordan decomposition of a signed measure is unique.  -/
MeasureTheory.JordanDecomposition.toSignedMeasure_injective : ∀ {α : Type u_1} [inst : MeasurableSpace α], Function.Injective MeasureTheory.JordanDecomposition.toSignedMeasure
-- Aesop.Index
Aesop.Index.byHyp : {α : Type} → Aesop.Index α → Lean.Meta.DiscrTree (Aesop.Rule α)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instInhabitedProof : Inhabited Mathlib.Tactic.ITauto.Proof
-- Lean.Elab.App
/-- Auxiliary method for propagating the expected type. We call it as soon as we find the first explicit
argument. The goal is to propagate the expected type in applications of functions such as
```lean
Add.add {α : Type u} : α → α → α
List.cons {α : Type u} : α → List α → List α
```
This is particularly useful when there applicable coercions. For example,
assume we have a coercion from `Nat` to `Int`, and we have
`(x : Nat)` and the expected type is `List Int`. Then, if we don't use this function,
the elaborator will fail to elaborate
```
List.cons x []
```
First, the elaborator creates a new metavariable `?α` for the implicit argument `{α : Type u}`.
Then, when it processes `x`, it assigns `?α := Nat`, and then obtains the
resultant type `List Nat` which is **not** definitionally equal to `List Int`.
We solve the problem by executing this method before we elaborate the first explicit argument (`x` in this example).
This method infers that the resultant type is `List ?α` and unifies it with `List Int`.
Then, when we elaborate `x`, the elaborate realizes the coercion from `Nat` to `Int` must be used, and the
term
```
@List.cons Int (coe x) (@List.nil Int)
```
is produced.

The method will do nothing if
1- The resultant type depends on the remaining arguments (i.e., `!eTypeBody.hasLooseBVars`).
2- The resultant type contains optional/auto params.

We have considered adding the following extra conditions
  a) The resultant type does not contain any type metavariable.
  b) The resultant type contains a non-type metavariable.

These two conditions would restrict the method to simple functions that are "morally" in
the Hindley&Milner fragment.
If users need to disable expected type propagation, we can add an attribute `[elab_without_expected_type]`.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.propagateExpectedType : Lean.Elab.Term.Arg → Lean.Elab.Term.ElabAppArgs.M Unit
-- Lean.Parser.Command
Lean.Parser.Command.assertNotImported.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Convex.Slope
/-- If `f` is concave on a set `s` in a linearly ordered field, and `f x < f y` for two points
`x < y` in `s`, then `f` is strictly monotone on `s ∩ (∞, x]`.  -/
ConcaveOn.strictMonoOn : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  ConcaveOn 𝕜 s f → ∀ {x y : 𝕜}, y ∈ s → x < y → f x < f y → StrictMonoOn f (s ∩ Set.Iic x)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.oreSub_add_oreSub : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {r₁ r₂ : R}
  {s₁ s₂ : ↥S},
  r₁ -ₒ s₁ + (r₂ -ₒ s₂) = AddOreLocalization.oreMin r₁ s₂ + r₂ -ₒ (AddOreLocalization.oreSubtra r₁ s₂ + s₁)
-- Mathlib.CategoryTheory.Limits.Final
/-- A variant of `final_of_colimit_comp_coyoneda_iso_pUnit` where we bind the various claims
about `colimit (F ⋙ coyoneda.obj (Opposite.op d))` for each `d : D` into a single claim about
the presheaf `colimit (F ⋙ yoneda)`.  -/
CategoryTheory.Functor.final_of_isTerminal_colimit_comp_yoneda : ∀ {C : Type v} [inst : CategoryTheory.Category.{v, v} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v, u₁} D]
  (F : CategoryTheory.Functor C D)
  (h : CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda))), F.Final
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.apply_ofVal : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (r : WithVal v), v r.ofVal = Valued.v r
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.IterM.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Data.ENNReal.Operations
ENNReal.image_coe_Ioo : ∀ (x y : NNReal), ENNReal.ofNNReal '' Set.Ioo x y = Set.Ioo ↑x ↑y
-- Mathlib.Logic.Equiv.Fin.Basic
finTwoArrowEquiv_apply : ∀ (α : Type u_1), ⇑(finTwoArrowEquiv α) = (piFinTwoEquiv fun x => α).toFun
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.instSetLike : {K : Type u_1} →
  {L : Type u_2} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → SetLike (IntermediateField K L) L
-- Lean.Meta.Tactic.NormCast
/-- The `norm_cast` attribute stores a simp set for each of the three types of `norm_cast` lemma.  -/
Lean.Meta.NormCast.NormCastExtension : Type
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.sub_iff_right : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M N : Matrix m m R} {b : m → α} [inst : LT α] [inst_1 : AddGroup R],
  M.BlockTriangular b → ((M - N).BlockTriangular b ↔ N.BlockTriangular b)
-- Mathlib.CategoryTheory.Subobject.Comma
/-- A subobject of the underlying object of a structured arrow can be lifted to a subobject of
the structured arrow, provided that there is a morphism making the subobject into a structured
arrow.  -/
CategoryTheory.StructuredArrow.liftSubobject : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {T : CategoryTheory.Functor C D} →
            {A : CategoryTheory.StructuredArrow S T} →
              (P : CategoryTheory.Subobject A.right) →
                {q : S ⟶ T.obj (CategoryTheory.Subobject.underlying.obj P)} →
                  CategoryTheory.CategoryStruct.comp q (T.map P.arrow) = A.hom → CategoryTheory.Subobject A
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.homologyMap'_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂),
  CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂ = γ.left.φH
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.Const.beq.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : BEq β]
  (m₁ m₂ : Std.DHashMap.Raw α fun x => β),
  Std.DHashMap.Raw.Const.beq m₁ m₂ =
    if h : 0 < m₁.buckets.size ∧ 0 < m₂.buckets.size then Std.DHashMap.Internal.Raw₀.Const.beq ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩
    else false
-- Mathlib.Algebra.Algebra.ZMod
/-- Any ring with a `ZMod p`-module structure can be upgraded to a `ZMod p`-algebra. Not an
instance because this is usually not the default way, and this will cause typeclass search loop.  -/
ZMod.algebraOfModule : (n : ℕ) → (R : Type u_2) → [inst : Ring R] → [Module (ZMod n) R] → Algebra (ZMod n) R
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_le_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, k ∈ t → (cmp t.minKey! k).isLE = true
-- Mathlib.Data.ENat.Basic
instCharZeroENat : CharZero ℕ∞
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k k' : α}, cmp k k' = Ordering.eq → t.get! k = t.get! k'
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map_map₂ : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {P₂ : Type u_7} [inst_7 : AddCommMonoid P₂] [inst_8 : Module R P₂] (f : P →ₗ[R] P₂)
  (g : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N),
  Submodule.map f (Submodule.map₂ g p q) = Submodule.map₂ (g.compr₂ f) p q
-- Lean.Elab.Tactic.Omega.Frontend
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.formatErrorMessage.varNames : Array Bool → Lean.MetaM (Array String)
-- Mathlib.Algebra.Field.Defs
DivisionSemiring.mk : {K : Type u_2} →
  [toSemiring : Semiring K] →
    [toInv : Inv K] →
      [toDiv : Div K] →
        [toZPow : ZPow K] →
          autoParam (∀ (a b : K), a / b = a * b⁻¹) DivInvMonoid.div_eq_mul_inv._autoParam →
            autoParam (∀ (a : K), a ^ 0 = 1) DivInvMonoid.zpow_zero'._autoParam →
              autoParam (∀ (n : ℕ) (a : K), a ^ ↑n.succ = a ^ ↑n * a) DivInvMonoid.zpow_succ'._autoParam →
                autoParam (∀ (n : ℕ) (a : K), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹) DivInvMonoid.zpow_neg'._autoParam →
                  [toNontrivial : Nontrivial K] →
                    0⁻¹ = 0 →
                      (∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) →
                        [toNNRatCast : NNRatCast K] →
                          autoParam (∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den) DivisionSemiring.nnratCast_def._autoParam →
                            (nnqsmul : ℚ≥0 → K → K) →
                              autoParam (∀ (q : ℚ≥0) (a : K), nnqsmul q a = ↑q * a)
                                  DivisionSemiring.nnqsmul_def._autoParam →
                                DivisionSemiring K
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Ideal.height_le_ringKrullDim_quotient_add_encard : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {p : Ideal R} [p.IsPrime],
  ∀ s ⊆ ↑p, ↑p.height ≤ ringKrullDim (R ⧸ Ideal.span s) + ↑s.encard
-- Lean.PrettyPrinter
Lean.PrettyPrinter.pp.exprSizes : Lean.Option Bool
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Functor.mapMatComp_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v₁, u_1} D] [inst_3 : CategoryTheory.Preadditive D] {E : Type u_2}
  [inst_4 : CategoryTheory.Category.{v₁, u_2} E] [inst_5 : CategoryTheory.Preadditive E]
  (F : CategoryTheory.Functor C D) [inst_6 : F.Additive] (G : CategoryTheory.Functor D E) [inst_7 : G.Additive]
  (X : CategoryTheory.Mat_ C), (F.mapMatComp G).hom.app X = CategoryTheory.CategoryStruct.id ((F.comp G).mapMat_.obj X)
-- Mathlib.Data.Multiset.UnionInter
Multiset.union_le_union_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ≤ t → ∀ (u : Multiset α), s ∪ u ≤ t ∪ u
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₂_obj_X_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (P : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ))
  (Δ : SimplexCategoryᵒᵖ), (AlgebraicTopology.DoldKan.Γ₂.obj P).X.obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ P.X Δ
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.algebraMap_leftInverse : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.LeftInverse ⇑TensorAlgebra.algebraMapInv ⇑(algebraMap R (TensorAlgebra R M))
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- The restriction of a reflexive bilinear form `B` onto a submodule `W` is
nondegenerate if `Disjoint W (B.orthogonal W)`.  -/
LinearMap.BilinForm.nondegenerate_restrict_of_disjoint_orthogonal : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  (B : LinearMap.BilinForm R₁ M₁),
  B.IsRefl → ∀ {W : Submodule R₁ M₁}, Disjoint W (B.orthogonal W) → (B.restrict W).Nondegenerate
-- Init.Grind.AC
Lean.Grind.AC.Seq.var.injEq : ∀ (x x_1 : Lean.Grind.AC.Var), (Lean.Grind.AC.Seq.var x = Lean.Grind.AC.Seq.var x_1) = (x = x_1)
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.mem.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_2 ()
-- Mathlib.Analysis.Convex.Star
/-- Alternative definition of star-convexity, in terms of pointwise set operations.  -/
starConvex_iff_pointwise_add_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {x : E} {s : Set E},
  StarConvex 𝕜 x s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • {x} + b • s ⊆ s
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainBialgHomEquiv.congr_simp : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G]
  [inst_3 : Group H], MonoidAlgebra.mapDomainBialgHomEquiv = MonoidAlgebra.mapDomainBialgHomEquiv
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_eq_univ_iff : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), sᶜ = Finset.univ ↔ s = ∅
-- Mathlib.Analysis.Normed.Module.Alternating.Curry
/-- Given a continuous alternating map `f` in `n+1` variables, split the first variable to obtain
a continuous linear map into continuous alternating maps in `n` variables,
given by `x ↦ (m ↦ f (Matrix.vecCons x m))`.
It can be thought of as a map $Hom(\bigwedge^{n+1} M, N) \to Hom(M, Hom(\bigwedge^n M, N))$.

This is `ContinuousMultilinearMap.curryLeft` for `AlternatingMap`. See also
`ContinuousAlternatingMap.curryLeftLI`.  -/
ContinuousAlternatingMap.curryLeft : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → {n : ℕ} → E [⋀^Fin (n + 1)]→L[𝕜] F → E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
_private.Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation.0.MeasureTheory.VectorMeasure.exists_one_le_enorm_apply_of_semivariation_eq_top : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  {μ : MeasureTheory.VectorMeasure X E} {s : Set X},
  MeasurableSet s → μ.semivariation s = ⊤ → ∃ t, MeasurableSet t ∧ t ⊆ s ∧ μ.semivariation t = ⊤ ∧ 1 ≤ ‖μ (s \ t)‖ₑ
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.instMulNorm.eq_1 : ∀ {E : Type u_2} [inst : SeminormedCommGroup E],
  SeparationQuotient.instMulNorm = { norm := SeparationQuotient.lift norm ⋯ }
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Code.size.go : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → ℕ → ℕ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go_denote_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (assign : α → Bool) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ)
  (hidx1 : idx < w),
  curr ≤ idx →
    ⟦assign,
        { aig := aig,
          ref :=
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go input distance curr hcurr s).get idx
              hidx1 }⟧ =
      if hidx : distance + idx < w then ⟦assign, { aig := aig, ref := input.get (distance + idx) hidx }⟧
      else ⟦assign, { aig := aig, ref := input.get (w - 1) ⋯ }⟧
-- Mathlib.Data.Stream.Init
Stream'.take_theorem : ∀ {α : Type u} (s₁ s₂ : Stream' α), (∀ (n : ℕ), Stream'.take n s₁ = Stream'.take n s₂) → s₁ = s₂
-- Mathlib.Order.RelIso.Basic
RelEmbedding.instInhabited : {α : Type u_1} → (r : α → α → Prop) → Inhabited (r ↪r r)