mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ratUnits = #[] ∧ f.assignments.size = n →
    ∀ (p : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHints : Array (ℕ × Array ℕ))
      (i : Fin ratHints.size),
      (Array.foldl (fun acc ratHint => if acc.2 = true then acc.1.performRatCheck p ratHint else (acc.1, false))
              (f, true) ratHints).2 =
          true →
        (f.performRatCheck p ratHints[i]).2 = true
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.recF_eq' : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β)
  (x : (MvQPF.P F).W α),
  MvQPF.recF g x = g (MvQPF.abs (MvFunctor.map (TypeVec.id ::: MvQPF.recF g) ((MvQPF.P F).wDest' x)))
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.truncGE.rightHomologyMapData_φH : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] {i j k : ι} {j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i)
  (hk : c.next j = k) (hj : e.BoundaryGE j),
  (HomologicalComplex.truncGE.rightHomologyMapData K e hj' hi hk hj).φH =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.RightHomologyData.canonical (K.sc j')).H
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Group.card_pow_eq_card_pow_card_univ : ∀ {G : Type u_5} [inst : Group G] [inst_1 : Fintype G] (S : Set G) [inst_2 : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k]
  (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.final_iff_comp_final_full_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [G.Final] [G.Full] [G.Faithful], F.Final ↔ (F.comp G).Final
-- Std.Http.Data.Headers.Value
Std.Http.Header.instReprValue : Repr Std.Http.Header.Value
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.norm_def : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (z : QuadraticAlgebra R a b),
  QuadraticAlgebra.norm z = z.re * z.re + b * z.re * z.im - a * z.im * z.im
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
_private.Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass.0.CategoryTheory.ShortComplex.ShortExact.termQis : Lean.ParserDescr
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.ElimAltInfo.mk.injEq : ∀ (name : Lean.Name) (declName? : Option Lean.Name) (numFields : ℕ) (provesMotive : Bool) (name_1 : Lean.Name)
  (declName?_1 : Option Lean.Name) (numFields_1 : ℕ) (provesMotive_1 : Bool),
  ({ name := name, declName? := declName?, numFields := numFields, provesMotive := provesMotive } =
      { name := name_1, declName? := declName?_1, numFields := numFields_1, provesMotive := provesMotive_1 }) =
    (name = name_1 ∧ declName? = declName?_1 ∧ numFields = numFields_1 ∧ provesMotive = provesMotive_1)
-- Init.Prelude
ShiftRight.mk : {α : Type u} → (α → α → α) → ShiftRight α
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.sum_map_le_apply_prod : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : AddMonoid β] [inst_2 : Preorder β] [AddLeftMono β]
  (l : List α) (f : α → β), 0 ≤ f 1 → (∀ (a b : α), f a + f b ≤ f (a * b)) → (List.map f l).sum ≤ f l.prod
-- Mathlib.Algebra.Group.Action.Units
Units.instSMul.eq_1 : ∀ {M : Type u_3} {α : Type u_5} [inst : Monoid M] [inst_1 : SMul M α], Units.instSMul = { smul := fun m a => ↑m • a }
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Makes the identity additive isomorphism from a proof two
subsemigroups of an additive semigroup are equal.  -/
AddEquiv.subsemigroupCongr : {M : Type u_1} → [inst : Add M] → {S T : AddSubsemigroup M} → S = T → ↥S ≃+ ↥T
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.neg_def : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (P : W'.Point), -P = P.neg
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constAlter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ (k : α) (f : Option β → Option β),
          (Std.DTreeMap.Raw.Const.alter t₁ k f).Equiv (Std.DTreeMap.Raw.Const.alter t₂ k f)
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.toPreValuationRing : ∀ {A : Type u} {inst : CommRing A} {inst_1 : IsDomain A} [self : ValuationRing A], PreValuationRing A
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)}
  {he : (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.isEmpty = false},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.minKey he = k ↔
    (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k k').isLE = true
-- Mathlib.Probability.Moments.IntegrableExpMul
ProbabilityTheory.sub_half_inf_sub_mem_Ioo : ∀ {l u v : ℝ}, v ∈ Set.Ioo l u → v - min (v - l) (u - v) / 2 ∈ Set.Ioo l u
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.log_apply : ∀ {n : ℕ}, ArithmeticFunction.log n = Real.log ↑n
-- Mathlib.Order.ScottContinuity
ScottContinuousOn.const : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {D : Set (Set α)} (x : β),
  ScottContinuousOn D (Function.const α x)
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckGroup.instInv.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M],
  Algebra.GrothendieckGroup.instInv = { inv := fun x => Localization.rec (fun m s => Localization.mk ↑s ⟨m, ⋯⟩) ⋯ x }
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
BoxIntegral.Box.Ioo_ae_eq_Icc : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) [inst : Fintype ι],
  BoxIntegral.Box.Ioo I =ᵐ[MeasureTheory.volume] BoxIntegral.Box.Icc I
-- Mathlib.Topology.Order
instIndiscreteTopologyOfSubsingleton : ∀ {α : Type u} [inst : TopologicalSpace α] [Subsingleton α], IndiscreteTopology α
-- Mathlib.GroupTheory.Congruence.Defs
AddConGen.Rel.below.symm : ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {motive : (a a_1 : M) → AddConGen.Rel r a a_1 → Prop} {x y : M}
  (a : AddConGen.Rel r x y), AddConGen.Rel.below a → motive x y a → AddConGen.Rel.below ⋯
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_hom_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.unop =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Opposite.unop X)).inv
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.left : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → C → CategoryTheory.Join C D
-- Mathlib.Topology.Compactness.Compact
IsCompact.nhdsSet_inf_eq_biSup : ∀ {X : Type u} [inst : TopologicalSpace X] {K : Set X},
  IsCompact K → ∀ (l : Filter X), nhdsSet K ⊓ l = ⨆ x ∈ K, nhds x ⊓ l
-- Plausible.Random
Plausible.Random.instBoundedRandomBitVec : {m : Type → Type u_1} → [Monad m] → {n : ℕ} → Plausible.BoundedRandom m (BitVec n)
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- `AddMonoidAlgebra.mapDomain` as a linear map.  -/
AddMonoidAlgebra.mapDomainLinearMap : (R : Type u_1) →
  (S : Type u_2) →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] → [inst_2 : Module R S] → (M → N) → AddMonoidAlgebra S M →ₗ[R] AddMonoidAlgebra S N
-- Init.Data.Float.Model.Unpacked.Round
/-- Pairs a mantissa with two residual bits, the 'round bit' and the 'sticky bit',
which carry precisely the required information to compute the `Accuracy` of the
mantissa.
 -/
Float.Model.UnpackedFloat.ExtendedMantissa : Type
-- Mathlib.Analysis.Normed.Operator.CompleteCodomain
LinearMap.mkContinuous₂.congr_simp : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] (f f_1 : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) (e_f : f = f_1) (C C_1 : ℝ) (e_C : C = C_1)
  (hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖), f.mkContinuous₂ C hC = f_1.mkContinuous₂ C_1 ⋯
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
/-- Given a localizer morphism `Φ : LocalizerMorphism W₁ W₂` between
morphism properties on `C₁` and `C₂`, and a functor `C₂ ⥤ H`, this
is the property that `W₁` is inverted by `Φ.functor ⋙ F`.
In case `Φ` is a (left/right) derivability structure, this allows
the construction of a derived functor for `F` relatively to `W₂`.  -/
CategoryTheory.LocalizerMorphism.Derives : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {H : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} H] →
            {W₁ : CategoryTheory.MorphismProperty C₁} →
              {W₂ : CategoryTheory.MorphismProperty C₂} →
                CategoryTheory.LocalizerMorphism W₁ W₂ → CategoryTheory.Functor C₂ H → Prop
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsAlt.neg_eq : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B₁ : LinearMap.BilinForm R₁ M₁}, B₁.IsAlt → ∀ (x y : M₁), -(B₁ x) y = (B₁ y) x
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_le_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] {f : Filter β} {u v : β → α},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a) ↔
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u ∧ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  [inst_3 : Inhabited α] {l : List α} {k : α}, l.contains k = false → (Std.ExtTreeSet.ofList l cmp).get! k = default
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.hFunctor_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (i : ι) {X Y : TopPair.HomologyPretheory C c} (f : X ⟶ Y),
  (TopPair.HomologyPretheory.hFunctor i).map f = f.hom i
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_zero : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S), Polynomial.map f 0 = 0
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.instMembershipProdReal : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Membership (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl)
      (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl)
-- Lean.Environment
/-- Function to transform state into data that should be imported into other modules. Returns entries
for all three olean levels at once so that expensive computations can be shared. When using the
module system without `import all`, `OLeanLevel.exported` is imported, else `OLeanLevel.private`.
Additionally, when using the module system in the language server, the `OLeanLevel.server` data is
accessible via `getModuleEntries (level := .server)`. By convention, each level should include all
data of previous levels.

This function is run once after elaborating the file and joining all asynchronous threads.
For non-module files, only the `private` field is used.
 -/
Lean.PersistentEnvExtensionDescrCore.exportEntriesFnEx : {α β σ : Type} → Lean.PersistentEnvExtensionDescrCore α β σ → Lean.Environment → σ → Lean.OLeanEntries (Array α)
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.instHasShiftInt : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.HasShift (CochainComplex C ℤ) ℤ
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.ofSimplex₀_map : ∀ {X Y : SSet} (f : X ⟶ Y) (x : X.obj (Opposite.op { len := 0 })) (y : Y.obj (Opposite.op { len := 0 }))
  (h : (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x = y),
  (SSet.RelativeMorphism.ofSimplex₀ f x y h).map = f
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.UnpackedFloat.zero.inj : ∀ {sign sign_1 : Float.Model.UnpackedFloat.Sign},
  Float.Model.UnpackedFloat.zero sign = Float.Model.UnpackedFloat.zero sign_1 → sign = sign_1
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The right homology map data associated to the identity morphism of a short complex.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.id : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.RightHomologyData) →
          CategoryTheory.ShortComplex.RightHomologyMapData (CategoryTheory.CategoryStruct.id S) h h
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The induced map from the quotient by the kernel to the codomain.  -/
QuotientGroup.kerLift : {G : Type u} → [inst : Group G] → {H : Type v} → [inst_1 : Group H] → (φ : G →* H) → G ⧸ φ.ker →* H
-- Mathlib.Data.List.Perm.Basic
List.perm_rfl : ∀ {α : Type u_1} {l : List α}, l.Perm l
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_exact : Bool → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.DiseqCnstr → Lean.Meta.Grind.AC.DiseqCnstrProof
-- Mathlib.Algebra.Group.Action.Defs
vadd_add_assoc : ∀ {α : Type u_5} {β : Type u_6} [inst : Add β] [inst_1 : VAdd α β] [VAddAssocClass α β β] (r : α) (x y : β),
  (r +ᵥ x) + y = r +ᵥ x + y
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
le_of_forall_pos_lt_add' : ∀ {α : Type u} [inst : LinearOrder α] [DenselyOrdered α] [inst_2 : AddMonoid α] [ExistsAddOfLE α] [AddLeftReflectLT α]
  {a b : α}, (∀ (ε : α), 0 < ε → a < b + ε) → a ≤ b
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.multiplicity.eq_1 : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : FermatLastTheoremForThreeGen.Solution'✝ hζ),
  FermatLastTheoremForThreeGen.Solution'.multiplicity✝ S' =
    multiplicity (hζ.toInteger - 1) (FermatLastTheoremForThreeGen.Solution'.c✝ S')
-- Mathlib.Algebra.Category.Ring.Under.Property
RingHom.HasFiniteProducts.preservesFiniteProducts_pushout : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => Q) →
      ∀ [inst : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q).IsStableUnderCobaseChange]
        {R S : CommRingCat} (f : R ⟶ S),
        CategoryTheory.Limits.PreservesFiniteProducts
          (CategoryTheory.MorphismProperty.Under.pushout
            (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q) ⊤ f)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- `FreeAddGroupBasis.ofRepr` constructs a basis given an equivalence with an additive free
group.  -/
FreeAddGroupBasis.ofRepr : {ι : Type u_1} → {G : Type u_2} → [inst : AddGroup G] → G ≃+ FreeAddGroup ι → FreeAddGroupBasis ι G
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.mkFreeVarMap : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadMCtx m] →
      Array Lean.Expr →
        Array Lean.FVarId →
          Array Lean.FVarId → Array Lean.Elab.Term.LetRecToLift → m Lean.Elab.Term.MutualClosure.FreeVarMap
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instReprTransferEncoding : Repr Std.Http.Header.TransferEncoding
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The space `Fin 2 → α` is measurably equivalent to `α × α`.  -/
MeasurableEquiv.finTwoArrow : {α : Type u_1} → [inst : MeasurableSpace α] → (Fin 2 → α) ≃ᵐ α × α
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.mapRingEquiv_apply : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : UniformSpace α] [inst_2 : IsTopologicalRing α] [inst_3 : IsUniformAddGroup α]
  {β : Type u} [inst_4 : UniformSpace β] [inst_5 : Ring β] [inst_6 : IsUniformAddGroup β] [inst_7 : IsTopologicalRing β]
  (f : α ≃+* β) (hf : Continuous ⇑f) (hf' : Continuous ⇑f.symm) (a : UniformSpace.Completion α),
  (UniformSpace.Completion.mapRingEquiv f hf hf') a = UniformSpace.Completion.map (⇑f) a
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexLinearEquiv_one : ∀ {m : Type u_2} {m' : Type u_6} (R : Type u_11) (A : Type u_12) [inst : Semiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : Module R A] [inst_3 : DecidableEq m] [inst_4 : DecidableEq m'] [inst_5 : One A] (e : m ≃ m'),
  (Matrix.reindexLinearEquiv R A e e) 1 = 1
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params.mk.sizeOf_spec : ∀ (config : Lean.Grind.Config) (extensions : Lean.Meta.Grind.ExtensionStateArray)
  (extra : Lean.PArray Lean.Meta.Grind.EMatchTheorem) (extraInj : Lean.PArray Lean.Meta.Grind.InjectiveTheorem)
  (extraFacts : Lean.PArray Lean.Expr) (symPrios : Lean.Meta.Grind.SymbolPriorities) (norm : Lean.Meta.Simp.Context)
  (normProcs : Array Lean.Meta.Simprocs) (anchorRefs? : Option (Array Lean.Meta.Grind.AnchorRef)),
  sizeOf
      { config := config, extensions := extensions, extra := extra, extraInj := extraInj, extraFacts := extraFacts,
        symPrios := symPrios, norm := norm, normProcs := normProcs, anchorRefs? := anchorRefs? } =
    1 + sizeOf config + sizeOf extensions + sizeOf extra + sizeOf extraInj + sizeOf extraFacts + sizeOf symPrios +
          sizeOf norm +
        sizeOf normProcs +
      sizeOf anchorRefs?
-- Mathlib.GroupTheory.Coxeter.Matrix
CoxeterMatrix.off_diagonal : ∀ {B : Type u_1} (self : CoxeterMatrix B) (i i' : B), i ≠ i' → self.M i i' ≠ 1
-- Mathlib.Data.Bracket
/-- `⁅x, y⁆` is the result of a bracket operation on elements `x` and `y`.
It is supported by the `Bracket` typeclass.  -/
Bracket.bracket : {L : Type u_1} → {M : Type u_2} → [self : Bracket L M] → L → M → M
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `MultipliableUniformlyOn f s` means that there is some infinite product to which
`f` converges uniformly on `s`. Use `fun x ↦ ∏' i, f i x` to get the product function.  -/
MultipliableUniformlyOn : {α : Type u_1} → {β : Type u_2} → {ι : Type u_3} → [CommMonoid α] → (ι → β → α) → Set β → [UniformSpace α] → Prop
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_inverse : ∀ {R : Type u} [inst : Monoid R] {A : Type v} [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A]
  {B₁ : Type u_2} [inst_3 : NonUnitalNonAssocSemiring B₁] [inst_4 : DistribMulAction R B₁] (f : A →ₙₐ[R] B₁)
  (g : B₁ → A) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f), ⇑(f.inverse g h₁ h₂) = g
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsNonloopAt.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (x : α), G.IsNonloopAt e x = ∃ y, y ≠ x ∧ G.IsLink e x y
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.mem_carrier : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {s : NonUnitalSubalgebra R A} {x : A}, x ∈ s.carrier ↔ x ∈ s
-- Lean.Elab.Do.Basic
/-- Look up a declared `mut` variable by its raw `Name`.  -/
Lean.Elab.Do.findMutVar? : Lean.Name → Lean.Elab.Do.DoElabM (Option Lean.Elab.Do.MutVar)
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.empty : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X], Convexity.IsConvexSet R ∅
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.isRkFinite_insert_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {e : α}, M.IsRkFinite (insert e X) ↔ M.IsRkFinite X
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The braiding isomorphism is symmetric.  -/
CategoryTheory.Limits.prod.symmetry_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : C) [inst_1 : CategoryTheory.Limits.HasBinaryProduct P Q]
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct Q P] {Z : C} (h : P ⨯ Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding P Q).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding Q P).hom h) =
    h
-- Mathlib.Order.Bounds.Basic
IsLeast.insert : ∀ {γ : Type u_3} [inst : LinearOrder γ] (a : γ) {b : γ} {s : Set γ}, IsLeast s b → IsLeast (insert a s) (min a b)
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.Finite.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] (it it_1 : Std.IterM m β),
  ({ it := it } = { it := it_1 }) = (it = it_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharNeTwoNF.mk : ∀ {R : Type u_1} [inst : CommRing R] {W : WeierstrassCurve R}, W.a₁ = 0 → W.a₃ = 0 → W.IsCharNeTwoNF
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.rankOne_hom'_def`. -/
NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R],
  Valuation.RankLeOne.hom' Valued.v =
    (WithZeroMulInt.toNNReal ⋯).comp
      (Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt Valued.v).toMonoidWithZeroHom
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ioo_succ_right_eq_Ioc_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {b : α},
  ¬IsMax b → ∀ (a : α), Set.Ioo a (Order.succ b) = Set.Ioc a b
-- Init.Data.Int.Linear
Int.Internal.Linear.le_eq_false : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr),
  (lhs.sub rhs).norm.isUnsatLe = true →
    (Int.Internal.Linear.Expr.denote ctx lhs ≤ Int.Internal.Linear.Expr.denote ctx rhs) = False
-- Mathlib.Data.FunLike.IsApply
IsMulApply.mul_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Mul β}
  {inst_2 : Mul F} [self : IsMulApply F α β] (f g : F) (x : α), (f * g) x = f x * g x
-- Mathlib.Data.Rat.Defs
Rat.divInt_mul_divInt_cancel : ∀ {x : ℤ}, x ≠ 0 → ∀ (n d : ℤ), Rat.divInt n x * Rat.divInt x d = Rat.divInt n d
-- Init.Data.Order.Factories
/-- Derives a `LawfulOrderMin α` instance for `LE.ofLT` from two properties involving
`LT α` and `Min α` instances.

The produced instance entails `LawfulOrderInf α` and `MinEqOr α`.
 -/
Std.LawfulOrderMin.of_lt : ∀ {α : Type u} [inst : Min α] [inst_1 : LT α],
  (∀ (a b c : α), b ⊓ c < a ↔ b < a ∨ c < a) → (∀ (a b : α), a ⊓ b = a ∨ a ⊓ b = b) → Std.LawfulOrderMin α
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.nlt.injEq : ∀ (lhs rhs : ℕ) (proof : Lean.Expr) (lhs_1 rhs_1 : ℕ) (proof_1 : Lean.Expr),
  (Mathlib.Tactic.Order.AtomicFact.nlt lhs rhs proof = Mathlib.Tactic.Order.AtomicFact.nlt lhs_1 rhs_1 proof_1) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1)
-- Batteries.Data.List.Lemmas
List.getElem_getElem_idxsOf_sub : ∀ {α : Type u_1} {i : ℕ} {xs : List α} {x : α} [inst : BEq α] (s : ℕ) (h : i < (List.idxsOf x xs s).length),
  (xs[(List.idxsOf x xs s)[i] - s] == x) = true