mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contSupp.eq_def : ∀ (x : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.contSupp x =
    match x with
    | Turing.PartrecToTM2.Cont'.cons₁ fs k =>
      Turing.PartrecToTM2.trStmts₁
          (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.aux
            (Turing.PartrecToTM2.move₂ (fun s => decide (s = Turing.PartrecToTM2.Γ'.consₗ)) Turing.PartrecToTM2.K'.stack
              Turing.PartrecToTM2.K'.main
              (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.aux Turing.PartrecToTM2.K'.stack
                (Turing.PartrecToTM2.trNormal fs k.cons₂)))) ∪
        (Turing.PartrecToTM2.codeSupp' fs k.cons₂ ∪
          (Turing.PartrecToTM2.trStmts₁
              (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)) ∪
            Turing.PartrecToTM2.contSupp k))
    | k.cons₂ =>
      Turing.PartrecToTM2.trStmts₁
          (Turing.PartrecToTM2.head Turing.PartrecToTM2.K'.stack (Turing.PartrecToTM2.Λ'.ret k)) ∪
        Turing.PartrecToTM2.contSupp k
    | Turing.PartrecToTM2.Cont'.comp f k => Turing.PartrecToTM2.codeSupp' f k ∪ Turing.PartrecToTM2.contSupp k
    | Turing.PartrecToTM2.Cont'.fix f k => Turing.PartrecToTM2.codeSupp' f.fix k ∪ Turing.PartrecToTM2.contSupp k
    | Turing.PartrecToTM2.Cont'.halt => ∅
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.rightUnitor_inv_apply : ∀ {R : Type u} [inst : CommSemiring R] {M : SemimoduleCat R} (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv) m = m ⊗ₜ[R] 1
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.add_comm : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x y : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (x.add y) (y.add x)
-- Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
CategoryTheory.Preadditive.DoldKan.equivalence_inverse : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Preadditive.DoldKan.equivalence.inverse = CategoryTheory.Preadditive.DoldKan.Γ
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The condition that a functor `F` has a pointwise right Kan extension along `L` at `Y`.
It means that the functor `StructuredArrow.proj Y L ⋙ F : StructuredArrow Y L ⥤ H`
has a limit.  -/
CategoryTheory.Functor.HasPointwiseRightKanExtensionAt : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            CategoryTheory.Functor C D → CategoryTheory.Functor C H → D → Prop
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequence_exact₁ : ∀ {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] [inst_8 : F.IsHomological] [inst_9 : F.ShiftSequence ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
  { X₁ := (F.shift n₀).obj T.obj₃, X₂ := (F.shift n₁).obj T.obj₁, X₃ := (F.shift n₁).obj T.obj₂,
      f := F.homologySequenceδ T n₀ n₁ h, g := (F.shift n₁).map T.mor₁, zero := ⋯ }.Exact
-- Mathlib.RingTheory.Ideal.Maps
RingHom.injective_iff_ker_eq_bot : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Ring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] (f : F), Function.Injective ⇑f ↔ RingHom.ker f = ⊥
-- Mathlib.Analysis.MeanInequalities
/-- **AM-GM inequality - equality condition**.
The condition is that all elements of `z` are equal to each other;
see `geom_mean_eq_arith_mean_weighted_iff_of_pos'` for a version that compares the elements to their
center of mass `∑ i ∈ s, w i * z i` instead.  -/
Real.geom_mean_eq_arith_mean_weighted_iff_of_pos : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 < w i) →
    ∑ i ∈ s, w i = 1 → (∀ i ∈ s, 0 ≤ z i) → (∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, ∀ k ∈ s, z j = z k)
-- Mathlib.Data.NNReal.Defs
NNReal.smulCommClass_left : ∀ {M : Type u_1} {N : Type u_2} [inst : MulAction ℝ N] [inst_1 : SMul M N] [SMulCommClass ℝ M N],
  SMulCommClass NNReal M N
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.property_ofPostconditionT : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] {x : Std.Iterators.PostconditionT m α},
  (Std.Iterators.HetT.ofPostconditionT x).Property = x.Property
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.toZFSet_add_one : ∀ (o : Ordinal.{u_1}), (o + 1).toZFSet = insert o.toZFSet o.toZFSet
-- Init.Sym.Lemmas
Lean.Sym.Char.le_eq_false : ∀ (a b : Char), decide (a ≤ b) = false → (a ≤ b) = False
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- An intermediate field is closed under subtraction.  -/
IntermediateField.sub_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {x y : L}, x ∈ S → y ∈ S → x - y ∈ S
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCommSq.valuationRing : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (self : AlgebraicGeometry.ValuativeCommSq f), ValuationRing self.R
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) l →
          k ∈ List.map Prod.fst l → ∀ {h' : k' ∈ m.insertMany l}, (m.insertMany l).getKey k' h' = k
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.restrict_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] (f : MeasureTheory.SimpleFunc α β),
  f.restrict Set.univ = f
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Combinators.Monadic.FlatMap.0.Std.Iterators.Types.Flatten.Rel : (α : Type w) →
  {α₂ : Type w} →
    (β : Type w) →
      (m : Type w → Type w') →
        [Monad m] →
          [inst : Std.Iterator α m (Std.IterM m β)] →
            [inst_1 : Std.Iterator α₂ m β] →
              [Std.Iterators.Finite α m] → [Std.Iterators.Finite α₂ m] → Std.IterM m β → Std.IterM m β → Prop
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, a ∈ m → m.getKey? a = some (m.getKey! a)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.Adj.of_spanningCoe : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {u v : ↑G'.verts}, G'.spanningCoe.Adj ↑u ↑v → G.Adj ↑u ↑v
-- Std.Time.Date.PlainDate
Std.Time.instDecidableEqPlainDate.decEq : (x x_1 : Std.Time.PlainDate) → Decidable (x = x_1)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
CauchySeq.neg : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  [inst_3 : Preorder ι] {u : ι → α}, CauchySeq u → CauchySeq (-u)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec.map_comp_assoc : ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map g)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) h)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.toSingleMk_postcomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0) {X' : C}
  (g : X ⟶ X'),
  CochainComplex.HomComplex.Cocycle.toSingleMk (CategoryTheory.CategoryStruct.comp f g) h p' hp' ⋯ =
    (CochainComplex.HomComplex.Cocycle.toSingleMk f h p' hp' hf).postcomp ((CochainComplex.singleFunctor C q).map g)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.inverse'_apply : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  {φ' : N → M} (f : X →ₑ[φ] Y) (g : Y → X) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g ⇑f)
  (h₂ : Function.RightInverse g ⇑f) (a : Y), (f.inverse' g k h₁ h₂) a = g a
-- Mathlib.Algebra.Group.Submonoid.Membership
Int.natMod.eq_1 : ∀ (m n : ℤ), m.natMod n = (m % n).toNat
-- Init.SimpLemmas
have_body_congr' : ∀ {α : Sort u} {β : Sort v} (a : α) {f f' : α → β}, (∀ (x : α), f x = f' x) → f a = f' a
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.id.match_1.eq_1 : ∀ {C : Type u_1} (motive : CategoryTheory.WithTerminal C → Sort u_2) (a : C)
  (h_1 : (a : C) → motive (CategoryTheory.WithTerminal.of a)) (h_2 : Unit → motive CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.of a with
    | CategoryTheory.WithTerminal.of a => h_1 a
    | CategoryTheory.WithTerminal.star => h_2 ()) =
    h_1 a
-- Mathlib.Data.Finset.Erase
Finset.coe_erase : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), ↑(s.erase a) = ↑s \ {a}
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_image : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α]
  {f : β → α} [inst_2 : DecidableEq β] {g : γ → β} (s : Finset γ), (Finset.image g s).gcd f = s.gcd (f ∘ g)
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
/-- Composing the `V`-enriched identity functor with any functor is isomorphic to that functor.  -/
CategoryTheory.EnrichedCat.leftUnitor : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₁} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              (F : CategoryTheory.EnrichedFunctor V C D) →
                CategoryTheory.EnrichedFunctor.comp V (CategoryTheory.EnrichedFunctor.id V C) F ≅ F
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.transnumAuxSeq_def : ∀ (f : CircleDeg1Lift), f.transnumAuxSeq = fun n => (f ^ 2 ^ n) 0 / 2 ^ n
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.id_apply : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (x : P),
  AffineIsometry.id x = x
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.getLastI.match_1.eq_4 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (head head_1 : α) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → motive [a]) (h_3 : (head b : α) → motive [head, b])
  (h_4 : (head head_2 : α) → (l : List α) → motive (head :: head_2 :: l)),
  (l = [] → False) →
    (match head :: head_1 :: l with
      | [] => h_1 ()
      | [a] => h_2 a
      | [head, b] => h_3 head b
      | head :: head_2 :: l => h_4 head head_2 l) =
      h_4 head head_1 l
-- Mathlib.CategoryTheory.Equivalence
/-- Equivalence of categories is reflexive.  -/
CategoryTheory.Equivalence.refl : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → C ≌ C
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Context : Type
-- Mathlib.Algebra.WithConv
WithConv.instAddCommMonoid : {A : Type u_2} → [AddCommMonoid A] → AddCommMonoid (WithConv A)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.right_inv : ∀ {𝕜 : 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) {x : E},
  x ∈ Set.range ↑I → ↑I (↑I.symm x) = x
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.case.injEq : ∀ (a a_1 a_2 a_3 : Turing.ToPartrec.Code), (a.case a_1 = a_2.case a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSES_mor₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact),
  (DerivedCategory.triangleOfSES hS).mor₁ = DerivedCategory.Q.map S.f
-- Mathlib.Topology.Constructible
/-- A constructible set is a set that can be written as the
finite union/finite intersection/complement of open retrocompact sets.

In other words, constructible sets form the Boolean subalgebra generated by open retrocompact sets.
 -/
Topology.IsConstructible : {X : Type u_2} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_lt_iff_lt_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b c : α}, a - c < b ↔ a < b + c
-- Mathlib.RingTheory.Derivation.Basic
Derivation.leibniz_invOf : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M) (a : A)
  [inst_6 : Invertible a], D ⅟a = -⅟a ^ 2 • D a
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- Completeness of the uniform structure on `PowerSeries`  -/
PowerSeries.WithPiTopology.instCompleteSpace : ∀ (R : Type u_1) [inst : UniformSpace R] [CompleteSpace R], CompleteSpace (PowerSeries R)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
CurveIntegrable.neg : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b}, CurveIntegrable ω γ → CurveIntegrable (-ω) γ
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `Zero` across an `Equiv`  -/
Equiv.zero : {α : Type u_2} → {β : Type u_3} → α ≃ β → [Zero β] → Zero α
-- Batteries.Tactic.Lint.Frontend
/-- `getChecks slow runOnly runAlways` produces a list of linters.
`runOnly` is an optional list of names that should resolve to declarations with type `NamedLinter`.
If populated, only these linters are run (regardless of the default configuration).
`runAlways` is an optional list of names that should resolve to declarations with type
`NamedLinter`. If populated, these linters are always run (regardless of their configuration).
Specifying a linter in `runAlways` but not `runOnly` is an error.
Otherwise, it uses all enabled linters in the environment tagged with `@[env_linter]`.
If `slow` is false, it only uses the fast default tests.  -/
Batteries.Tactic.Lint.getChecks : Bool → Option (List Lean.Name) → Option (List Lean.Name) → Lean.CoreM (Array Batteries.Tactic.Lint.NamedLinter)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toLinearEquiv_refl : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E],
  (LinearIsometryEquiv.refl R E).toLinearEquiv = LinearEquiv.refl R E
-- Lean.Expr
Lean.Expr.projIdx! : Lean.Expr → ℕ
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.swapRight_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α),
  κ.swapRight a = MeasureTheory.Measure.map Prod.swap (κ a)
-- Mathlib.Data.Finset.Image
Finset.image_id' : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α], Finset.image (fun x => x) s = s
-- Mathlib.CategoryTheory.Shift.ShiftSequence
/-- compatibility isomorphism with the shift  -/
CategoryTheory.Functor.ShiftSequence.shiftIso : {C : Type u_1} →
  {A : Type u_3} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Category.{v_3, u_3} A} →
        {F : CategoryTheory.Functor C A} →
          {M : Type u_4} →
            {inst_2 : AddMonoid M} →
              {inst_3 : CategoryTheory.HasShift C M} →
                [self : F.ShiftSequence M] →
                  (n a a' : M) →
                    n + a = a' →
                      ((CategoryTheory.shiftFunctor C n).comp (CategoryTheory.Functor.ShiftSequence.sequence F a) ≅
                        CategoryTheory.Functor.ShiftSequence.sequence F a')
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.add_inf_assoc : ∀ {G : Type u_2} [inst : AddGroup G] (A B C : AddSubgroup G), A ≤ C → ↑A + ↑(B ⊓ C) = (↑A + ↑B) ∩ ↑C
-- Mathlib.Algebra.MonoidAlgebra.Support
/-- **Alias** of `MonoidAlgebra.support_coeff_mul_subset`. -/
MonoidAlgebra.support_single_mul_eq_image : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : DecidableEq G] (x y : MonoidAlgebra k G),
  (x * y).coeff.support ⊆ x.coeff.support * y.coeff.support
-- Mathlib.Data.Int.Cast.Lemmas
Int.castRingHom_int : Int.castRingHom ℤ = RingHom.id ℤ
-- Init.Data.List.TakeDrop
List.drop_left' : ∀ {α : Type u_1} {l₁ l₂ : List α} {i : ℕ}, l₁.length = i → List.drop i (l₁ ++ l₂) = l₂
-- Mathlib.Tactic.DeriveCountable
/-- Constructs a function from the inductive type to `Nat`.  -/
Mathlib.Deriving.Countable.mkToNatFuns : Lean.Elab.Deriving.Context → Array Lean.Name → Lean.Elab.TermElabM (Lean.TSyntax `command)
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
mdifferentiable_chart : ∀ {𝕜 : 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] [IsManifold I 1 M] (x : M),
  OpenPartialHomeomorph.MDifferentiable I I (chartAt H x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_map_app_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (φ : S ⟶ S') (x : X),
  (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.map φ).app x).fst = φ.fst.app x
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.StAct.push : {K : Type u_1} → {Γ : K → Type u_2} → {σ : Type u_4} → {k : K} → (σ → Γ k) → Turing.TM2to1.StAct K Γ σ k
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.mul_end : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f g : Function.End α} {Kf Kg : NNReal},
  LipschitzWith Kf f → LipschitzWith Kg g → LipschitzWith (Kf * Kg) (f * g)
-- Mathlib.Topology.Algebra.Algebra.Equiv
/-- `Equiv.cast (congrArg _ h)` as a continuous algebra equiv.

Note that unlike `Equiv.cast`, this takes an equality of indices rather than an equality of types,
to avoid having to deal with an equality of the algebraic structure itself.  -/
ContinuousAlgEquiv.cast : {R : Type u_1} →
  [inst : CommSemiring R] →
    {ι : Type u_5} →
      {A : ι → Type u_6} →
        [inst_1 : (i : ι) → Semiring (A i)] →
          [inst_2 : (i : ι) → Algebra R (A i)] →
            [inst_3 : (i : ι) → TopologicalSpace (A i)] → {i j : ι} → i = j → A i ≃A[R] A j
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.hasEigenvalue_eigenvalues : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
  (i : Fin n), Module.End.HasEigenvalue T ↑(hT.eigenvalues hn i)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.foldM_filterMapWithPostcondition.match_1.splitter : {γ : Type u_1} →
  (motive : Option γ → Sort u_2) →
    (__x : Option γ) →
      ((c : γ) → motive (some c)) → ((x : Option γ) → (∀ (c : γ), x = some c → False) → motive x) → motive __x
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- Reinterpret a `NonUnitalSubalgebra` as a `Submodule`.  -/
NonUnitalSubalgebra.toSubmodule : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : Module R A] → NonUnitalSubalgebra R A → Submodule R A
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.leftUnitor_inv_app_apply : ∀ (K : SSet) {Δ : SimplexCategoryᵒᵖ} (x : K.obj Δ),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor (K.obj Δ)).inv) x =
    (PUnit.unit, x)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget.x : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {outWidth : ℕ} →
          (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget aig outWidth) → aig.RefVec self.w
-- Mathlib.Algebra.Order.Round
round_eq_zero_iff : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] {x : α},
  round x = 0 ↔ x ∈ Set.Ico (-(1 / 2)) (1 / 2)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_insertIfNew_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {v : β}, (cmp (t.insertIfNew k v).minKey! k).isLE = true
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.StrictOrLazy.strict.inj : ∀ {α β : Type} {a a_1 : α}, Lean.Widget.StrictOrLazy.strict a = Lean.Widget.StrictOrLazy.strict a_1 → a = a_1
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.addHom_ext'_iff : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {γ : Type u_1}
  [inst_2 : AddZeroClass γ] {f g : (DirectSum ι fun i => β i) →+ γ},
  f = g ↔ ∀ (i : ι), f.comp (DirectSum.of β i) = g.comp (DirectSum.of β i)
-- Mathlib.RingTheory.Regular.RegularSequence
/-- A sequence `[r₁, …, rₙ]` is weakly regular on `M` iff `rᵢ` is regular on
`M⧸(r₁, …, rᵢ₋₁)M` for all `1 ≤ i ≤ n`.  -/
RingTheory.Sequence.IsWeaklyRegular : {R : Type u_1} → (M : Type u_3) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → List R → Prop
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.union_div_inter_subset_union : ∀ {α : Type u_2} [inst : Div α] {s₁ s₂ t₁ t₂ : Set α}, (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂
-- Mathlib.Order.Bounds.Image
Monotone.mem_lowerBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ {a : α} {s : Set α}, a ∈ lowerBounds s → f a ∈ lowerBounds (f '' s)
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.below.succ : ∀ {motive : {n : ℕ} → (a : List.Vector ℕ n → ℕ) → Nat.Primrec' a → Prop}, Nat.Primrec'.below Nat.Primrec'.succ
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
Continuous.nndist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {f g : β → α},
  Continuous f → Continuous g → Continuous fun b => nndist (f b) (g b)
-- Lean.Elab.Do.InferControlInfo
/-- The `do` block syntactically contains a `continue`.  -/
Lean.Elab.Do.ControlInfo.continues : Lean.Elab.Do.ControlInfo → Bool