mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.isoZeroOfMonoZero_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (x : CategoryTheory.Mono 0),
  (CategoryTheory.Limits.isoZeroOfMonoZero x).inv = 0
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_associator : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  self.map₂ (CategoryTheory.Bicategory.associator f g h).hom =
    CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g).hom (self.map h))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h).inv)
            (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv)))
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_toAddMonoidHomEquiv_symm : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : A →+ Additive M),
  ⇑(AddChar.toAddMonoidHomEquiv.symm ψ) = ⇑Additive.toMul ∘ ⇑ψ
-- Mathlib.Data.Rel
SetRel.inv_id : ∀ {α : Type u_1}, SetRel.id.inv = SetRel.id
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- Given any pair of coprime elements of `R`, there exists a matrix in `SL(2, R)` having those
entries as its left or right column.  -/
IsCoprime.exists_SL2_col : ∀ {R : Type u_1} [inst : CommRing R] {a b : R}, IsCoprime a b → ∀ (j : Fin 2), ∃ g, ↑g 0 j = a ∧ ↑g 1 j = b
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The mixed embedding of a number field `K` into the mixed space of `K`.  -/
NumberField.mixedEmbedding : (K : Type u_1) → [inst : Field K] → K →+* NumberField.mixedEmbedding.mixedSpace K
-- Mathlib.Topology.Baire.BaireMeasurable
/-- Notation to say that a property of points in a topological space holds on a nonmeager set.  -/
Topology.«term∃ᵇ_,_» : Lean.ParserDescr
-- Mathlib.NumberTheory.NumberField.Units.Basic
/-- The image of `torsion K` by a complex embedding is the group of complex roots of unity of
order `torsionOrder K`.
 -/
NumberField.Units.map_complexEmbedding_torsion : ∀ (K : Type u_1) [inst : Field K] [NumberField K] (φ : K →+* ℂ),
  Subgroup.map (NumberField.Units.complexEmbedding φ) (NumberField.Units.torsion K) =
    rootsOfUnity (NumberField.Units.torsionOrder K) ℂ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : X → R → R` tends to `f x₀` uniformly (along `𝓝[s] x₀`) on the spectrum of `a`,
and eventually each `f x` is continuous on the spectrum of `a` and maps zero to itself, then
`fun x ↦ cfcₙ (f x) a` is continuous at `x₀` within `s`.  -/
continuousWithinAt_cfcₙ_fun : ∀ {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : Nontrivial R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : NonUnitalRing A] [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A]
  [inst_10 : SMulCommClass R A A] [inst_11 : IsScalarTower R A A]
  [inst_12 : NonUnitalContinuousFunctionalCalculus R A p] [inst_13 : TopologicalSpace X] {f : X → R → R} {a : A}
  {x₀ : X} {s : Set X},
  TendstoUniformlyOn f (f x₀) (nhdsWithin x₀ s) (quasispectrum R a) →
    (∀ᶠ (x : X) in nhdsWithin x₀ s, ContinuousOn (f x) (quasispectrum R a)) →
      autoParam (∀ᶠ (x : X) in nhdsWithin x₀ s, f x 0 = 0) continuousWithinAt_cfcₙ_fun._auto_1 →
        ContinuousWithinAt (fun x => cfcₙ (f x) a) s x₀
-- Mathlib.Topology.Maps.OpenQuotient
/-- An open quotient map is a quotient map.  -/
IsOpenQuotientMap.isQuotientMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenQuotientMap f → Topology.IsQuotientMap f
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.applyPartition.go.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.lt = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.lt = Ordering.eq → motive Ordering.eq) (h_3 : Ordering.lt = Ordering.gt → motive Ordering.gt),
  (match h : Ordering.lt with
    | Ordering.lt => h_1 h
    | Ordering.eq => h_2 h
    | Ordering.gt => h_3 h) =
    h_1 ⋯
-- Mathlib.Computability.Encoding
Computability.Γ'.comma : Computability.Γ'
-- Lean.Server.RequestCancellation
Lean.Server.CancellableM.checkCancelled : Lean.Server.CancellableM Unit
-- Init.Data.Float.Model.Unpacked.Sign
Float.Model.UnpackedFloat.instBEqSign.beq : Float.Model.UnpackedFloat.Sign → Float.Model.UnpackedFloat.Sign → Bool
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.exists : ∀ {α : Type u} {p : WithOne α → Prop}, (∃ x, p x) ↔ p 1 ∨ ∃ a, p ↑a
-- Mathlib.Algebra.Lie.Character
LieAlgebra.lieCharacter_apply_lie : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (χ : LieAlgebra.LieCharacter R L) (x y : L), χ ⁅x, y⁆ = 0
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
/-- If `f : ℂ → ℂ` is complex-analytic, then its imaginary part is harmonic.
 -/
AnalyticAt.harmonicAt_im : ∀ {x : ℂ} {f : ℂ → ℂ}, AnalyticAt ℂ f x → InnerProductSpace.HarmonicAt (fun z => (f z).im) x
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.eq_5 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1) (ids : Array ℕ)
  (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))),
  (match some (Std.Tactic.BVDecide.LRAT.Action.del ids) with
    | none => h_1 ()
    | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
    | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) =
    h_5 ids
-- Mathlib.GroupTheory.Coset.Basic
leftCosetEquivalence_rel : ∀ {α : Type u_1} [inst : Mul α] (s : Set α), Equivalence (LeftCosetEquivalence s)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.mk.injEq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (toFun : α → MeasureTheory.Measure β) (measurable' : Measurable toFun) (toFun_1 : α → MeasureTheory.Measure β)
  (measurable'_1 : Measurable toFun_1),
  ({ toFun := toFun, measurable' := measurable' } = { toFun := toFun_1, measurable' := measurable'_1 }) =
    (toFun = toFun_1)
-- Mathlib.RingTheory.Smooth.Kaehler
/-- Given a tower of algebras `S/P/R`, with `I = ker(P → S)`,
this is the `R`-derivative `P/I² → S ⊗[P] Ω[P⁄R]` given by `[x] ↦ 1 ⊗ D x`.
 -/
derivationQuotKerSq : (R : Type u_1) →
  (P : Type u_2) →
    (S : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing P] →
          [inst_2 : CommRing S] →
            [inst_3 : Algebra R P] →
              [inst_4 : Algebra P S] →
                [inst_5 : Algebra R S] →
                  [inst_6 : IsScalarTower R P S] →
                    Derivation R (P ⧸ RingHom.ker (algebraMap P S) ^ 2) (TensorProduct P S Ω[P⁄R])
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_congr : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k k' : α}, compare k k' = Ordering.eq → (k ∈ t ↔ k' ∈ t)
-- Init.Data.SInt.Basic
/-- Truncating division for 8-bit signed integers, rounding towards zero. Usually accessed via the `/`
operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int8.div 10 3 = 3`
* `Int8.div 10 (-3) = (-3)`
* `Int8.div (-10) (-3) = 3`
* `Int8.div (-10) 3 = (-3)`
* `Int8.div 10 0 = 0`
 -/
Int8.div : Int8 → Int8 → Int8
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_comp_neg_atBot_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] {l : Filter α}
  {f : G → α}, Filter.Tendsto (fun x => f (-x)) Filter.atBot l ↔ Filter.Tendsto f Filter.atTop l
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- To check whether two maps are coequalized by both maps of a cofork, it suffices to check it for
the second map  -/
CategoryTheory.Limits.Cofork.coequalizer_ext : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (s : CategoryTheory.Limits.Cofork f g)
  {W : C} {k l : s.pt ⟶ W},
  CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l →
    ∀ (j : CategoryTheory.Limits.WalkingParallelPair),
      CategoryTheory.CategoryStruct.comp (s.ι.app j) k = CategoryTheory.CategoryStruct.comp (s.ι.app j) l
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.smul_mk : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] (σ : Gal(K/k)) (φ : K →+* ℂ),
  σ • NumberField.InfinitePlace.mk φ = NumberField.InfinitePlace.mk (φ.comp ↑σ.symm)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.mem_of_mem_roc : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : LT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxc.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α] {a b : α}, r.lower ≤ b → (a ∈ b<...=r.upper) → a ∈ r
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommFold_empty : ∀ {α : Type u_3} (op : α → α → α) [assoc : Std.Associative op] (h : {x | x ∈ 0}.Pairwise fun x y => op x y = op y x)
  (a : α), Multiset.noncommFold op 0 h a = a
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuous_restrict_iff : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] (F : ι → X → α)
  {S : Set X}, Equicontinuous (S.domRestrict ∘ F) ↔ EquicontinuousOn F S
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.prop_limit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] [P.IsClosedUnderLimitsOfShape J] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasLimit F], (∀ (j : J), P (F.obj j)) → P (CategoryTheory.Limits.limit F)
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuous_restrict_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  LowerSemicontinuous (s.domRestrict f) ↔ LowerSemicontinuousOn f s
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
Lex.instDistribSMul : {G₀ : Type u_1} → {M₀ : Type u_2} → [inst : AddZeroClass M₀] → [DistribSMul G₀ M₀] → DistribSMul (Lex G₀) M₀
-- Mathlib.RingTheory.Ideal.Operations
Ideal.exists_subset_radical_span_sup_of_subset_radical_sup : ∀ {R : Type u_1} [inst : CommSemiring R] (s : Set R) (I J : Ideal R),
  s ⊆ ↑(I ⊔ J).radical → ∃ t, Set.range t ⊆ ↑I ∧ s ⊆ ↑(Ideal.span (Set.range t) ⊔ J).radical
-- Mathlib.CategoryTheory.Elements
/-- Constructor for morphisms in the category of elements of a functor to types.  -/
CategoryTheory.CategoryOfElements.homMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type w)} →
      (x y : F.Elements) → (f : x.fst ⟶ y.fst) → (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd = y.snd → (x ⟶ y)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullbackConeOfRightIso_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g],
  (CategoryTheory.Limits.pullbackConeOfRightIso f g).fst =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullbackConeOfRightIso f g).pt
-- Mathlib.NumberTheory.ModularForms.LFunction
CuspForm.hasSum_Λ : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} {F : Type u_1} [inst_1 : FunLike F UpperHalfPlane ℂ]
  (f : F) {s : ℂ} [inst_2 : CuspFormClass F Γ k] (hk : 0 < k),
  ↑k / 2 + 1 < s.re →
    HasSum
      (fun n =>
        ↑Real.pi ^ (-s) * Complex.Gamma s * (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) /
          ↑(2 * ↑n / Γ.strictWidthInfty) ^ s)
      (ModularForm.Λ hk f s)
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.sub : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S) (x y : WittVector p R),
  WittVector.mapFun (⇑f) (x - y) = WittVector.mapFun (⇑f) x - WittVector.mapFun (⇑f) y
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedHull.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] (s : Set E),
  balancedHull 𝕜 s = ⋃ r, ⋃ (_ : ‖r‖ ≤ 1), r • s
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Operations.0.SimpleGraph.Walk.concatRecAux.match_1.eq_2 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → Sort u_2) (v v_1 : V) (h : G.Adj u v_1)
  (p : G.Walk v_1 v) (h_1 : Unit → motive u SimpleGraph.Walk.nil)
  (h_2 : (v v_2 : V) → (h : G.Adj u v_2) → (p : G.Walk v_2 v) → motive v (SimpleGraph.Walk.cons h p)),
  (match v, SimpleGraph.Walk.cons h p with
    | .(u), SimpleGraph.Walk.nil => h_1 ()
    | v, SimpleGraph.Walk.cons h p => h_2 v v_2 h p) =
    h_2 v v_1 h p
-- Mathlib.Algebra.Order.Group.Synonym
isAddLeftRegular_ofLex : ∀ {α : Type u_1} [inst : AddMonoid α] {a : Lex α}, IsAddLeftRegular (ofLex a) ↔ IsAddLeftRegular a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β k}, k ∉ m₂ → (m₁ \ m₂).getD k fallback = m₁.getD k fallback
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabSorry : Lean.Elab.Term.TermElab
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.tensorTensorTensorComm_comp_map : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9}
  {T : Type u_10} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P]
  [inst_4 : AddCommMonoid Q] [inst_5 : AddCommMonoid S] [inst_6 : AddCommMonoid T] [inst_7 : Module R M]
  [inst_8 : Module R N] [inst_9 : Module R Q] [inst_10 : Module R S] [inst_11 : Module R T] [inst_12 : Module R P]
  {V : Type u_13} {W : Type u_14} [inst_13 : AddCommMonoid V] [inst_14 : AddCommMonoid W] [inst_15 : Module R V]
  [inst_16 : Module R W] (f : M →ₗ[R] S) (g : N →ₗ[R] T) (h : P →ₗ[R] V) (j : Q →ₗ[R] W),
  ↑(TensorProduct.tensorTensorTensorComm R S T V W) ∘ₗ
      TensorProduct.map (TensorProduct.map f g) (TensorProduct.map h j) =
    TensorProduct.map (TensorProduct.map f h) (TensorProduct.map g j) ∘ₗ
      ↑(TensorProduct.tensorTensorTensorComm R M N P Q)
-- Mathlib.Analysis.Complex.Hadamard
/-- The supremum of the norm of `scale f l u` on the line `z.re = 0` is the same as the supremum
of `f` on the line `z.re = l`.  -/
Complex.HadamardThreeLines.sSupNormIm_scale_left : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) {l u : ℝ},
  l < u →
    Complex.HadamardThreeLines.sSupNormIm (Complex.HadamardThreeLines.scale f l u) 0 =
      Complex.HadamardThreeLines.sSupNormIm f l
-- Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
CategoryTheory.MorphismProperty.instIsStableUnderCoproductsOfShapeFunctorMonomorphismsOfHasCoproductsOfShapeOfHasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type u'') [inst_1 : CategoryTheory.Category.{v'', u''} J]
  (K' : Type u') [(CategoryTheory.MorphismProperty.monomorphisms C).IsStableUnderCoproductsOfShape K']
  [CategoryTheory.Limits.HasCoproductsOfShape K' C] [CategoryTheory.Limits.HasPullbacks C],
  (CategoryTheory.MorphismProperty.monomorphisms (CategoryTheory.Functor J C)).IsStableUnderCoproductsOfShape K'
-- Mathlib.FieldTheory.Normal.Defs
IntermediateField.normal : ∀ (F : Type u_1) [inst : Field F] (E : Type u_3) [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E)
  [Normal F E], Normal (↥K) E
-- Mathlib.CategoryTheory.Yoneda
/-- The Yoneda embedding is full.  -/
CategoryTheory.Yoneda.yoneda_full : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], CategoryTheory.yoneda.Full
-- Mathlib.Data.Stream.Init
Stream'.mem_cons : ∀ {α : Type u} (a : α) (s : Stream' α), a ∈ Stream'.cons a s
-- Mathlib.Topology.Instances.CantorSet
/-- The ternary Cantor set is compact.  -/
isCompact_cantorSet : IsCompact cantorSet
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
/-- The natural transformation which gives the augmentation of the alternating face map
complex attached to an augmented simplicial object.  -/
AlgebraicTopology.AlternatingFaceMapComplex.ε : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        CategoryTheory.SimplicialObject.Augmented.drop.comp (AlgebraicTopology.alternatingFaceMapComplex C) ⟶
          CategoryTheory.SimplicialObject.Augmented.point.comp (ChainComplex.single₀ C)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The homology data for the short complex given by differentials on the
`r`th page of the spectral sequence which shows that the homology identifies
to an object on the next page.  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    (r r' : ℤ) →
                      (hrr' : r + 1 = r') →
                        (hr : r₀ ≤ r) →
                          (pq pq' pq'' : κ) →
                            (c r).prev pq' = pq →
                              (c r).next pq' = pq'' →
                                (i₀' i₀ i₁ i₂ i₃ i₃' : ι) →
                                  i₀' = data.i₀ r' pq' ⋯ →
                                    i₀ = data.i₀ r pq' ⋯ →
                                      i₁ = data.i₁ pq' →
                                        i₂ = data.i₂ pq' →
                                          i₃ = data.i₃ r pq' ⋯ →
                                            i₃' = data.i₃ r' pq' ⋯ →
                                              (n₀ n₁ n₂ : ℤ) →
                                                n₁ = data.deg pq' →
                                                  [X.HasSpectralSequence data] →
                                                    autoParam (n₀ + 1 = n₁)
                                                        CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_1 →
                                                      autoParam (n₁ + 1 = n₂)
                                                          CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_3 →
                                                        ((CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X
                                                                data r hr).sc'
                                                            pq pq' pq'').HomologyData
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.trim_eq_map : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0),
  μ.trim hm = MeasureTheory.Measure.map id μ
-- ProofWidgets.Presentation.Expr
/-- This component shows a selection of all known and applicable `ProofWidgets.ExprPresenter`s which
are used to render the expression when selected. The one with highest precedence (TODO) is shown by
default.  -/
ProofWidgets.ExprPresentation : ProofWidgets.Component ProofWidgets.ExprPresentationProps
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.map_eq_zero : ∀ {R : Type u} {S : Type v} [inst : Ring R] [IsSimpleRing R] [inst_2 : Semiring S] [Nontrivial S] {p : Polynomial R}
  (f : R →+* S), Polynomial.map f p = 0 ↔ p = 0
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instCStarRing : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : NonUnitalNormedRing β] [inst_2 : StarRing β]
  [inst_3 : CStarRing β], CStarRing (ZeroAtInftyContinuousMap α β)
-- Lean.Data.PersistentArray
Lean.PersistentArray.foldlM : {α : Type u} →
  {m : Type v → Type w} → [Monad m] → {β : Type v} → Lean.PersistentArray α → (β → α → m β) → β → optParam ℕ 0 → m β
-- Mathlib.RingTheory.Bialgebra.Hom
Bialgebra.subsingleton_to_ring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A],
  Subsingleton (A →ₐc[R] R)
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_sup_of_normal_right : ∀ {G : Type u_1} [inst : Group G] {s t : Subgroup G} [ht : t.Normal] {x : G}, x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_union_of_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₂ → k ∈ m₁ ∪ m₂
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.setTR.go.eq_3 : ∀ {α : Type u_1} (l : List α) (a : α) (a_1 : Array α) (x_3 : α) (xs : List α) (n : ℕ),
  List.setTR.go✝ l a (x_3 :: xs) n.succ a_1 = List.setTR.go✝ l a xs n (a_1.push x_3)
-- Mathlib.CategoryTheory.Enriched.Basic
/-- `app` is a natural transformation.  -/
CategoryTheory.GradedNatTrans.naturality : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D}
  (self : CategoryTheory.GradedNatTrans A F G) (X Y : C),
  CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (self.app Y))
        (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.app X) (G.map X Y))
      (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- The `Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_right`
for commutative rings.  -/
Submodule.LinearDisjoint.rank_inf_le_one_of_flat_right : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N → ∀ [Module.Flat R ↥N], Module.rank R ↥(M ⊓ N) ≤ 1