mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.deriv_cgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ},
  v ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    deriv (ProbabilityTheory.cgf X μ) v =
      (∫ (x : Ω), (fun ω => X ω * Real.exp (v * X ω)) x ∂μ) / ProbabilityTheory.mgf X μ v
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_eq_mul_inv : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] (I : FractionalIdeal (nonZeroDivisors B) L),
  FractionalIdeal.dual A K I = FractionalIdeal.dual A K 1 * I⁻¹
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalAnyGoals : Lean.Elab.Tactic.Tactic
-- Mathlib.Analysis.Convex.Birkhoff
/-- **Birkhoff's theorem**
The set of doubly stochastic matrices is the convex hull of the permutation matrices.  Note
`exists_eq_sum_perm_of_mem_doublyStochastic` gives a convex weighting of each permutation matrix
directly.  To show `doublyStochastic n` is convex, use `convex_doublyStochastic`.
 -/
doublyStochastic_eq_convexHull_permMatrix : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Field R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R], ↑(doublyStochastic R n) = (convexHull R) {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}
-- Mathlib.NumberTheory.FrobeniusNumber
/-- **Alias** of `Nat.finite_setOfPred_setGcd_dvd_and_mem_span`. -/
Nat.finite_setOf_setGcd_dvd_and_mem_span : ∀ (s : Set ℕ), {n | Nat.setGcd s ∣ n ∧ n ∉ Ideal.span s}.Finite
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap_fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) {Z : C} (h : HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj X)
      (CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap f) h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj Y) h)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V] [inst_4 : SizeOf C]
  [inst_5 : SizeOf V] (functor : CategoryTheory.Functor C V), sizeOf { functor := functor } = 1 + sizeOf functor
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
/-- The morphism `(toColon Φ Ψ)` is an isomorphism if and only if `Φ.quotient ⋙ Ψ.r` is the zero
object.  -/
CategoryTheory.Abelian.Preradical.isIso_toColon_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {Φ Ψ : CategoryTheory.Abelian.Preradical C},
  CategoryTheory.IsIso (Φ.toColon Ψ) ↔ CategoryTheory.Limits.IsZero (Φ.quotient.comp Ψ.r)
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.Path.root.sizeOf_spec : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} (x : P.last.M) (a : P.A) (f : P.last.B a → P.last.M) (h : x.dest = ⟨a, f⟩)
  (i : Fin2 n) (c : P.drop.B a i),
  sizeOf (MvPFunctor.M.Path.root x a f h i c) = 1 + sizeOf x + sizeOf a + sizeOf h + sizeOf i + sizeOf c
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.IsSFiniteKernel.add : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ η : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η], ProbabilityTheory.IsSFiniteKernel (κ + η)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.IsMonoidal.whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F₁ : CategoryTheory.Functor C D} [inst_6 : F₁.LaxMonoidal] {G₁ G₂ : CategoryTheory.Functor D E}
  [inst_7 : G₁.LaxMonoidal] [inst_8 : G₂.LaxMonoidal] (τ' : G₁ ⟶ G₂) [CategoryTheory.NatTrans.IsMonoidal τ'],
  CategoryTheory.NatTrans.IsMonoidal (F₁.whiskerLeft τ')
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.rel : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (self : c.Embedding c') {i₁ i₂ : ι},
  c.Rel i₁ i₂ → c'.Rel (self.f i₁) (self.f i₂)
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.forwardMatches.inj : ∀ {ms ms_1 : Array Aesop.ForwardRuleMatch},
  Aesop.RuleTacDescr.forwardMatches ms = Aesop.RuleTacDescr.forwardMatches ms_1 → ms = ms_1
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_add_single_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {n : ℕ} [NeZero n] {m : σ →₀ ℕ} (a : R) (i : σ),
  MvPolynomial.coeff (m + fun₀ | i => n) (MvPolynomial.C a) = 0
-- Init.Data.UInt.Lemmas
UInt32.eq_sub_iff_add_eq : ∀ {a b c : UInt32}, a = c - b ↔ a + b = c
-- Mathlib.Analysis.SpecificLimits.Normed
/-- The **alternating series test** for monotone sequences.
See also `Monotone.tendsto_alternating_series_of_tendsto_zero`.  -/
Monotone.cauchySeq_alternating_series_of_tendsto_zero : ∀ {f : ℕ → ℝ},
  Monotone f → Filter.Tendsto f Filter.atTop (nhds 0) → CauchySeq fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i
-- Mathlib.Data.Finsupp.Notation
/-- Unexpander for the `fun₀ | i => x` notation.  -/
Finsupp.singleUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.inertia_map_subtype : ∀ {M : Type u_6} [inst : AddGroup M] (I : AddSubgroup M) {G : Type u_7} [inst_1 : Group G] [inst_2 : MulAction G M]
  (H : Subgroup G), Subgroup.map H.subtype (I.inertia ↥H) = I.inertia G ⊓ H
-- Mathlib.Algebra.Star.Basic
Ring.inverse_star : ∀ {R : Type u} [inst : Semiring R] [inst_1 : StarRing R] (a : R), Ring.inverse (star a) = star (Ring.inverse a)
-- Mathlib.Data.Set.Finite.Basic
Set.finite_le_nat : ∀ (n : ℕ), {i | i ≤ n}.Finite
-- Lean.Parser.Level
Lean.Parser.Level.ident.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.connected_induce_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), (SimpleGraph.induce {v_1 | v_1 ∈ p.support} G).Connected
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Eta-expanded form of `MeasureTheory.AEStronglyMeasurable.const_vadd` -/
MeasureTheory.AEStronglyMeasurable.fun_const_vadd : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {𝕜 : Type u_5} [inst_1 : VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : 𝕜), MeasureTheory.AEStronglyMeasurable (fun i => c +ᵥ f i) μ
-- Mathlib.Tactic.Ring.Common
/-- Cast `ExProd btℕ sℕ` to `ExProdNat`.  -/
Mathlib.Tactic.Ring.Common.ExProd.toExProdNat : (e : Q(ℕ)) →
  Mathlib.Tactic.Ring.Common.ExProd Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ e →
    (e' : Q(ℕ)) × Mathlib.Tactic.Ring.Common.ExProdNat e'
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
ValueDistribution.characteristic.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (a : WithTop E),
  ValueDistribution.characteristic f a = ValueDistribution.proximity f a + ValueDistribution.logCounting f a
-- Init.Data.UInt.Bitwise
UInt16.toUInt64_shiftRight : ∀ (a b : UInt16), (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % 16)
-- Mathlib.RingTheory.Nilpotent.Basic
Commute.isNilpotent_add : ∀ {R : Type u_1} {x y : R} [inst : Semiring R], Commute x y → IsNilpotent x → IsNilpotent y → IsNilpotent (x + y)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → CategoryTheory.Category.{max v u_1, max (max u v) (u_1 + 1)} (CategoryTheory.PreZeroHypercover S)
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.IsUniform.toMeasurable : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} {x : MeasurableSpace Ω}
  {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E},
  MeasureTheory.pdf.IsUniform X s ℙ μ → MeasureTheory.pdf.IsUniform X (MeasureTheory.toMeasurable μ s) ℙ μ
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalCore.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G),
  H.normalCore = { carrier := {a | ∀ (b : G), b * a * b⁻¹ ∈ H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.ofPointIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit r)
  [i : CategoryTheory.IsIso (P.lift t)], P.ofPointIso = P.ofIsoLimit (CategoryTheory.asIso (P.liftConeMorphism t)).symm
-- Init.Data.List.Lemmas
List.getElem!_of_getElem? : ∀ {α : Type u_1} {a : α} [inst : Inhabited α] {l : List α} {i : ℕ}, l[i]? = some a → l[i]! = a
-- Init.Internal.Order.MonadTail
Lean.Order.instMonadTailStateRefT' : {ω σ : Type} → {m : Type → Type} → [inst : Monad m] → [Lean.Order.MonadTail m] → Lean.Order.MonadTail (StateRefT' ω σ m)
-- Lean.PrettyPrinter.Delaborator.Metavariable
_private.Lean.PrettyPrinter.Delaborator.Metavariable.0.Lean.PrettyPrinter.Delaborator.describeMVar.extraLCtxVars : Lean.MetavarDecl → Lean.MetaM String
-- Init.Data.Vector.Attach
Vector.attachWith_map : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : α → β} {P : β → Prop} (H : ∀ b ∈ Vector.map f xs, P b),
  (Vector.map f xs).attachWith P H =
    Vector.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, h⟩)
      (xs.attachWith (P ∘ f) ⋯)
-- Init.Data.Nat.Basic
Nat.sub_one_lt_of_lt : ∀ {n m : ℕ}, m < n → n - 1 < n
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- The set of right differentiability points of a function taking values in a complete space is
Borel-measurable.  -/
measurableSet_of_differentiableWithinAt_Ici : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [CompleteSpace F],
  MeasurableSet {x | DifferentiableWithinAt ℝ f (Set.Ici x) x}
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.commute_coe_coe : ∀ {S : Type u_4} {M : Type u_5} [inst : Mul M] [inst_1 : SetLike S M] [inst_2 : MulMemClass S M] {s : S} {x y : ↥s},
  Commute ↑x ↑y ↔ Commute x y
-- Mathlib.Data.Set.Card
Set.encard_ne_top_iff : ∀ {α : Type u_1} {s : Set α}, s.encard ≠ ⊤ ↔ s.Finite
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.coconeOfLocallyDirected_ι : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected],
  𝒰.coconeOfLocallyDirected.ι = 𝒰.functorOfLocallyDirectedHomBase
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero : ∀ (σ : Type u_1) [inst : Fintype σ] (R : Type u_2) [inst_1 : CommRing R],
  ∑ a ∈ Finset.HasAntidiagonal.antidiagonal (Fintype.card σ),
      (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2 =
    0
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- **Alias** of the forward direction of `hasProdUniformlyOn_iff_tendstoUniformlyOn`. -/
HasProdUniformlyOn.tendstoUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α],
  HasProdUniformlyOn f g s → TendstoUniformlyOn (fun x1 x2 => ∏ i ∈ x1, f i x2) g Filter.atTop s
-- Mathlib.CategoryTheory.Monoidal.Transport
/-- Transport a monoidal structure along an equivalence of (plain) categories.
 -/
CategoryTheory.Monoidal.transport : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} → [inst_2 : CategoryTheory.Category.{v₂, u₂} D] → (C ≌ D) → CategoryTheory.MonoidalCategory D
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.le_u_l : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ (a : α), a ≤ u (l a)
-- Init.Data.Dyadic.Basic
Dyadic.instAdd : Add Dyadic
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.mk.inj : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} {inst : Ring R} {inst_1 : AddCommGroup V}
  {inst_2 : Module R V} {inst_3 : TopologicalSpace P} {inst_4 : AddTorsor V P} {inst_5 : AddCommGroup W}
  {inst_6 : Module R W} {inst_7 : TopologicalSpace Q} {inst_8 : AddTorsor W Q} {toAffineMap : P →ᵃ[R] Q}
  {cont : Continuous toAffineMap.toFun} {toAffineMap_1 : P →ᵃ[R] Q} {cont_1 : Continuous toAffineMap_1.toFun},
  { toAffineMap := toAffineMap, cont := cont } = { toAffineMap := toAffineMap_1, cont := cont_1 } →
    toAffineMap = toAffineMap_1
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : C) (n m : ℤ)
  (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app._auto_1) {Z : Cᵒᵖᵒᵖ}
  (h : (CategoryTheory.shiftFunctor Cᵒᵖᵒᵖ n).obj ((CategoryTheory.opOp C).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (CategoryTheory.opOp C) n).hom.app X) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).hom.app (Opposite.op X)).op
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app (Opposite.op (Opposite.op X))) h)
-- Mathlib.Order.SuccPred.Basic
Order.covBy_succ_of_not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α}, ¬IsMax a → a ⋖ Order.succ a
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If the product comparison morphism is an iso, its inverse is natural.  -/
CategoryTheory.Limits.prodComparison_inv_natural_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A A' B B' : C} [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct A' B']
  [inst_4 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)]
  [inst_5 : CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B')
  [inst_6 : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)]
  [inst_7 : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A' B')] {Z : D} (h : F.obj (A' ⨯ B') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B))
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.prod.map f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (F.map f) (F.map g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A' B')) h)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (∀ a ∈ t, (List.map Prod.fst l).contains a = false) → (t.insertMany l).size = t.size + l.length
-- Batteries.Data.Float.Lemmas
/-- This theorem is true for all types but most other types have `LawfulBEq` where
`bne_self_eq_false` or `bne_iff_ne` apply.
 -/
Float.bne_eq : ∀ {f : Float}, (f != f) = !f == f
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOf.mk.sizeOf_spec : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  {i : M →ₗ[R] N} {f : M →ₗ[R] Q} [inst_7 : SizeOf R] [inst_8 : SizeOf Q] [inst_9 : SizeOf M] [inst_10 : SizeOf N]
  (toLinearPMap : N →ₗ.[R] Q) (le : i.range ≤ toLinearPMap.domain)
  (is_extension : ∀ (m : M), f m = ↑toLinearPMap ⟨i m, ⋯⟩),
  sizeOf { toLinearPMap := toLinearPMap, le := le, is_extension := is_extension } = 1 + sizeOf toLinearPMap
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {fallback : α} {hc : t.maxKeyD fallback ∈ t}, t.getKey (t.maxKeyD fallback) hc = t.maxKeyD fallback
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_addEquiv_trans : ∀ {R : Type u_4} {S : Type u_5} {S' : Type u_6} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S]
  [inst_4 : Mul S'] [inst_5 : Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S'), ↑(e₁.trans e₂) = (↑e₁).trans ↑e₂
-- Init.Data.Int.Order
Int.instLawfulOrderLeftLeaningMax : Std.LawfulOrderLeftLeaningMax ℤ
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.coe_symm : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  (equiv : S.Equiv S'), (↑equiv).symm = ↑equiv.symm
-- Mathlib.Topology.Maps.Proper.Basic
/-- The preimage of a compact set by a proper map is again compact. See also
`isProperMap_iff_isCompact_preimage` which proves that this property completely characterizes
proper map when the codomain is compactly generated and Hausdorff.  -/
IsProperMap.isCompact_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsProperMap f → ∀ {K : Set Y}, IsCompact K → IsCompact (f ⁻¹' K)
-- Mathlib.Data.NNReal.Defs
NNReal.instConditionallyCompleteLinearOrderBot : ConditionallyCompleteLinearOrderBot NNReal
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.stalkMap_toStalk : ∀ {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑S),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.StructureSheaf.toStalk (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p))
      (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom p) =
    CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.StructureSheaf.toStalk (↑S) p)
-- Mathlib.RingTheory.Etale.Kaehler
/-- If `P → Q` is formally étale, then `T ⊗ₛ (S ⊗ₚ Ω[P/R]) ≃ T ⊗_Q Ω[Q/R]`.  -/
Algebra.Extension.tensorCotangentSpaceOfFormallyEtale : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] →
                  [IsScalarTower R S T] →
                    {P : Algebra.Extension R S} →
                      {Q : Algebra.Extension R T} →
                        (f : P.Hom Q) →
                          f.toRingHom.FormallyEtale → TensorProduct S T P.CotangentSpace ≃ₗ[T] Q.CotangentSpace
-- Init.Data.Dyadic.Inv
/-- `invAtPrec x prec` is the unique dyadic with precision at most `prec` satisfying
both `_ * x ≤ 1` and `1 < (_ + ofIntWithPrec 1 prec) * x`, for `0 < x`.
 -/
Dyadic.eq_invAtPrec : ∀ {x : Dyadic},
  0 < x →
    ∀ {prec : ℤ} {y : Dyadic},
      y.precision ≤ some prec → y * x ≤ 1 → 1 < (y + Dyadic.ofIntWithPrec 1 prec) * x → y = x.invAtPrec prec
-- Mathlib.Data.Vector3
Vector3.append_cons : ∀ {α : Type u_1} {m n : ℕ} (a : α) (v : Vector3 α m) (w : Vector3 α n),
  (Vector3.cons a v).append w = Vector3.cons a (v.append w)
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- A loop is an edge whose associated vertex subset consists of a single vertex.  -/
Hypergraph.IsLoop : {α : Type u_1} → Hypergraph α → Set α → Prop
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
Lex.instSemigroupWithZero : {α : Type u_1} → [SemigroupWithZero α] → SemigroupWithZero (Lex α)
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.dual_map : ∀ {X Y : PartOrdEmb} (f : X ⟶ Y), PartOrdEmb.dual.map f = PartOrdEmb.ofHom (PartOrdEmb.Hom.hom f).dual
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr.eq_5 : ∀ (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr q.copy =
    Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.rev
      (Turing.TM2.Stmt.branch Option.isSome
        (Turing.PartrecToTM2.push' Turing.PartrecToTM2.K'.main
          (Turing.PartrecToTM2.push' Turing.PartrecToTM2.K'.stack (Turing.TM2.Stmt.goto fun x => q.copy)))
        (Turing.TM2.Stmt.goto fun x => q))
-- Mathlib.RingTheory.Etale.Kaehler
Algebra.Extension.Hom.mapKer.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] (f : P.Hom P')
  [alg : Algebra P.Ring P'.Ring] (halg : algebraMap P.Ring P'.Ring = f.toRingHom),
  f.mapKer halg = { toFun := fun x => ⟨f.toRingHom ↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
-- Init.Data.Vector.Basic
Vector.foldl : {β : Type u_1} → {α : Type u_2} → {n : ℕ} → (β → α → β) → β → Vector α n → β
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft_mop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {c c' : C} (f : c ⟶ c') (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f.mop d =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.bilinearComp.congr_simp : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  {E' : Type u_11} {F' : Type u_12} [inst_9 : SeminormedAddCommGroup E'] [inst_10 : SeminormedAddCommGroup F']
  {𝕜₁' : Type u_13} {𝕜₂' : Type u_14} [inst_11 : NontriviallyNormedField 𝕜₁'] [inst_12 : NontriviallyNormedField 𝕜₂']
  [inst_13 : NormedSpace 𝕜₁' E'] [inst_14 : NormedSpace 𝕜₂' F'] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂}
  {σ₂₃' : 𝕜₂' →+* 𝕜₃} [inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃']
  [inst_17 : RingHomIsometric σ₂₃] [inst_18 : RingHomIsometric σ₁₃'] [inst_19 : RingHomIsometric σ₂₃']
  (f f_1 : E →SL[σ₁₃] F →SL[σ₂₃] G),
  f = f_1 →
    ∀ (gE gE_1 : E' →SL[σ₁'] E),
      gE = gE_1 → ∀ (gF gF_1 : F' →SL[σ₂'] F), gF = gF_1 → f.bilinearComp gE gF = f_1.bilinearComp gE_1 gF_1