mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- A variant of `LeftHomotopy.compRight` useful for dealing with homotopy equivalences.  -/
CategoryTheory.Arrow.LeftHomotopy.compRightId : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {f : u ⟶ u} →
          CategoryTheory.Arrow.LeftHomotopy f (CategoryTheory.CategoryStruct.id u) →
            (g : u ⟶ v) → CategoryTheory.Arrow.LeftHomotopy (CategoryTheory.CategoryStruct.comp f g) g
-- Mathlib.RingTheory.SimpleRing.Defs
IsSimpleRing.mk : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R], IsSimpleOrder (TwoSidedIdeal R) → IsSimpleRing R
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A category has strong epi-mono factorisations if every morphism admits a strong epi-mono
factorisation.  -/
CategoryTheory.Limits.HasStrongEpiMonoFactorisations : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Algebra.Group.TypeTags.Basic
toAdd_ofAdd : ∀ {α : Type u} (x : α), Multiplicative.toAdd (Multiplicative.ofAdd x) = x
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
_private.Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds.0.HurwitzKernelBounds.isBigO_one_aux : (fun t => (1 - Real.exp (-Real.pi * t))⁻¹) =O[Filter.atTop] fun x => 1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast n))
  (h_3 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (x : Lean.Grind.CommRing.Expr) → motive x) (n : ℤ),
  a = Lean.Grind.CommRing.Expr.num n →
    (match a with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.intCast n => h_2 n
      | Lean.Grind.CommRing.Expr.natCast n => h_3 n
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | x => h_5 x) ≍
      h_1 n
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.colimitsOfShape_le_of_final : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {J' : Type u''} [inst_2 : CategoryTheory.Category.{v'', u''} J']
  (G : CategoryTheory.Functor J J') [G.Final], P.colimitsOfShape J' ≤ P.colimitsOfShape J
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₂ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive] (n : ℤ)
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((F.mapTriangleCommShiftIso n).inv.app X).hom₂ = (CategoryTheory.Functor.commShiftIso F n).inv.app X.obj₂
-- Mathlib.Algebra.Order.Archimedean.Basic
existsUnique_sub_zsmul_mem_Ioc : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G},
  0 < a → ∀ (b c : G), ∃! m, b - m • a ∈ Set.Ioc c (c + a)
-- Batteries.Data.List.Basic
List.takeWhile₂TR.go.eq_def : ∀ {α : Type u_1} {β : Type u_2} (R : α → β → Bool) (a : List α) (a_1 : List β) (a_2 : List α) (a_3 : List β),
  List.takeWhile₂TR.go R a a_1 a_2 a_3 =
    match a, a_1, a_2, a_3 with
    | a :: as, b :: bs, acca, accb =>
      bif R a b then List.takeWhile₂TR.go R as bs (a :: acca) (b :: accb) else (acca.reverse, accb.reverse)
    | x, x_1, acca, accb => (acca.reverse, accb.reverse)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.count_eq_forIn : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] {it : Std.IterM m β},
  it.length = forIn it { down := 0 } fun x acc => pure (ForInStep.yield { down := acc.down + 1 })
-- Mathlib.NumberTheory.NumberField.Units.Regulator
/-- Let `u` and `v` be two families of units. Assume that the subgroup `U` generated by `u` and
`torsion K` is contained in the subgroup `V` generated by `v` and `torsion K`. Then the ratio
`regOfFamily u / regOfFamily v` is equal to the index of `U` inside `V`.
 -/
NumberField.Units.regOfFamily_div_regOfFamily : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {u v : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ},
  NumberField.Units.IsMaxRank v →
    Subgroup.closure (Set.range u) ⊔ NumberField.Units.torsion K ≤
        Subgroup.closure (Set.range v) ⊔ NumberField.Units.torsion K →
      NumberField.Units.regOfFamily u / NumberField.Units.regOfFamily v =
        ↑((Subgroup.closure (Set.range u) ⊔ NumberField.Units.torsion K).relIndex
            (Subgroup.closure (Set.range v) ⊔ NumberField.Units.torsion K))
-- Mathlib.Analysis.Analytic.Binomial
Complex.one_div_sub_sq_sub_one_div_sq_hasFPowerSeriesOnBall_zero : ∀ (w x : ℂ),
  w ≠ x →
    HasFPowerSeriesOnBall (fun z => 1 / (z - w) ^ 2 - 1 / w ^ 2)
      (FormalMultilinearSeries.ofScalars ℂ fun i => (↑i + 1) * (w - x) ^ (-↑(i + 2)) - Nat.casesOn i (w ^ (-2)) 0) x
      ‖w - x‖ₑ
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.eval₂_C_mul_T_neg_n : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_3} [inst_1 : CommSemiring S] (f : R →+* S) (x : Sˣ) (r : R)
  (n : ℕ), (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.C r * LaurentPolynomial.T (-↑n)) = f r * ↑x⁻¹ ^ n
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_intCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : IntCast α] (m : ℤ),
  (Matrix.diagonal fun x => ↑m) = ↑m
-- Mathlib.Probability.Distributions.Gaussian.Fernique
ProbabilityTheory.IsGaussian.integral_dual : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E]
  (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = L (∫ (x : E), x ∂μ)
-- Mathlib.Algebra.Order.Ring.Idempotent
instOrderBotSubtypeIsIdempotentElem : {M₀ : Type u_2} → [inst : CommMonoidWithZero M₀] → OrderBot { a // IsIdempotentElem a }
-- Mathlib.Data.Fin.SuccPred
/-- Given a fixed pivot `p : Fin (n + 1)`, `p.succAbove` is injective.  -/
Fin.succAbove_right_injective : ∀ {n : ℕ} {p : Fin (n + 1)}, Function.Injective p.succAbove
-- Mathlib.RingTheory.Kaehler.TensorProduct
/-- The canonical isomorphism `(B ⊗[A] Ω[A⁄R]) ≃ₗ[B] Ω[B⁄S]` for `B = S ⊗[R] A`.
Also see `KaehlerDifferential.tensorKaehlerEquivBase` for the version with `S ⊗[R] Ω[A⁄R]`.  -/
KaehlerDifferential.tensorKaehlerEquiv : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      (B : Type u_4) →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : CommRing A] →
                [inst_4 : CommRing B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      [inst_7 : Algebra A B] →
                        [inst_8 : Algebra S B] →
                          [inst_9 : IsScalarTower R A B] →
                            [inst_10 : IsScalarTower R S B] →
                              [h : Algebra.IsPushout R S A B] → TensorProduct A B Ω[A⁄R] ≃ₗ[B] Ω[B⁄S]
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.comm₃₄_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂)
  {Z : C} (h : sq₂.X₄ ⟶ Z),
  CategoryTheory.CategoryStruct.comp sq₁.f₃₄ (CategoryTheory.CategoryStruct.comp self.τ₄ h) =
    CategoryTheory.CategoryStruct.comp self.τ₃ (CategoryTheory.CategoryStruct.comp sq₂.f₃₄ h)
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.instPreservesFiniteColimitsFunctorObjWhiskeringLeftOfHasFiniteColimits : ∀ {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)
  [CategoryTheory.Limits.HasFiniteColimits E],
  CategoryTheory.Limits.PreservesFiniteColimits ((CategoryTheory.Functor.whiskeringLeft C D E).obj F)
-- Init.Data.Float.Model.Float32
/-- Converts a `UInt32` to a `Float32.Model`, returning positive zero on zero.  -/
Float32.Model.ofUInt32 : UInt32 → Float32.Model
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- The inclusion `BifibrantObject C ⥤ C`, as a localizer morphism.  -/
HomotopicalAlgebra.BifibrantObject.localizerMorphism : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.LocalizerMorphism (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.BifibrantObject C))
        (HomotopicalAlgebra.weakEquivalences C)
-- Batteries.Data.Nat.Bisect
Nat.le_avg_left : ∀ {a b : ℕ}, a ≤ b → a ≤ a.avg b
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instStar : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddMonoid β] →
          [inst_3 : StarAddMonoid β] → [ContinuousStar β] → Star (CompactlySupportedContinuousMap α β)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
/-- Lower exponential growth as an `InfTopHom`.  -/
ExpGrowth.expGrowthInfTopHom : InfTopHom (ℕ → ENNReal) EReal
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_le_toIocMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a b ≤ toIocMod hp a b
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.isoOfι_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (t : CategoryTheory.Limits.Multifork I),
  t.isoOfι.inv.hom = CategoryTheory.CategoryStruct.id t.pt
-- Mathlib.RingTheory.PowerSeries.Exp
/-- Shows that
$\sum_{k = 0}^{n - 1} (e^{X})^k = \sum_{p = 0}^{\infty} \sum_{k = 0}^{n - 1} \frac{k^p}{p!}X^p$.  -/
PowerSeries.exp_pow_sum : ∀ {A : Type u_4} [inst : CommRing A] [inst_1 : Algebra ℚ A] (n : ℕ),
  ∑ k ∈ Finset.range n, PowerSeries.exp A ^ k =
    PowerSeries.mk fun p => ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p.factorial)⁻¹
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.isoEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y : C} (i : X ≅ Y), hF.isoEquiv i = F.mapIso i
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.ofArray_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a : Array ((a : α) × β a)},
  Std.DHashMap.Raw.ofArray a = ↑↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany a)
-- Init.Data.Array.InsertIdx
Array.insertIdx_comm : ∀ {α : Type u} (a b : α) {i j : ℕ} {xs : Array α} (x : i ≤ j) (x_1 : j ≤ xs.size),
  (xs.insertIdx i a ⋯).insertIdx (j + 1) b ⋯ = (xs.insertIdx j b x_1).insertIdx i a ⋯
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.re_ratCast : ∀ {K : Type u_1} [inst : Field K] {a b : K} (q : ℚ), (RatCast.ratCast q).re = ↑q
-- Init.Data.Nat.Lemmas
Nat.succ_mul_succ : ∀ (a b : ℕ), a.succ * b.succ = a * b + a + b + 1
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.fst_isEmbedding_of_right : ∀ {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S},
  Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g) →
    Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g))
-- Mathlib.Algebra.Category.Ring.Under.Limits
CommRingCat.Under.equalizerFork'_ι : ∀ {R : CommRingCat} {A B : Type u} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra (↑R) A]
  [inst_3 : Algebra (↑R) B] (f g : A →ₐ[↑R] B), (CommRingCat.Under.equalizerFork' f g).ι = (f.equalizer g).val.toUnder
-- Mathlib.Algebra.Group.TypeTags.Basic
/-- If `α` carries some additive structure, then `Multiplicative α` carries the corresponding
multiplicative structure.  -/
Multiplicative : Type u_1 → Type u_1
-- Mathlib.Order.Circular.ZMod
instCircularOrderFin : (n : ℕ) → CircularOrder (Fin n)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get!_union : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k)
-- Lean.Server.Requests
Lean.Server.routeLspRequest : String → Lean.Json → IO (Except Lean.Server.RequestError Lean.Lsp.DocumentUri)
-- Mathlib.RingTheory.Invariant.Basic
Algebra.IsInvariant.isIntegral : ∀ (A : Type u_1) (B : Type u_2) (G : Type u_3) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [Algebra.IsInvariant A B G] [Finite G], Algebra.IsIntegral A B
-- Mathlib.GroupTheory.OreLocalization.OreSet
AddOreLocalization.addOreSetComm_oreMin : ∀ {R : Type u_2} [inst : AddCommMonoid R] (S : AddSubmonoid R) (r : R) (s : ↥S), AddOreLocalization.oreMin r s = r
-- Mathlib.Logic.Encodable.Basic
Encodable.encode_none : ∀ {α : Type u_1} [inst : Encodable α], Encodable.encode none = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termF₁ : Lean.ParserDescr
-- Batteries.Data.Array.Basic
_private.Batteries.Data.Array.Basic.0.Array.scanlMFast.loop.congr_simp : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f f_1 : β → α → m β),
  f = f_1 →
    ∀ (init init_1 : β),
      init = init_1 →
        ∀ (as as_1 : Array α) (e_as : as = as_1) (start start_1 : USize),
          start = start_1 →
            ∀ (stop stop_1 : USize) (e_stop : stop = stop_1) (h_stop : stop.toNat ≤ as.size) (acc acc_1 : Array β),
              acc = acc_1 →
                Array.scanlMFast.loop✝ f init as start stop h_stop acc =
                  Array.scanlMFast.loop✝ f_1 init_1 as_1 start_1 stop_1 ⋯ acc_1
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_addNat_Icc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (fun x => x.addNat m) (Finset.Icc i j) = Finset.Icc (i.addNat m) (j.addNat m)
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {Z : C} (h : CategoryTheory.Limits.cokernel S.f ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.abelianImageToKernel
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π S.f) h)) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xy_succ_succ : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ),
  Pell.xn a1 (n + 2) + Pell.xn a1 n = 2 * a * Pell.xn a1 (n + 1) ∧
    Pell.yn a1 (n + 2) + Pell.yn a1 n = 2 * a * Pell.yn a1 (n + 1)
-- Lean.Expr
/-- Remove `outParam`, `optParam`, and `autoParam` applications/annotations from `e`.
Note that it does not remove nested annotations.
Examples:
- Given `e` of the form `outParam (optParam Nat b)`, `consumeTypeAnnotations e = b`.
- Given `e` of the form `Nat → outParam (optParam Nat b)`, `consumeTypeAnnotations e = e`.
 -/
Lean.Expr.consumeTypeAnnotations : Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShift_leftUnshift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {a n' : ℤ}
  (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ)
  (hn' : n + a = n'), (γ.leftUnshift n hn').leftShift a n' hn' = γ
-- Init.Data.UInt.Bitwise
UInt16.ofBitVec_shiftLeft_mod : ∀ (a : BitVec 16) (b : ℕ), { toBitVec := a <<< (b % 16) } = { toBitVec := a } <<< UInt16.ofNat b
-- Lean.Expr
/-- Return `some e'` if `e` is of the form `autoParam _ e'`  -/
Lean.Expr.getAutoParamTactic? : Lean.Expr → Option Lean.Expr
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.congr : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f g : α → β} {a : α},
  IsLocalMin f a → f =ᶠ[nhds a] g → IsLocalMin g a
-- Aesop.RuleSet
Aesop.GlobalRuleSet.mk.injEq : ∀ (toBaseRuleSet : Aesop.BaseRuleSet) (simpTheorems : Lean.Meta.SimpTheorems) (simprocs : Lean.Meta.Simprocs)
  (toBaseRuleSet_1 : Aesop.BaseRuleSet) (simpTheorems_1 : Lean.Meta.SimpTheorems) (simprocs_1 : Lean.Meta.Simprocs),
  ({ toBaseRuleSet := toBaseRuleSet, simpTheorems := simpTheorems, simprocs := simprocs } =
      { toBaseRuleSet := toBaseRuleSet_1, simpTheorems := simpTheorems_1, simprocs := simprocs_1 }) =
    (toBaseRuleSet = toBaseRuleSet_1 ∧ simpTheorems = simpTheorems_1 ∧ simprocs = simprocs_1)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.map_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid N']
  [inst_8 : Module R N] [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g] (h : M →ₗ[R] N)
  (x : M), ((IsLocalizedModule.map S f g) h) (f x) = g (h x)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Functor.prod'CompFst_hom_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B)
  (G : CategoryTheory.Functor A C) (X : A), (F.prod'CompFst G).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.NumberTheory.ZetaValues
hasSum_zeta_two : HasSum (fun n => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6)
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.llp_rlp_llp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C), T.llp.rlp.llp = T.llp
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_mono : ∀ {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  a ≤ b →
    IntervalIntegrable f μ a b →
      IntervalIntegrable g μ a b → f ≤ g → ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL.match_5.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (rs : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l_1 : Std.DTreeMap.Internal.Impl α β) →
      l_1.Balanced →
        Std.DTreeMap.Internal.Impl.BalanceLPrecond l_1.size (Std.DTreeMap.Internal.Impl.inner rs k v l r).size →
          Sort u_3)
  (l_1 : Std.DTreeMap.Internal.Impl α β) (hlb : l_1.Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l_1.size (Std.DTreeMap.Internal.Impl.inner rs k v l r).size)
  (h_1 :
    (hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr :
          Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
            (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
        motive Std.DTreeMap.Internal.Impl.leaf hlb hlr)
  (h_2 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) →
            (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLPrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) hlb hlr)
  (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β)
  (hlb_1 : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced)
  (hlr_1 :
    Std.DTreeMap.Internal.Impl.BalanceLPrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
      (Std.DTreeMap.Internal.Impl.inner rs k v l r).size),
  l_1 = Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr →
    hlb ≍ hlb_1 →
      hlr ≍ hlr_1 →
        (match l_1, hlb, hlr with
          | Std.DTreeMap.Internal.Impl.leaf, hlb, hlr => h_1 hlb hlr
          | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr, hlb, hlr => h_2 ls lk lv ll lr hlb hlr) ≍
          h_2 ls lk lv ll lr hlb_1 hlr_1
-- Mathlib.Data.Finset.Sups
Finset.sups_comm : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] (s t : Finset α), s ⊻ t = t ⊻ s
-- Mathlib.Topology.Algebra.Indicator
IsClopen.continuous_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  [inst_2 : Zero β], IsClopen s → Continuous f → Continuous (s.indicator f)
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.comp_id : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] (f : E₁ →ₚ[R] E₂), f.comp (PositiveLinearMap.id R E₁) = f
-- Std.Time.DateTime.PlainDateTime
Std.Time.instInhabitedPlainDateTime.default : Std.Time.PlainDateTime
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.uniformContinuous_ofSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : UniformSpace X],
  UniformContinuous ⇑Metric.Snowflaking.ofSnowflaking
-- Mathlib.Data.List.Rotate
List.rotate_eq_rotate : ∀ {α : Type u} {l l' : List α} {n : ℕ}, l.rotate n = l'.rotate n ↔ l = l'
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_comp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ l₃ : c ⟶ d} {r₁ r₂ r₃ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂)
  (adj₃ : CategoryTheory.Bicategory.Adjunction l₃ r₃) (α : l₂ ⟶ l₁) (β : l₃ ⟶ l₂),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂) α)
      ((CategoryTheory.Bicategory.conjugateEquiv adj₂ adj₃) β) =
    (CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₃) (CategoryTheory.CategoryStruct.comp β α)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.mk : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashMap.Node α β → Lean.PersistentHashMap α β
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.re_add_im : ∀ (z : UpperHalfPlane), ↑z.re + ↑z.im * Complex.I = ↑z
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.mk.injEq : ∀ {α : Type} (state state_1 : Std.Mutex (Std.Bounded.State✝ α)),
  ({ state := state } = { state := state_1 }) = (state = state_1)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.exists_eq_pow_of_exponent_coprime_of_pow_eq_pow : ∀ {a b m n : ℕ}, m.Coprime n → a ^ m = b ^ n → ∃ c, a = c ^ n ∧ b = c ^ m
-- Mathlib.Order.Defs.LinearOrder
LinearOrder.toMax : {α : Type u_2} → [self : LinearOrder α] → Max α
-- Mathlib.Algebra.GroupWithZero.Subgroup
Subgroup.mem_inv_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {G : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Group G] [inst_2 : MulDistribMulAction G₀ G]
  {a : G₀}, a ≠ 0 → ∀ (S : Subgroup G) (x : G), x ∈ a⁻¹ • S ↔ a • x ∈ S
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.intPow_ofNat : ∀ {a b c : ℕ}, a.pow b = c → (Int.ofNat a).pow b = Int.ofNat c
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.instInhabitedBodyState.default : Std.Http.Protocol.H1.Reader.BodyState