mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.primitive_element_root : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {f : Polynomial F}
  (h : IsAdjoinRoot E f), F⟮h.root⟯ = ⊤
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.ext : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {f g : E →ₛₗ.[σ] F},
  f.domain = g.domain → (∀ ⦃x : E⦄ ⦃hf : x ∈ f.domain⦄ ⦃hg : x ∈ g.domain⦄, ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩) → f = g
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftRightHomologyComparison_fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] {Z : C} (h : S.rightHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.leftRightHomologyComparison h =
    CategoryTheory.CategoryStruct.comp S.leftHomologyIso.hom
      (CategoryTheory.CategoryStruct.comp S.rightHomologyIso.inv h)
-- Init.Data.Vector.Range
Vector.range.eq_1 : ∀ (n : ℕ), Vector.range n = Vector.mk (Array.range n) ⋯
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.DHashMap.Const.ofList l).getKey! k' = k
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap'_surjective : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S),
  Function.Surjective ⇑(M.mulMap' N)
-- Mathlib.RingTheory.Lasker
Submodule.IsMinimalPrimaryDecomposition.minimal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {t : Finset (Submodule R M)},
  N.IsMinimalPrimaryDecomposition t → ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
-- Mathlib.GroupTheory.OrderOfElement
not_isOfFinOrder_of_isMulTorsionFree : ∀ {G : Type u_1} [inst : Monoid G] {a : G} [IsMulTorsionFree G], a ≠ 1 → ¬IsOfFinOrder a
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.mulActionHom_preimage : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : SMul 𝕜 F]
  {s : Set F}, Balanced 𝕜 s → ∀ (f : E →ₑ[id] F), Balanced 𝕜 (⇑f ⁻¹' s)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pullback_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {X Y S : C} (f : X ⟶ S)
  (g : Y ⟶ S) [inst_1 : CategoryTheory.Limits.HasPullback f g] [P.IsStableUnderBaseChangeAlong g],
  P f → P (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
/-- The isomorphism `unionProd S T ≅ unionProd T S` as simplicial sets.  -/
SSet.Subcomplex.unionProd.symmIso : {X Y : SSet} → (S : X.Subcomplex) → (T : Y.Subcomplex) → (S.unionProd T).toSSet ≅ (T.unionProd S).toSSet
-- Mathlib.Analysis.Complex.RealDeriv
Complex.differentiable_re : Differentiable ℝ Complex.re
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_sub_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.U R (n - 1) = 2 * Polynomial.X * Polynomial.Chebyshev.U R n - Polynomial.Chebyshev.U R (n + 1)
-- Mathlib.Algebra.Free
/-- Recursor that uses `pure` instead of `of`.  -/
FreeAddSemigroup.recOnPure : {α : Type u} →
  {C : FreeAddSemigroup α → Sort l} →
    (x : FreeAddSemigroup α) →
      ((x : α) → C (pure x)) → ((x : α) → (y : FreeAddSemigroup α) → C (pure x) → C y → C (pure x + y)) → C x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tendsto_cos_neg_pi_div_two : Filter.Tendsto Real.cos (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2)))) (nhdsWithin 0 (Set.Ioi 0))
-- Mathlib.Topology.ContinuousMap.Basic
Function.RightInverse.homeomorph_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)} {f' : C(Y, X)}
  (hf : Function.RightInverse ⇑f' ⇑f) (a : Quotient (Setoid.ker ⇑f)), hf.homeomorph a = Setoid.kerLift (⇑f) a
-- Lean.Meta.Basic
/-- `withReducible x` executes `x` using the reducible transparency setting. In this setting only definitions tagged as `[reducible]` are unfolded.  -/
Lean.Meta.withReducible : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- `AbsoluteValue.abs` is `abs` as a bundled `AbsoluteValue`.  -/
AbsoluteValue.abs : {S : Type u_6} → [inst : Ring S] → [inst_1 : LinearOrder S] → [IsStrictOrderedRing S] → AbsoluteValue S S
-- Init.Data.List.Nat.TakeDrop
List.drop_take : ∀ {α : Type u_1} {i j : ℕ} {l : List α}, List.drop i (List.take j l) = List.take (j - i) (List.drop i l)
-- Mathlib.Algebra.Order.SuccPred
PredSubOrder.toPredOrder : {α : Type u_1} → {inst : Preorder α} → {inst_1 : Sub α} → {inst_2 : One α} → [self : PredSubOrder α] → PredOrder α
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- Get the equalizer object from the typeclass `IsCosplitPair`.  -/
CategoryTheory.HasSplitEqualizer.equalizerOfSplit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (f g : X ⟶ Y) → [CategoryTheory.HasSplitEqualizer f g] → C
-- Mathlib.Order.Preorder.Finsupp
Finsupp.coe_mono : ∀ {ι : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : Preorder M], Monotone Finsupp.toFun
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.homOfVector_over_assoc : ∀ {n : Type u} {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤)))
  {Z : AlgebraicGeometry.Scheme} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.homOfVector f v)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace n S ↘ S) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Computability.Encoding
/-- A standard Turing machine alphabet, consisting of blank,bit0,bit1,bra,ket,comma.  -/
Computability.Γ' : Type
-- Mathlib.Order.Filter.AtTopBot.Defs
IsTop.atTop_eq : ∀ {α : Type u_3} [inst : Preorder α] {a : α}, IsTop a → Filter.atTop = Filter.principal (Set.Ici a)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Choose a representative element from a given archimedean class.  -/
MulArchimedeanClass.out : {M : Type u_1} →
  [inst : CommGroup M] → [inst_1 : LinearOrder M] → [inst_2 : IsOrderedMonoid M] → MulArchimedeanClass M → M
-- Mathlib.Order.Interval.Set.Image
Antitone.mapsTo_Ici : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  Antitone f → Set.MapsTo f (Set.Ici a) (Set.Iic (f a))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.module.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.module = 1
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `none` if the
map is empty.
 -/
Std.ExtTreeMap.minEntry? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → Option (α × β)
-- Mathlib.NumberTheory.Dioph
/-- The set of places where two Diophantine functions are equal is Diophantine.  -/
Dioph.eq_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph {v | f v = g v}
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.imageIsoImage_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Abelian.imageIsoImage f).inv =
    CategoryTheory.Limits.kernel.lift (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.Limits.image.ι f) ⋯
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.mkPatternFromTypeWithKey : {α : Type} →
  List Lean.Name → Lean.Expr → (Lean.Expr → Lean.MetaM (Lean.Expr × α)) → Lean.MetaM (Lean.Meta.Sym.Pattern × α)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.rcons.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : (i : ι) → DecidableEq (M i)] {i : ι}
  (p : Monoid.CoprodI.Word.Pair M i),
  Monoid.CoprodI.Word.rcons p = if h : p.head = 1 then p.tail else Monoid.CoprodI.Word.cons p.head p.tail ⋯ h
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.exists_eq_one : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → One (G i)] [∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)] (x : (i : ι) × G i),
  ⟦x⟧ = 1 ↔ ∃ i, ∃ (h : x.fst ≤ i), (f x.fst i h) x.snd = 1
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Flavors.unbounded : {α : Type} → Std.CloseableChannel.Unbounded✝ α → Std.CloseableChannel.Flavors α
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.mk_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) (e' : N → M)
  (h₁ : Function.LeftInverse e' ⇑e) (h₂ : Function.RightInverse e' ⇑e)
  (h₃ :
    ∀ (x y : M),
      { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) =
        { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x +
          { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y),
  { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_add' := h₃ } = e
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∈ m₂ → Std.DHashMap.Raw.Const.getD (m₁.diff m₂) k fallback = fallback
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.deriv.match_1.eq_6 : ∀ {α : Type u_1} (motive : RegularExpression α → α → Sort u_2) (P : RegularExpression α) (a : α)
  (h_1 : (x : α) → motive RegularExpression.zero x) (h_2 : (x : α) → motive RegularExpression.epsilon x)
  (h_3 : (a₁ a₂ : α) → motive (RegularExpression.char a₁) a₂)
  (h_4 : (P Q : RegularExpression α) → (a : α) → motive (P.plus Q) a)
  (h_5 : (P Q : RegularExpression α) → (a : α) → motive (P.comp Q) a)
  (h_6 : (P : RegularExpression α) → (a : α) → motive P.star a),
  (match P.star, a with
    | RegularExpression.zero, x => h_1 x
    | RegularExpression.epsilon, x => h_2 x
    | RegularExpression.char a₁, a₂ => h_3 a₁ a₂
    | P.plus Q, a => h_4 P Q a
    | P.comp Q, a => h_5 P Q a
    | P.star, a => h_6 P a) =
    h_6 P a
-- Qq.Macro
Qq.Impl.UnquoteState : Type
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.forget_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Comon C),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Comon.forget C) X Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X)
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommFoldr_cons : ∀ {α : Type u_3} {β : Type u_4} (f : α → β → β) (s : Multiset α) (a : α)
  (h : {x | x ∈ a ::ₘ s}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b))
  (h' : {x | x ∈ s}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)) (b : β),
  Multiset.noncommFoldr f (a ::ₘ s) h b = f a (Multiset.noncommFoldr f s h' b)
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUTimes.mk.inj : ∀ {user nice sys idle irq user_1 nice_1 sys_1 idle_1 irq_1 : UInt64},
  { user := user, nice := nice, sys := sys, idle := idle, irq := irq } =
      { user := user_1, nice := nice_1, sys := sys_1, idle := idle_1, irq := irq_1 } →
    user = user_1 ∧ nice = nice_1 ∧ sys = sys_1 ∧ idle = idle_1 ∧ irq = irq_1
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- A finite measure `μ` on the additive quotient of `α` by `G` satisfying
`AddQuotientMeasureEqMeasurePreimage` has finite covolume.  -/
MeasureTheory.AddQuotientMeasureEqMeasurePreimage.covolume_ne_top : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α]
  (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α)))
  [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.addCovolume G α ν < ⊤
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.id_map : ∀ (V : Type u_1) [inst : CategoryTheory.ReflQuiver V] {X Y : V} (f : X ⟶ Y), (𝟭rq V).map f = f
-- Mathlib.Data.Int.Init
Int.neg_pred : ∀ (a : ℤ), -a.pred = (-a).succ
-- Mathlib.Logic.Equiv.Prod
Equiv.sumProdDistrib_apply_right : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (b : β) (c : γ),
  (Equiv.sumProdDistrib α β γ) (Sum.inr b, c) = Sum.inr (b, c)
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.coe_toNonUnitalRingHom : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] (f : A →⋆ₙ+* B), ⇑f.toNonUnitalRingHom = ⇑f
-- Init.Classical
Classical.and_or_imp : ∀ {a b c : Prop}, a ∧ b ∨ (a → c) ↔ a → b ∨ c
-- Aesop.Tree.Data
Aesop.Rapp.state : Aesop.Rapp → Aesop.NodeState
-- Mathlib.Order.Interval.Finset.Defs
/-- A constructor from a definition of `Finset.Iic` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrderBot.ofIic'`, this one requires `PartialOrder` but
only `DecidableEq`.  -/
LocallyFiniteOrderBot.ofIic : (α : Type u_1) →
  [inst : PartialOrder α] →
    [DecidableEq α] → (finsetIic : α → Finset α) → (∀ (a x : α), x ∈ finsetIic a ↔ x ≤ a) → LocallyFiniteOrderBot α
-- Lean.Meta.Tactic.Util
/-- Assign `mvarId` to `sorryAx`  -/
Lean.MVarId.admit : Lean.MVarId → optParam Bool true → Lean.MetaM Unit
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isNone_minKey?_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.minKey?.isNone = t.isEmpty
-- Mathlib.RepresentationTheory.Intertwining
/-- dualTensorHom as an equivalence of representations.  -/
Representation.Equiv.dualTensorHom : {G : Type u_6} →
  {k : Type u_7} →
    {V : Type u_8} →
      {W : Type u_9} →
        [inst : Group G] →
          [inst_1 : Field k] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : Module k V] →
                [inst_4 : AddCommGroup W] →
                  [inst_5 : Module k W] →
                    [FiniteDimensional k V] →
                      (ρ : Representation k G V) → (σ : Representation k G W) → (ρ.dual.tprod σ).Equiv (ρ.linHom σ)
-- Std.Data.DHashMap.Lemmas
_private.Std.Data.DHashMap.Lemmas.0.Std.DHashMap.ext : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {t t' : Std.DHashMap α β}, t.inner = t'.inner → t = t'
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.toAlgHom_toLinearMap : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₐc[R] B), ↑↑f = ↑f
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The value group of the valuation associated to `A`. Note: it is actually a group with zero.  -/
ValuationSubring.ValueGroup : {K : Type u} → [inst : Field K] → ValuationSubring K → Type u
-- Mathlib.Algebra.CharP.IntermediateField
IntermediateField.charP : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E)
  (p : ℕ) [CharP F p], CharP (↥L) p
-- Mathlib.CategoryTheory.Action.Monoidal
CategoryTheory.Functor.mapAction_ε_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {W : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} W] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [inst_5 : F.LaxMonoidal],
  (CategoryTheory.Functor.LaxMonoidal.ε (F.mapAction G)).hom = CategoryTheory.Functor.LaxMonoidal.ε F
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instSMul : {M : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] → [inst_1 : SMul M X] → [ContinuousConstSMul M X] → SMul M (SeparationQuotient X)
-- Mathlib.RingTheory.Algebraic.Integral
IsIntegral.trans_isAlgebraic : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S]
  [alg : Algebra.IsAlgebraic R S] {a : A}, IsIntegral S a → IsAlgebraic R a
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comap_undef : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β}
  {μ : MeasureTheory.Measure β},
  ¬(Function.Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ) →
    MeasureTheory.Measure.comap f μ = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` preserves colimits of shape `Jᵒᵖ`, then `F.rightOp : C ⥤ Dᵒᵖ` preserves limits
of shape `J`.  -/
CategoryTheory.Limits.preservesLimitsOfShape_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ D)
  [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.PreservesLimitsOfShape J F.rightOp
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.abs_abs_iff : ∀ {R : Type u} [inst : CommRing R] [inst_1 : LinearOrder R] [AddLeftMono R] (x y : R), IsCoprime |x| |y| ↔ IsCoprime x y
-- Mathlib.Data.NNReal.Defs
Real.cast_natAbs_eq_nnabs_cast : ∀ (n : ℤ), ↑n.natAbs = Real.nnabs ↑n
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.toSubgraph_adj : ∀ {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H ≤ G) (a a_1 : V),
  (SimpleGraph.toSubgraph H h).Adj a a_1 = H.Adj a a_1
-- Aesop.Stats.Basic
Aesop.Stats.empty : Aesop.Stats
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.then_eval : ∀ {k k' : Turing.ToPartrec.Cont} {v : List ℕ}, (k.then k').eval v = k.eval v >>= k'.eval
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.LawfulEqCmp cmp]
  [Std.TransCmp cmp], t.WF → ∀ {k : α}, k ∈ t.keys ↔ k ∈ t
-- Mathlib.Data.Fintype.Quotient
Quotient.finChoiceEquiv_apply : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  (q : (i : ι) → Quotient (S i)), Quotient.finChoiceEquiv q = Quotient.finChoice q
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The tensor product `A ⊗[ℤ] B` is a coproduct for `A` and `B`.  -/
CommRingCat.coproductCoconeIsColimit : (A B : CommRingCat) → CategoryTheory.Limits.IsColimit (A.coproductCocone B)
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- Postcomposition with a linear isometry preserves the operator norm.  -/
ContinuousLinearMap.opNorm_linearIsometryEquiv_mul : ∀ {𝕜 : Type u_1} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] (e : E ≃ₗᵢ[𝕜] E) (f : E →L[𝕜] E), ‖↑↑e * f‖ = ‖f‖
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.ContainsIdentities]
  [P.RespectsIso] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f], P f
-- Lean.Meta.Tactic.Grind.Core
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.propagateUnitConstFuns : Array Lean.Expr → Array Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
_private.Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality.0.InnerProductGeometry.ortho_ne_zero_of_not_collinear : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  ‖x‖ = 1 →
    ‖y‖ = 1 →
      InnerProductGeometry.angle x y ≠ 0 →
        InnerProductGeometry.angle x y ≠ Real.pi → InnerProductGeometry.ortho✝ x y ≠ 0
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.Hom.mk.inj : ∀ {X Y : Bipointed} {toFun : X.X → Y.X} {map_fst : toFun X.toProd.1 = Y.toProd.1}
  {map_snd : toFun X.toProd.2 = Y.toProd.2} {toFun_1 : X.X → Y.X} {map_fst_1 : toFun_1 X.toProd.1 = Y.toProd.1}
  {map_snd_1 : toFun_1 X.toProd.2 = Y.toProd.2},
  { toFun := toFun, map_fst := map_fst, map_snd := map_snd } =
      { toFun := toFun_1, map_fst := map_fst_1, map_snd := map_snd_1 } →
    toFun = toFun_1
-- Mathlib.Algebra.Module.Projective
/-- A module is projective iff it is the direct summand of a free module.  -/
Module.Projective.iff_split : ∀ {R : Type u} [inst : Semiring R] {P : Type v} [inst_1 : AddCommMonoid P] [inst_2 : Module R P],
  Module.Projective R P ↔ ∃ M x x_1, ∃ (_ : Module.Free R M), ∃ i s, s ∘ₗ i = LinearMap.id
-- Mathlib.Data.Finset.Defs
Finset.decidableMem' : {α : Type u_1} → [DecidableEq α] → (a : α) → (s : Finset α) → Decidable (a ∈ ↑s)
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- Variant of `MeromorphicOn.circleIntegrable_log_norm` for factorized rational functions.
 -/
circleIntegrable_log_norm_factorizedRational : ∀ {R : ℝ} {c : ℂ} (D : ℂ → ℤ), CircleIntegrable (∑ᶠ (u : ℂ), fun x => ↑(D u) * Real.log ‖x - u‖) c R
-- Mathlib.Condensed.Discrete.Colimit
Condensed.isoFinYonedaComponents.congr_simp : ∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : Profinite) [inst_1 : Finite ↑X.toTop],
  Condensed.isoFinYonedaComponents F X = Condensed.isoFinYonedaComponents F X
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
isBoundedLinearMap_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f : E → F},
  IsBoundedLinearMap 𝕜 f ↔ IsLinearMap 𝕜 f ∧ ∃ M, 0 < M ∧ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullback i i]
  [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
  [inst_5 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
      (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i)
          (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
            (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f i)
          (CategoryTheory.CategoryStruct.comp g i))) =
    CategoryTheory.Limits.pullback.snd f g