mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.Schur
CategoryTheory.finrank_hom_simple_simple : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (𝕜 : Type u_2)
  [inst_2 : Field 𝕜] [IsAlgClosed 𝕜] [inst_4 : CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X Y : C)
  [∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y],
  Module.finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.toEquiv_injective : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β], Function.Injective UniformEquiv.toEquiv
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.addSplitCandidatesForExt.found : Lean.Expr → ℕ → Lean.Expr → ℕ → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_eq_false_iff_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {k : α},
  t.contains k = false ↔ k ∉ t
-- Mathlib.RingTheory.TensorProduct.Finite
instNontrivialTensorProduct : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  [Nontrivial M], Nontrivial (TensorProduct R M M)
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.range_pullbackSnd : ∀ {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_le_size_insertMany : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} {ρ : Type w}
  [inst_2 : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : ρ}, m.size ≤ (Std.DHashMap.Raw.Const.insertMany m l).size
-- Mathlib.Algebra.Opposites
AddOpposite.opEquiv.eq_1 : ∀ {α : Type u_1},
  AddOpposite.opEquiv = { toFun := AddOpposite.op, invFun := AddOpposite.unop, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.GroupTheory.PGroup
/-- The quotient by the center of a group of cardinality `p ^ 2` is cyclic.  -/
IsPGroup.cyclic_center_quotient_of_card_eq_prime_sq : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)], Nat.card G = p ^ 2 → IsCyclic (G ⧸ Subgroup.center G)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.instInfSet : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → InfSet hI.SubDPIdeal
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- Translates of a block form a block system  -/
MulAction.IsBlock.isBlockSystem : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X}
  [hGX : MulAction.IsPretransitive G X],
  MulAction.IsBlock G B → B.Nonempty → MulAction.IsBlockSystem G (Set.range fun g => g • B)
-- Mathlib.GroupTheory.Finiteness
AddGroup.fg_of_group_fg : ∀ {G : Type u_3} [inst : Group G] [Group.FG G], AddGroup.FG (Additive G)
-- Init.Data.UInt.Lemmas
UInt64.ofFin_mk : ∀ {n : ℕ} (hn : n < UInt64.size), UInt64.ofFin ⟨n, hn⟩ = UInt64.ofNatLT n hn
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.norm_int : ∀ (ctx : Lean.Grind.CommRing.Context ℤ) (e : Lean.Grind.CommRing.Expr) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.norm_int_cert e p = true →
    Lean.Grind.CommRing.Expr.denote ctx e = Lean.Grind.CommRing.Poly.denote' ctx p
-- Aesop.Stats.Report
/-- Assumes that `xs` is ascending. We use a simple nearest-rank definition of
percentiles.  -/
Aesop.sortedPercentileD : {α : Type u_1} → Aesop.Percent → α → Array α → α
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.linearIndependentInt : ∀ {ι : 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} (b : P.Base)
  [CharZero R], LinearIndependent ℤ fun i => P.rootSpanMem ℤ ↑i
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, List.find? (fun x_2 => x_2.fst == k) m.toList = none ↔ m.contains k = false
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
/-- If `f` is interval integrable on `a..(b + c)` where `a ≤ b` and `0 ≤ c`, then
`fun x ↦ slope f x (x + c)` is interval integrable on `a..b`.  -/
IntervalIntegrable.intervalIntegrable_slope : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  IntervalIntegrable f MeasureTheory.volume a (b + c) →
    a ≤ b → 0 ≤ c → IntervalIntegrable (fun x => slope f x (x + c)) MeasureTheory.volume a b
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Eta-expanded form of `MeasureTheory.AEStronglyMeasurable.sup` -/
MeasureTheory.AEStronglyMeasurable.fun_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : SemilatticeSup β] [ContinuousSup β],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun i => f i ⊔ g i) μ
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mem_biUnionIndex : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J}, J ∈ π.biUnion πi → J ∈ πi (π.biUnionIndex πi J)
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_one_div_of_pos : ∀ {a b : ℝ}, 0 < a → 0 < b → ∫ (x : ℝ) in a..b, 1 / x = Real.log (b / a)
-- Lean.Util.SCC
_private.Lean.Util.SCC.0.Lean.SCC.addSCC : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → α → Lean.SCC.M α Unit
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
/-- Extract the equation from a 2-morphism in a locally discrete 2-category.  -/
CategoryTheory.LocallyDiscrete.eq_of_hom : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {X Y : CategoryTheory.LocallyDiscrete C} {f g : X ⟶ Y}
  (η : f ⟶ g), f = g
-- Init.Data.Sum.Lemmas
Sum.inr_getRight : ∀ {α : Type u_1} {β : Type u_2} (x : α ⊕ β) (h : x.isRight = true), Sum.inr (x.getRight h) = x
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instNonUnitalNonAssocRing : {R : Type u_1} → [NonUnitalNonAssocRing R] → NonUnitalNonAssocRing Rᵐᵒᵖ
-- Init.Data.String.Basic
String.Pos.Raw.offsetOfPosAux : String → String.Pos.Raw → String.Pos.Raw → ℕ → ℕ
-- Mathlib.RingTheory.Etale.StandardEtale
Algebra.SubmersivePresentation.mk.congr_simp : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Finite σ]
  (toPreSubmersivePresentation toPreSubmersivePresentation_1 : Algebra.PreSubmersivePresentation R S ι σ)
  (e_toPreSubmersivePresentation : toPreSubmersivePresentation = toPreSubmersivePresentation_1)
  (jacobian_isUnit : IsUnit toPreSubmersivePresentation.jacobian),
  { toPreSubmersivePresentation := toPreSubmersivePresentation, jacobian_isUnit := jacobian_isUnit } =
    { toPreSubmersivePresentation := toPreSubmersivePresentation_1, jacobian_isUnit := ⋯ }
-- Mathlib.Algebra.Group.Pi.Basic
Pi.instSubtractionCommMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → SubtractionCommMonoid (f i)],
  Pi.instSubtractionCommMonoid = { toSubtractionMonoid := Pi.subtractionMonoid, add_comm := ⋯ }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.any_keys : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulHashable α]
  [EquivBEq α] {p : α → Bool}, m.WF → m.keys.any p = m.any fun a x => p a
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.instCanLiftSetCoeIsClosed : ∀ {α : Type u_2} [inst : TopologicalSpace α], CanLift (Set α) (TopologicalSpace.Closeds α) SetLike.coe IsClosed
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.cosimplicialToSimplicialAugmented_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ),
  (CategoryTheory.cosimplicialToSimplicialAugmented C).obj X = Opposite.op X.leftOp
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.adj_counit : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  GeneratedByTopCat.adj.counit = GeneratedByTopCat.adjCounit
-- Mathlib.Algebra.Notation.Prod
Prod.mk_div_mk : ∀ {G : Type u_8} {H : Type u_9} [inst : Div G] [inst_1 : Div H] (x₁ x₂ : G) (y₁ y₂ : H),
  (x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induceUnivIso_apply : ∀ {V : Type u_1} (G : SimpleGraph V) (self : { x // x ∈ Set.univ }), G.induceUnivIso self = ↑self
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
/-- (Implementation) The isomorphism that proves that `A` preserves finite limits.  -/
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso : {C : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteColimits C] →
      (A : CategoryTheory.Functor Cᵒᵖ (Type u)) →
        {J : Type} →
          [inst_2 : CategoryTheory.SmallCategory J] →
            [inst_3 : CategoryTheory.FinCategory J] →
              (K : CategoryTheory.Functor J Cᵒᵖ) →
                [CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)] →
                  A.obj (CategoryTheory.Limits.limit K) ≅ CategoryTheory.Limits.limit (K.comp A)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.add_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  {D1 D2 : Derivation R A M} (a : A), (D1 + D2) a = D1 a + D2 a
-- Mathlib.GroupTheory.Congruence.Defs
ConGen.Rel.of : ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} (x y : M), r x y → ConGen.Rel r x y
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.vle_trans'`. -/
ValuativeRel.vle.trans' : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, y ≤ᵥ z → x ≤ᵥ y → x ≤ᵥ z
-- Mathlib.Algebra.Algebra.Pi
AlgEquiv.piCongrRight_refl : ∀ {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A₁ i)]
  [inst_2 : (i : ι) → Algebra R (A₁ i)], (AlgEquiv.piCongrRight fun i => AlgEquiv.refl) = AlgEquiv.refl
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instInhabited.eq_1 : ∀ {α : Type u}, FreeAddGroup.instInhabited = { default := 0 }
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.dvd_div_of_mul_dvd : ∀ {R : Type u} [inst : EuclideanDomain R] {a b c : R}, a * b ∣ c → b ∣ c / a
-- Mathlib.Order.Filter.Pointwise
Filter.vaddCommClass : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α γ] [inst_1 : VAdd β γ] [VAddCommClass α β γ],
  VAddCommClass (Filter α) (Filter β) (Filter γ)
-- Init.Data.List.Find
List.isNone_idxOf? : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α}, ((List.idxOf? a l).isNone = true) = (a ∉ l)
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.τ_symm_apply_infinity : ∀ {A B : GrpCat} (f : A ⟶ B),
  (Equiv.symm (GrpCat.SurjectiveOfEpiAuxs.tau f)) GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity =
    GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(GrpCat.Hom.hom f).range, ⋯⟩
-- Mathlib.FieldTheory.Galois.Basic
/-- A field extension E/F is Galois if it is both separable and normal. Note that in mathlib
a separable extension of fields is by definition algebraic.  -/
IsGalois : (F : Type u_1) → [inst : Field F] → (E : Type u_2) → [inst_1 : Field E] → [Algebra F E] → Prop
-- Mathlib.Dynamics.Transitive
/-- An action of an additive monoid `M` on `α` is topologically transitive if and only
if for any nonempty open subset `U` of `α` the union of the preimages of `U` over the elements of
`M` is dense in `α`.  -/
AddAction.isTopologicallyTransitive_iff_dense_iUnion_preimage : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddMonoid M] [inst_2 : AddAction M α],
  AddAction.IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense (⋃ m, (fun x => m +ᵥ x) ⁻¹' U)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.Characteristic.mk : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G},
  (∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H = H) → H.Characteristic
-- Mathlib.Data.Num.Basic
/-- The number of bits required to represent a `Num`, as a `Nat`. `size 0` is defined to be `0`.  -/
Num.natSize : Num → ℕ
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
/-- The morphism `(karoubi.π' Λ).app X` is a retract of `(toKaroubi _).map (Λ.π.app X)`.  -/
CategoryTheory.Abelian.LeftResolution.karoubi.retractArrow : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          (Λ : CategoryTheory.Abelian.LeftResolution ι) →
            [inst_2 : CategoryTheory.Preadditive C] →
              [inst_3 : CategoryTheory.Preadditive A] →
                [inst_4 : ι.Additive] →
                  (X : A) →
                    CategoryTheory.RetractArrow ((CategoryTheory.Abelian.LeftResolution.karoubi.π' Λ).app X)
                      ((CategoryTheory.Idempotents.toKaroubi A).map (Λ.π.app X))
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_inter_distrib_right`. -/
Set.diff_inter_distrib_right : ∀ {α : Type u_1} (s t r : Set α), (t ∩ r) \ s = t \ s ∩ (r \ s)
-- Mathlib.Analysis.Complex.Conformal
/-- The **Cauchy-Riemann Equation**: A real-differentiable function `f` on `ℂ` is complex-differentiable
at `x` if and only if the derivative `fderiv ℝ f x` maps `I` to `I • (fderiv ℝ f x) 1`.
 -/
differentiableAt_complex_iff_differentiableAt_real : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ},
  DifferentiableAt ℂ f x ↔ DifferentiableAt ℝ f x ∧ (fderiv ℝ f x) Complex.I = Complex.I • (fderiv ℝ f x) 1
-- Mathlib.Logic.Basic
exists_mem_of_exists : ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (x : α), p x) → (∃ x, q x) → ∃ x, ∃ (_ : p x), q x
-- Init.System.IOError
IO.Error.noSuchThing.sizeOf_spec : ∀ (filename : Option String) (osCode : UInt32) (details : String),
  sizeOf (IO.Error.noSuchThing filename osCode details) = 1 + sizeOf filename + sizeOf osCode + sizeOf details
-- Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
_private.Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ.0.WeierstrassCurve.exists_variableChange_of_char_two_of_j_eq_zero : ∀ {F : Type u_1} [inst : Field F] [IsSepClosed F] (E E' : WeierstrassCurve F) [E.IsElliptic] [E'.IsElliptic] [CharP F 2]
  [E.IsCharTwoJEqZeroNF] [E'.IsCharTwoJEqZeroNF], ∃ C, C • E = E'
-- Init.Data.UInt.Bitwise
UInt32.toUSize_shiftRight : ∀ (a b : UInt32), (a >>> b).toUSize = a.toUSize >>> (b.toUSize % 32)
-- Lean.Syntax
Lean.SourceInfo.getRange? : optParam Bool false → Lean.SourceInfo → Option Lean.Syntax.Range
-- Mathlib.Algebra.Module.Submodule.Map
/-- A linear isomorphism induces an order isomorphism of submodules.  -/
Submodule.orderIsoMapComap : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} →
                      [RingHomSurjective σ₁₂] →
                        {σ₂₁ : R₂ →+* R} →
                          [inst_7 : RingHomInvPair σ₁₂ σ₂₁] →
                            [inst_8 : RingHomInvPair σ₂₁ σ₁₂] → (M ≃ₛₗ[σ₁₂] M₂) → Submodule R M ≃o Submodule R₂ M₂
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- A subsemigroup is isomorphic to its image under an injective function  -/
Subsemigroup.equivMapOfInjective : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Mul M] →
      [inst_1 : Mul N] → (S : Subsemigroup M) → (f : M →ₙ* N) → Function.Injective ⇑f → ↥S ≃* ↥(Subsemigroup.map f S)
-- Mathlib.Data.Num.Lemmas
Num.isStrictOrderedRing : IsStrictOrderedRing Num
-- Std.Tactic.BVDecide.LRAT.Parser
/-- Based on the first byte parses the input either as a binary or non-binary LRAT.
 -/
Std.Tactic.BVDecide.LRAT.Parser.parseActions : Std.Internal.Parsec.ByteArray.Parser (Array Std.Tactic.BVDecide.LRAT.IntAction)
-- Mathlib.Order.Lattice
AntitoneOn.of_map_inf : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α} [inst : SemilatticeInf α] [inst_1 : SemilatticeSup β],
  (∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊔ f y) → AntitoneOn f s
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.lift_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (f : F' ⟶ F)
  {G : CategoryTheory.Subfunctor F} (hf : CategoryTheory.Subfunctor.range f ≤ G) {Z : CategoryTheory.Functor C (Type w)}
  (h : F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.lift f hf) (CategoryTheory.CategoryStruct.comp G.ι h) =
    CategoryTheory.CategoryStruct.comp f h
-- Init.Data.Array.Lemmas
Array.getElem_push : ∀ {α : Type u_1} {xs : Array α} {x : α} {i : ℕ} (h : i < (xs.push x).size),
  (xs.push x)[i] = if h : i < xs.size then xs[i] else x
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_map_sectL : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (a b : α) (c : β),
  Finset.map (Function.Embedding.sectL α c) (Finset.uIcc a b) = Finset.uIcc (a, c) (b, c)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- Given `K ∈ ℝ` and a finite `S ⊆ G`, a fragment of `G` with respect to `K` and `S` is a finite
nonempty `A ⊆ G` whose expansion attains the value of the connectivity, that is,
`expansion K S A = κ`.  -/
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.IsFragment : {G : Type u_1} → [Group G] → [DecidableEq G] → ℝ → Finset G → Finset G → Prop
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
/-- Given a linear map `f` between two vector spaces with the same dimension, if
`ker f = ⊥` then `linearEquivOfInjective` is the induced isomorphism
between the two vector spaces.  -/
LinearMap.linearEquivOfInjective : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {V₂ : Type v'} →
            [inst_3 : AddCommGroup V₂] →
              [inst_4 : Module K V₂] →
                [FiniteDimensional K V] →
                  [FiniteDimensional K V₂] →
                    (f : V →ₗ[K] V₂) → Function.Injective ⇑f → Module.finrank K V = Module.finrank K V₂ → V ≃ₗ[K] V₂
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.coe_subtype : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : AffineSubspace k P) [inst_4 : Nonempty ↥s], ⇑s.subtype = Subtype.val
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'_zero_add_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A) (X : C),
  (CategoryTheory.shiftFunctorAdd' C 0 a a ⋯).inv.app X =
    (CategoryTheory.shiftFunctor C a).map ((CategoryTheory.shiftFunctorZero C A).hom.app X)
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.coe_pow : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mem_incidence_iff_neighbor : ∀ {V : Type u} (G : SimpleGraph V) {v w : V}, s(v, w) ∈ G.incidenceSet v ↔ w ∈ G.neighborSet v
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.VectorsProdEqOne.vectorEquiv_apply_coe : ∀ (G : Type u_2) [inst : Group G] (n : ℕ) (v : List.Vector G n),
  ↑((Equiv.Perm.VectorsProdEqOne.vectorEquiv G n) v) = v.toList.prod⁻¹ ::ᵥ v
-- Init.Data.Array.Lemmas
Array.foldr_push_eq_append : ∀ {α : Type u_1} {β : Type u_2} {start : ℕ} {as : Array α} {bs : Array β} {f : α → β},
  start = as.size → Array.foldr (fun a xs => xs.push (f a)) bs as start = bs ++ (Array.map f as).reverse
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.beq_eq_beqModel : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [inst : BEq α] [Std.TransOrd α] [inst_2 : LawfulBEq α]
  [inst_3 : Std.LawfulBEqOrd α] [inst_4 : (k : α) → BEq (β k)] {m₁ m₂ : Std.DTreeMap.Internal.Impl α β},
  m₁.WF → m₂.WF → m₁.beq m₂ = Std.Internal.List.beqModel m₁.toListModel m₂.toListModel
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid of a monoid `M` is a subset containing 1 and closed under multiplication.  -/
Submonoid : (M : Type u_3) → [MulOneClass M] → Type u_3
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_congr : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  (∀ (a : α), f a = g a) → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
-- Std.Http.Data.Method
/-- Apply a label to a version history.
Source: https://www.rfc-editor.org/rfc/rfc3253#section-8.2
 -/
Std.Http.Method.label : Std.Http.Method
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.isTangentAt_insphere_touchpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.insphere.IsTangentAt (s.touchpoint ∅ i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth.eq_1 : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j))
  (j : Fin (n + 1)), i.insertNth x p j = i.succAboveCases x p j
-- Mathlib.Data.PFun
PFun.preimage_subset_core : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β), f.preimage s ⊆ f.core s
-- Mathlib.Algebra.Ring.Basic
AddMonoid.End.mulRight_eq_mulLeft : ∀ {R : Type u_1} [inst : NonUnitalNonAssocCommSemiring R], AddMonoid.End.mulRight = AddMonoid.End.mulLeft
-- Lean.Elab.Term.TermElabM
/-- Given a free variable `fvar`, return its declaration.
This function panics if `fvar` is not a free variable.
 -/
Lean.Elab.Term.getFVarLocalDecl! : Lean.Expr → Lean.Elab.TermElabM Lean.LocalDecl
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.d₀₁_eq_zero : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G) [A.IsTrivial],
  groupCohomology.d₀₁ A = 0
-- Init.Data.Order.PackageFactories
/-- This class entails `LE α`, `LT α` and `BEq α` instances as well as proofs that these operations
represent the same partial order structure on `α`.
 -/
Std.PartialOrderPackage : Type u → Type u
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral norm is a `K`-algebra norm on `L` when `L/K` is finite and normal.
See also `spectralAlgNorm` for a more general construction.  -/
spectralAlgNorm_of_finiteDimensional_normal : (K : Type u_2) →
  [inst : NormedField K] →
    (L : Type u_3) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [h_fin : FiniteDimensional K L] → [hn : Normal K L] → [IsUltrametricDist K] → AlgebraNorm K L
-- Init.Data.List.Basic
List.beq.eq_3 : ∀ {α : Type u} [inst : BEq α] (x x_1 : List α),
  (x = [] → x_1 = [] → False) →
    (∀ (a : α) (as : List α) (b : α) (bs : List α), x = a :: as → x_1 = b :: bs → False) → x.beq x_1 = false
-- Mathlib.Topology.Inseparable
/-- **Alias** of the forward direction of `stableUnderSpecialization_iff_Union_eq`. -/
StableUnderSpecialization.Union_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, StableUnderSpecialization s → ⋃ x ∈ s, closure {x} = s
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.mul_2 : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  (x y y' : MonCat.Colimits.Prequotient F),
  MonCat.Colimits.Relation F y y' → MonCat.Colimits.Relation F (x.mul y) (x.mul y')