mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z))
          (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x)))
        (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
        (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)))
      (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y))
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.append_Nonneg : ∀ (p₁ p₂ : Lean.Grind.Linarith.Poly), p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.append p₂).NonnegCoeffs
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.mk_surjective : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α}, Function.Surjective QuotientAddGroup.mk
-- Mathlib.Topology.Category.CompHausLike.SigmaComparison
CategoryTheory.Limits.opCoproductIsoProduct.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct Z],
  CategoryTheory.Limits.opCoproductIsoProduct Z =
    CategoryTheory.Limits.opCoproductIsoProduct' (CategoryTheory.Limits.coproductIsCoproduct Z)
      (CategoryTheory.Limits.productIsProduct fun x => Opposite.op (Z x))
-- Init.Data.Array.Lemmas
Array.uset.eq_1 : ∀ {α : Type u} (xs : Array α) (i : USize) (v : α) (h : i.toNat < xs.size), xs.uset i v h = xs.set i.toNat v h
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
/-- Continuity at a point can be read under left composition with an open partial homeomorphism if a
neighborhood of the initial point is sent to the source of the partial homeomorphism  -/
OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Z → X} {x : Z},
  f ⁻¹' e.source ∈ nhds x → (ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_finset_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {a : α} (b : β), a +ᵥ {b} = {a +ᵥ b}
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- Reinterpret an affine equivalence as a homeomorphism.  -/
AffineEquiv.toHomeomorphOfFiniteDimensional : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type w} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                [CompleteSpace 𝕜] →
                  {PE : Type u_1} →
                    {PF : Type u_2} →
                      [inst_6 : MetricSpace PE] →
                        [inst_7 : NormedAddTorsor E PE] →
                          [inst_8 : MetricSpace PF] →
                            [inst_9 : NormedAddTorsor F PF] → [FiniteDimensional 𝕜 E] → (PE ≃ᵃ[𝕜] PF) → PE ≃ₜ PF
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableOn_fst : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {s : Set (M × M')}, MDiff[s] Prod.fst
-- Mathlib.Data.Set.Prod
Set.EqOn.left_of_eqOn_prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {f f' : α → γ} {g g' : β → δ},
  Set.EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t) → t.Nonempty → Set.EqOn f f' s
-- Mathlib.RingTheory.PicardGroup
Submodule.range_unitsToPic : ∀ (R : Type u) (A : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A], (Submodule.unitsToPic R A).range = CommRing.relPic R A
-- Mathlib.Algebra.Group.Conj
ConjClasses.map.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Monoid α] [inst_1 : Monoid β] (f : α →* β),
  ConjClasses.map f = Quotient.lift (ConjClasses.mk ∘ ⇑f) ⋯
-- Lean.Util.Profile
/-- Print all profiling times (if any) to standard error.  -/
Lean.displayCumulativeProfilingTimes : BaseIO Unit
-- Mathlib.Order.Cover
/-- **Alias** of the reverse direction of `toDual_covBy_toDual_iff`. -/
CovBy.toDual : ∀ {α : Type u_1} [inst : LT α] {a b : α}, a ⋖ b → OrderDual.toDual b ⋖ OrderDual.toDual a
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_unitIso_hom_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₁ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).unitIso.hom.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
/-- The inverse of the derivative of `(extChartAt I x).symm` at the chart point,
applied to a tangent vector, gives back the tangent vector.  -/
mfderivWithin_extChartAt_symm_inverse_apply : ∀ {𝕜 : 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} (v : TangentSpace I x),
  (mfderiv[Set.range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x)).inverse v = v
-- Mathlib.Topology.Algebra.Group.Basic
continuousNeg_of_discreteTopology : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : Neg H] [DiscreteTopology H], ContinuousNeg H
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_monotone : Monotone ExpGrowth.expGrowthSup
-- Lean.Parser.Extra
Lean.ppAllowUngrouped.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The forgetful functor `AffineScheme ⥤ Scheme` creates small limits.  -/
AlgebraicGeometry.AffineScheme.createsLimitsForgetToScheme : CategoryTheory.CreatesLimits AlgebraicGeometry.AffineScheme.forgetToScheme
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestRevMatch_iff_isLongestRevMatch_beq : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch c pos ↔
    String.Slice.Pattern.Model.IsLongestRevMatch (fun x => x == c) pos
-- Mathlib.Data.Int.Init
Int.inductionOn'_sub_one : ∀ {motive : ℤ → Sort u_1} {z b : ℤ} {zero : motive b} {succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)}
  {pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)} (hz : z ≤ b),
  Int.inductionOn' (z - 1) b zero succ pred = pred z hz (Int.inductionOn' z b zero succ pred)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_center_iff : ∀ {R : Type u} [inst : NonUnitalRing R] {z : R}, z ∈ NonUnitalSubring.center R ↔ ∀ (g : R), g * z = z * g
-- Lean.Widget.InteractiveDiagnostic
/-- Some messages (in particular, traces) are too costly to print eagerly.
Instead, we allow the user to expand sub-traces interactively.  -/
Lean.Widget.MsgEmbed.trace : ℕ →
  Lean.Name →
    Lean.Widget.TaggedText Lean.Widget.MsgEmbed →
      Bool →
        Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
            (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
          Lean.Widget.MsgEmbed
-- Mathlib.RingTheory.Finiteness.Descent
RingHom.Finite.codescendsAlong_faithfullyFlat : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => RingHom.Finite) fun {R S} [CommRing R] [CommRing S] =>
  RingHom.FaithfullyFlat
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of the monomial `a*X^n` is `n` if `a ≠ 0`.  -/
PowerSeries.order_monomial_of_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (a : R), a ≠ 0 → ((PowerSeries.monomial n) a).order = ↑n
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.gamma_le_gamma : ∀ {a b : Ordinal.{u}}, a.gamma ≤ b.gamma ↔ a ≤ b
-- Lean.DocString.Markdown
/-- A means of transforming values into Markdown lines.
 -/
Lean.Doc.ToMarkdown : Type u → Type u
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.continuous_rng_of_principal : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)] {S : Set ι}
  {X : Type u_3} [inst_1 : TopologicalSpace X]
  {f : X → RestrictedProduct (fun i => R i) (fun i => A i) (Filter.principal S)},
  Continuous f ↔ Continuous (DFunLike.coe ∘ f)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.Hom.mk.sizeOf_spec : ∀ {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.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} [inst_5 : SizeOf C] [inst_6 : SizeOf D]
  (hom : M.X ⟶ N.X) [isModHom : CategoryTheory.IsModHom A hom],
  sizeOf { hom := hom, isModHom := isModHom } = 1 + sizeOf hom + sizeOf isModHom
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.map_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α}
  (target : Std.Sat.AIG.RefVec.MapTarget aig len) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Sat.AIG.RefVec.map aig target).aig.decls.size),
  (Std.Sat.AIG.RefVec.map aig target).aig.decls[idx] = aig.decls[idx]
-- Mathlib.ModelTheory.Order
/-- Any model of a theory of preorders is a preorder.  -/
FirstOrder.Language.preorderOfModels : (L : FirstOrder.Language) →
  (M : Type w') → [inst : L.IsOrdered] → [inst_1 : L.Structure M] → [h : M ⊨ L.preorderTheory] → Preorder M
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_iInf : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {ι : Sort u_5} [Nonempty ι] (f : M →ₙ+ N),
  Function.Injective ⇑f →
    ∀ (s : ι → AddSubsemigroup M), AddSubsemigroup.map f (iInf s) = ⨅ i, AddSubsemigroup.map f (s i)
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.coeff_truncate : ∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x : WittVector p R) (i : Fin n),
  TruncatedWittVector.coeff i ((WittVector.truncate n) x) = x.coeff ↑i
-- Mathlib.Algebra.Group.Basic
inv_div : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b : α), (a / b)⁻¹ = b / a
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
IsManifold.mem_maximalAtlas_iff_contMDiffOn : ∀ {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M]
  (φ : OpenPartialHomeomorph M H),
  φ ∈ IsManifold.maximalAtlas I n M ↔ ContMDiffOn I I n (↑φ) φ.source ∧ ContMDiffOn I I n (↑φ.symm) φ.target
-- Mathlib.Algebra.Central.Matrix
Algebra.IsCentral.matrix : ∀ (K : Type u_1) (D : Type u_2) [inst : CommSemiring K] [inst_1 : Semiring D] [inst_2 : Algebra K D]
  [Algebra.IsCentral K D] (ι : Type u_3) [inst_4 : Fintype ι] [inst_5 : DecidableEq ι],
  Algebra.IsCentral K (Matrix ι ι D)
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Clause.eval_congr : ∀ {α : Type u_1} (a1 a2 : α → Bool) (c : Std.Sat.CNF.Clause α),
  (∀ (i : α), Std.Sat.CNF.Clause.Mem i c → a1 i = a2 i) → Std.Sat.CNF.Clause.eval a1 c = Std.Sat.CNF.Clause.eval a2 c
-- Init.Data.SInt.Lemmas
instAssociativeISizeHMul : Std.Associative fun x1 x2 => x1 * x2
-- Batteries.Data.UInt
USize.toNat_ofNat_of_le_of_lt : ∀ {n i : ℕ}, n < USize.size → i ≤ n → (USize.ofNat i).toNat = i
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_eq_getD_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α}
  {fallback : β}, t.getD a fallback = t[a]?.getD fallback
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.homOfLE_comp_eqToHom_assoc : ∀ {X : Type u} [inst : Preorder X] {a b c : X} (hab : a ≤ b) (hbc : b = c) {Z : X} (h : c ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hab)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hbc) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE ⋯) h
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.comapAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_5} [inst_1 : AddGroup H] (f : G ≃+ H),
  f.comapAddSubgroup =
    { toFun := AddSubgroup.comap ↑f, invFun := AddSubgroup.comap ↑f.symm, left_inv := ⋯, right_inv := ⋯,
      map_rel_iff' := ⋯ }
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- `x ↦ fderiv 𝕜 (f x) (g x)` is smooth.  -/
ContDiff.fderiv : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {m n : WithTop ℕ∞} {f : E → F → G} {g : E → F},
  ContDiff 𝕜 m (Function.uncurry f) → ContDiff 𝕜 n g → n + 1 ≤ m → ContDiff 𝕜 n fun x => fderiv 𝕜 (f x) (g x)
-- Mathlib.SetTheory.Lists
Lists.of_toList : ∀ {α : Type u_1} {l : Lists α}, l.IsList → Lists.ofList l.toList = l
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.Compatible.anti : ∀ {α : Type u_1} {β : Type u_2} {G G₁ H H₁ : Graph α β}, G₁ ≤ G → H₁ ≤ H → G.Compatible H → G₁.Compatible H₁
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
/-- The definition of `stdGaussian` does not depend on the basis.  -/
ProbabilityTheory.stdGaussian_eq_map_pi_orthonormalBasis : ∀ {ι : Type u_1} [inst : Fintype ι] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace ℝ E]
  [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [BorelSpace E] (b : OrthonormalBasis ι ℝ E),
  ProbabilityTheory.stdGaussian E =
    MeasureTheory.Measure.map (fun x => ∑ i, x i • b i)
      (MeasureTheory.Measure.pi fun x => ProbabilityTheory.gaussianReal 0 1)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∪ t₂).contains k = (t₁.contains k || t₂.contains k)
-- Batteries.Lean.Meta.Basic
/-- Declare a metavariable. You must make sure that the metavariable is not already
declared.
 -/
Lean.MetavarContext.declareExprMVar : Lean.MetavarContext → Lean.MVarId → Lean.MetavarDecl → Lean.MetavarContext
-- Init.Core
/-- Heterogeneous equality with an `Eq.rec` application on the left is equivalent to a heterogeneous
equality on the original term.
 -/
eqRec_heq_iff : ∀ {β : Sort v} {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v} {b : α} {refl : motive a ⋯} {h : a = b} {c : β},
  h ▸ refl ≍ c ↔ refl ≍ c
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.instSupSet : {ι : Type u_1} → SupSet (AbstractSimplicialComplex ι)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpOptions.mk.inj : ∀ {toWorkDoneProgressOptions : Lean.Lsp.WorkDoneProgressOptions}
  {triggerCharacters? retriggerCharacters? : Option (Array String)}
  {toWorkDoneProgressOptions_1 : Lean.Lsp.WorkDoneProgressOptions}
  {triggerCharacters?_1 retriggerCharacters?_1 : Option (Array String)},
  { toWorkDoneProgressOptions := toWorkDoneProgressOptions, triggerCharacters? := triggerCharacters?,
        retriggerCharacters? := retriggerCharacters? } =
      { toWorkDoneProgressOptions := toWorkDoneProgressOptions_1, triggerCharacters? := triggerCharacters?_1,
        retriggerCharacters? := retriggerCharacters?_1 } →
    toWorkDoneProgressOptions = toWorkDoneProgressOptions_1 ∧
      triggerCharacters? = triggerCharacters?_1 ∧ retriggerCharacters? = retriggerCharacters?_1
-- Lean.Expr
/-- If `e` is of the form `(fun x₁ ... xₙ => f x₁ ... xₙ)` and `f` does not contain `x₁`, ..., `xₙ`,
then return `some f`. Otherwise, return `none`.

It assumes `e` does not have loose bound variables.

Remark: `ₙ` may be 0
 -/
Lean.Expr.etaExpanded? : Lean.Expr → Option Lean.Expr
-- Mathlib.LinearAlgebra.DFinsupp
/-- A family of additive subgroups over an additive group are independent if and only if
`DFinsupp.sumAddHom` applied with `AddSubgroup.subtype` is injective.  -/
iSupIndep_iff_dfinsuppSumAddHom_injective : ∀ {ι : Type u_1} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : AddCommGroup N] (p : ι → AddSubgroup N),
  iSupIndep p ↔ Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.addContent_union : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_2} [inst : AddCommMonoid G]
  {m : MeasureTheory.AddContent G C}, MeasureTheory.IsSetRing C → s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t
-- Mathlib.Analysis.Complex.LocallyUniformLimit
Complex.cderiv.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (r : ℝ) (f : ℂ → E) (z : ℂ),
  Complex.cderiv r f z = (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w
-- Lean.Data.Lsp.CodeActions
/-- [Reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#codeActionClientCapabilities)  -/
Lean.Lsp.CodeActionClientCapabilities : Type
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
/-- Any functor from the bounded below homotopy category has a right derived functor
with respect to quasi-isomorphisms.  -/
HomotopyCategory.Plus.instHasPointwiseRightDerivedFunctorQuasiIso : ∀ {C : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} H] [CategoryTheory.EnoughInjectives C]
  (F : CategoryTheory.Functor (HomotopyCategory.Plus C) H),
  F.HasPointwiseRightDerivedFunctor (HomotopyCategory.Plus.quasiIso C)
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.finite_of_indep_subset : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α}, M.IsRkFinite X → M.Indep I → I ⊆ X → I.Finite
-- Mathlib.Data.Fin.Tuple.Sort
/-- A permutation `σ` equals `sort f` if and only if the map `i ↦ (f (σ i), σ i)` is
strictly monotone (w.r.t. the lexicographic ordering on the target).  -/
Tuple.eq_sort_iff' : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)},
  σ = Tuple.sort f ↔ StrictMono ⇑(Equiv.trans σ (Tuple.graphEquiv₁ f))
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.congr_simp : ∀ (K : Type u_1) [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  (M : Type u_2) [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] (R : Type u_3) [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R], HahnEmbedding.Seed K M R = HahnEmbedding.Seed K M R
-- Init.Data.Iterators.Producers.Monadic.List
Std.Iterators.Types.ListIterator.mk.injEq : ∀ {α : Type w} (list list_1 : List α), ({ list := list } = { list := list_1 }) = (list = list_1)
-- Mathlib.Lean.Expr.Basic
/-- If `e` has a structure as type with field `fieldName`, `mkDirectProjection e fieldName` creates
the projection expression `e.fieldName`  -/
Lean.Expr.mkDirectProjection : Lean.Expr → Lean.Name → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.monic_leadingTerm : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (p : MvPolynomial σ R),
  m.Monic (m.leadingTerm p) ↔ m.Monic p
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Composition of morphisms for `WalkingMultispan`.  -/
CategoryTheory.Limits.WalkingMultispan.Hom.comp : {J : CategoryTheory.Limits.MultispanShape} →
  {A B C : CategoryTheory.Limits.WalkingMultispan J} → A.Hom B → B.Hom C → A.Hom C
-- Init.Data.Option.Lemmas
Option.pmap_congr : ∀ {α : Type u} {β : Type v} {p p' : α → Prop} (hp : ∀ (x : α), p x ↔ p' x) {f : (x : α) → p x → β}
  {f' : (x : α) → p' x → β},
  (∀ (x : α) (h : p' x), f x ⋯ = f' x h) →
    ∀ {o o' : Option α} (ho : o = o') {h : ∀ (x : α), o = some x → p x}, Option.pmap f o h = Option.pmap f' o' ⋯
-- Init.Data.List.Sublist
List.prefix_self_append_iff : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₃ ++ l₁ <+: l₃ ++ l₂ ↔ l₁ <+: l₂
-- Mathlib.Algebra.Notation.Defs
VAdd.ext_iff : ∀ {G : Type u} {P : Type v} {x y : VAdd G P}, x = y ↔ VAdd.vadd = VAdd.vadd
-- Mathlib.Tactic.Linter.UnusedInstancesInType
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.instToMessageDataParameter : Lean.ToMessageData Mathlib.Linter.UnusedInstancesInType.Parameter✝
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.Hom.ker_eq_top_iff_isEmpty : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y), f.ker = ⊤ ↔ IsEmpty ↥X
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_map_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃)
  (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) {X_1 Y : C₁} (f : X_1 ⟶ Y)
  (X_2 : C₂) (X_3 : C₃),
  (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).map f).app X_2).app X_3 =
    ((X.map (F₁.map f)).app (F₂.obj X_2)).app (F₃.obj X_3)
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.Martingale.predictablePart_eq_zero : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0} [CompleteSpace E],
  MeasureTheory.Martingale f ℱ μ → ∀ (n : ℕ), MeasureTheory.predictablePart f ℱ μ n =ᵐ[μ] 0
-- Mathlib.Topology.Order.Basic
/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(x, ∞)` is separated above from `f x` is countable. We give
here a version relative to a set `t`.  -/
countable_image_lt_image_Ioi_within : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : LinearOrder β] [SecondCountableTopology α] (t : Set β) (f : β → α),
  {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}.Countable
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_iSup : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Add M] (S : ι → AddSubsemigroup Mᵃᵒᵖ), (iSup S).unop = ⨆ i, (S i).unop
-- Mathlib.Analysis.Calculus.FDeriv.Congr
HasStrictFDerivAt.congr_fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' g' : E →L[𝕜] F} {x : E},
  HasStrictFDerivAt f f' x → f' = g' → HasStrictFDerivAt f g' x