mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Bundle.ContMDiffRiemannianMetric.symm : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℝ F] {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_8 : (b : B) → TopologicalSpace (E b)] [inst_9 : (b : B) → AddCommGroup (E b)]
  [inst_10 : (b : B) → Module ℝ (E b)] [inst_11 : FiberBundle F E] [inst_12 : VectorBundle ℝ F E]
  (self : Bundle.ContMDiffRiemannianMetric IB n F E) (b : B) (v w : E b), ((self.inner b) v) w = ((self.inner b) w) v
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constMaxEntry_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {he : t₁.isEmpty = false} (h : t₁.Equiv t₂), Std.DTreeMap.Const.maxEntry t₁ he = Std.DTreeMap.Const.maxEntry t₂ ⋯
-- Lean.Message
/-- Serializes the message, converting its data into a string and saving its kind.  -/
Lean.Message.serialize : Lean.Message → BaseIO Lean.SerialMessage
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.addCommGroup : {R : Type u_1} → {M : Type u_4} → [inst : Ring R] → AddCommGroup (MonoidAlgebra R M)
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.map_length : ∀ {f : ℤ → ℤ} {xs : Lean.Omega.Coeffs}, (Lean.Omega.Coeffs.map f xs).length ≤ xs.length
-- Init.Data.UInt.Lemmas
USize.toUInt32_ofNatClamp_of_le : ∀ {n : ℕ},
  USize.size ≤ n →
    (USize.ofNatClamp n).toUInt32 = UInt32.ofNatLT (UInt32.size - 1) UInt64.toUInt32_ofNatClamp_of_le._proof_1
-- Mathlib.Algebra.Lie.TraceForm
/-- A finite, free representation of a Lie algebra `L` induces a bilinear form on `L` called
the trace form. See also `killingForm`.  -/
LieModule.traceForm : (R : Type u_1) →
  (L : Type u_3) →
    (M : Type u_4) →
      [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] → LinearMap.BilinForm R L
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.ofSet_source : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X) (hs : IsOpen s), (OpenPartialHomeomorph.ofSet s hs).source = s
-- Mathlib.Data.Finsupp.WellFounded
Finsupp.Lex.wellFoundedLT : ∀ {α : Type u_3} {N : Type u_4} [inst : LT α] [Std.Trichotomous fun x1 x2 => x1 < x2] [hα : WellFoundedGT α]
  [inst_2 : AddMonoid N] [inst_3 : PartialOrder N] [IsBotZeroClass N] [hN : WellFoundedLT N],
  WellFoundedLT (Lex (α →₀ N))
-- Mathlib.Order.UpperLower.Closure
le_upperClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {t : UpperSet α}, t ≤ upperClosure s ↔ s ⊆ ↑t
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.of_add_right : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s t : Set E},
  Bornology.IsVonNBounded 𝕜 (s + t) → s.Nonempty → Bornology.IsVonNBounded 𝕜 t
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesMap_comp : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C) (n : ℕ),
  groupHomology.cyclesMap (g.comp f) (CategoryTheory.CategoryStruct.comp φ ((Rep.resFunctor f).map ψ)) n =
    CategoryTheory.CategoryStruct.comp (groupHomology.cyclesMap f φ n) (groupHomology.cyclesMap g ψ n)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_4.eq_2 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (k : ℤ) (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match Lean.Grind.CommRing.Expr.intCast k with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.intCast k => h_2 k
    | Lean.Grind.CommRing.Expr.natCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_2 k
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.finite_quotient_of_pretransitive_of_finite_quotient : ∀ {G : Type u} (X : Type v) [inst : AddGroup G] [inst_1 : AddAction G X] [AddAction.IsPretransitive G X]
  {H : AddSubgroup G} [Finite (G ⧸ H)], Finite (AddAction.orbitRel.Quotient (↥H) X)
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso_hom : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C)
  (e : F.obj X ≅ CategoryTheory.Functor.id D) (Y : CategoryTheory.GradedObject J D) (a : I × J) (ha : a.1 = 0),
  (CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIso F X e Y a ha).hom =
    CategoryTheory.CategoryStruct.comp
      ((F.map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 X a.1 ha).hom).app (Y a.2)) (e.hom.app (Y a.2))
-- Std.Time.Internal.UnitVal
/-- Converts a `UnitVal` to an `Int`.
 -/
Std.Time.Internal.UnitVal.toInt : {α : ℚ} → Std.Time.Internal.UnitVal α → ℤ
-- Mathlib.Computability.NFA
/-- `M.reverse` constructs an NFA with the same states as `M`, but all the transitions reversed. The
resulting automaton accepts a word `x` if and only if `M` accepts `List.reverse x`.  -/
NFA.reverse : {α : Type u} → {σ : Type v} → NFA α σ → NFA α σ
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.withDensity.instIsLocallyFiniteMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : TopologicalSpace α]
  [MeasureTheory.IsLocallyFiniteMeasure μ], MeasureTheory.IsLocallyFiniteMeasure (ν.withDensity (μ.rnDeriv ν))
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.typeToCat_map : ∀ {X Y : Type u} (f : X ⟶ Y),
  CategoryTheory.typeToCat.map f =
    (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑(CategoryTheory.ConcreteCategory.hom f))).toCatHom
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- If `symm := true`, then the rewrite is right-to-left.  -/
Mathlib.Tactic.ClickSuggestions.RwKey.symm : Mathlib.Tactic.ClickSuggestions.RwKey → Bool
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_of_le_ge : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : Std.IsPartialOrder α]
  [Lean.Grind.OrderedAdd α] (ctx : Lean.Grind.Linarith.Context α) (p₁ p₂ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.eq_of_le_ge_cert p₁ p₂ = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ ≤ 0 →
      Lean.Grind.Linarith.Poly.denote' ctx p₂ ≤ 0 → Lean.Grind.Linarith.Poly.denote' ctx p₁ = 0
-- Lean.Parser.Basic
Lean.Parser.epsilonInfo : Lean.Parser.ParserInfo
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_comm : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s → (μ.restrict t).restrict s = (μ.restrict s).restrict t
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.inl_biprodComparison' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (F.biprodComparison' X Y) =
    F.map CategoryTheory.Limits.biprod.inl
-- Mathlib.Tactic.DefEqAbuse
/-- Find top-level synthesis failures and their `isDefEq` root causes.
Only enters failing synthesis nodes to avoid reporting recovered sub-attempts.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Mathlib.Tactic.DefEqAbuse.findSynthFailures : Std.HashSet String → Std.HashSet String → Lean.MessageData → BaseIO (Array (Lean.MessageData × Array Lean.MessageData))
-- Mathlib.CategoryTheory.Generator.Sheaf
CategoryTheory.Sheaf.hasSeparator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasCoproducts A]
  [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasSeparator A] [CategoryTheory.Preadditive A]
  [CategoryTheory.Limits.HasCoproducts A], CategoryTheory.HasSeparator (CategoryTheory.Sheaf J A)
-- Init.Data.SInt.Lemmas
Int16.zero_mul : ∀ {a : Int16}, 0 * a = 0
-- Lean.Language.Basic
/-- `Syntax` processed by this `SnapshotTask`.
The `Syntax` is used by the language server to determine whether to force this `SnapshotTask`
when a request is made.
In general, the elaborator retains the following invariant:
If `stx?` is `none`, then this snapshot task (and all of its children) do not contain `InfoTree`
information that can be used in the language server, and so the language server will ignore it
when it is looking for an `InfoTree`.
Nonetheless, if `stx?` is `none`, then this snapshot task (and any of its children) may still
contain message log information.
 -/
Lean.Language.SnapshotTask.stx? : {α : Type} → Lean.Language.SnapshotTask α → Option Lean.Syntax
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.instAddMonObjTensorObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        {M N : C} →
          [CategoryTheory.AddMonObj M] →
            [CategoryTheory.AddMonObj N] →
              CategoryTheory.AddMonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.Ordered : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Zipper α β → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {kf : CategoryTheory.Limits.KernelFork f}
  {kf' : CategoryTheory.Limits.KernelFork f'} (hf : CategoryTheory.Limits.IsLimit kf)
  (hf' : CategoryTheory.Limits.IsLimit kf') (φ : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'),
  (CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit hf hf' φ).hom = kf.mapOfIsLimit hf' φ.hom
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.IsFinite.isFiniteType_generators : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat}
  {inst_2 : J.WEqualsLocallyBijective AddCommGrpCat} {M : SheafOfModules R} {p : M.Presentation} [self : p.IsFinite],
  p.generators.IsFiniteType
-- Mathlib.Data.Matrix.Reflection
/-- This can be used to prove
```lean
example [AddCommMonoid α] [Mul α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :
  !![a₁₁, a₁₂;
     a₂₁, a₂₂] * !![b₁₁, b₁₂;
                    b₂₁, b₂₂] =
  !![a₁₁*b₁₁ + a₁₂*b₂₁, a₁₁*b₁₂ + a₁₂*b₂₂;
     a₂₁*b₁₁ + a₂₂*b₂₁, a₂₁*b₁₂ + a₂₂*b₂₂] :=
(mulᵣ_eq _ _).symm
```
 -/
Matrix.mulᵣ_eq : ∀ {l m n : ℕ} {α : Type u_1} [inst : Mul α] [inst_1 : AddCommMonoid α] (A : Matrix (Fin l) (Fin m) α)
  (B : Matrix (Fin m) (Fin n) α), A.mulᵣ B = A * B
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_apply : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (f : ι → MeasureTheory.Measure α) {s : Set α},
  MeasurableSet s → (MeasureTheory.Measure.sum f) s = ∑' (i : ι), (f i) s
-- Init.Data.Vector.Algebra
Vector.zero_mul : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] [inst_1 : Mul α], (∀ (x : α), 0 * x = 0) → ∀ (xs : Vector α n), 0 * xs = 0
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.uniformBell_one_right : ∀ (m : ℕ), m.uniformBell 1 = 1
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.le_iff_le : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (H : Subgroup Gal(E/F))
  (K : IntermediateField F E), K ≤ IntermediateField.fixedField H ↔ H ≤ K.fixingSubgroup
-- Mathlib.Algebra.Group.Submonoid.Support
AddSubmonoid.IsPointed.eq_zero_of_mem_of_neg_mem : ∀ {G : Type u_1} [inst : AddGroup G] {M : AddSubmonoid G}, M.IsPointed → ∀ {x : G}, x ∈ M → -x ∈ M → x = 0
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_apply : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x : ↑S.cycles),
  (CategoryTheory.ConcreteCategory.hom S.moduleCatLeftHomologyData.i)
      ((CategoryTheory.ConcreteCategory.hom S.moduleCatCyclesIso.hom) x) =
    (CategoryTheory.ConcreteCategory.hom S.iCycles) x
-- Init.System.IO
IO.RealWorld.instNonempty : Nonempty IO.RealWorld
-- Init.WF
/-- If the first projections of two pairs are ordered, then they are lexicographically ordered.
 -/
Prod.Lex.left : ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β),
  ra a₁ a₂ → Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.mkMetric.eq_1 : ∀ {X : Type u_2} [inst : EMetricSpace X] (m : ENNReal → ENNReal),
  MeasureTheory.OuterMeasure.mkMetric m = MeasureTheory.OuterMeasure.mkMetric' fun s => m (Metric.ediam s)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection onto `(𝕜 ∙ v)ᗮ` of `v` is zero.  -/
Submodule.orthogonalProjectionOnto_orthogonalComplement_singleton_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (v : E), (𝕜 ∙ v)ᗮ.orthogonalProjectionOnto v = 0
-- Mathlib.Data.DFinsupp.BigOperators
AddMonoidHom.coe_dfinsuppSum : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {R : Type u_1} {S : Type u_2} [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddZeroClass R] [inst_4 : AddCommMonoid S]
  (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →+ S), ⇑(f.sum g) = f.sum fun a b => ⇑(g a b)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] {U V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ}
  (i : U ⟶ V),
  CategoryTheory.CategoryStruct.comp (X.presheaf.map i)
      (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f (Opposite.unop V)) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f (Opposite.unop U))
      (Y.presheaf.map ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).op.map i))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_7 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.umod with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_7 ()
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.fderiv_implicitFunction_apply_eq_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G) {x : G} {y : E},
  (fderiv 𝕜 (φ.implicitFunction (φ.leftFun φ.pt)) (φ.rightFun φ.pt)) x = y ↔ φ.leftDeriv y = 0 ∧ φ.rightDeriv y = x
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}) →
      AddGroup ↑(Profinite.limitCone (F.comp (CategoryTheory.forget₂ ProfiniteAddGrp.{max u v} Profinite))).pt.toTop
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- Two homomorphisms `G →+ G'` of additive groups are equal if and only if they agree
on a generator of `G`.  -/
AddMonoidHom.eq_iff_eq_on_generator : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] {g : G},
  (∀ (x : G), x ∈ AddSubgroup.zmultiples g) → ∀ (f₁ f₂ : G →+ G'), f₁ = f₂ ↔ f₁ g = f₂ g
-- Mathlib.Topology.UnitInterval
unitInterval.symm_eq_zero : ∀ {i : ↑unitInterval}, unitInterval.symm i = 0 ↔ i = 1
-- Init.Grind.Offset
Lean.Grind.Nat.unsat_lo_lo : ∀ (u v k₁ k₂ : ℕ), Lean.Grind.isLt 0 (k₁ + k₂) = true → u + k₁ ≤ v → v + k₂ ≤ u → False
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.piUnique_apply : ∀ {α : Type u_9} [inst : Unique α] (R : Type u_10) [inst_1 : Semiring R] (f : α → Type u_11)
  [inst_2 : (x : α) → AddCommMonoid (f x)] [inst_3 : (x : α) → Module R (f x)]
  [inst_4 : (x : α) → TopologicalSpace (f x)], ⇑(ContinuousLinearEquiv.piUnique R f) = fun f => f default
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrTheorem.mk.injEq : ∀ (type proof : Lean.Expr) (argKinds : Array Lean.Meta.CongrArgKind) (type_1 proof_1 : Lean.Expr)
  (argKinds_1 : Array Lean.Meta.CongrArgKind),
  ({ type := type, proof := proof, argKinds := argKinds } =
      { type := type_1, proof := proof_1, argKinds := argKinds_1 }) =
    (type = type_1 ∧ proof = proof_1 ∧ argKinds = argKinds_1)
-- Init.Data.UInt.Lemmas
UInt32.sub_eq_add_mul : ∀ (a b : UInt32), a - b = a + 4294967295 * b
-- Mathlib.Order.Heyting.Hom
BiheytingHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} → [inst : BiheytingAlgebra α] → [inst_1 : BiheytingAlgebra β] → FunLike (BiheytingHom α β) α β
-- Mathlib.Algebra.BigOperators.Group.List.Defs
List.sum_replicate : ∀ {M : Type u_2} [inst : AddMonoid M] (n : ℕ) (a : M), (List.replicate n a).sum = n • a
-- Lean.Widget.UserWidget
Lean.Widget.instToJsonWidgetSource.toJson : Lean.Widget.WidgetSource → Lean.Json
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.subset_mul_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : MulOneClass α] (s : Finset α) {t : Finset α}, 1 ∈ t → s ⊆ s * t
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_left_mono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulRightMono α] {a : α}, Monotone fun x => x * a
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.instSemilinearIsometryEquivClass : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
  [inst_7 : Module R₂ E₂], SemilinearIsometryEquivClass (E ≃ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM` distributes over `<$>`, strongest postcondition version.
(Use this for reasoning forward from assumptions.)
 -/
SatisfiesM.map_post : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} {α_1 : Type u_1} {f : α → α_1} [inst : Functor m]
  [LawfulFunctor m] {x : m α}, SatisfiesM p x → SatisfiesM (fun b => ∃ a, p a ∧ b = f a) (f <$> x)
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `F : ι → X → α` of functions from a topological space to a uniform space is
*equicontinuous at `x₀ : X` within `S : Set X`* if, for all entourages `U ∈ 𝓤 α`, there is a
neighborhood `V` of `x₀` within `S` such that, for all `x ∈ V` and for all `i : ι`, `F i x` is
`U`-close to `F i x₀`.  -/
EquicontinuousWithinAt : {ι : Type u_1} →
  {X : Type u_3} → {α : Type u_6} → [tX : TopologicalSpace X] → [uα : UniformSpace α] → (ι → X → α) → Set X → X → Prop
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
NonUnitalIsometricContinuousFunctionalCalculus.mk : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : CommSemiring R] [inst_1 : Nontrivial R]
  [inst_2 : StarRing R] [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : NonUnitalRing A] [inst_7 : StarRing A] [inst_8 : MetricSpace A] [inst_9 : Module R A]
  [inst_10 : IsScalarTower R A A] [inst_11 : SMulCommClass R A A]
  [toNonUnitalContinuousFunctionalCalculus : NonUnitalContinuousFunctionalCalculus R A p],
  (∀ (a : A) (ha : p a), Isometry ⇑(cfcₙHom ha)) → NonUnitalIsometricContinuousFunctionalCalculus R A p
-- Mathlib.Analysis.Normed.Group.Basic
norm_mul_sub_norm_div_le_two_mul_min : ∀ {E : Type u_8} [inst : SeminormedCommGroup E] (u v : E), ‖u * v‖ - ‖u / v‖ ≤ 2 * min ‖u‖ ‖v‖
-- Mathlib.Tactic.CrossRefAttribute
/-- An optional comment supplied with the attribute.  -/
Mathlib.CrossRef.Tag.comment : Mathlib.CrossRef.Tag → String
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mk : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
              {X₁ Y₁ : C₁} →
                {f₁ : X₁ ⟶ Y₁} →
                  {X₃ Y₃ : C₃} →
                    {f₃ : X₃ ⟶ Y₃} →
                      (pt : C₂) →
                        (fst : pt ⟶ (G.obj (Opposite.op X₁)).obj X₃) →
                          (snd : pt ⟶ (G.obj (Opposite.op Y₁)).obj Y₃) →
                            CategoryTheory.IsPullback fst snd ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃) →
                              (π : (G.obj (Opposite.op Y₁)).obj X₃ ⟶ pt) →
                                autoParam (CategoryTheory.CategoryStruct.comp π fst = (G.map f₁.op).app X₃)
                                    CategoryTheory.Functor.PullbackObjObj.π_fst._autoParam →
                                  autoParam (CategoryTheory.CategoryStruct.comp π snd = (G.obj (Opposite.op Y₁)).map f₃)
                                      CategoryTheory.Functor.PullbackObjObj.π_snd._autoParam →
                                    G.PullbackObjObj f₁ f₃
-- Mathlib.Order.Monotone.Defs
strictAnti_of_le_iff_le : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  (∀ (x y : α), x ≤ y ↔ f y ≤ f x) → StrictAnti f