mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Finset.sum_intervalGapsWithin_add_sum_eq_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : AddCommGroup β] (F : Finset (α × α)) {k : ℕ}
  (h : F.card = k) {a b : α} (g : α → β),
  ∑ i ∈ Finset.range (k + 1), (g (F.intervalGapsWithin h a b ↑i).2 - g (F.intervalGapsWithin h a b ↑i).1) +
      ∑ z ∈ F, (g z.2 - g z.1) =
    g b - g a
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.sub_left : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G} (c : G), a ≡ b [PMOD p] → c - a ≡ c - b [PMOD p]
-- Mathlib.Analysis.Normed.Group.Constructions
pi_norm_const' : ∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : SeminormedGroup E] [Nonempty ι] (a : E),
  ‖fun _i => a‖ = ‖a‖
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.toSubalgebra_inj : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {S U : StarSubalgebra R A},
  S.toSubalgebra = U.toSubalgebra ↔ S = U
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.mk : {ι : Type u₁} →
  {k : Type u₂} →
    {V : Type u₃} →
      {P : Type u₄} →
        [inst : AddCommGroup V] →
          [inst_1 : AddTorsor V P] →
            [inst_2 : Ring k] →
              [inst_3 : Module k V] →
                (toFun : ι → P) → AffineIndependent k toFun → affineSpan k (Set.range toFun) = ⊤ → AffineBasis ι k P
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.closure_eq_image_prod : ∀ {M : Type u_1} [inst : Monoid M] (s : Set M), ↑(Submonoid.closure s) = List.prod '' {l | ∀ x ∈ l, x ∈ s}
-- Mathlib.GroupTheory.Index
AddSubgroup.finite_quotient_of_finite_quotient_of_index_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {X : Type u_3} [inst_1 : AddAction G X]
  [Finite (AddAction.orbitRel.Quotient G X)], H.index ≠ 0 → Finite (AddAction.orbitRel.Quotient (↥H) X)
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isValidRevSearchFrom_iff_isValidRevSearchFrom_beq : ∀ {c : Char} {s : String.Slice} {p : s.Pos} {l : List (String.Slice.Pattern.SearchStep s)},
  String.Slice.Pattern.Model.IsValidRevSearchFrom c p l ↔
    String.Slice.Pattern.Model.IsValidRevSearchFrom (fun x => x == c) p l
-- Mathlib.GroupTheory.PresentedGroup
instGroupPresentedGroup : {α : Type u_1} → (rels : Set (FreeGroup α)) → Group (PresentedGroup rels)
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Turn a morphism in `ModuleCat` back into a `LinearMap`.  -/
ModuleCat.Hom.hom : {R : Type u} → [inst : Ring R] → {A B : ModuleCat R} → A.Hom B → ↑A →ₗ[R] ↑B
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.isSyntheticTacticCompletion.isEmpty : Lean.Syntax → Bool
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.instanceTypes : Lean.Option Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_map : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.Limits.biproduct.map p) =
    CategoryTheory.CategoryStruct.comp (p j) (CategoryTheory.Limits.biproduct.ι g j)
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
eq_compactlyGenerated : ∀ {X : Type w} [t : TopologicalSpace X] [UCompactlyGeneratedSpace X], t = TopologicalSpace.compactlyGenerated X
-- Init.Data.Iterators.Lemmas.Combinators.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Append.0.Std.Iter.step_append.match_1.eq_2 : ∀ {α₁ β : Type u_1} [inst : Std.Iterator α₁ Id β] {it₁ : Std.Iter β} (motive : it₁.Step → Sort u_2) (it₁' : Std.Iter β)
  (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁'))
  (h_1 :
    (it₁' : Std.Iter β) →
      (out : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩)
  (h_2 : (it₁' : Std.Iter β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it₁', h⟩ with
    | ⟨Std.IterStep.yield it₁' out, h⟩ => h_1 it₁' out h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it₁' h
-- Mathlib.Topology.Compactification.StoneCech
Ultrafilter.tendsto_pure_self : ∀ {α : Type u} (b : Ultrafilter α), Filter.Tendsto pure (↑b) (nhds b)
-- Mathlib.Order.Interval.Set.OrdConnected
OrderEmbedding.image_Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β),
  (Set.range ⇑e).OrdConnected → ∀ (x y : α), ⇑e '' Set.Icc x y = Set.Icc (e x) (e y)
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
/-- The distribution of finite-dimensional marginals of the real Brownian motion at time `s`
is the centered Gaussian with variance `s`.  -/
ProbabilityTheory.BrownianReal.measurePreserving_eval_projectiveFamily : ∀ {I : Finset NNReal} (s : ↥I),
  MeasureTheory.MeasurePreserving (fun x => x s) (ProbabilityTheory.BrownianReal.projectiveFamily I)
    (ProbabilityTheory.gaussianReal 0 ↑s)
-- Mathlib.Data.Real.Basic
Real.instLE : LE ℝ
-- Mathlib.Data.LawfulXor.Basic
LawfulXor.xor_self : ∀ {α : Type u_1} {inst : XorOp α} {inst_1 : Zero α} [self : LawfulXor α] (a : α), a ^^^ a = 0
-- Lean.Elab.Coinductive
/-- This structure contains the data carried in `InductiveElabStep1` that are solely used in
mutual coinductive predicate elaboration.  -/
Lean.Elab.Command.CoinductiveElabData : Type
-- Batteries.Data.HashMap.Basic
/-- Returns true if the element `a` is in the map.
```
def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.contains "one" = true
hashMap.contains "three" = false
```
 -/
Batteries.HashMap.contains : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α β → α → Bool
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.updateSplitArgPosMap : Lean.Meta.Grind.SplitInfo → Lean.Meta.Grind.GoalM Unit
-- Std.Data.ExtDTreeMap.Basic
/-- Erases multiple mappings from the tree map by iterating over the given collection and calling
`erase`.
 -/
Std.ExtDTreeMap.eraseMany : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → {ρ : Type u_1} → [ForIn Id ρ α] → Std.ExtDTreeMap α β cmp → ρ → Std.ExtDTreeMap α β cmp
-- Mathlib.MeasureTheory.Measure.FiniteMeasurePi
MeasureTheory.FiniteMeasure.pi_map_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.FiniteMeasure (α i)) {β : ι → Type u_3} [inst_2 : (i : ι) → MeasurableSpace (β i)]
  {f : (i : ι) → α i → β i},
  (∀ (i : ι), AEMeasurable (f i) ↑(μ i)) →
    ((MeasureTheory.FiniteMeasure.pi μ).map fun x i => f i (x i)) =
      MeasureTheory.FiniteMeasure.pi fun i => (μ i).map (f i)
-- Lean.Environment
Lean.ConstantKind.quot : Lean.ConstantKind
-- Mathlib.Algebra.Ring.BooleanRing
/-- The "identity" equivalence between `α` and `AsBoolAlg α`.  -/
ofBoolAlg : {α : Type u_1} → AsBoolAlg α ≃ α
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsZGroup.exponent_eq_card : ∀ (G : Type u_1) [inst : Group G] [Finite G] [IsZGroup G], Monoid.exponent G = Nat.card G
-- Mathlib.Analysis.Complex.Isometry
linear_isometry_complex_aux : ∀ {f : ℂ ≃ₗᵢ[ℝ] ℂ}, f 1 = 1 → f = LinearIsometryEquiv.refl ℝ ℂ ∨ f = Complex.conjLIE
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.normal_of_isAddCommutative : ∀ {G : Type u_1} [inst : AddGroup G] [IsAddCommutative G] (H : AddSubgroup G), H.Normal
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_set_const : ∀ {α : Type u_4} (s : Set α) (c : ENNReal), ∑' (x : ↑s), c = ↑s.encard * c
-- Init.Prelude
/-- The Boolean values, `true` and `false`.

Logically speaking, this is equivalent to `Prop` (the type of propositions). The distinction is
public important for programming: both propositions and their proofs are erased in the code generator,
while `Bool` corresponds to the Boolean type in most programming languages and carries precisely one
bit of run-time information.
 -/
Bool : Type
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isOpen_subsets_of_isOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α] {U : Set α}, IsOpen U → IsOpen {K | ↑K ⊆ U}
-- Init.Tactics
/-- Implementation of `ac_nf` (the full `ac_nf` calls `trivial` afterwards).  -/
Lean.Parser.Tactic.acNf0 : Lean.ParserDescr
-- Lean.Expr
Lean.instSingletonFVarIdFVarIdSet : Singleton Lean.FVarId Lean.FVarIdSet
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
ContinuousLinearMapWOT.continuousAt_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} [inst_7 : TopologicalSpace α] {f : α → E →WOT[𝕜] F} {a : α},
  ContinuousAt f a ↔ ∀ (x : E) (y : F), ContinuousAt (fun x_1 => inner 𝕜 y ((f x_1) x)) a
-- Mathlib.Order.JordanHolder
CompositionSeries.inj : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X) {i j : Fin s.length.succ},
  s.toFun i = s.toFun j ↔ i = j
-- Init.Data.Array.Lex.Lemmas
Array.instTransLt : {α : Type u_1} →
  [inst : LT α] →
    [Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2] →
      Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.instReprOffset.repr : Std.Time.TimeZone.Offset → ℕ → Std.Format
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsStrictMinor.trans_isMinor : ∀ {α : Type u_1} {M M' N : Matroid α}, N <m M → M ≤m M' → N <m M'
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : DecidableEq I] [inst_4 : CategoryTheory.Limits.HasInitial C]
  [∀ (X₂ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)]
  (X : CategoryTheory.GradedObject I C),
  (((CategoryTheory.GradedObject.mapBifunctor (CategoryTheory.MonoidalCategory.curriedTensor C) I I).obj
            ((CategoryTheory.GradedObject.single₀ I).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).obj
        X).HasMap
    fun x =>
    match x with
    | (i₁, i₂) => i₁ + i₂
-- Mathlib.MeasureTheory.Measure.Comap
MeasurableEquiv.map_symm : ∀ {α : Type u_1} {β : Type u_2} {ma : MeasurableSpace α} {mb : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  (e : β ≃ᵐ α), MeasureTheory.Measure.map (⇑e.symm) μ = MeasureTheory.Measure.comap (⇑e) μ
-- Mathlib.Logic.Hydra
Relation.cutExpand_add_single : ∀ {α : Type u_1} {r : α → α → Prop} {a' a : α} (s : Multiset α), r a' a → Relation.CutExpand r (s + {a'}) (s + {a})
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.apply_eq_zero_of_lt_order : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] {n : ℕ} [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F}, n < p.order → p n = 0
-- Init.Data.Nat.Lcm
Nat.lcm_mul_left : ∀ (m n k : ℕ), (m * n).lcm (m * k) = m * n.lcm k
-- Lean.Expr
Lean.Expr.hasExprMVarEx : Lean.Expr → Bool
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.whiskerLeft_apply : ∀ (X : TopCat) {Y Z : TopCat} (f : Y ⟶ Z) (p : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)) p =
    (p.1, (CategoryTheory.ConcreteCategory.hom f) p.2)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- the condition that there exists a homology data  -/
CategoryTheory.ShortComplex.HasHomology.condition : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {S : CategoryTheory.ShortComplex C} [self : S.HasHomology], Nonempty S.HomologyData
-- Mathlib.Topology.UnitInterval
projIcc_eq_zero : ∀ {x : ℝ}, Set.projIcc 0 1 ⋯ x = 0 ↔ x ≤ 0
-- Mathlib.Data.List.MinMax
List.coe_minimum_of_length_pos : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} (h : 0 < l.length), ↑(List.minimum_of_length_pos h) = l.minimum
-- Init.Data.SInt.Bitwise
Int16.not_eq_comm : ∀ {a b : Int16}, ~~~a = b ↔ a = ~~~b
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.eval_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g h : C} {η η' : f ⟶ g} {θ θ' : g ⟶ h} {ι : f ⟶ h},
  η = η' → θ = θ' → CategoryTheory.CategoryStruct.comp η' θ' = ι → CategoryTheory.CategoryStruct.comp η θ = ι
-- Init.Data.Nat.Gcd
Nat.dvd_gcd_mul_gcd_iff_dvd_mul : ∀ {k n m : ℕ}, k ∣ k.gcd n * k.gcd m ↔ k ∣ n * m
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.l_injective : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : Preorder α] [inst_1 : PartialOrder β]
  (gi : GaloisCoinsertion l u), Function.Injective l
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.iUnion_cylinder_update : ∀ {E : ℕ → Type u_1} (x : (n : ℕ) → E n) (n : ℕ),
  ⋃ k, PiNat.cylinder (Function.update x n k) (n + 1) = PiNat.cylinder x n
-- Mathlib.Algebra.Star.Unitary
Unitary.inv_mem_iff : ∀ {G : Type u_2} [inst : Group G] [inst_1 : StarMul G] {g : G}, g⁻¹ ∈ unitary G ↔ g ∈ unitary G
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ ∪ t₂).isEmpty = (t₁.isEmpty && t₂.isEmpty)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk : ∀ {G₀ : Type u_1} {R : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : CommRing R] (φ : Polynomial R →*₀ G₀)
  (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀)) (n : Polynomial R)
  (d : ↥(nonZeroDivisors (Polynomial R))),
  (RatFunc.liftMonoidWithZeroHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.arrowArrowEquivalence_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Square.arrowArrowEquivalence.functor = CategoryTheory.Square.toArrowArrowFunctor
-- Lean.Elab.Term.TermElabM
/-- Enable auto-bound implicits, and execute `k` while catching auto bound implicit exceptions. When an exception is caught,
a new local declaration is created, registered, and `k` is tried to be executed again.  -/
Lean.Elab.Term.withAutoBoundImplicit : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filter_not_contains_map_fst_of_containsKey_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getValueCastD k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback =
        fallback
-- Init.Data.Rat.Lemmas
Rat.inv_pos : ∀ {a : ℚ}, 0 < a⁻¹ ↔ 0 < a
-- Mathlib.Order.Interval.Finset.Defs
Finset.Iic_prod_def : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : LocallyFiniteOrderBot β] [inst_4 : DecidableLE (α × β)] (x : α × β),
  Finset.Iic x = Finset.Iic x.1 ×ˢ Finset.Iic x.2
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isOpenEmbedding_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X], Topology.IsOpenEmbedding OnePoint.some
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
/-- An absolute value `R → ℤ` is admissible if it respects the Euclidean domain
structure and a large enough set of elements in `R^n` will contain a pair of
elements whose remainders are pointwise close together.  -/
AbsoluteValue.IsAdmissible : {R : Type u_1} → [inst : EuclideanDomain R] → AbsoluteValue R ℤ → Type
-- Mathlib.FieldTheory.SeparableDegree
/-- `F⟮x⟯ / F` is a separable extension if and only if `x` is a separable element.
As a consequence, any rational function of `x` is also a separable element.  -/
IntermediateField.isSeparable_adjoin_simple_iff_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  Algebra.IsSeparable F ↥F⟮x⟯ ↔ IsSeparable F x
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- A strict pseudofunctor carries an adjunction `f ⊣ g` to an adjunction
`F.map f ⊣ F.map g`.  -/
CategoryTheory.StrictPseudofunctor.mapAdjunction : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {a b : B} →
          {f : a ⟶ b} →
            {g : b ⟶ a} →
              (F : CategoryTheory.StrictPseudofunctor B C) →
                CategoryTheory.Bicategory.Adjunction f g → CategoryTheory.Bicategory.Adjunction (F.map f) (F.map g)
-- Mathlib.Order.CompleteLattice.Basic
sInf_image : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {s : Set β} {f : β → α}, sInf (f '' s) = ⨅ a ∈ s, f a
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.largeCategory : CategoryTheory.LargeCategory TwoP
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_diff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β},
      Std.DTreeMap.Internal.Impl.Const.getD (m₁.diff m₂ ⋯) k fallback =
        if Std.DTreeMap.Internal.Impl.contains k m₂ = true then fallback
        else Std.DTreeMap.Internal.Impl.Const.getD m₁ k fallback
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.IterM.step_drop.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (n = 0 → motive 0) → ((k : ℕ) → n = k.succ → motive k.succ) → motive n
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.id.eq_1 : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : AddZeroClass α],
  OrderAddMonoidHom.id α = { toAddMonoidHom := AddMonoidHom.id α, monotone' := ⋯ }
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
InnerProductGeometry.angle_smul_smul : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {c : ℝ},
  c ≠ 0 → ∀ (x y : V), InnerProductGeometry.angle (c • x) (c • y) = InnerProductGeometry.angle x y
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.inl_apply : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (x : M₁), (ContinuousLinearMap.inl R M₁ M₂) x = (x, 0)
-- Mathlib.Data.DFinsupp.Order
/-- This is called `tsub` for truncated subtraction, to distinguish it with subtraction in an
additive group.  -/
DFinsupp.tsub : {ι : Type u_1} →
  (α : ι → Type u_2) →
    [inst : (i : ι) → AddCommMonoid (α i)] →
      [inst_1 : (i : ι) → PartialOrder (α i)] →
        [∀ (i : ι), CanonicallyOrderedAdd (α i)] →
          [inst_3 : (i : ι) → Sub (α i)] → [∀ (i : ι), OrderedSub (α i)] → Sub (Π₀ (i : ι), α i)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- The first projection of `prod F G`, onto `F`.  -/
CategoryTheory.FunctorToTypes.prod.fst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C (Type w)} → CategoryTheory.FunctorToTypes.prod F G ⟶ F
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ), (∀ (m : ℕ), p (m + n) = 0) → p.radius = ⊤
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.resultant.eq_def : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m n : ℕ), f.resultant g m n = (f.sylvester g m n).det
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.instValuedSpaceWithValRatFuncWithZeroMultiplicativeIntPolynomialValuationXRatfuncAdicComplPkg : {K : Type u_2} → [inst : Field K] → Valued LaurentSeries.ratfuncAdicComplPkg.space (WithZero (Multiplicative ℤ))
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.symm_apply_of_notMem : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : ∀ (x : B), Nonempty (E x)] (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) {b : B},
  b ∉ e.baseSet → ∀ (y : F), e.symm b y = Classical.arbitrary (E b)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
Polynomial.valuation_of_mk : ∀ (K : Type u_1) [inst : Field K] (f : Polynomial K) {g : Polynomial K},
  g ≠ 0 →
    (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (Polynomial.idealX K)) (RatFunc.mk f g) =
      (Polynomial.idealX K).intValuation f / (Polynomial.idealX K).intValuation g
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualLift_of_mem : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {W : Subspace K V}
  {φ : Module.Dual K ↥W} {w : V} (hw : w ∈ W), (W.dualLift φ) w = φ ⟨w, hw⟩
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.unop2_id_bop : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b},
  (CategoryTheory.CategoryStruct.id f.op).unop2 = CategoryTheory.CategoryStruct.id f
-- Mathlib.Topology.UniformSpace.CompareReals
/-- Cauchy reals packaged as a completion of ℚ using the absolute value route.  -/
rationalCauSeqPkg : AbstractCompletion.{0, 0} ℚ
-- Mathlib.Topology.Category.FinTopCat
FinTopCat.instInhabited : Inhabited FinTopCat
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_inverse_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  {X Y : CategoryTheory.Comma S' (CategoryTheory.Functor.fromPUnit T)} (f : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).inverse.map f).left = f.left
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supportedEquivFinsupp_apply_apply : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set α) (a : ↥(Finsupp.supported M R s)) (a_1 : { x // x ∈ s }),
  ((Finsupp.supportedEquivFinsupp s) a) a_1 = ↑a ↑a_1
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The scalar multiplication on the Ore localization of monoids.  -/
OreLocalization.smul : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} → [inst_2 : MulAction R X] → OreLocalization S R → OreLocalization S X → OreLocalization S X
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biInter_insert_update : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] {x : α} {t : Finset α} (f : α → Set β) {s : Set β},
  x ∉ t → ⋂ i ∈ insert x t, Function.update f x s i = s ∩ ⋂ i ∈ t, f i