mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getEntry! : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → [Inhabited ((a : α) × β a)] → (a : α) × β a
-- Mathlib.Computability.RecursiveIn
Primrec₂.computableIn₂ : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ} {O : Set (ℕ →. ℕ)}, Primrec₂ f → ComputableIn₂ O f
-- Mathlib.Data.Fin.Tuple.Reflection
/-- This can be used to prove
```lean
example [CommMonoid α] (a : Fin 3 → α) : ∏ i, a i = a 0 * a 1 * a 2 :=
  (prod_eq _).symm
```
 -/
FinVec.prod_eq : ∀ {α : Type u_1} [inst : CommMonoid α] {m : ℕ} (a : Fin m → α), FinVec.prod a = ∏ i, a i
-- Mathlib.Order.SymmDiff
ofDual_bihimp : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : αᵒᵈ),
  OrderDual.ofDual (bihimp a b) = symmDiff (OrderDual.ofDual a) (OrderDual.ofDual b)
-- Init.Core
BitVec.ofFin.injEq : ∀ {w : ℕ} (toFin toFin_1 : Fin (2 ^ w)), ({ toFin := toFin } = { toFin := toFin_1 }) = (toFin = toFin_1)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.instStrongHomClass : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.StrongHomClass (L.Equiv M N) M N
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instWeaklyLocallyCompactSpacePrincipalOfFactLeFilterCofiniteOfCompactSpaceElem : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)] {S : Set ι}
  [∀ (i : ι), WeaklyLocallyCompactSpace (R i)] [hS : Fact (Filter.cofinite ≤ Filter.principal S)]
  [hAcompact : ∀ (i : ι), CompactSpace ↑(A i)],
  WeaklyLocallyCompactSpace (RestrictedProduct (fun i => R i) (fun i => A i) (Filter.principal S))
-- Mathlib.Util.Export
Lean.Export.instInhabitedState.default : Lean.Export.State
-- Mathlib.Analysis.Complex.Hadamard
/-- **Hadamard three-line theorem** on `re ⁻¹' [0, 1]`: If `f` is a bounded function, continuous on the
closed strip `re ⁻¹' [0, 1]` and differentiable on open strip `re ⁻¹' (0, 1)`, then for
`M(x) := sup ((norm ∘ f) '' re ⁻¹' {x})` we have that for all `z` in the closed strip
`re ⁻¹' [0, 1]` the inequality `‖f(z)‖ ≤ M(0) ^ (1 - z.re) * M(1) ^ z.re` holds.  -/
Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip₀₁ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) {z : ℂ},
  z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1 →
    DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1) →
      BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) →
        ‖f z‖ ≤ ‖Complex.HadamardThreeLines.interpStrip f z‖
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.bot_covers : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : CategoryTheory.Sieve X) (f : Y ⟶ X),
  ⊥.Covers S f ↔ S.arrows f
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.map_post : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C]
  {G : CategoryTheory.Functor J C} (α : F ⟶ G) {D : Type u'} [inst_3 : CategoryTheory.Category.{v', u'} D]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D] (H : CategoryTheory.Functor C D),
  CategoryTheory.CategoryStruct.comp (H.map (CategoryTheory.Limits.limMap α)) (CategoryTheory.Limits.limit.post G H) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.post F H)
      (CategoryTheory.Limits.limMap (CategoryTheory.Functor.whiskerRight α H))
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
/-- The main theorem of this file: given a precoverage `J` on `C`, a `Type*`-valued presheaf on `C` is
a sheaf for the associated Grothendieck topology if and only if it is a sheaf for all pullback
sieves of presieves in `J`.
 -/
CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {J : CategoryTheory.Precoverage C}
  (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)),
  CategoryTheory.Presieve.IsSheaf J.toGrothendieck P ↔
    ∀ {X Y : C} {f : Y ⟶ X},
      ∀ R ∈ J.coverings X,
        CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.generate R)).arrows
-- Mathlib.Topology.UniformSpace.Defs
/-- A uniform space generates a topological space  -/
UniformSpace.Core.toTopologicalSpace : {α : Type u} → UniformSpace.Core α → TopologicalSpace α
-- Mathlib.CategoryTheory.Functor.Const
/-- The canonical isomorphism
`F ⋙ Functor.const J ≅ Functor.const F ⋙ (whiskeringRight J _ _).obj L`.  -/
CategoryTheory.Functor.compConstIso : (J : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        {D : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} D] →
            (F : CategoryTheory.Functor C D) →
              F.comp (CategoryTheory.Functor.const J) ≅
                (CategoryTheory.Functor.const J).comp ((CategoryTheory.Functor.whiskeringRight J C D).obj F)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral norm is power-multiplicative.  -/
isPowMul_spectralNorm : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] [IsUltrametricDist K]
  [h_alg : Algebra.IsAlgebraic K L], IsPowMul (spectralNorm K L)
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.toMessageData? : Aesop.Script.StepTree → Option Lean.MessageData
-- Init.Data.ByteArray.Lemmas
ByteArray.append_eq_append_iff_of_size_eq_right : ∀ {ws xs ys zs : ByteArray}, ys.size = zs.size → (ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs)
-- Mathlib.Data.FunLike.Graded
Graded.map_mem_iff : ∀ {E : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [inst : SetLike σ A]
  [inst_1 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_2 : EquivLike E A B] [GradedEquivLike E 𝒜 ℬ] (e : E) {i : ι}
  {x : A}, e x ∈ ℬ i ↔ x ∈ 𝒜 i
-- Aesop.Script.StructureDynamic
/-- The tactic invocation steps corresponding to the original unstructured
script, but with `MVarId` keys adjusted to fit the current `MetaM` state. This
state evolves during dynamic structuring and we continually update the `steps`
so that this map's keys refer to metavariables which exist in the current
`MetaM` state.  -/
Aesop.Script.DynStructureM.Context.steps : Aesop.Script.DynStructureM.Context → Lean.PHashMap Lean.MVarId (ℕ × Aesop.Script.Step)
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- If two `R`-alternating maps from `R` are equal on 1, then they are equal.

This is the alternating version of `LinearMap.ext_ring`.  -/
AlternatingMap.ext_ring : ∀ {N : Type u_3} [inst : AddCommMonoid N] {ι : Type u_7} {R : Type u_12} [inst_1 : CommSemiring R] [inst_2 : Module R N]
  [Finite ι] ⦃f g : R [⋀^ι]→ₗ[R] N⦄, ((f fun x => 1) = g fun x => 1) → f = g
-- Std.Data.TreeSet.Basic
/-- Carries out a monadic action on each element in the tree set in ascending order.  -/
Std.TreeSet.forM : {α : Type u} →
  {cmp : α → α → Ordering} →
    {m : Type w → Type w₂} → [Monad m] → (α → m PUnit.{w + 1}) → Std.TreeSet α cmp → m PUnit.{w + 1}
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Let `A, B` be two graded rings with the same indexing set and `g : 𝒜 →+*ᵍ ℬ` be a graded ring
homomorphism. Let `P ≤ A` be a submonoid and `Q ≤ B` be a submonoid such that `P ≤ g⁻¹ Q`, then `g`
induces a map from the homogeneous localization `A⁰_P` to the homogeneous localization `B⁰_Q`.
 -/
HomogeneousLocalization.map : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} →
                  [inst_5 : GradedRing 𝒜] →
                    {B : Type u_4} →
                      {τ : Type u_5} →
                        [inst_6 : CommRing B] →
                          [inst_7 : SetLike τ B] →
                            [inst_8 : AddSubgroupClass τ B] →
                              {ℬ : ι → τ} →
                                [inst_9 : GradedRing ℬ] →
                                  {P : Submonoid A} →
                                    {Q : Submonoid B} →
                                      (g : 𝒜 →+*ᵍ ℬ) →
                                        P ≤ Submonoid.comap g Q →
                                          HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization ℬ Q
-- Mathlib.Data.List.OfFn
List.mem_ofFn' : ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (a : α), a ∈ List.ofFn f ↔ a ∈ Set.range f
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.leadingCoeff_eq_zero : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A],
  Function.Injective D → (AddMonoidAlgebra.leadingCoeff D p = 0 ↔ p = 0)
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.mem_comap : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β)
  {L : CompleteSublattice β} {a : α}, a ∈ CompleteSublattice.comap f L ↔ f a ∈ L
-- Mathlib.AlgebraicGeometry.Gluing
/-- The glued scheme of a glued space.  -/
AlgebraicGeometry.Scheme.GlueData.glued : AlgebraicGeometry.Scheme.GlueData → AlgebraicGeometry.Scheme
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.sum_comp : ∀ {R : Type u} {ι : Type y} [inst : Semiring R] (s : Finset ι) (p : ι → Polynomial R) (q : Polynomial R),
  (∑ i ∈ s, p i).comp q = ∑ i ∈ s, (p i).comp q
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- Given a TM2 machine `M` and a set `S` of states, `Supports M S` means that all states in
`S` jump only to other states in `S`.  -/
Turing.TM2.Supports : {K : Type u_1} →
  {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → [Inhabited Λ] → (Λ → Turing.TM2.Stmt Γ Λ σ) → Finset Λ → Prop
-- Mathlib.Data.DFinsupp.Multiset
Multiset.toDFinsupp_injective : ∀ {α : Type u_1} [inst : DecidableEq α], Function.Injective ⇑Multiset.toDFinsupp
-- Mathlib.Topology.ContinuousMap.Basic
/-- `Prod.swap` bundled as a `ContinuousMap`.  -/
ContinuousMap.prodSwap : {α : Type u_1} → {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → C(α × β, β × α)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (H : Subgroup G) [inst_5 : IsGaloisGroup G K L],
  Module.finrank (↥(FixedPoints.intermediateField ↥H)) L = Nat.card ↥H
-- Mathlib.Order.BoundedOrder.Basic
not_isMax_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] [Nontrivial α], ¬IsMax ⊥
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.instTopologicalSpaceMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M],
  MulOpposite.instTopologicalSpaceMulOpposite = TopologicalSpace.induced MulOpposite.unop inst
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.finrank_adjoin_simple_eq_one_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E},
  Module.finrank F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_algebra_tower`.

---

Let `T / S / R` be a tower of algebras, `p, P, Q` be ideals in `R, S, T` respectively,
and `P` and `Q` are prime. If `P = Q ∩ S`, then `e (Q | p) = e (P | p) * e (Q | P)`.  -/
Ideal.ramificationIdx_algebra_tower : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [IsScalarTower R S T] [IsDedekindDomain S]
  [IsDedekindDomain T] {p : Ideal R} {P : Ideal S} {Q : Ideal T} [hpm : P.IsPrime] [hqm : Q.IsPrime],
  Ideal.map (algebraMap S T) P ≠ ⊥ →
    Ideal.map (algebraMap R T) p ≠ ⊥ →
      Ideal.map (algebraMap S T) P ≤ Q → p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q
-- Init.Data.BitVec.Lemmas
BitVec.toFin_one : ∀ {w : ℕ}, BitVec.toFin 1 = 1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.mem_toArray_iff_mem : ∀ {α : Type u} {r : Std.Rco α} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLE α] [inst_7 : Std.Rxo.IsAlwaysFinite α]
  {a : α}, a ∈ r.toArray ↔ a ∈ r
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.coe_toEquiv : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), ⇑e.toEquiv = ⇑e
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.RootOrdered.eq_2 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x : α) (c : RBTree.RBColor) (parent : RBTree.RBNode.Path α) (x_2 : α)
  (r : RBTree.RBNode α),
  RBTree.RBNode.Path.RootOrdered cmp (RBTree.RBNode.Path.left c parent x_2 r) x =
    (RBTree.RBNode.cmpLT cmp x x_2 ∧ RBTree.RBNode.Path.RootOrdered cmp parent x)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.sup_toSubfield : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  (S T : IntermediateField F E), (S ⊔ T).toSubfield = S.toSubfield ⊔ T.toSubfield
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- Canonical map from the stalk of `smoothSheaf IM I M N` at `x` to `N`, given by evaluating
sections at `x`, considered as a morphism in the category of types.  -/
smoothSheaf.evalHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            {M : Type u} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (N : Type u) →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H N] →
                                        (x : ↑(TopCat.of M)) → (smoothSheaf IM I M N).presheaf.stalk x ⟶ N
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.Nondegenerate.separatingLeft : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Finite m]
  [inst_2 : Finite n] {M : Matrix m n R}, M.Nondegenerate → M.SeparatingLeft
-- Init.Data.List.Basic
/-- Removes the longest prefix of a list for which `p` returns `true`.

Elements are removed from the list until one is encountered for which `p` returns `false`. This
element and the remainder of the list are returned.

`O(|l|)`.

Examples:
 * `[1, 3, 2, 4, 2, 7, 4].dropWhile (· < 4) = [4, 2, 7, 4]`
 * `[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 4) = [8, 3, 2, 4, 2, 7, 4]`
 * `[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 100) = []`
 -/
List.dropWhile : {α : Type u} → (α → Bool) → List α → List α
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.ext_iff : ∀ {E : Type u_3} [inst : AddGroup E] {p q : NonarchAddGroupNorm E}, p = q ↔ ∀ (x : E), p x = q x
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.coe_copy : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) (f' : E → F)
  (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
/-- Category of groupoids  -/
CategoryTheory.Grpd : Type (max (u + 1) u (v + 1))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_erase_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k fallback : α}, (m.erase k).getKeyD k fallback = fallback
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.comp_hom_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {R S T : CategoryTheory.AddGrp C} (f : R ⟶ S) (g : S ⟶ T) {Z : C} (h : T.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom.hom h =
    CategoryTheory.CategoryStruct.comp f.hom.hom (CategoryTheory.CategoryStruct.comp g.hom.hom h)
-- Lean.Data.NameMap.Basic
Lean.NameHashSet.contains : Lean.NameHashSet → Lean.Name → Bool
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.addUnits_sInf : ∀ {M : Type u_1} [inst : AddMonoid M] {s : Set (AddSubmonoid M)}, (sInf s).addUnits = ⨅ S ∈ s, S.addUnits
-- Mathlib.Data.Rel
SetRel.isSymm_symmetrize : ∀ {α : Type u_1} {R : SetRel α α}, R.symmetrize.IsSymm
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
/-- Simproc version of `assoc_symm_comp_map_assoc` that only fires when `f₁ ≠ id`.  -/
CoassocSimps.assoc_symm_comp_map_assoc_simproc : Lean.Meta.Simp.Simproc
-- Mathlib.Analysis.Normed.Field.Krasner
IsKrasner.krasner : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField L] [inst_1 : Field K] [inst_2 : Algebra K L] [IsKrasner K L]
  {x y : L},
  (minpoly K x).Separable →
    (Polynomial.map (algebraMap K L) (minpoly K x)).Splits →
      IsIntegral K y → (∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖) → x ∈ K⟮y⟯
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.rightUnitor_hom_app : ∀ {B C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B),
  (CategoryTheory.Bicategory.rightUnitor F).hom.toNatTrans.app X = CategoryTheory.eqToHom ⋯
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instTop : {α : Type u_1} → [inst : LE α] → Top (UpperSet α)
-- Aesop.Forward.State
Aesop.instBEqRawHyp : BEq Aesop.RawHyp
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncateFun_surjective : ∀ (p n : ℕ) (R : Type u_1) [CommRing R], Function.Surjective (WittVector.truncateFun n)
-- Mathlib.NumberTheory.Chebyshev
_private.Mathlib.NumberTheory.Chebyshev.0.Chebyshev.sum_b_eq_b_add_sum_add_sum_add_sum : ∀ (x : ℝ) (N : ℕ),
  ∑ n ∈ Finset.Icc 1 (1 + 6 * N), Chebyshev.b✝ x n =
    Chebyshev.b✝ x 1 + ∑ n ∈ Finset.Icc 1 (3 * N), Chebyshev.b✝ x (2 * n) +
        ∑ n ∈ Finset.Icc 1 (2 * N), Chebyshev.b✝ x (3 * n) +
      ∑ n ∈ Finset.Icc 1 N, Chebyshev.c✝ x n
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.SupportsStmt.eq_4 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (S : Finset Λ) (a : Γ → σ → Bool) (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.SupportsStmt S (Turing.TM1.Stmt.branch a q₁ q₂) =
    (Turing.TM1.SupportsStmt S q₁ ∧ Turing.TM1.SupportsStmt S q₂)
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.FiniteMeasure.prod_apply_symm : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) (s : Set (α × β)),
  MeasurableSet s → (μ.prod ν) s = (∫⁻ (y : β), ↑μ ((fun x => (x, y)) ⁻¹' s) ∂↑ν).toNNReal
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ico_succ : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∑ i ∈ Finset.Ico a.succ b.succ, f i = ∑ i ∈ Finset.Ico a b, f i.succ
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.liftAux_tprodCoeff : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  (φ : MultilinearMap R s E) (z : R) (f : (i : ι) → s i),
  (PiTensorProduct.liftAux φ) (PiTensorProduct.tprodCoeff R z f) = z • φ f
-- Std.Http.Internal.Char
/-- Checks if a character is a hexadecimal digit (0-9, a-f, or A-F).
 -/
Std.Http.Internal.Char.isHexDigit : Char → Bool
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsOpenImmersionInrScheme : ∀ (X Y : AlgebraicGeometry.Scheme), AlgebraicGeometry.IsOpenImmersion CategoryTheory.Limits.coprod.inr
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.addWeight_nil : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : AddMonoid R] (w : {i j : V} → (i ⟶ j) → R) (a : V),
  Quiver.Path.addWeight (fun {i j} => w) Quiver.Path.nil = 0
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.sUnion_union_sUnion_disjointOfDiffUnion_of_subset : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C)
  (hI : ↑I ⊆ C), (∀ t ∈ I, t ⊆ s) → ⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI) = s
-- Init.Data.SInt.Lemmas
Int64.ofIntClamp.eq_1 : ∀ (i : ℤ),
  Int64.ofIntClamp i =
    if hl : Int64.minValue.toInt ≤ i then
      if hr : i ≤ Int64.maxValue.toInt then Int64.ofIntLE i hl hr else Int64.maxValue
    else Int64.minValue
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeries_zero : ∀ (G : Type u_1) [inst : AddGroup G], AddSubgroup.upperCentralSeries G 0 = ⊥
-- Mathlib.Algebra.Category.FGModuleCat.Basic
LinearEquiv.toFGModuleCatIso_inv : ∀ {R : Type u} [inst : Ring R] {V W : Type v} [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : Module.Finite R V] [inst_4 : AddCommGroup W] [inst_5 : Module R W] [inst_6 : Module.Finite R W]
  (e : V ≃ₗ[R] W), e.toFGModuleCatIso.inv = CategoryTheory.ConcreteCategory.ofHom ↑e.symm
-- Mathlib.Analysis.Normed.Module.Complemented
ContinuousLinearMap.coe_equivProdOfSurjectiveOfIsCompl : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : CompleteSpace E] [inst_8 : CompleteSpace (F × G)]
  {f : E →L[𝕜] F} {g : E →L[𝕜] G} (hf : (↑f).range = ⊤) (hg : (↑g).range = ⊤) (hfg : IsCompl (↑f).ker (↑g).ker),
  ↑↑(f.equivProdOfSurjectiveOfIsCompl g hf hg hfg) = ↑(f.prod g)
-- Init.Data.SInt.Lemmas
Int16.toInt_div_of_ne_right : ∀ (a b : Int16), b ≠ -1 → (a / b).toInt = a.toInt.tdiv b.toInt
-- Init.System.IO
instMonadBaseIO : Monad BaseIO
-- Mathlib.Order.Concept
Concept.extent_ofAttributes : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β), (Concept.ofAttributes r t).extent = lowerPolar r t
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_functor_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T),
  ((CategoryTheory.StructuredArrow.mapNatIso i).functor.obj X).left = X.left
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.measure_eq_left_of_subset_of_measure_add_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s t : Set α},
  (μ + ν) t ≠ ⊤ → s ⊆ t → (μ + ν) s = (μ + ν) t → μ s = μ t
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- Infinitely differentiable diffeomorphism between `M` and `M'` with respect to `I` and `I'`.  -/
Manifold.«term_≃ₘ⟮_,_⟯_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Images
/-- The factorisation of any morphism in `ModuleCat R` through a mono.  -/
ModuleCat.monoFactorisation : {R : Type u} → [inst : Ring R] → {G H : ModuleCat R} → (f : G ⟶ H) → CategoryTheory.Limits.MonoFactorisation f