mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Internal.Char
_private.Std.Http.Internal.Char.0.Std.Http.Internal.Char.quotedPairChar.match_1.eq_3 : ∀ (motive : Char → Sort u_1) (x : Char) (h_1 : Unit → motive '\t') (h_2 : Unit → motive ' ')
  (h_3 : (x : Char) → motive x),
  (x = '\t' → False) →
    (x = ' ' → False) →
      (match x with
        | '\t' => h_1 ()
        | ' ' => h_2 ()
        | x => h_3 x) =
        h_3 x
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.prec.eq_1 : ∀ (f g : Turing.ToPartrec.Code),
  f.prec g =
    ((Turing.ToPartrec.Code.id.case
              (((Turing.ToPartrec.Code.tail.comp Turing.ToPartrec.Code.tail).comp
                    (Turing.ToPartrec.Code.tail.cons
                        (Turing.ToPartrec.Code.succ.cons
                          ((Turing.ToPartrec.Code.pred.comp Turing.ToPartrec.Code.tail).cons
                            ((g.comp
                                  (Turing.ToPartrec.Code.id.cons
                                    (Turing.ToPartrec.Code.tail.comp Turing.ToPartrec.Code.tail))).cons
                              (Turing.ToPartrec.Code.tail.comp
                                (Turing.ToPartrec.Code.tail.comp Turing.ToPartrec.Code.tail)))))).fix).comp
                Turing.ToPartrec.Code.zero')).comp
          (Turing.ToPartrec.Code.head.cons ((f.comp Turing.ToPartrec.Code.tail).cons Turing.ToPartrec.Code.tail))).cons
      Turing.ToPartrec.Code.nil
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.toTestFunctionClass : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] → {n : ℕ∞} → TestFunctionClass (TestFunction Ω F n) Ω F n
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Any `S`-module M is also an `R`-module via a ring homomorphism `f : R ⟶ S` by defining
`r • m := f r • m` (`Module.compHom`). This is called restriction of scalars.  -/
ModuleCat.RestrictScalars.obj' : {R : Type u₁} → {S : Type u₂} → [inst : Ring R] → [inst_1 : Ring S] → (R →+* S) → ModuleCat S → ModuleCat R
-- Std.Do.WP.SimpLemmas
Std.Do.WP.orElse_Except : ∀ {ε α : Type u_1} {x : Except ε α} {h : Unit → Except ε α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε Std.Do.PostShape.pure)},
  (Std.Do.wp (OrElse.orElse x h)).apply Q = (Std.Do.wp x).apply (Q.1, fun x => (Std.Do.wp (h ())).apply Q, Q.2.2)
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (ord : autoParam (Ord α) Std.Packages.LinearPreorderOfOrdArgs.ord._autoParam)
  (transOrd : autoParam (Std.TransOrd α) Std.Packages.LinearPreorderOfOrdArgs.transOrd._autoParam)
  (le :
    autoParam
      (let this := ord;
      LE α)
      Std.Packages.LinearPreorderOfOrdArgs.le._autoParam)
  (lawfulOrderOrd :
    autoParam
      (let this := ord;
      let this_1 := transOrd;
      let this_2 := le;
      Std.LawfulOrderOrd α)
      Std.Packages.LinearPreorderOfOrdArgs.lawfulOrderOrd._autoParam)
  (decidableLE :
    autoParam
      (let this := ord;
      let this := le;
      have this_1 := lawfulOrderOrd;
      DecidableLE α)
      Std.Packages.LinearPreorderOfOrdArgs.decidableLE._autoParam)
  (lt :
    autoParam
      (let this := ord;
      LT α)
      Std.Packages.LinearPreorderOfOrdArgs.lt._autoParam)
  (lt_iff :
    autoParam
      (let this := ord;
      let this_1 := le;
      have this_2 := lawfulOrderOrd;
      let this_3 := lt;
      ∀ (a b : α), a < b ↔ compare a b = Ordering.lt)
      Std.Packages.LinearPreorderOfOrdArgs.lt_iff._autoParam)
  (decidableLT :
    autoParam
      (let this := ord;
      let this := lt;
      let this_1 := le;
      have this_2 := lawfulOrderOrd;
      have this_3 := lt_iff;
      DecidableLT α)
      Std.Packages.LinearPreorderOfOrdArgs.decidableLT._autoParam)
  (beq :
    autoParam
      (let this := ord;
      BEq α)
      Std.Packages.LinearPreorderOfOrdArgs.beq._autoParam)
  (beq_iff :
    autoParam
      (let this := ord;
      let this_1 := le;
      have this_2 := lawfulOrderOrd;
      let this_3 := beq;
      ∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq)
      Std.Packages.LinearPreorderOfOrdArgs.beq_iff._autoParam),
  sizeOf
      { ord := ord, transOrd := transOrd, le := le, lawfulOrderOrd := lawfulOrderOrd, decidableLE := decidableLE,
        lt := lt, lt_iff := lt_iff, decidableLT := decidableLT, beq := beq, beq_iff := beq_iff } =
    1 + sizeOf ord + sizeOf transOrd + sizeOf le + sizeOf lawfulOrderOrd + sizeOf lt + sizeOf beq
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidtNormed_unit_length : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] {f : ι → E}
  (n : ι), LinearIndependent 𝕜 f → ‖InnerProductSpace.gramSchmidtNormed 𝕜 f n‖ = 1
-- Mathlib.NumberTheory.ModularForms.Derivative
/-- How `D` interacts with the slash action.  -/
Derivative.normalizedDerivOfComplex_slash : ∀ {k : ℤ} {F : UpperHalfPlane → ℂ},
  MDiff F →
    ∀ {g : GL (Fin 2) ℝ},
      0 < (↑g).det →
        Derivative.normalizedDerivOfComplex (SlashAction.map k g F) = fun z =>
          (↑(↑g).det)⁻¹ * SlashAction.map (k + 2) g (Derivative.normalizedDerivOfComplex F) z -
            ↑k * (2 * ↑Real.pi * Complex.I)⁻¹ * (↑(↑g 1 0) / UpperHalfPlane.denom g ↑z) * SlashAction.map k g F z
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.sum_add_index : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : AddCommMonoid S] (p q : SkewPolynomial R) (f : ℕ → R → S),
  (∀ (i : ℕ), f i 0 = 0) → (∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂) → (p + q).sum f = p.sum f + q.sum f
-- Init.Grind.Config
/-- A `grind` configuration that only uses `cutsat`, splitting, and the `@[lia]` lemma set.

Note: `cutsat` benefits from some amount of instantiation, e.g. `Nat.max_def`.
Lemmas tagged with the `@[lia]` attribute are instantiated via E-matching when running
`lia`, while the much larger `@[grind]` lemma set is left disabled. Tag lemmas with
`@[lia =] theorem ...` (or `attribute [lia =] ...`) to add them to this set.
 -/
Lean.Grind.CutsatConfig : Type
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.minimalPeriod_piMap_fintype : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i → α i} {x : (i : ι) → α i} [inst : Fintype ι],
  Function.minimalPeriod (Pi.map f) x = Finset.univ.lcm fun i => Function.minimalPeriod (f i) (x i)
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.mem_ofUnits_iff : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ) (x : M), x ∈ S.ofUnits ↔ ∃ y ∈ S, ↑y = x
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- Squashing at position `n + 1` and taking the tail is the same as squashing the tail of the
sequence at position `n`.  -/
GenContFract.squashSeq_succ_n_tail_eq_squashSeq_tail_n : ∀ {K : Type u_1} {n : ℕ} {s : Stream'.Seq (GenContFract.Pair K)} [inst : DivisionRing K],
  (GenContFract.squashSeq s (n + 1)).tail = GenContFract.squashSeq s.tail n
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, (m₁ \ m₂).getKeyD k fallback = if k ∈ m₂ then fallback else m₁.getKeyD k fallback
-- Mathlib.AlgebraicGeometry.Scheme
/-- Pretty printer for coercing morphisms between schemes to functions.  -/
AlgebraicGeometry.Scheme.delabCoeFunNotation : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Precomp.map_zero_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left), CategoryTheory.ComposableArrows.Precomp.map F f 0 1 ⋯ = f
-- Init.Data.List.Control
List.forM_eq_forM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m], List.forM = forM
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearMap.mdifferentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E →L[𝕜] E') {s : Set E}, MDiff[s] ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- `(F ⨿ G).obj a` is in bijection with disjoint union of `F.obj a` and `G.obj a`.  -/
CategoryTheory.FunctorToTypes.binaryCoproductEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G : CategoryTheory.Functor C (Type w)) → (a : C) → (F ⨿ G).obj a ≃ F.obj a ⊕ G.obj a
-- Mathlib.Order.Filter.Basic
/-- **Alias** of the reverse direction of `Filter.eventuallyEq_set`. -/
Filter.Eventually.set_eq : ∀ {α : Type u} {s t : Set α} {l : Filter α}, (∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t) → s =ᶠ[l] t
-- Mathlib.Data.Finset.Powerset
Finset.powersetCard_self : ∀ {α : Type u_1} (s : Finset α), Finset.powersetCard s.card s = {s}
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.δ_toSingleMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q) (n' p' : ℤ) (h' : p' + n' = q),
  CochainComplex.HomComplex.δ n n' (CochainComplex.HomComplex.Cochain.toSingleMk f h) =
    n'.negOnePow • CochainComplex.HomComplex.Cochain.toSingleMk (CategoryTheory.CategoryStruct.comp (K.d p' p) f) h'
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.norm_eq_zero_iff' : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ Set.range ⇑(NumberField.mixedEmbedding K) → (NumberField.mixedEmbedding.norm x = 0 ↔ x = 0)
-- Mathlib.LinearAlgebra.AffineSpace.Restrict
/-- An affine equivalence restricts to an affine equivalence between an affine subspace and its
image.  -/
AffineEquiv.affineSubspaceMap : {k : Type u_1} →
  {V₁ : Type u_2} →
    {P₁ : Type u_3} →
      {V₂ : Type u_4} →
        {P₂ : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] →
                      [inst_6 : AddTorsor V₂ P₂] →
                        (e : P₁ ≃ᵃ[k] P₂) →
                          (s : AffineSubspace k P₁) → [inst_7 : Nonempty ↥s] → ↥s ≃ᵃ[k] ↥(AffineSubspace.map (↑e) s)
-- Mathlib.Order.Atoms
IsAtom.of_isAtom_coe_Iic : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderBot α] {x : α} {a : ↑(Set.Iic x)}, IsAtom a → IsAtom ↑a
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (arrows arrows_1 : (c d : C) → Set (c ⟶ d))
  (e_arrows : arrows = arrows_1)
  (inv : ∀ {c d : C} {p : c ⟶ d}, p ∈ arrows c d → CategoryTheory.Groupoid.inv p ∈ arrows d c)
  (mul :
    ∀ {c d e : C} {p : c ⟶ d},
      p ∈ arrows c d → ∀ {q : d ⟶ e}, q ∈ arrows d e → CategoryTheory.CategoryStruct.comp p q ∈ arrows c e),
  { arrows := arrows, inv := inv, mul := mul } = { arrows := arrows_1, inv := ⋯, mul := ⋯ }
-- Mathlib.Data.Fin.Fin2
/-- `left k` is the embedding `Fin2 n → Fin2 (k + n)`  -/
Fin2.left : (k : ℕ) → {n : ℕ} → Fin2 n → Fin2 (k + n)
-- Mathlib.Combinatorics.SimpleGraph.Dart
/-- The edge associated to the dart.  -/
SimpleGraph.Dart.edge : {V : Type u_1} → {G : SimpleGraph V} → G.Dart → Sym2 V
-- Mathlib.LinearAlgebra.Basis.Cardinality
_private.Mathlib.LinearAlgebra.Basis.Cardinality.0.Option.elim.match_1.eq_2 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Option α → β → (α → β) → Sort u_2) (y : β) (x : α → β)
  (h_1 : (x : α) → (x_1 : β) → (f : α → β) → motive (some x) x_1 f) (h_2 : (y : β) → (x : α → β) → motive none y x),
  (match none, y, x with
    | some x, x_1, f => h_1 x x_1 f
    | none, y, x => h_2 y x) =
    h_2 y x
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.elabResetGrindAttrs : Lean.Elab.Command.CommandElab
-- Init.System.IO
IO.FS.instReprMetadata.repr : IO.FS.Metadata → ℕ → Std.Format
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.val_comp_inclusion : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A}
  (hst : S ≤ T), T.val.comp (Subalgebra.inclusion hst) = S.val
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.linearOrder : LinearOrder Cardinal.{u}
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the reverse direction of `uniqueMDiffOn_iff_uniqueDiffOn`. -/
UniqueDiffOn.uniqueMDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, UniqueDiffOn 𝕜 s → UniqueMDiff[s]
-- Init.Grind.ToInt
Lean.Grind.IntInterval.nonEmpty.eq_2 : ∀ (lo : ℤ), (Lean.Grind.IntInterval.ci lo).nonEmpty = true
-- Mathlib.CategoryTheory.Monoidal.Functor.Types
CategoryTheory.μ_def : ∀ (F : Type u_1 → Type u_2) [inst : Applicative F] [inst_1 : LawfulApplicative F] (x x_1 : Type u_1),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.ofTypeFunctor F) x x_1 =
    TypeCat.ofHom fun p => Prod.mk <$> p.1 <*> p.2
-- Lean.Compiler.InlineAttrs
/-- This is an approximate test for testing whether `declName` can be annotated with the `[macro_inline]` attribute or not.
 -/
_private.Lean.Compiler.InlineAttrs.0.Lean.Compiler.isValidMacroInline : Lean.Name → Lean.CoreM Bool
-- Mathlib.Computability.DFA
DFA.comap_id : ∀ {α : Type u} {σ : Type v} (M : DFA α σ), DFA.comap id M = M
-- Init.System.Platform
System.Platform.System.Platform.numBits_dvd : System.Platform.numBits ∣ 64
-- Aesop.Stats.Basic
Aesop.ForwardClusterStateStats.mk : ℕ → Array Aesop.ForwardInstantiationStats → Aesop.ForwardClusterStateStats
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_smul : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) (r : NNReal),
  (r • μ).singularPart ν = r • μ.singularPart ν
-- Lean.Parser.Attr
Lean.Parser.Attr.specialize.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_eq_some_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.maxKey? = some (t.maxKeyD fallback)
-- Lean.Util.CollectLooseBVars
Lean.Expr.CollectLooseBVars.State.bvars : Lean.Expr.CollectLooseBVars.State → Std.HashSet ℕ
-- Init.Data.Array.Perm
Array.Perm.toList : ∀ {α : Type u_1} {as bs : Array α}, as.Perm bs → as.toList.Perm bs.toList
-- Mathlib.Analysis.MeanInequalities
/-- **AM-GM inequality - strict inequality condition**.
The condition is that not all elements of `z` with a nonzero weight are equal to their center of
mass `∑ i ∈ s, w i * z i`; see `geom_mean_lt_arith_mean_weighted_iff_of_nonneg` for a version that
compares the elements to each other instead.  -/
Real.geom_mean_lt_arith_mean_weighted_iff_of_nonneg' : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 ≤ w i) →
    ∑ i ∈ s, w i = 1 →
      (∀ i ∈ s, 0 ≤ z i) → (∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i ↔ ∃ j ∈ s, w j ≠ 0 ∧ z j ≠ ∑ i ∈ s, w i * z i)
-- Batteries.Data.List.Perm
List.Subperm.idxInj_inj : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : List α} {h : xs.Subperm ys} (i j : Fin xs.length),
  h.idxInj i = h.idxInj j ↔ i = j
-- Init.Data.SInt.Float
/-- Obtains the `Float` whose value is the same as the given `Int16`.

This function does not reduce in the kernel.
 -/
Int16.toFloat : Int16 → Float
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C}
  (h_1 : X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p₁₃ (CategoryTheory.CategoryStruct.comp h₁₃.p₁ h_1) =
    CategoryTheory.CategoryStruct.comp h.p₁ h_1
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- If `α` is complete, then it is an abstract completion of itself.  -/
AbstractCompletion.ofComplete : {α : Type uα} → [inst : UniformSpace α] → [T0Space α] → [CompleteSpace α] → AbstractCompletion.{uα, uα} α
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMapClass.map_smul_of_tower : ∀ {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 : Type u_16} [LinearMap.CompatibleSMul M M₂ R S] [inst_8 : FunLike F M M₂] [LinearMapClass F S M M₂] (fₗ : F)
  (c : R) (x : M), fₗ (c • x) = c • fₗ x
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Relation.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {S : J.Cover X} → {fst snd : S.Arrow} → fst.Relation snd → S.Relation
-- Mathlib.RingTheory.PowerSeries.Log
PowerSeries.coeff_one_log : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A], (PowerSeries.coeff 1) (PowerSeries.log A) = 1
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {A B : CategoryTheory.Mon C} → CategoryTheory.Category.{v₁, max u₁ v₁} (Bimod A B)
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.finCategoryWidePullback : {J : Type v} → [Fintype J] → CategoryTheory.FinCategory (CategoryTheory.Limits.WidePullbackShape J)
-- Mathlib.Topology.Algebra.Monoid
nhds_zero_add_nhds : ∀ {M : Type u_6} [inst : AddZeroClass M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] (a : M),
  nhds 0 + nhds a = nhds a
-- Mathlib.Order.Fin.Basic
Fin.addNatOrderEmb_toEmbedding : ∀ {n : ℕ} (m : ℕ), (Fin.addNatOrderEmb m).toEmbedding = { toFun := fun x => x.addNat m, inj' := ⋯ }
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.coe_one : ∀ {α : Type u_1} [inst : One α], ↑1 = 1
-- Mathlib.Order.WithBot
WithBot.LE.coe_le_coe : ∀ {α : Type u_1} [inst : LE α] {a b : α}, a ≤ b → (↑a).LE ↑b
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Connected.dist_eq_zero_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.Connected → (G.dist u v = 0 ↔ u = v)
-- Init.Data.UInt.Bitwise
UInt64.toUSize_shiftLeft : ∀ (a b : UInt64), b.toNat < System.Platform.numBits → (a <<< b).toUSize = a.toUSize <<< b.toUSize
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.isRoot_root : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R), (Polynomial.map (AdjoinRoot.of f) f).IsRoot (AdjoinRoot.root f)
-- Std.Http.Internal.ChunkedBuffer
Std.Http.Internal.ChunkedBuffer.instInhabited : Inhabited Std.Http.Internal.ChunkedBuffer
-- Std.Time.DateTime
/-- Add `Millisecond.Offset` to a `DateTime`.
 -/
Std.Time.DateTime.addMilliseconds : Std.Time.DateTime → Std.Time.Millisecond.Offset → Std.Time.DateTime
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
fderiv_clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {H : Type u_5} [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {d : E → F →L[𝕜] G},
  DifferentiableAt 𝕜 c x →
    DifferentiableAt 𝕜 d x →
      fderiv 𝕜 (fun y => c y ∘SL d y) x =
        (ContinuousLinearMap.compL 𝕜 F G H) (c x) ∘SL fderiv 𝕜 d x +
          (ContinuousLinearMap.compL 𝕜 F G H).flip (d x) ∘SL fderiv 𝕜 c x
-- Mathlib.Order.CompleteLattice.Defs
CompleteLinearOrder.toBiheytingAlgebra : {α : Type u_8} → [self : CompleteLinearOrder α] → BiheytingAlgebra α
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.image_of_comp : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {ι : Type u_3}
  {ι' : Type u_4} (s : Set ι) (f : ι → ι') (g : ι' → A),
  (AlgebraicIndependent R fun x => g (f ↑x)) → AlgebraicIndependent R fun x => g ↑x
-- Mathlib.CategoryTheory.Subobject.Limits
/-- Taking kernels is an order-reversing map from the quotient objects of `X` to the subobjects of
`X`.  -/
CategoryTheory.Limits.kernelOrderHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasKernels C] →
        (X : C) → (CategoryTheory.Subobject (Opposite.op X))ᵒᵈ →o CategoryTheory.Subobject X
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.num_add : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜] (c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x),
  ↑(c1 + c2).num = ↑c1.den * ↑c2.num + ↑c2.den * ↑c1.num
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.prod_symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β × γ → α},
  Multipliable f → Multipliable fun p => f p.swap
-- Mathlib.Algebra.Ring.Rat
Rat.den_mul_eq_num : ∀ (q : ℚ), ↑q.den * q = ↑q.num
-- Mathlib.Algebra.Order.Ring.Idempotent
instSemilatticeInfSubtypeIsIdempotentElem : {S : Type u_2} → [inst : CommSemigroup S] → SemilatticeInf { a // IsIdempotentElem a }
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (Set.Ioc b a).OrdConnected
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryProductTriangle_obj₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryProduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryProductTriangle X₁ X₂).obj₂ = (X₁ ⨯ X₂)
-- Mathlib.Topology.OmegaCompletePartialOrder
Scott.IsOpen.isUpperSet : ∀ (α : Type u) [inst : OmegaCompletePartialOrder α] {s : Set α}, Scott.IsOpen α s → IsUpperSet s
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.prod_source : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  [inst_5 : (x : B) → Zero (E₁ x)] [inst_6 : (x : B) → Zero (E₂ x)],
  (e₁.prod e₂).source = Bundle.TotalSpace.proj ⁻¹' e₁.baseSet ∩ Bundle.TotalSpace.proj ⁻¹' e₂.baseSet
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- We say a measurable space is countably generated
if it can be generated by a countable set of sets.  -/
MeasurableSpace.CountablyGenerated : (α : Type u_3) → [m : MeasurableSpace α] → Prop
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.LinearWeights.map_add : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  {inst_3 : AddCommGroup M} {inst_4 : Module R M} {inst_5 : LieRingModule L M} {inst_6 : LieModule R L M}
  {inst_7 : LieRing.IsNilpotent L} [self : LieModule.LinearWeights R L M] (χ : L → R),
  LieModule.genWeightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y