mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_comp_const_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {s : Set 𝕜} {f : 𝕜 → F} (c : 𝕜),
  iteratedDerivWithin n (fun z => f (c - z)) s = fun x => (-1) ^ n • iteratedDerivWithin n f (c +ᵥ -s) (c - x)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_pi : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → Inv (α i)] (s : Set ι) (t : (i : ι) → Set (α i)),
  (s.pi t)⁻¹ = s.pi fun i => (t i)⁻¹
-- Mathlib.Algebra.Ring.Int.Field
/-- `ℤ` with its usual ring structure is not a field.  -/
Int.not_isField : ¬IsField ℤ
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.toReal_laverage : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → (∀ᵐ (x : α) ∂μ, f x ≠ ⊤) → (⨍⁻ (x : α), f x ∂μ).toReal = ⨍ (x : α), (f x).toReal ∂μ
-- Mathlib.Computability.Primrec.List
Primcodable.vector : {α : Type u_1} → [Primcodable α] → {n : ℕ} → Primcodable (List.Vector α n)
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearMap.transvection.det : ∀ {R : Type u_3} {V : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] [Module.Free R V]
  [Module.Finite R V] (f : Module.Dual R V) (v : V), LinearMap.det (LinearMap.transvection f v) = 1 + f v
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote'.go.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α) (r : α)
  (v : Lean.Grind.Linarith.Var) (p_2 : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.Poly.denote'.go ctx r (Lean.Grind.Linarith.Poly.add 1 v p_2) =
    Lean.Grind.Linarith.Poly.denote'.go ctx (r + Lean.Grind.Linarith.Var.denote ctx v) p_2
-- Init.Data.Int.Gcd
Int.gcd_mul_left_left_of_gcd_eq_one : ∀ {n m k : ℤ}, n.gcd m = 1 → (k * n).gcd m = k.gcd m
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.sigmoid_inj : ∀ {a b : ℝ}, unitInterval.sigmoid a = unitInterval.sigmoid b ↔ a = b
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_mono : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8}
  [inst : NormedAddCommGroup G''] [inst_1 : PartialOrder G''] [IsOrderedAddMonoid G''] [inst_3 : NormedSpace ℝ G'']
  [inst_4 : CompleteSpace G''] [inst_5 : NormedAddCommGroup G'] [inst_6 : PartialOrder G'] [inst_7 : NormedSpace ℝ G']
  [ClosedIciTopology G''] [IsOrderedAddMonoid G'] {T : Set α → G' →L[ℝ] G''} {C : ℝ}
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) →
    ∀ {f g : ↥(MeasureTheory.Lp G' 1 μ)}, f ≤ g → (MeasureTheory.L1.setToL1 hT) f ≤ (MeasureTheory.L1.setToL1 hT) g
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor_map_right_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  (CategoryTheory.Square.toArrowArrowFunctor.map φ).right.right = φ.τ₄
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.setBody : Lean.IR.Alt → Lean.IR.FnBody → Lean.IR.Alt
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.rel_of_zero_of_inner : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  {it it' : Std.IterM m β} (h : it.internalState.countdown = 0),
  it'.internalState.countdown = 0 →
    it'.internalState.inner.finitelyManySteps.Rel it.internalState.inner.finitelyManySteps →
      Std.Iterators.Types.Take.Rel m it' it
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.Λ'.normal : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → Λ → Turing.TM1to1.Λ' Γ Λ σ
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.intervalIntegral_tendsto_integral_Ioi : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {b : ι → ℝ} {f : ℝ → E} (a : ℝ),
  MeasureTheory.IntegrableOn f (Set.Ioi a) μ →
    Filter.Tendsto b l Filter.atTop →
      Filter.Tendsto (fun i => ∫ (x : ℝ) in a..b i, f x ∂μ) l (nhds (∫ (x : ℝ) in Set.Ioi a, f x ∂μ))
-- Init.Data.SInt.Basic
/-- The modulo operator for 16-bit signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by `Int16.div`. Usually accessed via the `%`
operator.

When the divisor is `0`, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int16.mod 5 2 = 1`
* `Int16.mod 5 (-2) = 1`
* `Int16.mod (-5) 2 = (-1)`
* `Int16.mod (-5) (-2) = (-1)`
* `Int16.mod 4 2 = 0`
* `Int16.mod 4 (-2) = 0`
* `Int16.mod 4 0 = 4`
* `Int16.mod (-4) 0 = (-4)`
 -/
Int16.mod : Int16 → Int16 → Int16
-- Mathlib.CategoryTheory.Galois.Action
CategoryTheory.PreGaloisCategory.instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.PreGaloisCategory.PreservesIsConnected (CategoryTheory.PreGaloisCategory.functorToAction F)
-- Mathlib.Order.Category.PartOrd
_private.Mathlib.Order.Category.PartOrd.0.PartOrd.Hom.mk.inj : ∀ {X Y : PartOrd} {hom' hom'_1 : ↑X →o ↑Y}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.NumberTheory.FunctionField
FunctionField.instFiniteDimensionalRatFuncSubtypeMemIntermediateField : ∀ {F : Type u_1} (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (Polynomial F) K]
  [inst_3 : FaithfulSMul (Polynomial F) K] [FunctionField F K] [inst_5 : Algebra F K] (E : IntermediateField F K)
  [inst_6 : Algebra (Polynomial ↥E) K] [FaithfulSMul (Polynomial ↥E) K]
  [IsScalarTower (Polynomial F) (Polynomial ↥E) K], FiniteDimensional (RatFunc F) (RatFunc ↥E)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail.  -/
Std.DTreeMap.Internal.Impl.forInStep : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      {m : Type w → Type u_1} →
        [Monad m] → ((a : α) → β a → δ → m (ForInStep δ)) → δ → Std.DTreeMap.Internal.Impl α β → m (ForInStep δ)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `sub_nonneg`. -/
sub_nonneg_of_le : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, b ≤ a → 0 ≤ a - b
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.inf_eq_left : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {a b : CauSeq α abs},
  a ≤ b → a ⊓ b ≈ a
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.toFun_eq_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), ↑e.toPartialEquiv = ↑e
-- Init.Control.Lawful.MonadLift.Instances
_private.Init.Control.Lawful.MonadLift.Instances.0.Except.map.match_1.eq_1 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (err : ε) (h_1 : (err : ε) → motive (Except.error err))
  (h_2 : (v : α) → motive (Except.ok v)),
  (match Except.error err with
    | Except.error err => h_1 err
    | Except.ok v => h_2 v) =
    h_1 err
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [Std.LawfulEqOrd α] [inst_5 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {km : α},
        Std.Internal.List.maxKey! l = km ↔
          Std.Internal.List.containsKey km l = true ∧
            ∀ (k : α), Std.Internal.List.containsKey k l = true → (compare k km).isLE = true
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
SSet.Truncated.rightExtensionInclusion_hom_app : ∀ (X : SSet) (n : ℕ) (X_1 : (SimplexCategory.Truncated n)ᵒᵖ),
  (SSet.Truncated.rightExtensionInclusion X n).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj (Opposite.op (Opposite.unop X_1).obj))
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.partialTraj_succ_self : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} (a : ℕ),
  ProbabilityTheory.Kernel.partialTraj κ a (a + 1) =
    (ProbabilityTheory.Kernel.id.prod ((κ a).map ⇑(MeasurableEquiv.piSingleton a))).map (IicProdIoc a (a + 1))
-- Mathlib.Algebra.Lie.SemiDirect
/-- As raw types, the semidirect product is just a product.  -/
LieAlgebra.SemiDirectSum.toProd : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → {ψ : L →ₗ⁅R⁆ LieDerivation R K K} → K ⋊⁅ψ⁆ L ≃ K × L
-- Mathlib.Topology.Sheaves.Points
Opens.isConservativeFamilyOfPoints_pointsGrothendieckTopology : ∀ (X : Type u) [inst : TopologicalSpace X], (Opens.pointsGrothendieckTopology X).IsConservativeFamilyOfPoints
-- Batteries.Data.UnionFind.Basic
/-- Validity for parent nodes  -/
Batteries.UnionFind.parentD_lt : ∀ (self : Batteries.UnionFind) {i : ℕ}, i < self.arr.size → Batteries.UnionFind.parentD self.arr i < self.arr.size
-- Mathlib.Algebra.Algebra.Equiv
/-- The tautological action by `A₁ ≃ₐ[R] A₁` on `A₁`.

This generalizes `Function.End.applyMulAction`.  -/
AlgEquiv.applyMulSemiringAction : {R : Type uR} →
  {A₁ : Type uA₁} →
    [inst : CommSemiring R] → [inst_1 : Semiring A₁] → [inst_2 : Algebra R A₁] → MulSemiringAction (A₁ ≃ₐ[R] A₁) A₁
-- Mathlib.Geometry.Euclidean.Triangle
/-- The greatest angle of a possibly degenerate triangle is at least `π / 3`.  -/
EuclideanGeometry.pi_div_three_le_angle_of_le_of_le : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₂ p₃ p₁ ≤ EuclideanGeometry.angle p₁ p₂ p₃ →
    EuclideanGeometry.angle p₃ p₁ p₂ ≤ EuclideanGeometry.angle p₁ p₂ p₃ → Real.pi / 3 ≤ EuclideanGeometry.angle p₁ p₂ p₃
-- Mathlib.Algebra.Category.Grp.AB
instAB4StarAddCommGrpCat : CategoryTheory.AB4Star AddCommGrpCat
-- Lean.Meta.Sym.Util
/-- Debug helper: throws if any subexpression of `e` is not in the table of maximally shared terms.  -/
Lean.Expr.checkMaxShared : Lean.Expr → optParam String "" → Lean.Meta.Sym.SymM Unit
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Two n-simplices among cospherical points in an n-dimensional
subspace have the same circumradius.  -/
EuclideanGeometry.circumradius_eq_of_cospherical_subset : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
  ps ⊆ ↑s →
    ∀ [Nonempty ↥s] {n : ℕ} [FiniteDimensional ℝ ↥s.direction],
      Module.finrank ℝ ↥s.direction = n →
        EuclideanGeometry.Cospherical ps →
          ∀ {sx₁ sx₂ : Affine.Simplex ℝ P n},
            Set.range sx₁.points ⊆ ps → Set.range sx₂.points ⊆ ps → sx₁.circumradius = sx₂.circumradius
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_eq_iff_eq_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {x : M} {y : ↥S} {z : N}, f.mk' x y = z ↔ f x = z + f ↑y
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumLocallyUniformly.tendstoLocallyUniformly_finsetRange : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] {g : β → α} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β] {f : ℕ → β → α},
  HasSumLocallyUniformly f g → TendstoLocallyUniformly (fun x1 x2 => ∑ i ∈ Finset.range x1, f i x2) g Filter.atTop
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- The counit is natural in `S : CompHausLike P`  -/
CompHausLike.LocallyConstant.counitApp : {P : TopCat → Prop} →
  [∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    [inst : CompHausLike.HasProp P PUnit.{u + 1}] →
      [CompHausLike.HasExplicitFiniteCoproducts P] →
        (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))) →
          [CategoryTheory.Limits.PreservesFiniteProducts Y] →
            CompHausLike.LocallyConstant.functorToPresheaves.obj
                (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1}))) ⟶
              Y
-- Mathlib.NumberTheory.Divisors
Nat.fst_mem_divisors_of_mem_antidiagonal : ∀ {n : ℕ} {x : ℕ × ℕ}, x ∈ n.divisorsAntidiagonal → x.1 ∈ n.divisors
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin_congr_of_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s : Set M},
  (∀ x ∈ s, f₁ x = f x) → x ∈ s → mfderiv[s] f₁ x = mfderiv[s] f x
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_le_nnnorm_add_nnnorm_div' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), ‖a‖₊ ≤ ‖b‖₊ + ‖a / b‖₊
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Auxiliary definition for `iso`.  -/
CategoryTheory.Adjunction.RightAdjointCommShift.iso' : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {A : Type u_3} →
                [inst_2 : AddGroup A] →
                  [inst_3 : CategoryTheory.HasShift C A] →
                    [inst_4 : CategoryTheory.HasShift D A] →
                      (a b : A) →
                        b + a = 0 →
                          [F.CommShift A] →
                            (CategoryTheory.shiftFunctor D a).comp G ≅ G.comp (CategoryTheory.shiftFunctor C a)
-- Mathlib.RingTheory.Coalgebra.GroupLike
/-- A group-like element `a` satisfies `Δ(a) = a ⊗ₜ a`.  -/
IsGroupLikeElem.comul_eq_tmul_self : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] {a : A}, IsGroupLikeElem R a → CoalgebraStruct.comul a = a ⊗ₜ[R] a
-- Mathlib.Data.Set.Basic
Set.union_isAssoc : ∀ {α : Type u}, Std.Associative fun x1 x2 => x1 ∪ x2
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a fallback : α} {v : β k}, (m.insert k v).getKeyD a fallback = if (k == a) = true then k else m.getKeyD a fallback
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- The function `x ^ (a / (b * x + c))` tends to `1` at `+∞`, for any real numbers `a`, `b`, and
`c` such that `b` is nonzero.  -/
tendsto_rpow_div_mul_add : ∀ (a b c : ℝ), 0 ≠ b → Filter.Tendsto (fun x => x ^ (a / (b * x + c))) Filter.atTop (nhds 1)
-- Mathlib.Analysis.SpecificLimits.Normed
dist_partial_sum' : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] (u : ℕ → α) (n : ℕ),
  dist (∑ k ∈ Finset.range n, u k) (∑ k ∈ Finset.range (n + 1), u k) = ‖u n‖
-- Mathlib.Data.Finset.Finsupp
Finset.card_finsupp : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (s : Finset ι) (t : ι → Finset α),
  (s.finsupp t).card = ∏ i ∈ s, (t i).card
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.main : Lean.ParseImports.Parser
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.algebraMap_surjective : ∀ (k : Type u) [inst : Field k] (K : Type v) [inst_1 : Field K] [IsSepClosed k] [inst_3 : Algebra k K]
  [Algebra.IsSeparable k K], Function.Surjective ⇑(algebraMap k K)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.maxKey?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.maxKey? = t₂.maxKey?
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instInvolutiveInv.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [inst_2 : ContinuousInv G],
  SeparationQuotient.instInvolutiveInv = Function.Surjective.involutiveInv SeparationQuotient.mk ⋯ ⋯
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafifyMap_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R),
  CategoryTheory.sheafifyMap J (CategoryTheory.CategoryStruct.comp η γ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyMap J η) (CategoryTheory.sheafifyMap J γ)
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
arithGeom_succ : ∀ {R : Type u_1} {a b u₀ : R} [inst : Mul R] [inst_1 : Add R] (n : ℕ),
  arithGeom a b u₀ (n + 1) = a * arithGeom a b u₀ n + b
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_eq_bot_iff_le_ker : ∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] {I : Ideal R} (f : F), Ideal.map f I = ⊥ ↔ I ≤ RingHom.ker f
-- Lean.Declaration
Lean.QuotVal.mk : Lean.ConstantVal → Lean.QuotKind → Lean.QuotVal
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp a (p + b) = toIocMod hp a b
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_inv_π_π : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape K C] (k : K) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.flip.comp CategoryTheory.Limits.lim) k)
        (CategoryTheory.Limits.limit.π (F.flip.obj k) j)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j)
      (CategoryTheory.Limits.limit.π (F.obj j) k)
-- Mathlib.Data.List.Chain
instIsWellFoundedChainsLex_chains : ∀ {α : Type u_1} {r : α → α → Prop} [hwf : IsWellFounded α r], IsWellFounded (List.chains r) (List.lex_chains r)
-- Mathlib.Algebra.Module.Presentation.Basic
/-- Given a ring `A`, this structure involves a family of elements (indexed by a type `R`)
in a free module `G →₀ A`. This allows to define an `A`-module by generators and relations,
see `Relations.Quotient`.  -/
Module.Relations : (A : Type u) → [Ring A] → Type (max (max u (w₀ + 1)) (w₁ + 1))
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_liftWith_ExceptT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε α : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ (ε → Pred) EPred} (f : ({β : Type u} → ExceptT ε m β → m (Except ε β)) → m α),
  Std.Internal.Do.wp (MonadControl.liftWith f) post epost =
    Std.Internal.Do.wp (Except.ok <$> f fun {β} x => x.run) (Std.Internal.Do.EPost.Cons.pushExcept post epost)
      epost.tail
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getEntryLTD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : α × β}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryLTD k fallback = t₂.getEntryLTD k fallback
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.Normal.mem_comm_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Normal → ∀ {a b : G}, a * b ∈ H ↔ b * a ∈ H
-- Aesop.Stats.Basic
Aesop.Stats.mk : Aesop.Nanos →
  Aesop.Nanos →
    Aesop.Nanos →
      Aesop.Nanos →
        Aesop.Nanos →
          Aesop.Nanos →
            Aesop.Nanos → Option Aesop.ScriptGenerated → Array Aesop.RuleStats → Array Aesop.GoalStats → Aesop.Stats
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v},
  (m.insertIfNew k v)[a] = if h₂ : (k == a) = true ∧ k ∉ m then v else m[a]
-- Mathlib.CategoryTheory.Dialectica.Basic
/-- An isomorphism in `Dial C` can be induced by isomorphisms on the source and target,
which respect the respective relations on `X` and `Y`.
 -/
CategoryTheory.Dial.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        {X Y : CategoryTheory.Dial C} →
          (e₁ : X.src ≅ Y.src) →
            (e₂ : X.tgt ≅ Y.tgt) →
              X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel →
                (X ≅ Y)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.isUnit_shift : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A},
  g.IsWeierstrassDivisorAt I →
    IsUnit (PowerSeries.mk fun i => (PowerSeries.coeff (i + ((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat)) g)
-- Mathlib.Order.Cover
WithTop.coe_covBy_coe : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, ↑a ⋖ ↑b ↔ a ⋖ b
-- Mathlib.MeasureTheory.Measure.AddContent
/-- If a set can be written in two different ways as a disjoint union of elements of a semi-ring
of sets `C`, then the sums of the values of `m : addContent C` along the two decompositions give
the same result.
In other words, `m` can be canonically extended to finite unions of elements of `C`.  -/
MeasureTheory.sum_addContent_eq_of_sUnion_eq : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] {m : MeasureTheory.AddContent G C},
  MeasureTheory.IsSetSemiring C →
    ∀ (J J' : Finset (Set α)),
      ↑J ⊆ C →
        (↑J).PairwiseDisjoint id → ↑J' ⊆ C → (↑J').PairwiseDisjoint id → ⋃₀ ↑J = ⋃₀ ↑J' → ∑ s ∈ J, m s = ∑ t ∈ J', m t
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctor_map_f' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n p : ℤ),
  ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ).f p = φ.f (p + n)
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.ext : ∀ {X Y : PartOrdEmb} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.ιTotal_totalFlipIso_f_inv : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c]
  [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c]
  [inst_6 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₁.π c₂ c (i₁, i₂) = j),
  CategoryTheory.CategoryStruct.comp (K.ιTotal c i₁ i₂ j h) ((K.totalFlipIso c).inv.f j) =
    c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
Lean.Meta.Grind.Arith.Linear.reportInstIssue : Lean.Expr → Lean.Meta.Grind.GoalM Unit