mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Similarity
Similar.comp_isometry_right : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃] {f : P₂ → P₃},
  Isometry f → Similar v₁ v₂ → Similar v₁ (f ∘ v₂)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_inverse_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T'),
  ((CategoryTheory.StructuredArrow.mapNatIso i).inverse.obj X).right = X.right
-- Mathlib.Topology.Algebra.Monoid
AddSubmonoid.topologicalClosure_mono : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : SeparatelyContinuousAdd M]
  {s t : AddSubmonoid M}, s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Mathlib.Tactic.Widget.Calc
CalcParams.mk.injEq : ∀ (toSelectInsertParams : SelectInsertParams) (isFirst : Bool) (indent : ℕ)
  (toSelectInsertParams_1 : SelectInsertParams) (isFirst_1 : Bool) (indent_1 : ℕ),
  ({ toSelectInsertParams := toSelectInsertParams, isFirst := isFirst, indent := indent } =
      { toSelectInsertParams := toSelectInsertParams_1, isFirst := isFirst_1, indent := indent_1 }) =
    (toSelectInsertParams = toSelectInsertParams_1 ∧ isFirst = isFirst_1 ∧ indent = indent_1)
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_toUInt16 : ∀ (n : UInt64), n.toUInt16.toUInt32 = n.toUInt32 % 65536
-- Mathlib.Analysis.Normed.Group.Constructions
pi_norm_le_iff_of_nonempty : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i)
  {r : ℝ} [Nonempty ι], ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
-- Mathlib.Order.Category.DistLat
DistLat.mk : (carrier : Type u_1) → [str : DistribLattice carrier] → DistLat
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.Ioi_mem_atTop : ∀ {α : Type u_3} [inst : Preorder α] [NoTopOrder α] (x : α), Set.Ioi x ∈ Filter.atTop
-- Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
PositiveLinearMap.apply_le_of_isSelfAdjoint : ∀ {B₁ : Type u_3} {B₂ : Type u_4} [inst : CStarAlgebra B₁] [inst_1 : CStarAlgebra B₂] [inst_2 : PartialOrder B₁]
  [inst_3 : PartialOrder B₂] [StarOrderedRing B₁] (f : B₁ →ₚ[ℂ] B₂) (x : B₁),
  IsSelfAdjoint x → f x ≤ f ((algebraMap ℝ B₁) ‖x‖)
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instInterOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Inter (Std.ExtHashMap α β)
-- Mathlib.Order.Monotone.MonovaryOrder
antivaryOn_iff_exists_monotoneOn_antitoneOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, AntivaryOn f g s ↔ ∃ x, MonotoneOn f s ∧ AntitoneOn g s
-- Init.Data.Int.DivMod.Lemmas
Int.add_neg_fmod_self : ∀ (a b : ℤ), (a + -b).fmod b = a.fmod b
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_pos_iff_support : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → (0 < ∫⁻ (a : α), f a ∂μ ↔ 0 < μ (Function.support f))
-- Mathlib.Algebra.Order.GroupWithZero.WithZero
instMulPosStrictMonoWithZeroOfMulRightStrictMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulRightStrictMono α], MulPosStrictMono (WithZero α)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.equivOp.eq_1 : ∀ {M : Type u_2} [inst : Mul M] (H : Subsemigroup M), H.equivOp = MulOpposite.opEquiv.subtypeEquiv ⋯
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.eq_zero_of_smul_eq_zero : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ∀ r ∈ S, ∀ (x : LocalizedModule S M), r • x = 0 → x = 0
-- Init.System.Promise
/-- The result task of a `Promise`.

The task blocks until `Promise.resolve` is called. If the promise is dropped without ever being
resolved, evaluating the task will panic and, when not using fatal panics, block forever. As
`Promise.result!` is a pure value and thus the point of evaluation may not be known precisely, this
means that any promise on which `Promise.result!` *may* be evaluated *must* be resolved eventually.
When in doubt, always prefer `Promise.result?` to handle dropped promises explicitly.
 -/
IO.Promise.result! : {α : Type} → IO.Promise α → Task α
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.is_alexandrovDiscrete : ∀ (self : AlexDisc), AlexandrovDiscrete ↑self.toTopCat
-- Mathlib.Tactic.NormNum.PowMod
Mathlib.Meta.NormNum.natPow_one_natMod : ∀ {a m : ℕ}, (a.pow 1).mod m = a.mod m
-- Mathlib.Computability.TuringMachine.Tape
/-- `BlankRel` is the symmetric closure of `BlankExtends`, turning it into an equivalence
relation. Two lists are related by `BlankRel` if one extends the other by blanks.  -/
Turing.BlankRel : {Γ : Type u_1} → [Inhabited Γ] → List Γ → List Γ → Prop
-- Lean.Meta.Sym.Canon
/-- Auxiliary function for normalizing the arguments of `OfNat.ofNat` during canonicalization.
This is needed because satellite solvers create `Nat` and `Int` numerals using the
APIs `mkNatLit` and `mkIntLit`, which produce terms of the form
`@OfNat.ofNat Nat <num> inst` and `@OfNat.ofNat Int <num> inst`.
This becomes a problem when a term in the input goal has already been canonicalized
and its type is not exactly `Nat` or `Int`. For example, in issue #9477, we have:
```
structure T where
upper_bound : Nat
def T.range (a : T) := 0...a.upper_bound
theorem range_lower (a : T) : a.range.lower = 0 := by rfl
```
Here, the `0` in `range_lower` is actually represented as:
```
(@OfNat.ofNat
  (Std.PRange.Bound (Std.PRange.RangeShape.lower (Std.PRange.RangeShape.mk Std.PRange.BoundShape.closed Std.PRange.BoundShape.open)) Nat)
  (nat_lit 0)
  (instOfNatNat (nat_lit 0)))
```
Without this normalization step, the satellite solver would need to handle multiple
representations for `(0 : Nat)` and `(0 : Int)`, complicating reasoning.
 -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.normOfNatArgs? : Array Lean.Expr → Lean.MetaM (Option (Array Lean.Expr))
-- Mathlib.Topology.Separation.Regular
T25Space.of_injective_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T25Space Y] {f : X → Y},
  Function.Injective f → Continuous f → T25Space X
-- Init.Data.Array.Lemmas
Array.forall_none_of_filterMap_eq_empty : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {xs : Array α}, Array.filterMap f xs = #[] → ∀ x ∈ xs, f x = none
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.append.eq_def : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (x : List Γ) (x_1 : Turing.ListBlank Γ),
  Turing.ListBlank.append x x_1 =
    match x, x_1 with
    | [], L => L
    | a :: l, L => Turing.ListBlank.cons a (Turing.ListBlank.append l L)
-- Batteries.Data.List.Basic
List.swapAtTR.go.eq_def : ∀ {α : Type u_1} (l : List α) (v : α) (a : List α) (a_1 : ℕ) (a_2 : Array α),
  List.swapAtTR.go l v a a_1 a_2 =
    match a, a_1, a_2 with
    | [], x, x_1 => (v, l)
    | a :: xs, 0, acc => (a, acc.toListAppend (v :: xs))
    | a :: xs, i.succ, acc => List.swapAtTR.go l v xs i (acc.push a)
-- Init.Data.Float.Float
/-- Converts a floating-point number to an 8-bit unsigned integer.

If the given `Float` is non-negative, truncates the value to a positive integer, rounding down and
clamping to the range of `UInt8`. Returns `0` if the `Float` is negative or `NaN`, and returns the
largest `UInt8` value (i.e. `UInt8.size - 1`) if the float is larger than it.

This function has a logical model in terms of `Float.Model`.
 -/
Float.toUInt8 : Float → UInt8
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S), WithAbs.toAbs v 0 = 0
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentContentChangeEvent.fullChange.inj : ∀ {text text_1 : String},
  Lean.Lsp.TextDocumentContentChangeEvent.fullChange text = Lean.Lsp.TextDocumentContentChangeEvent.fullChange text_1 →
    text = text_1
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.exists_norm_lt_one : ∀ (α : Type u_2) [inst : NontriviallyNormedField α], ∃ x, 0 < ‖x‖ ∧ ‖x‖ < 1
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.lift_symm_apply : ∀ {I : Type u} [inst : DecidableEq I] (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] {B : Type w'} [inst_4 : Semiring B]
  [inst_5 : Algebra R B] (π : LinearAlgebra.FreeProduct R A →ₐ[R] B) (i : I),
  (LinearAlgebra.FreeProduct.lift R A).symm π = π.comp (LinearAlgebra.FreeProduct.ι R A i)
-- Qq.ForLean.ReduceEval
Lean.Meta.instReduceEvalList_qq : {α : Type} → [Lean.Meta.ReduceEval α] → Lean.Meta.ReduceEval (List α)
-- Mathlib.Analysis.ODE.Basic
isIntegralCurve_iff_isIntegralCurveAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E},
  IsIntegralCurve γ v ↔ ∀ (t : ℝ), IsIntegralCurveAt γ v t
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.associatorIsEquivalence : ∀ (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.sum.associator C D E).IsEquivalence
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_roi_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ},
  Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rco.Sliceable.mkSlice xs (lo + 1)...xs.size
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Array.Matcher.modifyStep.match_1.eq_2 : ∀ {α σ : Type u_1} {n : Type u_1 → Type u_2} [inst : BEq α] (m : Array.Matcher α) [inst_1 : Std.Iterator σ n α]
  (it : Std.IterM n σ) (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM n α)
  (property : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 : (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩)
  (h_2 :
    (it' : Std.IterM n α) →
      (property : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) →
        motive ⟨Std.IterStep.skip it', property⟩)
  (h_3 :
    (it' : Std.IterM n α) →
      (x : α) →
        (property : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' x)) →
          motive ⟨Std.IterStep.yield it' x, property⟩),
  (match ⟨Std.IterStep.skip it', property⟩ with
    | ⟨Std.IterStep.done, property⟩ => h_1 property
    | ⟨Std.IterStep.skip it', property⟩ => h_2 it' property
    | ⟨Std.IterStep.yield it' x, property⟩ => h_3 it' x property) =
    h_2 it' property
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instVAddAssocClass_1 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M N] [inst_1 : VAdd M α] [inst_2 : VAdd N α]
  [VAddAssocClass M N α], VAddAssocClass M Nᵒᵈ α
-- Init.Data.Slice.List.Lemmas
ListSlice.toArray_mkSlice_rco : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...hi) = (Std.Slice.toArray xs).extract lo hi
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Spec.map_inj : ∀ {R S : CommRingCat} {φ ψ : R ⟶ S}, AlgebraicGeometry.Spec.map φ = AlgebraicGeometry.Spec.map ψ ↔ φ = ψ
-- Lean.Elab.Tactic.Basic
Lean.Elab.goalsToMessageData : List Lean.MVarId → Lean.MessageData
-- Mathlib.Algebra.BigOperators.Finprod
single_le_finsum : ∀ {α : Type u_1} {M : Type u_7} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] (i : α)
  {f : α → M}, Function.HasFiniteSupport f → (∀ (j : α), 0 ≤ f j) → f i ≤ ∑ᶠ (j : α), f j
-- Lean.Parser.Attr
Lean.Parser.Attr.instance : Lean.Parser.Parser
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.uniformContinuousConstSMul : ∀ (M : Type u_1) (α : Type u_2) (X : Type u_3) [inst : SMul M X] [inst_1 : UniformSpace X]
  [UniformContinuousConstSMul M X], UniformContinuousConstSMul M (UniformFun α X)
-- Mathlib.RepresentationTheory.Invariants
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `ρ` induces a `G ⧸ S`-representation on
the invariants of `ρ|_S`.  -/
Rep.quotientToInvariants : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] → Rep.{w, u, v} k G → (S : Subgroup G) → [inst_2 : S.Normal] → Rep.{w, u, v} k (G ⧸ S)
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.mem_hasEvalIdeal_iff : ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : TopologicalSpace S] [inst_2 : IsTopologicalRing S]
  [inst_3 : IsLinearTopology S S] {a : S}, a ∈ PowerSeries.hasEvalIdeal ↔ PowerSeries.HasEval a
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- A functor between monoidal categories is monoidal if it is lax and oplax monoidals,
and both data give inverse isomorphisms.  -/
CategoryTheory.Functor.Monoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [CategoryTheory.MonoidalCategory D] → CategoryTheory.Functor C D → Type (max u₁ v₂)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.comp.eq_1 : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (A B C : HomologicalComplex V c)
  (φ : A.Hom B) (ψ : B.Hom C),
  A.comp B C φ ψ = { f := fun i => CategoryTheory.CategoryStruct.comp (φ.f i) (ψ.f i), comm' := ⋯ }
-- Mathlib.Algebra.Algebra.Defs
algebraMap.coe_sub : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a b : R),
  ↑(a - b) = ↑a - ↑b
-- Lean.Meta.Hint
Lean.Meta.Hint.DiffGranularity.none.sizeOf_spec : sizeOf Lean.Meta.Hint.DiffGranularity.none = 1
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.instPreservesLimitsOfShapeDiscreteWalkingPairOfIsHomological : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.rat_rawCast_neg : ∀ {n d : ℕ} {R : Type u_2} [inst : DivisionRing R],
  Rat.rawCast (Int.negOfNat n) d = (Int.negOfNat n).rawCast / d.rawCast
-- Lean.MetavarContext
Lean.instInhabitedMetavarContext : Inhabited Lean.MetavarContext
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
CategoryTheory.Functor.DenseAt.hasPointwiseLeftKanExtensionAt : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} (hf : F.DenseAt Y), F.HasPointwiseLeftKanExtensionAt F Y
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_eq_iff_eq_trop : ∀ {R : Type u} {x : Tropical R} {y : R}, Tropical.untrop x = y ↔ x = Tropical.trop y
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_conj_eq_ite : ∀ (x : ℂ), Complex.log ((starRingEnd ℂ) x) = if x.arg = Real.pi then Complex.log x else (starRingEnd ℂ) (Complex.log x)
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesLimits.conePoint_a : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra)
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t).a =
    t.lift (CategoryTheory.Monad.ForgetCreatesLimits.newCone D c)
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.map : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {len : ℕ} → (aig : Std.Sat.AIG α) → Std.Sat.AIG.RefVec.MapTarget aig len → Std.Sat.AIG.RefVecEntry α len
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.insert_sdiff_singleton_comm`. -/
Set.insert_diff_singleton_comm : ∀ {α : Type u_1} {a b : α}, a ≠ b → ∀ (s : Set α), insert a (s \ {b}) = insert a s \ {b}
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.sq.eq_1 : ∀ {R : Type u_3} {A : Type u_7} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A],
  QuadraticMap.sq = QuadraticMap.linMulLin LinearMap.id LinearMap.id
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α],
  t.WF → ∀ {k : α} {f : β k → β k}, (t.modify k f).minKey! = t.minKey!
-- Mathlib.Algebra.Module.Torsion.Pi
Pi.instModuleIsTorsionFree : ∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.IsTorsionFree R (M i)], Module.IsTorsionFree R ((i : ι) → M i)
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_int32ToBitVec : ∀ (x : Int32), Int16.ofBitVec (BitVec.signExtend 16 x.toBitVec) = x.toInt16
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertListIfNewUnit.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (hd : α) (tl : List α) (h_1 : Unit → motive [])
  (h_2 : (hd : α) → (tl : List α) → motive (hd :: tl)),
  (match hd :: tl with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_2 hd tl
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- If two ring homomorphisms from `R[M]` are equal on all `single m 1`
and `single 0 r`, then they are equal.

See note [partially-applied ext lemmas].  -/
AddMonoidAlgebra.ringHom_ext' : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddMonoid M]
  {f g : AddMonoidAlgebra R M →+* S},
  f.comp AddMonoidAlgebra.singleZeroRingHom = g.comp AddMonoidAlgebra.singleZeroRingHom →
    (↑f).comp (AddMonoidAlgebra.of R M) = (↑g).comp (AddMonoidAlgebra.of R M) → f = g
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a fallback : α}, ∅.getKeyD a fallback = fallback
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} {x y : CategoryTheory.Presieve.FamilyOfElements P R},
  (∀ {Y : C} (f : Y ⟶ X) (hf : R f), x f hf = y f hf) → x = y
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.ab_exact_iff_ker_le_range : ∀ {S : CategoryTheory.ShortComplex Ab}, S.Exact ↔ (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range
-- Mathlib.Data.Sum.Order
/-- `Equiv.sumEmpty` as an `OrderIso` with the lexicographic sum.  -/
OrderIso.sumLexEmpty : {α : Type u_1} → {β : Type u_2} → [inst : LE α] → [inst_1 : LE β] → [IsEmpty β] → α ⊕ₗ β ≃o α
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_of_not_le : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E], ¬m ≤ m₀ → μ[f | m] = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.subset_mul_right : ∀ {α : Type u_2} [inst : MulOneClass α] {s : Set α} (t : Set α), 1 ∈ s → t ⊆ s * t
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.SharedState.mk.injEq : ∀ (clientToServer serverToClient clientToServer_1 serverToClient_1 : Std.CloseableChannel ByteArray),
  ({ clientToServer := clientToServer, serverToClient := serverToClient } =
      { clientToServer := clientToServer_1, serverToClient := serverToClient_1 }) =
    (clientToServer = clientToServer_1 ∧ serverToClient = serverToClient_1)
-- Mathlib.Tactic.SetNotationForOrder
/-- `UsesSetNotationForOrder` is used to track whether a type is tagged with
`@[use_set_notation_for_order]`.  -/
UsesSetNotationForOrder : Type u_1 → Type
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.instRing : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type u_3} → [inst_1 : Ring A] → [inst_2 : Algebra R A] → {S : Submonoid R} → Ring (LocalizedModule S A)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_empty : ∀ {ι : Type u_1} {M : Type u_3} {f : ι → M} [inst : CommMonoid M], ∏ x ∈ ∅, f x = 1
-- Mathlib.Logic.Equiv.Option
Equiv.removeNoneAux_some : ∀ {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α},
  (∃ x', e (some x) = some x') → some (e.removeNoneAux x) = e (some x)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} {z₁ z₂ : CochainComplex.HomComplex.Cocycle F G n}, ↑z₁ = ↑z₂ → z₁ = z₂
-- Mathlib.CategoryTheory.Localization.Bifunctor
/-- Given functors `L₁ : C₁ ⥤ D₁`, `L₂ : C₂ ⥤ D₂`, morphisms properties `W₁` on `C₁`
and `W₂` on `C₂`, and functors `F : C₁ ⥤ C₂ ⥤ E` and `F' : D₁ ⥤ D₂ ⥤ E`, we say
`Lifting₂ L₁ L₂ W₁ W₂ F F'` holds if `F` is induced by `F'`, up to an isomorphism.  -/
CategoryTheory.Localization.Lifting₂ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                    CategoryTheory.Functor C₁ D₁ →
                      CategoryTheory.Functor C₂ D₂ →
                        CategoryTheory.MorphismProperty C₁ →
                          CategoryTheory.MorphismProperty C₂ →
                            CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E) →
                              CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E) → Type (max (max u_1 u_2) v_5)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Iso.sumCongr_symm_apply : ∀ {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W}
  {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H') (a : V' ⊕ W'),
  (RelIso.symm (f.sumCongr g)) a = Sum.map (⇑f.symm) (⇑g.symm) a
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.inv_r : ∀ {n : ℕ} (i : ZMod n), (DihedralGroup.r i)⁻¹ = DihedralGroup.r (-i)
-- Init.Data.Option.Lemmas
Option.min_join_right : ∀ {α : Type u_1} [inst : Min α] {o : Option α} {o' : Option (Option α)}, o ⊓ o'.join = (some o ⊓ o').join
-- Mathlib.Analysis.Convex.Cone.InnerDual
/-- Dual cone of the convex cone `{0}` is the total space.  -/
ProperCone.innerDual_zero : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E],
  ProperCone.innerDual 0 = ⊤
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- If one controls the seminorm for every `x`, then one controls the seminorm.

Variant for functions `𝓢(ℝ, F)`.  -/
SchwartzMap.seminorm_le_bound' : ∀ (𝕜 : Type u_2) {F : Type u_6} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [inst_2 : NormedField 𝕜]
  [inst_3 : NormedSpace 𝕜 F] [inst_4 : SMulCommClass ℝ 𝕜 F] (k n : ℕ) (f : SchwartzMap ℝ F) {M : ℝ},
  0 ≤ M → (∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ M) → (SchwartzMap.seminorm 𝕜 k n) f ≤ M