mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.linear_of_iso : ∀ (R : Type u_1) [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  {F G : CategoryTheory.Functor C D} (e : F ≅ G) [CategoryTheory.Functor.Linear R F], CategoryTheory.Functor.Linear R G
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- A graph embedding is an embedding `f` such that for vertices `v w : V`,
`G'.Adj (f v) (f w) ↔ G.Adj v w`. Its image is an induced subgraph of G'.

The notation `G ↪g G'` represents the type of graph embeddings.  -/
SimpleGraph.Embedding : {V : Type u_1} → {W : Type u_2} → SimpleGraph V → SimpleGraph W → Type (max u_1 u_2)
-- Mathlib.RingTheory.KrullDimension.Basic
finiteRingKrullDim_iff_ne_bot_and_top : ∀ {R : Type u_1} [inst : CommSemiring R], FiniteRingKrullDim R ↔ ringKrullDim R ≠ ⊥ ∧ ringKrullDim R ≠ ⊤
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.Awareness.getD : Std.Time.Awareness → Std.Time.TimeZone → Std.Time.TimeZone
-- Mathlib.LinearAlgebra.LinearIndependent.Algebra
LinearIndepOn.id_image_algebraMap_iff : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A] [FaithfulSMul S A]
  {s : Set S}, LinearIndepOn R id (⇑(algebraMap S A) '' s) ↔ LinearIndepOn R id s
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- The 'unopposite' of an iso `αᵐᵒᵖ ≃* βᵐᵒᵖ`. Inverse to `MulEquiv.op`.  -/
MulEquiv.unop : {α : Type u_3} → {β : Type u_4} → [inst : Mul α] → [inst_1 : Mul β] → αᵐᵒᵖ ≃* βᵐᵒᵖ ≃ (α ≃* β)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.eq_1 : ∀ {α : Type u_1} (M : Matroid α) (I X : Set α), M.IsBasis I X = (Maximal (fun A => M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E)
-- Aesop.Tree.Data
Aesop.GoalId.mk.inj : ∀ {toNat toNat_1 : ℕ}, { toNat := toNat } = { toNat := toNat_1 } → toNat = toNat_1
-- Init.Data.SInt.Bitwise
Int16.and_neg_one : ∀ {a : Int16}, a &&& -1 = a
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Ordering.swap.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_3 ()
-- Init.Data.List.Nat.Modify
List.head?_modifyHead : ∀ {α : Type u_1} {l : List α} {f : α → α}, (List.modifyHead f l).head? = Option.map f l.head?
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightUnshift_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ₁ γ₂ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ)
  (hn : n' + a = n), (γ₁ + γ₂).rightUnshift n hn = γ₁.rightUnshift n hn + γ₂.rightUnshift n hn
-- Mathlib.LinearAlgebra.Contraction
dualTensorHom_comp_rTensor_dualMap : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] N),
  dualTensorHom R M P ∘ₗ LinearMap.rTensor P f.dualMap = LinearMap.lcomp R P f ∘ₗ dualTensorHom R N P
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.toList_pruneLT : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β),
  t.Ordered →
    ∀ (lowerBound : α),
      (Std.DTreeMap.Internal.Impl.pruneLT✝ t lowerBound).toList =
        List.filter (fun e => (compare e.fst lowerBound).isGT) t.toList
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.ofHom_comp : ∀ {X Y Z : Type u} [inst : AddSemigroup X] [inst_1 : AddSemigroup Y] [inst_2 : AddSemigroup Z] (f : X →ₙ+ Y)
  (g : Y →ₙ+ Z),
  AddSemigrp.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (AddSemigrp.ofHom f) (AddSemigrp.ofHom g)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_add : ∀ {α : Type u} [inst : Add α] (a b : α), ↑(a + b) = ↑a + ↑b
-- Init.Data.String.Defs
String.pushn_eq_repeat_push : ∀ {s : String} {c : Char} {n : ℕ}, s.pushn c n = Nat.repeat (fun s => s.push c) n s
-- Init.Data.UInt.Lemmas
UInt16.toFin_toUSize : ∀ (n : UInt16), n.toUSize.toFin = Fin.castLE UInt16.size_le_usizeSize n.toFin
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isAdjointPair_unique_of_nondegenerate : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  (B : LinearMap.BilinForm R₁ M₁),
  B.Nondegenerate →
    ∀ (φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁), LinearMap.IsAdjointPair B B ⇑ψ₁ ⇑φ → LinearMap.IsAdjointPair B B ⇑ψ₂ ⇑φ → ψ₁ = ψ₂
-- Mathlib.LinearAlgebra.Matrix.ToLin
Module.Basis.smulTower'.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [inst_6 : IsScalarTower R S A] {ι : Type u_5}
  {ι' : Type u_6} (b b_1 : Module.Basis ι R S),
  b = b_1 → ∀ (c c_1 : Module.Basis ι' S A), c = c_1 → b.smulTower' c = b_1.smulTower' c_1
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.isUniformEmbedding_singleton : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T0Space α], IsUniformEmbedding fun x => {x}
-- Mathlib.RingTheory.MvPowerSeries.Equiv
/-- The isomorphism between multivariable power series in no variables and the ground ring.  -/
MvPowerSeries.isEmptyEquiv : (σ : Type u_1) → (R : Type u_2) → [inst : CommSemiring R] → [IsEmpty σ] → MvPowerSeries σ R ≃ₐ[R] R
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagNode.mk.sizeOf_spec : ∀ (origin : Lean.Meta.Grind.Origin) (proof : Lean.Expr),
  sizeOf { origin := origin, proof := proof } = 1 + sizeOf origin + sizeOf proof
-- Mathlib.Data.QPF.Univariate.Basic
QPF.LiftpPreservation.eq_1 : ∀ {F : Type u → Type u} [q : QPF F],
  QPF.LiftpPreservation =
    ∀ ⦃α : Type u⦄ (p : α → Prop) (x : ↑(QPF.P F) α), Functor.Liftp p (QPF.abs x) ↔ Functor.Liftp p x
-- Mathlib.Algebra.Order.Nonneg.Field
/-- In an ordered field, the units of the nonnegative elements are the positive elements.  -/
Nonneg.unitsEquivPos : (R : Type u_2) →
  [inst : DivisionSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] → [PosMulReflectLT R] → { r // 0 ≤ r }ˣ ≃* { r // 0 < r }
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.mk.injEq : ∀ {n : ℕ} (length : ℕ) (partSize : Fin length → ℕ) (partSize_pos : ∀ (m : Fin length), 0 < partSize m)
  (emb : (m : Fin length) → Fin (partSize m) → Fin n) (emb_strictMono : ∀ (m : Fin length), StrictMono (emb m))
  (parts_strictMono : StrictMono fun m => emb m ⟨partSize m - 1, ⋯⟩)
  (disjoint : Set.univ.PairwiseDisjoint fun m => Set.range (emb m)) (cover : ∀ (x : Fin n), ∃ m, x ∈ Set.range (emb m))
  (length_1 : ℕ) (partSize_1 : Fin length_1 → ℕ) (partSize_pos_1 : ∀ (m : Fin length_1), 0 < partSize_1 m)
  (emb_1 : (m : Fin length_1) → Fin (partSize_1 m) → Fin n)
  (emb_strictMono_1 : ∀ (m : Fin length_1), StrictMono (emb_1 m))
  (parts_strictMono_1 : StrictMono fun m => emb_1 m ⟨partSize_1 m - 1, ⋯⟩)
  (disjoint_1 : Set.univ.PairwiseDisjoint fun m => Set.range (emb_1 m))
  (cover_1 : ∀ (x : Fin n), ∃ m, x ∈ Set.range (emb_1 m)),
  ({ length := length, partSize := partSize, partSize_pos := partSize_pos, emb := emb, emb_strictMono := emb_strictMono,
        parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover } =
      { length := length_1, partSize := partSize_1, partSize_pos := partSize_pos_1, emb := emb_1,
        emb_strictMono := emb_strictMono_1, parts_strictMono := parts_strictMono_1, disjoint := disjoint_1,
        cover := cover_1 }) =
    (length = length_1 ∧ partSize ≍ partSize_1 ∧ emb ≍ emb_1)
-- Init.Data.Int.DivMod.Lemmas
Int.mul_add_fmod_self_left : ∀ (a b c : ℤ), (a * b + c).fmod a = c.fmod a
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.free_congr_right : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ}
  (e₂ : B ≃g C), A.Free B ↔ A.Free C
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.one_def : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : One M], 1 = MonoidAlgebra.single 1 1
-- Mathlib.Analysis.Calculus.Deriv.Slope
HasDerivWithinAt.limsup_slope_le : ∀ {f : ℝ → ℝ} {f' : ℝ} {s : Set ℝ} {x r : ℝ},
  HasDerivWithinAt f f' s x → f' < r → ∀ᶠ (z : ℝ) in nhdsWithin x (s \ {x}), slope f x z < r
-- Mathlib.Order.Sublattice
Sublattice.coe_eq_empty : ∀ {α : Type u_2} [inst : Lattice α] {L : Sublattice α}, ↑L = ∅ ↔ L = ⊥
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Cell.getKey?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α} (c : Std.DTreeMap.Internal.Cell α β (compare k)),
  c.getKey? =
    match c.inner with
    | none => none
    | some p => some p.fst
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- Auxiliary construction for `desc`.  -/
CategoryTheory.InjectiveResolution.descFSucc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        (I : CategoryTheory.InjectiveResolution Y) →
          (J : CategoryTheory.InjectiveResolution Z) →
            (n : ℕ) →
              (g : J.cocomplex.X n ⟶ I.cocomplex.X n) →
                (g' : J.cocomplex.X (n + 1) ⟶ I.cocomplex.X (n + 1)) →
                  CategoryTheory.CategoryStruct.comp (J.cocomplex.d n (n + 1)) g' =
                      CategoryTheory.CategoryStruct.comp g (I.cocomplex.d n (n + 1)) →
                    (g'' : J.cocomplex.X (n + 2) ⟶ I.cocomplex.X (n + 2)) ×'
                      CategoryTheory.CategoryStruct.comp (J.cocomplex.d (n + 1) (n + 2)) g'' =
                        CategoryTheory.CategoryStruct.comp g' (I.cocomplex.d (n + 1) (n + 2))
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.Internal.AssocList.step_iter_nil : ∀ {α : Type u} {β : α → Type v}, Std.DHashMap.Internal.AssocList.nil.iter.step = ⟨Std.IterStep.done, ⋯⟩
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.map_obj_hom : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.map α β).obj X).hom =
    CategoryTheory.CategoryStruct.comp (α.app X.left) (CategoryTheory.CategoryStruct.comp (F.map X.hom) (β.app X.right))
-- Mathlib.Topology.Algebra.Valued.WithVal
Valuation.IsEquiv.orderRingIso_apply : ∀ {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} (h : v.IsEquiv w)
  (x : WithVal v), h.orderRingIso x = WithVal.toVal w x.ofVal
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The functoriality of `X.cycles` with respect to morphisms in
`ComposableArrows ι 2`.  -/
CategoryTheory.Abelian.SpectralObject.cyclesMap : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  {i' j' k' : ι} →
                    (f' : i' ⟶ j') →
                      (g' : j' ⟶ k') →
                        (CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') →
                          (n : ℤ) → X.cycles f g n ⟶ X.cycles f' g' n
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.rnDeriv_tilted_left : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ℝ} {ν : MeasureTheory.Measure α}
  [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν],
  AEMeasurable f ν →
    (μ.tilted f).rnDeriv ν =ᵐ[ν] fun x => ENNReal.ofReal (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) * μ.rnDeriv ν x
-- Std.Sat.CNF.Basic
Std.Sat.CNF.instMembershipClause : {α : Type u_1} → Membership (Std.Sat.CNF.Clause α) (Std.Sat.CNF α)
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- For complex-valued `f`, the difference between `proximity f ⊤` and `proximity f⁻¹ ⊤` is the circle
average of `log ‖f ·‖`.
 -/
ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage : ∀ {f : ℂ → ℂ},
  Meromorphic f →
    ValueDistribution.proximity f ⊤ - ValueDistribution.proximity f⁻¹ ⊤ = Real.circleAverage (fun x => Real.log ‖f x‖) 0
-- Mathlib.Logic.Function.FiberPartition
/-- Given `y : Y`, `Fiber.mk f y` is the fiber of `f` that `y` belongs to, as an element of `Fiber f`.
 -/
Function.Fiber.mk : {Y : Type u_2} → {Z : Type u_3} → (f : Y → Z) → Y → Function.Fiber f
-- Mathlib.Algebra.Order.CauSeq.Basic
IsCauSeq.cauchy₂ : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f : ℕ → β},
  IsCauSeq abv f → ∀ {ε : α}, 0 < ε → ∃ i, ∀ j ≥ i, ∀ k ≥ i, abv (f j - f k) < ε
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mem_mapEquiv_iff : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] (f : M ≃L[R] N) (s : ClosedSubmodule R M) (x : N),
  x ∈ (ClosedSubmodule.mapEquiv f) s ↔ f.symm x ∈ s
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Restriction along equal morphisms are isomorphic.  -/
AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr : {X Y : AlgebraicGeometry.Scheme} →
  {f g : X ⟶ Y} →
    f = g →
      [inst : AlgebraicGeometry.IsOpenImmersion f] →
        [inst_1 : AlgebraicGeometry.IsOpenImmersion g] →
          AlgebraicGeometry.Scheme.Modules.restrictFunctor f ≅ AlgebraicGeometry.Scheme.Modules.restrictFunctor g
-- Mathlib.CategoryTheory.Pi.Basic
/-- A family of isomorphisms gives rise to an isomorphism of families.  -/
CategoryTheory.Pi.isoMk : {I : Type w₀} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] → {X Y : (i : I) → C i} → ((i : I) → X i ≅ Y i) → (X ≅ Y)
-- Mathlib.GroupTheory.Solvable
map_derivedSeries_le_derivedSeries : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G') (n : ℕ),
  Subgroup.map f (derivedSeries G n) ≤ derivedSeries G' n
-- Mathlib.LinearAlgebra.Complex.Determinant
/-- The determinant of `conjAe`, as a linear map.  -/
Complex.det_conjAe : LinearMap.det ↑↑Complex.conjAe = -1
-- Lean.Parser.Term
Lean.Parser.Term.matchAltsWhereDecls : Lean.Parser.Parser
-- Aesop.Tree.Data
Aesop.Rapp.parentPostNormMetaState : Aesop.Rapp → Lean.Meta.SavedState → BaseIO Lean.Meta.SavedState
-- Mathlib.Logic.Relator
Relator.rel_iff : Relator.LiftFun (fun x1 x2 => x1 ↔ x2) (Relator.LiftFun (fun x1 x2 => x1 ↔ x2) fun x1 x2 => x1 ↔ x2)
  (fun x1 x2 => x1 ↔ x2) fun x1 x2 => x1 ↔ x2
-- Mathlib.Order.Birkhoff
/-- **Birkhoff's Representation Theorem**. Any finite distributive lattice can be embedded in a
powerset lattice.  -/
LatticeHom.birkhoffFinset : {α : Type u_1} →
  [inst : DistribLattice α] → [Fintype α] → [DecidablePred SupIrred] → LatticeHom α (Finset { a // SupIrred a })
-- Mathlib.Tactic.Simproc.Factors
Mathlib.Meta.Simproc.FactorsHelper.cons_self : ∀ {n m : ℕ} (a : ℕ) {l : List ℕ},
  Mathlib.Meta.NormNum.IsNat (a * m) n →
    Mathlib.Meta.Simproc.FactorsHelper m a l → Mathlib.Meta.Simproc.FactorsHelper n a (a :: l)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.ofAbs_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S), WithAbs.ofAbs 0 = 0
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Transfer `GrpObj` along an isomorphism.  -/
CategoryTheory.GrpObj.ofIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G X : C} → [CategoryTheory.GrpObj G] → (G ≅ X) → CategoryTheory.GrpObj X
-- Lean.Widget.UserWidget
_private.Lean.Widget.UserWidget.0.Lean.Widget.moduleRegistry : Lean.Widget.ModuleRegistry✝
-- Mathlib.Control.Functor.Multivariate
_private.Mathlib.Control.Functor.Multivariate.0.TypeVec.append1.match_1.eq_2 : ∀ {n : ℕ} (motive : Fin2 (n + 1) → Sort u_1) (h_1 : (i : Fin2 n) → motive i.fs) (h_2 : Unit → motive Fin2.fz),
  (match Fin2.fz with
    | i.fs => h_1 i
    | Fin2.fz => h_2 ()) =
    h_2 ()
-- Mathlib.RingTheory.RootsOfUnity.Complex
Complex.card_rootsOfUnity : ∀ (n : ℕ) [NeZero n], Nat.card ↥(rootsOfUnity n ℂ) = n
-- Mathlib.Data.DFinsupp.BigOperators
/-- `DFinsupp.prod f g` is the product of `g i (f i)` over the support of `f`.  -/
DFinsupp.prod : {ι : Type u} →
  {γ : Type w} →
    {β : ι → Type v} →
      [DecidableEq ι] →
        [inst : (i : ι) → Zero (β i)] →
          [(i : ι) → (x : β i) → Decidable (x ≠ 0)] → [CommMonoid γ] → (Π₀ (i : ι), β i) → ((i : ι) → β i → γ) → γ
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.finitePresentation_of_isFinite : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Finite σ] [Finite ι] (P : Algebra.Presentation R S ι σ), Algebra.FinitePresentation R S
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α}, t.getKey! a = t.getKeyD a default
-- Lean.Meta.Match.MatcherInfo
/-- `uElimPos?` is `some pos` when the matcher can eliminate in different universe levels, and
`pos` is the position of the universe level parameter that specifies the elimination universe.
It is `none` if the matcher only eliminates into `Prop`.
 -/
Lean.Meta.Match.MatcherInfo.uElimPos? : Lean.Meta.MatcherInfo → Option ℕ
-- Lean.Level
Lean.instEmptyCollectionLMVarIdMap : {α : Type} → EmptyCollection (Lean.LMVarIdMap α)
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.mem_cardSuppLTSubring : ∀ {Γ : Type u_1} {R : Type u_2} (κ : Cardinal.{u_1}) [inst : PartialOrder Γ] [inst_1 : AddCommMonoid Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : Ring R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] {x : HahnSeries Γ R},
  x ∈ HahnSeries.cardSuppLTSubring Γ R κ ↔ x.cardSupp < κ
-- Init.Data.List.Scan.Lemmas
List.head_scanr : ∀ {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → β → β} (h : List.scanr f b l ≠ []),
  (List.scanr f b l).head h = List.foldr f b l
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.im_mul : ∀ {R : Type u_1} {a b : R} [inst : Mul R] [inst_1 : Add R] (z w : QuadraticAlgebra R a b),
  (z * w).im = z.re * w.im + z.im * w.re + b * z.im * w.im
-- Mathlib.Data.Finset.Image
Finset.mem_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {b : β},
  b ∈ Finset.image f s ↔ ∃ a ∈ s, f a = b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_ofList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l → (Std.DTreeMap.Raw.ofList l cmp).size = l.length
-- Mathlib.Order.Interval.Finset.Defs
/-- This is a mixin class describing a locally finite order,
that is, is an order where bounded intervals are finite.
When you don't care too much about definitional equality, you can use `LocallyFiniteOrder.ofIcc` or
`LocallyFiniteOrder.ofFiniteIcc` to build a locally finite order from just `Finset.Icc`.  -/
LocallyFiniteOrder : (α : Type u_1) → [Preorder α] → Type u_1
-- Lean.Data.Options
Lean.Option.Decl.defValue : {α : Type} → Lean.Option.Decl α → α
-- Mathlib.RingTheory.Smooth.Kaehler
tensorKaehlerQuotKerSqEquiv_symm_tmul_D : ∀ {R : Type u_1} {P : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S] (s : S) (t : P),
  (tensorKaehlerQuotKerSqEquiv R P S).symm (s ⊗ₜ[P] (KaehlerDifferential.D R P) t) =
    s ⊗ₜ[P ⧸ RingHom.ker (algebraMap P S) ^ 2]
      (KaehlerDifferential.D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2))
        ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)
-- Mathlib.Order.CompleteLattice.Lemmas
disjoint_sSup_right : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : Set α} {b : α}, Disjoint b (sSup a) → ∀ {i : α}, i ∈ a → Disjoint b i
-- Mathlib.RingTheory.Multiplicity
pow_multiplicity_dvd : ∀ {α : Type u_1} [inst : Monoid α] (a b : α), a ^ multiplicity a b ∣ b
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
isTranscendenceBasis_iff_of_subsingleton : ∀ {ι : Type u} {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Subsingleton R] (x : ι → A), IsTranscendenceBasis R x ↔ Nonempty ι
-- Mathlib.Algebra.Group.Basic
div_div_div_cancel_right : ∀ {G : Type u_3} [inst : Group G] (a b c : G), a / c / (b / c) = a / b
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.HoCat.exists_resolution : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C),
  ∃ X',
    ∃ (_ : HomotopicalAlgebra.IsFibrant X'),
      ∃ i, HomotopicalAlgebra.Cofibration i ∧ HomotopicalAlgebra.WeakEquivalence i
-- Mathlib.Order.Heyting.Basic
/-- `(a ⇨ ·)` is right adjoint to `(a ⊓ ·)`  -/
GeneralizedHeytingAlgebra.le_himp_iff : ∀ {α : Type u_4} [self : GeneralizedHeytingAlgebra α] (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.instSliceableRocSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.instSliceableRocSlice._auto_1) →
      Std.Roc.Sliceable (Std.DTreeMap α β cmp) α (Std.DTreeMap.Internal.RocSlice α β)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.aeval_val_σ' : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (self : Algebra.Generators R S ι) (s : S), (MvPolynomial.aeval self.val) (self.σ' s) = s
-- Mathlib.Topology.Algebra.Group.Basic
/-- A compact set is covered by finitely many left additive translates of a set
with non-empty interior.  -/
compact_covered_by_add_left_translates : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {K V : Set G},
  IsCompact K → (interior V).Nonempty → ∃ t, K ⊆ ⋃ g ∈ t, (fun x => g + x) ⁻¹' V
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
/-- The **Wedderburn–Artin Theorem**, algebra form: an Artinian simple algebra is isomorphic
to a matrix algebra over the opposite of the endomorphism algebra of its simple module.  -/
IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite : ∀ (R₀ : Type u_1) (R : Type u) [inst : CommSemiring R₀] [inst_1 : Ring R] [inst_2 : Algebra R₀ R] [IsSimpleRing R]
  [IsArtinianRing R],
  ∃ n,
    ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, (t₁ \ t₂)[k]! = if k ∈ t₂ then default else t₁[k]!