mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_rev_Ioc : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.rev (Finset.Ioc i j) = Finset.Ico j.rev i.rev
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.mk.sizeOf_spec : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Semiring R] [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} {E : Type u_11}
  {E₂ : Type u_12} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] [inst_6 : SizeOf R] [inst_7 : SizeOf R₂] [inst_8 : SizeOf E] [inst_9 : SizeOf E₂]
  (toLinearMap : E →ₛₗ[σ₁₂] E₂) (norm_map' : ∀ (x : E), ‖toLinearMap x‖ = ‖x‖),
  sizeOf { toLinearMap := toLinearMap, norm_map' := norm_map' } = 1 + sizeOf toLinearMap
-- Init.Data.Array.Int
Array.sum_reverse_int : ∀ (xs : Array ℤ), xs.reverse.sum = xs.sum
-- Mathlib.Data.Fin.Tuple.Reflection
_private.Mathlib.Data.Fin.Tuple.Reflection.0.FinVec.sum.match_1.eq_3 : ∀ {α : Type u_2} (motive : (x : ℕ) → (Fin x → α) → Sort u_1) (n : ℕ) (v : Fin (n + 2) → α)
  (h_1 : (x : Fin 0 → α) → motive 0 x) (h_2 : (v : Fin 1 → α) → motive 1 v)
  (h_3 : (n : ℕ) → (v : Fin (n + 2) → α) → motive n.succ.succ v),
  (match n.succ.succ, v with
    | 0, x => h_1 x
    | 1, v => h_2 v
    | n.succ.succ, v => h_3 n v) =
    h_3 n v
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.append.congr_simp : ∀ {l r w : ℕ} (lhs lhs_1 : Std.Tactic.BVDecide.BVExpr l),
  lhs = lhs_1 →
    ∀ (rhs rhs_1 : Std.Tactic.BVDecide.BVExpr r),
      rhs = rhs_1 → ∀ (h : w = l + r), lhs.append rhs h = lhs_1.append rhs_1 h
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.compare_maxKey?_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {km kmm : α} (hkm : t.maxKey? = some km),
  (Std.ExtDTreeMap.Const.modify t k f).maxKey?.get ⋯ = kmm → cmp kmm km = Ordering.eq
-- Mathlib.Lean.Expr.Basic
/-- Update the type of a `ConstantInfo`.  -/
Lean.ConstantInfo.updateType : Lean.ConstantInfo → Lean.Expr → Lean.ConstantInfo
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_of_mem_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α}, m.WF → k ∈ Std.DHashMap.Raw.map f m → k ∈ m
-- Mathlib.RingTheory.LocalRing.Basic
/-- A semiring is local if it has a unique maximal ideal.  -/
IsLocalRing.of_unique_max_ideal : ∀ {R : Type u_1} [inst : CommSemiring R], (∃! I, I.IsMaximal) → IsLocalRing R
-- Mathlib.Data.Set.Function
Set.bijOn_empty_iff_left : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.BijOn f s ∅ ↔ s = ∅
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.generateFrom_empty : ∀ {α : Type u_1}, MeasurableSpace.generateFrom ∅ = ⊥
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.smallCategory : CategoryTheory.SmallCategory SimplexCategory
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- A subsemigroup of a semigroup inherits a semigroup structure.  -/
MulMemClass.toSemigroup : {M : Type u_4} →
  [inst : Semigroup M] → {A : Type u_5} → [inst_1 : SetLike A M] → [MulMemClass A M] → (S : A) → Semigroup ↥S
-- Mathlib.Algebra.Order.Hom.Basic
MulRingNormClass.toRingNormClass : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : NonAssocRing α] [inst_2 : Semiring β]
  [inst_3 : PartialOrder β] [MulRingNormClass F α β], RingNormClass F α β
-- Mathlib.Order.DirSupClosed
/-- **Alias** of the reverse direction of `dirSupInaccOn_compl`. -/
DirSupClosedOn.compl : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α], DirSupClosedOn D s → DirSupInaccOn D sᶜ
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.coprodMk_inl : ∀ (X Y : AlgebraicGeometry.Scheme) (x : ↥X),
  (AlgebraicGeometry.coprodMk X Y) (Sum.inl x) = CategoryTheory.Limits.coprod.inl x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 1st differential in the complex of inhomogeneous cochains of `A : Rep k G`, as a
`k`-linear map `Fun(G, A) → Fun(G × G, A)`. It sends
`(f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).`  -/
groupCohomology.d₁₂ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u_1, u, u} k G) → ModuleCat.of k (G → ↑A) ⟶ ModuleCat.of k (G × G → ↑A)
-- Mathlib.Util.Export
Lean.Export.instInhabitedEntry.default : Lean.Export.Entry
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
/-- If a right adjoint functor is isomorphic to the identity functor,
so is the left adjoint.  -/
CategoryTheory.Adjunction.leftAdjointIdIso : {C₀ : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C₀] →
    {F G : CategoryTheory.Functor C₀ C₀} →
      (F ⊣ G) → (G ≅ CategoryTheory.Functor.id C₀) → (F ≅ CategoryTheory.Functor.id C₀)
-- Mathlib.Topology.Sheaves.Points
Opens.instHasEnoughPointsOpensGrothendieckTopology : ∀ {X : Type u} [inst : TopologicalSpace X], (Opens.grothendieckTopology X).HasEnoughPoints
-- Init.Data.SInt.Lemmas
Int8.sub_add_cancel : ∀ (a b : Int8), a - b + b = a
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f * g) x = f x * g x`, `1 x = 1`, and `(f ^ n) x = f x ^ n`
is a cancel monoid if `β` is a cancel monoid.  -/
FunLike.cancelMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] →
          [inst_2 : One F] →
            [inst_3 : Pow F ℕ] →
              [inst_4 : CancelMonoid β] →
                [IsOneApply F α β] → [IsMulApply F α β] → [IsPowApply ℕ F α β] → CancelMonoid F
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.natCard_neg : ∀ {G : Type u_1} [inst : InvolutiveNeg G] (s : Set G), Nat.card ↑(-s) = Nat.card ↑s
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_coeToMvPowerSeries : ∀ {R : Type u_1} [inst : Semiring R] {f : PowerSeries R} (n : ℕ),
  (MvPowerSeries.coeff fun₀ | () => n) f = (PowerSeries.coeff n) f
-- Lean.LocalContext
Lean.LocalContext.allM : {m : Type → Type u_1} → [Monad m] → Lean.LocalContext → (Lean.LocalDecl → m Bool) → m Bool
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_zero : ∀ {K : Type u} [inst : Field K], RatFunc.num 0 = 0
-- Init.Data.Int.Linear
Int.Internal.Linear.cmod_eq_zero_iff_emod_eq_zero : ∀ (a b : ℤ), Int.Internal.Linear.cmod a b = 0 ↔ a % b = 0
-- Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant
HomotopicalAlgebra.instCofibrationInlOfIsCofibrant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (X Y : C)
  [(HomotopicalAlgebra.cofibrations C).IsStableUnderCobaseChange]
  [inst_4 : CategoryTheory.Limits.HasBinaryCoproduct X Y] [hY : HomotopicalAlgebra.IsCofibrant Y],
  HomotopicalAlgebra.Cofibration CategoryTheory.Limits.coprod.inl
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
/-- `klFun` is convex on $[0,∞)$.  -/
InformationTheory.convexOn_klFun : ConvexOn ℝ (Set.Ici 0) InformationTheory.klFun
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G A : C} {M : ModuleCat (CategoryTheory.End G)ᵐᵒᵖ}
  (g : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ A)) (m : ↑M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => G) m)
      (CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d g) =
    (ModuleCat.Hom.hom g) m
-- Init.Prelude
instDecidableLeBitVec : {w : ℕ} → (x y : BitVec w) → Decidable (x ≤ y)
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.down.eq_1 : ∀ (α : Type u_2) [inst : Add α] [inst_1 : IsRightCancelAdd α] [inst_2 : One α],
  ComplexShape.down α = ComplexShape.down' 1
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Frame.frame : ∀ {σs : List (Type u)} {P Q T : Std.Do.SPred σs} {φ : Prop} [Std.Do.SPred.Tactic.HasFrame P Q φ], (φ → Q ⊢ₛ T) → P ⊢ₛ T
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- Implementation; see `nonempty_indParallelPairPresentation`.  -/
CategoryTheory.NonemptyParallelPairPresentationAux.K : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      (A ⟶ B) →
        (A ⟶ B) →
          CategoryTheory.Limits.IndObjectPresentation A → CategoryTheory.Limits.IndObjectPresentation B → Type v₁
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_add_ediv_le_add_ediv : ∀ {x y z : ℤ}, 0 < z → x / z + y / z ≤ (x + y) / z
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.exists_intro' : ∀ {α : Sort u_1} {σs : List (Type u_2)} {P : Std.Do.SPred σs} {Ψ : α → Std.Do.SPred σs} (a : α),
  (P ⊢ₛ Ψ a) → P ⊢ₛ ∃ a, Ψ a
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientKerAlgEquivOfSurjective_mk : ∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] {f : A →ₐ[R₁] B} (hf : Function.Surjective ⇑f) (a : A),
  (Ideal.quotientKerAlgEquivOfSurjective hf) ((Ideal.Quotient.mk (RingHom.ker f)) a) = f a
-- Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
/-- Evaluation of continuous linear maps as a continuous linear map in the
case of finite dimensional topological vector spaces over a complete field.
See also `ContinuousLinearMap.apply` for the case of normed spaces.

TODO: generalize the two constructions in the setting of maps from a bornological space to a locally
convex one, or define a `NormableSpace` class to deduce this case from the normed case.
 -/
ContinuousLinearMap.evalL : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    [CompleteSpace 𝕜] →
      (E : Type u_2) →
        [inst_2 : AddCommGroup E] →
          [inst_3 : Module 𝕜 E] →
            [inst_4 : TopologicalSpace E] →
              [IsTopologicalAddGroup E] →
                [ContinuousSMul 𝕜 E] →
                  [FiniteDimensional 𝕜 E] →
                    [T2Space E] →
                      (F : Type u_3) →
                        [inst_9 : AddCommGroup F] →
                          [inst_10 : Module 𝕜 F] →
                            [inst_11 : TopologicalSpace F] →
                              [inst_12 : IsTopologicalAddGroup F] →
                                [inst_13 : ContinuousSMul 𝕜 F] →
                                  [FiniteDimensional 𝕜 F] → [T2Space F] → E →L[𝕜] (E →L[𝕜] F) →L[𝕜] F
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k : α} {f : Option β → Option β}
  {h : k ∈ Std.ExtDHashMap.Const.alter m k f}, (Std.ExtDHashMap.Const.alter m k f).getKey k h = k
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
isCyclic_right_of_prod : ∀ (M : Type u_4) (N : Type u_5) [inst : Group M] [inst_1 : Group N] [cyc : IsCyclic (M × N)], IsCyclic N
-- Std.Data.HashMap.DecidableEquiv
Std.HashMap.instDecidableEquivOfLawfulBEq : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [LawfulBEq α] →
        [inst_2 : Hashable α] → [inst_3 : BEq β] → [LawfulBEq β] → (m₁ m₂ : Std.HashMap α β) → Decidable (m₁.Equiv m₂)
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- `binEntropy` is symmetric about 1/2.  -/
Real.binEntropy_two_inv_add : ∀ (p : ℝ), Real.binEntropy (2⁻¹ + p) = Real.binEntropy (2⁻¹ - p)
-- Mathlib.Tactic.NormNum.Ordinal
Mathlib.Meta.NormNum.isNat_ordinalOPow : ∀ {a b : Ordinal.{u}} {an bn rn : ℕ},
  Mathlib.Meta.NormNum.IsNat a an →
    Mathlib.Meta.NormNum.IsNat b bn → an ^ bn = rn → Mathlib.Meta.NormNum.IsNat (a ^ b) rn
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.applyComposition.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup E] [inst_8 : ContinuousConstSMul 𝕜 E] [inst_9 : IsTopologicalAddGroup F]
  [inst_10 : ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (c : Composition n) (v : Fin n → E)
  (i : Fin c.length), p.applyComposition c v i = (p (c.blocksFun i)) (v ∘ ⇑(c.embedding i))
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- (implementation) right whiskering for R-modules  -/
SemimoduleCat.MonoidalCategory.whiskerRight : {R : Type u} →
  [inst : CommSemiring R] →
    {M₁ M₂ : SemimoduleCat R} →
      (M₁ ⟶ M₂) →
        (N : SemimoduleCat R) →
          SemimoduleCat.MonoidalCategory.tensorObj M₁ N ⟶ SemimoduleCat.MonoidalCategory.tensorObj M₂ N
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.sum_finsupport' : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) {x₀ : X},
  x₀ ∈ s → ∀ {I : Finset ι}, ρ.finsupport x₀ ⊆ I → ∑ i ∈ I, (ρ i) x₀ = 1
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.Amem.decidable : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → (x : α) → (t : Ordnode α) → Decidable (Ordnode.Amem x t)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.mapPreimage_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.GrothendieckTopology C}
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  (F : CategoryTheory.Sheaf J A) (X : C),
  CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F (CategoryTheory.CategoryStruct.id (G.obj X)) =
    CategoryTheory.CategoryStruct.id (F.obj.obj (Opposite.op X))
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.ofStabilizer_carrier : ∀ (G : Type u_1) [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] (a : α),
  (SubAddAction.ofStabilizer G a).carrier = {a}ᶜ
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contMDiff_invFun : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  (self : Diffeomorph I I' M M' n), ContMDiff I' I n ⇑self.symm
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.separatingRight_iff_det_ne_zero : ∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} [inst_1 : CommRing A] [IsDomain A] {M : Matrix n n A}
  [inst_3 : DecidableEq n], M.SeparatingRight ↔ M.det ≠ 0
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM : Type → Type
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.map_le_map_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) {p p' : Submodule R M},
  Submodule.map f p ≤ Submodule.map f p' ↔ p ≤ p' ⊔ f.ker
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_iff_not_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α}, Order.pred a < a ↔ ¬IsMin a
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.isCyclic_units_four_mul_iff : ∀ (n : ℕ), IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1
-- Init.Data.List.Lemmas
List.get_cons_succ' : ∀ {α : Type u_1} {a : α} {as : List α} {i : Fin as.length}, (a :: as).get i.succ = as.get i
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.path_self : ∀ (x : Circle), x.path x = Path.refl x
-- Std.Sync.Mutex
_private.Std.Sync.Mutex.0.Std.Mutex.mk.injEq : ∀ {α : Type} (ref : IO.Ref α) (mutex : Std.BaseMutex) (ref_1 : IO.Ref α) (mutex_1 : Std.BaseMutex),
  ({ ref := ref, mutex := mutex } = { ref := ref_1, mutex := mutex_1 }) = (ref = ref_1 ∧ mutex = mutex_1)
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.instInhabited : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          {η : F ⟶ G} → Inhabited (CategoryTheory.Pseudofunctor.StrongTrans.Modification η η)
-- Init.Data.SInt.Lemmas
Int64.lt_of_le_of_ne : ∀ {a b : Int64}, a ≤ b → a ≠ b → a < b
-- Mathlib.Data.FunLike.IsApply
pow_apply_eq_iterate : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α α] [inst_1 : Monoid F] [IsOneApplyEqSelf F α] [IsMulApplyEqComp F α]
  (f : F) (n : ℕ) (x : α), (f ^ n) x = (⇑f)^[n] x
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.map_apply : ∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : Group G] [inst_1 : Group H] (b : FreeGroupBasis ι G) (e : G ≃* H)
  (x : ι), (b.map e) x = e (b x)
-- Mathlib.Data.Finsupp.Order
Finsupp.embDomain_mono : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : Zero α] [inst_1 : Preorder α] (f : ι ↪ κ),
  Monotone (Finsupp.embDomain f)
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.Sublist.prod_dvd_prod : ∀ {M : Type u_4} [inst : CommMonoid M] {l₁ l₂ : List M}, l₁.Sublist l₂ → l₁.prod ∣ l₂.prod
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.add_subset_iff_right : ∀ {α : Type u_2} [inst : Add α] {s t u : Set α}, s + t ⊆ u ↔ ∀ b ∈ t, AddOpposite.op b +ᵥ s ⊆ u
-- Mathlib.Algebra.Category.Ring.Limits
CommRingCat.hasLimits : CategoryTheory.Limits.HasLimits CommRingCat
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- Given an open immersion `f : U ⟶ X`, the isomorphism between global sections
of `U` and the sections of `X` at the image of `f`.  -/
AlgebraicGeometry.IsOpenImmersion.ΓIsoTop : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] →
      X.presheaf.obj (Opposite.op ⊤) ≅ Y.presheaf.obj (Opposite.op (AlgebraicGeometry.Scheme.Hom.opensRange f))
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curry_obj_obj_obj : ∀ {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] (F : CategoryTheory.Functor (C × D) E) (X : C) (Y : D),
  ((CategoryTheory.Functor.curry.obj F).obj X).obj Y = F.obj (X, Y)
-- Mathlib.Data.Rat.Lemmas
Rat.sub_intCast_den : ∀ (q : ℚ) (n : ℤ), (q - ↑n).den = q.den
-- Init.System.IOError
IO.Error.mkProtocolError : UInt32 → String → IO.Error
-- Init.Data.Option.Lemmas
Option.pfilter.eq_2 : ∀ {α : Type u_1} (a : α) (p_2 : (a_1 : α) → some a = some a_1 → Bool),
  (some a).pfilter p_2 = bif p_2 a ⋯ then some a else none
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.foldlM_eq_foldlM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : δ → α → m δ} {init : δ}, Std.TreeSet.foldlM f init t = List.foldlM f init t.toList
-- Lean.LocalContext
Lean.LocalDecl.ldecl.sizeOf_spec : ∀ (index : ℕ) (fvarId : Lean.FVarId) (userName : Lean.Name) (type value : Lean.Expr) (nondep : Bool)
  (kind : Lean.LocalDeclKind),
  sizeOf (Lean.LocalDecl.ldecl index fvarId userName type value nondep kind) =
    1 + sizeOf index + sizeOf fvarId + sizeOf userName + sizeOf type + sizeOf value + sizeOf nondep + sizeOf kind
-- Plausible.Shrinkable
/-- Given an example `x : α`, `Shrinkable α` gives us a way to shrink it
and suggest simpler examples.  -/
Plausible.Shrinkable : Type u → Type u
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α}, k ∈ m₂ → Std.ExtDHashMap.Const.get! (m₁ \ m₂) k = default
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.universallyClosed_eq : @AlgebraicGeometry.UniversallyClosed = (AlgebraicGeometry.topologically @IsClosedMap).universally
-- Mathlib.CategoryTheory.Limits.Types.PreservesLimit
CategoryTheory.Presheaf.nonempty_isLimit_mapCone_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] {F : CategoryTheory.Functor J Cᵒᵖ}
  (c : CategoryTheory.Limits.Cone F)
  {c' : CategoryTheory.Limits.Cocone (F.leftOp.comp CategoryTheory.shrinkYoneda.{w, v, u})}
  (hc' : CategoryTheory.Limits.IsColimit c') (P : CategoryTheory.Functor Cᵒᵖ (Type w)),
  Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone c)) ↔
    (CategoryTheory.MorphismProperty.single (CategoryTheory.Presheaf.coconePtToShrinkYoneda c hc')).isLocal P
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_eq_fintype_linearCombination_apply : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (v : α → M) (x : α → R),
  (Finsupp.linearCombination R v) ((Finsupp.linearEquivFunOnFinite R R α).symm x) = (Fintype.linearCombination R v) x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_7 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.umod with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_7 ()
-- Mathlib.Data.Finset.Filter
Finset.filter_ssubset : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α}, Finset.filter p s ⊂ s ↔ ∃ x ∈ s, ¬p x
-- Mathlib.Algebra.Category.AlgCat.Limits
/-- Construction of a limit cone in `AlgCat R`.
(Internal use only; use the limits API.)
 -/
AlgCat.HasLimits.limitCone : {R : Type u} →
  [inst : CommRing R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (AlgCat R)) →
          [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] → CategoryTheory.Limits.Cone F
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.code.opener : Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipping_counitIso_hom_app_app_app : ∀ {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]
  (X : CategoryTheory.Functor D (CategoryTheory.Functor C E)) (X_1 : D) (X_2 : C),
  ((CategoryTheory.Functor.flipping.counitIso.hom.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id ((X.obj X_1).obj X_2)
-- Mathlib.Order.Max
/-- **Alias** of the reverse direction of `isMin_toDual_iff`. -/
IsMax.toDual : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMax a → IsMin (OrderDual.toDual a)
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.generator_submoduleImage_dvd_of_mem : ∀ {R : Type u} {M : Type v} [inst : AddCommMonoid M] [inst_1 : CommSemiring R] [inst_2 : Module R M]
  {N O : Submodule R M} (hNO : N ≤ O) (ϕ : ↥O →ₗ[R] R) [inst_3 : (ϕ.submoduleImage N).IsPrincipal] {x : M} (hx : x ∈ N),
  Submodule.IsPrincipal.generator (ϕ.submoduleImage N) ∣ ϕ ⟨x, ⋯⟩
-- Aesop.Forward.LevelIndex
Aesop.instInhabitedLevelIndex : Inhabited Aesop.LevelIndex