mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
SheafOfModules.pullback_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {D' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D'] {D'' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D''] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat}
  {R : CategoryTheory.Sheaf K RingCat} [inst_4 : F.IsContinuous J K]
  (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) [inst_5 : (SheafOfModules.pushforward φ).IsRightAdjoint]
  {K' : CategoryTheory.GrothendieckTopology D'} {K'' : CategoryTheory.GrothendieckTopology D''}
  {G : CategoryTheory.Functor D D'} {R' : CategoryTheory.Sheaf K' RingCat} [inst_6 : G.IsContinuous K K']
  [inst_7 : (F.comp G).IsContinuous J K'] (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R')
  [inst_8 : (SheafOfModules.pushforward ψ).IsRightAdjoint] {G' : CategoryTheory.Functor D' D''}
  {R'' : CategoryTheory.Sheaf K'' RingCat} [inst_9 : G'.IsContinuous K' K''] [inst_10 : (G.comp G').IsContinuous K K'']
  [inst_11 : ((F.comp G).comp G').IsContinuous J K''] [inst_12 : (F.comp (G.comp G')).IsContinuous J K'']
  (ψ' : R' ⟶ (G'.sheafPushforwardContinuous RingCat K' K'').obj R'')
  [inst_13 : (SheafOfModules.pushforward ψ').IsRightAdjoint],
  (SheafOfModules.pullback φ).isoWhiskerLeft (SheafOfModules.pullbackComp ψ ψ') ≪≫
      SheafOfModules.pullbackComp φ
        (CategoryTheory.CategoryStruct.comp ψ ((G.sheafPushforwardContinuous RingCat K K').map ψ')) =
    ((SheafOfModules.pullback φ).associator (SheafOfModules.pullback ψ) (SheafOfModules.pullback ψ')).symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight (SheafOfModules.pullbackComp φ ψ) (SheafOfModules.pullback ψ') ≪≫
        SheafOfModules.pullbackComp
          (CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ)) ψ'
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
/-- A cyclic group is always commutative. This is not an `instance` because often we have a better
proof of `CommGroup`.  -/
IsCyclic.commGroup : {α : Type u_1} → [inst : Group α] → [IsCyclic α] → CommGroup α
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If a function `f` tends to infinity along a filter, then `f` multiplied by a positive
constant (on the right) also tends to infinity. For a version working in `ℕ` or `ℤ`, use
`Filter.Tendsto.atTop_mul_const'` instead.  -/
Filter.Tendsto.atTop_mul_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, 0 < r → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x * r) l Filter.atTop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- A pair of morphisms `h : W ⟶ X` and `k : W ⟶ Y` satisfying `h ≫ f = k ≫ g` induces a morphism
`pullback.lift : W ⟶ pullback f g`.  -/
CategoryTheory.Limits.pullback.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          [inst_1 : CategoryTheory.Limits.HasPullback f g] →
            (h : W ⟶ X) →
              (k : W ⟶ Y) →
                autoParam (CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
                    CategoryTheory.Limits.pullback.lift._auto_1 →
                  (W ⟶ CategoryTheory.Limits.pullback f g)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_isIso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h)
  [CategoryTheory.IsIso η], CategoryTheory.IsIso (CategoryTheory.Bicategory.whiskerLeft f η)
-- Mathlib.FieldTheory.PrimitiveElement
/-- Alternative phrasing of primitive element theorem:
a finite separable field extension has a basis `1, α, α^2, ..., α^n`.

See also `exists_primitive_element`.  -/
Field.powerBasisOfFiniteOfSeparable : (F : Type u_1) →
  (E : Type u_2) →
    [inst : Field F] →
      [inst_1 : Field E] → [inst_2 : Algebra F E] → [FiniteDimensional F E] → [Algebra.IsSeparable F E] → PowerBasis F E
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.mk : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} (d : CategoryTheory.Limits.LimitCone F), CategoryTheory.Limits.HasLimit F
-- Mathlib.Topology.Order.LocalExtr
Filter.EventuallyEq.isLocalMinOn_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {s : Set α} {f g : α → β} {a : α},
  f =ᶠ[nhdsWithin a s] g → a ∈ s → (IsLocalMinOn f s a ↔ IsLocalMinOn g s a)
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.subst_into_smulg : ∀ {α : Type u_1} [inst : AddCommGroup α] (l : ℤ) (r : α) (tl : ℤ) (tr t : α),
  l = tl → r = tr → Mathlib.Tactic.Abel.smulg tl tr = t → Mathlib.Tactic.Abel.smulg l r = t
-- Mathlib.Topology.Sets.Closeds
/-- The equivalence between `IrreducibleCloseds α` and `{x : Set α // IsIrreducible x ∧ IsClosed x }`.
 -/
TopologicalSpace.IrreducibleCloseds.equivSubtype : {α : Type u_2} →
  [inst : TopologicalSpace α] → TopologicalSpace.IrreducibleCloseds α ≃ { x // IsIrreducible x ∧ IsClosed x }
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.subterminalInclusion_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C]
  (self : CategoryTheory.ObjectProperty.FullSubcategory fun A => CategoryTheory.IsSubterminal A),
  (CategoryTheory.subterminalInclusion C).obj self = self.obj
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_2.go : {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
  {motive_2 :
      Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
        Sort u} →
    {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
      {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
        {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
          {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
            {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
              {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
                (t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                  ((t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t) →
                    ((t :
                          Lean.Language.TransformedSnap
                            (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
                        Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t) →
                      ((t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                          Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t) →
                        ((t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
                            Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t) →
                          ((t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                              Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t) →
                            ((t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                                Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t) →
                              ((t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
                                  Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t) →
                                ((t : Task Lean.Elab.Tactic.TacticParsedSnapshot) →
                                    Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t) →
                                  motive_3 t ×' Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t
-- Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
/-- The complement of the irreducible components unequal to `Z` of a Noetherian scheme.  -/
AlgebraicGeometry.Scheme.irreducibleComponentOpen : (X : AlgebraicGeometry.Scheme) → Set ↥X → [AlgebraicGeometry.IsNoetherian X] → X.Opens
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Category.{v, max u v} (CategoryTheory.RingObjCat C)
-- Mathlib.Algebra.Ring.Parity
Odd.of_isUnit_two : ∀ {α : Type u_2} [inst : Ring α], IsUnit 2 → ∀ (a : α), Odd a
-- Lean.Util.Diff
_private.Lean.Util.Diff.0.Lean.Diff.matchSuffix.go.eq_def : ∀ {α : Type u_1} [inst : BEq α] (left right : Subarray α) (i : ℕ),
  Lean.Diff.matchSuffix.go✝ left right i =
    if x : i < Std.Slice.size left ∧ i < Std.Slice.size right then
      if (left[Std.Slice.size left - i - 1] == right[Std.Slice.size right - i - 1]) = true then
        Lean.Diff.matchSuffix.go✝ left right i.succ
      else
        (left.take (Std.Slice.size left - i), right.take (Std.Slice.size right - i),
          Std.Slice.toArray (left.drop (Std.Slice.size left - i)))
    else
      (left.take (Std.Slice.size left - i), right.take (Std.Slice.size right - i),
        Std.Slice.toArray (left.drop (Std.Slice.size left - i)))
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} [MeasureTheory.SFinite μ]
  (s : Set Ω),
  (μ.tilted fun x => t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, Real.exp (t * X a) / ProbabilityTheory.mgf X μ t ∂μ)
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_def : ∀ {α : Type u_2} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
  InformationTheory.klDiv μ ν =
    if μ.AbsolutelyContinuous ν ∧ MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ then
      ENNReal.ofReal (∫ (x : α), MeasureTheory.llr μ ν x ∂μ + ν.real Set.univ - μ.real Set.univ)
    else ⊤
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp},
  Array.map Sigma.fst t.toArray = t.keysArray
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.of_forall_constGet?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], (∀ (k : α), Std.DTreeMap.Const.get? t₁ k = Std.DTreeMap.Const.get? t₂ k) → t₁.Equiv t₂
-- Mathlib.Algebra.Algebra.StrictPositivity
IsUnit.isStrictlyPositive : ∀ {A : Type u_1} [inst : LE A] [inst_1 : Monoid A] [inst_2 : Zero A] {a : A}, IsUnit a → 0 ≤ a → IsStrictlyPositive a
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.sub_mem : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M)
  {x y : M}, x ∈ p → y ∈ p → x - y ∈ p
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings
SheafOfModules.instAdditiveRestrictScalars : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R R' : CategoryTheory.Sheaf J RingCat} (α : R ⟶ R'), (SheafOfModules.restrictScalars α).Additive
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.cons_nonzero_iff : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] {v : Fin n → α} {x : α}, Matrix.vecCons x v ≠ 0 ↔ x ≠ 0 ∨ v ≠ 0
-- Mathlib.CategoryTheory.Filtered.Basic
/-- for every pair of parallel morphisms there exists a morphism to the left
so the compositions are equal  -/
CategoryTheory.IsCofilteredOrEmpty.cone_maps : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsCofilteredOrEmpty C] ⦃X Y : C⦄
  (f g : X ⟶ Y), ∃ W h, CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g
-- Mathlib.Tactic.NormNum.Irrational
_private.Mathlib.Tactic.NormNum.Irrational.0.Mathlib.Meta.NormNum.not_power_nat_pow : ∀ {n p q : ℕ}, p.Coprime q → 0 < q → (∀ (m : ℕ), n ≠ m ^ q) → ∀ (m : ℕ), n ^ p ≠ m ^ q
-- Lean.Elab.Match
/-- Normalize the pattern and collect all patterns variables (explicit and implicit).
This method is the one that decides where the inaccessible annotations must be inserted.
The pattern variables are both free variables (for explicit pattern variables) and metavariables (for implicit ones).
Recall that `mkLambdaFVars` now allows us to abstract both free variables and metavariables.
 -/
Lean.Elab.Term.ToDepElimPattern.normalize : Lean.Expr → Lean.Elab.Term.ToDepElimPattern.M Lean.Expr
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.IsNormal.bsup_eq : ∀ {f : Ordinal.{u} → Ordinal.{max u v}},
  Order.IsNormal f → ∀ {o : Ordinal.{u}}, Order.IsSuccLimit o → (o.bsup fun x x_1 => f x) = f o
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_roo_eq_some_iff : ∀ {k m n i : ℕ}, (m<...n).toArray[i]? = some k ↔ i < n - (m + 1) ∧ m + 1 + i = k
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlock.eq_1 : ∀ (G : Type u_1) {X : Type u_2} [inst : VAdd G X] (B : Set X),
  AddAction.IsBlock G B = ∀ ⦃g₁ g₂ : G⦄, g₁ +ᵥ B ≠ g₂ +ᵥ B → Disjoint (g₁ +ᵥ B) (g₂ +ᵥ B)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
/-- The composition of a matrix (as an endomorphism of `ι → R`) with the projection
`(ι → R) →ₗ[R] M`.  -/
PiToModule.fromMatrix : {ι : Type u_1} →
  [Fintype ι] →
    {M : Type u_2} →
      [inst : AddCommGroup M] →
        (R : Type u_3) →
          [inst_1 : CommRing R] → [inst_2 : Module R M] → (ι → M) → [DecidableEq ι] → Matrix ι ι R →ₗ[R] (ι → R) →ₗ[R] M
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.of_finite : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [Finite α] [MeasureTheory.IsFiniteMeasure μ] {f : α → β}, MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` is an intermediate field of `E / F`, and `E / L / F` is a field extension tower,
then `A` and `L` are linearly disjoint, if they are linearly disjoint as subalgebras of `E`
(`Subalgebra.LinearDisjoint`).  -/
IntermediateField.LinearDisjoint : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          IntermediateField F E →
            (L : Type w) →
              [inst_3 : Field L] → [inst_4 : Algebra F L] → [inst_5 : Algebra L E] → [IsScalarTower F L E] → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.PreservesColimitsOfSize.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  autoParam
      (∀ {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J], CategoryTheory.Limits.PreservesColimitsOfShape J F)
      CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape._autoParam →
    CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
-- Init.Data.String.Basic
String.ext : ∀ {s₁ s₂ : String}, s₁.toList = s₂.toList → s₁ = s₂
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.epi_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {A : C},
  CategoryTheory.Epi (CategoryTheory.NonPreadditiveAbelian.r A)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k k' : α}, t.getKey? k = some k' → (Std.TreeMap.map f t)[k]? = Option.map (f k') t[k]?
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The map `Cocycle (K⟦a⟧) L n' → Cocycle K L n` when `n + a = n'`.  -/
CochainComplex.HomComplex.Cocycle.leftUnshift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n' a : ℤ} →
          CochainComplex.HomComplex.Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n' →
            (n : ℤ) → n + a = n' → CochainComplex.HomComplex.Cocycle K L n
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_app : ∀ {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} {G G' : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : C),
  CategoryTheory.CategoryStruct.comp (adj1.unit.app x) ((adj1.rightAdjointUniq adj2).hom.app (F.obj x)) =
    adj2.unit.app x
-- Mathlib.MeasureTheory.Measure.Real
/-- If `s` is a `Finset`, then the measure of its preimage can be found as the sum of measures
of the fibers `f ⁻¹' {y}`.  -/
MeasureTheory.sum_measureReal_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Finset β) {f : α → β},
  (∀ y ∈ s, MeasurableSet (f ⁻¹' {y})) →
    autoParam (∀ a ∈ s, μ (f ⁻¹' {a}) ≠ ⊤) MeasureTheory.sum_measureReal_preimage_singleton._auto_1 →
      ∑ b ∈ s, μ.real (f ⁻¹' {b}) = μ.real (f ⁻¹' ↑s)
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.instProductive : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  [inst_2 : Monad m] [Std.Iterators.Productive α₁ m] [Std.Iterators.Productive α₂ m],
  Std.Iterators.Productive (Std.Iterators.Types.Zip α₁ m α₂ β₂) m
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.get_eq_of_skipSuffixWhile_le_char : ∀ {c : Char} {s : String.Slice} {pos : s.Pos}, s.skipSuffixWhile c ≤ pos → ∀ (h' : pos < s.endPos), pos.get ⋯ = c
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
Finset.le_prod_of_submultiplicative_of_nonneg : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {M : Type u_4}
  [inst_3 : CommMonoid M] (f : M → R),
  (∀ (a : M), 0 ≤ f a) →
    f 1 ≤ 1 → (∀ (x y : M), f (x * y) ≤ f x * f y) → ∀ (s : Finset ι) (g : ι → M), f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
-- Init.Data.SInt.Basic
instInhabitedInt16 : Inhabited Int16
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Lean.Data.Lsp.Basic
Lean.Lsp.RenameFile.mk.injEq : ∀ (oldUri newUri : Lean.Lsp.DocumentUri) (options? : Option Lean.Lsp.CreateFile.Options) (annotationId? : Option String)
  (oldUri_1 newUri_1 : Lean.Lsp.DocumentUri) (options?_1 : Option Lean.Lsp.CreateFile.Options)
  (annotationId?_1 : Option String),
  ({ oldUri := oldUri, newUri := newUri, options? := options?, annotationId? := annotationId? } =
      { oldUri := oldUri_1, newUri := newUri_1, options? := options?_1, annotationId? := annotationId?_1 }) =
    (oldUri = oldUri_1 ∧ newUri = newUri_1 ∧ options? = options?_1 ∧ annotationId? = annotationId?_1)
-- Mathlib.Data.Nat.Prime.Defs
Nat.instDecidableEqPrimes : DecidableEq Nat.Primes
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.fold_cons : ∀ {α : Type u} {β : α → Type v} {l : Std.DHashMap.Raw α β} {acc : List ((a : α) × β a)},
  Std.DHashMap.Raw.fold (fun acc k v => ⟨k, v⟩ :: acc) acc l =
    (Std.DHashMap.Internal.toListModel l.buckets).reverse ++ acc
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.eventually_mul_right_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G)
  [μ.IsMulRightInvariant] (t : G) {p : G → Prop}, (∀ᵐ (x : G) ∂μ, p (x * t)) ↔ ∀ᵐ (x : G) ∂μ, p x
-- Mathlib.Algebra.Lie.Basic
instSubsingletonLieAlgebraRat : ∀ (L : Type u_1) [inst : LieRing L], Subsingleton (LieAlgebra ℚ L)
-- Mathlib.Analysis.Distribution.DerivNotation
LineDerivSMul.lineDerivOp_smul : ∀ {R : Type u_11} {V : Type u} {E : Type v} {F : outParam (Type w)} {inst : SMul R E} {inst_1 : SMul R F}
  {inst_2 : LineDeriv V E F} [self : LineDerivSMul R V E F] (v : V) (r : R) (x : E),
  LineDeriv.lineDerivOp v (r • x) = r • LineDeriv.lineDerivOp v x
-- Mathlib.GroupTheory.DivisibleHull
_private.Mathlib.GroupTheory.DivisibleHull.0.DivisibleHull.archimedeanClassOrderHom.eq_1 : ∀ (M : Type u_2) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  DivisibleHull.archimedeanClassOrderHom✝ M = ArchimedeanClass.orderHom (DivisibleHull.coeOrderAddMonoidHom M)
-- Lean.DocString.Types
Lean.Doc.instOrdBlock.ord : {i : Type u_1} → {b : Type u_2} → [Ord i] → [Ord b] → Lean.Doc.Block i b → Lean.Doc.Block i b → Ordering
-- Init.Data.BitVec.Lemmas
BitVec.instCommutativeHXor : ∀ {w : ℕ}, Std.Commutative fun x y => x ^^^ y
-- Std.Data.TreeMap.Basic
Std.TreeMap.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} {cmp : autoParam (α → α → Ordering) Std.TreeMap._auto_1} [inst : SizeOf α]
  [inst_1 : SizeOf β] (inner : Std.DTreeMap α (fun x => β) cmp), sizeOf { inner := inner } = 1 + sizeOf inner
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.containsThenInsert.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a),
  m.containsThenInsert a b =
    if h : 0 < m.buckets.size then
      match Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨m, h⟩ a b with
      | (replaced, ⟨r, property⟩) => (replaced, r)
    else (false, m)
-- Mathlib.Algebra.Ring.Defs
/-- A `NonUnitalNonAssocRing` which `IsMulCommutative` is a `NonUnitalNonAssocCommRing`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsMulCommutative.instNonUnitalNonAssocCommRing : {R : Type v} → [inst : NonUnitalNonAssocRing R] → [IsMulCommutative R] → NonUnitalNonAssocCommRing R
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.tfaeHavePatDecl.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectR_map : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] (b : B) (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {X Y : C} (a : X ⟶ Y),
  (CategoryTheory.Bicategory.Prod.sectR b C).map a = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id b) a
-- Mathlib.Order.Closure
LowerAdjoint.le_iff_subset : ∀ {α : Type u_1} {β : Type u_4} [inst : SetLike α β] [inst_1 : Preorder α] (l : LowerAdjoint SetLike.coe) (s : Set β)
  (S : α), l.toFun s ≤ S ↔ s ⊆ ↑S
-- Mathlib.Data.Nat.BitIndices
Nat.bitIndices_sorted : ∀ {n : ℕ}, n.bitIndices.SortedLT
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instNonUnitalSemiringOfAddOpposite : {M : Type u_1} → [NonUnitalSemiring Mᵃᵒᵖ] → NonUnitalSemiring Mᵈᵃᵃ
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.algebraMap_rootLength : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) [inst_9 : FaithfulSMul S R] [inst_10 : Module S M]
  [inst_11 : IsScalarTower S R M] (i : ι), (algebraMap S R) (B.rootLength i) = (B.form (P.root i)) (P.root i)