mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
    (∀ a ∈ t, l.contains a = false) → (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).size = t.size + l.length
-- Mathlib.Combinatorics.Quiver.Push
Quiver.PushQuiver.arrow.inj : ∀ {V : Type u} {inst : Quiver V} {W : Type u₂} {σ : V → W} {X Y : V} {f f_1 : X ⟶ Y},
  Quiver.PushQuiver.arrow f = Quiver.PushQuiver.arrow f_1 → f = f_1
-- Init.Data.SInt.Lemmas
ISize.sub_lt : ∀ {a b : ISize}, 0 < b → b ≤ a → a - b < a
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.generator_mem : ∀ {R : Type u} {M : Type v} [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M] (S : Submodule R M)
  [inst_3 : S.IsPrincipal], Submodule.IsPrincipal.generator S ∈ S
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The canonical isomorphism `S.op.homology ≅ Opposite.op S.homology` when a short
complex `S` has homology.  -/
CategoryTheory.ShortComplex.homologyOpIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasHomology] → S.op.homology ≅ Opposite.op S.homology
-- Mathlib.Topology.Order.PartialSups
ContinuousAt.partialSups : ∀ {L : Type u_1} [inst : SemilatticeSup L] [inst_1 : TopologicalSpace L] [ContinuousSup L] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : ℕ → X → L} {n : ℕ} {x : X},
  (∀ k ≤ n, ContinuousAt (f k) x) → ContinuousAt ((partialSups f) n) x
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_eq : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : Subsingleton αˣ] (x : α), normalize x = x
-- Mathlib.Tactic.Module
/-- Given two terms `l₁`, `l₂` of type `qNF R M`, i.e. lists of `(Q($R) × Q($M)) × ℕ`s (two `Expr`s
and a natural number), construct another such term `l`, which will have the property that in the
`$R`-module `$M`, the difference of the "linear combinations" represented by `l₁` and `l₂` is the
linear combination represented by `l`.

The construction assumes, to be valid, that the lists `l₁` and `l₂` are in strictly increasing order
by `ℕ`-component, and that if pairs `(a₁, x₁)` and `(a₂, x₂)` appear in `l₁`, `l₂` respectively with
the same `ℕ`-component `k`, then the expressions `x₁` and `x₂` are equal.

The construction is as follows: merge the first list and the negation of the second list, except
that if pairs `(a₁, x₁)` and `(a₂, x₂)` appear in `l₁`, `l₂` respectively with the same
`ℕ`-component `k`, then contribute a term `(a₁ - a₂, x₁)` to the output list with `ℕ`-component `k`.
 -/
Mathlib.Tactic.Module.qNF.sub : {u v : Lean.Level} →
  {M : Q(Type v)} →
    {R : Q(Type u)} →
      Q(Ring «$R») → Mathlib.Tactic.Module.qNF R M → Mathlib.Tactic.Module.qNF R M → Mathlib.Tactic.Module.qNF R M
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.eq_of_grevlex : ∀ {m₁ m₂ : Lean.Grind.CommRing.Mon}, m₁.grevlex m₂ = Ordering.eq → m₁ = m₂
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.modifyState.unsafe_11 : {σ : Type} → Lean.EnvExtension σ → (σ → σ) → Lean.Kernel.Environment → Array Lean.EnvExtensionState
-- Mathlib.Analysis.Matrix.Normed
/-- This applies to the sup norm of sup norm.  -/
Matrix.isBoundedSMul : ∀ {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedRing R] [inst_3 : SeminormedAddCommGroup α] [inst_4 : Module R α] [IsBoundedSMul R α],
  IsBoundedSMul R (Matrix m n α)
-- Mathlib.NumberTheory.ModularForms.Petersson
/-- The integrand in the Petersson scalar product of two modular forms.  -/
UpperHalfPlane.petersson : ℤ → (UpperHalfPlane → ℂ) → (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂ
-- Mathlib.Analysis.Normed.Group.Constructions
/-- The seminorm of an element in a product space is `< r` if and only
if the norm of each component is.  -/
pi_norm_lt_iff : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i}
  {r : ℝ}, 0 < r → (‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r)
-- Mathlib.RingTheory.FiniteType
/-- If `R[M]` is of finite type, then there is a `G : Finset M` such that its
image generates, as algebra, `R[M]`.  -/
AddMonoidAlgebra.exists_finset_adjoin_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddMonoid M]
  [h : Algebra.FiniteType R (AddMonoidAlgebra R M)], ∃ G, Algebra.adjoin R (AddMonoidAlgebra.of' R M '' ↑G) = ⊤
-- Init.Data.Int.DivMod.Bootstrap
Int.ediv.eq_5 : ∀ (m n : ℕ), (Int.negSucc m).ediv (Int.negSucc n) = Int.ofNat (m / n.succ).succ
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.map_id_c_app : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) (j : J)
  (U : (TopologicalSpace.Opens ↑↑(F.obj j))ᵒᵖ),
  (F.map (CategoryTheory.CategoryStruct.id j)).c.app U =
    CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.Pushforward.id (F.obj j).presheaf).inv.app U)
      ((TopCat.Presheaf.pushforwardEq ⋯ (F.obj j).presheaf).hom.app U)
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.iff_of_equiv_comm : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {f : M →ₗ[R] N} {P : Type u_2} {Q : Type u_3}
  [inst_9 : AddCommMonoid P] [inst_10 : Module R P] [inst_11 : AddCommMonoid Q] [inst_12 : Module S Q]
  [inst_13 : Module R Q] [inst_14 : IsScalarTower R S Q] {f' : P →ₗ[R] Q} (eM : M ≃ₗ[R] P) (eN : N ≃ₗ[S] Q),
  f' ∘ₗ ↑eM = ↑(LinearEquiv.restrictScalars R eN) ∘ₗ f → (IsBaseChange S f ↔ IsBaseChange S f')
-- Mathlib.Analysis.Calculus.Deriv.Abs
DifferentiableWithinAt.abs : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E},
  DifferentiableWithinAt ℝ f s x → f x ≠ 0 → DifferentiableWithinAt ℝ (fun x => |f x|) s x
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- On an empty space, bounded continuous functions are at distance 0.  -/
BoundedContinuousFunction.dist_zero_of_empty : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β} [IsEmpty α], dist f g = 0
-- Init.Data.Int.Linear
Int.Internal.Linear.not_le_of_le_cert.induct_unfolding : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool → Prop),
  (∀ (k : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly) (k_1 : ℤ),
      motive (Int.Internal.Linear.Poly.add k v p) (Int.Internal.Linear.Poly.num k_1) false) →
    (∀ (k k_1 : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
        motive (Int.Internal.Linear.Poly.num k) (Int.Internal.Linear.Poly.add k_1 v p) false) →
      (∀ (c₁ c₂ : ℤ),
          motive (Int.Internal.Linear.Poly.num c₁) (Int.Internal.Linear.Poly.num c₂) (decide (c₁ ≥ 1 - c₂))) →
        (∀ (a₁ : ℤ) (x₁ : Int.Internal.Linear.Var) (p₁ : Int.Internal.Linear.Poly) (a₂ : ℤ)
            (x₂ : Int.Internal.Linear.Var) (p₂ : Int.Internal.Linear.Poly),
            motive p₁ p₂ (Int.Internal.Linear.not_le_of_le_cert p₁ p₂) →
              motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂)
                (a₁ == -a₂ && x₁ == x₂ && Int.Internal.Linear.not_le_of_le_cert p₁ p₂)) →
          ∀ (p₁ p₂ : Int.Internal.Linear.Poly), motive p₁ p₂ (Int.Internal.Linear.not_le_of_le_cert p₁ p₂)
-- Mathlib.RingTheory.TensorProduct.Maps
/-- If A and B are both R- and S-algebras and their actions on them commute,
and if the S-action on `A ⊗[R] B` can switch between the two factors, then there is a
canonical T-algebra homomorphism from `A ⊗[S] B` to `A ⊗[R] B`,
where `T` is any other ring acting on `A` and whose action commutes with the `R` and `S`-actions.  -/
Algebra.TensorProduct.mapOfCompatibleSMul : (R : Type u_3) →
  (S : Type u_4) →
    (T : Type u_5) →
      (A : Type u_6) →
        (B : Type u_7) →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : CommSemiring T] →
                [inst_3 : Semiring A] →
                  [inst_4 : Semiring B] →
                    [inst_5 : Algebra R A] →
                      [inst_6 : Algebra R B] →
                        [inst_7 : Algebra S A] →
                          [inst_8 : Algebra S B] →
                            [inst_9 : Algebra T A] →
                              [inst_10 : SMulCommClass R T A] →
                                [inst_11 : SMulCommClass S T A] →
                                  [SMulCommClass R S A] →
                                    [TensorProduct.CompatibleSMul R S A B] →
                                      TensorProduct S A B →ₐ[T] TensorProduct R A B
-- Aesop.Tracing
Aesop.ruleSkippedEmoji : String
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addU_ne_zero_of_Y_ne : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F},
  P 2 ≠ 0 → Q 2 ≠ 0 → P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3 → WeierstrassCurve.Jacobian.addU P Q ≠ 0
-- Mathlib.Algebra.Ring.Equiv
/-- A ring isomorphism sends zero to zero.  -/
RingEquiv.map_zero : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R ≃+* S), f 0 = 0
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
/-- Left whiskering of an oplax natural transformation and a modification.  -/
CategoryTheory.Oplax.OplaxTrans.whiskerLeft : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.OplaxFunctor B C} →
          (η : F ⟶ G) →
            {θ ι : G ⟶ H} → (θ ⟶ ι) → (CategoryTheory.CategoryStruct.comp η θ ⟶ CategoryTheory.CategoryStruct.comp η ι)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.add_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m₁ m₂ : M) (n : N),
  (m₁ + m₂) ⊗ₜ[R] n = m₁ ⊗ₜ[R] n + m₂ ⊗ₜ[R] n
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.contains : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → α → Bool
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzOnWith.mul : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E} {s : Set α},
  LipschitzOnWith Kf f s → LipschitzOnWith Kg g s → LipschitzOnWith (Kf + Kg) (fun x => f x * g x) s
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.numeratorHom.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S],
  AddOreLocalization.numeratorHom = { toFun := fun r => r -ₒ 0, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.isEquivalence_of_isOneHypercoverDense : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor C₀ C) (J₀ : CategoryTheory.GrothendieckTopology C₀)
  (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A]
  [F.IsOneHypercoverDense J₀ J], (F.sheafPushforwardContinuous A J₀ J).IsEquivalence
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.norm.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.norm c = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.norm c_1 → c = c_1
-- Lean.Elab.Binders
Lean.Elab.Term.FunBinders.State.localInsts : Lean.Elab.Term.FunBinders.State → Lean.LocalInstances
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The type of `1`-hypercovers of an object `S : C` in a category equipped with a
Grothendieck topology `J`. This can be constructed from a covering of `S` and
a covering of the fibre products of the objects in this covering (see `OneHypercover.mk'`).  -/
CategoryTheory.GrothendieckTopology.OneHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C → C → Type (max (max u v) (w + 1))
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.horn.IsCompatible.δ_lift : ∀ {X : SSet} {n : ℕ} {i : Fin (n + 2)} {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)}
  (hf : SSet.horn.IsCompatible f) {Y : SSet} (p : X ⟶ Y) [inst : HomotopicalAlgebra.Fibration p]
  (b : SSet.stdSimplex.obj { len := n + 1 } ⟶ Y)
  (comm :
    ∀ (j : Fin (n + 2)) (hj : j ≠ i),
      CategoryTheory.CategoryStruct.comp (f j hj) p = CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) b)
  (j : Fin (n + 2)) (hj : autoParam (j ≠ i) SSet.horn.IsCompatible.δ_lift._auto_1),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) (hf.lift p b comm) = f j hj
-- Mathlib.GroupTheory.OrderOfElement
CharP.addOrderOf_one : ∀ (R : Type u_6) [inst : NonAssocRing R], CharP R (addOrderOf 1)
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.coe_eq_of_mem_split_of_mem_le : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {i : ι} {x : ℝ} {y : ι → ℝ},
  J ∈ BoxIntegral.Prepartition.split I i x → y ∈ J → y i ≤ x → ↑J = ↑I ∩ {y | y i ≤ x}
-- Mathlib.Order.PropInstances
Pi.eq_bot_iff_irrefl_of_subsingleton : ∀ {α : Type u_2} [Subsingleton α] {r : α → α → Prop}, r = ⊥ ↔ Std.Irrefl r
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.embedding_mk_eq_of_isReal : ∀ {K : Type u_1} [inst : Field K] {φ : K →+* ℂ},
  NumberField.ComplexEmbedding.IsReal φ → (NumberField.InfinitePlace.mk φ).embedding = φ
-- Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle
/-- The first projection in a product is a trivial fiber bundle.  -/
isHomeomorphicTrivialFiberBundle_fst : ∀ {B : Type u_1} (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F],
  IsHomeomorphicTrivialFiberBundle F Prod.fst
-- Mathlib.Analysis.Real.Cardinality
/-- The cardinality of the interval $(-∞, a]$.  -/
Cardinal.mk_Iic_real : ∀ (a : ℝ), Cardinal.mk ↑(Set.Iic a) = Cardinal.continuum
-- Mathlib.Data.List.Sort
List.decidableSortedGT : {α : Type u_1} → [inst : Preorder α] → [DecidableLT α] → DecidablePred List.SortedGT
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.trans_toLHom : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (e : L ≃ᴸ L') (e' : L' ≃ᴸ L''),
  (e.trans e').toLHom = e'.toLHom.comp e.toLHom
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.Icc_def : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι}, BoxIntegral.Box.Icc I = Set.Icc I.lower I.upper
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.linearEquivAt_symm_apply : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] (b : B)
  (hb : b ∈ e.baseSet) (v : F), (Bundle.Trivialization.linearEquivAt R e b hb).symm v = e.symm b v
-- Mathlib.Order.Filter.Map
Filter.disjoint_comap_iff_map' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {F : Filter α} {G : Filter β},
  Disjoint (Filter.comap f G) F ↔ Disjoint G (Filter.map f F)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft'_assoc : ∀ {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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : C} (f : x ⟶ y)
  [inst_4 : CategoryTheory.IsIso f] (z : D) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj y z ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft (CategoryTheory.inv f) z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f z)
        h) =
    h
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.const_comp : ∀ {P : TopCat → Prop} {S T U : CompHausLike P} (s : ↑S.toTop) (g : S ⟶ U),
  CategoryTheory.CategoryStruct.comp (T.const s) g = T.const ((CategoryTheory.ConcreteCategory.hom g) s)
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.mk.inj : ∀ {α : Type u_8} {β : Type u_9} {inst : CompleteLattice α} {inst_1 : CompleteLattice β} {toInfTopHom : InfTopHom α β}
  {map_sSup' : ∀ (s : Set α), toInfTopHom.toFun (sSup s) = sSup (toInfTopHom.toFun '' s)}
  {toInfTopHom_1 : InfTopHom α β}
  {map_sSup'_1 : ∀ (s : Set α), toInfTopHom_1.toFun (sSup s) = sSup (toInfTopHom_1.toFun '' s)},
  { toInfTopHom := toInfTopHom, map_sSup' := map_sSup' } = { toInfTopHom := toInfTopHom_1, map_sSup' := map_sSup'_1 } →
    toInfTopHom = toInfTopHom_1
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.of.d.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] {inst_4 : DecidableEq α} [inst_5 : DecidableEq α]
  (X : α → V) (d d_1 : (n : α) → X (n + 1) ⟶ X n),
  d = d_1 → ∀ (i j : α), ChainComplex.of.d X d i j = ChainComplex.of.d X d_1 i j
-- Mathlib.Topology.LocalAtTarget
Set.restrictPreimage_isInducing : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} (s : Set β),
  Topology.IsInducing f → Topology.IsInducing (s.restrictPreimage f)
-- Mathlib.Tactic.LinearCombinationPrime
/-- Implementation of `linear_combination'` and `linear_combination2`.  -/
Mathlib.Tactic.LinearCombinationPrime.elabLinearCombination' : Lean.Syntax →
  Option Lean.Syntax.Tactic →
    Option Lean.NumLit → Option Lean.Term → optParam Bool false → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.pIntegral.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) (x x_1 : ℚ),
  x = x_1 → ∀ [inst : Fact (Nat.Prime p)], Bernoulli.pIntegral✝ p x = Bernoulli.pIntegral✝ p_1 x_1
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.factors_prod_eq_basis_of_ne : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (s : Finset I)
  {x y : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)}, y ≠ x → (Profinite.NobelingProof.factors C s x).prod y = 0
-- Init.Data.ByteArray.Lemmas
List.toByteArray_append : ∀ {l l' : List UInt8}, (l ++ l').toByteArray = l.toByteArray ++ l'.toByteArray
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.color.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.color = 1
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Eta-expanded form of `MeromorphicNFAt.zpow`

---

Integer powers of meromorphic functions in normal form are in normal form.
 -/
MeromorphicNFAt.fun_zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {n : ℤ} {x : 𝕜},
  MeromorphicNFAt f x → MeromorphicNFAt (fun i => f i ^ n) x
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.smul : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ],
  MeasureTheory.IsFundamentalDomain G s μ → ∀ (g : G), MeasureTheory.IsFundamentalDomain G (g • s) μ
-- Mathlib.MeasureTheory.Measure.Real
/-- If `s` is a `Finset`, then the sums of the real measures of the singletons in the set is the
real measure of the set.  -/
MeasureTheory.sum_measureReal_singleton : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α]
  [MeasureTheory.SigmaFinite μ] (s : Finset α), ∑ b ∈ s, μ.real {b} = μ.real ↑s
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.pow_mem : ∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Ring E] [IsDomain E] [inst_3 : Algebra F E] (q : ℕ) [ExpChar F q]
  (x : E) [IsPurelyInseparable F E], ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanr.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (as : List α),
  List.scanr f init as = (List.scanrM (fun x1 x2 => pure (f x1 x2)) init as).run
-- Init.MetaTypes
Lean.Meta.Command.ReduceConfig.mk : Bool → Bool → Bool → Lean.Meta.TransparencyMode → Bool → Bool → Bool → Lean.Meta.Command.ReduceConfig
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULiftHom.down_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.ULiftHom C} (f : X ⟶ Y),
  CategoryTheory.ULiftHom.down.map f = f.down
-- Mathlib.RingTheory.Localization.Module
LinearMap.extendScalarsOfIsLocalization.congr_simp : ∀ {R : Type u_3} [inst : CommSemiring R] (S S_1 : Submonoid R) (e_S : S = S_1) (A : Type u_4) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_5} {N : Type u_6} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Module A M] [inst_7 : IsScalarTower R A M] [inst_8 : AddCommMonoid N]
  [inst_9 : Module R N] [inst_10 : Module A N] [inst_11 : IsScalarTower R A N] (f f_1 : M →ₗ[R] N),
  f = f_1 → LinearMap.extendScalarsOfIsLocalization S A f = LinearMap.extendScalarsOfIsLocalization S_1 A f_1
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.unop_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ) (X : C),
  P.unop X ↔ P (Opposite.op X)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The iterated derivative of the difference of two functions is the difference of the iterated
derivatives.
 -/
iteratedFDeriv_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {i : ℕ}
  {f g : E → F},
  ContDiff 𝕜 (↑i) f → ContDiff 𝕜 (↑i) g → iteratedFDeriv 𝕜 i (f - g) = iteratedFDeriv 𝕜 i f - iteratedFDeriv 𝕜 i g
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.Rewrites.reverse : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} {u v : List (Symbol T N)},
  r.Rewrites u v → r.reverse.Rewrites u.reverse v.reverse
-- Mathlib.Algebra.Exact.Basic
LinearMap.injective_range_liftQ_of_exact : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact ⇑f ⇑g), Function.Injective ⇑(f.range.liftQ g ⋯)
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
/-- The derivative of `klFun` is `log x`. This also holds at `x = 0` although `klFun` is not
differentiable there since the default value of `deriv` in that case is 0.  -/
InformationTheory.deriv_klFun : deriv InformationTheory.klFun = Real.log
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.toList_roo : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.toList_roo._auto_1)
  [Std.TransCmp cmp] {t : Std.DTreeMap.Raw α β cmp},
  t.WF →
    ∀ {lowerBound upperBound : α},
      Std.Slice.toList (Std.Roo.Sliceable.mkSlice t lowerBound<...upperBound) =
        List.filter (fun e => decide ((cmp e.fst lowerBound).isGT = true ∧ (cmp e.fst upperBound).isLT = true)) t.toList