mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.localInverse_contMDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x), ContMDiffAt J I n (↑hf.localInverse.toPartialEquiv) (f x)
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.composePath_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : CategoryTheory.Paths C},
  CategoryTheory.composePath (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.id
      (have this := X;
      this)
-- Mathlib.GroupTheory.FiniteAbelian.Duality
/-- The cardinality of the dual subgroup of `G →* Mˣ` associated to a subgroup `H` of `G`
equals the index of `H` in `G`.  -/
CommGroup.card_subgroupOrderIsoSubgroupMonoidHom : ∀ {G : Type u_1} (M : Type u_2) [inst : CommGroup G] [inst_1 : Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G),
  Nat.card ↥(OrderDual.ofDual ((CommGroup.subgroupOrderIsoSubgroupMonoidHom G M) H)) = Nat.card (G ⧸ H)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_mul_ideal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (I J : Ideal A),
  ProjectiveSpectrum.zeroLocus 𝒜 ↑(I * J) = ProjectiveSpectrum.zeroLocus 𝒜 ↑I ∪ ProjectiveSpectrum.zeroLocus 𝒜 ↑J
-- Mathlib.Algebra.Group.Basic
sub_add_add_cancel : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b c : G), a - c + (b + c) = a + b
-- Aesop.Stats.Basic
Aesop.instInhabitedForwardClusterStateStats.default : Aesop.ForwardClusterStateStats
-- Mathlib.Analysis.Convex.Topology
/-- **Alias** of `Convex.nhdsWithin_sdiff_eq_nhdsNE`. -/
Convex.nhdsWithin_diff_eq_nhdsNE : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜},
  Convex 𝕜 s →
    ∀ {a : 𝕜},
      a ∈ closure s → (s ∩ Set.Iio a).Nonempty → (s ∩ Set.Ioi a).Nonempty → nhdsWithin a (s \ {a}) = nhdsWithin a {a}ᶜ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k},
  t.WF → (Std.DTreeMap.Raw.filterMap f t).getD k fallback = ((t.get? k).bind (f k)).getD fallback
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.first_num_eq : ∀ {K : Type u_1} {g : GenContFract K} [inst : DivisionRing K] {gp : GenContFract.Pair K},
  g.s.get? 0 = some gp → g.nums 1 = gp.b * g.h + gp.a
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} ⦃X₁ X₂ : C⦄
  ⦃M₁ : ↑(F.obj { as := Opposite.op X₁ })⦄ ⦃M₂ : ↑(F.obj { as := Opposite.op X₂ })⦄ ⦃Y : C⦄ ⦃f₁ : Y ⟶ X₁⦄ ⦃f₂ : Y ⟶ X₂⦄
  (φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂) ⦃Y' : C⦄ (g : Y' ⟶ Y)
  (gf₁ : Y' ⟶ X₁) (gf₂ : Y' ⟶ X₂) (hgf₁ : CategoryTheory.CategoryStruct.comp g f₁ = gf₁)
  (hgf₂ : CategoryTheory.CategoryStruct.comp g f₂ = gf₂),
  (F.map g.op.toLoc).toFunctor.map φ =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).inv.toNatTrans.app M₁)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom φ g gf₁ gf₂ hgf₁ hgf₂)
        ((F.mapComp' f₂.op.toLoc g.op.toLoc gf₂.op.toLoc ⋯).hom.toNatTrans.app M₂))
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instUnionOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Union (Std.ExtHashMap α β)
-- Init.Data.String.Pattern.Basic
/-- A lawful forward pattern is one where the three functions `ForwardPattern.skipPrefix?`,
`ForwardPattern.skipPrefixOfNonempty?` and `ForwardPattern.startsWith` agree for any
given input slice.

Note that this is a relatively weak condition. It is non-uniform in the sense that the functions
can still return completely different results on different slices, even if they represent the same
string.

There is a stronger lawfulness typeclass `LawfulForwardPatternModel` that asserts that the
`ForwardPattern.skipPrefix?` function behaves like a function that drops the longest prefix
according to some notion of matching.
 -/
String.Slice.Pattern.LawfulForwardPattern : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → Prop
-- Mathlib.Data.Sum.Interval
Finset.sumLift₂.eq_4 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  (f : α₁ → β₁ → Finset γ₁) (g : α₂ → β₂ → Finset γ₂) (a : α₂) (b : β₂),
  Finset.sumLift₂ f g (Sum.inr a) (Sum.inr b) = Finset.map Function.Embedding.inr (g a b)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves binary biproducts if it preserves the binary biproduct of `X` and `Y`
for all `X` and `Y`.  -/
CategoryTheory.Limits.PreservesBinaryBiproducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) → [F.PreservesZeroMorphisms] → Prop
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.equivariantOfLinearOfComm_apply : ∀ {R : Type u_1} {M : Type u_7} [inst : Monoid M] [inst_1 : CommSemiring R] {V : Type u_10} {W : Type u_11}
  [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : Module (MonoidAlgebra R M) V]
  [inst_5 : IsScalarTower R (MonoidAlgebra R M) V] [inst_6 : AddCommMonoid W] [inst_7 : Module R W]
  [inst_8 : Module (MonoidAlgebra R M) W] [inst_9 : IsScalarTower R (MonoidAlgebra R M) W] (f : V →ₗ[R] W)
  (h : ∀ (g : M) (v : V), f (MonoidAlgebra.single g 1 • v) = MonoidAlgebra.single g 1 • f v) (v : V),
  (MonoidAlgebra.equivariantOfLinearOfComm f h) v = f v
-- Mathlib.Algebra.Module.Defs
Module.eq_zero_of_zero_eq_one : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [Module R M] (x : M), 0 = 1 → x = 0
-- Mathlib.Computability.Encoding
/-- Deprecated alias for `Encoding.card_le_aleph0`.  -/
Computability.FinEncoding.card_le_aleph0 : ∀ {α : Type u_1} {Γ : Type u_2} [Countable Γ] (e : Computability.Encoding α Γ), Cardinal.mk α ≤ Cardinal.aleph0
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.Measurable.eval_cylinderEvents : ∀ {α : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {mα : MeasurableSpace α} [m : (i : ι) → MeasurableSpace (X i)]
  {Δ : Set ι} {i : ι} {g : α → (i : ι) → X i}, i ∈ Δ → Measurable g → Measurable fun a => g a i
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_mul_left_nhdsLT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousMul H] {c a : H},
  Filter.map (fun x => c * x) (nhdsWithin a (Set.Iio a)) = nhdsWithin (c * a) (Set.Iio (c * a))
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.isOrdinal_empty : ∅.IsOrdinal
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.instInvertibleInv : {n : Type u'} →
  {α : Type v} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing α] → (A : Matrix n n α) → [Invertible A] → Invertible A⁻¹
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_pair : ∀ {X : Type u_1} {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F]
  [CompleteSpace E] [CompleteSpace F] {f : X → E} {g : X → F},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → ∫ (x : X), (f x, g x) ∂μ = (∫ (x : X), f x ∂μ, ∫ (x : X), g x ∂μ)
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
PrimeSpectrum.finite_of_toPiLocalization_surjective : ∀ {R : Type u_1} [inst : CommSemiring R],
  Function.Surjective ⇑(PrimeSpectrum.toPiLocalization R) → Finite (PrimeSpectrum R)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
IsCyclotomicExtension.Rat.Three.coe_eta : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3), ↑⋯.unit = hζ.toInteger
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_app_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (f : Φ.presheafFiber.obj P ⟶ M) (X : C) (x : Φ.fiber.obj X),
  CategoryTheory.CategoryStruct.comp ((Φ.skyscraperPresheafHomEquiv f).app (Opposite.op X))
      (CategoryTheory.Limits.Pi.π (fun x => M) x) =
    CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) f
-- Mathlib.MeasureTheory.Group.GeometryOfNumbers
ConvexBody.mk.congr_simp : ∀ {V : Type u_2} [inst : TopologicalSpace V] [inst_1 : AddCommMonoid V] [inst_2 : SMul ℝ V] (carrier carrier_1 : Set V)
  (e_carrier : carrier = carrier_1) (convex' : Convex ℝ carrier) (isCompact' : IsCompact carrier)
  (nonempty' : carrier.Nonempty),
  { carrier := carrier, convex' := convex', isCompact' := isCompact', nonempty' := nonempty' } =
    { carrier := carrier_1, convex' := ⋯, isCompact' := ⋯, nonempty' := ⋯ }
-- Mathlib.Algebra.Group.Action.Equidecomp
/-- The composition of two equidecompositions as an equidecomposition.  -/
Equidecomp.trans : {X : Type u_1} →
  {G : Type u_2} → [inst : Monoid G] → [inst_1 : MulAction G X] → Equidecomp X G → Equidecomp X G → Equidecomp X G
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.foldlM.match_1.splitter : {σ : Type u_3} →
  {α : Type u_1} →
    (motive : σ → RBTree.RBNode α → Sort u_2) →
      (x : σ) →
        (x_1 : RBTree.RBNode α) →
          ((b : σ) → motive b RBTree.RBNode.nil) →
            ((b : σ) →
                (c : RBTree.RBColor) →
                  (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive b (RBTree.RBNode.node c l v r)) →
              motive x x_1
-- Mathlib.Data.Set.Image
Set.preimage_eq_iff_eq_image : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Bijective f → ∀ {s : Set β} {t : Set α}, f ⁻¹' s = t ↔ s = f '' t
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_cancel_left : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m : M) (s₁ s₂ : ↥S),
  IsLocalizedModule.mk' f (s₁ • m) (s₁ * s₂) = IsLocalizedModule.mk' f m s₂
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.long_eq_three_mul_short : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (B : P.InvariantForm),
  (B.form (RootPairing.EmbeddedG2.longRoot P)) (RootPairing.EmbeddedG2.longRoot P) =
    3 * (B.form (RootPairing.EmbeddedG2.shortRoot P)) (RootPairing.EmbeddedG2.shortRoot P)
-- Mathlib.NumberTheory.Cyclotomic.Gal
IsCyclotomicExtension.zeta.congr_simp : ∀ (n n_1 : ℕ) (e_n : n = n_1) [inst : NeZero n] (A : Type w) (B : Type z) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [inst_4 : IsCyclotomicExtension {n} A B],
  IsCyclotomicExtension.zeta n A B = IsCyclotomicExtension.zeta n_1 A B
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_symm : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} [inst_3 : IsDedekindDomain R] (f : R ⧸ I ≃+* A ⧸ J) (hI : I ≠ ⊥) (hJ : J ≠ ⊥),
  (IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv f hI hJ).symm =
    IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv f.symm hJ hI
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiff.mk.inj : ∀ {changesBefore changesAfter changesBefore_1 changesAfter_1 : Lean.SubExpr.PosMap Lean.Widget.ExprDiffTag✝},
  { changesBefore := changesBefore, changesAfter := changesAfter } =
      { changesBefore := changesBefore_1, changesAfter := changesAfter_1 } →
    changesBefore = changesBefore_1 ∧ changesAfter = changesAfter_1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DeclarationParams.toTextDocumentPositionParams : Lean.Lsp.DeclarationParams → Lean.Lsp.TextDocumentPositionParams
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.eval_nodal_not_at_node : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [Nontrivial R] [NoZeroDivisors R]
  {x : R}, (∀ i ∈ s, x ≠ v i) → Polynomial.eval x (Lagrange.nodal s v) ≠ 0
-- Init.Data.SInt.Bitwise
ISize.xor_comm : ∀ (a b : ISize), a ^^^ b = b ^^^ a
-- Lean.Meta.Sym.ExprPtr
Lean.Meta.Sym.instHashableExprPtr : Hashable Lean.Meta.Sym.ExprPtr
-- Mathlib.Topology.Order.LeftRightLim
tendsto_leftLim_atBot_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [T3Space β] {f : α → β} {b : β},
  Filter.Tendsto f Filter.atBot (nhds b) → Filter.Tendsto (Function.leftLim f) Filter.atBot (nhds b)
-- Aesop.Builder.Tactic
Aesop.RuleBuilder.tactic : Aesop.RuleBuilder
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- Explicit description of the kernel functions of `OfKernel K`.
This is marked as private because it equals `RKHS.kerFun`. However, it must be defined separately
since the `RKHS.kerFun` spelling depends on the `RKHS (OfKernel K)` instance, which itself
depends on `OfKernel.kerFun`.  -/
_private.Mathlib.Analysis.InnerProductSpace.Reproducing.0.RKHS.OfKernel.kerFun : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {X : Type u_2} →
      {V : Type u_3} →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            [inst_3 : CompleteSpace V] →
              (K : Matrix X X (V →L[𝕜] V)) →
                [inst_4 : Fact K.PosSemidef] → X → V →L[𝕜] UniformSpace.Completion (RKHS.H₀ K)
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
AlgebraicIndependent.aevalEquiv_apply_coe : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (hx : AlgebraicIndependent R x) (a : MvPolynomial ι R),
  ↑(hx.aevalEquiv a) = (MvPolynomial.aeval x) a
-- Mathlib.Condensed.TopCatAdjunction
/-- Auxiliary definition to define the topology on `X(*)` for a condensed set `X`.  -/
_private.Mathlib.Condensed.TopCatAdjunction.0.CondensedSet.coinducingCoprod : (X : CondensedSet) →
  (i : (S : CompHaus) × X.obj.obj (Opposite.op S)) × ↑i.fst.toTop → X.obj.obj (Opposite.op (CompHaus.of PUnit.{u + 1}))
-- Mathlib.Data.Seq.Basic
Stream'.Seq.get?_enum : ∀ {α : Type u} (s : Stream'.Seq α) (n : ℕ), s.enum.get? n = Option.map (Prod.mk n) (s.get? n)
-- Mathlib.Topology.Order.LeftRightLim
leftLim_eq_of_eq_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [hα : TopologicalSpace α]
  [h'α : OrderTopology α] (f : α → β) {a : α}, nhdsWithin a (Set.Iio a) = ⊥ → Function.leftLim f a = f a
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.brecOn_2.eq : ∀ {motive_1 : Lean.IR.Alt → Sort u} {motive_2 : Lean.IR.FnBody → Sort u} {motive_3 : Array Lean.IR.Alt → Sort u}
  {motive_4 : List Lean.IR.Alt → Sort u} (t : List Lean.IR.Alt) (F_1 : (t : Lean.IR.Alt) → t.below → motive_1 t)
  (F_2 : (t : Lean.IR.FnBody) → t.below → motive_2 t)
  (F_3 : (t : Array Lean.IR.Alt) → Lean.IR.Alt.below_1 t → motive_3 t)
  (F_4 : (t : List Lean.IR.Alt) → Lean.IR.Alt.below_2 t → motive_4 t),
  Lean.IR.Alt.brecOn_2 t F_1 F_2 F_3 F_4 = F_4 t (Lean.IR.Alt.brecOn_2.go t F_1 F_2 F_3 F_4).2
-- Mathlib.LinearAlgebra.Prod
LinearMap.graph_eq_range_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂), f.graph = (LinearMap.id.prod f).range
-- Mathlib.Order.Category.HeytAlg
HeytAlg.forget_map : ∀ {X Y : HeytAlg} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget HeytAlg).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.Stable.of_le : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {F : I.Filtration M} [IsNoetherianRing R] [Module.Finite R M], F.Stable → ∀ {F' : I.Filtration M}, F' ≤ F → F'.Stable
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelDesc_zero : ∀ {X Y Z : SemiNormedGrp} {f : X ⟶ Y}, SemiNormedGrp.explicitCokernelDesc ⋯ = 0
-- Mathlib.CategoryTheory.EqToHom
/-- Proving equality between functors using heterogeneous equality.  -/
CategoryTheory.Functor.hext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D},
  (∀ (X : C), F.obj X = G.obj X) → (∀ (X Y : C) (f : X ⟶ Y), F.map f ≍ G.map f) → F = G
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_exchange : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α},
  e ∈ M.closure (insert f X) \ M.closure X → f ∈ M.closure (insert e X) \ M.closure X
-- Mathlib.Analysis.Normed.Ring.Lemmas
antilipschitzWith_mul_left : ∀ {α : Type u_1} [inst : NonUnitalNormedRing α] [NormMulClass α] {a : α},
  a ≠ 0 → AntilipschitzWith ‖a‖₊⁻¹ fun x => a * x
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.Functor.commShiftUnop_commShiftIso : ∀ {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] (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] (F : CategoryTheory.Functor C D)
  [inst_5 : (CategoryTheory.OppositeShift.functor A F).CommShift A] (a : A),
  CategoryTheory.Functor.commShiftIso F a =
    CategoryTheory.NatIso.removeOp
      (CategoryTheory.Functor.commShiftIso (CategoryTheory.OppositeShift.functor A F) a).symm
-- Mathlib.Topology.Category.Profinite.Product
/-- The functor from the poset of finsets of `ι` to  `Profinite`, indexing the limit.  -/
Profinite.indexFunctor : {ι : Type u} →
  {X : ι → Type} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {C : Set ((i : ι) → X i)} →
        [∀ (i : ι), T2Space (X i)] →
          [∀ (i : ι), TotallyDisconnectedSpace (X i)] → IsCompact C → CategoryTheory.Functor (Finset ι)ᵒᵖ Profinite
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonUnitalNonAssocSemiring : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [Add M] → NonUnitalNonAssocSemiring (AddMonoidAlgebra R M)
-- Init.Omega.Constraint
/-- `positivize` and `normalize`, returning `none` if neither does anything.  -/
Lean.Omega.tidy? : Lean.Omega.Constraint × Lean.Omega.Coeffs → Option (Lean.Omega.Constraint × Lean.Omega.Coeffs)
-- Mathlib.Topology.Algebra.Monoid
continuous_finprod : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : CommMonoid M] [ContinuousMul M] {f : ι → X → M},
  (∀ (i : ι), Continuous (f i)) →
    (LocallyFinite fun i => Function.mulSupport (f i)) → Continuous fun x => ∏ᶠ (i : ι), f i x
-- Mathlib.Data.List.Map2
List.zipLeft_cons_nil : ∀ {α : Type u} {β : Type v} (a : α) (as : List α), (a :: as).zipLeft [] = (a, none) :: List.map (fun a => (a, none)) as
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.instBEqKey.beq : Lean.Meta.RefinedDiscrTree.Key → Lean.Meta.RefinedDiscrTree.Key → Bool
-- Init.Data.UInt.BasicAux
/-- Decides whether one word-sized unsigned integer is strictly less than another. Usually accessed via
the `DecidableLT USize` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (6 : USize) < 7 then "yes" else "no") = "yes"`
 * `(if (5 : USize) < 5 then "yes" else "no") = "no"`
 * `show ¬((7 : USize) < 7) by decide`
 -/
USize.decLt : (a b : USize) → Decidable (a < b)
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- **Alias** of `FunLike.coe_neg`. -/
SlashInvariantForm.coe_neg : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Neg F] [inst_2 : Neg β]
  [IsNegApply F α β] (f : F), ⇑(-f) = -⇑f
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
/-- `Majorized f g exp` for real functions `f` and `g` means that for any `exp' > exp`,
`f =o[atTop] g ^ exp'`. This is used to define the `MultiseriesExpansion.Approximates` predicate.
The naming `Majorized` is non-standard because this notion is invented for the purposes of
this tactic, and does not exists in literature.  -/
Tactic.ComputeAsymptotics.Majorized : (ℝ → ℝ) → (ℝ → ℝ) → ℝ → Prop
-- Mathlib.Data.Matrix.Diagonal
Matrix.diag_map : ∀ {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {A : Matrix n n α}, (A.map f).diag = f ∘ A.diag
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.ι_plusCompIso_hom_assoc : ∀ {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] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_8 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] (X : Cᵒᵖ)
  (W : (J.Cover (Opposite.unop X))ᵒᵖ) {Z : E} (h : (J.plusObj (P.comp F)).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.colimit.ι (J.diagram P (Opposite.unop X)) W))
      (CategoryTheory.CategoryStruct.comp ((J.plusCompIso F P).hom.app X) h) =
    CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P (Opposite.unop X)).hom.app W)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (J.diagram (P.comp F) (Opposite.unop X)) W)
        h)
-- Mathlib.Data.Vector3
/-- Get the head of a nonempty vector.  -/
Vector3.head : {α : Type u_1} → {n : ℕ} → Vector3 α (n + 1) → α
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow.congr_simp : ∀ {A : Type u_1} [inst : CommSemiring A] (I I_1 : Ideal A),
  I = I_1 →
    ∀ {inst_1 : DecidablePred fun x => x ∈ I} [inst_2 : DecidablePred fun x => x ∈ I_1] (a a_1 : ℕ),
      a = a_1 →
        ∀ (a_2 a_3 : A),
          a_2 = a_3 →
            DividedPowers.OfInvertibleFactorial.dpow I a a_2 = DividedPowers.OfInvertibleFactorial.dpow I_1 a_1 a_3