mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddMonoidHom.map_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_3} [inst_1 : AddGroup N] (f : G →+ N) (x : G),
  AddSubgroup.map f (AddSubgroup.zmultiples x) = AddSubgroup.zmultiples (f x)
-- Mathlib.Order.Grade
OrderDual.gradeOrder : {𝕆 : Type u_1} → {α : Type u_3} → [inst : Preorder 𝕆] → [inst_1 : Preorder α] → [GradeOrder 𝕆 α] → GradeOrder 𝕆ᵒᵈ αᵒᵈ
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instInsertProdOfTransCmp : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Insert (α × β) (Std.ExtTreeMap α β cmp)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, (m.insert k v).getKey? a = if (k == a) = true then some k else m.getKey? a
-- Mathlib.Order.RelClasses
instWellFoundedLTNat : WellFoundedLT ℕ
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- The trivial charted space structure on the model space is compatible with any groupoid.  -/
hasGroupoid_model_space : ∀ (H : Type u_5) [inst : TopologicalSpace H] (G : StructureGroupoid H), HasGroupoid H G
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert_mem_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (i : ℕ), p.getVert i ∈ p.support
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.coe_curry : ∀ (ι : Type u_6) (κ : Type u_7) (X : Type u_8) [inst : MeasurableSpace X],
  ⇑(MeasurableEquiv.curry ι κ X) = Function.curry
-- Std.Time.Date.Unit.Month
Std.Time.Month.instOfNatQuarter : {n : ℕ} → OfNat Std.Time.Month.Quarter n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.lift_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : R ⟶ S) (g : R ⟶ T),
  CategoryTheory.Over.Hom.left (CategoryTheory.CartesianMonoidalCategory.lift f g) =
    CategoryTheory.Limits.pullback.lift (CategoryTheory.Over.Hom.left f) (CategoryTheory.Over.Hom.left g) ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pos_of_mul_pos_right : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [PosMulReflectLT α], 0 < a * b → 0 ≤ a → 0 < b
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma.eq_1 : ∀ (k : ℕ), ArithmeticFunction.sigma k = { toFun := fun n => ∑ d ∈ n.divisors, d ^ k, map_zero' := ⋯ }
-- Mathlib.Data.Multiset.Fintype
Multiset.ToType.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] (m m_1 : Multiset α), m = m_1 → m.ToType = m_1.ToType
-- Lean.Server.GoTo
Lean.Server.GoToContext.children : Lean.Server.GoToContext → Lean.PersistentArray Lean.Elab.InfoTree
-- Init.Data.SInt.Basic
instLEInt8 : LE Int8
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_eq_empty_of_le : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], b ≤ a → Finset.Ico a b = ∅
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
/-- **Alias** of the reverse direction of `Complex.log_mul_eq_add_log_iff`. -/
Complex.log_mul : ∀ {x y : ℂ},
  x ≠ 0 → y ≠ 0 → x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi → Complex.log (x * y) = Complex.log x + Complex.log y
-- Init.Data.UInt.Basic
/-- Bitwise complement, also known as bitwise negation, for 64-bit unsigned integers. Usually accessed
via the `~~~` prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.complement : UInt64 → UInt64
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGELT : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (a b : ℤ), t.IsGE ((t.truncGELT a b).obj X) a
-- Mathlib.Order.Category.Semilat
SemilatInfCat.Iso.mk_hom_toFun : ∀ {α β : SemilatInfCat} (e : α.X ≃o β.X) (a : α.X), (SemilatInfCat.Iso.mk e).hom a = e a
-- Mathlib.Data.Nat.Cast.Order.Basic
instNontrivialOfCharZero : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [CharZero α], Nontrivial α
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.aemeasurable : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} {β : Type u_3}
  [inst_1 : MeasurableSpace β] [l.IsCountablyGenerated] [l.NeBot] {f : α → β} {φ : ι → Set α},
  MeasureTheory.AECover μ l φ → (∀ (i : ι), AEMeasurable f (μ.restrict (φ i))) → AEMeasurable f μ
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_homologyMap_of_isIso_cyclesMap_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.IsIso (CategoryTheory.ShortComplex.cyclesMap φ) →
    CategoryTheory.Epi φ.τ₁ → CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_smulRightL_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι],
  ‖ContinuousMultilinearMap.smulRightL 𝕜 E G‖ ≤ 1
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.ΓSpecIso_naturality : ∀ {R S : CommRingCat} (f : R ⟶ S),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map f))
      (AlgebraicGeometry.Scheme.ΓSpecIso S).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).hom f
-- Mathlib.Order.Types.Defs
OrderType.instOne : One OrderType.{u_1}
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.clear.sizeOf_spec : ∀ (p : Turing.PartrecToTM2.Γ' → Bool) (k : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ'),
  sizeOf (Turing.PartrecToTM2.Λ'.clear p k q) = 1 + sizeOf k + sizeOf q
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceGT : Lean.Meta.Simp.Simproc
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
RootPairing.restrictScalars_pairing : ∀ {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field L] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module L M] [inst_4 : Module L N] (P : RootPairing ι L M N) (K : Type u_5)
  [inst_5 : Field K] [inst_6 : Algebra K L] [inst_7 : Module K M] [inst_8 : Module K N] [inst_9 : IsScalarTower K L M]
  [inst_10 : IsScalarTower K L N] [inst_11 : P.IsBalanced] [inst_12 : P.IsValuedIn K] (i j : ι),
  (algebraMap K L) ((P.restrictScalars' K).pairing i j) = P.pairing i j
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofTacticInfo.injEq : ∀ (i i_1 : Lean.Elab.TacticInfo), (Lean.Elab.Info.ofTacticInfo i = Lean.Elab.Info.ofTacticInfo i_1) = (i = i_1)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.norm_toZeroAtInfty : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : ProperSpace E] (f : SchwartzMap E F),
  ‖f.toZeroAtInfty‖ = ‖f.toBoundedContinuousFunction‖
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits of shape `Jᵒᵖ`, then `F : C ⥤ D` reflects colimits
of shape `J`.  -/
CategoryTheory.Limits.reflectsColimitsOfShape_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.ReflectsLimitsOfShape Jᵒᵖ F.op], CategoryTheory.Limits.ReflectsColimitsOfShape J F
-- Init.Data.SInt.Lemmas
Int8.ofNat_bitVecToNat : ∀ (n : BitVec 8), Int8.ofNat n.toNat = Int8.ofBitVec n
-- Init.Data.Vector.Basic
Vector.mem_toArray_iff : ∀ {α : Type u_1} {n : ℕ} (a : α) (xs : Vector α n), a ∈ xs.toArray ↔ a ∈ xs
-- Mathlib.Tactic.Linter.HaveLetLinter
/-- The main implementation of the `have` vs `let` linter.  -/
_private.Mathlib.Tactic.Linter.HaveLetLinter.0.Mathlib.Linter.haveLet.haveLetLinter : Lean.Linter
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instToFormatProof : Std.ToFormat Mathlib.Tactic.ITauto.Proof
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.forget_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C C)
  (A : CategoryTheory.Endofunctor.Coalgebra F), (CategoryTheory.Endofunctor.Coalgebra.forget F).obj A = A.V
-- Std.Http.Data.Body.Empty
Std.Http.Body.instEmpty : Std.Http.Body Std.Http.Body.Empty
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Cases.mk.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (typeName : Lean.Name) (resultType : Lean.Expr) (discr : Lean.FVarId)
  (alts : Array (Lean.Compiler.LCNF.Alt pu)) (typeName_1 : Lean.Name) (resultType_1 : Lean.Expr) (discr_1 : Lean.FVarId)
  (alts_1 : Array (Lean.Compiler.LCNF.Alt pu)),
  (Lean.Compiler.LCNF.Cases.mk typeName resultType discr alts =
      Lean.Compiler.LCNF.Cases.mk typeName_1 resultType_1 discr_1 alts_1) =
    (typeName = typeName_1 ∧ resultType = resultType_1 ∧ discr = discr_1 ∧ alts = alts_1)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddLocalization.addEquivOfQuotient_addMonoidOf : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  {f : S.LocalizationMap N} (x : M), (AddLocalization.addEquivOfQuotient f) ((AddLocalization.addMonoidOf S) x) = f x
-- Mathlib.Computability.Language
Language.instInsertList : {α : Type u_1} → Insert (List α) (Language α)
-- Init.TacticsExtra
_private.Init.TacticsExtra.0.Lean.Parser.Tactic.expandIfThenElse : Lean.Syntax →
  Lean.Syntax →
    Lean.Syntax →
      Lean.Syntax → Lean.Syntax → (Lean.Term → Lean.Term → Lean.MacroM Lean.Term) → Lean.MacroM (Lean.TSyntax `tactic)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedCommAux.eq_1 : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)],
  TensorProduct.gradedCommAux R 𝒜 ℬ =
    DirectSum.toModule R (ι × ι) (DirectSum (ι × ι) fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)) fun i =>
      have o := DirectSum.lof R (ι × ι) (fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)) (i.2, i.1);
      have s := (-1) ^ (i.1 * i.2);
      (s • o) ∘ₗ ↑(TensorProduct.comm R (𝒜 i.1) (ℬ i.2))
-- Mathlib.Analysis.Normed.Field.Basic
/-- A normed division ring is a normed ring.  -/
NormedDivisionRing.toNormedRing : {α : Type u_2} → [β : NormedDivisionRing α] → NormedRing α
-- Mathlib.Data.Nat.Log
Nat.log_eq_one_iff : ∀ {b n : ℕ}, Nat.log b n = 1 ↔ n < b * b ∧ 1 < b ∧ b ≤ n
-- Mathlib.Algebra.Order.Group.Basic
zpow_right_mono : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {a : α},
  1 ≤ a → Monotone fun n => a ^ n
-- Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
DomMulAct.instSMulCommClassMulActionHomId : ∀ {M : Type u_1} {α : Type u_2} {N : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul N α]
  [inst_2 : SMulCommClass M N α] [inst_3 : SMul N β] {M' : Type u_5} [inst_4 : SMul M' α]
  [inst_5 : SMulCommClass M' N α] [SMulCommClass M M' α], SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (α →ₑ[id] β)
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.instInhabited : {a : String.Slice} → Inhabited (String.Slice.Pattern.ForwardSliceSearcher a)
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.DiagnosticsState.mk.inj : ∀ {stickyDiagsRef : IO.Ref (Lean.PersistentArray Lean.Widget.InteractiveDiagnostic)}
  {diags : Lean.PersistentArray Lean.Widget.InteractiveDiagnostic} {isIncremental : Bool} {publishedDiagsAmount : ℕ}
  {stickyDiagsRef_1 : IO.Ref (Lean.PersistentArray Lean.Widget.InteractiveDiagnostic)}
  {diags_1 : Lean.PersistentArray Lean.Widget.InteractiveDiagnostic} {isIncremental_1 : Bool}
  {publishedDiagsAmount_1 : ℕ},
  { stickyDiagsRef := stickyDiagsRef, diags := diags, isIncremental := isIncremental,
        publishedDiagsAmount := publishedDiagsAmount } =
      { stickyDiagsRef := stickyDiagsRef_1, diags := diags_1, isIncremental := isIncremental_1,
        publishedDiagsAmount := publishedDiagsAmount_1 } →
    stickyDiagsRef = stickyDiagsRef_1 ∧
      diags = diags_1 ∧ isIncremental = isIncremental_1 ∧ publishedDiagsAmount = publishedDiagsAmount_1
-- Mathlib.RingTheory.Polynomial.IsIntegral
/-- [Stacks Tag 00H0](https://stacks.math.columbia.edu/tag/00H0) ((2)) -/
IsIntegral.coeff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Polynomial S},
  IsIntegral (Polynomial R) p → ∀ (i : ℕ), IsIntegral R (p.coeff i)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_eq_sum_theta' : ∀ {x : ℝ},
  0 ≤ x →
    ∀ {N : ℕ}, ⌊Real.log x / Real.log 2⌋₊ ≤ N → Chebyshev.psi x = ∑ n ∈ Finset.Icc 1 N, Chebyshev.theta (x ^ (1 / ↑n))
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The obvious functor `ShortComplex Cᵒᵖ ⥤ (ShortComplex C)ᵒᵖ`.  -/
CategoryTheory.ShortComplex.unopFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      CategoryTheory.Functor (CategoryTheory.ShortComplex Cᵒᵖ) (CategoryTheory.ShortComplex C)ᵒᵖ
-- Mathlib.Algebra.Order.Monoid.Submonoid
/-- An `AddSubmonoid` of an ordered cancellative additive monoid is an ordered cancellative
additive monoid.  -/
AddSubmonoid.toIsOrderedCancelAddMonoid : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M] (S : AddSubmonoid M),
  IsOrderedCancelAddMonoid ↥S
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Commute.cfcAbs_left : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a b : A},
  Commute a b → Commute a (star b) → Commute (CFC.abs a) b
-- Lean.Elab.Binders
_private.Lean.Elab.Binders.0.Lean.Elab.Term.elabBindersAux : {α : Type} → Array Lean.Syntax → (Array (Lean.Syntax × Lean.Expr) → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
/-- The kernel fork `KernelFork.ofι Φ.ι Φ.ι_π` exhibits `Φ.ι : Φ.r ⟶ 𝟭 C` as the kernel
of the canonical projection `Φ.π : 𝟭 C ⟶ Φ.quotient`.  -/
CategoryTheory.Abelian.Preradical.isLimitKernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (Φ : CategoryTheory.Abelian.Preradical C) →
        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι Φ.ι ⋯)
-- Mathlib.GroupTheory.Exponent
AddSubmonoid.exponent_top : ∀ (G : Type u) [inst : AddMonoid G], AddMonoid.exponent ↥⊤ = AddMonoid.exponent G
-- Init.Data.SInt.Lemmas
Int32.ofIntTruncate_toInt : ∀ (x : Int32), Int32.ofIntClamp x.toInt = x
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableAt_const : ∀ {𝕜 : 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] {x : E} (c : F), DifferentiableAt 𝕜 (fun x => c) x
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instOrElseGrindTacticM : {α : Type} → OrElse (Lean.Elab.Tactic.Grind.GrindTacticM α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k : α},
  t.WF → (List.find? (fun x => compare x.1 k == Ordering.eq) (Std.DTreeMap.Internal.Impl.Const.toList t) = none ↔ k ∉ t)
-- Mathlib.Algebra.Group.Basic
inv_mul_eq_inv_mul_iff_mul_eq_mul : ∀ {G : Type u_3} [inst : CommGroup G] {a b c d : G}, b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- Extension of `PolynomialLaw.smul_def`  -/
PolynomialLaw.toFun_smul : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_4}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (r : R) (f : M →ₚₗ[R] N) (S : Type u_5) [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S], PolynomialLaw.toFun S (r • f) = r • PolynomialLaw.toFun S f
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineSubspace.subtypeₐᵢ_toAffineMap : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s], s.subtypeₐᵢ.toAffineMap = s.subtype
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instOne.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : One β],
  MeasureTheory.SimpleFunc.instOne = { one := MeasureTheory.SimpleFunc.const α 1 }
-- Mathlib.Data.Quot
Trunc.induction_on : ∀ {α : Sort u_1} {β : Trunc α → Prop} (q : Trunc α), (∀ (a : α), β (Trunc.mk a)) → β q
-- Init.Data.UInt.Bitwise
UInt64.toUInt32_or : ∀ (a b : UInt64), (a ||| b).toUInt32 = a.toUInt32 ||| b.toUInt32
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.instSemiring : {α : Type u_1} →
  [DecidableEq α] →
    [inst : Semiring α] →
      [inst_1 : PartialOrder α] → [CanonicallyOrderedAdd α] → [NoZeroDivisors α] → [Nontrivial α] → Semiring (WithTop α)
-- Mathlib.Geometry.Euclidean.Inversion.Basic
ContinuousOn.inversion : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {X : Type u_3} [inst_4 : TopologicalSpace X] {c x : X → P} {R : X → ℝ} {s : Set X},
  ContinuousOn c s →
    ContinuousOn R s →
      ContinuousOn x s → (∀ a ∈ s, x a ≠ c a) → ContinuousOn (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) s
-- Mathlib.Order.CompleteLattice.Defs
OrderDual.infSet.eq_1 : ∀ (α : Type u_8) [h : SupSet α], OrderDual.infSet α = { sInf := fun s => sSup s }
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftKanExtension_hom_ext_iff : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} [inst_3 : L.HasLeftKanExtension F]
  {G : CategoryTheory.Functor D H} {γ₁ γ₂ : L.leftKanExtension F ⟶ G},
  γ₁ = γ₂ ↔
    CategoryTheory.CategoryStruct.comp (L.leftKanExtensionUnit F) (L.whiskerLeft γ₁) =
      CategoryTheory.CategoryStruct.comp (L.leftKanExtensionUnit F) (L.whiskerLeft γ₂)
-- Mathlib.Order.Cover
Set.wcovBy_insert : ∀ {α : Type u_1} (x : α) (s : Set α), s ⩿ insert x s
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.adj_of_mem_walk_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v),
  ¬p.Nil → ∀ {x : V}, x ∈ p.support → ∃ y ∈ p.support, G.Adj x y
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Bornology α] [inst_1 : Bornology β] {f g : LocallyBoundedMap α β},
  (∀ (a : α), f a = g a) → f = g
-- Lean.Meta.ACLt
Lean.Meta.ACLt.ReduceMode.reduce : Lean.Meta.ACLt.ReduceMode
-- Mathlib.RingTheory.Localization.Module
Module.Basis.ofIsLocalizedModule_span : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ]
  [inst_2 : Algebra R Rₛ] [inst_3 : IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid Mₛ] [inst_7 : Module R Mₛ] [inst_8 : Module Rₛ Mₛ]
  [inst_9 : IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [inst_10 : IsLocalizedModule S f] {ι : Type u_5}
  (b : Module.Basis ι R M), Submodule.span R (Set.range ⇑(Module.Basis.ofIsLocalizedModule Rₛ S f b)) = f.range
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.product_nsmul : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : AddMonoid α]
  [inst_3 : AddMonoid β] (s : Finset α) (t : Finset β) (n : ℕ), n • s ×ˢ t = (n • s) ×ˢ (n • t)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.SemiCartesianMonoidalCategory.default_eq_toUnit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory C]
  (X : C), default = CategoryTheory.SemiCartesianMonoidalCategory.toUnit X
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.δ_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X' X : CategoryTheory.SimplicialObject C} (f : X ⟶ X') {n : ℕ}
  (i : Fin (n + 2)) {Z : C} (h : X'.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n })) h) =
    CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n + 1 }))
      (CategoryTheory.CategoryStruct.comp (X'.δ i) h)
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.IsReduced.append_flatten_replicate_append : ∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)},
  FreeAddGroup.IsCyclicallyReduced L₂ →
    FreeAddGroup.IsReduced (L₁ ++ L₂ ++ L₃) →
      ∀ {n : ℕ}, n ≠ 0 → FreeAddGroup.IsReduced (L₁ ++ (List.replicate n L₂).flatten ++ L₃)
-- Lean.ExtraModUses
Lean.IndirectModUse.mk.injEq : ∀ (kind : String) (declName : Lean.Name) (kind_1 : String) (declName_1 : Lean.Name),
  ({ kind := kind, declName := declName } = { kind := kind_1, declName := declName_1 }) =
    (kind = kind_1 ∧ declName = declName_1)
-- Mathlib.Order.Bounds.Basic
Set.subsingleton_of_isLUB_le_isGLB : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {a b : α}, IsGLB s a → IsLUB s b → b ≤ a → s.Subsingleton
-- Mathlib.CategoryTheory.Sites.Precoverage.Generates
CategoryTheory.Precoverage.Generates.generate_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {J : CategoryTheory.GrothendieckTopology C},
  K.Generates J → ∀ {X : C} {R : CategoryTheory.Presieve X}, R ∈ K.coverings X → CategoryTheory.Sieve.generate R ∈ J X
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_coeIdeal : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : Ideal R), ↑↑I = IsLocalization.coeSubmodule P I
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.InducedWideCategory.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} D] {F : C → D}
  {P : CategoryTheory.MorphismProperty D} [inst_1 : P.IsMultiplicative] {X Y : CategoryTheory.InducedWideCategory D F P}
  [inst_2 : SizeOf C] [inst_3 : SizeOf D] [inst_4 : ⦃X Y : D⦄ → (x : X ⟶ Y) → SizeOf (P x)] (hom : F X ⟶ F Y)
  (property : P hom), sizeOf { hom := hom, property := property } = 1 + sizeOf hom + sizeOf property
-- Mathlib.Order.Interval.Set.Basic
Set.decidableMemIoo : {α : Type u_1} →
  [inst : Preorder α] → {a b x : α} → [Decidable (a < x)] → [Decidable (x < b)] → Decidable (x ∈ Set.Ioo a b)