mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.TwoPointing
TwoPointing.snd_ne_fst : ∀ {α : Type u_1} (p : TwoPointing α), p.toProd.2 ≠ p.toProd.1
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.coe_inclusion : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] [inst_3 : LE S]
  [inst_4 : IsConcreteLE S G] {H K : S} (h : H ≤ K) (a : ↥H), ↑((SubgroupClass.inclusion h) a) = ↑a
-- Mathlib.Analysis.Calculus.Deriv.Shift
/-- Translation in the domain does not change the derivative.  -/
HasDerivAt.comp_const_add : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} (a x : 𝕜),
  HasDerivAt f f' (a + x) → HasDerivAt (fun x => f (a + x)) f' x
-- Init.Data.Array.Lemmas
Array.toList_filterMap' : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} {stop : ℕ},
  stop = xs.size → (Array.filterMap f xs 0 stop).toList = List.filterMap f xs.toList
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_surjective : ∀ {R : Type u} {M : Type v} [Nonempty R], Function.Surjective TrivSqZeroExt.snd
-- Lean.Expr
/-- Returns true when the expression does not have any sub-expressions.  -/
Lean.Expr.isAtomic : Lean.Expr → Bool
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ShowDocumentClientCapabilities.mk.sizeOf_spec : ∀ (support : Bool), sizeOf { support := support } = 1 + sizeOf support
-- Mathlib.Analysis.Fourier.LpSpace
/-- The Fourier transform on `L2` as a linear isometry equivalence.  -/
MeasureTheory.Lp.fourierTransformₗᵢ : (E : Type u_1) →
  (F : Type u_2) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : MeasurableSpace E] →
        [inst_2 : BorelSpace E] →
          [inst_3 : NormedAddCommGroup F] →
            [inst_4 : InnerProductSpace ℂ F] →
              [CompleteSpace F] →
                [inst_6 : InnerProductSpace ℝ E] →
                  [inst_7 : FiniteDimensional ℝ E] →
                    ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)
-- Mathlib.Order.Bounds.Basic
IsCofinalFor.trans : ∀ {α : Type u_1} [inst : Preorder α] {s t u : Set α}, IsCofinalFor s t → IsCofinalFor t u → IsCofinalFor s u
-- Mathlib.Topology.Constructible
_private.Mathlib.Topology.Constructible.0.supClosed_isRetrocompact : ∀ {X : Type u_2} [inst : TopologicalSpace X], SupClosed {s | IsRetrocompact s}
-- Mathlib.Tactic.Simproc.Factors
/-- A simproc for terms of the form `Nat.primeFactorsList (OfNat.ofNat n)`.  -/
Nat.primeFactorsList_ofNat : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.of_boundedSpace : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s t : Set α} [BoundedSpace M], Absorbs M s t
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_subset_Iic_union_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iio b ⊆ Set.Iic a ∪ Set.Ico a b
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- The *Euler Product* for multiplicative (on coprime arguments) functions.

If `f : ℕ → R`, where `R` is a complete normed commutative ring, `f 0 = 0`, `f 1 = 1`, `f` is
multiplicative on coprime arguments, and `‖f ·‖` is summable, then
`∏' p : ℕ, if p.Prime then ∑' e, f (p ^ e) else 1 = ∑' n, f n`.
This version is stated using `HasProd` and `Set.mulIndicator`.  -/
EulerProduct.eulerProduct_hasProd_mulIndicator : ∀ {R : Type u_1} [inst : NormedCommRing R] {f : ℕ → R} [CompleteSpace R],
  f 1 = 1 →
    (∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) →
      (Summable fun x => ‖f x‖) →
        f 0 = 0 → HasProd ({p | Nat.Prime p}.mulIndicator fun p => ∑' (e : ℕ), f (p ^ e)) (∑' (n : ℕ), f n)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Entry.entry.injEq : ∀ {α : Type u} {β : Type v} {σ : Type w} (key : α) (val : β) (key_1 : α) (val_1 : β),
  (Lean.PersistentHashMap.Entry.entry key val = Lean.PersistentHashMap.Entry.entry key_1 val_1) =
    (key = key_1 ∧ val = val_1)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `f ◁ η` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.evalWhiskerLeft : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
        [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
          Mathlib.Tactic.BicategoryLike.Mor₁ →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_cocyclesIso₀_hom_f : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap f φ 0)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesIso₀ B).hom (groupCohomology.shortComplexH0 B).f) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesIso₀ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH0 A).f (Rep.Hom.toModuleCatHom φ))
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
BoundedVariationOn.vectorMeasure_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E}
  {a b : α} (hf : BoundedVariationOn f Set.univ),
  a < b → hf.vectorMeasure (Set.Ioo a b) = Function.leftLim f b - Function.rightLim f a
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  k ∉ t₁ → (t₁ \ t₂).getD k fallback = fallback
-- Mathlib.CategoryTheory.Comma.Arrow
/-- A helper construction: given a square between `i` and `f ≫ g`, produce a square between
`i` and `g`, whose top leg uses `f`:
```
A  → X
     ↓f
↓i   Y             --> A → Y
     ↓g                ↓i  ↓g
B  → Z                 B → Z
```
 -/
CategoryTheory.Arrow.squareToSnd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {i : CategoryTheory.Arrow C} →
        {f : X ⟶ Y} →
          {g : Y ⟶ Z} →
            (i ⟶ CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp f g)) → (i ⟶ CategoryTheory.Arrow.mk g)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplit.mk.sizeOf_spec : ∀ (pred : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred) (k : ℕ) (h : Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof),
  sizeOf { pred := pred, k := k, h := h } = 1 + sizeOf pred + sizeOf k + sizeOf h
-- Mathlib.Data.Finset.Disjoint
Finset.disjUnion_val : ∀ {α : Type u_2} (s t : Finset α) (h : Disjoint s t), (s.disjUnion t h).val = s.val + t.val
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_diff_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.isEmpty = true → (m₁ \ m₂).isEmpty = true
-- Init.Data.List.Sublist
List.IsPrefix.mem : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, a ∈ l₁ → l₁ <+: l₂ → a ∈ l₂
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.hexagon_reverse_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).hom
      (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv
        (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).inv Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).inv))
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_one : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α], normalize 1 = 1
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} →
            (app : (a : B) → η.app a ⟶ θ.app a) →
              autoParam
                  (∀ {a b : B} (f : a ⟶ b),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))
                        (θ.naturality f) =
                      CategoryTheory.CategoryStruct.comp (η.naturality f)
                        (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
                  CategoryTheory.Oplax.OplaxTrans.Modification.naturality._autoParam →
                CategoryTheory.Oplax.OplaxTrans.Modification η θ
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℕ → Bool
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddSemigroup : {α : Type u_1} → [AddSemigroup α] → AddSemigroup (Colex α)
-- Mathlib.Topology.Constructions
instTopologicalSpaceMultiplicative : {X : Type u} → [TopologicalSpace X] → TopologicalSpace (Multiplicative X)
-- Std.Time.DateTime.Timestamp
/-- Creates a `Timestamp` from a `Nanosecond.Offset`.
 -/
Std.Time.Timestamp.ofNanosecondsSinceUnixEpoch : Std.Time.Nanosecond.Offset → Std.Time.Timestamp
-- Mathlib.Geometry.Manifold.VectorField.Pullback
ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq : ∀ {𝕜 : 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] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} {y₀ : M'} [CompleteSpace E]
  [inst_12 : IsManifold I 1 M] [inst_13 : IsManifold I' 1 M'],
  ContMDiffWithinAt I' I'.tangent m (fun x => ⟨x, V x⟩) t y₀ →
    ContMDiffWithinAt I I' n f s x₀ →
      (mfderiv[s] f x₀).IsInvertible →
        x₀ ∈ s →
          UniqueMDiff[s] →
            m + 1 ≤ n →
              f x₀ = y₀ →
                ContMDiffWithinAt I I.tangent m (fun x => ⟨x, VectorField.mpullbackWithin I I' f V s x⟩) (s ∩ f ⁻¹' t)
                  x₀
-- Init.Data.UInt.Lemmas
UInt8.toNat_ofNat_of_lt' : ∀ {n : ℕ}, n < UInt8.size → (UInt8.ofNat n).toNat = n
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.liftCochain_descCochain : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K L : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) {n' m' : ℤ}
  (α' : CochainComplex.HomComplex.Cochain F L m') (β' : CochainComplex.HomComplex.Cochain G L n') (h : n + 1 = m)
  (h' : m' + 1 = n') (p : ℤ) (hp : n + n' = p),
  (CochainComplex.mappingCone.liftCochain φ α β h).comp (CochainComplex.mappingCone.descCochain φ α' β' h') hp =
    α.comp α' ⋯ + β.comp β' ⋯
-- Mathlib.Data.Nat.Cast.Order.Field
Nat.one_sub_one_div_cast_le_one : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [AddLeftMono α] (n : ℕ),
  1 - 1 / ↑n ≤ 1
-- Init.Data.SInt.Lemmas
Int32.neg_mul : ∀ (a b : Int32), -a * b = -(a * b)
-- Std.Async.UDP
/-- Enables or disables broadcasting for the UDP socket.
 -/
Std.Async.UDP.Socket.setBroadcast : Std.Async.UDP.Socket → Bool → IO Unit
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
CategoryTheory.LocalizerMorphism.Derives.isRightDerivedFunctor_iff_isIso : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H] {D₂ : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  {F : CategoryTheory.Functor C₂ H},
  Φ.Derives F →
    ∀ [Φ.IsRightDerivabilityStructure] {L₂ : CategoryTheory.Functor C₂ D₂} [inst_5 : L₂.IsLocalization W₂]
      {RF : CategoryTheory.Functor D₂ H} (α : F ⟶ L₂.comp RF),
      RF.IsRightDerivedFunctor α W₂ ↔ ∀ (X₁ : C₁), CategoryTheory.IsIso (α.app (Φ.functor.obj X₁))
-- Mathlib.Order.Sublattice
Sublattice.coe_sup : ∀ {α : Type u_2} [inst : Lattice α] {L : Sublattice α} (a b : ↥L), ↑(a ⊔ b) = ↑a ⊔ ↑b
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instIsDedekindDomain : ∀ (K : Type u_1) [inst : Field K] [NumberField K], IsDedekindDomain (NumberField.RingOfIntegers K)
-- Std.Time.Format.Modifier
Std.Time.OffsetX.noConfusionType : Sort v✝ → Std.Time.OffsetX → Std.Time.OffsetX → Sort v✝
-- Mathlib.Data.List.Basic
List.instLawfulSingleton_mathlib : ∀ {α : Type u} [inst : DecidableEq α], LawfulSingleton α (List α)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- The notion of variable assignments for `BVExpr`.
 -/
Std.Tactic.BVDecide.BVExpr.Assignment : Type
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_Ioo : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α], b < a → sInf (Set.Ioo b a) = b
-- Mathlib.RingTheory.Ideal.GoingDown
/-- Flat algebras satisfy the going down property.  -/
Algebra.HasGoingDown.of_flat : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S],
  Algebra.HasGoingDown R S
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.coe_subset_Icc : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι}, ↑I ⊆ BoxIntegral.Box.Icc I
-- Mathlib.Algebra.Star.StarRingHom
/-- The composition of non-unital ⋆-ring homomorphisms, as a non-unital ⋆-ring homomorphism.  -/
NonUnitalStarRingHom.comp : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : NonUnitalNonAssocSemiring A] →
        [inst_1 : Star A] →
          [inst_2 : NonUnitalNonAssocSemiring B] →
            [inst_3 : Star B] →
              [inst_4 : NonUnitalNonAssocSemiring C] → [inst_5 : Star C] → (B →⋆ₙ+* C) → (A →⋆ₙ+* B) → A →⋆ₙ+* C
-- Mathlib.LinearAlgebra.Projection
Submodule.coe_prodEquivOfIsCompl' : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E)
  (h : IsCompl p q) (x : ↥p × ↥q), (p.prodEquivOfIsCompl q h) x = ↑x.1 + ↑x.2
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Naturality of the oplax functoriality constraint, on the left.  -/
CategoryTheory.OplaxFunctor.mapComp_naturality_left_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (X : ↑(self.obj a)) {Z : ↑(self.obj c)}
  (h : (self.map g).toFunctor.obj ((self.map f').toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.mapComp f' g).toNatTrans.app X) h) =
    CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map g).toFunctor.map ((self.map₂ η).toNatTrans.app X)) h)
-- Mathlib.Order.Comparable
IncompRel.not_ge : ∀ {α : Type u_1} {a b : α} [inst : LE α], IncompRel (fun x1 x2 => x1 ≤ x2) a b → ¬b ≤ a
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (w : F ≅ G),
  (P.conePointsIsoOfNatIso Q w).hom = CategoryTheory.Limits.IsLimit.map s Q w.hom
-- Lean.HeadIndex
Lean.HeadIndex.proj : Lean.Name → ℕ → Lean.HeadIndex
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.instInhabited : {n : ℕ} → Inhabited (Composition n)
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instInhabited : {α : Type u_1} → [inst : Preorder α] → [Inhabited α] → Inhabited (NonemptyInterval α)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.toSubfield_map : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (S : IntermediateField K L) (f : L →ₐ[K] L'),
  (IntermediateField.map f S).toSubfield = Subfield.map (↑f) S.toSubfield
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
/-- Equational lemma for `Pseudofunctor.isoMapOfCommSq` when
both horizontal maps of the square are the same and vertical maps are identities.  -/
CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {X₁ X₂ : B} (f : X₁ ⟶ X₂),
  F.isoMapOfCommSq ⋯ =
    CategoryTheory.Bicategory.whiskerLeftIso (F.map f) (F.mapId X₂) ≪≫
      CategoryTheory.Bicategory.rightUnitor (F.map f) ≪≫
        (CategoryTheory.Bicategory.leftUnitor (F.map f)).symm ≪≫
          (CategoryTheory.Bicategory.whiskerRightIso (F.mapId X₁) (F.map f)).symm
-- Mathlib.Topology.DiscreteQuotient
/-- If `X` is a compact space, then any discrete quotient of `X` is finite.  -/
DiscreteQuotient.instFiniteQuotientOfCompactSpace : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X) [CompactSpace X], Finite (Quotient S.toSetoid)
-- Mathlib.Algebra.Group.Action.Units
/-- Transfer `SMulCommClass G H M` to `SMulCommClass G H Mˣ`.  -/
Units.smulCommClass' : ∀ {G : Type u_1} {H : Type u_2} {M : Type u_3} [inst : Group G] [inst_1 : Group H] [inst_2 : Monoid M]
  [inst_3 : MulAction G M] [inst_4 : SMulCommClass G M M] [inst_5 : MulAction H M] [inst_6 : SMulCommClass H M M]
  [inst_7 : IsScalarTower G M M] [inst_8 : IsScalarTower H M M] [SMulCommClass G H M], SMulCommClass G H Mˣ
-- Mathlib.Order.Interval.Finset.Nat
Nat.Iio_eq_range : ∀ (a : ℕ), Finset.Iio a = Finset.range a
-- Mathlib.Tactic.WLOG
/-- The array of `FVarId`s that was reverted to produce the reduction hypothesis `H` in
`reductionGoal`, which are still present in the context of `reductionGoal` (but not necessarily
`hypothesisGoal`).  -/
Mathlib.Tactic.WLOGResult.revertedFVarIds : Mathlib.Tactic.WLOGResult → Array Lean.FVarId
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- `biproduct_comparison' F f` is a split monomorphism.  -/
CategoryTheory.Functor.splitMonoBiproductComparison' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {J : Type w₁} →
              (F : CategoryTheory.Functor C D) →
                (f : J → C) →
                  [inst_4 : CategoryTheory.Limits.HasBiproduct f] →
                    [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] →
                      [F.PreservesZeroMorphisms] → CategoryTheory.SplitMono (F.biproductComparison' f)
-- Init.Data.String.Subslice
/-- Constructs a subslice of `s` starting at the given position and going until the end of the
slice.
 -/
String.Slice.subsliceFrom : (s : String.Slice) → s.Pos → s.Subslice
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isEmpty_inter_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t₁.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Init.Internal.Order.MonadTail
Lean.Order.instMonadTailExcept : {ε : Type u_1} → Lean.Order.MonadTail (Except ε)
-- Mathlib.Order.WithBot
WithTop.decidableLE.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (a : WithTop α), a.decidableLE none = isTrue ⋯
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.instDecidableEqΓ' : DecidableEq Turing.PartrecToTM2.Γ'
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_apply : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (f : MvPowerSeries σ R) (d : σ →₀ ℕ),
  (MvPowerSeries.coeff d) f = f d
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.PreZeroHypercoverFamily.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (property : ⦃X : C⦄ → CategoryTheory.ObjectProperty (CategoryTheory.PreZeroHypercover X))
  (iff_shrink : ∀ {X : C} {E : CategoryTheory.PreZeroHypercover X}, property E ↔ property E.shrink)
  (property_1 : ⦃X : C⦄ → CategoryTheory.ObjectProperty (CategoryTheory.PreZeroHypercover X))
  (iff_shrink_1 : ∀ {X : C} {E : CategoryTheory.PreZeroHypercover X}, property_1 E ↔ property_1 E.shrink),
  ({ property := property, iff_shrink := iff_shrink } = { property := property_1, iff_shrink := iff_shrink_1 }) =
    (property = property_1)
-- Mathlib.Data.Finset.PImage
Finset.pimage.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α →. β) [inst_1 : (x : α) → Decidable (f x).Dom]
  (s : Finset α), Finset.pimage f s = s.biUnion fun x => (f x).toFinset
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.top_prod_top : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M], ⊤.prod ⊤ = ⊤
-- Mathlib.GroupTheory.Congruence.Opposite
Con.unop.eq_1 : ∀ {M : Type u_1} [inst : Mul M] (c : Con Mᵐᵒᵖ),
  c.unop = { r := fun a b => c (MulOpposite.op b) (MulOpposite.op a), iseqv := ⋯, mul' := ⋯ }
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.zero_add : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddMonoid X] [inst_3 : DistribMulAction R X] (x : OreLocalization S X), 0 + x = x
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.instIsClosedImmersionMapDescScheme : ∀ {X Y S T : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) (i : S ⟶ T) [AlgebraicGeometry.IsSeparated i],
  AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.mapDesc f g i)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.op_refl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.Iso.refl X).op = CategoryTheory.Iso.refl (Opposite.op X)
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.mul_inv_cancel_right'` for a stronger version.  -/
ENNReal.mul_inv_cancel_right : ∀ {a b : ENNReal}, b ≠ 0 → b ≠ ⊤ → a * b * b⁻¹ = a
-- Mathlib.Algebra.Group.Defs
one_div : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a : G), 1 / a = a⁻¹
-- Lean.Environment
Lean.MonadEnv.modifyEnv : {m : Type → Type} → [self : Lean.MonadEnv m] → (Lean.Environment → Lean.Environment) → m Unit
-- Init.Data.List.Lemmas
List.getLast_eq_iff_getLast?_eq_some : ∀ {α : Type u_1} {a : α} {xs : List α} (h : xs ≠ []), xs.getLast h = a ↔ xs.getLast? = some a
-- Mathlib.Topology.Constructions.SumProd
Topology.isInducing_prod_const : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {y : Y} {f : X → Z}, (Topology.IsInducing fun x => (f x, y)) ↔ Topology.IsInducing f