mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_functor_obj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C),
  (CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit.functor.obj F).X =
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{w + 1}))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- Conjugation in `G` as a morphism. This is the map `(x, y) ↦ x + y + (-x)`,
see `CategoryTheory.AddGrpObj.lift_conj_eq_add_add_neg`.  -/
CategoryTheory.AddGrpObj.addConj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (G : C) → [CategoryTheory.AddGrpObj G] → CategoryTheory.MonoidalCategoryStruct.tensorObj G G ⟶ G
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_congr : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k₁ k₂ : α} (h' : compare k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t), t.getKey k₁ h₁ = t.getKey k₂ ⋯
-- Mathlib.Data.Int.Interval
Int.Icc_eq_pair : ∀ (a : ℤ), Finset.Icc a (a + 1) = {a, a + 1}
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.instCommRingObjForgetAlgHomCarrier : {R : Type u} → [inst : CommRing R] → {A : CommAlgCat R} → CommRing ((CategoryTheory.forget (CommAlgCat R)).obj A)
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.isSymm_posForm : ∀ {ι : 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], LinearMap.IsSymm B.posForm
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.mul_eval_of_const_right : ∀ (l₁ l₂ : Lean.Omega.LinearCombo) (v : Lean.Omega.Coeffs),
  l₂.coeffs.isZero → (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v
-- Mathlib.Algebra.Polynomial.Inductions
/-- `divX` as an additive homomorphism.  -/
Polynomial.divX_hom : {R : Type u} → [inst : Semiring R] → Polynomial R →+ Polynomial R
-- Lean.Parser.Command
Lean.Parser.Command.check_failure : Lean.Parser.Parser
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ne_empty_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a : α}, a ∈ t → t ≠ ∅
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The identity functor is also the identity on additive monoid objects.  -/
CategoryTheory.Functor.mapAddMonIdIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (CategoryTheory.Functor.id C).mapAddMon ≅ CategoryTheory.Functor.id (CategoryTheory.AddMon C)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.reverse_append : ∀ {n m : ℕ} (c₁ : Composition m) (c₂ : Composition n), (c₁.append c₂).reverse = (c₂.reverse.append c₁.reverse).cast ⋯
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
/-- `legendreSym p 2` is given by `χ₈ p`.  -/
legendreSym.at_two : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], p ≠ 2 → legendreSym p 2 = ZMod.χ₈ ↑p
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instBEqPreInstance : BEq Lean.Meta.Grind.PreInstance
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeAPFree.prod : ∀ {α : Type u_2} {β : Type u_3} [inst : AddMonoid α] [inst_1 : AddMonoid β] {s : Set α} {t : Set β},
  ThreeAPFree s → ThreeAPFree t → ThreeAPFree (s ×ˢ t)
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.instGeometricallyIntegralFstScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyIntegral g],
  AlgebraicGeometry.GeometricallyIntegral (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.instCStarModuleProd : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      {E : Type u_2} →
        {F : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : Module ℂ E] →
              [inst_4 : SMul A E] →
                [inst_5 : NormedAddCommGroup F] →
                  [inst_6 : Module ℂ F] →
                    [inst_7 : SMul A F] →
                      [inst_8 : CStarModule A E] →
                        [inst_9 : CStarModule A F] → [StarOrderedRing A] → CStarModule A (WithCStarModule A (E × F))
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The homology of a homological complex in degree `j` can be computed
by specifying a choice of `c.prev j` and `c.next j`.  -/
HomologicalComplex.opcyclesIsoSc' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            (i j k : ι) →
              c.prev j = i →
                c.next j = k →
                  [inst_2 : K.HasHomology j] →
                    [inst_3 : (K.sc' i j k).HasHomology] → K.opcycles j ≅ (K.sc' i j k).opcycles
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- The optimal coupling between two compact spaces `X` and `Y` is still a compact space  -/
GromovHausdorff.compactSpace_optimalGHCoupling : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
  CompactSpace (GromovHausdorff.OptimalGHCoupling X Y)
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_submatrix_equiv_self : ∀ {m : Type u} {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : Fintype m] [inst_4 : CommRing α] (e : n ≃ m) (A : Matrix m m α),
  (A.submatrix ⇑e ⇑e).adjugate = A.adjugate.submatrix ⇑e ⇑e
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.ext : ∀ ⦃f g : CircleDeg1Lift⦄, (∀ (x : ℝ), f x = g x) → f = g
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.freeHomEquiv.eq_1 : ∀ {R : Type u} [inst : Ring R] {X : Type u} {M : ModuleCat R},
  ModuleCat.freeHomEquiv =
    { toFun := fun φ => TypeCat.ofHom fun x => (CategoryTheory.ConcreteCategory.hom φ) (ModuleCat.freeMk x),
      invFun := fun ψ => ModuleCat.freeDesc (TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom ψ)), left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {g : α → β},
  MeasureTheory.MeasurePreserving g μ ν →
    ∀ {s : Set β},
      MeasurableSet s → ∀ {f : β → ENNReal}, Measurable f → ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν
-- Mathlib.AlgebraicGeometry.AffineSpace
/-- The morphism `X ⟶ 𝔸(n; S)` given by a `X ⟶ S` and a choice of `n`-coordinate functions.  -/
AlgebraicGeometry.AffineSpace.homOfVector : {n : Type u} →
  {S X : AlgebraicGeometry.Scheme} →
    (X ⟶ S) → (n → ↑(X.presheaf.obj (Opposite.op ⊤))) → (X ⟶ AlgebraicGeometry.AffineSpace n S)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.instIsLeftCancelAdd : IsLeftCancelAdd Ordinal.{u_4}
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.subtype_univ : ∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : Fintype { a // p a }],
  Finset.subtype p Finset.univ = Finset.univ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool} {k k' : α},
  m.WF → m.getKey? k = some k' → (Std.HashMap.Raw.filter f m)[k]? = Option.filter (f k') m[k]?
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.I_zero : ∀ {θ : ℝ}, I✝ 0 θ * θ = 2 * Real.sin θ
-- Mathlib.CategoryTheory.Grothendieck
/-- Construct a functor from `Grothendieck F` to another category `E` by providing a family of
functors on the fibers of `Grothendieck F`, a family of natural transformations on morphisms in the
base of `Grothendieck F` and coherence data for this family of natural transformations.  -/
CategoryTheory.Grothendieck.functorFrom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {E : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} E] →
          (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) →
            (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c')) →
              (∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) →
                (∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
                    hom (CategoryTheory.CategoryStruct.comp f g) =
                      CategoryTheory.CategoryStruct.comp (hom f)
                        (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g))
                          (CategoryTheory.eqToHom ⋯))) →
                  CategoryTheory.Functor (CategoryTheory.Grothendieck F) E
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer.ι_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {Z : CategoryTheory.Functor C (Type w)} (h : F₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.equalizer.ι f g)
      (CategoryTheory.CategoryStruct.comp A.ι h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.equalizer f g).ι h
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.mono : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r r' : ENNReal},
  HasFPowerSeriesOnBall f p x r → 0 < r' → r' ≤ r → HasFPowerSeriesOnBall f p x r'
-- Mathlib.Order.Heyting.Hom
/-- The type of co-Heyting homomorphisms from `α` to `β`. Bounded lattice homomorphisms that
preserve difference.  -/
CoheytingHom : (α : Type u_6) → (β : Type u_7) → [CoheytingAlgebra α] → [CoheytingAlgebra β] → Type (max u_6 u_7)
-- Mathlib.Analysis.Normed.Group.Uniform
AntilipschitzWith.mul_lipschitzWith : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E},
  AntilipschitzWith Kf f → LipschitzWith Kg g → Kg < Kf⁻¹ → AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun x => f x * g x
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.autCongr_symm : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂), ϕ.autCongr.symm = ϕ.symm.autCongr
-- Init.Data.Fin.Lemmas
Fin.zero_eq_mk : ∀ {n a : ℕ} {ha : a < n} [inst : NeZero n], 0 = ⟨a, ha⟩ ↔ a = 0
-- Mathlib.Data.FunLike.Equiv
EquivLike.surjective_comp : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [inst : EquivLike E α β] (e : E) (f : β → γ),
  Function.Surjective (f ∘ ⇑e) ↔ Function.Surjective f
-- Mathlib.Algebra.Order.SuccPred
Order.wcovBy_add_one : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α] (x : α), x ⩿ x + 1
-- Mathlib.Analysis.Analytic.IteratedFDeriv
/-- If a function has a power series in a ball, then its `n`-th iterated derivative is given by
`(v₁, ..., vₙ) ↦ ∑ pₙ (v_{σ (1)}, ..., v_{σ (n)})` where the sum is over all
permutations of `{1, ..., n}`.  -/
HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    AnalyticOn 𝕜 f s →
      UniqueDiffOn 𝕜 s →
        x ∈ s → ∀ {n : ℕ} (v : Fin n → E), (iteratedFDerivWithin 𝕜 n f s x) v = ∑ σ, (p n) fun i => v (σ i)
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_pos_of_neg_of_neg : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPartialOrder R]
  [Lean.Grind.OrderedRing R] [Std.LawfulOrderLT R] {a b : R}, a < 0 → b < 0 → 0 < a * b
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.externalCoveringNumber_eq_one_of_ediam_le : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal},
  A.Nonempty → Metric.ediam A ≤ ↑ε → Metric.externalCoveringNumber ε A = 1
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.neg_norm_le_apply : ∀ {α : Type u} [inst : TopologicalSpace α] (f : BoundedContinuousFunction α ℝ) (x : α), -‖f‖ ≤ f x
-- Mathlib.Order.CompleteLattice.Group
le_iInf_add : ∀ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] [inst_1 : Add α] [AddLeftMono α] [AddRightMono α]
  (u v : ι → α), (⨅ i, u i) + ⨅ i, v i ≤ ⨅ i, u i + v i
-- Mathlib.MeasureTheory.Measure.LevyConvergence
/-- Let `μ` be a tight sequence of probability measures and `μ₀` a probability measure.
If `A` is a star sub-algebra of bounded continuous scalar functions that separates points
and the integrals of elements of `A` with respect to `μ` converge to the integrals
with respect to `μ₀`, then `μ` converges weakly to `μ₀`.  -/
MeasureTheory.ProbabilityMeasure.tendsto_of_tight_of_separatesPoints : ∀ (𝕜 : Type u_2) [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : MeasurableSpace E] [inst_2 : TopologicalSpace E]
  [PolishSpace E] [inst_4 : BorelSpace E] {ι : Type u_4} {𝓕 : Filter ι} {μ : ι → MeasureTheory.ProbabilityMeasure E},
  MeasureTheory.IsTightMeasureSet {x | ∃ n, ↑(μ n) = x} →
    ∀ {μ₀ : MeasureTheory.ProbabilityMeasure E} {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)},
      (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).SeparatesPoints →
        (∀ g ∈ A, Filter.Tendsto (fun n => ∫ (x : E), g x ∂↑(μ n)) 𝓕 (nhds (∫ (x : E), g x ∂↑μ₀))) →
          Filter.Tendsto μ 𝓕 (nhds μ₀)
-- Mathlib.Algebra.Order.Group.OrderIso
/-- **Alias** of the forward direction of `le_inv'`. -/
le_inv_of_le_inv : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] [MulRightMono α] {a b : α}, a ≤ b⁻¹ → b ≤ a⁻¹
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- Normalize the multiplicity of a prime ideal `p` in the factorization of `I`
as `multiplicity p.asIdeal I`.  -/
IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiplicity : ∀ {R : Type u_3} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R},
  I ≠ ⊥ → ∀ (p : IsDedekindDomain.HeightOneSpectrum R), p.maxPowDividing I = p.asIdeal ^ multiplicity p.asIdeal I
-- Lean.Linter.UnusedVariables
/-- An extension which keeps track of registered `IgnoreFunction`s.  -/
Lean.Linter.unusedVariablesIgnoreFnsExt : Lean.PersistentEnvExtension Lean.Name (Lean.Name × Lean.Linter.IgnoreFunction)
  (List Lean.Name × Array Lean.Linter.IgnoreFunction)
-- Lean.Elab.Match
/-- Try to restore `Syntax` ref information stored in `map` after
applying `whnf` at `whnfPreservingPatternRef`.
It assumes `map` has been constructed using `mkPatternRefMap`.
 -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.applyRefMap : Lean.Expr → Lean.ExprMap Lean.Expr → Lean.Expr
-- Lean.DocString.Parser
/-- Parses a link.  -/
Lean.Doc.Parser.link : Lean.Doc.Parser.InlineCtxt → Lean.Parser.ParserFn
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.zipWithTR.go.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : List α) (a_1 : List β) (a_2 : Array γ),
  (∀ (a_3 : α) (as : List α) (b : β) (bs : List β), a = a_3 :: as → a_1 = b :: bs → False) →
    List.zipWithTR.go✝ f a a_1 a_2 = a_2.toList
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_pos : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R}, 0 < ⌊a⌋ ↔ 1 ≤ a
-- Mathlib.MeasureTheory.Constructions.SimpleGraph
SimpleGraph.measurable_edgeSet : ∀ {V : Type u_1}, Measurable SimpleGraph.edgeSet
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β}, k ∉ m₂ → (m₁ \ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.eq_zero_of_hom_shift_pos : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_4 : CategoryTheory.Category.{v_2, u_2} A] {ι : CategoryTheory.Functor A C},
  (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) →
    ∀ {X Y : A} {n : ℤ} (f : (CategoryTheory.shiftFunctor C n).obj (ι.obj X) ⟶ ι.obj Y), 0 < n → f = 0
-- Init.SimpLemmas
instLawfulIdentityOrFalse : Std.LawfulIdentity Or False
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_iInf' : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {x : ι → Filter α} {y : Filter β} (i : ι),
  Filter.Tendsto f (x i) y → Filter.Tendsto f (⨅ i, x i) y
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp_assoc_left_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X)
      ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X)) =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)
        ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X)))
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.seminorm_one_eq_one_iff_ne_zero : ∀ {R : Type u_1} [inst : Ring R] (p : RingSeminorm R), p 1 ≤ 1 → (p 1 = 1 ↔ p ≠ 0)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.le_inv_iff : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : Aˣ},
  0 ≤ ↑a → 0 ≤ ↑b → (↑a ≤ ↑b⁻¹ ↔ ↑b ≤ ↑a⁻¹)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α},
  Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.filter f m) k =
    (Std.ExtDHashMap.Const.get? m k).pfilter fun x_2 h' => f (m.getKey k ⋯) x_2
-- Mathlib.Data.List.GetD
List.getD_eq_default : ∀ {α : Type u} (l : List α) (d : α) {n : ℕ}, l.length ≤ n → l.getD n d = d
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {b : β}, s • {b} = (fun x => x • b) '' s
-- Mathlib.Order.Defs.LinearOrder
min_self : ∀ {α : Type u_1} [inst : LinearOrder α] (a : α), min a a = a
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.d₀₁_comp_d₁₂_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k (G × G → ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.d₀₁ A)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.d₁₂ A) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.boundary_length : ∀ {n : ℕ} (c : CompositionAsSet n), c.boundary ⟨c.length, ⋯⟩ = Fin.last n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Raw.Const.modify t k f).size = t.size
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
Algebra.TensorProduct.includeLeftSubRight_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S] (s : S),
  (Algebra.TensorProduct.includeLeftSubRight R S) s = s ⊗ₜ[R] 1 - 1 ⊗ₜ[R] s
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- The `atBot` filter for `↑(Iic a)` comes from the `atBot` filter in the ambient order.  -/
Filter.atBot_Iic_eq : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] (a : α), Filter.atBot = Filter.comap Subtype.val Filter.atBot
-- Mathlib.CategoryTheory.Types.Basic
/-- The equivalence between `Fun`s and functions between types.  -/
TypeCat.Fun.homEquiv : (X Y : Type u) → TypeCat.Fun X Y ≃ (X → Y)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.homMk_hom_apply : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R}
  (φ :
    (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj M ⟶
      (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj N)
  (hφ : ∀ (r : R), CategoryTheory.CategoryStruct.comp φ (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ)
  (a : ↑((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).obj M)),
  (ModuleCat.Hom.hom (ModuleCat.homMk φ hφ)) a = (CategoryTheory.ConcreteCategory.hom φ) a
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.compCoyonedaIso_inv_app_app_hom_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : Cᵒᵖ) (X_1 : D)
  (x : Opposite.unop X ⟶ G.obj X_1),
  (CategoryTheory.ConcreteCategory.hom ((adj.compCoyonedaIso.inv.app X).app X_1)) x =
    CategoryTheory.CategoryStruct.comp (F.map x) (adj.counit.app X_1)
-- Lean.Data.Lsp.Utf16
Lean.String.utf16PosToCodepointPos : String → ℕ → ℕ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, (m.insertIfNew k v).isEmpty = false
-- Mathlib.Algebra.Module.Submodule.Pointwise
/-- Induction principle for set acting on submodules. To prove `P` holds for all `s • N`, it is enough
to prove:
- for all `r ∈ s` and `n ∈ N`, `P (r • n)`;
- for all `r` and `m ∈ s • N`, `P (r • n)`;
- for all `m₁, m₂`, `P m₁` and `P m₂` implies `P (m₁ + m₂)`;
- `P 0`.

To invoke this induction principle, use `induction x, hx using Submodule.set_smul_inductionOn` where
`x : M` and `hx : x ∈ s • N`
 -/
Submodule.set_smul_inductionOn : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] {s : Set S} {N : Submodule R M}
  {motive : (x : M) → x ∈ s • N → Prop} (x : M) (hx : x ∈ s • N),
  (∀ ⦃r : S⦄ ⦃n : M⦄ (mem₁ : r ∈ s) (mem₂ : n ∈ N), motive (r • n) ⋯) →
    (∀ (r : R) ⦃m : M⦄ (mem : m ∈ s • N), motive m mem → motive (r • m) ⋯) →
      (∀ ⦃m₁ m₂ : M⦄ (mem₁ : m₁ ∈ s • N) (mem₂ : m₂ ∈ s • N), motive m₁ mem₁ → motive m₂ mem₂ → motive (m₁ + m₂) ⋯) →
        motive 0 ⋯ → motive x hx
-- Mathlib.Combinatorics.Graph.Simple
Graph.toSimpleGraph_adj_iff : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] (u v : ↑G.vertexSet), G.toSimpleGraph.Adj u v ↔ G.Adj ↑u ↑v