mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {A : C} (toPrepathObject : HomotopicalAlgebra.PrepathObject A)
  (weakEquivalence_ι :
    autoParam (HomotopicalAlgebra.WeakEquivalence toPrepathObject.ι)
      HomotopicalAlgebra.PathObject.weakEquivalence_ι._autoParam)
  (toPrepathObject_1 : HomotopicalAlgebra.PrepathObject A)
  (weakEquivalence_ι_1 :
    autoParam (HomotopicalAlgebra.WeakEquivalence toPrepathObject_1.ι)
      HomotopicalAlgebra.PathObject.weakEquivalence_ι._autoParam),
  ({ toPrepathObject := toPrepathObject, weakEquivalence_ι := weakEquivalence_ι } =
      { toPrepathObject := toPrepathObject_1, weakEquivalence_ι := weakEquivalence_ι_1 }) =
    (toPrepathObject = toPrepathObject_1)
-- Std.Http.Data.Headers.Basic
/-- The `Connection` header, represented as a list of connection option tokens.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-connection
 -/
Std.Http.Header.Connection : Type
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.Type₁.mk.inj : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d + 1} {index : Fin (d + 1)} {isIndex : SSet.prodStdSimplex.pairingCore.IsIndex x hd index.succ}
  {x_1 : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d_1 : ℕ} {hd_1 : x_1.dim = d_1 + 1}
  {index_1 : Fin (d_1 + 1)} {isIndex_1 : SSet.prodStdSimplex.pairingCore.IsIndex x_1 hd_1 index_1.succ},
  { x := x, d := d, hd := hd, index := index, isIndex := isIndex } =
      { x := x_1, d := d_1, hd := hd_1, index := index_1, isIndex := isIndex_1 } →
    x = x_1 ∧ d = d_1 ∧ index ≍ index_1
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- *Dirichlet's approximation theorem:*
For any real number `ξ` and positive natural `n`, there is a natural number `k`,
with `0 < k ≤ n` such that `|k*ξ - round(k*ξ)| ≤ 1/(n+1)`.
 -/
Real.exists_nat_abs_mul_sub_round_le : ∀ (ξ : ℝ) {n : ℕ}, 0 < n → ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)
-- Mathlib.Data.List.Permutation
/-- The `r` argument to `permutationsAux2` is the same as appending.  -/
List.permutationsAux2_append : ∀ {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (ys : List α) (f : List α → β),
  (List.permutationsAux2 t ts [] ys f).2 ++ r = (List.permutationsAux2 t ts r ys f).2
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.ofEq_h : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  (h : f = g),
  (SSet.RelativeMorphism.Homotopy.ofEq h).h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X (SSet.stdSimplex.obj { len := 1 })) f.map
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_add_add_eq_append : ∀ {m n : ℕ}, (*...m + n).toList = (*...m).toList ++ (m...m + n).toList
-- Init.Data.BitVec.Lemmas
/-- When `r < w`, we give a formula for `(x.rotateLeft r).getLsbD i`.  -/
BitVec.getLsbD_rotateLeft_of_le : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ},
  r < w →
    (x.rotateLeft r).getLsbD i = bif decide (i < r) then x.getLsbD (w - r + i) else decide (i < w) && x.getLsbD (i - r)
-- Mathlib.Data.Prod.Basic
Prod.swap_bijective : ∀ {α : Type u_1} {β : Type u_2}, Function.Bijective Prod.swap
-- Mathlib.Topology.Convenient.HomSpace
/-- The evaluation `Y × ContinuousMapGeneratedBy X Y Z → Z` as a `X`-continuous map.  -/
Topology.ContinuousMapGeneratedBy.ev : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} →
        [inst_1 : TopologicalSpace Y] →
          {Z : Type v'} →
            [inst_2 : TopologicalSpace Z] →
              [∀ (i : ι), LocallyCompactSpace (X i)] →
                [∀ (i j : ι), Topology.IsGeneratedBy X (X i × X j)] →
                  Topology.ContinuousMapGeneratedBy X (Y × Topology.ContinuousMapGeneratedBy X Y Z) Z
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.instAddSemigroup : {α : Type u} → [inst : Add α] → AddSemigroup (AddMagma.FreeAddSemigroup α)
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Icc_right : ∀ {α : Type v} [inst : Preorder α] (a : α), ⋃ b, Set.Icc a b = Set.Ici a
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.secondCountableTopology_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) [SecondCountableTopology Y], SecondCountableTopology ↑e.source
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.strongEpiCategory_of_regularEpiCategory : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsRegularEpiCategory C],
  CategoryTheory.StrongEpiCategory C
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndinter_subset_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s.ndinter t ⊆ t
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.BinaryCofan.mono_inr_of_isVanKampen : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] {X Y : C}
  {c : CategoryTheory.Limits.BinaryCofan X Y}, CategoryTheory.IsVanKampenColimit c → CategoryTheory.Mono c.inr
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitIsoFlipCompLim_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (X : K),
  (CategoryTheory.Limits.limitIsoFlipCompLim F).inv.app X =
    (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F X).inv
-- Lean.Meta.SynthInstance
/-- Try the next instance in the node on the top of the generator stack.  -/
Lean.Meta.SynthInstance.generate : Lean.Meta.SynthInstance.SynthM Unit
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Slice.slice!.eq_1 : ∀ (s : String.Slice) (newStart newEnd : s.Pos),
  s.slice! newStart newEnd =
    if h : newStart ≤ newEnd then s.slice newStart newEnd h
    else
      panicWithPosWithDecl "Init.Data.String.Basic" "String.Slice.slice!" 1096 4
        "Starting position must be less than or equal to end position."
-- Mathlib.Data.Finset.Lattice.Basic
Finset.instDistribLattice : {α : Type u_1} → [DecidableEq α] → DistribLattice (Finset α)
-- Lean.Parser.Extension
Lean.Parser.parserExtension : Lean.Parser.ParserExtension
-- Mathlib.Data.Finset.NatDivisors
/-- The divisors of a product of natural numbers are the pointwise product of the divisors of the
factors.  -/
Nat.divisors_mul : ∀ (m n : ℕ), (m * n).divisors = m.divisors * n.divisors
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result.ematchDiags : Lean.Meta.Grind.Result → Lean.PArray Lean.Meta.Grind.EMatchDiagInfo
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.of_preimage : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β}, (f ⁻¹' s).Finite → Function.Surjective f → s.Finite
-- Mathlib.Probability.Moments.ComplexMGF
ProbabilityTheory.complexMGF.eq_1 : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) (z : ℂ),
  ProbabilityTheory.complexMGF X μ z = ∫ (ω : Ω), Complex.exp (z * ↑(X ω)) ∂μ
-- Mathlib.Order.SuccPred.Limit
Order.mem_range_succ_or_isSuccPrelimit : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] (a : α),
  a ∈ Set.range Order.succ ∨ Order.IsSuccPrelimit a
-- Std.Time.Format.Modifier
Std.Time.Modifier.v.injEq : ∀ (presentation presentation_1 : Std.Time.ZoneName),
  (Std.Time.Modifier.v presentation = Std.Time.Modifier.v presentation_1) = (presentation = presentation_1)
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_union : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s₁ s₂ : Finset β}
  {f : β → α} [inst_2 : DecidableEq β], (s₁ ∪ s₂).lcm f = lcm (s₁.lcm f) (s₂.lcm f)
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- If `f` admits a Taylor series `p` in a set `s`, and `g` is linear, then `g ∘ f` admits a Taylor
series whose `k`-th term is given by `g ∘ (p k)`.  -/
HasFTaylorSeriesUpToOn.continuousLinearMap_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F}
  {p : E → FormalMultilinearSeries 𝕜 E F} {n : WithTop ℕ∞} (g : F →L[𝕜] G),
  HasFTaylorSeriesUpToOn n f p s →
    HasFTaylorSeriesUpToOn n (⇑g ∘ f) (fun x k => g.compContinuousMultilinearMap (p x k)) s
-- Mathlib.Order.Interval.Set.Basic
Set.subsingleton_Icc_iff : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (Set.Icc a b).Subsingleton ↔ b ≤ a
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_ofLp : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] (f : PiLp ⊤ β),
  ‖f.ofLp‖ = ‖f‖
-- Mathlib.Tactic.Determinant.Bird.Meta
Mathlib.Tactic.Determinant.Ctx.mk.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)}
  {cα : Mathlib.Tactic.Ring.Common.Cache (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα)}
  {rc :
    Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.RatCoeff
      (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα)}
  {dimension : ℕ} {dimensionLit : Q(ℕ)} {arrayExpr : Q(Array «$α»)} {arrayEntries : Array Q(«$α»)}
  {cα_1 : Mathlib.Tactic.Ring.Common.Cache (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα)}
  {rc_1 :
    Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.RatCoeff
      (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα)}
  {dimension_1 : ℕ} {dimensionLit_1 : Q(ℕ)} {arrayExpr_1 : Q(Array «$α»)} {arrayEntries_1 : Array Q(«$α»)},
  { cα := cα, rc := rc, dimension := dimension, dimensionLit := dimensionLit, arrayExpr := arrayExpr,
        arrayEntries := arrayEntries } =
      { cα := cα_1, rc := rc_1, dimension := dimension_1, dimensionLit := dimensionLit_1, arrayExpr := arrayExpr_1,
        arrayEntries := arrayEntries_1 } →
    cα = cα_1 ∧
      rc = rc_1 ∧
        dimension = dimension_1 ∧
          dimensionLit = dimensionLit_1 ∧ arrayExpr = arrayExpr_1 ∧ arrayEntries = arrayEntries_1
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
Finpartition.coe_energy : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) (G : SimpleGraph α)
  [inst_1 : DecidableRel G.Adj] {𝕜 : Type u_2} [inst_2 : Field 𝕜] [inst_3 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜],
  ↑(P.energy G) = (∑ uv ∈ P.parts.offDiag, ↑(G.edgeDensity uv.1 uv.2) ^ 2) / ↑P.parts.card ^ 2
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
/-- The isomorphism of categories of bifunctors given by flipping the arguments.  -/
CategoryTheory.flippingIso : {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.Cat.of (CategoryTheory.Functor C (CategoryTheory.Functor D E)) ≅
              CategoryTheory.Cat.of (CategoryTheory.Functor D (CategoryTheory.Functor C E))
-- Init.Data.String.Termination
/-- The number of bytes between `p` and the end position. This number decreases as `p` advances.  -/
String.Pos.remainingBytes : {s : String} → s.Pos → ℕ
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.instInhabitedPresieve : {C : Type u_1} → [inst : CategoryTheory.Category.{u_2, u_1} C] → (X : C) → Inhabited (CategoryTheory.Presieve X)
-- Batteries.Tactic.Trans
/-- solving `tgt ← mkAppM' rel #[x, z]` given `tgt = f z`  -/
Batteries.Tactic.getExplicitRelArg? : Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
MulAction.isMultiplyPreprimitive_congr : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {N : Type u_3} {β : Type u_4}
  [inst_2 : Group N] [inst_3 : MulAction N β] {φ : M → N},
  Function.Surjective φ →
    ∀ {f : α →ₑ[φ] β},
      Function.Bijective ⇑f → ∀ {n : ℕ}, MulAction.IsMultiplyPreprimitive M α n ↔ MulAction.IsMultiplyPreprimitive N β n
-- Mathlib.Topology.ContinuousMap.Algebra
AddMonoidHom.compLeftContinuous_apply : ∀ (α : Type u_1) {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {γ : Type u_3}
  [inst_2 : AddMonoid β] [inst_3 : ContinuousAdd β] [inst_4 : TopologicalSpace γ] [inst_5 : AddMonoid γ]
  [inst_6 : ContinuousAdd γ] (g : β →+ γ) (hg : Continuous ⇑g) (f : C(α, β)),
  (AddMonoidHom.compLeftContinuous α g hg) f = { toFun := ⇑g, continuous_toFun := hg }.comp f
-- Mathlib.Analysis.Convex.Star
/-- The translation of a star-convex set is also star-convex.  -/
StarConvex.preimage_add_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {x z : E} {s : Set E}, StarConvex 𝕜 (x + z) s → StarConvex 𝕜 x ((fun x => x + z) ⁻¹' s)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabRoi : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_div_div : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Div β] [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.IndepFun (f i / f j) (f k / f l) μ
-- Mathlib.Analysis.Complex.Poisson
poissonKernel_def : ∀ (c w z : ℂ), poissonKernel c w z = (‖z - c‖ ^ 2 - ‖w - c‖ ^ 2) / ‖z - c - (w - c)‖ ^ 2
-- Mathlib.Analysis.Meromorphic.Basic
meromorphicAt_smul_iff_of_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {g : 𝕜 → 𝕜} {x : 𝕜} {f : 𝕜 → E},
  AnalyticAt 𝕜 g x → g x ≠ 0 → (MeromorphicAt (g • f) x ↔ MeromorphicAt f x)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.sign_signedInfDist_touchpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ {i j : Fin (n + 1)},
      i ≠ j →
        SignType.sign ((s.signedInfDist j) (s.touchpoint signs i)) =
          SignType.sign ((s.signedInfDist j) (s.excenter signs))
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getCast!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) [inst_2 : Inhabited (β a)] (a_1 : α)
  (b : β a_1) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getCast! a (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    if h : (a_1 == a) = true then cast ⋯ b else Std.DHashMap.Internal.AssocList.getCast! a es
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.isoOfIsAffine.congr_simp : ∀ (n : Type u) (S : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine S],
  AlgebraicGeometry.AffineSpace.isoOfIsAffine n S = AlgebraicGeometry.AffineSpace.isoOfIsAffine n S
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- The limit of a diagram `F : J ⥤ K ⥤ C` is isomorphic to the functor given by
the individual limits on objects.  -/
CategoryTheory.Limits.limitIsoFlipCompLim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] →
              (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
                CategoryTheory.Limits.limit F ≅ F.flip.comp CategoryTheory.Limits.lim
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_add_le_of_degree_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} {n : ℕ}, p.degree ≤ ↑n → q.degree ≤ ↑n → (p + q).degree ≤ ↑n
-- Mathlib.Order.CompleteLattice.Finset
Set.iUnion_finset_eq_set : ∀ {ι : Type u_5} (s : Set ι), ⋃ s', Subtype.val '' ↑s' = s
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.ext : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x y : MvQPF.Cofix F α),
  x.dest = y.dest → x = y
-- Mathlib.RingTheory.Derivation.Lie
Derivation.Compatible.mem : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {A' : Type u_3}
  [inst_3 : CommRing A'] [inst_4 : Algebra R A'] [inst_5 : Algebra A A'] [inst_6 : IsScalarTower R A A']
  (x : Derivation R A' A' × Derivation R A A),
  x ∈ Derivation.couple R A A' ↔ ⇑x.1 ∘ ⇑(Algebra.ofId A A') = ⇑(Algebra.ofId A A') ∘ ⇑x.2
-- Mathlib.Algebra.GradedMonoid
/-- If all grades are the same type and themselves form a commutative monoid, then there is a
trivial grading structure.  -/
CommMonoid.gCommMonoid : (ι : Type u_1) → {R : Type u_2} → [inst : AddCommMonoid ι] → [CommMonoid R] → GradedMonoid.GCommMonoid fun x => R
-- Init.System.ST
/-- Reads the value of a mutable reference cell, removing it.

This causes subsequent attempts to read from or take the reference cell to block until a new value
is written using `ST.Ref.set`.
 -/
ST.Ref.take : {σ : Type} → {m : Type → Type} → [MonadLiftT (ST σ) m] → {α : Type} → ST.Ref σ α → m α
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instContMDiffInv₀OfTopWithTopENat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G] {a : WithTop ℕ∞}
  [ContMDiffInv₀ I ⊤ G], ContMDiffInv₀ I a G
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.disjoint_closedEBall_of_lt_infEDist`. -/
EMetric.disjoint_closedBall_of_lt_infEdist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α} {r : ENNReal},
  r < Metric.infEDist x s → Disjoint (Metric.closedEBall x r) s
-- Mathlib.Data.FunLike.Group
FunLike.coeAddHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [inst_3 : IsAddApply F α β] (f : F), (FunLike.coeAddHom F α β) f = ⇑f
-- Aesop.Forward.State
/-- The pattern substitutions present in the rule states. Invariant:
`patSubsts` maps the source `s` to a rule name `r` and pattern substitution `i`
iff the rule state of `r` contains `i` with source `s`.  -/
Aesop.ForwardState.patSubsts : Aesop.ForwardState → Lean.PHashMap Aesop.PatSubstSource (Lean.PArray (Aesop.RuleName × Aesop.Substitution))
-- Init.Data.Vector.Basic
/-- The vector of length `n` whose `i`-th element is `f i`.  -/
Vector.ofFn : {n : ℕ} → {α : Type u_1} → (Fin n → α) → Vector α n
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.eq_re_of_eq_coe : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : CommRing R] {a : QuaternionAlgebra R c₁ c₂ c₃} {x : R}, a = ↑x → a = ↑a.re
-- Mathlib.Data.Multiset.Defs
Multiset.decidableDexistsMultiset : {α : Type u_1} →
  {m : Multiset α} →
    {p : (a : α) → a ∈ m → Prop} →
      [_hp : (a : α) → (h : a ∈ m) → Decidable (p a h)] → Decidable (∃ a, ∃ (h : a ∈ m), p a h)
-- Init.Data.List.Find
List.findFinIdx?_append : ∀ {α : Type u_1} {xs ys : List α} {p : α → Bool},
  List.findFinIdx? p (xs ++ ys) =
    (Option.map (Fin.castLE ⋯) (List.findFinIdx? p xs)).or
      (Option.map (Fin.cast ⋯) (Option.map (Fin.natAdd xs.length) (List.findFinIdx? p ys)))
-- Aesop.Tree.Data
Aesop.Rapp.setMetaState : Lean.Meta.SavedState → Aesop.Rapp → Aesop.Rapp
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_add : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p x y : 𝕜), ↑(x + y) = ↑x + ↑y
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_union_of_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∉ t₂) → (t₁ ∪ t₂).size = t₁.size + t₂.size
-- Init.Data.Array.Erase
Array.eraseP_replicate_of_neg : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {a : α}, ¬p a = true → (Array.replicate n a).eraseP p = Array.replicate n a
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.AutGalois.π_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F)
  (x : CategoryTheory.PreGaloisCategory.AutGalois F), (CategoryTheory.PreGaloisCategory.AutGalois.π F A) x = ↑x A
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.congr_symm : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  {S : Type u_3} [inst_2 : Ring S] {Λ₀ : Type u_4} [inst_3 : LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀)
  (f : R ≃+* S), (WithVal.congr v w f).symm = WithVal.congr w v f.symm
-- Mathlib.ModelTheory.Skolem
FirstOrder.Language.skolem₁_Relations : ∀ (L : FirstOrder.Language) (x : ℕ), L.skolem₁.Relations x = Empty
-- Mathlib.Analysis.CStarAlgebra.Classes
instCommCStarAlgebraProd : {A : Type u_1} → {B : Type u_2} → [CommCStarAlgebra A] → [CommCStarAlgebra B] → CommCStarAlgebra (A × B)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit!_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t.WF →
    ∀ {l : List α} {k fallback : α},
      k ∈ t → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.RingTheory.KrullDimension.NonZeroDivisors
/-- If `R →+* S` is surjective whose kernel contains a nonzero divisor, then `dim S + 1 ≤ dim R`.  -/
ringKrullDim_succ_le_of_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  Function.Surjective ⇑f → ∀ {r : R}, r ∈ nonZeroDivisors R → f r = 0 → ringKrullDim S + 1 ≤ ringKrullDim R
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.endPos_cast : ∀ {s t : String.Slice} (hst : s.copy = t.copy) {st : String.Slice.Pattern.SearchStep s},
  (String.Slice.Pattern.SearchStep.cast hst st).endPos = st.endPos.cast hst
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.SmoothOfRelativeDimension.mk : ∀ {n : ℕ} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (∀ (x : ↥X),
      ∃ U,
        ∃ (_ : AlgebraicGeometry.IsAffineOpen U),
          ∃ V,
            ∃ (_ : AlgebraicGeometry.IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              RingHom.IsStandardSmoothOfRelativeDimension n
                (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e))) →
    AlgebraicGeometry.SmoothOfRelativeDimension n f
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_natAdd_Iic_natAdd : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Fin.natAdd m ⁻¹' Set.Iic (Fin.natAdd m i) = Set.Iic i
-- Mathlib.Algebra.Field.Basic
self_eq_inv₀ : ∀ {K : Type u_1} [inst : DivisionRing K] {a : K}, a = a⁻¹ ↔ a = -1 ∨ a = 0 ∨ a = 1
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.WalkingParallelFamily.zero.sizeOf_spec : ∀ {J : Type w} [inst : SizeOf J], sizeOf CategoryTheory.Limits.WalkingParallelFamily.zero = 1
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.memP_iff_lowerBoundP? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut], RBTree.RBSet.MemP cut t ↔ ∃ x, t.lowerBoundP? cut = some x ∧ cut x = Ordering.eq
-- Mathlib.Data.List.AList
/-- Fold a function over the key-value pairs in the map.  -/
AList.foldl : {α : Type u} → {β : α → Type v} → {δ : Type w} → (δ → (a : α) → β a → δ) → δ → AList β → δ