mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_monadMap_trans_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m n o : Type u → Type v} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : (α : Type u) → Std.Internal.Do.WP (o α) α Pred EPred]
  {α : Type u} {f : {β : Type u} → m β → m β} {post : α → Pred} {epost : EPred} [inst_3 : MonadFunctor n o]
  [inst_4 : MonadFunctorT m n] (x : o α),
  Std.Internal.Do.wp (monadMap f x) post epost =
    Std.Internal.Do.wp (MonadFunctor.monadMap (fun {β} => monadMap fun {β} => f) x) post epost
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (state : Std.Mutex (Std.CloseableChannel.Zero.State✝ α)),
  sizeOf { state := state } = 1 + sizeOf state
-- Mathlib.Data.Seq.Computation
Computation.LiftRelRec.lem : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} (C : Computation α → Computation β → Prop),
  (∀ {ca : Computation α} {cb : Computation β}, C ca cb → Computation.LiftRelAux R C ca.destruct cb.destruct) →
    ∀ (ca : Computation α) (cb : Computation β), C ca cb → ∀ a ∈ ca, Computation.LiftRel R ca cb
-- Mathlib.Order.Bounded
Set.unbounded_gt_iff : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α], Set.Unbounded (fun x1 x2 => x1 > x2) s ↔ ∀ (a : α), ∃ b ∈ s, b ≤ a
-- Mathlib.Logic.Relator
Relator.rel_or : Relator.LiftFun (fun x1 x2 => x1 ↔ x2) (Relator.LiftFun (fun x1 x2 => x1 ↔ x2) fun x1 x2 => x1 ↔ x2)
  (fun x1 x2 => x1 ∨ x2) fun x1 x2 => x1 ∨ x2
-- Init.Conv
Lean.Parser.Tactic.Conv.conv.quot : Lean.ParserDescr
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.toArray_succ_succ_eq_map : ∀ {α : Type u} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [inst_4 : Std.PRange.InfinitelyUpwardEnumerable α]
  [inst_5 : Std.Rxi.IsAlwaysFinite α] [inst_6 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] {lo : α},
  (Std.PRange.succ lo)<...*.toArray = Array.map Std.PRange.succ lo<...*.toArray
-- Init.Control.State
instMonadAttachStateTOfMonad : {m : Type u_1 → Type u_2} → {σ : Type u_1} → [Monad m] → [MonadAttach m] → MonadAttach (StateT σ m)
-- Mathlib.Data.Finset.Option
Finset.insertNone.eq_1 : ∀ {α : Type u_1},
  Finset.insertNone = OrderEmbedding.ofMapLEIff (fun s => Finset.cons none (Finset.map Function.Embedding.some s) ⋯) ⋯
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
/-- Converting a monoid object in `ModuleCat R` to a bundled algebra.
 -/
ModuleCat.MonModuleEquivalenceAlgebra.functor : {R : Type u} → [inst : CommRing R] → CategoryTheory.Functor (CategoryTheory.Mon (ModuleCat R)) (AlgCat R)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.degree_toSubgraph : ∀ {V : Type u} (G H : SimpleGraph V) (h : H ≤ G) {v : V} [inst : Fintype ↑((SimpleGraph.toSubgraph H h).neighborSet v)]
  [inst_1 : Fintype ↑(H.neighborSet v)], (SimpleGraph.toSubgraph H h).degree v = H.degree v
-- Mathlib.Order.Interval.Set.Union
/-- Union of consecutive intervals contains the interval defined by the initial and final points.  -/
Ico_subset_biUnion_Ico : ∀ {X : Type u_1} [inst : LinearOrder X] (N : ℕ) (a : ℕ → X),
  Set.Ico (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Set.Ico (a i) (a (i + 1))
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeAddGroup.basis.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : IsFreeAddGroup G],
  IsFreeAddGroup.basis G = { repr := (IsFreeAddGroup.addEquiv G).symm }
-- Init.Data.SInt.Basic
/-- Negates 32-bit signed integers. Usually accessed via the `-` prefix operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.neg : Int32 → Int32
-- Mathlib.Algebra.Free
Magma.AssocQuotient.hom_ext_iff : ∀ {α : Type u} [inst : Mul α] {β : Type v} [inst_1 : Semigroup β] {f g : Magma.AssocQuotient α →ₙ* β},
  f = g ↔ f.comp Magma.AssocQuotient.of = g.comp Magma.AssocQuotient.of
-- Lean.Elab.DefView
/-- Type including parameters.  -/
Lean.Elab.DefViewElabHeaderData.type : Lean.Elab.DefViewElabHeaderData → Lean.Expr
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.tensorUnit_obj : ∀ (R : Type u) [inst : CommRing R],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat R)).obj =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R)
-- Mathlib.Data.Finset.Option
Finset.none_mem_insertNone : ∀ {α : Type u_1} {s : Finset α}, none ∈ Finset.insertNone s
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If two unoriented angles are equal, and the signs of the corresponding oriented angles are
equal, then the oriented angles are equal (even in degenerate cases).  -/
EuclideanGeometry.oangle_eq_of_angle_eq_of_sign_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ p₅ p₆ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₅ p₆ →
    (EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₄ p₅ p₆).sign →
      EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₄ p₅ p₆
-- Init.Core
Or.symm : ∀ {a b : Prop}, a ∨ b → b ∨ a
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm.congr_simp : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (f f_1 : PadicSeq p), f = f_1 → f.norm = f_1.norm
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.Suggestion.mk.inj : ∀ {suggestion : Lean.Meta.Tactic.TryThis.SuggestionText} {preInfo? postInfo? : Option String}
  {style? : Option Lean.Meta.Tactic.TryThis.SuggestionStyle} {messageData? : Option Lean.MessageData}
  {toCodeActionTitle? : Option (String → String)} {suggestion_1 : Lean.Meta.Tactic.TryThis.SuggestionText}
  {preInfo?_1 postInfo?_1 : Option String} {style?_1 : Option Lean.Meta.Tactic.TryThis.SuggestionStyle}
  {messageData?_1 : Option Lean.MessageData} {toCodeActionTitle?_1 : Option (String → String)},
  { suggestion := suggestion, preInfo? := preInfo?, postInfo? := postInfo?, style? := style?,
        messageData? := messageData?, toCodeActionTitle? := toCodeActionTitle? } =
      { suggestion := suggestion_1, preInfo? := preInfo?_1, postInfo? := postInfo?_1, style? := style?_1,
        messageData? := messageData?_1, toCodeActionTitle? := toCodeActionTitle?_1 } →
    suggestion = suggestion_1 ∧
      preInfo? = preInfo?_1 ∧
        postInfo? = postInfo?_1 ∧
          style? = style?_1 ∧ messageData? = messageData?_1 ∧ toCodeActionTitle? = toCodeActionTitle?_1
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.Raw.Const.getEntryLED : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α → α × β → α × β
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.pairingIn_le_zero_of_ne : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [CharZero R] [IsDomain R] [inst_7 : P.IsCrystallographic] [Finite ι] {i j : ι},
  i ≠ j → i ∈ b.support → j ∈ b.support → P.pairingIn ℤ i j ≤ 0
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- A generalized eigenvalue for some exponent `k` is also
a generalized eigenvalue for exponents larger than `k`.  -/
Module.End.HasUnifEigenvalue.le : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k m : ℕ∞}, k ≤ m → f.HasUnifEigenvalue μ k → f.HasUnifEigenvalue μ m
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.tensorObj.eq_1 : ∀ (m_2 n_2 : SimplexCategory),
  AugmentedSimplexCategory.tensorObj (CategoryTheory.WithInitial.of m_2) (CategoryTheory.WithInitial.of n_2) =
    CategoryTheory.WithInitial.of (AugmentedSimplexCategory.tensorObjOf m_2 n_2)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- A linear equivalence constructing a semilinear map `M ⊗ N → P` given a bilinear map `M → N → P`
with the property that its composition with the canonical bilinear map `M → N → M ⊗ N` is
the given bilinear map `M → N → P`.  -/
TensorProduct.lift.equiv : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring R₂] →
        (σ₁₂ : R →+* R₂) →
          (M : Type u_7) →
            (N : Type u_8) →
              (P₂ : Type u_17) →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid N] →
                    [inst_4 : AddCommMonoid P₂] →
                      [inst_5 : Module R M] →
                        [inst_6 : Module R N] →
                          [inst_7 : Module R₂ P₂] → (M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) ≃ₗ[R₂] TensorProduct R M N →ₛₗ[σ₁₂] P₂
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaAddMonObjIsoOfRepresentableBy_inv_app_hom_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (F : CategoryTheory.Functor Cᵒᵖ AddMonCat) (α : (F.comp (CategoryTheory.forget AddMonCat)).RepresentableBy X)
  (X_1 : Cᵒᵖ) (a : ↑(F.1 X_1)),
  (AddMonCat.Hom.hom ((CategoryTheory.yonedaAddMonObjIsoOfRepresentableBy X F α).inv.app X_1)) a = α.homEquiv'.symm a
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.map_comap_eq_self : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] {f : K →+* L} {s : Subfield L},
  s ≤ f.fieldRange → Subfield.map f (Subfield.comap f s) = s
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Functor.essImage.of_underPost : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {F : CategoryTheory.Functor T D} {Y : CategoryTheory.Under (F.obj X)},
  (CategoryTheory.Under.post F).essImage Y → F.essImage Y.right
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectL_map₂ : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (c : C)
  {a b : B} {f g : a ⟶ b} (a_1 : f ⟶ g),
  (CategoryTheory.Bicategory.Prod.sectL B c).map₂ a_1 =
    CategoryTheory.Prod.mkHom a_1 (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id c))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_eq_some_get!_of_contains : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF → ∀ {a : α}, m.contains a = true → Std.DHashMap.Raw.Const.get? m a = some (Std.DHashMap.Raw.Const.get! m a)
-- Mathlib.Data.Fin.Rev
Fin.predAbove_rev_left : ∀ {n : ℕ} (p : Fin n) (i : Fin (n + 1)), p.rev.predAbove i = (p.predAbove i.rev).rev
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  k ∈ t.insertMany l ↔ k ∈ t ∨ (List.map Sigma.fst l).contains k = true
-- Mathlib.LinearAlgebra.LinearPMap
/-- Restrict a linear map to a submodule, reinterpreting the result as a `LinearPMap`.  -/
LinearMap.toPMap : {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] → (E →ₛₗ[σ] F) → Submodule R E → E →ₛₗ.[σ] F
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.intCast_toProd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (n : ℤ), (↑n).toProd = ↑n
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertMany!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ ((a : α) × β a)]
  (t : Std.DTreeMap.Internal.Impl α β) (l : ρ),
  t.insertMany! l =
    (have r := ⟨t, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | ⟨a, b⟩ =>
              have r := ⟨Std.DTreeMap.Internal.Impl.insert! a b ↑r, ⋯⟩;
              pure (ForInStep.yield r)
      have r : t.IteratedSlowInsertionInto := __s
      pure r).run
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.semiring : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [Monoid M] → Semiring (MonoidAlgebra R M)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.leftHomologyMap'_sub : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.ShortComplex.leftHomologyMap' (φ - φ') h₁ h₂ =
    CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂ - CategoryTheory.ShortComplex.leftHomologyMap' φ' h₁ h₂
-- Mathlib.Order.WithBot
WithTop.coe_injective : ∀ {α : Type u_1}, Function.Injective WithTop.some
-- Lean.Meta.MkIffOfInductiveProp
/-- For each forall-bound variable in the type of the constructor, minus
the "params" that apply to the entire inductive type, this list contains `true`
if that variable has been kept after `compactRelation`.

For example, `List.Chain.nil` has type
```lean
  ∀ {α : Type u_1} {R : α → α → Prop} {a : α}, List.Chain R a []`
```
and the first two variables `α` and `R` are "params", while the `a : α` gets
eliminated in a `compactRelation`, so `variablesKept = [false]`.

`List.Chain.cons` has type
```lean
  ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α},
     R a b → List.Chain R b l → List.Chain R a (b :: l)
```
and the `a : α` gets eliminated, so `variablesKept = [false,true,true,true,true]`.
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.Shape.variablesKept : Lean.Meta.Shape✝ → List Bool
-- Mathlib.Topology.Connected.Basic
DenseRange.preconnectedSpace : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [PreconnectedSpace α] {f : α → β},
  DenseRange f → Continuous f → PreconnectedSpace β
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
Rep.norm_comp_d_eq_zero : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (M : Rep.{max u u_1, u, u} R G),
  CategoryTheory.CategoryStruct.comp (Rep.Hom.toModuleCatHom M.norm) (groupCohomology.d₀₁ M) = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.eta_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (t : CategoryTheory.Limits.PullbackCone f g), t.eta.hom.hom = CategoryTheory.CategoryStruct.id t.pt
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.ofLE_comp_ofLE : ∀ {X : Type u_2} [inst : TopologicalSpace X] {A B C : DiscreteQuotient X} (h₁ : A ≤ B) (h₂ : B ≤ C),
  DiscreteQuotient.ofLE h₂ ∘ DiscreteQuotient.ofLE h₁ = DiscreteQuotient.ofLE ⋯
-- Mathlib.RingTheory.Congruence.Basic
/-- The infimum of two congruence relations equals the infimum of the underlying binary
operations.  -/
RingCon.coe_inf : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R}, ⇑(c ⊓ d) = ⇑c ⊓ ⇑d
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k a : α} {v : β k},
      (t.insertIfNew k v).get? a = if h : cmp k a = Ordering.eq ∧ k ∉ t then some (cast ⋯ v) else t.get? a
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.sinPoly.eq_1 : sinPoly✝ 0 = Polynomial.C 2
-- Aesop.Frontend.Saturate
Aesop.Frontend.mkForwardOptions : Option ℕ → Bool → Lean.CoreM Aesop.Options'
-- Mathlib.Combinatorics.SimpleGraph.Hasse
/-- `αᵒᵈ` and `α` have the same Hasse diagram.  -/
SimpleGraph.hasseDualIso : {α : Type u_1} → [inst : Preorder α] → SimpleGraph.hasse αᵒᵈ ≃g SimpleGraph.hasse α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  (Std.TreeMap.Raw.unitOfList l cmp)[k]? = if l.contains k = true then some () else none
-- Std.Http.Data.Chunk
Std.Http.Trailer.mk.injEq : ∀ (headers headers_1 : Std.Http.Headers), ({ headers := headers } = { headers := headers_1 }) = (headers = headers_1)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.centralizer_le : ∀ {R : Type u_1} [inst : Ring R] (s t : Set R), s ⊆ t → Subring.centralizer t ≤ Subring.centralizer s
-- Mathlib.Data.Set.Inclusion
Set.eq_of_inclusion_surjective : ∀ {α : Type u_1} {s t : Set α} {h : s ⊆ t}, Function.Surjective (Set.inclusion h) → s = t
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Returns the sequence of partial numerators `aᵢ` of `g`.  -/
GenContFract.partNums : {α : Type u_1} → GenContFract α → Stream'.Seq α
-- Mathlib.RingTheory.Bialgebra.Quotient
Bialgebra.Quotient.counit_comp_mkₐ : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Bialgebra R A] (I : Ideal A)
  [inst_3 : I.IsTwoSided] [inst_4 : (Submodule.restrictScalars R I).IsCoideal],
  (Bialgebra.Quotient.counitAlgHom I).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap = CoalgebraStruct.counit
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.proetaleTopology_eq_propQCTopology : AlgebraicGeometry.Scheme.proetaleTopology = AlgebraicGeometry.Scheme.propQCTopology @AlgebraicGeometry.WeaklyEtale
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.instBEqExtTheorem : BEq Lean.Meta.Ext.ExtTheorem
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.int_hom_ext : ∀ {G : AddCommGrpCat} (f g : AddCommGrpCat.of ℤ ⟶ G),
  (CategoryTheory.ConcreteCategory.hom f) 1 = (CategoryTheory.ConcreteCategory.hom g) 1 → f = g
-- Mathlib.Data.Num.Bitwise
/-- Bitwise "or" for `PosNum`.  -/
PosNum.lor : PosNum → PosNum → PosNum
-- Mathlib.Order.Hom.WithTopBot
/-- A version of `WithTop.map` for order embeddings.  -/
OrderEmbedding.withTopMap : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → α ↪o β → WithTop α ↪o WithTop β
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) {V : (↑U).Opens} (x : ↥U) (hx : x ∈ V),
  CategoryTheory.CategoryStruct.comp ((↑U).presheaf.germ V x hx) (U.stalkIso x).hom =
    X.presheaf.germ ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V) ↑x ⋯
-- Init.Data.SInt.Lemmas
ISize.sub_add_cancel : ∀ (a b : ISize), a - b + b = a
-- Mathlib.Order.ScottContinuity
ScottContinuousOn.snd : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {D : Set (Set (α × β))},
  ScottContinuousOn D Prod.snd
-- Std.Data.ExtHashSet.Basic
/-- Returns `true` if the given key is present in the set. There is also a `Prop`-valued version of
this: `a ∈ m` is equivalent to `m.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` use
`==` for comparisons, while for hash sets, both use `==`.
 -/
Std.ExtHashSet.contains : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashSet α → α → Bool
-- Mathlib.GroupTheory.Finiteness
AddSubmonoid.FG.map : ∀ {M : Type u_1} [inst : AddMonoid M] {M' : Type u_3} [inst_1 : AddMonoid M'] {P : AddSubmonoid M},
  P.FG → ∀ (e : M →+ M'), (AddSubmonoid.map e P).FG
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
Topology.IsClosedEmbedding.integral_map : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {β : Type u_6} [inst_2 : TopologicalSpace α] [BorelSpace α]
  [inst_4 : TopologicalSpace β] [inst_5 : MeasurableSpace β] [BorelSpace β] {φ : α → β},
  Topology.IsClosedEmbedding φ → ∀ (f : β → G), ∫ (y : β), f y ∂MeasureTheory.Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
/-- The Cartesian lift of `f`.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.cartesianLift : {𝒮 : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      {R S : 𝒮} →
        (a : ↑(F.obj { as := Opposite.op S })) →
          (f : R ⟶ S) → CategoryTheory.Pseudofunctor.CoGrothendieck.domainCartesianLift a f ⟶ { base := S, fiber := a }
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.CompatibleSMul.mk : ∀ {M : Type u_8} {M₂ : Type u_10} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] {R : Type u_14} {S : Type u_15}
  [inst_2 : Semiring S] [inst_3 : SMul R M] [inst_4 : Module S M] [inst_5 : SMul R M₂] [inst_6 : Module S M₂],
  (∀ (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c • x) = c • fₗ x) → LinearMap.CompatibleSMul M M₂ R S
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₂ : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  (hfg : (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker),
  (CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg).X₂ = X₂
-- Mathlib.Algebra.Module.LinearMap.End
LinearMap.compRight_apply : ∀ {R : Type u_1} (S : Type u_3) {M : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module S M₁] [inst_9 : Module S M₂]
  [inst_10 : SMulCommClass R S M₁] [inst_11 : SMulCommClass R S M₂] [inst_12 : LinearMap.CompatibleSMul M₁ M₂ S R]
  (f : M₁ →ₗ[R] M₂) (g : M →ₗ[R] M₁), (LinearMap.compRight S f) g = f ∘ₗ g
-- Mathlib.Data.Semiquot
Semiquot.eq_mk_of_mem : ∀ {α : Type u_1} {q : Semiquot α} {a : α} (h : a ∈ q), q = Semiquot.mk h
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.snd.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
  (p : CategoryTheory.OverPresheafAux.YonedaCollection F X), p.snd = p.snd
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
/-- If a group `K` acts on a cyclic `p`-group `G` of coprime order, then the map `K × G → G`
defined by `(k, g) ↦ k • g * g⁻¹` is either trivial or surjective.  -/
IsPGroup.smul_mul_inv_trivial_or_surjective : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] [IsCyclic G],
  IsPGroup p G →
    ∀ {K : Type u_4} [inst_3 : Group K] [inst_4 : MulDistribMulAction K G],
      (Nat.card G).Coprime (Nat.card K) → (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g
-- Mathlib.Order.RelSeries
RelSeries.mk.inj : ∀ {α : Type u_1} {r : SetRel α α} {length : ℕ} {toFun : Fin (length + 1) → α}
  {step : ∀ (i : Fin length), (toFun i.castSucc, toFun i.succ) ∈ r} {length_1 : ℕ} {toFun_1 : Fin (length_1 + 1) → α}
  {step_1 : ∀ (i : Fin length_1), (toFun_1 i.castSucc, toFun_1 i.succ) ∈ r},
  { length := length, toFun := toFun, step := step } = { length := length_1, toFun := toFun_1, step := step_1 } →
    length = length_1 ∧ toFun ≍ toFun_1
-- Init.System.IOError
IO.Error.mkNoSuchThingFile : String → UInt32 → String → IO.Error
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.of.inj : ∀ {carrier : Type u} {commRing : CommRing carrier} {carrier_1 : Type u} {commRing_1 : CommRing carrier_1},
  CommRingCat.of carrier = CommRingCat.of carrier_1 → carrier = carrier_1 ∧ commRing ≍ commRing_1
-- Init.Prelude
Applicative.mk : {f : Type u → Type v} →
  [toFunctor : Functor f] →
    [toPure : Pure f] → [toSeq : Seq f] → [toSeqLeft : SeqLeft f] → [toSeqRight : SeqRight f] → Applicative f
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- Notation for a prefunctor between reflexive quivers.  -/
CategoryTheory.ReflPrefunctor.«term_⥤rq_» : Lean.TrailingParserDescr