mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.pseudofunctorOfIsLocallyDiscrete_mapComp : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory B]
  [inst_1 : CategoryTheory.Bicategory.IsLocallyDiscrete B] [inst_2 : CategoryTheory.Bicategory C] (obj : B → C)
  (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b'))
  (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b))
  (mapComp :
    {b₀ b₁ b₂ : B} →
      (f : b₀ ⟶ b₁) →
        (g : b₁ ⟶ b₂) →
          map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g))
  (map₂_associator :
    autoParam
      (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv)
                  (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_1)
  (map₂_left_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f))
              (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_3)
  (map₂_right_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom)
              (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_5)
  {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor
          map₂_right_unitor).mapComp
      f g =
    mapComp f g
-- Aesop.Builder.Basic
Aesop.PhaseSpec.norm.injEq : ∀ (info info_1 : Aesop.NormRuleInfo), (Aesop.PhaseSpec.norm info = Aesop.PhaseSpec.norm info_1) = (info = info_1)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- If `G` preserves the cokernel of `f`, then the cokernel comparison map for `G` at `f` is
an isomorphism.
 -/
CategoryTheory.Limits.PreservesCokernel.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (G : CategoryTheory.Functor C D) →
              [G.PreservesZeroMorphisms] →
                {X Y : C} →
                  (f : X ⟶ Y) →
                    [inst_5 : CategoryTheory.Limits.HasCokernel f] →
                      [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)] →
                        [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G] →
                          G.obj (CategoryTheory.Limits.cokernel f) ≅ CategoryTheory.Limits.cokernel (G.map f)
-- Mathlib.RingTheory.LocalProperties.Exactness
injective_of_localized_span : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (f : M →ₗ[R] N),
      (∀ (r : ↑s), Function.Injective ⇑((LocalizedModule.map (Submonoid.powers ↑r)) f)) → Function.Injective ⇑f
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isEmpty_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m.isEmpty = true ↔ m = ∅
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.himp_mono_left : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P P' Q : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel P' P → Lean.Order.PartialOrder.rel (Lean.Order.himp P Q) (Lean.Order.himp P' Q)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- Monomorphisms are stable under pullback in the first argument.  -/
CategoryTheory.Limits.PullbackCone.mono_snd_of_is_pullback_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsLimit t) [CategoryTheory.Mono f],
  CategoryTheory.Mono t.snd
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k k' : α}, t.getKey? k = some k' → (Std.ExtTreeMap.map f t)[k]? = Option.map (f k') t[k]?
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (a : R)
  {S : Type u_3} [inst_3 : SMul S R] [inst_4 : SMul S M] [inst_5 : IsScalarTower S R M] [inst_6 : IsScalarTower S R R],
  IsScalarTower S (R ⧸ R ∙ a) ↥(Submodule.torsionBy R M a)
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.support_normalize : ∀ {α : Type u_1} {f : α → ENNReal} (hf0 : tsum f ≠ 0) (hf : tsum f ≠ ⊤),
  (PMF.normalize f hf0 hf).support = Function.support f
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_insert_eq_of_mem_closure : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e : α}, e ∈ M.closure X → M.closure (insert e X) = M.closure X
-- Mathlib.Logic.Equiv.Fin.Basic
Nat.divModEquiv_apply : ∀ (n : ℕ) [inst : NeZero n] (a : ℕ), n.divModEquiv a = (a / n, Fin.ofNat n a)
-- Mathlib.Data.Set.Pairwise.Basic
Set.Pairwise.inter_right : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, s.Pairwise r → ∀ (t : Set α), (t ∩ s).Pairwise r
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- An `n`-dimensional `R`-vector space is equivalent to `Fin n → R`.  -/
finDimVectorspaceEquiv : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [StrongRankCondition R] → [Module.Free R M] → (n : ℕ) → Module.rank R M = ↑n → M ≃ₗ[R] Fin n → R
-- Mathlib.Analysis.Calculus.FDeriv.WithLp
PiLp.hasFDerivAt_ofLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [Finite ι] (p : ENNReal)
  [Fact (1 ≤ p)] (f : PiLp p E), HasFDerivAt WithLp.ofLp (↑(PiLp.continuousLinearEquiv p 𝕜 E)) f
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.norm_compContinuousLinearMap_le : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F)
  (n : ℕ), ‖p.compContinuousLinearMap u n‖ ≤ ‖p n‖ * ‖u‖ ^ n
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.instHashableRealizeConstKey.hash : Lean.Environment.RealizeConstKey✝ → UInt64
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.completion_toCompl : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  (f : NormedAddGroupHom G H), f.completion.comp NormedAddCommGroup.toCompl = NormedAddCommGroup.toCompl.comp f
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedResult.default : Lean.Meta.Simp.Result
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.ofDigits.match_1.eq_1 : ∀ (motive : List ℕ → Sort u_1) (h_1 : Unit → motive []) (h_2 : (h : ℕ) → (t : List ℕ) → motive (h :: t)),
  (match [] with
    | [] => h_1 ()
    | h :: t => h_2 h t) =
    h_1 ()
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag'_map : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} {β : Type u_13}
  (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (f : α → β), (M.map f).blockDiag' = fun k => (M.blockDiag' k).map f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_iff_isSome_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  a ∈ t ↔ (t.getKey? a).isSome = true
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp₂_toGerm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : TopologicalSpace β] [inst_3 : TopologicalSpace γ] (g : β → γ → δ)
  (hg : Continuous (Function.uncurry g)) (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ),
  (MeasureTheory.AEEqFun.comp₂ g hg f₁ f₂).toGerm = Filter.Germ.map₂ g f₁.toGerm f₂.toGerm
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Adjunction.comp_left_triangle_aux : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b}
  (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂),
  CategoryTheory.Bicategory.leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f₁ f₂)).hom
      (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f₁ f₂)).inv
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.find?_toList_eq_some_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {v : β k}, List.find? (fun x => cmp x.fst k == Ordering.eq) t.toList = some ⟨k, v⟩ ↔ t.get? k = some v
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.PullbackShift.adjunction_unit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) {D : Type u_4}
  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] [inst_5 : CategoryTheory.HasShift D B]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G),
  (CategoryTheory.PullbackShift.adjunction φ adj).unit =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.PullbackShift.natIsoId C φ).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.PullbackShift.natTrans φ adj.unit)
        (CategoryTheory.NatTrans.PullbackShift.natIsoComp φ F G).hom)
-- Mathlib.Order.Interval.Set.Monotone
MonotoneOn.Ioi : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  MonotoneOn f s → AntitoneOn (fun x => Set.Ioi (f x)) s
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.toOrderHom : CircleDeg1Lift → ℝ →o ℝ
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
CategoryTheory.NatTrans.ofOpSequence.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.Functor ℕᵒᵖ C}
  (app app_1 : (n : ℕ) → F.obj (Opposite.op n) ⟶ G.obj (Opposite.op n)) (e_app : app = app_1)
  (naturality :
    ∀ (n : ℕ),
      CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯).op) (app n) =
        CategoryTheory.CategoryStruct.comp (app (n + 1)) (G.map (CategoryTheory.homOfLE ⋯).op)),
  CategoryTheory.NatTrans.ofOpSequence app naturality = CategoryTheory.NatTrans.ofOpSequence app_1 ⋯
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
AddCon.lift.congr_simp : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (c : AddCon M) (f f_1 : M →+ P)
  (e_f : f = f_1) (H : c ≤ AddCon.ker f), c.lift f H = c.lift f_1 ⋯
-- Lean.Elab.Tactic.Grind.Basic
/-- Runs `x` with only the first unsolved goal as the goal.
Fails if there are no goal to be solved.
 -/
Lean.Elab.Tactic.Grind.focus : {α : Type} → Lean.Elab.Tactic.Grind.GrindTacticM α → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Batteries.Data.Array.Basic
/-- auxiliary tail-recursive function for scanlM  -/
Array.scanlM.loop : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    {α : Type u_3} →
      [Monad m] → (β → α → m β) → β → (as : Array α) → ℕ → (stop : ℕ) → stop ≤ as.size → Array β → m (Array β)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  Function.Injective ⇑(AddMonoid.Coprod.swap M N)
-- Mathlib.CategoryTheory.Functor.Trifunctor
/-- Auxiliary definition for `bifunctorComp₁₂`.  -/
CategoryTheory.bifunctorComp₁₂Obj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₁₂ : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] →
                    CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂) →
                      CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄) →
                        C₁ → CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)
-- Mathlib.Order.Northcott
/-- A composition `h' ∘ h` is Northcott when `h` is Northcott and preimages of bounded above sets
under `h'` are bounded above.  -/
Northcott.comp_of_bddAbove : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α → β) (h' : β → γ) [inst : Preorder β] [inst_1 : LE γ]
  [Northcott h], (∀ (c : γ), BddAbove (h' ⁻¹' {x | x ≤ c})) → Northcott (h' ∘ h)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.IsMonoidal.mk : ∀ {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} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} [inst_4 : F.OplaxMonoidal]
  [inst_5 : G.LaxMonoidal],
  autoParam
      (CategoryTheory.Functor.LaxMonoidal.ε G =
        CategoryTheory.CategoryStruct.comp (adj.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
          (G.map (CategoryTheory.Functor.OplaxMonoidal.η F)))
      CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_ε._autoParam →
    autoParam
        (∀ (X Y : D),
          CategoryTheory.Functor.LaxMonoidal.μ G X Y =
            CategoryTheory.CategoryStruct.comp
              (adj.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (G.obj X) (G.obj Y)))
              (G.map
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y))
                  (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y)))))
        CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_μ._autoParam →
      adj.IsMonoidal
-- Mathlib.Order.SuccPred.Limit
Order.isMin_or_mem_range_succ_or_isSuccLimit : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] (a : α),
  IsMin a ∨ a ∈ Set.range Order.succ ∨ Order.IsSuccLimit a
-- Mathlib.Order.Interval.Finset.Defs
instLocallyFiniteOrderTopSubtypeLeOfDecidableLEOfLocallyFiniteOrder : {α : Type u_1} →
  [inst : Preorder α] → {y : α} → [DecidableLE α] → [LocallyFiniteOrder α] → LocallyFiniteOrderTop { x // x ≤ y }
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_abs : ∀ (x : ℝ), |x|.toNNReal = Real.nnabs x
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithTerminal.id.match_1.eq_1 : ∀ {C : Type u_1} (motive : CategoryTheory.WithTerminal C → Sort u_2) (a : C)
  (h_1 : (a : C) → motive (CategoryTheory.WithTerminal.of a)) (h_2 : Unit → motive CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.of a with
    | CategoryTheory.WithTerminal.of a => h_1 a
    | CategoryTheory.WithTerminal.star => h_2 ()) =
    h_1 a
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst_succ_right : ∀ (n k : ℕ), n ≠ 0 → n.stirlingFirst (k + 1) = (n - 1) * (n - 1).stirlingFirst (k + 1) + (n - 1).stirlingFirst k
-- Mathlib.CategoryTheory.Shift.ShiftSequence
/-- Compatibility isomorphism `shiftFunctor C n ⋙ F.shift a ≅ F.shift a'` when `n + a = a'`.  -/
CategoryTheory.Functor.shiftIso : {C : Type u_1} →
  {A : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} A] →
        (F : CategoryTheory.Functor C A) →
          {M : Type u_4} →
            [inst_2 : AddMonoid M] →
              [inst_3 : CategoryTheory.HasShift C M] →
                [inst_4 : F.ShiftSequence M] →
                  (n a a' : M) → n + a = a' → ((CategoryTheory.shiftFunctor C n).comp (F.shift a) ≅ F.shift a')
-- Mathlib.NumberTheory.ModularForms.NormTrace
SlashInvariantForm.norm.congr_simp : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f f_1 : F),
  f = f_1 →
    ∀ [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ} [inst_1 : SlashInvariantFormClass F 𝒢 k]
      [inst_2 : 𝒢.IsFiniteRelIndex ℋ] [inst_3 : ℋ.HasDetPlusMinusOne],
      SlashInvariantForm.norm ℋ f = SlashInvariantForm.norm ℋ f_1
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mk.injEq : ∀ {numVarsSucc : ℕ} (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (clauses_1 : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc)))
  (rupUnits_1 ratUnits_1 : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc)))
  (assignments_1 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  ({ clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =
      { clauses := clauses_1, rupUnits := rupUnits_1, ratUnits := ratUnits_1, assignments := assignments_1 }) =
    (clauses = clauses_1 ∧ rupUnits = rupUnits_1 ∧ ratUnits = ratUnits_1 ∧ assignments = assignments_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {l : List α}, (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).size ≤ m.size + l.length
-- Mathlib.Algebra.Group.Hom.Defs
/-- See note [hom simp lemma priority]  -/
map_one : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
  [OneHomClass F M N] (f : F), f 1 = 1
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_inv_tensorUnit_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C),
  (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Functor.injective_of_map_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful]
  [F.PreservesMonomorphisms] {I : C}, CategoryTheory.Injective (F.obj I) → CategoryTheory.Injective I
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.φ_castSucc : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d),
  SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd (SSet.prodStdSimplex.pairingCore.min x hd).castSucc =
    (k.castSucc, (x.cast hd).simplex.2 (SSet.prodStdSimplex.pairingCore.min x hd))
-- Mathlib.LinearAlgebra.Basis.Submodule
Module.Basis.addSubgroupOfClosure.eq_1 : ∀ {M : Type u_7} {R : Type u_8} [inst : Ring R] [inst_1 : Nontrivial R] [inst_2 : IsAddTorsionFree R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (A : AddSubgroup M) {ι : Type u_9} (b : Module.Basis ι R M)
  (h : A = AddSubgroup.closure (Set.range ⇑b)),
  Module.Basis.addSubgroupOfClosure A b h =
    (Module.Basis.restrictScalars ℤ b).map
      (LinearEquiv.ofEq (Submodule.span ℤ (Set.range ⇑b)) (AddSubgroup.toIntSubmodule A) ⋯)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {R₁ R₂ : CategoryTheory.RingObjCat C} {x y : R₁.Hom R₂},
  x.hom = y.hom → x = y
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueData_ι_subschemeIso_inv : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.CategoryStruct.comp (I.glueData.ι U) I.subschemeIso.inv) =
    (TopologicalSpace.Opens.map I.subschemeι.base).obj ↑U
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} (f : V₀.V ⟶ V₁.V)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp V₀.str (F.map f) = CategoryTheory.CategoryStruct.comp f V₁.str)
      CategoryTheory.Endofunctor.Coalgebra.Hom.h._autoParam)
  (f_1 : V₀.V ⟶ V₁.V)
  (h_1 :
    autoParam (CategoryTheory.CategoryStruct.comp V₀.str (F.map f_1) = CategoryTheory.CategoryStruct.comp f_1 V₁.str)
      CategoryTheory.Endofunctor.Coalgebra.Hom.h._autoParam),
  ({ f := f, h := h } = { f := f_1, h := h_1 }) = (f = f_1)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.forInStep.eq_def : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [inst : Monad m]
  (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (x : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.forInStep f init x =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf => pure (ForInStep.yield init)
    | Std.DTreeMap.Internal.Impl.inner size k v l r => do
      let __do_lift ← Std.DTreeMap.Internal.Impl.forInStep f init l
      match __do_lift with
        | ForInStep.done d => pure (ForInStep.done d)
        | ForInStep.yield d => do
          let __do_lift ← f k v d
          match __do_lift with
            | ForInStep.done d => pure (ForInStep.done d)
            | ForInStep.yield d => Std.DTreeMap.Internal.Impl.forInStep f d r
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.IsCovering.map_injective : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V),
  φ.IsCovering → ∀ {u v : U}, Function.Injective fun f => φ.map f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k} {hc : k ∈ t.modify k f},
  (t.modify k f).get k hc = f (t.get k ⋯)