mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.hasFiniteIntegral_compProd_iff' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  ⦃f : β × γ → E⦄,
  MeasureTheory.AEStronglyMeasurable f ((κ.compProd η) a) →
    (MeasureTheory.HasFiniteIntegral f ((κ.compProd η) a) ↔
      (∀ᵐ (x : β) ∂κ a, MeasureTheory.HasFiniteIntegral (fun y => f (x, y)) (η (a, x))) ∧
        MeasureTheory.HasFiniteIntegral (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a))
-- Mathlib.Analysis.Normed.Ring.Basic
/-- This inequality is particularly useful when `c = 1` and `‖a‖ = ‖b‖ = 1` as it then shows that
chord length is a metric on the unit complex numbers.  -/
nnnorm_sub_mul_le' : ∀ {α : Type u_2} [inst : SeminormedRing α] {a b c : α}, ‖b‖₊ ≤ 1 → ‖c - a * b‖₊ ≤ ‖1 - a‖₊ + ‖c - b‖₊
-- Mathlib.Order.Filter.Pointwise
Filter.mapMonoidHom.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MulOneClass α] [inst_1 : MulOneClass β] [inst_2 : FunLike F α β]
  [inst_3 : MonoidHomClass F α β] (φ : F),
  Filter.mapMonoidHom φ = { toFun := Filter.map ⇑φ, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] (e : R ≃+* S)
  (v : IsDedekindDomain.HeightOneSpectrum S),
  (IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv e).symm v = IsDedekindDomain.HeightOneSpectrum.comap ↑e ⋯ v
-- Lean.Parser.Command
Lean.Parser.Tactic.open.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.RelSeries
RelSeries.length_ne_zero_of_nontrivial : ∀ {α : Type u_1} {r : SetRel α α} {s : RelSeries r}, {x | x ∈ s}.Nontrivial → s.length ≠ 0
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In any preadditive category, any binary biproduct satisfies
`biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y)`.
 -/
CategoryTheory.Limits.biprod.total : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.inl +
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.inr =
    CategoryTheory.CategoryStruct.id (X ⊞ Y)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightComp_hom_app_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ L₃ : CategoryTheory.Functor B T} (r : R₂ ⟶ R₁) (r' : L₃ ⟶ R₂) (X : CategoryTheory.Comma L L₃),
  ((CategoryTheory.Comma.mapRightComp L r r').hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Std.Time.Format.Modifier
Std.Time.Modifier.G.injEq : ∀ (presentation presentation_1 : Std.Time.Text),
  (Std.Time.Modifier.G presentation = Std.Time.Modifier.G presentation_1) = (presentation = presentation_1)
-- Mathlib.RepresentationTheory.Coinduced
/-- If `ρ : Representation k G A` and `φ : G →* H` then `coindV φ ρ` is the sub-`k`-module of
functions `H → A` underlying the coinduction of `ρ` along `φ`, i.e., the functions `f : H → A`
such that `f (φ g * h) = (ρ g) (f h)` for all `g : G` and `h : H`.
 -/
Representation.coindV : {k : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : Semiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] →
            (G →* H) →
              {A : Type u_4} →
                [inst_3 : AddCommMonoid A] → [inst_4 : Module k A] → Representation k G A → Submodule k (H → A)
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- The connecting homomorphism in group cohomology induced by a short exact sequence
of `G`-modules.  -/
TateCohomology.δ : {R G : Type u} →
  [inst : CommRing R] →
    [inst_1 : Group G] →
      [inst_2 : Fintype G] →
        {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} →
          S.ShortExact → (n : ℤ) → tateCohomology S.X₃ n ⟶ tateCohomology S.X₁ (n + 1)
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.instConditionallyCompleteLinearOrder : ConditionallyCompleteLinearOrder ℝ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The cokernel of `biproduct.fromSubtype f p` is `⨁ Subtype.restrict pᶜ f`.  -/
CategoryTheory.Limits.cokernelBiproductFromSubtypeIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K : Type} →
        [inst_2 : Finite K] →
          [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] →
            (f : K → C) →
              (p : K → Prop) →
                CategoryTheory.Limits.cokernel (CategoryTheory.Limits.biproduct.fromSubtype f p) ≅
                  ⨁ Subtype.restrict pᶜ f
-- Std.Time.Zoned.ZoneRules
/-- Indicates if daylight saving time is observed.
 -/
Std.Time.TimeZone.LocalTimeType.isDst : Std.Time.TimeZone.LocalTimeType → Bool
-- Mathlib.Analysis.Normed.Ring.Basic
/-- `norm` as a `MonoidWithZeroHom`.  -/
normHom : {α : Type u_2} → [inst : SeminormedRing α] → [NormOneClass α] → [NormMulClass α] → α →*₀ ℝ
-- Mathlib.Data.Multiset.MapFold
Multiset.map_map : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (g : β → γ) (f : α → β) (s : Multiset α),
  Multiset.map g (Multiset.map f s) = Multiset.map (g ∘ f) s
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.center_toSubring : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  (Subalgebra.center R A).toSubring = Subring.center A
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalAlgebra.elemental.le_centralizer_centralizer : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] [inst_5 : TopologicalSpace A]
  [inst_6 : IsSemitopologicalSemiring A] [inst_7 : ContinuousConstSMul R A] [T2Space A] (x : A),
  NonUnitalAlgebra.elemental R x ≤ NonUnitalSubalgebra.centralizer R ↑(NonUnitalSubalgebra.centralizer R {x})
-- Mathlib.Analysis.Complex.SqrtDeriv
Complex.derivWithin_sqrt : ∀ {z : ℂ}, z ∈ Complex.slitPlane → derivWithin Complex.sqrt Complex.slitPlane z = z ^ (-1 / 2) / 2
-- Lean.Elab.Do.Basic
_private.Lean.Elab.Do.Basic.0.Lean.Elab.Do.extractMonadInfo.extract? : Lean.Elab.Do.DoOps → Lean.Expr → Lean.Elab.TermElabM (Option (Lean.Elab.Do.MonadInfo × Lean.Expr))
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.inf_subgroupOf_inf_normal_of_left : ∀ {G : Type u_1} [inst : Group G] {A' A : Subgroup G} (B : Subgroup G) [hN : (A'.subgroupOf A).Normal],
  ((A' ⊓ B).subgroupOf (A ⊓ B)).Normal
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
/-- Note: this assumes that `f` is `IntervalIntegrable`, in contrast to some other lemmas here.  -/
intervalIntegral.continuousOn_primitive_interval' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b₁ b₂ : ℝ} {μ : MeasureTheory.Measure ℝ}
  {f : ℝ → E} [MeasureTheory.NullSingletonClass μ],
  IntervalIntegrable f μ b₁ b₂ → a ∈ Set.uIcc b₁ b₂ → ContinuousOn (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Set.uIcc b₁ b₂)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries_zero`. -/
lowerCentralSeries_zero : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G), S.lowerCentralSeries 0 = S
-- Mathlib.Data.Set.Restrict
Set.range_extend : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β},
  Function.Injective f →
    ∀ (g : α → γ) (g' : β → γ), Set.range (Function.extend f g g') = Set.range g ∪ g' '' (Set.range f)ᶜ
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {V : (x : M) → TangentSpace I x},
  VectorField.mlieBracketWithin I V V = 0
-- Mathlib.Order.TypeTags
WithBot.inhabited.eq_1 : ∀ {α : Type u_1}, WithBot.inhabited = { default := ⊥ }
-- Mathlib.Data.Rel
SetRel.mem_inv : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {a : α} {b : β}, (b, a) ∈ R.inv ↔ (a, b) ∈ R
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- Euler's reflection formula for the complex Gamma function.  -/
Complex.Gamma_mul_Gamma_one_sub : ∀ (z : ℂ), Complex.Gamma z * Complex.Gamma (1 - z) = ↑Real.pi / Complex.sin (↑Real.pi * z)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.EvalTacticFailure.mk : Lean.Exception → Lean.Elab.Tactic.Grind.SavedState → Lean.Elab.Tactic.Grind.EvalTacticFailure
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.ite_ae_eq_of_measure_compl_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {γ : Type u_5} (f g : α → γ) (s : Set α)
  [inst : DecidablePred fun x => x ∈ s], μ sᶜ = 0 → (fun x => if x ∈ s then f x else g x) =ᵐ[μ] f
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.trans : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} {Γ''₀ : Type u_6} [inst : Ring R]
  [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀]
  [inst_3 : LinearOrderedCommMonoidWithZero Γ''₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} {v₃ : Valuation R Γ''₀},
  v₁.IsEquiv v₂ → v₂.IsEquiv v₃ → v₁.IsEquiv v₃
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.map_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α}
  (target : Std.Sat.AIG.RefVec.MapTarget aig len), aig.decls.size ≤ (Std.Sat.AIG.RefVec.map aig target).aig.decls.size
-- Mathlib.Data.Set.Lattice
Set.iInter_false : ∀ {α : Type u_1} {s : False → Set α}, Set.iInter s = Set.univ
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousAt_iInf_dom : ∀ {ι : Type u_1} {κ : Type u_2} {X' : Type u_4} {α : Type u_6} [uα : UniformSpace α] {t : κ → TopologicalSpace X'}
  {F : ι → X' → α} {x₀ : X'} {k : κ}, EquicontinuousAt F x₀ → EquicontinuousAt F x₀
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The top map in the right unitality square.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapᵣ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶
                  F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                (F.comp (CategoryTheory.MonoidalCategory.tensorUnitRight D) ⟶
                  (CategoryTheory.MonoidalCategory.curriedTensorPre F).flip.obj
                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- If `P` is a sheaf, then `P` is isomorphic to `J.sheafify P`.  -/
CategoryTheory.GrothendieckTopology.isoSheafify : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
              {P : CategoryTheory.Functor Cᵒᵖ D} → CategoryTheory.Presheaf.IsSheaf J P → (P ≅ J.sheafify P)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertList_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.containsKey k l = false →
        Std.Internal.List.getKeyD k (Std.Internal.List.insertList l toInsert) fallback =
          Std.Internal.List.getKeyD k toInsert fallback
-- Init.Grind.Ring.Basic
Lean.Grind.CommSemiring.mul_pow : ∀ {α : Type u} [inst : Lean.Grind.CommSemiring α] (a b : α) (n : ℕ), (a * b) ^ n = a ^ n * b ^ n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A kernel fork for the kernel of `BinaryBicone.fst`. It consists of the morphism
`BinaryBicone.inr`.  -/
CategoryTheory.Limits.BinaryBicone.fstKernelFork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → (c : CategoryTheory.Limits.BinaryBicone X Y) → CategoryTheory.Limits.KernelFork c.fst
-- Mathlib.Algebra.Free
FreeAddMagma.brecOn.eq : ∀ {α : Type u} {motive : FreeAddMagma α → Sort u_1} (t : FreeAddMagma α)
  (F_1 : (t : FreeAddMagma α) → FreeAddMagma.below t → motive t),
  FreeAddMagma.brecOn t F_1 = F_1 t (FreeAddMagma.brecOn.go t F_1).2
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.add_const_of_norm_tendsto_atTop : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α} {c : β},
  Asymptotics.IsEquivalent l u v →
    Filter.Tendsto (norm ∘ v) l Filter.atTop → Asymptotics.IsEquivalent l (fun x => u x + c) v
-- Mathlib.RingTheory.RingHom.FaithfullyFlat
/-- A ring map `f : R →+* S` is faithfully flat if `S` is faithfully flat as an `R`-algebra.  -/
RingHom.FaithfullyFlat : {R : Type u_3} → {S : Type u_4} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Mathlib.RingTheory.Unramified.LocalRing
Localization.exists_awayMap_bijective_of_residueField_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  [inst_3 : p.IsPrime] {q : Ideal S} [inst_4 : q.IsPrime],
  p.primesOver S = {q} →
    ∀ [Module.Finite R S] [FaithfulSMul R S] [inst_7 : q.LiesOver p] [Algebra.IsUnramifiedAt R q]
      [inst_9 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
      [inst_10 : Localization.AtPrime.IsLiesOverAlgebra p q],
      Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField) →
        ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Bijective ⇑(Localization.awayMap (algebraMap R S) r')
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- A monad equipped with the ability to manipulate 2-morphisms.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂ : (Type → Type) → Type
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_eq_zero_iff : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) {x : 𝕜}, ↑x = 0 ↔ ∃ n, n • p = x
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.map_le_iff_le_functorPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C} {R : CategoryTheory.Presieve X} {S : CategoryTheory.Presieve (F.obj X)},
  CategoryTheory.Presieve.map F R ≤ S ↔ R ≤ CategoryTheory.Presieve.functorPullback F S
-- Mathlib.Algebra.Field.Defs
Rat.cast_mk' : ∀ {K : Type u_1} [inst : DivisionRing K] (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : a.natAbs.Coprime b),
  ↑{ num := a, den := b, den_nz := h1, reduced := h2 } = ↑a / ↑b
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.mk.injEq : ∀ {α : Type} (root : Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex)
  (tries : Array (Lean.Meta.RefinedDiscrTree.Trie α))
  (root_1 : Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex)
  (tries_1 : Array (Lean.Meta.RefinedDiscrTree.Trie α)),
  ({ root := root, tries := tries } = { root := root_1, tries := tries_1 }) = (root = root_1 ∧ tries = tries_1)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.equivProd_inverse_map_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X Y : A × B} (f : X ⟶ Y),
  ((CategoryTheory.Comma.equivProd L R).inverse.map f).left = f.1
-- Mathlib.Order.Cover
covBy_iff_le_iff_lt_right : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α}, y ⋖ x ↔ ∀ {z : α}, x ≤ z ↔ y < z
-- Mathlib.AlgebraicGeometry.Sites.BigZariski
/-- The Zariski topology on the category of schemes.  -/
AlgebraicGeometry.Scheme.zariskiTopology : CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instIsAddApplySet : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  [inst_2 : ContinuousAdd M], IsAddApply (MeasureTheory.VectorMeasure α M) (Set α) M
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
instIsInertiaFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupInertiaOfIsGalois : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) [inst_4 : MulSemiringAction Gal(L/K) B] [IsGalois K L],
  IsInertiaField K L P ↥(FixedPoints.intermediateField ↥(Ideal.inertia Gal(L/K) P))
-- Mathlib.Order.SuccPred.CompleteLinearOrder
exists_eq_iSup_of_not_isSuccPrelimit : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompleteLinearOrder α] {f : ι → α},
  ¬Order.IsSuccPrelimit (⨆ i, f i) → ∃ i, f i = ⨆ i, f i
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.one_eq_top : ∀ {X : AlgebraicGeometry.Scheme}, 1 = ⊤
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.instNeg : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} → Neg (ContIntertwiningMap π₁ π₂)
-- Lean.AuxRecursor
Lean.getNoConfusionInfo : Lean.Environment → Lean.Name → Lean.NoConfusionInfo
-- Mathlib.Data.Fin.Rev
Fin.rev_pred : ∀ {n : ℕ} {i : Fin (n + 1)} (h : i ≠ 0) (h' : optParam (i.rev ≠ Fin.last n) ⋯), (i.pred h).rev = i.rev.castPred h'
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- The `sSup` of a union of two sets is the max of the suprema of each subset, under the
assumptions that all sets are bounded above and nonempty.  -/
csSup_union : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
  BddAbove s → s.Nonempty → BddAbove t → t.Nonempty → sSup (s ∪ t) = sSup s ⊔ sSup t
-- Init.Data.Int.DivMod.Lemmas
Int.eq_ediv_of_mul_eq_left : ∀ {a b c : ℤ}, b ≠ 0 → a * b = c → a = c / b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S}
  (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.equalizer.ι
          (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
            (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
          (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
            (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
        (CategoryTheory.Limits.pullback.snd s v)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.equalizer.ι f g)
        (CategoryTheory.Limits.pullback.fst s v))
      (CategoryTheory.Limits.pullback.snd s v)
-- Mathlib.Order.CompleteLattice.Defs
le_sSup_iff : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α}, a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b
-- Mathlib.Algebra.Order.Ring.Defs
IsStrictOrderedRing.toMulPosStrictMono : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : PartialOrder R} [self : IsStrictOrderedRing R], MulPosStrictMono R
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.rankFinite_iff_cRank_lt_aleph0 : ∀ {α : Type u} {M : Matroid α}, M.RankFinite ↔ M.cRank < Cardinal.aleph0
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsLower.isUpperSet_of_isClosed : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α] {s : Set α},
  IsClosed s → IsUpperSet s
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.pi_toPartialHomeomorph : ∀ {ι : Type u_7} [inst : Finite ι] {X : ι → Type u_8} {Y : ι → Type u_9} [inst_1 : (i : ι) → TopologicalSpace (X i)]
  [inst_2 : (i : ι) → TopologicalSpace (Y i)] (ei : (i : ι) → OpenPartialHomeomorph (X i) (Y i)),
  (OpenPartialHomeomorph.pi ei).toPartialHomeomorph =
    { toPartialEquiv := PartialEquiv.pi fun i => (ei i).toPartialEquiv, continuousOn_toFun := ⋯,
      continuousOn_invFun := ⋯ }
-- Init.Data.BitVec.Lemmas
BitVec.neg_intMin : ∀ {w : ℕ}, -BitVec.intMin w = BitVec.intMin w
-- Init.Data.Array.Basic
/-- Pairs each element of an array with its index, optionally starting from an index other than `0`.

Examples:
* `#[a, b, c].zipIdx = #[(a, 0), (b, 1), (c, 2)]`
* `#[a, b, c].zipIdx 5 = #[(a, 5), (b, 6), (c, 7)]`
 -/
Array.zipIdx : {α : Type u} → Array α → optParam ℕ 0 → Array (α × ℕ)
-- Mathlib.Order.Category.BddDistLat
BddDistLat.coe_comp : ∀ {X Y Z : BddDistLat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquiv_comp_algebraMap : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (Rₘ : Type u_4) (Sₙ : Type u_5) (Rₘ' : Type u_6) (Sₙ' : Type u_7) [inst_3 : CommSemiring Rₘ]
  [inst_4 : CommSemiring Sₙ] [inst_5 : CommSemiring Rₘ'] [inst_6 : CommSemiring Sₙ'] [inst_7 : Algebra R Rₘ]
  [inst_8 : Algebra S Sₙ] [inst_9 : Algebra R Rₘ'] [inst_10 : Algebra S Sₙ'] [inst_11 : Algebra R Sₙ]
  [inst_12 : Algebra Rₘ Sₙ] [inst_13 : Algebra Rₘ' Sₙ'] [inst_14 : Algebra R Sₙ'] (N : Submonoid S)
  [inst_15 : IsLocalization M Rₘ] [inst_16 : IsLocalization N Sₙ] [inst_17 : IsLocalization M Rₘ']
  [inst_18 : IsLocalization N Sₙ'] [IsScalarTower R Rₘ Sₙ] [IsScalarTower R S Sₙ] [IsScalarTower R Rₘ' Sₙ']
  [IsScalarTower R S Sₙ'],
  (↑(IsLocalization.algEquiv N Sₙ Sₙ')).comp (algebraMap Rₘ Sₙ) =
    (algebraMap Rₘ' Sₙ').comp ↑(IsLocalization.algEquiv M Rₘ Rₘ')
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
/-- In a Banach algebra `A` over `𝕜`, for `a : A` the function `fun z ↦ (1 - z • a)⁻¹` is
differentiable on any closed ball centered at zero of radius `r < (spectralRadius 𝕜 a)⁻¹`.  -/
spectrum.differentiableOn_inverse_one_sub_smul : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] {a : A} {r : NNReal},
  ↑r < (spectralRadius 𝕜 a)⁻¹ → DifferentiableOn 𝕜 (fun z => Ring.inverse (1 - z • a)) (Metric.closedBall 0 ↑r)
-- Mathlib.Logic.Embedding.Basic
/-- If `e₁` and `e₂` are embeddings, then so is `Prod.map e₁ e₂ : (a, b) ↦ (e₁ a, e₂ b)`.  -/
Function.Embedding.prodMap : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → {δ : Type u_4} → (α ↪ β) → (γ ↪ δ) → α × γ ↪ β × δ