mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.minKey? = some km → t.getKey? km = some km
-- Lean.Parser.Term.Basic
Lean.Parser.Term.strictImplicitRightBracket.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.coe_withTop : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β),
  ⇑f.withTop = WithTop.map ⇑f
-- Batteries.Util.ProofWanted
DefWanted.mk.sizeOf_spec : ∀ {α : Sort u} [inst : SizeOf α], sizeOf { } = 1
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.inhabited : {Γ : Type u_1} → [inst : Inhabited Γ] → Inhabited (Turing.Tape Γ)
-- Mathlib.CategoryTheory.Localization.Bousfield
/-- The bijection `(X ⟶ Y) ≃ (X ⟶ Z)` induced by `g : Y ⟶ Z` when `P.isColocal g`
and `P X`.  -/
CategoryTheory.ObjectProperty.isColocal.homEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} → {Y Z : C} → {g : Y ⟶ Z} → P.isColocal g → (X : C) → P X → (X ⟶ Y) ≃ (X ⟶ Z)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.map_range : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  [inst_7 : Semiring D] [inst_8 : Algebra R D] (f : A →ₐ[R] C) (g : B →ₐ[R] D),
  (Algebra.TensorProduct.map f g).range =
    (Algebra.TensorProduct.includeLeft.comp f).range ⊔ (Algebra.TensorProduct.includeRight.comp g).range
-- Std.Internal.Parsec.ByteArray
/-- Skips until a predicate is satisfied, up to a given limit.
 -/
Std.Internal.Parsec.ByteArray.skipUntilUpTo : (UInt8 → Bool) → ℕ → Std.Internal.Parsec.ByteArray.Parser Unit
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.isSFiniteKernel_prodMkLeft_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [Nonempty γ] {κ : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.prodMkLeft γ κ) ↔ ProbabilityTheory.IsSFiniteKernel κ
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.mk : {G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} →
      [inst : Group G] →
        [inst_1 : MulAction G X] →
          {ps : DiscreteTiling.Protoset G X ιₚ} →
            (index : ιₚ) →
              G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries →
                DiscreteTiling.PlacedTile ps
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.transIsBigOIsBigO : {α : Type u_1} →
  {E : Type u_3} →
    {G : Type u_5} →
      {F' : Type u_7} →
        [inst : Norm E] →
          [inst_1 : Norm G] →
            [inst_2 : SeminormedAddCommGroup F'] →
              {l : Filter α} → Trans (fun x1 x2 => x1 =O[l] x2) (fun x1 x2 => x1 =O[l] x2) fun x1 x2 => x1 =O[l] x2
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The ring homomorphism induced by the partial order.  -/
ValuationSubring.inclusion : {K : Type u} → [inst : Field K] → (R S : ValuationSubring K) → R ≤ S → ↥R →+* ↥S
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.epiModSerre.isoModSerre_image_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsSerreClass] {X Y : C} {f : X ⟶ Y},
  P.epiModSerre f → P.isoModSerre (CategoryTheory.Abelian.image.ι f)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
Measurable.of_union_range_cover : ∀ {α : Type u_1} {β : Type u_2} {α₁ : Type u_6} {α₂ : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mα₁ : MeasurableSpace α₁} {mα₂ : MeasurableSpace α₂} {i₁ : α₁ → α} {i₂ : α₂ → α} {f : α → β},
  MeasurableEmbedding i₁ →
    MeasurableEmbedding i₂ →
      Set.univ ⊆ Set.range i₁ ∪ Set.range i₂ → Measurable (f ∘ i₁) → Measurable (f ∘ i₂) → Measurable f
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.primeHeight_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} [inst_1 : I.IsPrime], Ideal.primeHeight✝ I = 0 ↔ I ∈ minimalPrimes R
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.L1.norm_of_fun_eq_integral_norm : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {H : Type u_6} [inst : NormedAddCommGroup H]
  {f : α → H} (hf : MeasureTheory.Integrable f μ), ‖MeasureTheory.Integrable.toL1 f hf‖ = ∫ (a : α), ‖f a‖ ∂μ
-- Batteries.Util.ProofWanted
/-- `true` if the wanted's payload is a typeclass. The generated parameter is then an instance
binder so Lean's instance synth can find it.  -/
_private.Batteries.Util.ProofWanted.0.WantedRefInfo.isClass : WantedRefInfo✝ → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.sigmaConst_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C] (X : C)
  (n : Type w), (CategoryTheory.Limits.sigmaConst.obj X).obj n = ∐ fun x => X
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.rlp_pushouts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C), T.pushouts.rlp = T.rlp
-- Mathlib.Topology.ClusterPt
not_isOpen_singleton : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot], ¬IsOpen {x}
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- A morphism between target objects `T ⟶ T'`
covariantly induces a functor between costructured arrows,
`CostructuredArrow S T ⥤ CostructuredArrow S T'`.

Ideally this would be described as a 2-functor from `D`
(promoted to a 2-category with equations as 2-morphisms)
to `Cat`.
 -/
CategoryTheory.CostructuredArrow.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T T' : D} →
          {S : CategoryTheory.Functor C D} →
            (T ⟶ T') →
              CategoryTheory.Functor (CategoryTheory.CostructuredArrow S T) (CategoryTheory.CostructuredArrow S T')
-- Mathlib.Algebra.Ring.Units
Units.map_neg : ∀ {α : Type u} {β : Type v} [inst : Ring α] {F : Type u_1} [inst_1 : Ring β] [inst_2 : FunLike F α β]
  [inst_3 : RingHomClass F α β] (f : F) (u : αˣ), (Units.map ↑f) (-u) = -(Units.map ↑f) u
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_smul_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {S : Type u_3}
  [inst_9 : SMul S R] [ContinuousConstSMul S R] [inst_11 : SMulZeroClass S A] [IsScalarTower S R A]
  [IsScalarTower S R (R → R)] (s : S) (a : A), autoParam (p a) cfc_smul_id._auto_1 → cfc (fun x => s • x) a = s • a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.inr_freeSumIso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] (I J_1 : Type u) {Z : SheafOfModules R}
  (h : SheafOfModules.free (I ⊕ J_1) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (SheafOfModules.freeSumIso I J_1).hom h) =
    CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap Sum.inr) h
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.inv_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A : ↥(Matrix.unitaryGroup n α)), ↑A⁻¹ = star ↑A
-- Mathlib.RingTheory.Smooth.AdicCompletion
/-- If `A` is formally smooth over `R`, any map `A →ₐ[R] S ⧸ I` lifts
to `A →ₐ[R] S` if `S` is `I`-adically complete.
See `Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq` for a version
about `AdicCompletion`.  -/
Algebra.FormallySmooth.exists_mkₐ_comp_eq_of_isAdicComplete : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] [Algebra.FormallySmooth R A] {I : Ideal S} [IsAdicComplete I S]
  (f : A →ₐ[R] S ⧸ I), ∃ g, (Ideal.Quotient.mkₐ R I).comp g = f
-- Mathlib.GroupTheory.Goursat
Subgroup.normal_goursatFst : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {I : Subgroup (G × H)},
  Function.Surjective (Prod.fst ∘ ⇑I.subtype) → I.goursatFst.Normal
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgHom.mem_equalizer : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (φ ψ : F) (x : A), x ∈ NonUnitalAlgHom.equalizer φ ψ ↔ φ x = ψ x
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.eraPairs : Vector String 2 → Array (String × Std.Time.Year.Era)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'.eq_6 : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (n : ℕ),
  preNormEDS' b c d n.succ.succ.succ.succ.succ =
    if hn : Even n then
      (preNormEDS' b c d (n / 2 + 4) * preNormEDS' b c d (n / 2 + 2) ^ 3 * if Even (n / 2) then b else 1) -
        preNormEDS' b c d (n / 2 + 1) * preNormEDS' b c d (n / 2 + 3) ^ 3 * if Even (n / 2) then 1 else b
    else
      have this := ⋯;
      preNormEDS' b c d (n / 2 + 2) ^ 2 * preNormEDS' b c d (n / 2 + 3) * preNormEDS' b c d (n / 2 + 5) -
        preNormEDS' b c d (n / 2 + 1) * preNormEDS' b c d (n / 2 + 3) * preNormEDS' b c d (n / 2 + 4) ^ 2
-- Mathlib.Algebra.Group.Conj
ConjClasses.mk.eq_1 : ∀ {α : Type u_1} [inst : Monoid α] (a : α), ConjClasses.mk a = ⟦a⟧
-- Mathlib.Topology.Irreducible
isPreirreducible_iff_preirreducibleSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsPreirreducible s ↔ PreirreducibleSpace ↑s
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.evalOp_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (A : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasProducts A] {X Y : CategoryTheory.Functor Cᵒᵖ A} (α : X ⟶ Y)
  (f : (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ),
  ((CategoryTheory.Limits.FormalCoproduct.evalOp C A).map α).app f =
    CategoryTheory.Limits.Pi.map fun i => α.app (Opposite.op ((Opposite.unop f).obj i))
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.utf8DecodeChar?_append_eq_assemble₁ : ∀ {l : List UInt8} {b : ByteArray} (hl : l.length = 1)
  (h : ByteArray.utf8DecodeChar?.parseFirstByte l[0] = ByteArray.utf8DecodeChar?.FirstByte.done),
  (l.toByteArray ++ b).utf8DecodeChar? 0 = ByteArray.utf8DecodeChar?.assemble₁ l[0] h
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Compose a presieve on the right with a morphism.  -/
CategoryTheory.Presieve.pushforward : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (X ⟶ Y) → CategoryTheory.Presieve X → CategoryTheory.Presieve Y
-- Mathlib.Algebra.Algebra.Operations
Submodule.instIsOrderedRing : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A],
  IsOrderedRing (Submodule R A)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_left_le_mk_div : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b → MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk (a / b)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.prodMk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {s : Set M} {x : M} {f : M → M'} {g : M → M''}, MDiffAt[s] f x → MDiffAt[s] g x → (MDiffAt[s] fun x => (f x, g x)) x
-- Mathlib.Algebra.Group.Prod
mulMonoidHom.eq_1 : ∀ {α : Type u_6} [inst : CommMonoid α], mulMonoidHom = { toFun := mulMulHom.toFun, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- The `AddSubsemigroup` generated by a set includes the set.  -/
AddSubsemigroup.subset_closure : ∀ {M : Type u_1} [inst : Add M] {s : Set M}, s ⊆ ↑(AddSubsemigroup.closure s)
-- Mathlib.Order.Disjoint
Codisjoint.eq_top : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b → a ⊔ b = ⊤
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrict_restrict_eq : ∀ {α : Type u_1} {R₁ R₂ : Set α} (M : Matroid α), R₂ ⊆ R₁ → (M.restrict R₁).restrict R₂ = M.restrict R₂
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.tensorRight' : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      (f : a ⟶ b) →
        (g : b ⟶ b) →
          [CategoryTheory.BicategoricalCoherence g (CategoryTheory.CategoryStruct.id b)] →
            CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp f g) f
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_toUSize : ∀ (n : UInt8), n.toUSize.toUInt32 = n.toUInt32
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
MvQPF.Pi.inhabited : {n : ℕ} →
  {A : Type u} →
    (F : A → TypeVec.{u} n → Type u) → {α : TypeVec.{u} n} → [(a : A) → Inhabited (F a α)] → Inhabited (MvQPF.Pi F α)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The equivalence relation underlying an additive congruence relation.  -/
AddCon.toSetoid : {M : Type u_1} → [inst : Add M] → AddCon M → Setoid M
-- Mathlib.Order.WithBot
WithBot.toDual_apply_coe : ∀ {α : Type u_1} (a : α), WithBot.toDual ↑a = ↑(OrderDual.toDual a)
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- The converse of the construction in `liftToFinsetColimitCocone`: we can form a cocone on the
coproduct of `f` whose legs are the coproducts over the finite subsets of `α`.  -/
CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type w} →
      [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        (f : α → C) →
          [CategoryTheory.Limits.HasCoproduct f] →
            CategoryTheory.Limits.Cocone
              (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj (CategoryTheory.Discrete.functor f))
-- Lean.LocalContext
/-- Given an `FVarId`, this function returns the corresponding user name,
but only if the name can be used to recover the original FVarId.
 -/
Lean.LocalContext.getRoundtrippingUserName? : Lean.LocalContext → Lean.FVarId → Option Lean.Name
-- Mathlib.Computability.Primrec.Basic
PrimrecPred.or : ∀ {α : Type u_1} [inst : Primcodable α] {p q : α → Prop}, PrimrecPred p → PrimrecPred q → PrimrecPred fun a => p a ∨ q a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.apply_eq_true_of_lt_skipWhile_bool : ∀ {p : Char → Bool} {s : String} {pos pos' : s.Pos}, pos ≤ pos' → ∀ (h₂ : pos' < pos.skipWhile p), p (pos'.get ⋯) = true
-- Batteries.Data.ByteArray
/-- `mapM f a` applies the monadic function `f` to each element of the array.  -/
ByteArray.mapM : {m : Type → Type u_1} → [Monad m] → ByteArray → (UInt8 → m UInt8) → m ByteArray
-- Mathlib.Data.Fin.Tuple.Basic
Fin.exists_cons : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} (q : (i : Fin (n + 1)) → α i), ∃ x₀ x, q = Fin.cons x₀ x
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.expand.go_pos : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] {i : ℕ} {source : Array (Std.DHashMap.Internal.AssocList α β)}
  {target : { d // 0 < d.size }} (h : i < source.size),
  Std.DHashMap.Internal.Raw₀.expand.go✝ i source target =
    Std.DHashMap.Internal.Raw₀.expand.go✝ (i + 1) (source.set i Std.DHashMap.Internal.AssocList.nil h)
      (Std.DHashMap.Internal.AssocList.foldl (Std.DHashMap.Internal.Raw₀.reinsertAux hash) target source[i])
-- Mathlib.NumberTheory.GaussSum
/-- For a quadratic character `χ` and when the characteristic `p` of the target ring
is a unit in the source ring, the `p`th power of the Gauss sum of `χ` and `ψ` is
`χ p` times the original Gauss sum.  -/
MulChar.IsQuadratic.gaussSum_frob : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (p : ℕ)
  [fp : Fact (Nat.Prime p)] [hch : CharP R' p],
  IsUnit ↑p → ∀ {χ : MulChar R R'}, χ.IsQuadratic → ∀ (ψ : AddChar R R'), gaussSum χ ψ ^ p = χ ↑p * gaussSum χ ψ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filterMap.congr_simp : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] (f f_1 : (a : α) → β a → Option (γ a)),
  f = f_1 →
    ∀ (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (hl : t.Balanced),
      Std.DTreeMap.Internal.Impl.filterMap f t hl = Std.DTreeMap.Internal.Impl.filterMap f_1 t_1 ⋯
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.zero_add_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] {Z : C} (f : Z ⟶ M) {Z_1 : C} (h : M ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero f)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon : Type
-- Std.Http.Internal.IndexMultiMap
/-- Maps each key to its indices in `entries`. Each array is non-empty.
 -/
Std.Internal.IndexMultiMap.indexes : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β → Std.HashMap α (Array ℕ)
-- Lean.Server.Snapshots
Lean.Server.Snapshots.Snapshot.mk.inj : ∀ {stx : Lean.Syntax} {mpState : Lean.Parser.ModuleParserState} {cmdState : Lean.Elab.Command.State}
  {stx_1 : Lean.Syntax} {mpState_1 : Lean.Parser.ModuleParserState} {cmdState_1 : Lean.Elab.Command.State},
  { stx := stx, mpState := mpState, cmdState := cmdState } =
      { stx := stx_1, mpState := mpState_1, cmdState := cmdState_1 } →
    stx = stx_1 ∧ mpState = mpState_1 ∧ cmdState = cmdState_1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.GoalState.mk.injEq : ∀ (nextDeclIdx : ℕ) (enodeMap : Lean.Meta.Grind.ENodeMap) (exprs : Lean.PArray Lean.Expr)
  (parents : Lean.Meta.Grind.ParentMap) (congrTable : Lean.Meta.Grind.CongrTable enodeMap)
  (appMap : Lean.PHashMap Lean.HeadIndex (List Lean.Expr)) (indicesFound : Lean.PHashSet Lean.HeadIndex)
  (newFacts : Array Lean.Meta.Grind.NewFact) (inconsistent : Bool) (nextIdx : ℕ)
  (newRawFacts : Std.Queue Lean.Meta.Grind.NewRawFact) (facts : Lean.PArray Lean.Expr)
  (extThms : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Array Lean.Meta.Ext.ExtTheorem))
  (ematch : Lean.Meta.Grind.EMatch.State) (inj : Lean.Meta.Grind.Injective.State) (split : Lean.Meta.Grind.Split.State)
  (clean : Lean.Meta.Grind.Clean.State) (sstates : Array Lean.Meta.Grind.SolverExtensionState) (nextDeclIdx_1 : ℕ)
  (enodeMap_1 : Lean.Meta.Grind.ENodeMap) (exprs_1 : Lean.PArray Lean.Expr) (parents_1 : Lean.Meta.Grind.ParentMap)
  (congrTable_1 : Lean.Meta.Grind.CongrTable enodeMap_1) (appMap_1 : Lean.PHashMap Lean.HeadIndex (List Lean.Expr))
  (indicesFound_1 : Lean.PHashSet Lean.HeadIndex) (newFacts_1 : Array Lean.Meta.Grind.NewFact) (inconsistent_1 : Bool)
  (nextIdx_1 : ℕ) (newRawFacts_1 : Std.Queue Lean.Meta.Grind.NewRawFact) (facts_1 : Lean.PArray Lean.Expr)
  (extThms_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Array Lean.Meta.Ext.ExtTheorem))
  (ematch_1 : Lean.Meta.Grind.EMatch.State) (inj_1 : Lean.Meta.Grind.Injective.State)
  (split_1 : Lean.Meta.Grind.Split.State) (clean_1 : Lean.Meta.Grind.Clean.State)
  (sstates_1 : Array Lean.Meta.Grind.SolverExtensionState),
  ({ nextDeclIdx := nextDeclIdx, enodeMap := enodeMap, exprs := exprs, parents := parents, congrTable := congrTable,
        appMap := appMap, indicesFound := indicesFound, newFacts := newFacts, inconsistent := inconsistent,
        nextIdx := nextIdx, newRawFacts := newRawFacts, facts := facts, extThms := extThms, ematch := ematch,
        inj := inj, split := split, clean := clean, sstates := sstates } =
      { nextDeclIdx := nextDeclIdx_1, enodeMap := enodeMap_1, exprs := exprs_1, parents := parents_1,
        congrTable := congrTable_1, appMap := appMap_1, indicesFound := indicesFound_1, newFacts := newFacts_1,
        inconsistent := inconsistent_1, nextIdx := nextIdx_1, newRawFacts := newRawFacts_1, facts := facts_1,
        extThms := extThms_1, ematch := ematch_1, inj := inj_1, split := split_1, clean := clean_1,
        sstates := sstates_1 }) =
    (nextDeclIdx = nextDeclIdx_1 ∧
      enodeMap = enodeMap_1 ∧
        exprs = exprs_1 ∧
          parents = parents_1 ∧
            congrTable ≍ congrTable_1 ∧
              appMap = appMap_1 ∧
                indicesFound = indicesFound_1 ∧
                  newFacts = newFacts_1 ∧
                    inconsistent = inconsistent_1 ∧
                      nextIdx = nextIdx_1 ∧
                        newRawFacts = newRawFacts_1 ∧
                          facts = facts_1 ∧
                            extThms = extThms_1 ∧
                              ematch = ematch_1 ∧ inj = inj_1 ∧ split = split_1 ∧ clean = clean_1 ∧ sstates = sstates_1)
-- Mathlib.Order.CompleteLattice.Basic
sInf_empty : ∀ {α : Type u_1} [inst : CompleteLattice α], sInf ∅ = ⊤
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensRangeParams.mk.inj : ∀ {textDocument : Lean.Lsp.TextDocumentIdentifier} {range : Lean.Lsp.Range}
  {textDocument_1 : Lean.Lsp.TextDocumentIdentifier} {range_1 : Lean.Lsp.Range},
  { textDocument := textDocument, range := range } = { textDocument := textDocument_1, range := range_1 } →
    textDocument = textDocument_1 ∧ range = range_1
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.deriv_smoothingFn : ∀ {x : ℝ}, deriv AkraBazziRecurrence.smoothingFn x = -x⁻¹ / Real.log x ^ 2
-- Mathlib.RingTheory.Localization.FractionRing
/-- The inverse of an element in the field of fractions of an integral domain.  -/
IsFractionRing.inv : (A : Type u_6) →
  [inst : CommRing A] →
    {K : Type u_7} → [inst_1 : CommRing K] → [inst_2 : Algebra A K] → [IsFractionRing A K] → [IsDomain A] → K → K
-- Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
CategoryTheory.Precoverage.ZeroHypercover.glueMorphisms.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C}
  [inst_1 : J.toGrothendieck.Subcanonical] {S T : C} (𝒰 : J.ZeroHypercover S) [inst_2 : 𝒰.HasPullbacks]
  (f f_1 : (i : 𝒰.I₀) → 𝒰.X i ⟶ T) (e_f : f = f_1)
  (hf :
    ∀ (i j : 𝒰.I₀),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f i) (𝒰.f j)) (f i) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (f j)),
  𝒰.glueMorphisms f hf = 𝒰.glueMorphisms f_1 ⋯
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.op_le_op_iff : ∀ {G : Type u_2} [inst : AddGroup G] {S₁ S₂ : AddSubgroup G}, S₁.op ≤ S₂.op ↔ S₁ ≤ S₂