mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyMap'_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.LeftHomologyData)
  (h₂ : S₂.LeftHomologyData) (h₃ : S₃.LeftHomologyData) {Z : C} (h : h₃.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ₁ h₁ h₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ₂ h₂ h₃) h)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.isScalarTower_right : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {α : Type u_1} {β : Type u_2} [inst_3 : SMul α R] [inst_4 : SMul α A] [inst_5 : IsScalarTower α R A]
  [inst_6 : SMul β R] [inst_7 : SMul β A] [inst_8 : IsScalarTower β R A] [inst_9 : SMul α β] [IsScalarTower α β A],
  IsScalarTower α β ↥S
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- See Note [custom simps projection]  -/
NonUnitalAlgHom.Simps.apply : {R : Type u} →
  {S : Type u₁} →
    [inst : Monoid R] →
      [inst_1 : Monoid S] →
        (φ : R →* S) →
          (A : Type v) →
            (B : Type w) →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [inst_3 : DistribMulAction R A] →
                  [inst_4 : NonUnitalNonAssocSemiring B] → [inst_5 : DistribMulAction S B] → (A →ₛₙₐ[φ] B) → A → B
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.hasNestedAction : Lean.Syntax → Bool
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.of.inj : ∀ {J : Type v} {inst : CategoryTheory.SmallCategory J} {F : CategoryTheory.Functor J RingCat} {j : J} {x : ↑(F.obj j)}
  {j_1 : J} {x_1 : ↑(F.obj j_1)},
  RingCat.Colimits.Prequotient.of j x = RingCat.Colimits.Prequotient.of j_1 x_1 → j = j_1 ∧ x ≍ x_1
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.delta_mul_eq_smul_delta : ∀ {f : ℕ → ℂ}, LSeries.delta * f = f 1 • LSeries.delta
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform.0.EisensteinSeries.G2_S_action_eq_tsum_G2Term : ∀ (z : UpperHalfPlane),
  (↑z ^ 2)⁻¹ * EisensteinSeries.G2 (ModularGroup.S • z) - -2 * ↑Real.pi * Complex.I / ↑z =
    ∑' (n : ℤ) (m : ℤ), EisensteinSeries.G2Term✝ z ![m, n]
-- Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms
SSet.instIsStableUnderCobaseChangeMonomorphisms : (CategoryTheory.MorphismProperty.monomorphisms SSet).IsStableUnderCobaseChange
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_eq_cons : ∀ {m n : ℤ}, m < n → (m<...=n).toList = (m + 1) :: ((m + 1)<...=n).toList
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k k' : α} {f : Option β → Option β},
  (t.alter k f).getKey! k' =
    if cmp k k' = Ordering.eq then if (f t[k]?).isSome = true then k else default else t.getKey! k'
-- Init.Data.Option.Attach
Option.attachWith_congr : ∀ {α : Type u_1} {o₁ o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ (x : α), o₁ = some x → P x},
  o₁.attachWith P H = o₂.attachWith P ⋯
-- Lean.Elab.Tactic.Basic
/-- Auxiliary datastructure for capturing exceptions at `evalTactic`.
 -/
Lean.Elab.Tactic.EvalTacticFailure : Type
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
/-- A reduced irreducible finite crystallographic root system has roots of at most two different
lengths.  -/
RootPairing.InvariantForm.exists_apply_eq_or : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} [Finite ι]
  [CharZero R] [P.IsCrystallographic] [IsDomain R] [P.IsReduced] (B : P.InvariantForm) [P.IsIrreducible] [Nonempty ι],
  ∃ i j,
    ∀ (k : ι),
      (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
        (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.minEntry.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (x_1 : x.isEmpty = false) →
          ((size : ℕ) →
              (k : α) →
                (v : β) →
                  (r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    (x :
                        (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
                      motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (size_1 : ℕ) →
                      (k_1 : α) →
                        (v_1 : β) →
                          (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                            (h :
                                (Std.DTreeMap.Internal.Impl.inner size k v
                                      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
                                  false) →
                              motive
                                (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
                                h) →
              motive x x_1
-- Mathlib.Combinatorics.Matroid.Dual
/-- The `✶` symbol, which denotes matroid duality.
(This is distinct from the usual `*` symbol for multiplication, due to precedence issues.)  -/
Matroid.«term_✶» : Lean.TrailingParserDescr
-- Init.Data.SInt.Lemmas
Int64.toBitVec_ofIntLE : ∀ (x : ℤ) (h₁ : Int64.minValue.toInt ≤ x) (h₂ : x ≤ Int64.maxValue.toInt),
  (Int64.ofIntLE x h₁ h₂).toBitVec = BitVec.ofInt 64 x
-- Mathlib.Topology.AlexandrovDiscrete
nhdsSet_basis_nhdsKer : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] (s : Set α),
  (nhdsSet s).HasBasis (fun x => True) fun x => nhdsKer s
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.Monic.neg_one_pow_natDegree_mul_comp_neg_X : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R}, p.Monic → ((-1) ^ p.natDegree * p.comp (-Polynomial.X)).Monic
-- Mathlib.FieldTheory.Finite.Basic
ZMod.instSubsingletonSubfield : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], Subsingleton (Subfield (ZMod p))
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.pi_refl : ∀ {ι : Type u_5} {αi : ι → Type u_6},
  (PartialEquiv.pi fun i => PartialEquiv.refl (αi i)) = PartialEquiv.refl ((i : ι) → αi i)
-- Aesop.Forward.State
/-- Get the `InstMap` associated with a variable, or an empty `InstMap`.  -/
Aesop.VariableMap.find : Aesop.VariableMap → Aesop.PremiseIndex → Aesop.InstMap
-- Lean.Parser.Types
Lean.Parser.SyntaxStack.isEmpty : Lean.Parser.SyntaxStack → Bool
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.FG.sup : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N₁ N₂ : Submodule R M}, N₁.FG → N₂.FG → (N₁ ⊔ N₂).FG
-- Init.Data.UInt.Lemmas
USize.ofNatClamp_finVal : ∀ (n : Fin USize.size), USize.ofNatClamp ↑n = USize.ofFin n
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.supp_subset_range_natDegree_succ : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.support ⊆ Finset.range (p.natDegree + 1)
-- Batteries.Tactic.Lint.Simp
Batteries.Tactic.Lint.SimpTheoremInfo.mk : Array Lean.Expr → Lean.Expr → Lean.Expr → Batteries.Tactic.Lint.SimpTheoremInfo
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_le_rpow : ∀ {x y : NNReal} {z : ℝ}, x ≤ y → 0 ≤ z → x ^ z ≤ y ^ z
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine S],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).inv
      (AlgebraicGeometry.AffineSpace n S ↘ S) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom MvPolynomial.C)) S.isoSpec.inv
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.sub : ∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : StarAddMonoid R] {x y : R},
  IsSelfAdjoint x → IsSelfAdjoint y → IsSelfAdjoint (x - y)
-- Mathlib.Order.InitialSeg
/-- Initial segment embedding of an order `r` into the disjoint union of `r` and `s`.  -/
InitialSeg.leAdd : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → InitialSeg r (Sum.Lex r s)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.length_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → (Std.DHashMap.Raw.Const.toList m).length = m.size
-- Mathlib.Order.Lattice
AntitoneOn.of_map_sup : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α} [inst : SemilatticeSup α] [inst_1 : SemilatticeInf β],
  (∀ x ∈ s, ∀ y ∈ s, f (x ⊔ y) = f x ⊓ f y) → AntitoneOn f s
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.instIsIsoμ : ∀ {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) [inst_4 : F.Monoidal] (X Y : C),
  CategoryTheory.IsIso (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_comp_succ_succAbove : ∀ {n : ℕ} {β : Sort u_2} (x : β) (p : Fin (n + 1) → β) (i : Fin (n + 1)),
  Fin.cons x p ∘ i.succ.succAbove = Fin.cons x (i.removeNth p)
-- Mathlib.Order.WithBot
WithBot.instUniqueOfIsEmpty.eq_1 : ∀ {α : Type u_1} [inst : IsEmpty α], WithBot.instUniqueOfIsEmpty = { toInhabited := WithBot.inhabited, uniq := ⋯ }
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.inv_eq : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K}, I⁻¹ = 1 / I
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∉ t₂ → k ∉ t₁ ∩ t₂
-- Mathlib.CategoryTheory.Localization.Resolution
/-- an object in the source category  -/
CategoryTheory.LocalizerMorphism.LeftResolution.X₁ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} → {X₂ : C₂} → Φ.LeftResolution X₂ → C₁
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_add : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ ν : MeasureTheory.Measure α)
  {f : α → β},
  Measurable f → MeasureTheory.Measure.map f (μ + ν) = MeasureTheory.Measure.map f μ + MeasureTheory.Measure.map f ν
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- **Alias** of `CoxeterMatrix.A`.

---

The Coxeter matrix of type Aₙ.

The corresponding Coxeter-Dynkin diagram is:
```
    o --- o --- o ⬝ ⬝ ⬝ ⬝ o --- o
```
 -/
CoxeterMatrix.Aₙ : (n : ℕ) → CoxeterMatrix (Fin n)
-- Mathlib.RingTheory.Ideal.Operations
Submodule.mem_of_span_top_of_smul_mem : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (M' : Submodule R M)
  (s : Set R), Ideal.span s = ⊤ → ∀ (x : M), (∀ (r : ↑s), ↑r • x ∈ M') → x ∈ M'
-- Init.Data.String.Basic
String.Slice.Pos.byte.congr_simp : ∀ {s : String.Slice} (pos pos_1 : s.Pos) (e_pos : pos = pos_1) (h : pos ≠ s.endPos), pos.byte h = pos_1.byte ⋯
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousComponent_apply : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (n : ℕ) (φ : MvPolynomial σ R),
  (MvPolynomial.homogeneousComponent n) φ =
    ∑ d ∈ φ.support with Finsupp.degree d = n, (MvPolynomial.monomial d) (MvPolynomial.coeff d φ)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- Given a semilinear map `M ⊗ N → P`, compose it with the canonical bilinear map
`M → N → M ⊗ N` to form a bilinear map `M → N → P`.  -/
TensorProduct.lcurry : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring R₂] →
        (σ₁₂ : R →+* R₂) →
          (M : Type u_7) →
            (N : Type u_8) →
              (P₂ : Type u_17) →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid N] →
                    [inst_4 : AddCommMonoid P₂] →
                      [inst_5 : Module R M] →
                        [inst_6 : Module R N] →
                          [inst_7 : Module R₂ P₂] → (TensorProduct R M N →ₛₗ[σ₁₂] P₂) →ₗ[R₂] M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
-- Mathlib.Data.Rel
/-- A shorthand for `α → β → Prop`.

Consider using `SetRel` instead if you want extra API for relations.  -/
Rel : Type u_6 → Type u_7 → Type (max u_6 u_7)
-- Init.Internal.Order.Basic
Lean.Order.lfp_monotone : {α : Sort u} → [inst : Lean.Order.CompleteLattice α] → (f : α → α) → Lean.Order.monotone f → α
-- Mathlib.Order.CompleteLattice.Lemmas
iInf_sup_le_iInf_sup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (f : ι → α) (a : α), (⨅ i, f i) ⊔ a ≤ ⨅ i, f i ⊔ a
-- Mathlib.Logic.Small.Defs
small_ulift : ∀ (α : Type u) [Small.{v, u} α], Small.{v, max w u} (ULift.{w, u} α)
-- Mathlib.NumberTheory.Chebyshev
/-- Chebyshev's bound `ψ x ≤ c x` with an explicit constant.
Note that `Chebyshev.psi_le` gives a sharper bound with a better main term.  -/
Chebyshev.psi_le_const_mul_self : ∀ {x : ℝ}, 0 ≤ x → Chebyshev.psi x ≤ (Real.log 4 + 4) * x
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext.getValue : Lean.IR.LocalContext → Lean.IR.VarId → Option Lean.IR.Expr
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.glue!.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (r : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((sz' : ℕ) →
              (k' : α) →
                (v' : β k') →
                  (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')) →
            motive r
-- Init.Data.UInt.Lemmas
USize.toBitVec_ofNatClamp_of_le : ∀ {n : ℕ}, USize.size ≤ n → (USize.ofNatClamp n).toBitVec = (USize.size - 1)#'USize.toBitVec_ofNatClamp_of_le._proof_1
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_le_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E}
  {T : IntermediateField F E}, IntermediateField.adjoin F S ≤ T ↔ S ⊆ ↑T
-- Mathlib.Analysis.Normed.Group.Bounded
HasCompactSupport.exists_pos_le_norm : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddGroup α] {f : α → E} [inst_1 : Zero E],
  HasCompactSupport f → ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_of_Y_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 ≠ Q 1 * P 2 → W.add P Q = WeierstrassCurve.Projective.addU P Q • ![0, 1, 0]
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotient_map_mkₐ : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Ring B] [inst_4 : Algebra R₁ B] {I : Ideal A} (J : Ideal B) [inst_5 : I.IsTwoSided] [inst_6 : J.IsTwoSided]
  (f : A →ₐ[R₁] B) (H : I ≤ Ideal.comap f J) {x : A},
  (Ideal.quotientMapₐ J f H) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mkₐ R₁ J) (f x)
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.biSup_comap_eq_top_of_range_eq_biSup : ∀ {M : Type u_4} {M₂ : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] {R : Type u_8} {R₂ : Type u_9}
  [inst_2 : Semiring R] [inst_3 : Ring R₂] {τ₁₂ : R →+* R₂} [inst_4 : RingHomSurjective τ₁₂] [inst_5 : Module R M]
  [inst_6 : Module R₂ M₂] {ι : Type u_10} (s : Set ι),
  s.Nonempty →
    ∀ (p : ι → Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂), f.range = ⨆ i ∈ s, p i → ⨆ i ∈ s, Submodule.comap f (p i) = ⊤
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_comm_apply : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) (g : G)
  (a : ↑A), (Rep.Hom.hom f) ((A.ρ g) a) = (B.ρ g) ((Rep.Hom.hom f) a)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The canonical compatibility square between (the object components of)
`transform` and `precompose`.
This is a "naturality square" if we think as `precompose` as the
(app component of the) map component of a pseudofunctor from the opposite
bicategory of categories to pseudofunctors of categorical cospans
(its value on `X` being the pseudofunctor `transform X _`).  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {A₁ : Type u₄} →
                  {B₁ : Type u₅} →
                    {C₁ : Type u₆} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] →
                            {F₁ : CategoryTheory.Functor A₁ B₁} →
                              {G₁ : CategoryTheory.Functor C₁ B₁} →
                                {X : Type u₇} →
                                  {Y : Type u₈} →
                                    [inst_6 : CategoryTheory.Category.{v₇, u₇} X] →
                                      [inst_7 : CategoryTheory.Category.{v₈, u₈} Y] →
                                        (U : CategoryTheory.Functor X Y) →
                                          (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) →
                                            CategoryTheory.CatCommSq
                                              ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj
                                                ψ)
                                              ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F
                                                    G).obj
                                                U)
                                              ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁
                                                    G₁).obj
                                                U)
                                              ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj
                                                ψ)
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_lt_div_right : ∀ {a b c : ENNReal}, c ≠ 0 → c ≠ ⊤ → a < b → a / c < b / c
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.le_powerlt : ∀ {b c : Cardinal.{u}} (a : Cardinal.{u}), c < b → a ^ c ≤ a ^< b
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instSMulCommClass : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] {S : Type u_3}
  [inst_5 : Monoid S] [inst_6 : DistribMulAction S A] [inst_7 : SMulCommClass 𝕜 S A] [inst_8 : ContinuousConstSMul S A]
  [inst_9 : IsScalarTower S A A] [inst_10 : SMulCommClass S A A] {T : Type u_4} [inst_11 : Monoid T]
  [inst_12 : DistribMulAction T A] [inst_13 : SMulCommClass 𝕜 T A] [inst_14 : ContinuousConstSMul T A]
  [inst_15 : IsScalarTower T A A] [inst_16 : SMulCommClass T A A] [SMulCommClass S T A],
  SMulCommClass S T (DoubleCentralizer 𝕜 A)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.modByMonicHom_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f), 1 < f.natDegree → h.modByMonicHom h.root = Polynomial.X
-- Init.Data.Range.Polymorphic.RangeIterator
/-- Internal state of the range iterators. Do not depend on its internals.  -/
Std.Rxc.Iterator : Type u → Type u
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
intervalIntegral.continuousOn_primitive_interval : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  {f : ℝ → E} [MeasureTheory.NullSingletonClass μ],
  MeasureTheory.IntegrableOn f (Set.uIcc a b) μ → ContinuousOn (fun x => ∫ (t : ℝ) in a..x, f t ∂μ) (Set.uIcc a b)
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_le_tight_cert : ℤ → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso_hom_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C)
  (X_1 : SimplexCategoryᵒᵖ),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompDropIso.hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.id
      (X.obj
        (match CategoryTheory.WithTerminal.incl.obj X_1 with
        | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
        | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star))
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.naturality_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.OplaxTrans F G) {a b : B} {f g : a ⟶ b}
  (η : f ⟶ g) {Z : F.obj a ⟶ G.obj b} (h : CategoryTheory.CategoryStruct.comp (self.app a) (G.map g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b))
      (CategoryTheory.CategoryStruct.comp (self.naturality g) h) =
    CategoryTheory.CategoryStruct.comp (self.naturality f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η)) h)
-- Mathlib.Data.PEquiv
PEquiv.symm_trans_rev : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ), (f.trans g).symm = g.symm.trans f.symm
-- Mathlib.Topology.Order.LeftRightNhds
mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a u' : α} {s : Set α},
  a < u' → (s ∈ nhdsWithin a (Set.Ici a) ↔ ∃ u ∈ Set.Ioc a u', Set.Ico a u ⊆ s)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrableOn_const_enorm : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {μ : MeasureTheory.Measure X} {s : Set X} [MeasureTheory.IsLocallyFiniteMeasure μ]
  {c : ε}, ‖c‖ₑ ≠ ⊤ → MeasureTheory.LocallyIntegrableOn (fun x => c) s μ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α}
  {h : k ∈ Std.ExtHashMap.unitOfList l}, (Std.ExtHashMap.unitOfList l)[k] = ()