mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.compl.eq_1 : ∀ {α : Type u_1} {V : Type u_2} [inst : Zero α] [inst_1 : One α] [inst_2 : DecidableEq α] [inst_3 : DecidableEq V]
  (A : Matrix V V α), A.compl = Matrix.of fun i j => if i = j then 0 else if A i j = 0 then 1 else 0
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.characteristic_centralizer : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [hH : H.Characteristic], (Subgroup.centralizer ↑H).Characteristic
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.ofNatIsoRight_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D C} (adj : H ⊣ F) (iso : F ≅ G),
  (adj.ofNatIsoRight iso).unit = CategoryTheory.CategoryStruct.comp adj.unit (H.whiskerLeft iso.hom)
-- Mathlib.NumberTheory.Height.Basic
/-- Extension for the `positivity` tactic: `Height.mulHeight` is always positive.  -/
Mathlib.Meta.Positivity.evalMulHeight : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.mul_le_prod : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s : Finset ι} [MulLeftMono N]
  {i j : ι}, (∀ i ∈ s, 1 ≤ f i) → i ∈ s → j ∈ s → i ≠ j → f i * f j ≤ ∏ k ∈ s, f k
-- Mathlib.Data.Seq.Basic
Stream'.Seq.drop_zero : ∀ {α : Type u} {s : Stream'.Seq α}, s.drop 0 = s
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_counitIso_inv_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₂ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).counitIso.inv.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.ofSubmodule_iSup : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (s : Set (Submodule R E)), ↑(⨆ S ∈ s, S) = ⨆ S ∈ s, ↑S
-- Mathlib.RingTheory.Bialgebra.Hom
/-- The proposition that the function preserves 1  -/
BialgHom.map_one' : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (self : A →ₐc[R] B), self.toFun 1 = 1
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.get_map_const : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (x : α), (fun x_1 => x) <$> get = pure x
-- Mathlib.Analysis.LocallyConvex.HahnBanach
Module.Dual.exists_extension_of_le_seminorm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : NormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_3 : Module 𝕜 E] (S : Submodule 𝕜 E) (f : Module.Dual 𝕜 ↥S) {p : Seminorm 𝕜 E},
  (∀ (x : ↥S), ‖f x‖ ≤ p ↑x) → ∃ g, (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), ‖g x‖ ≤ p x
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ofLinearEquiv_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_one : l 1 = 1)
  (map_mul : ∀ (x y : A₁), l (x * y) = l x * l y) (a : A₁), (AlgEquiv.ofLinearEquiv l map_one map_mul) a = l a
-- Mathlib.Algebra.Polynomial.Bivariate
/-- **Alias** of `Polynomial.evalEval_finsetSum`. -/
Polynomial.evalEval_finset_sum : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_3} (s : Finset ι) (x y : R) (f : ι → Polynomial (Polynomial R)),
  Polynomial.evalEval x y (∑ i ∈ s, f i) = ∑ i ∈ s, Polynomial.evalEval x y (f i)
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.invRotCompRot.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive],
  CategoryTheory.Pretriangulated.invRotCompRot = CategoryTheory.Pretriangulated.invRotCompRot
-- Mathlib.CategoryTheory.Abelian.Projective.Basic
/-- An object is projective if its preadditive co-Yoneda functor preserves finite colimits.  -/
CategoryTheory.projective_of_preservesFiniteColimits_preadditiveCoyonedaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (P : C)
  [hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj P)],
  CategoryTheory.Projective P
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.veq_refl : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : R), x =ᵥ x
-- Mathlib.Topology.MetricSpace.Isometry
/-- An isometry is continuous.  -/
Isometry.continuous : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → Continuous f
-- Mathlib.Topology.Compactness.Compact
nhds_prod_le_of_disjoint_cocompact : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : Filter Y} (x : X),
  Disjoint f (Filter.cocompact Y) → nhds x ×ˢ f ≤ nhdsSet ({x} ×ˢ Set.univ)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.uproj.injEq : ∀ (i : ℕ) (x : Lean.IR.VarId) (i_1 : ℕ) (x_1 : Lean.IR.VarId),
  (Lean.IR.Expr.uproj i x = Lean.IR.Expr.uproj i_1 x_1) = (i = i_1 ∧ x = x_1)
-- Mathlib.Algebra.Lie.Basic
/-- We could avoid defining this by instead defining a `LieRingModule L R` instance with a zero
bracket and relying on `LinearMap.instLieRingModule`. We do not do this because in the case that
`L = R` we would have a non-defeq diamond via `Ring.instBracket`.  -/
Module.Dual.instLieRingModule : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] → [inst_5 : LieRingModule L M] → [LieModule R L M] → LieRingModule L (M →ₗ[R] R)
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.derivedSeriesOfIdeal_add : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (k l : ℕ),
  LieAlgebra.derivedSeriesOfIdeal R L (k + l) I =
    LieAlgebra.derivedSeriesOfIdeal R L k (LieAlgebra.derivedSeriesOfIdeal R L l I)
-- Mathlib.Tactic.SetNotationForOrder
/-- Add an instance of `UsesSetNotationForOrder` for `declName`.  -/
_private.Mathlib.Tactic.SetNotationForOrder.0.Mathlib.Meta.SetNotationForOrder.mkUsesSetNotationForOrderInstance : Lean.Name → Lean.AttributeKind → Lean.CoreM Unit
-- Mathlib.Data.DFinsupp.Defs
/-- Adds a term to a dfinsupp, making a dfinsupp indexed by an `Option`.

This is the dfinsupp version of `Option.rec`.  -/
DFinsupp.extendWith : {ι : Type u} →
  {α : Option ι → Type v} →
    [inst : (i : Option ι) → Zero (α i)] → α none → (Π₀ (i : ι), α (some i)) → Π₀ (i : Option ι), α i
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
Mathlib.Tactic.ClickSuggestions.ApplyAtKey.mk : ℕ → ℕ → ℕ → String → Array Lean.Meta.AbstractMVarsResult → Mathlib.Tactic.ClickSuggestions.ApplyAtKey
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (m.insert k v).isEmpty = false
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get!_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₂).get! k = if k ∈ t₂ then default else t₁.get! k
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
SimpleGraph.two_colorable_iff_forall_loop_even : ∀ {α : Type u_1} {G : SimpleGraph α}, G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), Even w.length
-- Aesop.Options.Internal
Aesop.Options'.mk.sizeOf_spec : ∀ (toOptions : Aesop.Options) (generateScript : Bool) (forwardMaxDepth? : Option ℕ),
  sizeOf { toOptions := toOptions, generateScript := generateScript, forwardMaxDepth? := forwardMaxDepth? } =
    1 + sizeOf toOptions + sizeOf generateScript + sizeOf forwardMaxDepth?
-- Mathlib.Algebra.Prime.Lemmas
succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p : M},
  Prime p → ∀ {a b : M} {k l : ℕ}, p ^ k ∣ a → p ^ l ∣ b → p ^ (k + l + 1) ∣ a * b → p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.coe_toHom : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ↪g H), ⇑f.toHom = ⇑f
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.instInhabitedOfDecidableEq : {E : Type u_3} → [inst : AddGroup E] → [DecidableEq E] → Inhabited (NonarchAddGroupNorm E)
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.GoalContext.mk.sizeOf_spec : ∀ (lctx₁ : Lean.LocalContext) (localInstances₁ : Lean.LocalInstances) (lctx₂ : Lean.LocalContext)
  (localInstances₂ : Lean.LocalInstances) (equalFVarIds : Std.HashMap Lean.FVarId Lean.FVarId),
  sizeOf
      { lctx₁ := lctx₁, localInstances₁ := localInstances₁, lctx₂ := lctx₂, localInstances₂ := localInstances₂,
        equalFVarIds := equalFVarIds } =
    1 + sizeOf lctx₁ + sizeOf localInstances₁ + sizeOf lctx₂ + sizeOf localInstances₂ + sizeOf equalFVarIds
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.InfinitelyUpwardEnumerable.mk : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α],
  (∀ (a : α), (Std.PRange.succ? a).isSome = true) → Std.PRange.InfinitelyUpwardEnumerable α
-- Mathlib.Data.Finite.Defs
Set.infinite_coe_iff : ∀ {α : Type u} {s : Set α}, Infinite ↑s ↔ s.Infinite
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_range : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module S P] {σ : R →+* S}
  [inst_6 : RingHomSurjective σ] (f : M →ₛₗ[σ] P) [IsNoetherian R M], IsNoetherian S ↥f.range
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.invFun_eq_symm : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), e.invFun = ⇑e.symm
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
/-- The continuous `ℚ`-algebra isomorphism between `ℚ_[p]` and
`(primesEquiv.symm p).adicCompletion ℚ`.  -/
Padic.adicCompletionEquiv : (R : Type u_2) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      [inst_2 : Algebra R ℚ] →
        [inst_3 : IsFractionRing R ℚ] →
          [inst_4 : IsIntegralClosure R ℤ ℚ] →
            (p : Nat.Primes) →
              ℚ_[↑p] ≃A[ℚ]
                IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ (Rat.HeightOneSpectrum.primesEquiv.symm p)
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.forget_reflects_isos : (CategoryTheory.forget GrpCat).ReflectsIsomorphisms
-- Lean.Environment
Lean.AsyncConstantInfo.mk.injEq : ∀ (name : Lean.Name) (kind : Lean.ConstantKind) (sig : Task Lean.ConstantVal) (constInfo : Task Lean.ConstantInfo)
  (name_1 : Lean.Name) (kind_1 : Lean.ConstantKind) (sig_1 : Task Lean.ConstantVal)
  (constInfo_1 : Task Lean.ConstantInfo),
  ({ name := name, kind := kind, sig := sig, constInfo := constInfo } =
      { name := name_1, kind := kind_1, sig := sig_1, constInfo := constInfo_1 }) =
    (name = name_1 ∧ kind = kind_1 ∧ sig = sig_1 ∧ constInfo = constInfo_1)
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Z ⟶ Y)
  (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z) {Z_1 : C}
  (h : I.cocomplex.X 0 ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (J.ι.f 0)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.InjectiveResolution.desc f I J).f 0) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f (I.ι.f 0)) h
-- Mathlib.Data.Fin.Fin2
Fin2.IsLT.zero : ∀ (n : ℕ), Fin2.IsLT 0 n.succ
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.extensionMapRef : IO.Ref Lean.Meta.Grind.ExtensionMap
-- Mathlib.Data.Set.Function
Set.MapsTo.iterate_restrict : ∀ {α : Type u_1} {f : α → α} {s : Set α} (h : Set.MapsTo f s s) (n : ℕ),
  (Set.MapsTo.restrict f s s h)^[n] = Set.MapsTo.restrict f^[n] s s ⋯
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {a b : α},
  (a == b) = true → Std.DHashMap.Const.get! m a = Std.DHashMap.Const.get! m b
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
/-- If `f` sends `I` to `0` and `Iᶜ` to units, then `f` lifts to `κ(I)`.  -/
Ideal.ResidueField.liftₐ : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                (I : Ideal A) →
                  [inst_5 : I.IsPrime] →
                    (f : A →ₐ[R] B) →
                      I ≤ RingHom.ker f → I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid B) → I.ResidueField →ₐ[R] B
-- Mathlib.Data.Finset.Insert
Finset.insert_eq_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, a ∈ s → insert a s = s
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.underlyingIso_arrow_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f]
  {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_2 : CategoryTheory.ConcreteCategory C F] (x : carrier X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Subobject.mk f).arrow)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Subobject.underlyingIso f).inv) x) =
    (CategoryTheory.ConcreteCategory.hom f) x
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le' : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} (P : CategoryTheory.ObjectProperty C)
  [self : CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P],
  ∃ Q, ∃ (_ : CategoryTheory.ObjectProperty.Small.{w, v, u} Q), P ≤ Q.isoClosure
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.toEndUnit_inv : ∀ {ι : 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) (g : P.Aut),
  ((RootPairing.Equiv.toEndUnit P) g).inv = ↑(RootPairing.Equiv.symm P P g)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_le_size_insertMany_list : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {l : List (α × β)}, m.size ≤ (m.insertMany l).size
-- Std.Http.Data.Status
Std.Http.instToStringCustomStatus : ToString Std.Http.CustomStatus
-- Mathlib.CategoryTheory.Limits.Final.ParallelPair
CategoryTheory.Limits.parallelPair_initial_mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y),
  (∀ (Z : C), Nonempty (X ⟶ Z)) →
    (∀ ⦃Z : C⦄ (i j : X ⟶ Z),
        CategoryTheory.Zigzag (CategoryTheory.CostructuredArrow.mk i) (CategoryTheory.CostructuredArrow.mk j)) →
      (CategoryTheory.Limits.parallelPair f g).Initial
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → γ} {k : α} {h' : k ∈ Std.HashMap.Raw.map f m}
  (h : m.WF), (Std.HashMap.Raw.map f m).getKey k h' = m.getKey k ⋯
-- Lean.Environment
/-- Creates an async context when realizing `declName`  -/
_private.Lean.Environment.0.Lean.Environment.enterAsyncRealizing : Lean.Name → Lean.Environment → Lean.Environment
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toMultiplicative_apply_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : AddZeroClass G] [inst_1 : AddZeroClass H] (f : G ≃+ H) (a : Multiplicative G),
  (AddEquiv.toMultiplicative f) a = (AddMonoidHom.toMultiplicative f.toAddMonoidHom) a
-- Std.Time.Zoned.Database.PosixTz
_private.Std.Time.Zoned.Database.PosixTz.0.Std.Time.TimeZone.posixParseOffset : Std.Internal.Parsec.String.Parser Std.Time.TimeZone.Offset
-- Mathlib.Combinatorics.Hall.Basic
hallMatchingsFunctor.eq_1 : ∀ {ι : Type u} {α : Type v} (t : ι → Finset α),
  hallMatchingsFunctor t =
    { obj := fun ι' => ↑(hallMatchingsOn t (Opposite.unop ι')),
      map := fun {x x_1} g => TypeCat.ofHom (hallMatchingsOn.restrict t ⋯), map_id := ⋯, map_comp := ⋯ }
-- Init.Data.Option.Monadic
_private.Init.Data.Option.Monadic.0.Option.instDecidableEq.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (b : Option α) → (Unit → motive none) → ((val : α) → motive (some val)) → motive b
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- The category of `j`th iterations of a successor structure `Φ : SuccStruct C`.
An object consists of the data of all iterations of `Φ` for `i : J` such
that `i ≤ j` (this is the field `F`). Such objects are
equipped with data and properties which characterizes uniquely the iterations
on three types of elements: `⊥`, successors, limit elements.  -/
CategoryTheory.SmallObject.SuccStruct.Iteration : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      CategoryTheory.SmallObject.SuccStruct C →
        [inst_1 : LinearOrder J] →
          [SuccOrder J] →
            [OrderBot J] →
              [CategoryTheory.Limits.HasIterationOfShape J C] → [WellFoundedLT J] → J → Type (max (max u v) w)
-- Aesop.RuleTac.Basic
Aesop.instInhabitedSubgoal.default : Aesop.Subgoal
-- Mathlib.Algebra.Lie.Free
FreeNonUnitalNonAssocAlgebra.lift.congr_simp : ∀ (R : Type u_1) {X : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A],
  FreeNonUnitalNonAssocAlgebra.lift R = FreeNonUnitalNonAssocAlgebra.lift R
-- Mathlib.Analysis.Complex.Exponential
Real.exp_le_one_iff : ∀ {x : ℝ}, Real.exp x ≤ 1 ↔ x ≤ 0
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.integrable_iff_integrableAtFilter_cocompact : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε],
  MeasureTheory.Integrable f μ ↔
    MeasureTheory.IntegrableAtFilter f (Filter.cocompact X) μ ∧ MeasureTheory.LocallyIntegrable f μ
-- Batteries.Tactic.Init
/-- The `conv` mode tactic `exact e` closes the goal `⊢ t` by rewriting it to `t'`,
where `e : t = t'`.  -/
Batteries.Tactic.Conv.exact : Lean.ParserDescr
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.homAddEquiv_add : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f f' : F.obj X ⟶ Y),
  (adj.homEquiv X Y) (f + f') = (adj.homEquiv X Y) f + (adj.homEquiv X Y) f'
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_eq_iSup_addOrderOf : ∀ {G : Type u} [inst : AddCommMonoid G], (∀ (g : G), 0 < addOrderOf g) → AddMonoid.exponent G = ⨆ g, addOrderOf g
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₂ → (m₁ ∪ m₂)[k]? = m₁[k]?
-- Mathlib.Data.List.Dedup
List.Disjoint.dedup_append : ∀ {α : Type u_1} [inst : DecidableEq α] {xs ys : List α}, xs.Disjoint ys → (xs ++ ys).dedup = xs.dedup ++ ys.dedup
-- Batteries.Data.Random.MersenneTwister
Batteries.Random.MersenneTwister.State.mk : {cfg : Batteries.Random.MersenneTwister.Config} →
  Vector (BitVec cfg.wordSize) cfg.stateSize → Fin cfg.stateSize → Batteries.Random.MersenneTwister.State cfg
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshotInner.toSnapshot : {α : Type} → Lean.Elab.Tactic.TacticParsedSnapshotInner α → Lean.Language.Snapshot
-- Mathlib.Tactic.DepRewrite
/-- The free variable to substitute for `p`.  -/
Mathlib.Tactic.DepRewrite.Context.x : Mathlib.Tactic.DepRewrite.Context → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Every functor indexing a (co)equalizer is naturally isomorphic (actually, equal) to a
`parallelPair`  -/
CategoryTheory.Limits.diagramIsoParallelPair : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) →
      F ≅
        CategoryTheory.Limits.parallelPair (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
          (F.map CategoryTheory.Limits.WalkingParallelPairHom.right)
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRio.decEq : {α : Type u_1} → [DecidableEq α] → (x x_1 : Std.Rio α) → Decidable (x = x_1)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- The function supported at `i`, with value `x` there, and `1` elsewhere.  -/
RestrictedProduct.mulSingle : {ι : Type u_1} →
  {S : ι → Type u_3} →
    {G : ι → Type u_4} →
      [inst : (i : ι) → SetLike (S i) (G i)] →
        (A : (i : ι) → S i) →
          [DecidableEq ι] →
            [inst_2 : (i : ι) → One (G i)] →
              [∀ (i : ι), OneMemClass (S i) (G i)] →
                (i : ι) → G i → RestrictedProduct (fun i => G i) (fun i => ↑(A i)) Filter.cofinite
-- Lean.Elab.ConfigEval.Types
/-- Previous root components of `option` in reverse order, collecting results from `ConfigItem.shift`.  -/
Lean.Elab.ConfigEval.ConfigItem.prevOptionComps : Lean.Elab.ConfigEval.ConfigItem → List Lean.Syntax
-- Init.Notation
/-- Builtin command code action. See `command_code_action`.
 -/
Lean.builtin_command_code_action : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.MooreComplex
/-- The normalized Moore complex functor, on objects.
 -/
AlgebraicTopology.NormalizedMooreComplex.obj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.SimplicialObject C → ChainComplex C ℕ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_maxKey?_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, k ∈ t → t.maxKey?.isSome = true
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.lratProofToBinary.addNat : ByteArray → ℕ → ByteArray
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.algEquiv_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : Ring T] [inst_4 : Algebra R T] (h' : IsAdjoinRoot T f),
  (h.algEquiv h') h.root = h'.root
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_eq_of_le : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A}
  (S : Subalgebra R A), s ⊆ ↑S → S ≤ Algebra.adjoin R s → Algebra.adjoin R s = S