mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.getThenInsertIfNew?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] (m : Std.DHashMap.Raw α β)
  (a : α) (b : β a),
  m.getThenInsertIfNew? a b =
    if h : 0 < m.buckets.size then
      match Std.DHashMap.Internal.Raw₀.getThenInsertIfNew? ⟨m, h⟩ a b with
      | (previous, ⟨r, property⟩) => (previous, r)
    else (none, m)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintKind.parameter.sizeOf_spec : sizeOf Lean.Lsp.InlayHintKind.parameter = 1
-- Mathlib.RingTheory.PicardGroup
instInvertibleCarrierOutSemimoduleCatValSkeleton : ∀ (R : Type u) [inst : CommSemiring R] (M : (CategoryTheory.Skeleton (SemimoduleCat R))ˣ),
  Module.Invertible R ↑(Quotient.out ↑M)
-- Mathlib.Algebra.Order.SuccPred.TypeTags
Order.pred_toAdd : ∀ {X : Type u_1} [inst : Preorder X] [inst_1 : PredOrder X] (x : Multiplicative X),
  Order.pred (Multiplicative.toAdd x) = Multiplicative.toAdd (Order.pred x)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.inj_left : ∀ {α : Type u_1} [inst : Add α] [IsAddCommutative α] [inst_2 : PartialOrder α] {a b c : α},
  AddLECancellable c → (a + c = b + c ↔ a = b)
-- Mathlib.Combinatorics.Compactness
/-- Given a (dependent) function `g s : (a : α) → β a` for each finite set `s` of `α`, provided that
each `β a` is finite, we can find another function `χ : (a : α) → β a` such that on every `s`,
there is some larger `t` such that `χ` agrees with `g t` on `s`.
Informally, we are stitching together the local functions `g s` into a global `χ` such that on
each `s`, `χ` can be expressed in terms of one of the `g`.
 -/
Set.Finite.rado_selection : ∀ {α : Type u_1} {β : α → Type u_2} [∀ (a : α), Finite (β a)] (g : (s : Set α) → s.Finite → (a : α) → β a),
  ∃ χ, ∀ (s : Set α), s.Finite → ∃ t, ∃ (ht : t.Finite), s ⊆ t ∧ ∀ x ∈ s, χ x = g t ht x
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.normalizeIsoApp'.match_1.eq_2 : ∀ (C : Type u_1)
  (motive :
    CategoryTheory.FreeMonoidalCategory C → CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C → Sort u_2)
  (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C)
  (h_1 :
    (a : C) →
      (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
        motive (CategoryTheory.FreeMonoidalCategory.of a) x)
  (h_2 :
    (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
      motive CategoryTheory.FreeMonoidalCategory.unit x)
  (h_3 :
    (X Y : CategoryTheory.FreeMonoidalCategory C) →
      (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) → motive (X.tensor Y) n),
  (match CategoryTheory.FreeMonoidalCategory.unit, x with
    | CategoryTheory.FreeMonoidalCategory.of a, x => h_1 a x
    | CategoryTheory.FreeMonoidalCategory.unit, x => h_2 x
    | X.tensor Y, n => h_3 X Y n) =
    h_2 x
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pushout.inl_codiagonal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f f)
      (CategoryTheory.Limits.pushout.codiagonal f) =
    CategoryTheory.CategoryStruct.id Y
-- Mathlib.CategoryTheory.MorphismProperty.IsSmall
CategoryTheory.MorphismProperty.instIsSmallISupOfSmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} [Small.{w, t} α]
  (W : α → CategoryTheory.MorphismProperty C) [∀ (i : α), CategoryTheory.MorphismProperty.IsSmall.{w, v, u} (W i)],
  CategoryTheory.MorphismProperty.IsSmall.{w, v, u} (⨆ i, W i)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Pairwise intersection of two pre-`0`-hypercovers.  -/
CategoryTheory.PreZeroHypercover.inter : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {T : C} →
      (E : CategoryTheory.PreZeroHypercover T) →
        (F : CategoryTheory.PreZeroHypercover T) →
          [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] →
            CategoryTheory.PreZeroHypercover T
-- Mathlib.LinearAlgebra.LinearDisjoint
Submodule.linearDisjoint_iff : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S),
  M.LinearDisjoint N ↔ Function.Injective ⇑(M.mulMap N)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- ε-characterization of the closure in pseudometric spaces  -/
Metric.mem_closure_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {a : α}, a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.ext : ∀ {R : Type u_1} {a b c : R} {x y : QuaternionAlgebra R a b c},
  x.re = y.re → x.imI = y.imI → x.imJ = y.imJ → x.imK = y.imK → x = y
-- Batteries.Recycling.MonadSatisfying.Array
_private.Batteries.Recycling.MonadSatisfying.Array.0.Array.forIn'.loop.match_3.splitter : {α : Type u_1} →
  (as : Array α) →
    (motive : (i : ℕ) → i ≤ as.size → Sort u_2) →
      (i : ℕ) →
        (h : i ≤ as.size) →
          ((x : 0 ≤ as.size) → motive 0 x) → ((i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h) → motive i h
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_id_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct W Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct W Z],
  CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) f)
      (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id W) g)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.open_target : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (self : OpenPartialHomeomorph X Y), IsOpen self.target
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousAlternatingMap.alternatizeUncurryFin.eq_1 : ∀ {𝕜 : 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 : ℕ}
  (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F),
  ContinuousAlternatingMap.alternatizeUncurryFin f = (ContinuousAlternatingMap.alternatizeUncurryFinCLM 𝕜 E F) f
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileSystemWatcher : Type
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.symm_mapRingEquiv : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (e : R ≃+* S), (MonoidAlgebra.mapRingEquiv M e).symm = MonoidAlgebra.mapRingEquiv M e.symm
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- Any invertible linear map rescales Lebesgue measure through the absolute value of its
determinant.  -/
Real.map_linearMap_volume_pi_eq_smul_volume_pi : ∀ {ι : Type u_1} [inst : Fintype ι] {f : (ι → ℝ) →ₗ[ℝ] ι → ℝ},
  LinearMap.det f ≠ 0 →
    MeasureTheory.Measure.map (⇑f) MeasureTheory.volume = ENNReal.ofReal |(LinearMap.det f)⁻¹| • MeasureTheory.volume
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_one_sub_smoothingFn_r_pos : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r),
  ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < 1 - AkraBazziRecurrence.smoothingFn ↑(r i n)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivAt.div : ∀ {𝕜 : 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] {z : M} {F' : Type u_21} [inst_6 : NormedField F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'} {p' q' : TangentSpace I z →L[𝕜] F'},
  HasMFDerivAt% p z p' →
    HasMFDerivAt% q z q' → q z ≠ 0 → HasMFDerivAt% (p / q) z ((1 / q z) • p' - (p z / q z ^ 2) • q')
-- Mathlib.Data.Seq.Basic
Stream'.Seq.getElem?_take : ∀ {α : Type u} (n k : ℕ) (s : Stream'.Seq α), (Stream'.Seq.take k s)[n]? = if n < k then s.get? n else none
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l →
    (∀ a ∈ m, l.contains a = false) → (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).size = m.size + l.length
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousAlternatingMap.alternatizeUncurryFin_smul : ∀ {𝕜 : 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 : ℕ} {S : Type u_5}
  [inst_5 : Monoid S] [inst_6 : DistribMulAction S F] [inst_7 : ContinuousConstSMul S F] [inst_8 : SMulCommClass 𝕜 S F]
  (c : S) (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F),
  ContinuousAlternatingMap.alternatizeUncurryFin (c • f) = c • ContinuousAlternatingMap.alternatizeUncurryFin f
-- Mathlib.Algebra.Group.Translate
translate_apply : ∀ {α : Type u_2} {G : Type u_5} [inst : AddCommGroup G] (a : G) (f : G → α) (x : G), translate a f x = f (x - a)
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.IterM.step_intermediateZip.match_1.eq_2 : ∀ {α₁ β₁ : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β₁] {it₁ : Std.IterM m β₁}
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β₁) (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁'))
  (h_1 :
    (it₁' : Std.IterM m β₁) →
      (out : β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, hp⟩)
  (h_2 :
    (it₁' : Std.IterM m β₁) → (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩)
  (h_3 : (hp : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩),
  (match ⟨Std.IterStep.skip it₁', hp⟩ with
    | ⟨Std.IterStep.yield it₁' out, hp⟩ => h_1 it₁' out hp
    | ⟨Std.IterStep.skip it₁', hp⟩ => h_2 it₁' hp
    | ⟨Std.IterStep.done, hp⟩ => h_3 hp) =
    h_2 it₁' hp
-- Mathlib.Algebra.GroupWithZero.ProdHom
/-- The trivial group-with-zero hom is absorbing for composition.  -/
MonoidWithZeroHom.one_comp : ∀ {M₀ : Type u_1} {N₀ : Type u_2} {G₀ : Type u_3} [inst : GroupWithZero M₀] [inst_1 : MulZeroOneClass N₀]
  [inst_2 : Nontrivial N₀] [inst_3 : NoZeroDivisors N₀] [inst_4 : MulZeroOneClass G₀]
  [inst_5 : DecidablePred fun x => x = 0] [inst_6 : DecidablePred fun x => x = 0] (f : M₀ →*₀ N₀),
  MonoidWithZeroHom.comp 1 f = 1
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObj.toIsCommMonObj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {R : C} [self : CategoryTheory.CommRingObj R],
  CategoryTheory.IsCommMonObj R
-- Init.Data.SInt.Lemmas
Int16.toISize_ofNat' : ∀ {n : ℕ}, ↑n ≤ Int16.maxValue.toInt → (Int16.ofNat n).toISize = ISize.ofNat n
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] (s t : Finset α), ↑(s + t) = ↑s + ↑t
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.toList_flattenAfter : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m (Std.IterM m β)] [inst_5 : Std.Iterator α₂ m β]
  [Std.Iterators.Finite α m] [Std.Iterators.Finite α₂ m] {it₁ : Std.IterM m (Std.IterM m β)}
  {it₂ : Option (Std.IterM m β)},
  (Std.IterM.flattenAfter✝ it₁ it₂).toList =
    match it₂ with
    | none => List.flatten <$> (Std.IterM.mapM (fun it₂ => it₂.toList) it₁).toList
    | some it₂ => do
      let __do_lift ← it₂.toList
      let __do_lift_1 ← List.flatten <$> (Std.IterM.mapM (fun it₂ => it₂.toList) it₁).toList
      pure (__do_lift ++ __do_lift_1)
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- We now prove that `Mat_ C` has finite biproducts.

Be warned, however, that `Mat_ C` is not necessarily Krull-Schmidt,
and so the internal indexing of a biproduct may have nothing to do with the external indexing,
even though the construction we give uses a sigma type.
See however `isoBiproductEmbedding`.
 -/
CategoryTheory.Mat_.hasFiniteBiproducts : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Mat_ C)
-- Mathlib.Order.InitialSeg
InitialSeg.mk.inj : ∀ {α : Type u_4} {β : Type u_5} {r : α → α → Prop} {s : β → β → Prop} {toRelEmbedding : r ↪r s}
  {mem_range_of_rel' : ∀ (a : α) (b : β), s b (toRelEmbedding a) → b ∈ Set.range ⇑toRelEmbedding}
  {toRelEmbedding_1 : r ↪r s}
  {mem_range_of_rel'_1 : ∀ (a : α) (b : β), s b (toRelEmbedding_1 a) → b ∈ Set.range ⇑toRelEmbedding_1},
  { toRelEmbedding := toRelEmbedding, mem_range_of_rel' := mem_range_of_rel' } =
      { toRelEmbedding := toRelEmbedding_1, mem_range_of_rel' := mem_range_of_rel'_1 } →
    toRelEmbedding = toRelEmbedding_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_alter_eq_sub_one : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  k ∈ t → (f (t.get? k)).isNone = true → (t.alter k f).size = t.size - 1
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Fanin.invert_mk : ∀ {g : ℕ} {i : Bool}, (Std.Sat.AIG.Fanin.mk g i).invert = i
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
normEDS_neg : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (n : ℤ), normEDS b c d (-n) = -normEDS b c d n
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.measureReal_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb →
    ∀ {s : Set β}, MeasureTheory.NullMeasurableSet s μb → μa.real (f ⁻¹' s) = μb.real s
-- Init.Data.Int.Basic
Int.instSub : Sub ℤ
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valued.toNormedField.one_le_norm_iff : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne] {x : L}, 1 ≤ ‖x‖ ↔ 1 ≤ Valued.v x
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.ofReal_log : ∀ {x : ℝ}, 0 ≤ x → ↑(Real.log x) = Complex.log ↑x
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ Dᵒᵖ` creates finite products, then `F.leftOp : Cᵒᵖ ⥤ D` creates finite
coproducts.  -/
CategoryTheory.Limits.createsFiniteCoproductsLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C Dᵒᵖ) →
          [CategoryTheory.Limits.CreatesFiniteProducts F] → CategoryTheory.Limits.CreatesFiniteCoproducts F.leftOp
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- A continuous function on a compact space is automatically a continuous function vanishing at
infinity.  -/
ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Zero β] → [CompactSpace α] → C(α, β) ≃ ZeroAtInftyContinuousMap α β
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.instCoeFun : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : Semiring R] → CoeFun (GL n R) fun x => n → n → R
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroup_eq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  (MonoidWithZeroHom.ofClass (IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation K v)).valueGroup =
    (MonoidWithZeroHom.ofClass Valued.v).valueGroup
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. The rank, or the number of trees in the forest.
It is also the depth of the forest.
 -/
Batteries.BinomialHeap.Imp.HeapNode.rank : {α : Type u_1} → Batteries.BinomialHeap.Imp.HeapNode α → ℕ
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instHasFramePureAndOfAnd : ∀ {φ : Prop} (σs : List (Type u_1)) (P P' : Prop) (Q : Std.Do.SPred σs)
  [Std.Do.SPred.Tactic.HasFrame spred(⌜P⌝ ∧ ⌜P'⌝) Q φ], Std.Do.SPred.Tactic.HasFrame ⌜P ∧ P'⌝ Q φ
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.le_sup_inf_aux : ∀ {α : Type u_1} [inst : BooleanRing α] (a b c : α), (a + b + a * b) * (a + c + a * c) = a + b * c + a * (b * c)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.applyCell.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    {δ : Type u_4} →
      [inst : Ord α] →
        (k : α) →
          (motive :
              (l : Std.DTreeMap.Internal.Impl α β) →
                ((c : Std.DTreeMap.Internal.Cell α β (compare k)) →
                    (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true) → δ) →
                  Sort u_3) →
            (l : Std.DTreeMap.Internal.Impl α β) →
              (f :
                  (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
                    (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true) → δ) →
                ((f :
                      (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
                        (Std.DTreeMap.Internal.Impl.contains' (compare k) Std.DTreeMap.Internal.Impl.leaf = true →
                            c.contains = true) →
                          δ) →
                    motive Std.DTreeMap.Internal.Impl.leaf f) →
                  ((size : ℕ) →
                      (k' : α) →
                        (v' : β k') →
                          (l r : Std.DTreeMap.Internal.Impl α β) →
                            (f :
                                (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
                                  (Std.DTreeMap.Internal.Impl.contains' (compare k)
                                          (Std.DTreeMap.Internal.Impl.inner size k' v' l r) =
                                        true →
                                      c.contains = true) →
                                    δ) →
                              motive (Std.DTreeMap.Internal.Impl.inner size k' v' l r) f) →
                    motive l f
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.forward.eq_1 : ∀ (x : String.Legacy.Iterator), x.forward 0 = x
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A cofan `c` on `f` such that the induced map `∐ f ⟶ c.pt` is an iso, is a coproduct.  -/
CategoryTheory.Limits.Cofan.isColimitOfIsIsoSigmaDesc : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} →
        [inst_1 : CategoryTheory.Limits.HasCoproduct f] →
          (c : CategoryTheory.Limits.Cofan f) →
            [hc : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc c.inj)] → CategoryTheory.Limits.IsColimit c
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.leftUnitor_comp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).inv
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).hom g)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_Q : ∀ {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 l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex._auto_3),
  (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).Q = X.opcycles f₂ f₃ n₁
-- Init.Data.Fin.Lemmas
Fin.last_add_one : ∀ (n : ℕ), Fin.last n + 1 = 0
-- Mathlib.Tactic.Translate.GuessName
/-- Apply the `nameDict` and decapitalize the output like the input.

E.g.
```
#eval applyNameDict ["Inv", "HMul", "LE", "Conjugate₂", "SMul", "_", "ne", "_", "top"]
```
yields `["Neg", "HAdd", "LE", "Conjugate₂", "VAdd", "_", "ne", "_", "top"]`.
 -/
Mathlib.Tactic.GuessName.applyNameDict : Mathlib.Tactic.GuessName.GuessNameData → List String → List String
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans'_target : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ)
  (h : e.target = e'.source), (e.trans' e' h).target = e'.target
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.containsThenInsert_eq_containsₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α)
  (b : β a), (m.containsThenInsert a b).1 = m.containsₘ a
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.toAddMonoidHom_injective : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S},
  Function.Injective LinearMap.toAddMonoidHom
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.exists_fixed_point_of_prime' : ∀ {α : Type u_1} [inst : Fintype α] {p n : ℕ} [hp : Fact (Nat.Prime p)],
  p ∣ Fintype.card α → ∀ {σ : Equiv.Perm α}, σ ^ p ^ n = 1 → ∀ {a : α}, σ a = a → ∃ b, σ b = b ∧ b ≠ a
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
/-- An additive submonoid `H` of `M` determines an additive submonoid
`H.op` of the opposite monoid `Mᵐᵒᵖ`.  -/
AddSubmonoid.opEquiv : {M : Type u_2} → [inst : AddZeroClass M] → AddSubmonoid M ≃o AddSubmonoid Mᵃᵒᵖ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp], ∅.minKey? = none
-- Mathlib.CategoryTheory.Limits.Indization.LocallySmall
CategoryTheory.colimitYonedaHomEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} I]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape I (Type v)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type v)]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u v))] (F : CategoryTheory.Functor I C)
  (G : CategoryTheory.Functor Cᵒᵖ (Type v)),
  CategoryTheory.colimitYonedaHomEquiv F G =
    (Equiv.ulift.symm.trans
        (Trans.trans
              (Trans.trans (CategoryTheory.Limits.colimitYonedaHomIsoLimitOp F G)
                (CategoryTheory.Limits.HasLimit.isoOfNatIso
                  (F.op.associator G CategoryTheory.uliftFunctor.{u, v}).symm))
              (CategoryTheory.preservesLimitIso CategoryTheory.uliftFunctor.{u, v}
                  (F.op.comp G)).symm).toEquiv.symm).symm
-- Mathlib.CategoryTheory.Limits.Cones
/-- Eta rule for cocones.  -/
CategoryTheory.Limits.Cocone.eta : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → (c : CategoryTheory.Limits.Cocone F) → c ≅ { pt := c.pt, ι := c.ι }