mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.fiberwiseColimCompColimIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  [inst_2 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape C H]
  (X : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H),
  CategoryTheory.Limits.fiberwiseColimCompColimIso.hom.app X = (CategoryTheory.Limits.colimitFiberwiseColimitIso X).hom
-- Mathlib.CategoryTheory.Functor.OfSequence
_private.Mathlib.CategoryTheory.Functor.OfSequence.0.CategoryTheory.Functor.OfSequence.map.match_3.eq_3 : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  (motive : (x : ℕ → C) → ((n : ℕ) → x n ⟶ x (n + 1)) → ℕ → ℕ → Sort u_3) (x : ℕ → C) (f : (n : ℕ) → x n ⟶ x (n + 1))
  (l : ℕ) (h_1 : (x : ℕ → C) → (x_1 : (n : ℕ) → x n ⟶ x (n + 1)) → motive x x_1 0 0)
  (h_2 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → motive x f 0 1)
  (h_3 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → (l : ℕ) → motive x f 0 l.succ)
  (h_4 : (x : ℕ → C) → (x_1 : (n : ℕ) → x n ⟶ x (n + 1)) → (n : ℕ) → motive x x_1 n.succ 0)
  (h_5 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → (k l : ℕ) → motive x f k.succ l.succ),
  (l = 0 → False) →
    (match x, f, 0, l.succ with
      | x, x_2, 0, 0 => h_1 x x_2
      | x, f, 0, 1 => h_2 x f
      | x, f, 0, l.succ => h_3 x f l
      | x, x_2, n.succ, 0 => h_4 x x_2 n
      | x, f, k.succ, l.succ => h_5 x f k l) =
      h_3 x f l
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Impl.treeSize.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.leaf.treeSize = 0
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.min?_reverse : ∀ {α : Type u_1} (t : RBTree.RBNode α), t.reverse.min? = t.max?
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` preserves colimits, then `F : C ⥤ Dᵒᵖ` preserves limits.  -/
CategoryTheory.Limits.preservesLimits_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimits F.leftOp],
  CategoryTheory.Limits.PreservesLimits F
-- Std.Time.Format.Basic
/-- Typeclass for formatting and parsing values with the given format type.
 -/
Std.Time.Format : (f : Type) → (Type → f → Type) → Type 1
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
/-- Path from `x` to `y` on the circle traversing in anti-clockwise direction.  -/
Circle.path : (x y : Circle) → Path x y
-- Lean.Data.Lsp.Internal
/-- Denotes the range of a reference, as well as the parent declaration of the reference.
If the reference is itself a declaration, then it contains no parent declaration.
The position information is inlined to reduce memory consumption.
 -/
Lean.Lsp.RefInfo.Location : Type
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The image under a ring homomorphism of the subsemiring generated by a set equals
the subsemiring generated by the image of the set.  -/
RingHom.map_closureS : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (s : Set R),
  Subsemiring.map f (Subsemiring.closure s) = Subsemiring.closure (⇑f '' s)
-- Mathlib.GroupTheory.Complement
/-- Given two subgroups `H' ⊆ H`, there exists a transversal to `H'` inside `H`  -/
AddSubgroup.exists_left_transversal_of_le : ∀ {G : Type u_1} [inst : AddGroup G] {H' H : AddSubgroup G},
  H' ≤ H → ∃ S, S + ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_nat_floor_atTop : ∀ {α : Type u_4} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorSemiring α],
  Filter.Tendsto (fun x => ⌊x⌋₊) Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.Discrete.StructuredArrow
/-- If `F : C ⥤ Discrete T` is a functor with `T` containing
a unique element `t`, then this is the equivalence
`StructuredArrow (Discrete.mk t) F ≌ C`.  -/
CategoryTheory.Discrete.structuredArrowEquivalenceOfUnique : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {T : Type w} →
      (F : CategoryTheory.Functor C (CategoryTheory.Discrete T)) →
        (t : T) → [Subsingleton T] → CategoryTheory.StructuredArrow { as := t } F ≌ C
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_fst_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  (X Y : P.FullSubcategory),
  (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y).hom =
    CategoryTheory.SemiCartesianMonoidalCategory.fst X.obj Y.obj
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} TopCat
-- Mathlib.Algebra.Polynomial.BigOperators
/-- The leading coefficient of a product of polynomials is equal to
the product of the leading coefficients.

See `Polynomial.leadingCoeff_prod'` (with a `'`) for a version for commutative semirings,
where additionally, the product of the leading coefficients must be nonzero.
 -/
Polynomial.leadingCoeff_prod : ∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] [NoZeroDivisors R] (f : ι → Polynomial R),
  (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff
-- Mathlib.Algebra.Module.Bimodule
/-- Forgetting the `B` action, a `Submodule` over `A ⊗[R] B` is just a `Submodule` over `A`.  -/
Subbimodule.toSubmodule : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {M : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : Semiring A] →
                [inst_4 : Semiring B] →
                  [inst_5 : Module A M] →
                    [inst_6 : Module B M] →
                      [inst_7 : Algebra R A] →
                        [inst_8 : Algebra R B] →
                          [inst_9 : IsScalarTower R A M] →
                            [inst_10 : IsScalarTower R B M] →
                              [inst_11 : SMulCommClass A B M] → Submodule (TensorProduct R A B) M → Submodule A M
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.eraIndex : Std.Time.Year.Era → Fin 2
-- Batteries.Classes.RatCast
/-- The canonical homomorphism `Rat → K`.  -/
RatCast.ratCast : {K : Type u} → [self : RatCast K] → ℚ → K
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getEntry?ₘ_eq_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β}, t.Ordered → t.getEntry?ₘ k = Std.Internal.List.getEntry? k t.toListModel
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_sub_cancel_right : ∀ {α : Type u} [inst : SubtractionMonoid α] {b : α}, IsAddUnit b → ∀ (a : α), a + b - b = a
-- Init.Data.SInt.Bitwise
Int8.toUInt8_xor : ∀ (a b : Int8), (a ^^^ b).toUInt8 = a.toUInt8 ^^^ b.toUInt8
-- Init.Data.UInt.Bitwise
USize.ofNat_and : ∀ (a b : ℕ), USize.ofNat (a &&& b) = USize.ofNat a &&& USize.ofNat b
-- Lean.LoadDynlib
Lean.instNonemptySymbol : ∀ {dynlib : Lean.Dynlib}, Nonempty dynlib.Symbol
-- Lean.Meta.MkIffOfInductiveProp
/-- `mkOpList op empty [x1, x2, ...]` is defined as `op x1 (op x2 ...)`.
Returns `empty` if the list is empty.  -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.mkOpList : Lean.Expr → Lean.Expr → List Lean.Expr → Lean.Expr
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cfg.then.eq_2 : ∀ (k : Turing.ToPartrec.Cont) (v : List ℕ),
  (Turing.ToPartrec.Cfg.ret k v).then = fun k' => Turing.ToPartrec.Cfg.ret (k.then k') v
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.balanceR_eq_balance : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond r.size l.size},
  Std.DTreeMap.Internal.Impl.balanceR k v l r hlb hrb hlr = Std.DTreeMap.Internal.Impl.balance k v l r hlb hrb ⋯
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxcIterator.FinitenessRelation : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.Iterators.FinitenessRelation (Std.DTreeMap.Internal.RxcIterator α β) Id
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.commonNeighbors.eq_1 : ∀ {V : Type u} (G : SimpleGraph V) (v w : V), G.commonNeighbors v w = G.neighborSet v ∩ G.neighborSet w
-- Mathlib.Algebra.Group.Defs
/-- A `SubNegMonoid` is an `AddMonoid` with unary `-` and binary `-` operations
satisfying `sub_eq_add_neg : ∀ a b, a - b = a + -b`.

The default for `sub` is such that `a - b = a + -b` holds by definition.

Adding `sub` as a field rather than defining `a - b := a + -b` allows us to
avoid certain classes of unification failures, for example:
Let `foo X` be a type with a `∀ X, Sub (Foo X)` instance but no
`∀ X, Neg (Foo X)`. Suppose we also have an instance
`∀ X [Cromulent X], AddGroup (Foo X)`. Then the `(-)` coming from
`AddGroup.sub` cannot be definitionally equal to the `(-)` coming from
`Foo.Sub`.

In the same way, adding a `zsmul` field makes it possible to avoid definitional failures
in diamonds. See the definition of `AddMonoid` and Note [forgetful inheritance] for more
explanations on this.
 -/
SubNegMonoid : Type u → Type u
-- Mathlib.Combinatorics.Hindman
/-- Constructor for `FP`. This is the preferred spelling over `FP.tail'`.  -/
Hindman.FP.tail : ∀ {M : Type u_1} [inst : Semigroup M] (a : Stream' M) (m : M), Hindman.FP a.tail m → m ∈ Hindman.FP a
-- Batteries.Tactic.Trans
/-- solving `e ← mkAppM' f #[x]`  -/
Batteries.Tactic.getExplicitFuncArg? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Lean.Expr
Lean.ExprStructEq.instHashable : Hashable Lean.ExprStructEq
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_preimage_mul_right : ∀ {a : ℝ},
  a ≠ 0 → ∀ (s : Set ℝ), MeasureTheory.volume ((fun x => x * a) ⁻¹' s) = ENNReal.ofReal |a⁻¹| * MeasureTheory.volume s
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.isCoatom_map_of_ker_le : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
  Function.Surjective ⇑f → ∀ {p : Submodule R M}, f.ker ≤ p → IsCoatom p → IsCoatom (Submodule.map f p)
-- Mathlib.Analysis.Analytic.Order
/-- A function vanishes at a point if its analytic order is nonzero in `ℕ∞`.  -/
apply_eq_zero_of_analyticOrderAt_ne_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜}, analyticOrderAt f z₀ ≠ 0 → f z₀ = 0
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicField.instAlgebra : (n : ℕ) →
  (A : Type u_1) →
    (K : Type u_2) → [inst : CommRing A] → [inst_1 : Field K] → [Algebra A K] → Algebra A (CyclotomicField n K)
-- Batteries.Data.Fin.Coding
Fin.encodeSubtype_decodeSubtype : ∀ {n : ℕ} (P : Fin n → Prop) [inst : DecidablePred P] (x : Fin (Fin.countP fun x => decide (P x))),
  Fin.encodeSubtype P (Fin.decodeSubtype P x) = x
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atBot_mul_const_right : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] (l : Filter α)
  {f : α → G} (C : G), Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => f x * C) l Filter.atBot
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_eq_iff_eq_coe : ∀ {r : ℝ} {p : NNReal}, p ≠ 0 → (r.toNNReal = p ↔ r = ↑p)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_ext_right_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {X Y : C} {f : J → C}
  {g h : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y (⨁ f)},
  g = h ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp g
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j)) =
        CategoryTheory.CategoryStruct.comp h
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j))
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mk_self : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (a : ↥S), Localization.mk (↑a) a = 1
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.left' : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (f g : a ⟶ b) →
        [CategoryTheory.BicategoricalCoherence f g] →
          CategoryTheory.BicategoricalCoherence f
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g)
-- Init.Data.Array.Monadic
Array.findM?_pure : ∀ {α : Type} {m : Type → Type u_1} [inst : Monad m] [LawfulMonad m] {p : α → Bool} {xs : Array α},
  Array.findM? (fun x => pure (p x)) xs = pure (Array.find? p xs)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.updateBox! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu → Lean.Expr → Lean.FVarId → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.Indep.union_indep_iff_contract_indep : ∀ {α : Type u_1} {M : Matroid α} {I J : Set α}, M.Indep I → (M.Indep (I ∪ J) ↔ (M.contract I).Indep (J \ I))
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
contMDiffWithinAt_iff_contDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} {f : E → E'} {s : Set E} {x : E},
  ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.unitOfList_equiv_foldl : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α},
  (Std.DHashMap.Raw.Const.unitOfList l).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) ∅ l)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.FinitePlace.norm_embedding'`.

---

The norm of the image after the embedding associated to `v` is equal to the norm of `v` raised
to the power of the `v`-adic valuation.  -/
NumberField.FinitePlace.norm_def' : ∀ {K : Type u_1} [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (x : K),
  ‖(NumberField.FinitePlace.embedding v) x‖ =
    ↑((WithZeroMulInt.toNNReal ⋯) ((IsDedekindDomain.HeightOneSpectrum.valuation K v) x))
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.instIsIsoFromGlued : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰)
-- Lean.Meta.CongrTheorems
/-- Similar to `mkHCongrWithArity`, but uses reserved names to ensure we don't keep creating the
same congruence theorem over and over again.
 -/
Lean.Meta.mkHCongrWithArityForConst? : Lean.Name → List Lean.Level → ℕ → Lean.MetaM (Option Lean.Meta.CongrTheorem)
-- Mathlib.Analysis.ODE.Gronwall
gronwallBound.eq_1 : ∀ (δ K ε x : ℝ),
  gronwallBound δ K ε x = if K = 0 then δ + ε * x else δ * Real.exp (K * x) + ε / K * (Real.exp (K * x) - 1)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Functor.prod'_obj : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B)
  (G : CategoryTheory.Functor A C) (a : A), (F.prod' G).obj a = (F.obj a, G.obj a)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- The submodule of skew-adjoint matrices with respect to the bilinear form corresponding to
the matrix `J`.  -/
skewAdjointMatricesSubmodule' : {R₂ : Type u_3} →
  [inst : CommRing R₂] → {n : Type u_5} → [Fintype n] → Matrix n n R₂ → [DecidableEq n] → Submodule R₂ (Matrix n n R₂)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- A strictly unitary lax functor `F` between bicategories `B` and `C` is a
lax functor `F` from `B` to `C` such that the structure 2-morphism
`𝟙 (obj X) ⟶ map (𝟙 X)` is in fact an identity 2-morphism for every `X : B`.  -/
CategoryTheory.StrictlyUnitaryLaxFunctor : (B : Type u₁) →
  [CategoryTheory.Bicategory B] →
    (C : Type u₂) → [CategoryTheory.Bicategory C] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)
-- Mathlib.RingTheory.Congruence.Hom
RingCon.coe_comapQuotientEquivRangeₐ_mk : ∀ {M : Type u_1} {N : Type u_2} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring N] [inst_4 : Algebra R N] (c : RingCon M) (f : N →ₐ[R] M) (x : N) {d : RingCon N}
  (h : d = c.comap f), ↑((c.comapQuotientEquivRangeₐ f h) ↑x) = ↑(f x)
-- Mathlib.Order.CompleteBooleanAlgebra
symmDiff_sSup_le : ∀ {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α},
  s.Nonempty → ∀ {a : α}, symmDiff a (sSup s) ≤ sSup ((fun x => symmDiff a x) '' s)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.instIsMonoidalMonoidalOppositeMopMopEquivalence : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).IsMonoidal
-- Mathlib.Algebra.Group.End
Equiv.permCongr_mul : ∀ {α : Type u_4} {β : Type u_5} (e : α ≃ β) (p q : Equiv.Perm α), e.permCongr (p * q) = e.permCongr p * e.permCongr q
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.Header.mk.sizeOf_spec : ∀ (version : UInt8) (isutcnt isstdcnt leapcnt timecnt typecnt charcnt : UInt32),
  sizeOf
      { version := version, isutcnt := isutcnt, isstdcnt := isstdcnt, leapcnt := leapcnt, timecnt := timecnt,
        typecnt := typecnt, charcnt := charcnt } =
    1 + sizeOf version + sizeOf isutcnt + sizeOf isstdcnt + sizeOf leapcnt + sizeOf timecnt + sizeOf typecnt +
      sizeOf charcnt
-- Mathlib.Data.Set.Prod
Set.offDiag_univ : ∀ {α : Type u_1}, Set.univ.offDiag = (Set.diagonal α)ᶜ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_eq_some_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α} (h : a ∈ m), Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.get m a h)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f g : A ⟶ B),
  CategoryTheory.StructuredArrow.Hom.right f = CategoryTheory.StructuredArrow.Hom.right g → f = g
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.IsSRGWith.of_not_adj : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ},
  G.IsSRGWith n k ℓ μ → Pairwise fun v w => ¬G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) = μ
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.aevalDifferential.congr_simp : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P P_1 : Algebra.PreSubmersivePresentation R S ι σ),
  P = P_1 → ∀ [inst_3 : Finite σ], P.aevalDifferential = P_1.aevalDifferential
-- Mathlib.Tactic.Linter.MinImports
/-- The transitive closure of the import graph of the current file.  The value is `none` only at
initialization time, as the linter immediately sets it to its value for the current file.  -/
_private.Mathlib.Tactic.Linter.MinImports.0.Mathlib.Linter.ImportState.transClosure : Mathlib.Linter.ImportState✝ → Option (Lean.NameMap Lean.NameSet)
-- Mathlib.NumberTheory.RamificationInertia.Galois
/-- All the `Ideal.inertiaDeg` over a fixed maximal ideal are the same.  -/
Ideal.inertiaDeg_eq_of_isGaloisGroup : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (p : Ideal A)
  (P Q : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] [hQp : Q.IsPrime] [Q.LiesOver p] (G : Type u_3)
  [inst_4 : Group G] [Finite G] [inst_6 : MulSemiringAction G B] [IsGaloisGroup G A B], P.inertiaDeg A = Q.inertiaDeg A
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).hom.app X).hom₂ =
    CategoryTheory.CategoryStruct.id X.obj₂
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.ground_id_apply : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M),
  PolynomialLaw.id.ground m = m
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.neg_unique : ∀ {α : Type u} [inst : AddMonoid α] {u₁ u₂ : AddUnits α}, ↑u₁ = ↑u₂ → ↑(-u₁) = ↑(-u₂)
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.instMulActionAEEqFun : {M : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : Monoid M] →
              [inst_3 : MulAction M α] →
                [MeasurableConstSMul M α] → [MeasureTheory.SMulInvariantMeasure M α μ] → MulAction Mᵈᵐᵃ (α →ₘ[μ] β)
-- Mathlib.GroupTheory.Index
AddSubgroup.index_range : ∀ {G : Type u_1} [inst : AddGroup G] {f : G →+ G} [hf : f.ker.FiniteIndex], f.range.index = Nat.card ↥f.ker
-- Mathlib.Order.Closure
/-- Convenience constructor for a closure operator using the weaker minimality axiom:
`x ≤ f y → f x ≤ f y`, which is sometimes easier to prove in practice.  -/
ClosureOperator.mk₂ : {α : Type u_1} →
  [inst : PartialOrder α] → (f : α → α) → (∀ (x : α), x ≤ f x) → (∀ ⦃x y : α⦄, x ≤ f y → f x ≤ f y) → ClosureOperator α
-- Mathlib.Topology.Category.Profinite.Basic
instFiniteCarrierToTopTotallyDisconnectedSpaceOfObj : ∀ (X : FintypeCat), Finite ↑(Profinite.of X.obj).toTop
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded : Type → Type
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_ne_zero_iff_of_exponent_ne_zero : ∀ {x y : ℂ}, y ≠ 0 → (x ^ y ≠ 0 ↔ x ≠ 0)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.toAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {ι : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : DecidableEq ι] →
                    [inst_6 : AddMonoid ι] →
                      {𝒜 : ι → Submodule R A} →
                        {ℬ : ι → Submodule R B} →
                          [inst_7 : GradedAlgebra 𝒜] → [inst_8 : GradedAlgebra ℬ] → (𝒜 →ₐᵍ[R] ℬ) → A →ₐ[R] B
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- A function `f` has the continuous linear map `f'` as derivative at `x` if
`f x' = f x + f' (x' - x) + o (x' - x)` when `x'` tends to `x`.  -/
HasFDerivAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          [inst_3 : TopologicalSpace E] →
            {F : Type u_3} →
              [inst_4 : AddCommGroup F] →
                [inst_5 : Module 𝕜 F] → [inst_6 : TopologicalSpace F] → (E → F) → (E →L[𝕜] F) → E → Prop