mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  (D : F.DescentData' sq sq₃) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃)
  (hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
      CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom'._auto_1)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
      CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom'._auto_3)
  (hf₃ :
    autoParam (CategoryTheory.CategoryStruct.comp f₃ (f i₃) = q)
      CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom'._auto_5)
  {Z : ↑(F.obj { as := Opposite.op Y })} (h : (F.map f₃.op.toLoc).toFunctor.obj (D.obj i₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData'.pullHom' D.hom q f₁ f₂ hf₁ hf₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData'.pullHom' D.hom q f₂ f₃ hf₂ hf₃)
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData'.pullHom' D.hom q f₁ f₃ hf₁ hf₃) h
-- Mathlib.Topology.Inseparable
Topology.IsOpenEmbedding.generalizingMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsOpenEmbedding f → GeneralizingMap f
-- Init.Data.List.MapIdx
List.getElem?_mapFinIdx : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : ℕ) → α → i < l.length → β} {i : ℕ},
  (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => some (f i x ⋯)
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.one_div_eq : ∀ (p q r : ENNReal) [p.HolderTriple q r], 1 / r = 1 / p + 1 / q
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.instSmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (K : CategoryTheory.Precoverage C), K.Small
-- Mathlib.Topology.Specialization
/-- `ofEquiv` is the identity function from the `Specialization` of a type.  -/
Specialization.ofEquiv : {α : Type u_1} → Specialization α ≃ α
-- Mathlib.Topology.Algebra.Module.ModuleTopology
IsModuleTopology.instQuot : ∀ {R : Type u_1} [τR : TopologicalSpace R] [inst : Ring R] {A : Type u_3} [inst_1 : AddCommGroup A]
  [inst_2 : Module R A] [inst_3 : TopologicalSpace A] [IsModuleTopology R A] (S : Submodule R A),
  IsModuleTopology R (A ⧸ S)
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.locallyFinite : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s),
  LocallyFinite fun i => Function.support ⇑(f i)
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.counitAlgHom_comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] (f : A →ₐc[R] B),
  (Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- The trivial commutative group object.  -/
CategoryTheory.CommGrp.trivial : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.CommGrp C
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.mapComp_hom_app : ∀ {I : Type w₁} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} {K : Type w₃}
  (f : K → J) (g : J → I) (X : (i : K) × (fun i => C (g (f i))) i),
  (CategoryTheory.Sigma.mapComp C f g).hom.app X = CategoryTheory.CategoryStruct.id ⟨g (f X.fst), X.snd⟩
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.lift_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  (hg : ∀ (y : ↥M), IsUnit (g ↑y)) (x : R), (IsLocalization.lift hg) ((algebraMap R S) x) = g x
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.id_tensor_rightUnitor_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X)
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv
      (CategoryTheory.MonoidalCategoryStruct.associator X Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.forIn_eq_forIn_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ},
  (forIn t init fun a d => f a.1 d) = forIn t.keysArray init f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic.0.tacticPderiv_simp : Lean.ParserDescr
-- Mathlib.Algebra.Star.Unitary
Unitary.instSMulSubtypeMemSubmonoidUnitary : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Monoid R] →
      [inst_1 : Monoid A] →
        [inst_2 : MulAction R A] →
          [SMulCommClass R A A] →
            [IsScalarTower R A A] →
              [inst_5 : StarMul R] → [inst_6 : StarMul A] → [StarModule R A] → SMul ↥(unitary R) ↥(unitary A)
-- Mathlib.NumberTheory.NumberField.Basic
/-- Given `f : M →+ K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function
`M →+ 𝓞 K`.  -/
NumberField.RingOfIntegers.restrict_addMonoidHom : {K : Type u_1} →
  [inst : Field K] →
    {M : Type u_3} →
      [inst_1 : AddZeroClass M] → (f : M →+ K) → (∀ (x : M), IsIntegral ℤ (f x)) → M →+ NumberField.RingOfIntegers K
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.Cancels.eq_1 : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (u : ℤˣ)
  (w : HNNExtension.NormalWord d),
  HNNExtension.NormalWord.Cancels u w =
    (w.head ∈ HNNExtension.toSubgroup A B u ∧ Option.map Prod.fst w.toList.head? = some (-u))
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff.addMonoidHom_apply : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (g : Γ) (f : HahnSeries Γ R),
  (HahnSeries.coeff.addMonoidHom g) f = f.coeff g
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- `legendreSym p (-1)` is given by `χ₄ p`.  -/
legendreSym.at_neg_one : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], p ≠ 2 → legendreSym p (-1) = ZMod.χ₄ ↑p
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.IsSheaf.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {E : A} {X : C} {P : CategoryTheory.Functor Cᵒᵖ A},
  CategoryTheory.Presheaf.IsSheaf J P →
    ∀ (S : J.Cover X) (e₁ e₂ : E ⟶ P.obj (Opposite.op X)),
      (∀ (I : S.Arrow),
          CategoryTheory.CategoryStruct.comp e₁ (P.map I.f.op) = CategoryTheory.CategoryStruct.comp e₂ (P.map I.f.op)) →
        e₁ = e₂
-- Mathlib.Data.Nat.Digits.Lemmas
/-- The map `L ↦ Nat.ofDigits b L` is bijection between the set of lists of natural integers of
length `l` with coefficients `< b` to the set of natural integers `< b ^ l`.
 -/
Nat.bijOn_ofDigits : ∀ {b : ℕ}, 1 < b → ∀ (l : ℕ), Set.BijOn (Nat.ofDigits b) {L | L.length = l ∧ ∀ x ∈ L, x < b} {n | n < b ^ l}
-- Aesop.Tree.Data
Aesop.TreeSpec : Type 1
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_le_encard_ground : ∀ {α : Type u_1} (M : Matroid α), M.eRank ≤ M.E.encard
-- Init.Data.UInt.Lemmas
UInt64.ofNatTruncate_bitVecToNat : ∀ (n : BitVec 64), UInt64.ofNatClamp n.toNat = { toBitVec := n }
-- Mathlib.Order.Disjoint
IsCompl.symm : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y → IsCompl y x
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.exists_mem_target : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {p : β → Prop}, (∃ y ∈ e.target, p y) ↔ ∃ x ∈ e.source, p (↑e x)
-- Mathlib.MeasureTheory.Measure.DiracProba
/-- The assignment `x ↦ diracProba x` is injective if all singletons are measurable.  -/
MeasureTheory.injective_diracProba : ∀ {X : Type u_2} [inst : MeasurableSpace X] [MeasurableSpace.SeparatesPoints X],
  Function.Injective fun x => MeasureTheory.diracProba x
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.inradius.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 → s.inradius = s_1.inradius
-- Lean.Environment
Lean.mkModuleData : Lean.Environment →
  optParam Lean.OLeanLevel Lean.OLeanLevel.private →
    optParam (Option (Lean.OLeanEntries (Array (Lean.Name × Array Lean.EnvExtensionEntry)))) none → IO Lean.ModuleData
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.instUniqueHomEmptyCollection : {X : AlgebraicGeometry.LocallyRingedSpace} → Unique (∅ ⟶ X)
-- Mathlib.Analysis.Normed.Group.Hom
/-- **Alias** of `NormedAddGroupHom.mkNormedAddGroupHom_norm_le`.

---

If a bounded group homomorphism map is constructed from a group homomorphism via the constructor
`AddMonoidHom.mkNormedAddGroupHom`, then its norm is bounded by the bound given to the constructor
if it is nonnegative.  -/
AddMonoidHom.mkNormedAddGroupHom_norm_le : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (f : V₁ →+ V₂)
  {C : ℝ}, 0 ≤ C → ∀ (h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖), ‖f.mkNormedAddGroupHom C h‖ ≤ C
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Given two subgraphs, one a subgraph of the other, there is an induced injective homomorphism of
the subgraphs as graphs.  -/
SimpleGraph.Subgraph.inclusion : {V : Type u} → {G : SimpleGraph V} → {x y : G.Subgraph} → x ≤ y → x.coe →g y.coe
-- Mathlib.Topology.ContinuousMap.Ideals
/-- Given a topological ring `R` and `s : Set X`, construct the ideal in `C(X, R)` of functions
which vanish on the complement of `s`.  -/
ContinuousMap.idealOfSet : {X : Type u_1} →
  (R : Type u_2) →
    [inst : TopologicalSpace X] →
      [inst_1 : Semiring R] → [inst_2 : TopologicalSpace R] → [inst_3 : IsTopologicalSemiring R] → Set X → Ideal C(X, R)
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `setOfPred_gauge_lt_one_eq_self_of_isOpen`. -/
setOf_gauge_lt_one_eq_self_of_isOpen : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
  [ContinuousSMul ℝ E], Convex ℝ s → 0 ∈ s → IsOpen s → {x | gauge s x < 1} = s
-- Mathlib.Topology.Compactness.CompactSystem
/-- A set system is a compact system iff adding `∅` gives a compact system.  -/
isCompactSystem_insert_empty_iff : ∀ {α : Type u_1} {S : Set (Set α)}, IsCompactSystem (insert ∅ S) ↔ IsCompactSystem S
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.containsThenInsert_snd : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] {k : α}
  {v : β k}, (m.containsThenInsert k v).2 = m.insert k v
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.root_apply_cartanEquivDual_symm_ne_zero : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [inst_7 : CharZero K]
  {α : LieModule.Weight K (↥H) L},
  α.IsNonZero → α ((LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α)) ≠ 0
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.compl_top : ∀ {α : Type u_1} [inst : LE α], ⊤.compl = ⊤
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.FormallySmooth.respectsIso : RingHom.RespectsIso @RingHom.FormallySmooth
-- Mathlib.Topology.Defs.Basic
isOpen_sUnion : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set (Set X)}, (∀ t ∈ s, IsOpen t) → IsOpen (⋃₀ s)
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S : Solution`, `S.multiplicity` is the multiplicity of `λ` in `S.c`, as a natural
number.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.multiplicity : {K : Type u_1} → [inst : Field K] → {ζ : K} → {hζ : IsPrimitiveRoot ζ 3} → FermatLastTheoremForThreeGen.Solution✝ hζ → ℕ
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.neg_eq_eval : ∀ {S : Type u_1} {R : Type u_2} {M : Type u_3} [inst : AddCommGroup M] [inst_1 : Semiring S] [inst_2 : Module S M]
  [inst_3 : Ring R] [inst_4 : Module R M] {l : Mathlib.Tactic.Module.NF R M} {l₀ : Mathlib.Tactic.Module.NF S M},
  l.eval = l₀.eval → ∀ {x : M}, x = l₀.eval → -x = (-l).eval
-- Init.GrindInstances.Ring.UInt
UInt32.natCast : NatCast UInt32
-- Mathlib.Algebra.Module.Defs
Convex.combo_self : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {a b : R},
  a + b = 1 → ∀ (x : M), a • x + b • x = x
-- Mathlib.Logic.Relation
Relation.reflTransGen_reflGen : ∀ {α : Type u_1} {r : α → α → Prop}, Relation.ReflTransGen (Relation.ReflGen r) = Relation.ReflTransGen r
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.restrict.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R₁ R₂ : CategoryTheory.Presieve X} (h : R₁ ≤ R₂) (x : CategoryTheory.Presieve.FamilyOfElements P R₂) (x_1 : C)
  (f : x_1 ⟶ X) (hf : R₁ f), CategoryTheory.Presieve.FamilyOfElements.restrict h x f hf = x f ⋯
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.getFunInduct? : Bool → Bool → Lean.Name → Lean.CoreM (Option Lean.Name)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.nonneg' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν → ∀ (a : α) (q : ℚ), ∀ᵐ (c : β) ∂ν a, 0 ≤ f (a, c) q
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.mem_homologicalKernel_iff : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) [inst_3 : F.ShiftSequence ℤ] (X : C),
  F.homologicalKernel X ↔ ∀ (n : ℤ), CategoryTheory.Limits.IsZero ((F.shift n).obj X)
-- Init.Data.UInt.Lemmas
USize.toFin_val : ∀ (x : USize), ↑x.toFin = x.toNat
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_bot_left : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), ⊥.relIndex H = Nat.card ↥H
-- Mathlib.MeasureTheory.Order.Lattice
AEMeasurable.sup_const : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → M} [inst_1 : Max M] [MeasurableSup M], AEMeasurable f μ → ∀ (c : M), AEMeasurable (fun x => f x ⊔ c) μ
-- Init.Data.Int.DivMod.Lemmas
Int.lt_ediv_iff_of_dvd_of_neg : ∀ {a b c : ℤ}, c < 0 → c ∣ b → (a < b / c ↔ b < c * a)
-- Lean.Data.KVMap
Lean.instCoeBoolDataValue : Coe Bool Lean.DataValue
-- Std.Do.WP.Basic
/-- A weakest precondition interpretation of a monadic program `x : m α` in terms of a predicate
transformer `PredTrans ps α`. The monad `m` determines `ps : PostShape`.

For practical reasoning, an instance of `WPMonad m ps` is typically needed in addition to `WP m ps`.
 -/
Std.Do.WP : (Type u → Type v) → outParam Std.Do.PostShape → Type (max (u + 1) v)
-- Mathlib.Data.Finset.Basic
Equiv.Finset.disjUnionEquiv_inl : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} (h : Disjoint s t) (x : ↥s),
  (Equiv.Finset.disjUnionEquiv s t h) (Sum.inl x) = ⟨↑x, ⋯⟩
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.partial_sups : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : Preorder ι] [inst_4 : LocallyFiniteOrderBot ι] {p : SeminormFamily 𝕜 E ι} [inst_5 : TopologicalSpace E],
  WithSeminorms p → WithSeminorms fun i => (Finset.Iic i).sup p
-- Lean.EnvExtension
Lean.SimplePersistentEnvExtensionDescr.mk.injEq : ∀ {α σ : Type} (name : autoParam Lean.Name Lean.SimplePersistentEnvExtensionDescr.name._autoParam)
  (addEntryFn : σ → α → σ) (addImportedFn : Array (Array α) → σ) (toArrayFn : List α → Array α)
  (exportEntriesFnEx? : Option (Lean.Environment → σ → List α → Lean.OLeanEntries (Array α)))
  (asyncMode : Lean.EnvExtension.AsyncMode) (replay? : Option (List α → σ → σ → List α × σ))
  (name_1 : autoParam Lean.Name Lean.SimplePersistentEnvExtensionDescr.name._autoParam) (addEntryFn_1 : σ → α → σ)
  (addImportedFn_1 : Array (Array α) → σ) (toArrayFn_1 : List α → Array α)
  (exportEntriesFnEx?_1 : Option (Lean.Environment → σ → List α → Lean.OLeanEntries (Array α)))
  (asyncMode_1 : Lean.EnvExtension.AsyncMode) (replay?_1 : Option (List α → σ → σ → List α × σ)),
  ({ name := name, addEntryFn := addEntryFn, addImportedFn := addImportedFn, toArrayFn := toArrayFn,
        exportEntriesFnEx? := exportEntriesFnEx?, asyncMode := asyncMode, replay? := replay? } =
      { name := name_1, addEntryFn := addEntryFn_1, addImportedFn := addImportedFn_1, toArrayFn := toArrayFn_1,
        exportEntriesFnEx? := exportEntriesFnEx?_1, asyncMode := asyncMode_1, replay? := replay?_1 }) =
    (name = name_1 ∧
      addEntryFn = addEntryFn_1 ∧
        addImportedFn = addImportedFn_1 ∧
          toArrayFn = toArrayFn_1 ∧
            exportEntriesFnEx? = exportEntriesFnEx?_1 ∧ asyncMode = asyncMode_1 ∧ replay? = replay?_1)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.commIsometry_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  (x : TensorProduct 𝕜 E F), (TensorProduct.commIsometry 𝕜 E F) x = (TensorProduct.comm 𝕜 E F) x
-- Mathlib.Topology.Bases
TopologicalSpace.instSeparableSpaceSum : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace β] [TopologicalSpace.SeparableSpace α]
  [TopologicalSpace.SeparableSpace β], TopologicalSpace.SeparableSpace (α ⊕ β)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.discreteTopology_iff_toPiLocalization_surjective : ∀ {R : Type u_1} [inst : CommSemiring R],
  DiscreteTopology (PrimeSpectrum R) ↔ Function.Surjective ⇑(PrimeSpectrum.toPiLocalization R)
-- Std.Time.Time.PlainTime
/-- Adds seconds to a `PlainTime`.
 -/
Std.Time.PlainTime.addSeconds : Std.Time.PlainTime → Std.Time.Second.Offset → Std.Time.PlainTime
-- Std.Tactic.Do.ProofMode
/-- This is the same as `SPred.entails`.
This constant is used to detect `SPred` proof mode goals.  -/
Std.Tactic.Do.MGoalEntails : {σs : List (Type u_1)} → Std.Do.SPred σs → Std.Do.SPred σs → Prop
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_mk : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (toLinearMap : M →ₛₗ[σ] M₂)
  (invFun : M₂ → M) (h₁ : Function.LeftInverse invFun toLinearMap.toFun)
  (h₂ : Function.RightInverse invFun toLinearMap.toFun),
  { toLinearMap := toLinearMap, invFun := invFun, left_inv := h₁, right_inv := h₂ }.symm =
    { toFun := invFun, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑toLinearMap, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor_map_left_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  (CategoryTheory.Square.toArrowArrowFunctor.map φ).left.left = φ.τ₁
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- `lpMeas F 𝕜 m p μ` is the subspace of `Lp F p μ` containing functions `f` verifying
`AEStronglyMeasurable[m] f μ`, i.e. functions which are `μ`-a.e. equal to
an `m`-strongly measurable function.  -/
MeasureTheory.lpMeas : {α : Type u_1} →
  (F : Type u_2) →
    (𝕜 : Type u_3) →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace 𝕜 F] →
            MeasurableSpace α →
              [inst_3 : MeasurableSpace α] →
                (p : ENNReal) → (μ : MeasureTheory.Measure α) → Submodule 𝕜 ↥(MeasureTheory.Lp F p μ)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instToJsonDidSaveTextDocumentParams.toJson : Lean.Lsp.DidSaveTextDocumentParams → Lean.Json
-- Mathlib.MeasureTheory.Measure.Stieltjes
measurableSet_botSet : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : MeasurableSpace R] [MeasurableSingletonClass R], MeasurableSet botSet
-- Mathlib.Analysis.Normed.Group.Basic
nontrivialTopology_iff_exists_nnnorm_ne_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], NontrivialTopology E ↔ ∃ x, ‖x‖₊ ≠ 0
-- Mathlib.Topology.Category.TopCommRingCat
RingHom.id.eq_1 : ∀ (α : Type u_5) [inst : NonAssocSemiring α],
  RingHom.id α = { toFun := fun x => x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.instNonemptyOfNontrivial : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] [Nontrivial M],
  Nonempty (FiniteArchimedeanClass M)
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_ofNat' : ∀ {n : ℕ}, n < UInt16.size → (UInt16.ofNat n).toUInt64 = UInt64.ofNat n
-- Mathlib.Data.Sym.Sym2
Sym2.eq_of_ne_mem : ∀ {α : Type u_1} {x y : α} {z z' : Sym2 α}, x ≠ y → x ∈ z → y ∈ z → x ∈ z' → y ∈ z' → z = z'
-- Init.Data.List.MapIdx
List.getElem_mapFinIdx : ∀ {α : Type u_1} {β : Type u_2} {as : List α} {f : (i : ℕ) → α → i < as.length → β} {i : ℕ}
  {h : i < (as.mapFinIdx f).length}, (as.mapFinIdx f)[i] = f i as[i] ⋯
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mul_one_div_le_one : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K}, I * (1 / I) ≤ 1
-- Mathlib.Algebra.Group.Basic
eq_one_iff_eq_one_of_mul_eq_one : ∀ {M : Type u_4} [inst : MulOneClass M] {a b : M}, a * b = 1 → (a = 1 ↔ b = 1)
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.conj_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y),
  α.conj (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id Y
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instR0Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [R0Space M], R0Space Mᵈᵃᵃ
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_of_lt_mul_left₀ : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [PosMulReflectLT α],
  0 ≤ a → a < a * b → 1 < b
-- Init.Data.Int.Order
Int.sub_le_self : ∀ (a : ℤ) {b : ℤ}, 0 ≤ b → a - b ≤ a
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.sInter_empty : ∅.sInter = ∅
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.find?_bool_eq_some_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  s.find? p = some pos ↔
    ∃ (h : pos ≠ s.endPos), p (pos.get h) = true ∧ ∀ (pos' : s.Pos) (h' : pos' < pos), p (pos'.get ⋯) = false
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDeriv_const_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜}, iteratedDeriv n 0 x = 0