mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.mulEquivCongrRight_symm_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (e : M ≅ N)
  [inst_4 : CategoryTheory.IsMonHom e.hom] (X : C)
  (a : ↑((CategoryTheory.yonedaMon.obj { X := N, mon := inst_3 }).obj (Opposite.op X))),
  (CategoryTheory.Hom.mulEquivCongrRight e X).symm a =
    (MonCat.Hom.hom (MonCat.ofHom (CategoryTheory.IsMonHom.monoidHom e.inv X))) a
-- Std.Data.DHashMap.Basic
Std.DHashMap.instInsertSigma : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Insert ((a : α) × β a) (Std.DHashMap α β)
-- Mathlib.Analysis.SpecialFunctions.NonIntegrable
/-- If `f` grows in the punctured neighborhood of `c : ℝ` at least as fast as `1 / (x - c)`,
then it is not interval integrable on any nontrivial interval `a..b`, `c ∈ [a, b]`.  -/
not_intervalIntegrable_of_sub_inv_isBigO_punctured : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] {f : ℝ → F} {a b c : ℝ},
  (fun x => (x - c)⁻¹) =O[nhdsWithin c {c}ᶜ] f →
    a ≠ b → c ∈ Set.uIcc a b → ¬IntervalIntegrable f MeasureTheory.volume a b
-- Init.Data.Nat.Simproc
Nat.Simproc.beqEqOfEqEq : ∀ {a b c d : ℕ}, (a = b) = (c = d) → (a == b) = (c == d)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.State.mk.sizeOf_spec : ∀ {σ : Type} [inst : SizeOf σ] (state : σ) (activeScopes : Lean.NameSet) (delimitsLocal : Bool),
  sizeOf { state := state, activeScopes := activeScopes, delimitsLocal := delimitsLocal } =
    1 + sizeOf state + sizeOf activeScopes + sizeOf delimitsLocal
-- Mathlib.NumberTheory.NumberField.House
NumberField.house_nat_mul : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (α : K) (c : ℕ),
  NumberField.house (↑c * α) = ↑c * NumberField.house α
-- Mathlib.Data.Rel
SetRel.image_univ_left : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Nonempty → SetRel.image Set.univ s = Set.univ
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.smul_zero_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β] [inst_1 : SMulZeroClass α β] (s : Set α), s • 0 ⊆ 0
-- Init.Data.Int.Lemmas
Int.natCast_add_one : ∀ (n : ℕ), ↑(n + 1) = ↑n + 1
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.coe_toAlgEquiv : ∀ {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.toAlgEquiv = ⇑e
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- Construct an object in the free groupoid on `C` by providing an object in `C`.  -/
CategoryTheory.FreeGroupoid.mk : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → C → CategoryTheory.FreeGroupoid C
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {X : C} {K : Type s} [inst_3 : CategoryTheory.SmallCategory K] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape K D]
  {W : (J.Cover X)ᵒᵖ} (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D))
  (E :
    CategoryTheory.Limits.Cone
      (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W))))
  (i : (Opposite.unop W).Arrow) (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux F E i)
      ((CategoryTheory.Limits.limit.π F k).app (Opposite.op i.Y)) =
    CategoryTheory.CategoryStruct.comp (E.π.app k)
      (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (F.obj k)) i)
-- Init.Data.Rat.Lemmas
Rat.mul_neg : ∀ (a b : ℚ), a * -b = -(a * b)
-- Init.Data.Int.Linear
Int.not_gt_eq : ∀ (a b : ℤ), (¬a > b) = (a ≤ b)
-- Mathlib.Algebra.Group.Defs
/-- An `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.


[Wikidata Q83478](https://www.wikidata.org/wiki/Q83478) -/
AddGroup : Type u → Type u
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.orElse_Except : ∀ {ε α : Type} {post : α → Prop} {epost : EPost⟨ε → Prop⟩} (x : Except ε α) (h : Unit → Except ε α),
  ⦃ Std.Internal.Do.wp x post epost⟨fun x => Std.Internal.Do.wp (h ()) post epost⟩ ⦄ OrElse.orElse x h ⦃ post; epost ⦄
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.comap_comap : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {uγ : UniformSpace γ} {f : α → β} {g : β → γ},
  UniformSpace.comap (g ∘ f) uγ = UniformSpace.comap f (UniformSpace.comap g uγ)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- `K` and `Kᗮ` have trivial intersection.  -/
ClosedSubmodule.inf_orthogonal_eq_bot : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : ClosedSubmodule 𝕜 E), K ⊓ Kᗮ = ⊥
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residueFieldCongr_fromSpecResidueField_assoc : ∀ {X : AlgebraicGeometry.Scheme} {x y : ↥X} (h : x = y) {Z : AlgebraicGeometry.Scheme} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.residueFieldCongr h).hom)
      (CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) h_1) =
    CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField y) h_1
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.transPartialEquiv_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : α ≃ β) (f' : PartialEquiv β γ)
  (f'' : PartialEquiv γ δ), (e.transPartialEquiv f').trans f'' = e.transPartialEquiv (f'.trans f'')
-- Mathlib.Order.CompactlyGenerated.Basic
/-- **Alias** of the reverse direction of `CompleteLattice.isSupFiniteCompact_iff_isSupClosedCompact`. -/
CompleteLattice.IsSupClosedCompact.isSupFiniteCompact : ∀ (α : Type u_2) [inst : CompleteLattice α], CompleteLattice.IsSupClosedCompact α → CompleteLattice.IsSupFiniteCompact α
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- the underlying sheaf morphism is an isomorphism on each open subset  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.c_iso : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : AlgebraicGeometry.PresheafedSpace C} {f : X ⟶ Y}
  [self : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X),
  CategoryTheory.IsIso (f.c.app (Opposite.op (⋯.functor.obj U)))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toArray_insert_perm : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : BEq α] [Std.TransOrd α]
  [Std.LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.toArray.Perm
    ((Array.filter (fun x => decide ¬(k == x.fst) = true) t.toArray).push ⟨k, v⟩)
-- Mathlib.Data.Nat.WithBot
Nat.WithBot.lt_one_iff_le_zero : ∀ {x : WithBot ℕ}, x < 1 ↔ x ≤ 0
-- Mathlib.MeasureTheory.Group.Action
/-- If measure `μ` is invariant under a group action and is nonzero on a compact set `K`, then it is
positive on any nonempty open set. In case of a regular measure, one can assume `μ ≠ 0` instead of
`μ K ≠ 0`, see `MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero`.  -/
MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero : ∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [inst_3 : TopologicalSpace α]
  [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {K U : Set α},
  IsCompact K → μ K ≠ 0 → IsOpen U → U.Nonempty → 0 < μ U
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialRightAdjointMap.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : F.PartialRightAdjointSource} (f : X ⟶ Y),
  F.partialRightAdjointMap f =
    F.partialRightAdjointHomEquiv.symm
      (CategoryTheory.CategoryStruct.comp
        (F.partialRightAdjointHomEquiv (CategoryTheory.CategoryStruct.id (F.partialRightAdjointObj X))) f.hom)
-- Lean.Elab.MutualDef
/-- Ensures that the of let-rec definition types do not contain functions being defined.
In principle, this test can be improved. We could perform it after we separate the set of functions is strongly connected components.
However, this extra complication doesn't seem worth it.
 -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.checkLetRecsToLiftTypes : Array Lean.Expr → List Lean.Elab.Term.LetRecToLift → Lean.Elab.TermElabM Unit
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.inducedOuterMeasure_eq : ∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0),
  (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
      Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) →
    ∀ {s : Set α} (hs : MeasurableSet s), (MeasureTheory.inducedOuterMeasure m ⋯ m0) s = m s hs
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.comp_inverse' : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  {φ' : N → M} {f : X →ₑ[φ] Y} {g : Y → X} {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ}
  {h₁ : Function.LeftInverse g ⇑f} {h₂ : Function.RightInverse g ⇑f}, (f.inverse' g k₂ h₁ h₂).comp f = AddActionHom.id M
-- Mathlib.Order.RelClasses
WellFounded.psigma_skipLeft : ∀ (α : Type u) {β : Type v} {s : β → β → Prop}, WellFounded s → WellFounded (PSigma.SkipLeft α s)
-- Mathlib.NumberTheory.Dioph
Poly.induction : ∀ {α : Type u_1} {C : Poly α → Prop},
  (∀ (i : α), C (Poly.proj i)) →
    (∀ (n : ℤ), C (Poly.const n)) →
      (∀ (f g : Poly α), C f → C g → C (f - g)) → (∀ (f g : Poly α), C f → C g → C (f * g)) → ∀ (f : Poly α), C f
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.tendsto_abv_eval₂_atTop : ∀ {R : Type u_1} {S : Type u_2} {k : Type u_3} {α : Type u_4} [inst : Semiring R] [inst_1 : Ring S] [inst_2 : Field k]
  [inst_3 : LinearOrder k] [IsStrictOrderedRing k] (f : R →+* S) (abv : S → k) [IsAbsoluteValue abv] (p : Polynomial R),
  0 < p.degree →
    f p.leadingCoeff ≠ 0 →
      ∀ {l : Filter α} {z : α → S},
        Filter.Tendsto (abv ∘ z) l Filter.atTop →
          Filter.Tendsto (fun x => abv (Polynomial.eval₂ f (z x) p)) l Filter.atTop
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.mem_typeOf : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {M : Type w'} [inst : L.Structure M] [inst_1 : Nonempty M]
  [inst_2 : M ⊨ T] {v : α → M} {φ : (L.withConstants α).Sentence},
  φ ∈ T.typeOf v ↔ (FirstOrder.Language.Formula.equivSentence.symm φ).Realize v
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- In a cartesian monoidal category, `tensorLeft X` is naturally isomorphic `prod.functor.obj X`.
 -/
CategoryTheory.CartesianMonoidalCategory.tensorLeftIsoProd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] →
        (X : C) → CategoryTheory.MonoidalCategory.tensorLeft X ≅ CategoryTheory.Limits.prod.functor.obj X
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.mk'_Z : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : HomotopicalAlgebra.IsCofibrant X] [inst_3 : HomotopicalAlgebra.IsCofibrant Y]
  (h :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
      (CategoryTheory.Limits.coprod.desc f (CategoryTheory.CategoryStruct.id Y))),
  (HomotopicalAlgebra.CofibrantBrownFactorization.mk' f h).Z = h.Z
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Each element of the group defines a module automorphism.

This is a stronger version of `DistribMulAction.toAddAut`.  -/
DistribMulAction.toModuleAut : (R : Type u_1) →
  {S : Type u_4} →
    (M : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Group S] → [inst_4 : DistribMulAction S M] → [SMulCommClass S R M] → S →* M ≃ₗ[R] M
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.symm_mapRingEquiv : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddMonoid M]
  (e : R ≃+* S), (AddMonoidAlgebra.mapRingEquiv M e).symm = AddMonoidAlgebra.mapRingEquiv M e.symm
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.congr_trans : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} {P' : Type uP'} {Q' : Type uQ'}
  [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N]
  [inst_9 : AddCommMonoid P] [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P]
  [inst_13 : AddCommMonoid Q] [inst_14 : Module R Q] [inst_15 : AddCommMonoid P'] [inst_16 : Module R P']
  [inst_17 : Module A P'] [inst_18 : IsScalarTower R A P'] [inst_19 : AddCommMonoid Q'] [inst_20 : Module R Q']
  (f₁ : M ≃ₗ[A] P) (f₂ : P ≃ₗ[A] P') (g₁ : N ≃ₗ[R] Q) (g₂ : Q ≃ₗ[R] Q'),
  TensorProduct.AlgebraTensorModule.congr (f₁ ≪≫ₗ f₂) (g₁ ≪≫ₗ g₂) =
    TensorProduct.AlgebraTensorModule.congr f₁ g₁ ≪≫ₗ TensorProduct.AlgebraTensorModule.congr f₂ g₂
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_apply_lt_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} [MeasurableSingletonClass α],
  MeasureTheory.Measure.count s < ⊤ ↔ s.Finite
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.instHomIsOverInvOfHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] {e : X ≅ Y} [CategoryTheory.HomIsOver e.hom S],
  CategoryTheory.HomIsOver e.inv S
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- **Alias** of the forward direction of `Metric.inseparable_iff`. -/
Inseparable.dist_eq_zero : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α}, Inseparable x y → dist x y = 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.keys_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {c : ℕ}, (Std.DHashMap.emptyWithCapacity c).keys = []
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.integral_smul_eq_self : ∀ {α : Type u_3} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {G : Type u_7}
  [inst_2 : Group G] [inst_3 : MeasurableSpace α] [inst_4 : MulAction G α] [MeasurableConstSMul G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (f : α → E) {g : G},
  ∫ (x : α), f (g • x) ∂μ = ∫ (x : α), f x ∂μ
-- Init.Data.Array.Subarray
Subarray.size_eq : ∀ {α : Type u_1} {xs : Subarray α}, Std.Slice.size xs = xs.stop - xs.start
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ici_iSup : ∀ {α : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] (f : ι → α),
  UpperSet.Ici (⨆ i, f i) = ⨆ i, UpperSet.Ici (f i)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- The uncurrying of `A ⟶ (pushforward f).obj X` in `Over J` to a morphism
`(Over.pullback f).obj A ⟶ X` in `Over I`.  -/
CategoryTheory.ExponentiableMorphism.pushforwardUncurry : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I J : C} →
      {f : I ⟶ J} →
        [inst_1 : CategoryTheory.ChosenPullbacksAlong f] →
          [inst_2 : CategoryTheory.ExponentiableMorphism f] →
            {X : CategoryTheory.Over I} →
              {A : CategoryTheory.Over J} →
                (A ⟶ (CategoryTheory.ExponentiableMorphism.pushforward f).obj X) →
                  ((CategoryTheory.ChosenPullbacksAlong.pullback f).obj A ⟶ X)
-- Batteries.Data.UnionFind.Basic
Batteries.UFNode.mk : ℕ → ℕ → Batteries.UFNode
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.smul_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {𝕜' : Type u_5}
  [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F]
  {c : E → 𝕜'} {s : Set E}, DiffContOnCl 𝕜 c s → ∀ (y : F), DiffContOnCl 𝕜 (fun x => c x • y) s
-- Lean.Meta.Basic
Lean.Meta.instHashableSynthInstanceCacheKey : Hashable Lean.Meta.SynthInstanceCacheKey
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
PiTensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse : ∀ {ι : Type u_1} {R : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [inst : CommRing R]
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Finite ι]
  [inst_4 : ∀ (i : ι), Finite (κ i)] (b : (i : ι) → Module.Basis (κ i) R (M i)),
  PiTensorProduct.dualDistrib ∘ₗ PiTensorProduct.dualDistribInvOfBasis b = LinearMap.id
-- Mathlib.Control.Fold
Traversable.foldr : {α β : Type u} → {t : Type u → Type u} → [Traversable t] → (α → β → β) → β → t α → β
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.forM_eq_forM_keysArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α → m' PUnit.{w + 1}},
  Std.DHashMap.forM (fun a x => f a) m = Array.forM f m.keysArray
-- Lean.Elab.DeclarationRange
Lean.Elab.getDeclarationRange? : {m : Type → Type} → [Monad m] → [Lean.MonadFileMap m] → Lean.Syntax → m (Option Lean.DeclarationRange)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_eq_getD : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {a : α} {fallback : β} {h : a ∈ m}, Std.DHashMap.Raw.Const.get m a h = Std.DHashMap.Raw.Const.getD m a fallback
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- If `u'` is a right quasi-inverse of `u` and `w` is a left quasi-inverse of `v ∘ₗ u`,
then `u ∘ₗ w` is a left quasi-inverse of `v`.  -/
LinearMap.IsLeftQuasiInverse.of_comp_left : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V]
  [inst_2 : Module K V] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : AddCommGroup V₃]
  [inst_6 : Module K V₃] {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V₃} {u' : V₂ →ₗ[K] V} {w : V₃ →ₗ[K] V},
  u'.IsRightQuasiInverse u → w.IsLeftQuasiInverse (v ∘ₗ u) → (u ∘ₗ w).IsLeftQuasiInverse v
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.union_congr : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ m₄ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF),
  m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁.union m₂ ⋯ ⋯).Equiv (m₃.union m₄ ⋯ ⋯)
-- Mathlib.RingTheory.Algebraic.Defs
Algebra.IsAlgebraic.isAlgebraic : ∀ {R : Type u} {A : Type v} {inst : CommRing R} {inst_1 : Ring A} {inst_2 : Algebra R A}
  [self : Algebra.IsAlgebraic R A] (x : A), IsAlgebraic R x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.GoalState.parents : Lean.Meta.Grind.GoalState → Lean.Meta.Grind.ParentMap
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeWhile₂.match_3.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (a : α) (as : List α) (b : β) (bs : List β)
  (h_1 : (a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs))
  (h_2 : (x : List α) → (x_1 : List β) → motive x x_1),
  (match a :: as, b :: bs with
    | a :: as, b :: bs => h_1 a as b bs
    | x, x_1 => h_2 x x_1) =
    h_1 a as b bs
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of `SimpleGraph.IsContained.maxDegree_mono`. -/
SimpleGraph.IsContained.max_degree_le : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : DecidableRel G.Adj] [inst_3 : DecidableRel H.Adj], G.IsContained H → G.maxDegree ≤ H.maxDegree
-- Std.Http.Internal.Char
/-- Checks if a byte is a hexadecimal digit (0-9, a-f, or A-F).
 -/
Std.Http.Internal.Char.isHexDigitByte : UInt8 → Bool
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.natCast.injEq : ∀ (k k_1 : ℕ), (Lean.Grind.CommRing.Expr.natCast k = Lean.Grind.CommRing.Expr.natCast k_1) = (k = k_1)
-- Mathlib.Logic.Equiv.Defs
/-- This cannot be a `simp` lemmas as it incorrectly matches against `e : α ≃ synonym α`, when
`synonym α` is semireducible. This makes a mess of `Multiplicative.ofAdd` etc.  -/
Equiv.Perm.coe_subsingleton : ∀ {α : Type u_1} [Subsingleton α] (e : Equiv.Perm α), ⇑e = id
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_insert_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α} {fallback b : β a}, (m.insert a b).getD a fallback = b
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The first projection at a point in a product is `C^∞`.  -/
contDiffAt_fst : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {p : E × F},
  ContDiffAt 𝕜 n Prod.fst p
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_C_mul : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R],
  a ≠ 0 → (Polynomial.C a * p).natDegree = p.natDegree
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.constOfIsEmpty_apply : ∀ (R : Type u) {ι : Type v} (M₁ : ι → Type w₁) {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  [inst_7 : IsEmpty ι] (m : M₂) (a : (i : ι) → M₁ i), (ContinuousMultilinearMap.constOfIsEmpty R M₁ m) a = m
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalExprApplyNewGoals.evalExpr : Lean.Expr → Lean.MetaM Lean.Meta.ApplyNewGoals
-- Mathlib.Order.Filter.Basic
/-- Eta-expanded form of `Filter.EventuallyEq.neg` -/
Filter.EventuallyEq.fun_neg : ∀ {α : Type u} {β : Type v} [inst : Neg β] {f g : α → β} {l : Filter α}, f =ᶠ[l] g → (fun i => -f i) =ᶠ[l] fun i => -g i
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.Ordinal.instReprOfDay : Repr Std.Time.Nanosecond.Ordinal.OfDay
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.lcm_dedup : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [inst_2 : DecidableEq α]
  (s : Multiset α), s.dedup.lcm = s.lcm
-- Mathlib.Lean.Expr.Basic
/-- `Lean.Expr.lt? e` takes `e : Expr` as input.
If `e` represents `a < b`, then it returns `some (t, a, b)`, where `t` is the Type of `a`,
otherwise, it returns `none`.  -/
Lean.Expr.lt? : Lean.Expr → Option (Lean.Expr × Lean.Expr × Lean.Expr)
-- Lean.Meta.LitValues
/-- Check if an expression is a list literal (i.e. a nested chain of `List.cons`, ending at a `List.nil`),
where each element is "recognised" by a given function `f : Expr → MetaM (Option α)`,
and return the array of recognised values.
 -/
Lean.Meta.getListLitOf? : {α : Type} → Lean.Expr → (Lean.Expr → Lean.MetaM (Option α)) → Lean.MetaM (Option (Array α))
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.mkSemiringThm : Lean.Name → Lean.Expr → Lean.MetaM (Option Lean.Expr)