mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (X Y : C) (f f_1 : X ⟶ Y),
  f = f_1 →
    ∀ (g g_1 : X ⟶ Y),
      g = g_1 →
        CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y f g =
          CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd X Y f_1 g_1
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedSimprocs.default : Lean.Meta.Simprocs
-- Mathlib.Order.Filter.AtTopBot.BigOperators
/-- Let `g : γ → β` be an injective function and `f : β → α` be a function from the codomain of `g`
to a commutative monoid. Suppose that `f x = 1` outside of the range of `g`. Then the filters
`atTop.map (fun s ↦ ∏ i ∈ s, f (g i))` and `atTop.map (fun s ↦ ∏ i ∈ s, f i)` coincide.

The additive version of this lemma is used to prove the equality `∑' x, f (g x) = ∑' y, f y` under
the same assumptions.  -/
Function.Injective.map_atTop_finsetProd_eq : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : CommMonoid M] {g : α → β},
  Function.Injective g →
    ∀ {f : β → M},
      (∀ x ∉ Set.range g, f x = 1) →
        Filter.map (fun s => ∏ i ∈ s, f (g i)) Filter.atTop = Filter.map (fun s => ∏ i ∈ s, f i) Filter.atTop
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Given expressions `y₁ y₂ : Q($M)` with specified signs (either + or -), construct a proof that
the product of (± `y₁`) and (± `y₂`) (here taking the specified signs) is ± `y₁ * y₂`; return this
proof and the computed sign.  -/
Mathlib.Tactic.FieldSimp.Sign.mul : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (y₁ y₂ : Q(«$M»)) →
        (g₁ g₂ : Mathlib.Tactic.FieldSimp.Sign M) →
          Lean.MetaM
            ((G : Mathlib.Tactic.FieldSimp.Sign M) ×
              have a := G.expr q(«$y₁» * «$y₂»);
              have a_1 := g₂.expr y₂;
              have a_2 := g₁.expr y₁;
              Q(«$a_2» * «$a_1» = «$a»))
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.ext_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : TopologicalSpace.Compacts α}, s = t ↔ ↑s = ↑t
-- Mathlib.Order.Category.DistLat
_private.Mathlib.Order.Category.DistLat.0.DistLat.Hom.mk.sizeOf_spec : ∀ {X Y : DistLat} (hom' : LatticeHom ↑X ↑Y), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instIsCharPUInt32OfNatNat : Lean.Grind.IsCharP UInt32 4294967296
-- Init.Data.List.Attach
List.getElem_attach : ∀ {α : Type u_1} {xs : List α} {i : ℕ} (h : i < xs.attach.length), xs.attach[i] = ⟨xs[i], ⋯⟩
-- Mathlib.Analysis.Analytic.Binomial
binomialSeries.eq_1 : ∀ {𝕂 : Type u} [inst : Field 𝕂] [inst_1 : CharZero 𝕂] (𝔸 : Type v) [inst_2 : Ring 𝔸] [inst_3 : Algebra 𝕂 𝔸]
  [inst_4 : TopologicalSpace 𝔸] [inst_5 : IsTopologicalRing 𝔸] (a : 𝕂),
  binomialSeries 𝔸 a = FormalMultilinearSeries.ofScalars 𝔸 fun x => Ring.choose a x
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Action of `iterateFrobenius` on the top field.  -/
IsPurelyInseparable.algebraMap_iterateFrobenius : ∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable.HasExponent K L] (p : ℕ) [inst_4 : ExpChar K p] {n : ℕ}
  (hn : IsPurelyInseparable.exponent K L ≤ n) (a : L),
  (algebraMap K L) ((IsPurelyInseparable.iterateFrobenius K L p hn) a) = a ^ p ^ n
-- Mathlib.Data.Num.ZNum
ZNum.of_intCast : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (n : ℤ), ↑↑n = ↑n
-- Init.Data.BitVec.Bitblast
BitVec.ushiftRightRec.eq_1 : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y 0 = x >>> (y &&& BitVec.twoPow w₂ 0)
-- Mathlib.FieldTheory.SeparableClosure
/-- If `K / E / F` is a field extension tower, such that `E / F` is separable, then
`separableClosure F K` is equal to `separableClosure E K`.  -/
separableClosure.eq_restrictScalars_of_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K] [Algebra.IsSeparable F E],
  separableClosure F K = IntermediateField.restrictScalars F (separableClosure E K)
-- Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
/-- We deduce that `N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ)`
reflects isomorphisms from the fact that
`N₁ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ)` does.  -/
AlgebraicTopology.DoldKan.instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  AlgebraicTopology.DoldKan.N₂.ReflectsIsomorphisms
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Non-dependent recursion principle for `AddLocalization`s: given elements `f a b : p`
for all `a b`, such that `r S (a, b) (c, d)` implies `f a b = f c d`,
then `f` is defined on the whole `Localization S`.  -/
AddLocalization.liftOn : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {p : Sort u} →
        AddLocalization S →
          (f : M → ↥S → p) → (∀ {a c : M} {b d : ↥S}, (AddLocalization.r S) (a, b) (c, d) → f a b = f c d) → p
-- Mathlib.Tactic.DepRewrite
/-- `rewrite!` is like `rewrite`,
but can also insert casts to adjust types that depend on the LHS of a rewrite.
It is available as an ordinary tactic and a `conv` tactic.

The sort of casts that are inserted is controlled by the `castMode` configuration option.
By default, only proof terms are casted;
by proof irrelevance, this adds no observable complexity.

With `rewrite! +letAbs (castMode := .all)`, casts are inserted whenever necessary.
This means that the 'motive is not type correct' error never occurs,
at the expense of creating potentially complicated terms.
 -/
Mathlib.Tactic.DepRewrite.depRewriteSeq : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.mem_bot : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {x : A},
  x ∈ ⊥ ↔ x ∈ Set.range ⇑(algebraMap R A)
-- Mathlib.LinearAlgebra.InvariantBasisNumber
nontrivial_of_invariantBasisNumber : ∀ (R : Type u) [inst : Semiring R] [InvariantBasisNumber R], Nontrivial R
-- Mathlib.Data.Set.Function
Set.bijOn_singleton : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {b : β}, Set.BijOn f {a} {b} ↔ f a = b
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.instEvalExprConfig.evalExpr : Lean.Expr → Lean.MetaM Lean.Try.Config
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` has distributive negation if `α` has.  -/
Filter.instDistribNeg : {α : Type u_2} → [inst : Mul α] → [HasDistribNeg α] → HasDistribNeg (Filter α)
-- Mathlib.Algebra.Algebra.Equiv
/-- Algebra equivalences are transitive.  -/
AlgEquiv.trans : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      {A₃ : Type uA₃} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A₁] →
            [inst_2 : Semiring A₂] →
              [inst_3 : Semiring A₃] →
                [inst_4 : Algebra R A₁] →
                  [inst_5 : Algebra R A₂] → [inst_6 : Algebra R A₃] → (A₁ ≃ₐ[R] A₂) → (A₂ ≃ₐ[R] A₃) → A₁ ≃ₐ[R] A₃
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.simp_suffix.inj : ∀ {lhs : Bool} {s : Lean.Grind.AC.Seq} {c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr} {lhs_1 : Bool} {s_1 : Lean.Grind.AC.Seq}
  {c₁_1 c₂_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.simp_suffix lhs s c₁ c₂ =
      Lean.Meta.Grind.AC.EqCnstrProof.simp_suffix lhs_1 s_1 c₁_1 c₂_1 →
    lhs = lhs_1 ∧ s = s_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.RingTheory.Artinian.Algebra
/-- Integral element of an algebra over Artinian ring `R` is either a zero divisor or a unit.  -/
IsArtinianRing.isUnit_iff_nonZeroDivisor_of_isIntegral : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [IsArtinianRing R] [inst_2 : Ring A] [inst_3 : Algebra R A] {a : A},
  IsIntegral R a → (IsUnit a ↔ a ∈ nonZeroDivisors A)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
/-- The underlying function of `Proj ℬ ⟶ Proj 𝒜` on the level of structure sheaves.  -/
AlgebraicGeometry.Proj.comapStructureSheafFun : {A : Type u_1} →
  {B : Type u_2} →
    {σ : Type u_4} →
      {τ : Type u_5} →
        [inst : CommRing A] →
          [inst_1 : SetLike σ A] →
            [inst_2 : AddSubgroupClass σ A] →
              [inst_3 : CommRing B] →
                [inst_4 : SetLike τ B] →
                  [inst_5 : AddSubgroupClass τ B] →
                    {𝒜 : ℕ → σ} →
                      {ℬ : ℕ → τ} →
                        [inst_6 : GradedRing 𝒜] →
                          [inst_7 : GradedRing ℬ] →
                            (f : 𝒜 →+*ᵍ ℬ) →
                              (hf :
                                  HomogeneousIdeal.irrelevant ℬ ≤
                                    HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) →
                                (U : TopologicalSpace.Opens (ProjectiveSpectrum 𝒜)) →
                                  (V : TopologicalSpace.Opens (ProjectiveSpectrum ℬ)) →
                                    V.carrier ⊆ ⇑(AlgebraicGeometry.ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier →
                                      ((x : ↥U) →
                                          HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toSubmodule) →
                                        (y : ↥V) → HomogeneousLocalization.AtPrime ℬ (↑y).asHomogeneousIdeal.toSubmodule
-- Mathlib.RingTheory.Smooth.Kaehler
tensorKaehlerQuotKerSqEquiv.congr_simp : ∀ (R : Type u_1) (P : Type u_2) (S : Type u_3) [inst : CommRing R] [inst_1 : CommRing P] [inst_2 : CommRing S]
  [inst_3 : Algebra R P] [inst_4 : Algebra P S] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R P S],
  tensorKaehlerQuotKerSqEquiv R P S = tensorKaehlerQuotKerSqEquiv R P S
-- Mathlib.Order.RelClasses
/-- Set notation form of `le_trans` -/
subset_trans : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b c : α}, a ⊆ b → b ⊆ c → a ⊆ c
-- Mathlib.RingTheory.Localization.Defs
/-- See note [partially-applied ext lemmas]  -/
IsLocalization.monoidHom_ext : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {P : Type u_4} [inst_4 : Monoid P] ⦃j k : S →* P⦄,
  j.comp ↑(algebraMap R S) = k.comp ↑(algebraMap R S) → j = k
-- Mathlib.Topology.Algebra.Group.Defs
IsTopologicalAddGroup.mk : ∀ {G : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [toContinuousAdd : ContinuousAdd G]
  [toContinuousNeg : ContinuousNeg G], IsTopologicalAddGroup G
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Coyoneda.coyoneda_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], CategoryTheory.coyoneda.Faithful
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_mem_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {t : Set 𝕜} {s : Set F} {x : 𝕜},
  derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
-- Std.Data.ExtTreeSet.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise `fallback`.
If they key is contained the result is guaranteed to be pointer equal to the key in the set.
 -/
Std.ExtTreeSet.getD : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → α → α
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.limNthHom.eq_1 : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R),
  PadicInt.limNthHom f_compat r = PadicInt.ofIntSeq (PadicInt.nthHom f r) ⋯
-- Init.Data.Range.Polymorphic.UInt
UInt16.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable UInt16
-- Mathlib.Data.List.Lookmap
_private.Mathlib.Data.List.Lookmap.0.List.replaceFTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (x : α) (xs : List α) (acc : Array α)
  (h_1 : (acc : Array α) → motive [] acc) (h_2 : (x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc),
  (match x :: xs, acc with
    | [], acc => h_1 acc
    | x :: xs, acc => h_2 x xs acc) =
    h_2 x xs acc
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharTwoNF.eq_1 : ∀ {F : Type u_2} [inst : Field F] (W : WeierstrassCurve F) [inst_1 : DecidableEq F],
  W.toCharTwoNF = if ha₁ : W.a₁ = 0 then W.toCharTwoJEqZeroNF else W.toCharTwoJNeZeroNF ha₁
-- Init.Control.Option
instToBoolOption : {α : Type u_1} → ToBool (Option α)
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.SuggestionText.string.sizeOf_spec : ∀ (a : String), sizeOf (Lean.Meta.Tactic.TryThis.SuggestionText.string a) = 1 + sizeOf a
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mk.injEq : ∀ {α : Type u_2} [inst : TopologicalSpace α] (carrier : Set α) (is_open' : IsOpen carrier) (carrier_1 : Set α)
  (is_open'_1 : IsOpen carrier_1),
  ({ carrier := carrier, is_open' := is_open' } = { carrier := carrier_1, is_open' := is_open'_1 }) =
    (carrier = carrier_1)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.isUnramified : ∀ (k : Type u_1) [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  [IsUnramifiedAtInfinitePlaces k K] (w : NumberField.InfinitePlace K), NumberField.InfinitePlace.IsUnramified k w
-- Mathlib.Probability.Distributions.Gaussian.Fernique
/-- Characteristic function of a centered Gaussian measure.
For a Gaussian measure, the hypothesis `∀ L : StrongDual ℝ E, μ[L] = 0` is equivalent to the simpler
`μ[id] = 0`, but at this point we don't know yet that `μ` has a first moment so we can't use it.
See `charFunDual_eq_of_integral_eq_zero`  -/
ProbabilityTheory.IsGaussian.charFunDual_eq_of_forall_strongDual_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ],
  (∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0) →
    ∀ (L : StrongDual ℝ E), MeasureTheory.charFunDual μ L = Complex.exp (-↑(ProbabilityTheory.variance (⇑L) μ) / 2)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : C) (a : T.obj A ⟶ A)
  (unit :
    autoParam (CategoryTheory.CategoryStruct.comp (T.η.app A) a = CategoryTheory.CategoryStruct.id A)
      CategoryTheory.Monad.Algebra.unit._autoParam)
  (assoc :
    autoParam (CategoryTheory.CategoryStruct.comp (T.μ.app A) a = CategoryTheory.CategoryStruct.comp (T.map a) a)
      CategoryTheory.Monad.Algebra.assoc._autoParam)
  (A_1 : C) (a_1 : T.obj A_1 ⟶ A_1)
  (unit_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (T.η.app A_1) a_1 = CategoryTheory.CategoryStruct.id A_1)
      CategoryTheory.Monad.Algebra.unit._autoParam)
  (assoc_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (T.μ.app A_1) a_1 = CategoryTheory.CategoryStruct.comp (T.map a_1) a_1)
      CategoryTheory.Monad.Algebra.assoc._autoParam),
  ({ A := A, a := a, unit := unit, assoc := assoc } = { A := A_1, a := a_1, unit := unit_1, assoc := assoc_1 }) =
    (A = A_1 ∧ a ≍ a_1)
-- Mathlib.LinearAlgebra.StdBasis
Pi.basis_repr : ∀ {R : Type u_2} {η : Type u_4} {ιs : η → Type u_5} {Ms : η → Type u_6} [inst : Semiring R]
  [inst_1 : (i : η) → AddCommMonoid (Ms i)] [inst_2 : (i : η) → Module R (Ms i)] [inst_3 : Fintype η]
  (s : (j : η) → Module.Basis (ιs j) R (Ms j)) (x : (j : η) → Ms j) (ji : (j : η) × ιs j),
  ((Pi.basis s).repr x) ji = ((s ji.fst).repr (x ji.fst)) ji.snd
-- Mathlib.Analysis.Analytic.Linear
_private.Mathlib.Analysis.Analytic.Linear.0.ContinuousLinearMap.fpowerSeriesBilinear.match_1.eq_4 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : (x : ℕ) → motive x),
  (x = 0 → False) →
    (x = 1 → False) →
      (x = 2 → False) →
        (match x with
          | 0 => h_1 ()
          | 1 => h_2 ()
          | 2 => h_3 ()
          | x => h_4 x) =
          h_4 x
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_lt_of_lt_mul' : ∀ {a b c : ENNReal}, a < b * c → a / b < c
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKey?_modifyKey_eq_minKey? : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α]
  {k : α} {f : β → β} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.minKey? (Std.Internal.List.Const.modifyKey k f l) = Std.Internal.List.minKey? l
-- Mathlib.Data.Int.Bitwise
Int.testBit_bit_succ : ∀ (m : ℕ) (b : Bool) (n : ℤ), (Int.bit b n).testBit m.succ = n.testBit m
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_eq_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {a : α}, a ∉ t → t.get! a = default
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.injective : ∀ {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E₂] [inst_3 : Module R₂ E₂] [inst_4 : NormedAddCommGroup F]
  [inst_5 : Module R F] (f₁ : F →ₛₗᵢ[σ₁₂] E₂), Function.Injective ⇑f₁
-- Init.MethodSpecsSimp
SMul.smul_eq_hSMul : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β], SMul.smul = HSMul.hSMul
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.underToAlgebra_map_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  {X_1 Y : CategoryTheory.Under X} (g : X_1 ⟶ Y),
  ((CategoryTheory.underToAlgebra X).map g).f = CategoryTheory.Under.Hom.right g
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.find?_toArray_eq_some_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, Array.find? (fun x_2 => x_2.fst == k) m.toArray = some ⟨k, v⟩ ↔ m.get? k = some v
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- The objects over `X i` for all `i`  -/
CategoryTheory.Pseudofunctor.DescentData.obj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} → {f : (i : ι) → X i ⟶ S} → F.DescentData f → (i : ι) → ↑(F.obj { as := Opposite.op (X i) })
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.eval_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} {h : b ⟶ c} {η η' : f ⟶ g}
  {θ : CategoryTheory.CategoryStruct.comp f h ⟶ CategoryTheory.CategoryStruct.comp g h},
  η = η' → CategoryTheory.Bicategory.whiskerRight η' h = θ → CategoryTheory.Bicategory.whiskerRight η h = θ
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.NormNum.Finset.prod_empty : ∀ {β : Type u_1} {α : Type u_2} [inst : CommSemiring β] (f : α → β), Mathlib.Meta.NormNum.IsNat (∅.prod f) 1
-- Mathlib.Data.Finsupp.Weight
Finsupp.degree_preimage_nsmul : ∀ {σ : Type u_5} (s : Set ℕ) (n : ℕ), n ≠ 0 → ⇑Finsupp.degree ⁻¹' (n • s) = n • ⇑Finsupp.degree ⁻¹' s
-- Batteries.Data.List.Perm
List.subset_cons_diff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α}, (a :: l₁).diff l₂ ⊆ a :: l₁.diff l₂
-- Init.Core
DoResultSBC.break.sizeOf_spec : ∀ {α σ : Type u} [inst : SizeOf α] [inst_1 : SizeOf σ] (a : σ), sizeOf (DoResultSBC.break a) = 1 + sizeOf a
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.contractibleTriangleFunctor_map_hom₂ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.contractibleTriangleFunctor C).map f).hom₂ = f
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.comp_obj : ∀ {U : Type u_1} [inst : CategoryTheory.ReflQuiver U] {V : Type u_2} [inst_1 : CategoryTheory.ReflQuiver V]
  {W : Type u_3} [inst_2 : CategoryTheory.ReflQuiver W] (F : U ⥤rq V) (G : V ⥤rq W) (X : U),
  (F ⋙rq G).obj X = G.obj (F.obj X)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
_private.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital.0.termσₙ : Lean.ParserDescr
-- Mathlib.Order.UpperLower.Hom
/-- `UpperSet.Ici` as a `sSupHom`.  -/
UpperSet.icisSupHom : {α : Type u_1} → [inst : CompleteLattice α] → sSupHom α (UpperSet α)
-- Lean.Server.ServerTask
Lean.Server.ServerTask.EIO.bindTaskCostly : {α : Type u_1} →
  {ε β : Type} →
    Lean.Server.ServerTask α →
      (α → EIO ε (Lean.Server.ServerTask (Except ε β))) → BaseIO (Lean.Server.ServerTask (Except ε β))
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.ι_comp_colimitRightOpIsoUnopLimit_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : J) {Z : Cᵒᵖ}
  (h : Opposite.op (CategoryTheory.Limits.limit F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.rightOp j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitRightOpIsoUnopLimit F).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F (Opposite.op j)).op h
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.toMultilinearMap_smul : ∀ {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : (i : ι) → AddCommMonoid (M₁ i)] [inst_1 : AddCommMonoid M₂]
  [inst_2 : (i : ι) → TopologicalSpace (M₁ i)] [inst_3 : TopologicalSpace M₂] {R' : Type u_1} {A : Type u_3}
  [inst_4 : Semiring A] [inst_5 : (i : ι) → Module A (M₁ i)] [inst_6 : Module A M₂] [inst_7 : DistribSMul R' M₂]
  [inst_8 : ContinuousConstSMul R' M₂] [inst_9 : SMulCommClass A R' M₂] (c : R') (f : ContinuousMultilinearMap A M₁ M₂),
  (c • f).toMultilinearMap = c • f.toMultilinearMap
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital normed ring is a non-unital seminormed ring.  -/
NonUnitalNormedRing.toNonUnitalSeminormedRing : {α : Type u_2} → [β : NonUnitalNormedRing α] → NonUnitalSeminormedRing α
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenCGraph.inter : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → Set β},
  HasOpenCGraph f → HasOpenCGraph g → HasOpenCGraph fun x => f x ∩ g x
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instMonoCoprodScheme : CategoryTheory.Limits.MonoCoprod AlgebraicGeometry.Scheme
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.pointwiseProductCompEvaluation_hom_app : ∀ {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] {α : Type u_3} {I : α → Type u_4}
  [inst_2 : (i : α) → CategoryTheory.Category.{u_5, u_4} (I i)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
  (F : (i : α) → CategoryTheory.Functor (I i) (CategoryTheory.Functor D C)) (d : D) (X : (i : α) → I i),
  (CategoryTheory.Limits.pointwiseProductCompEvaluation F d).hom.app X =
    (CategoryTheory.Limits.piObjIso ((CategoryTheory.Functor.pi F).obj X) d).hom
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- If `a` = ± `b`, `b = C * d`, and `d = e`, construct a proof that `a` = `C` * ± `e`.  -/
Mathlib.Tactic.FieldSimp.Sign.mkEqMul : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      {a b C d e : Q(«$M»)} →
        {g : Mathlib.Tactic.FieldSimp.Sign M} →
          (have a_1 := g.expr b;
            Q(«$a» = «$a_1»)) →
            Q(«$b» = «$C» * «$d») →
              Q(«$d» = «$e») →
                Lean.MetaM
                  (have a_1 := g.expr e;
                  Q(«$a» = «$C» * «$a_1»))