mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0`, `+`, unary `-`, and binary `-`
is a `SubtractionMonoid` if it admits an injective map that preserves `0`, `+`, unary `-`, and
binary `-` to a `SubtractionMonoid`. This version takes custom `nsmul` and `zsmul` as `[SMul ℕ M₁]`
and `[SMul ℤ M₁]` arguments.  -/
Function.Injective.subtractionMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : Neg M₁] →
            [inst_4 : Sub M₁] →
              [inst_5 : SMul ℤ M₁] →
                [inst_6 : SubtractionMonoid M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 0 = 0 →
                        (∀ (x y : M₁), f (x + y) = f x + f y) →
                          (∀ (x : M₁), f (-x) = -f x) →
                            (∀ (x y : M₁), f (x - y) = f x - f y) →
                              (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) →
                                (∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) → SubtractionMonoid M₁
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.isoShift_hom_naturality : ∀ {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 : M) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C n).map f)) ((F.isoShift n).hom.app Y) =
    CategoryTheory.CategoryStruct.comp ((F.isoShift n).hom.app X) ((F.shift n).map f)
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Sheaf.toImage_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F'),
  (CategoryTheory.Sheaf.toImage f).hom = CategoryTheory.Subfunctor.toRangeSheafify J f.hom
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.instCoeHeadObjToFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type w)} →
      (G : CategoryTheory.Subfunctor F) → {U : C} → CoeHead (G.toFunctor.obj U) (F.obj U)
-- Mathlib.Algebra.MvPolynomial.Eval
/-- If `S` is an `R`-algebra, then `MvPolynomial σ S` is a `MvPolynomial σ R` algebra.

Warning: This produces a diamond for
`Algebra (MvPolynomial σ R) (MvPolynomial σ (MvPolynomial σ S))`. That's why it is not a
global instance.
 -/
MvPolynomial.algebraMvPolynomial : {R : Type u_2} →
  {S : Type u_3} →
    {σ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] → [Algebra R S] → Algebra (MvPolynomial σ R) (MvPolynomial σ S)
-- Mathlib.Data.Set.Equitable
Finset.equitableOn_iff : ∀ {α : Type u_1} {s : Finset α} {f : α → ℕ},
  (↑s).EquitableOn f ↔ ∀ a ∈ s, f a = (∑ i ∈ s, f i) / s.card ∨ f a = (∑ i ∈ s, f i) / s.card + 1
-- Std.Sync.Channel
/-- Create a new channel. If:
- `capacity` is `none` it will be unbounded (the default)
- `capacity` is `some 0` it will always force a rendezvous between sender and receiver
- `capacity` is `some n` with `n > 0` it will use a buffer of size `n` and begin blocking once it
  is filled
 -/
Std.Channel.Sync.new : {α : Type} → optParam (Option ℕ) none → BaseIO (Std.Channel.Sync α)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_eq_some_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.max? = some t.max!
-- Mathlib.Algebra.MvPolynomial.Derivation
MvPolynomial.derivation_eq_of_forall_mem_vars : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] {D₁ D₂ : Derivation R (MvPolynomial σ R) A} {f : MvPolynomial σ R},
  (∀ i ∈ f.vars, D₁ (MvPolynomial.X i) = D₂ (MvPolynomial.X i)) → D₁ f = D₂ f
-- Mathlib.Topology.Sheaves.Functors
/-- The "naive" sheaf pullback by an open embedding `f`: on the underlying presheaf, this is just
composition by the functor `IsOpenMap.functor f` (sending an open `U` to `f '' U`).
 -/
Topology.IsOpenEmbedding.sheafPullback : {X Y : TopCat} →
  (A : Type u_1) →
    [inst : CategoryTheory.Category.{w, u_1} A] →
      {f : X ⟶ Y} →
        Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) →
          CategoryTheory.Functor (TopCat.Sheaf A Y) (TopCat.Sheaf A X)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.instToFormatPComp : Std.ToFormat Mathlib.Tactic.Linarith.PComp
-- Mathlib.Algebra.Order.ToIntervalMod
self_sub_toIocMod_eq_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R), b - toIocMod hp a b = ↑(toIocDiv hp a b) * p
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKeyLT?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyLT? k = t₂.getKeyLT? k
-- Mathlib.Data.List.Map2
List.map₂Right'_nil_cons : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (b : β) (bs : List β),
  List.map₂Right' f [] (b :: bs) = (f none b :: List.map (f none) bs, [])
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.whisker_left_comp : ∀ {B : Type u} [inst : Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b)
  {g h i : CategoryTheory.FreeBicategory.Hom b c} (η : CategoryTheory.FreeBicategory.Hom₂ g h)
  (θ : CategoryTheory.FreeBicategory.Hom₂ h i),
  CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_left f (η.vcomp θ))
    ((CategoryTheory.FreeBicategory.Hom₂.whisker_left f η).vcomp (CategoryTheory.FreeBicategory.Hom₂.whisker_left f θ))
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_hom_app_op_zero : CategoryTheory.Limits.walkingParallelPairOpEquiv.counitIso.hom.app
    (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero) =
  CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_subtype : ∀ {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {α : Type u_6}
  [inst_2 : MeasureTheory.MeasureSpace α] {s : Set α},
  MeasurableSet s → ∀ (f : α → G), ∫ (x : ↑s), f ↑x = ∫ (x : α) in s, f x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.toCone_pt : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q), c.toCone.pt = c.pt
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.hf_modif_int : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E),
  MeasureTheory.LocallyIntegrableOn P.f_modif (Set.Ioi 0) MeasureTheory.volume
-- Mathlib.Data.Nat.ModEq
Nat.modEq_sub : ∀ {a b : ℕ}, b ≤ a → a ≡ b [MOD a - b]
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.invert.eq_1 : ∀ {R : Type u_3} [inst : CommSemiring R], LaurentPolynomial.invert = AddMonoidAlgebra.domCongr R R (AddEquiv.neg ℤ)
-- Aesop.RuleSet.Filter
Aesop.RuleSetNameFilter.mk : Array Aesop.RuleSetName → Aesop.RuleSetNameFilter
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.sSup_add_one_lt_of_lt_cof : ∀ {s : Set Ordinal.{u}} {a : Ordinal.{u}},
  Cardinal.mk ↑s < (Ordinal.lift.{u + 1, u} a).cof → (∀ i ∈ s, i < a) → sSup ((fun x => x + 1) '' s) < a
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_zero_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  [Nonempty β] [L.LeAtTop], HasProd (fun x => 0) 0 L
-- Mathlib.Order.Filter.Extr
IsMinOn.isGLB : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  a ∈ s → IsMinOn f s a → IsGLB {x | ∃ x_1 ∈ s, f x_1 = x} (f a)
-- Mathlib.Lean.Expr.Basic
/-- Test if an expression is either `Nat.zero`, or `OfNat.ofNat 0`.  -/
Lean.Expr.zero? : Lean.Expr → Bool
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.commRing : {R : Type u} → [inst : CommRing R] → CommRing (Polynomial R)
-- Mathlib.CategoryTheory.Equivalence
/-- To see that a functor is an equivalence, it suffices to provide an inverse functor `G` such that
`F ⋙ G` and `G ⋙ F` are naturally isomorphic to identity functors.  -/
CategoryTheory.Functor.IsEquivalence.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} (G : CategoryTheory.Functor D C) (η : CategoryTheory.Functor.id C ≅ F.comp G)
  (ε : G.comp F ≅ CategoryTheory.Functor.id D), F.IsEquivalence
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.quotientTensorEquiv_symm_apply_mk_tmul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (m : Submodule R M) (x : M) (y : N),
  (TensorProduct.quotientTensorEquiv N m).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) = Submodule.Quotient.mk x ⊗ₜ[R] y
-- Mathlib.Topology.Constructions
mem_nhds_of_pi_mem_nhds : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {I : Set ι} {s : (i : ι) → Set (A i)}
  (a : (i : ι) → A i), I.pi s ∈ nhds a → ∀ {i : ι}, i ∈ I → s i ∈ nhds (a i)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IteratorLoop.wellFounded_of_productive.match_1.splitter : {γ : Type u_1} →
  (motive : ForInStep γ → Sort u_2) →
    (s : ForInStep γ) →
      ((a : γ) → motive (ForInStep.done a)) →
        ((x : ForInStep γ) → (∀ (a : γ), x = ForInStep.done a → False) → motive x) → motive s
-- Mathlib.Topology.LocallyFinsupp
/-- Restriction as a lattice morphism  -/
Function.locallyFinsuppWithin.restrictLatticeHom : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} →
      {Y : Type u_2} →
        [inst_1 : AddCommGroup Y] →
          [inst_2 : Lattice Y] →
            {V : Set X} → V ⊆ U → LatticeHom (Function.locallyFinsuppWithin U Y) (Function.locallyFinsuppWithin V Y)
-- Mathlib.Data.Nat.Factorization.Defs
/-- For prime `p` the only prime factor of `p^k` is `p` with multiplicity `k`  -/
Nat.Prime.factorization_pow : ∀ {p k : ℕ}, Nat.Prime p → (p ^ k).factorization = fun₀ | p => k
-- Init.Data.List.Lemmas
List.all_eq_true : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, l.all p = true ↔ ∀ x ∈ l, p x = true
-- Mathlib.Algebra.Order.Module.Defs
SMulPosMono.toSMulPosStrictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : AddCommGroup β] [inst_2 : Module α β]
  [inst_3 : PartialOrder α] [inst_4 : PartialOrder β] [IsDomain α] [Module.IsTorsionFree α β] [SMulPosMono α β],
  SMulPosStrictMono α β
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.dist_left_right_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ → dist p₁ p₂ / 2 = s.radius
-- Mathlib.Algebra.Group.Hom.Instances
ZeroHom.zsmul_apply : ∀ {M : Type uM} {N : Type uN} [inst : Zero M] [inst_1 : AddGroup N] (f : ZeroHom M N) (z : ℤ) (x : M),
  (z • f) x = z • f x
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
max_sub_min_eq_abs : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] [AddRightMono α] (a b : α),
  max a b - min a b = |b - a|
-- Mathlib.Dynamics.Ergodic.AddCircle
MeasurableEquiv.addLeft.congr_simp : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableAdd G] (g g_1 : G),
  g = g_1 → MeasurableEquiv.addLeft g = MeasurableEquiv.addLeft g_1
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The data part of a continuation is a list of lists, which is encoded on the `stack` stack
using `trLList`.  -/
Turing.PartrecToTM2.contStack : Turing.ToPartrec.Cont → List (List ℕ)
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- The radical of a quadratic map is contained in the kernel of its polar bilinear map.

See `radical_eq_ker_polarBilin` for the equality when 2 is invertible in the
coefficient ring.  -/
QuadraticMap.radical_le_ker_polarBilin : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] {Q : QuadraticMap R M P}, Q.radical ≤ LinearMap.ker Q.polarBilin
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.preimage_sphere : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ℝ), f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r
-- Mathlib.Order.RelSeries
RelSeries.ofLE_length : ∀ {α : Type u_1} {r : SetRel α α} (x : RelSeries r) {s : SetRel α α} (h : r ⊆ s), (x.ofLE h).length = x.length
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_False : Set.Iio False = ∅
-- Mathlib.RingTheory.Idempotents
Subsemigroup.mem_corner_iff_mem_range_mul_left : ∀ {R : Type u_1} {e : R} [inst : Semigroup R],
  IsIdempotentElem e → IsMulCentral e → ∀ {r : R}, r ∈ Subsemigroup.corner e ↔ r ∈ Set.range fun x => e * x
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
CliffordAlgebra.prodEquiv_apply : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] (Q₁ : QuadraticForm R M₁)
  (Q₂ : QuadraticForm R M₂) (a : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)),
  (CliffordAlgebra.prodEquiv Q₁ Q₂) a = (CliffordAlgebra.ofProd Q₁ Q₂) a
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteObjFinite : ∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : FintypeCat), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete X.obj) F
-- Init.Data.BitVec.Lemmas
BitVec.umod_zero : ∀ {n : ℕ} {x : BitVec n}, x % 0#n = x
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.coprodOpenCover.eq_1 : ∀ (X Y : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.coprodOpenCover X Y =
    { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1}, X := fun x => Sum.elim (fun x => X) (fun x => Y) x,
      f := fun x => Sum.rec (fun x => CategoryTheory.Limits.coprod.inl) (fun x => CategoryTheory.Limits.coprod.inr) x,
      mem₀ := ⋯ }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.constGetD_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β},
  m₁.WF → m₂.WF → m₁.Equiv m₂ → Std.DHashMap.Raw.Const.getD m₁ k fallback = Std.DHashMap.Raw.Const.getD m₂ k fallback
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.llr_def : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
  MeasureTheory.llr μ ν = fun x => Real.log (μ.rnDeriv ν x).toReal
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.ae_eq_image_of_ae_eq_comap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β)
  (μ : MeasureTheory.Measure β),
  Function.Injective f →
    (∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ) →
      ∀ {s t : Set α}, s =ᵐ[MeasureTheory.Measure.comap f μ] t → f '' s =ᵐ[μ] f '' t
-- Std.Http.Internal.Char
/-- Checks if a byte is an alphanumeric digit (0-9, a-z, or A-Z).
 -/
Std.Http.Internal.Char.isAlphaNum : UInt8 → Bool
-- Mathlib.Logic.Equiv.Fin.Basic
finSumFinEquiv_symm_last : ∀ {n : ℕ}, finSumFinEquiv.symm (Fin.last n) = Sum.inr 0
-- Aesop.Script.Step
Aesop.Script.LazyStep.BuildInput : Type → Type
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.add_pair : ∀ {α : Type u_2} [inst : Add α] (s : Set α) (a b : α), s + {a, b} = (AddOpposite.op a +ᵥ s) ∪ (AddOpposite.op b +ᵥ s)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.sigmoid_lt : ∀ {a b : ℝ}, a < b → unitInterval.sigmoid a < unitInterval.sigmoid b
-- Mathlib.Order.UpperLower.Closure
UpperSet.sdiff_idem : ∀ {α : Type u_1} [inst : Preorder α] (s : UpperSet α) (t : Set α), (s.sdiff t).sdiff t = s.sdiff t
-- Mathlib.Order.Basic
LE.le.ge_iff_eq' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, b ≤ a → (a ≤ b ↔ a = b)
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
CategoryTheory.TwoSquare.GuitartExact.hComp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [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} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {V₁ : CategoryTheory.Functor C₁ D₁} {T₁ : CategoryTheory.Functor C₁ C₂} {B₁ : CategoryTheory.Functor D₁ D₂}
  {V₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T₁ V₁ V₂ B₁) {T₂ : CategoryTheory.Functor C₂ C₃}
  {B₂ : CategoryTheory.Functor D₂ D₃} {V₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare T₂ V₂ V₃ B₂)
  [w.GuitartExact] [w'.GuitartExact], (w.hComp w').GuitartExact
-- Mathlib.Computability.Primrec.Basic
Primrec.const : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] (x : σ), Primrec fun x_1 => x
-- Mathlib.SetTheory.Ordinal.Notation
ONote.instAdd : Add ONote
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instNorm : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} → {μ : MeasureTheory.Measure α} → [inst : NormedAddCommGroup E] → Norm ↥(MeasureTheory.Lp E p μ)
-- Std.Sat.AIG.CachedGates
/-- Create a not gate in the input AIG. This uses the builtin cache to enable automated subterm sharing.
 -/
Std.Sat.AIG.mkNotCached : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- This lemma is impractical to state in the dependent case.  -/
PiTensorProduct.reindex_symm : ∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {M : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (e : ι ≃ ι₂),
  (PiTensorProduct.reindex R (fun x => M) e).symm = PiTensorProduct.reindex R (fun x => M) e.symm
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instFaithfulSMul : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  {S : Type u_3} [inst_2 : SMul R S] [FaithfulSMul R S], FaithfulSMul (WithVal v) S
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.toLinearMap_lTensor : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (f : ρ.IntertwiningMap σ),
  (Representation.IntertwiningMap.lTensor τ f).toLinearMap = LinearMap.lTensor U f.toLinearMap
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousLinearEquiv.continuousMultilinearMapCongrRight_symm : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_5} {G : Type u_6} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [inst_8 : ContinuousConstSMul 𝕜 F] [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜 G]
  [inst_11 : TopologicalSpace G] [inst_12 : IsTopologicalAddGroup G] [inst_13 : ContinuousConstSMul 𝕜 G]
  (g : F ≃L[𝕜] G),
  (ContinuousLinearEquiv.continuousMultilinearMapCongrRight E g).symm =
    ContinuousLinearEquiv.continuousMultilinearMapCongrRight E g.symm
-- Init.Data.Nat.ToString
Nat.toDigits_zero : ∀ (b : ℕ), b.toDigits 0 = ['0']
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.add_iff_left : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : AddCommGroup β] [IsTopologicalAddGroup β],
  MeasureTheory.AEStronglyMeasurable f μ →
    (MeasureTheory.AEStronglyMeasurable (g + f) μ ↔ MeasureTheory.AEStronglyMeasurable g μ)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.mem_isPairSelfAdjointSubmodule : ∀ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂] {B F : M →ₗ[R] M →ₗ[R] M₂} (f : Module.End R M),
  f ∈ B.isPairSelfAdjointSubmodule F ↔ B.IsPairSelfAdjoint F ⇑f
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.inf_apply : ∀ {E : Type u_3} [inst : CommGroup E] (p q : GroupSeminorm E) (x : E), (p ⊓ q) x = ⨅ y, p y + q (x / y)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.mkError : Lean.ParseImports.State → String → Lean.ParseImports.State
-- Mathlib.Order.Interval.Finset.Defs
WithBot.Icc_coe_coe : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : LocallyFiniteOrder α] (a b : α),
  Finset.Icc ↑b ↑a = Finset.map Function.Embedding.some (Finset.Icc b a)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_id : ∀ {P : Type u_3} [inst : Mul P] (S : Subsemigroup P), Subsemigroup.comap (MulHom.id P) S = S
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
measurableEmbedding_addRight : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [MeasurableAdd G] (g : G),
  MeasurableEmbedding fun x => x + g
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedCallHierarchyItem : Inhabited Lean.Lsp.CallHierarchyItem
-- Lean.Meta.Transform
_private.Lean.Meta.Transform.0.Lean.Meta.transformWithCache.visit.visitPost : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] →
      [MonadControlT Lean.MetaM m] →
        (Lean.Expr → m Lean.TransformStep) →
          (Lean.Expr → m Lean.TransformStep) →
            Bool →
              Bool →
                Bool →
                  (x : STWorld IO.RealWorld m) →
                    MonadLiftT (ST IO.RealWorld) m →
                      Lean.Expr → Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mem_support : ∀ {V : Type u} (G : SimpleGraph V) {v : V}, v ∈ G.support ↔ ∃ w, G.Adj v w
-- Mathlib.CategoryTheory.Limits.Cones
/-- Cocones on `F : J ⥤ C` are equivalent to cones on `F.op : Jᵒᵖ ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.coconeOpEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → (CategoryTheory.Limits.Cocone F)ᵒᵖ ≌ CategoryTheory.Limits.Cone F.op
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.coe_ofClass : ∀ {S : Type u_3} {M : Type u_4} [inst : AddMonoid M] [inst_1 : SetLike S M] [inst_2 : AddSubmonoidClass S M] (s : S),
  ↑(AddSubmonoid.ofClass s) = ↑s
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- The product functor given by the instance `HasBinaryProducts (Type u)` is isomorphic to the
explicit binary product functor given by the product type.
 -/
CategoryTheory.Limits.Types.binaryProductIsoProd : CategoryTheory.Limits.Types.binaryProductFunctor ≅ CategoryTheory.Limits.prod.functor
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.add_left_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {T : Set α → β}
  [inst : AddMonoid β] {ν : MeasureTheory.Measure α},
  MeasureTheory.FinMeasAdditive μ T → MeasureTheory.FinMeasAdditive (ν + μ) T