mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.ιTotal_totalFlipIso_f_hom : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₂.π c₁ c (i₂, i₁) = j),
  CategoryTheory.CategoryStruct.comp (K.flip.ιTotal c i₂ i₁ j h) ((K.totalFlipIso c).hom.f j) =
    c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instAddActionOfUniformContinuousConstVAdd : (M : Type v) →
  (X : Type x) →
    [inst : UniformSpace X] →
      [inst_1 : AddMonoid M] →
        [inst_2 : AddAction M X] → [UniformContinuousConstVAdd M X] → AddAction M (UniformSpace.Completion X)
-- Mathlib.Algebra.Field.IsField
/-- Transferring from `Semifield` to `IsField`.  -/
Semifield.toIsField : ∀ (R : Type u) [inst : Semifield R], IsField R
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.erase_zero : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), Polynomial.erase n 0 = 0
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
one_le_mabs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] (a : α), 1 ≤ |a|ₘ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.contains_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).contains k' =
        if cmp k k' = Ordering.eq then (f (Std.DTreeMap.Raw.Const.get? t k)).isSome else t.contains k'
-- Mathlib.Algebra.Module.Submodule.EqLocus
LinearMap.eqLocus_toAddSubmonoid : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f g : M →ₛₗ[τ₁₂] M₂), (f.eqLocus g).toAddSubmonoid = (↑f).eqLocusM ↑g
-- Std.Async.TCP
/-- Creates a `Selector` that resolves once `s` has data available, up to at most `size` bytes,
and provides that data. Calling this function does not starts the data wait, so it must not be called
in parallel with `recv?`.
 -/
Std.Async.TCP.Socket.Client.recvSelector : Std.Async.TCP.Socket.Client → UInt64 → Std.Async.Selector (Option ByteArray)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.ExtTreeMap.ofList l cmp).getKey? k' = some k
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.op_v₀₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.op.v₀₁ = CategoryTheory.ShortComplex.opMap S.v₂₃
-- Init.Data.String.Basic
String.Pos.ofSliceTo_inj : ∀ {s : String} {p₀ : s.Pos} {pos pos' : (s.sliceTo p₀).Pos},
  String.Pos.ofSliceTo pos = String.Pos.ofSliceTo pos' ↔ pos = pos'
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.alterKey.match_1.eq_1 : ∀ {α : Type u_3} {β : α → Type u_1} (k : α) (motive : Option (β k) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (v : β k) → motive (some v)),
  (match none with
    | none => h_1 ()
    | some v => h_2 v) =
    h_1 ()
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.restrictionLEIso_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (i : ℕ),
  h.restrictionLEIso.inv.f i =
    (HomologicalComplex.restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).inv
-- Std.Data.DHashMap.Basic
/-- Retrieves the key-value pair, whose key matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DHashMap.getEntry : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → (m : Std.DHashMap α β) → (a : α) → a ∈ m → (a : α) × β a
-- Mathlib.Topology.Spectral.ConstructibleTopology
compl_mem_constructibleTopologySubbasis_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  sᶜ ∈ constructibleTopologySubbasis X ↔ s ∈ constructibleTopologySubbasis X
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isDetecting_unop_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ),
  P.unop.IsDetecting ↔ P.IsCodetecting
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.instIsLeftCancelAdd : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] [∀ (i : ι), IsLeftCancelAdd (β i)],
  IsLeftCancelAdd (Π₀ (i : ι), β i)
-- Mathlib.Topology.MetricSpace.Isometry
/-- The composition of isometries is an isometry.  -/
Isometry.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {g : β → γ} {f : α → β}, Isometry g → Isometry f → Isometry (g ∘ f)
-- Mathlib.Data.List.Rotate
List.rotate'_rotate' : ∀ {α : Type u} (l : List α) (n m : ℕ), (l.rotate' n).rotate' m = l.rotate' (n + m)
-- Mathlib.Order.Bounds.Basic
lowerBounds_Ioo : ∀ {γ : Type u_3} [inst : SemilatticeSup γ] [DenselyOrdered γ] {a b : γ}, a < b → lowerBounds (Set.Ioo a b) = Set.Iic a
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_ae_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {f g : α → β} {d : α → ENNReal},
  AEMeasurable d μ → (∀ᵐ (x : α) ∂μ, d x ≠ 0) → (f =ᵐ[μ.withDensity d] g ↔ f =ᵐ[μ] g)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- An algebraic integer whose conjugates are all of norm one is a root of unity.  -/
NumberField.Embeddings.pow_eq_one_of_norm_eq_one : ∀ (K : Type u_1) [inst : Field K] [NumberField K] (A : Type u_2) [inst_2 : NormedField A] [IsAlgClosed A]
  [NormedAlgebra ℚ A] {x : K}, IsIntegral ℤ x → (∀ (φ : K →+* A), ‖φ x‖ = 1) → ∃ n, ∃ (_ : 0 < n), x ^ n = 1
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
MeasureTheory.IntegrableOn.continuousWithinAt_Ici_primitive_Ioi : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E}
  {a₀ : ℝ},
  MeasureTheory.IntegrableOn f (Set.Ioi a₀) μ →
    ContinuousWithinAt (fun b => ∫ (x : ℝ) in Set.Ioi b, f x ∂μ) (Set.Ici a₀) a₀
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_eq_some_get! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α},
  a ∈ m → Std.ExtDHashMap.Const.get? m a = some (Std.ExtDHashMap.Const.get! m a)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.measurableSet_inf : ∀ {α : Type u_1} {m₂ m₁ : MeasurableSpace α} {s : Set α}, MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atTop_of_antitone : ∀ {ι : Type u_3} {α : Type u_4} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α},
  Antitone f → Filter.Tendsto f Filter.atTop Filter.atBot ∨ ∃ l, Filter.Tendsto f Filter.atTop (nhds l)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.div_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Div Y] (f g : LocallyConstant X Y) (x : X),
  (f / g) x = f x / g x
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.instCoeTCFilter : {α : Type u} → CoeTC (Ultrafilter α) (Filter α)
-- Mathlib.Computability.Primrec.Basic
Primrec.encdec : ∀ {α : Type u_1} [inst : Primcodable α], Primrec fun n => Encodable.encode (Encodable.decode n)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimprocOLeanEntry.mk.sizeOf_spec : ∀ (declName : Lean.Name) (post : Bool) (keys : Array Lean.Meta.SimpTheoremKey),
  sizeOf { declName := declName, post := post, keys := keys } = 1 + sizeOf declName + sizeOf post + sizeOf keys
-- Mathlib.Tactic.NormNum.BigOperators
/-- If `s = t` and we can get the result for `t`, then we can get the result for `s`.
 -/
Mathlib.Meta.List.ProveNilOrConsResult.eq_trans : {u : Lean.Level} →
  {α : Q(Type u)} →
    {s t : Q(List «$α»)} →
      Q(«$s» = «$t») → Mathlib.Meta.List.ProveNilOrConsResult t → Mathlib.Meta.List.ProveNilOrConsResult s
-- Mathlib.CategoryTheory.Sums.Associator
/-- Characterizing the composition of the inverse of the associator and the right inclusion.  -/
CategoryTheory.sum.inrCompInverseAssociator : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (CategoryTheory.Sum.inr_ C (D ⊕ E)).comp (CategoryTheory.sum.inverseAssociator C D E) ≅
              ((CategoryTheory.Sum.inr_ C D).comp (CategoryTheory.Sum.inl_ (C ⊕ D) E)).sum'
                (CategoryTheory.Sum.inr_ (C ⊕ D) E)
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.map.denote_go : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {assign : α → Bool} {aig : Std.Sat.AIG α} (curr : ℕ)
  (hcurr : curr ≤ len) (s : aig.RefVec curr) (input : aig.RefVec len)
  (f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [inst_3 : Std.Sat.AIG.RefVec.LawfulMapOperator α f]
  (idx : ℕ) (hidx1 : idx < len),
  curr ≤ idx →
    ⟦assign,
        { aig := (Std.Sat.AIG.RefVec.map.go aig curr hcurr s input f).aig,
          ref := (Std.Sat.AIG.RefVec.map.go aig curr hcurr s input f).vec.get idx hidx1 }⟧ =
      ⟦assign, f aig (input.get idx hidx1)⟧
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.support_subset_verts : ∀ {V : Type u} {G : SimpleGraph V} (H : G.Subgraph), H.support ⊆ H.verts
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- Create a `BoxIntegral.Prepartition` from a collection of possibly empty boxes by filtering out
the empty one if it exists.  -/
BoxIntegral.Prepartition.ofWithBot : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} →
    (boxes : Finset (WithBot (BoxIntegral.Box ι))) →
      (∀ J ∈ boxes, J ≤ ↑I) → (↑boxes).Pairwise Disjoint → BoxIntegral.Prepartition I
-- Mathlib.NumberTheory.KummerDedekind
/-- Let `Q` be a lift of factor of the minimal polynomial of `x`, a generator of `S` over `R`, taken
`mod I`. Then (the reduction of) `Q` corresponds via
`normalizedFactorsMapEquivNormalizedFactorsMinPolyMk` to
`span (I.map (algebraMap R S) ∪ {Q.aeval x})`.  -/
KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R}
  [inst_3 : IsDomain R] [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDedekindDomain S]
  [inst_6 : Module.IsTorsionFree R S] (hI : I.IsMaximal) {Q : Polynomial R}
  (hQ :
    Polynomial.map (Ideal.Quotient.mk I) Q ∈
      UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
  (hI' : I ≠ ⊥) (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x),
  ↑((KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm
        ⟨Polynomial.map (Ideal.Quotient.mk I) Q, hQ⟩) =
    Ideal.span (↑(Ideal.map (algebraMap R S) I) ∪ {(Polynomial.aeval x) Q})
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.homologyData'_right_Q : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hk : c.next j = k) (h : (K.sc' i j k).HomologyData),
  (HomologicalComplex.extend.homologyData' K e hj' hi hk h).right.Q = h.right.Q
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.ediam_image_inter_le_of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s t : Set X}, HolderOnWith C r f s → ∀ {d : ENNReal}, Metric.ediam t ≤ d → Metric.ediam (f '' (t ∩ s)) ≤ ↑C * d ^ ↑r
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.brecOn.go : {motive : Lean.Meta.Grind.Arith.CommRing.PolyDerivation → Sort u} →
  (t : Lean.Meta.Grind.Arith.CommRing.PolyDerivation) →
    ((t : Lean.Meta.Grind.Arith.CommRing.PolyDerivation) →
        Lean.Meta.Grind.Arith.CommRing.PolyDerivation.below t → motive t) →
      motive t ×' Lean.Meta.Grind.Arith.CommRing.PolyDerivation.below t
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.addConstC.eq_def : ∀ (p : Lean.Grind.CommRing.Poly) (k : ℤ) (c : ℕ),
  p.addConstC k c =
    match p with
    | Lean.Grind.CommRing.Poly.num k' => Lean.Grind.CommRing.Poly.num ((k' + k) % ↑c)
    | Lean.Grind.CommRing.Poly.add k' m p => Lean.Grind.CommRing.Poly.add k' m (p.addConstC k c)
-- Mathlib.RingTheory.PowerSeries.Substitution
_private.Mathlib.RingTheory.PowerSeries.Substitution.0.PowerSeries.substInvFun.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ => h_3 n) =
    h_1 ()
-- Mathlib.RingTheory.FiniteType
RingHom.FiniteType.of_comp_finiteType : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  {f : A →+* B} {g : B →+* C}, (g.comp f).FiniteType → g.FiniteType
-- Batteries.Data.MLList.Basic
/-- Implementation of `MLList.aux`.  -/
_private.Batteries.Data.MLList.Basic.0.MLList.getLast?.aux : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → α → MLList m α → m (Option α)
-- Mathlib.Order.Bounds.Basic
isGLB_Ioo : ∀ {γ : Type u_3} [inst : SemilatticeSup γ] [DenselyOrdered γ] {a b : γ}, a < b → IsGLB (Set.Ioo a b) a
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.comp.match_1.splitter : {C : Type u_1} →
  (motive : CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Sort u_2) →
    (x x_1 x_2 : CategoryTheory.WithTerminal C) →
      ((_X _Y _Z : C) →
          motive (CategoryTheory.WithTerminal.of _X) (CategoryTheory.WithTerminal.of _Y)
            (CategoryTheory.WithTerminal.of _Z)) →
        ((_X : C) →
            (x : CategoryTheory.WithTerminal C) →
              motive (CategoryTheory.WithTerminal.of _X) x CategoryTheory.WithTerminal.star) →
          ((_X : C) →
              (x : CategoryTheory.WithTerminal C) →
                motive CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of _X) x) →
            ((x : CategoryTheory.WithTerminal C) →
                (_Y : C) → motive x CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of _Y)) →
              (Unit →
                  motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star
                    CategoryTheory.WithTerminal.star) →
                motive x x_1 x_2
-- Init.Data.Array.Lemmas
Array.mem_set : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size) {a : α}, a ∈ xs.set i a h
-- Mathlib.GroupTheory.PGroup
isPGroup_iff_orderOf_dvd_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g ∣ p ^ k
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.mul_X_pow_comp : ∀ {R : Type u} [inst : Semiring R] {p r : Polynomial R} {k : ℕ}, (p * Polynomial.X ^ k).comp r = p.comp r * r ^ k
-- Std.Time.Format.Modifier
Std.Time.Modifier.H.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.H presentation = Std.Time.Modifier.H presentation_1) = (presentation = presentation_1)
-- Mathlib.LinearAlgebra.Finsupp.LSum
Submodule.mulRightMap.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_4} [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : SMulCommClass R R S] [inst_4 : IsScalarTower R S S] (M : Submodule R S) {N : Submodule R S} {ι : Type u_5}
  (n n_1 : ι → ↥N), n = n_1 → M.mulRightMap n = M.mulRightMap n_1
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.prodEquiv_symm_apply : ∀ {R : Type u} [inst : Monoid R] {A : Type v} {B : Type w} {C : Type w₁} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : NonUnitalNonAssocSemiring C]
  [inst_5 : DistribMulAction R B] [inst_6 : DistribMulAction R C] (f : A →ₙₐ[R] B × C),
  NonUnitalAlgHom.prodEquiv.symm f = ((NonUnitalAlgHom.fst R B C).comp f, (NonUnitalAlgHom.snd R B C).comp f)
-- Init.Data.SInt.Basic
/-- Converts `true` to `1` and `false` to `0`.
 -/
Bool.toInt16 : Bool → Int16
-- Mathlib.Probability.Distributions.SetBernoulli
/-- `setBer(u, p)` only gives mass to families of sets contained in `u`.  -/
ProbabilityTheory.setBernoulli_apply_eq_apply_subsets : ∀ {ι : Type u_1} [Countable ι] (u : Set ι) (p : ↑unitInterval) (S : Set (Set ι)),
  (ProbabilityTheory.setBernoulli u p) S = (ProbabilityTheory.setBernoulli u p) {s | s ∈ S ∧ s ⊆ u}
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.instFstScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsSeparated g],
  AlgebraicGeometry.IsSeparated (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
DomMulAct.instSMulMulActionHomId : {M : Type u_1} →
  {α : Type u_2} →
    {N : Type u_3} →
      {β : Type u_4} →
        [inst : SMul M α] → [inst_1 : SMul N α] → [SMulCommClass M N α] → [inst : SMul N β] → SMul Mᵈᵐᵃ (α →ₑ[id] β)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D)
  (P : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))),
  ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).obj P).right = P.base
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.Functor.mapSkeleton_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.EssSurj], Function.Surjective F.mapSkeleton.obj
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
/-- Construct a preordering from a minimal set of axioms.  -/
RingPreordering.mk' : {R : Type u_3} →
  [inst : CommRing R] →
    (P : Set R) →
      (∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P) →
        (∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P) → (∀ (x : R), x * x ∈ P) → -1 ∉ P → RingPreordering R
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.instAndThenParser : AndThen Lean.ParseImports.Parser
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k a : α} {v : β},
  Std.DHashMap.Const.get? (m.insert k v) a = if (k == a) = true then some v else Std.DHashMap.Const.get? m a
-- Mathlib.Condensed.TopCatAdjunction
/-- The functor from condensed sets to topological spaces lands in compactly generated spaces.  -/
CondensedSet.condensedSetToCompactlyGenerated : CategoryTheory.Functor CondensedSet CompactlyGenerated
-- Mathlib.Analysis.Normed.Order.Lattice
HasSolidNorm.solid : ∀ {α : Type u_1} {inst : NormedAddCommGroup α} {inst_1 : Lattice α} [self : HasSolidNorm α] ⦃x y : α⦄,
  |x| ≤ |y| → ‖x‖ ≤ ‖y‖
-- Mathlib.Data.Complex.Basic
Complex.equivRealProdAddHom_symm_apply_im : ∀ (p : ℝ × ℝ), (Complex.equivRealProdAddHom.symm p).im = p.2
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.div_one : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K}, I / 1 = I
-- Init.Data.Range.Polymorphic.Basic
Std.Rxc.LawfulHasSize.mk : ∀ {α : Type u} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.Rxc.HasSize α],
  (∀ (lo hi : α), ¬lo ≤ hi → Std.Rxc.HasSize.size lo hi = 0) →
    (∀ (lo hi : α), lo ≤ hi → Std.PRange.succ? lo = none → Std.Rxc.HasSize.size lo hi = 1) →
      (∀ (lo hi lo' : α),
          lo ≤ hi → Std.PRange.succ? lo = some lo' → Std.Rxc.HasSize.size lo hi = Std.Rxc.HasSize.size lo' hi + 1) →
        Std.Rxc.LawfulHasSize α
-- Mathlib.RingTheory.IsAdjoinRoot
/-- See `finrank_quotient_span_eq_natDegree` for a more general version over a field.
 -/
finrank_quotient_span_eq_natDegree' : ∀ {R : Type u} [inst : CommRing R] {f : Polynomial R} [StrongRankCondition R],
  f.Monic → Module.finrank R (Polynomial R ⧸ Ideal.span {f}) = f.natDegree
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_add : ∀ {a b : UInt64}, (a + b).toBitVec = a.toBitVec + b.toBitVec
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote_div_eq_of_divCoeffs : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.Poly.divCoeffs k p = true →
    Int.Internal.Linear.Poly.denote ctx (Int.Internal.Linear.Poly.div k p) * k + Int.Internal.Linear.cmod p.getConst k =
      Int.Internal.Linear.Poly.denote ctx p
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_eq_single_of_mem : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] {s : Finset ι} {f : ι → M},
  ∀ a ∈ s, (∀ b ∈ s, b ≠ a → f b = 1) → ∏ x ∈ s, f x = f a
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
Homeomorph.refl_toOpenPartialHomeomorph : ∀ {X : Type u_1} [inst : TopologicalSpace X], (Homeomorph.refl X).toOpenPartialHomeomorph = OpenPartialHomeomorph.refl X
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.IsRestriction.restrict_delete_of_disjoint : ∀ {α : Type u_1} {M N : Matroid α} {X : Set α}, N.IsRestriction M → Disjoint X N.E → N.IsRestriction (M.delete X)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_rightUnitor : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  (X : Type u₇) [inst_6 : CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁),
  (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map ψ.rightUnitor.hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ
          (CategoryTheory.Limits.CatCospanTransform.id F₁ G₁)).hom
      (CategoryTheory.CategoryStruct.comp
        (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).whiskerLeft
          (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F₁ G₁).hom)
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).rightUnitor.hom)